47619
|
1 |
(* Author: Tobias Nipkow *)
|
|
2 |
|
|
3 |
theory Abs_State
|
|
4 |
imports Abs_Int0
|
|
5 |
begin
|
|
6 |
|
49396
|
7 |
subsubsection "Set-based lattices"
|
47619
|
8 |
|
|
9 |
instantiation com :: vars
|
|
10 |
begin
|
|
11 |
|
|
12 |
fun vars_com :: "com \<Rightarrow> vname set" where
|
|
13 |
"vars com.SKIP = {}" |
|
|
14 |
"vars (x::=e) = {x} \<union> vars e" |
|
|
15 |
"vars (c1;c2) = vars c1 \<union> vars c2" |
|
|
16 |
"vars (IF b THEN c1 ELSE c2) = vars b \<union> vars c1 \<union> vars c2" |
|
|
17 |
"vars (WHILE b DO c) = vars b \<union> vars c"
|
|
18 |
|
|
19 |
instance ..
|
|
20 |
|
|
21 |
end
|
|
22 |
|
|
23 |
|
|
24 |
lemma finite_avars: "finite(vars(a::aexp))"
|
|
25 |
by(induction a) simp_all
|
|
26 |
|
|
27 |
lemma finite_bvars: "finite(vars(b::bexp))"
|
|
28 |
by(induction b) (simp_all add: finite_avars)
|
|
29 |
|
|
30 |
lemma finite_cvars: "finite(vars(c::com))"
|
|
31 |
by(induction c) (simp_all add: finite_avars finite_bvars)
|
|
32 |
|
|
33 |
|
49396
|
34 |
class L =
|
|
35 |
fixes L :: "vname set \<Rightarrow> 'a set"
|
47619
|
36 |
|
|
37 |
|
49396
|
38 |
instantiation acom :: (L)L
|
47619
|
39 |
begin
|
|
40 |
|
49396
|
41 |
definition L_acom where
|
|
42 |
"L X = {C. vars(strip C) \<subseteq> X \<and> (\<forall>a \<in> set(annos C). a \<in> L X)}"
|
47619
|
43 |
|
|
44 |
instance ..
|
|
45 |
|
|
46 |
end
|
|
47 |
|
|
48 |
|
49396
|
49 |
instantiation option :: (L)L
|
47619
|
50 |
begin
|
|
51 |
|
49396
|
52 |
definition L_option where
|
|
53 |
"L X = {opt. case opt of None \<Rightarrow> True | Some x \<Rightarrow> x \<in> L X}"
|
47619
|
54 |
|
49396
|
55 |
lemma L_option_simps[simp]: "None \<in> L X" "(Some x \<in> L X) = (x \<in> L X)"
|
|
56 |
by(simp_all add: L_option_def)
|
47619
|
57 |
|
|
58 |
instance ..
|
|
59 |
|
|
60 |
end
|
|
61 |
|
49396
|
62 |
class semilatticeL = join + L +
|
49577
|
63 |
fixes top :: "com \<Rightarrow> 'a"
|
49396
|
64 |
assumes join_ge1 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<sqsubseteq> x \<squnion> y"
|
|
65 |
and join_ge2 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> y \<sqsubseteq> x \<squnion> y"
|
47619
|
66 |
and join_least[simp]: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
|
49396
|
67 |
and top[simp]: "x \<in> L(vars c) \<Longrightarrow> x \<sqsubseteq> top c"
|
|
68 |
and top_in_L[simp]: "top c \<in> L(vars c)"
|
|
69 |
and join_in_L[simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<squnion> y \<in> L X"
|
47619
|
70 |
|
49577
|
71 |
notation (input) top ("\<top>\<^bsub>_\<^esub>")
|
|
72 |
notation (latex output) top ("\<top>\<^bsub>\<^raw:\isa{>_\<^raw:}>\<^esub>")
|
47619
|
73 |
|
49396
|
74 |
instantiation option :: (semilatticeL)semilatticeL
|
47619
|
75 |
begin
|
|
76 |
|
|
77 |
definition top_option where "top c = Some(top c)"
|
|
78 |
|
|
79 |
instance proof
|
|
80 |
case goal1 thus ?case by(cases x, simp, cases y, simp_all)
|
|
81 |
next
|
|
82 |
case goal2 thus ?case by(cases y, simp, cases x, simp_all)
|
|
83 |
next
|
|
84 |
case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
|
|
85 |
next
|
|
86 |
case goal4 thus ?case by(cases x, simp_all add: top_option_def)
|
|
87 |
next
|
|
88 |
case goal5 thus ?case by(simp add: top_option_def)
|
|
89 |
next
|
49396
|
90 |
case goal6 thus ?case by(simp add: L_option_def split: option.splits)
|
47619
|
91 |
qed
|
|
92 |
|
|
93 |
end
|
|
94 |
|
|
95 |
|
|
96 |
subsection "Abstract State with Computable Ordering"
|
|
97 |
|
|
98 |
hide_type st --"to avoid long names"
|
|
99 |
|
|
100 |
text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
|
|
101 |
|
|
102 |
datatype 'a st = FunDom "vname \<Rightarrow> 'a" "vname set"
|
|
103 |
|
49344
|
104 |
fun "fun" where "fun (FunDom f X) = f"
|
|
105 |
fun dom where "dom (FunDom f X) = X"
|
47619
|
106 |
|
|
107 |
definition "show_st S = (\<lambda>x. (x, fun S x)) ` dom S"
|
|
108 |
|
|
109 |
value [code] "show_st (FunDom (\<lambda>x. 1::int) {''a'',''b''})"
|
|
110 |
|
|
111 |
definition "show_acom = map_acom (Option.map show_st)"
|
|
112 |
definition "show_acom_opt = Option.map show_acom"
|
|
113 |
|
|
114 |
definition "update F x y = FunDom ((fun F)(x:=y)) (dom F)"
|
|
115 |
|
|
116 |
lemma fun_update[simp]: "fun (update S x y) = (fun S)(x:=y)"
|
|
117 |
by(rule ext)(auto simp: update_def)
|
|
118 |
|
|
119 |
lemma dom_update[simp]: "dom (update S x y) = dom S"
|
|
120 |
by(simp add: update_def)
|
|
121 |
|
|
122 |
definition "\<gamma>_st \<gamma> F = {f. \<forall>x\<in>dom F. f x \<in> \<gamma>(fun F x)}"
|
|
123 |
|
|
124 |
|
|
125 |
instantiation st :: (preord) preord
|
|
126 |
begin
|
|
127 |
|
|
128 |
definition le_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> bool" where
|
|
129 |
"F \<sqsubseteq> G = (dom F = dom G \<and> (\<forall>x \<in> dom F. fun F x \<sqsubseteq> fun G x))"
|
|
130 |
|
|
131 |
instance
|
|
132 |
proof
|
|
133 |
case goal2 thus ?case by(auto simp: le_st_def)(metis preord_class.le_trans)
|
|
134 |
qed (auto simp: le_st_def)
|
|
135 |
|
|
136 |
end
|
|
137 |
|
|
138 |
instantiation st :: (join) join
|
|
139 |
begin
|
|
140 |
|
|
141 |
definition join_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" where
|
|
142 |
"F \<squnion> G = FunDom (\<lambda>x. fun F x \<squnion> fun G x) (dom F)"
|
|
143 |
|
|
144 |
instance ..
|
|
145 |
|
|
146 |
end
|
|
147 |
|
49396
|
148 |
instantiation st :: (type) L
|
47619
|
149 |
begin
|
|
150 |
|
49396
|
151 |
definition L_st :: "vname set \<Rightarrow> 'a st set" where
|
|
152 |
"L X = {F. dom F = X}"
|
47619
|
153 |
|
|
154 |
instance ..
|
|
155 |
|
|
156 |
end
|
|
157 |
|
49396
|
158 |
instantiation st :: (semilattice) semilatticeL
|
47619
|
159 |
begin
|
|
160 |
|
|
161 |
definition top_st where "top c = FunDom (\<lambda>x. \<top>) (vars c)"
|
|
162 |
|
|
163 |
instance
|
|
164 |
proof
|
49396
|
165 |
qed (auto simp: le_st_def join_st_def top_st_def L_st_def)
|
47619
|
166 |
|
|
167 |
end
|
|
168 |
|
|
169 |
|
49399
|
170 |
text{* Trick to make code generator happy. *}
|
|
171 |
lemma [code]: "L = (L :: _ \<Rightarrow> _ st set)"
|
|
172 |
by(rule refl)
|
|
173 |
(* L is not used in the code but is part of a type class that is used.
|
|
174 |
Hence the code generator wants to build a dictionary with L in it.
|
|
175 |
But L is not executable. This looping defn makes it look as if it were. *)
|
|
176 |
|
|
177 |
|
47619
|
178 |
lemma mono_fun: "F \<sqsubseteq> G \<Longrightarrow> x : dom F \<Longrightarrow> fun F x \<sqsubseteq> fun G x"
|
|
179 |
by(auto simp: le_st_def)
|
|
180 |
|
|
181 |
lemma mono_update[simp]:
|
|
182 |
"a1 \<sqsubseteq> a2 \<Longrightarrow> S1 \<sqsubseteq> S2 \<Longrightarrow> update S1 x a1 \<sqsubseteq> update S2 x a2"
|
|
183 |
by(auto simp add: le_st_def update_def)
|
|
184 |
|
|
185 |
|
49396
|
186 |
locale Gamma = Val_abs where \<gamma>=\<gamma> for \<gamma> :: "'av::semilattice \<Rightarrow> val set"
|
47619
|
187 |
begin
|
|
188 |
|
49497
|
189 |
abbreviation \<gamma>\<^isub>s :: "'av st \<Rightarrow> state set"
|
|
190 |
where "\<gamma>\<^isub>s == \<gamma>_st \<gamma>"
|
47619
|
191 |
|
|
192 |
abbreviation \<gamma>\<^isub>o :: "'av st option \<Rightarrow> state set"
|
49497
|
193 |
where "\<gamma>\<^isub>o == \<gamma>_option \<gamma>\<^isub>s"
|
47619
|
194 |
|
|
195 |
abbreviation \<gamma>\<^isub>c :: "'av st option acom \<Rightarrow> state set acom"
|
|
196 |
where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o"
|
|
197 |
|
49497
|
198 |
lemma gamma_s_Top[simp]: "\<gamma>\<^isub>s (top c) = UNIV"
|
47619
|
199 |
by(auto simp: top_st_def \<gamma>_st_def)
|
|
200 |
|
|
201 |
lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o (top c) = UNIV"
|
|
202 |
by (simp add: top_option_def)
|
|
203 |
|
|
204 |
(* FIXME (maybe also le \<rightarrow> sqle?) *)
|
|
205 |
|
49497
|
206 |
lemma mono_gamma_s: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>s f \<subseteq> \<gamma>\<^isub>s g"
|
47619
|
207 |
apply(simp add:\<gamma>_st_def subset_iff le_st_def split: if_splits)
|
|
208 |
by (metis mono_gamma subsetD)
|
|
209 |
|
|
210 |
lemma mono_gamma_o:
|
|
211 |
"S1 \<sqsubseteq> S2 \<Longrightarrow> \<gamma>\<^isub>o S1 \<subseteq> \<gamma>\<^isub>o S2"
|
49497
|
212 |
by(induction S1 S2 rule: le_option.induct)(simp_all add: mono_gamma_s)
|
47619
|
213 |
|
|
214 |
lemma mono_gamma_c: "C1 \<sqsubseteq> C2 \<Longrightarrow> \<gamma>\<^isub>c C1 \<le> \<gamma>\<^isub>c C2"
|
|
215 |
by (induction C1 C2 rule: le_acom.induct) (simp_all add:mono_gamma_o)
|
|
216 |
|
|
217 |
lemma in_gamma_option_iff:
|
|
218 |
"x : \<gamma>_option r u \<longleftrightarrow> (\<exists>u'. u = Some u' \<and> x : r u')"
|
|
219 |
by (cases u) auto
|
|
220 |
|
|
221 |
end
|
|
222 |
|
|
223 |
end
|