-
Notifications
You must be signed in to change notification settings - Fork 0
/
Value.thy
112 lines (85 loc) · 4.23 KB
/
Value.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
section\<open>Values\<close>
text\<open>Our EFSM implementation can currently handle integers and strings. Here we define a sum type
which combines these. We also define an arithmetic in terms of values such that EFSMs do not need
to be strongly typed.\<close>
theory Value
imports Trilean
begin
text_raw\<open>\snip{valuetype}{1}{2}{%\<close>
datatype "value" = Num int | Str String.literal
text_raw\<open>}%endsnip\<close>
fun is_Num :: "value \<Rightarrow> bool" where
"is_Num (Num _) = True" |
"is_Num (Str _) = False"
text_raw\<open>\snip{maybeIntArith}{1}{2}{%\<close>
fun maybe_arith_int :: "(int \<Rightarrow> int \<Rightarrow> int) \<Rightarrow> value option \<Rightarrow> value option \<Rightarrow> value option" where
"maybe_arith_int f (Some (Num x)) (Some (Num y)) = Some (Num (f x y))" |
"maybe_arith_int _ _ _ = None"
text_raw\<open>}%endsnip\<close>
lemma maybe_arith_int_not_None:
"maybe_arith_int f a b \<noteq> None = (\<exists>n n'. a = Some (Num n) \<and> b = Some (Num n'))"
using maybe_arith_int.elims maybe_arith_int.simps(1) by blast
lemma maybe_arith_int_Some:
"maybe_arith_int f a b = Some (Num x) = (\<exists>n n'. a = Some (Num n) \<and> b = Some (Num n') \<and> f n n' = x)"
using maybe_arith_int.elims maybe_arith_int.simps(1) by blast
lemma maybe_arith_int_None:
"(maybe_arith_int f a1 a2 = None) = (\<nexists>n n'. a1 = Some (Num n) \<and> a2 = Some (Num n'))"
using maybe_arith_int_not_None by blast
lemma maybe_arith_int_Not_Num:
"(\<forall>n. maybe_arith_int f a1 a2 \<noteq> Some (Num n)) = (maybe_arith_int f a1 a2 = None)"
by (metis maybe_arith_int.elims option.distinct(1))
lemma maybe_arith_int_never_string: "maybe_arith_int f a b \<noteq> Some (Str x)"
using maybe_arith_int.elims by blast
definition "value_plus = maybe_arith_int (+)"
lemma value_plus_never_string: "value_plus a b \<noteq> Some (Str x)"
by (simp add: value_plus_def maybe_arith_int_never_string)
lemma value_plus_symmetry: "value_plus x y = value_plus y x"
apply (induct x y rule: maybe_arith_int.induct)
by (simp_all add: value_plus_def)
definition "value_minus = maybe_arith_int (-)"
lemma value_minus_never_string: "value_minus a b \<noteq> Some (Str x)"
by (simp add: maybe_arith_int_never_string value_minus_def)
definition "value_times = maybe_arith_int (*)"
lemma value_times_never_string: "value_times a b \<noteq> Some (Str x)"
by (simp add: maybe_arith_int_never_string value_times_def)
fun MaybeBoolInt :: "(int \<Rightarrow> int \<Rightarrow> bool) \<Rightarrow> value option \<Rightarrow> value option \<Rightarrow> trilean" where
"MaybeBoolInt f (Some (Num a)) (Some (Num b)) = (if f a b then true else false)" |
"MaybeBoolInt _ _ _ = invalid"
lemma MaybeBoolInt_not_num_1:
"\<forall>n. r \<noteq> Some (Num n) \<Longrightarrow> MaybeBoolInt f n r = invalid"
using MaybeBoolInt.elims by blast
definition value_gt :: "value option \<Rightarrow> value option \<Rightarrow> trilean" where
"value_gt a b \<equiv> MaybeBoolInt (>) a b"
fun value_eq :: "value option \<Rightarrow> value option \<Rightarrow> trilean" where
"value_eq None _ = invalid" |
"value_eq _ None = invalid" |
"value_eq (Some a) (Some b) = (if a = b then true else false)"
lemma value_eq_true: "(value_eq a b = true) = (\<exists>x y. a = Some x \<and> b = Some y \<and> x = y)"
apply (cases a, simp)
by (cases b, auto)
lemma value_eq_false: "(value_eq a b = false) = (\<exists>x y. a = Some x \<and> b = Some y \<and> x \<noteq> y)"
apply (cases a, simp)
by (cases b, auto)
lemma value_gt_true_Some: "value_gt a b = true \<Longrightarrow> (\<exists>x. a = Some x) \<and> (\<exists>y. b = Some y)"
apply (simp add: value_gt_def)
apply (cases a)
apply simp
apply (cases b)
by auto
lemma value_gt_true: "(value_gt a b = true) = (\<exists>x y. a = Some (Num x) \<and> b = Some (Num y) \<and> x > y)"
apply (cases a)
using value_gt_true_Some apply blast
apply (cases b)
using value_gt_true_Some apply blast
apply simp
apply (case_tac aa)
apply simp
apply (case_tac aaa)
by (simp add: value_gt_def)+
lemma value_gt_false_Some: "value_gt a b = false \<Longrightarrow> (\<exists>x. a = Some x) \<and> (\<exists>y. b = Some y)"
apply (simp add: value_gt_def)
apply (cases a)
apply simp
apply (cases b)
by auto
end