author | smolkas |
Wed, 28 Nov 2012 12:25:43 +0100 | |
changeset 50272 | 316d94b4ffe2 |
parent 49497 | 860b7c6bd913 |
child 50896 | fb0fcd278ac5 |
permissions | -rw-r--r-- |
47613 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
theory Abs_Int0 |
|
4 |
imports Abs_Int_init |
|
5 |
begin |
|
6 |
||
7 |
subsection "Orderings" |
|
8 |
||
9 |
class preord = |
|
10 |
fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50) |
|
11 |
assumes le_refl[simp]: "x \<sqsubseteq> x" |
|
12 |
and le_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z" |
|
13 |
begin |
|
14 |
||
15 |
definition mono where "mono f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)" |
|
16 |
||
17 |
declare le_trans[trans] |
|
18 |
||
19 |
end |
|
20 |
||
21 |
text{* Note: no antisymmetry. Allows implementations where some abstract |
|
22 |
element is implemented by two different values @{prop "x \<noteq> y"} |
|
23 |
such that @{prop"x \<sqsubseteq> y"} and @{prop"y \<sqsubseteq> x"}. Antisymmetry is not |
|
24 |
needed because we never compare elements for equality but only for @{text"\<sqsubseteq>"}. |
|
25 |
*} |
|
26 |
||
27 |
class join = preord + |
|
28 |
fixes join :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65) |
|
29 |
||
49396 | 30 |
class semilattice = join + |
47613 | 31 |
fixes Top :: "'a" ("\<top>") |
32 |
assumes join_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y" |
|
33 |
and join_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y" |
|
34 |
and join_least: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z" |
|
35 |
and top[simp]: "x \<sqsubseteq> \<top>" |
|
36 |
begin |
|
37 |
||
38 |
lemma join_le_iff[simp]: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z" |
|
39 |
by (metis join_ge1 join_ge2 join_least le_trans) |
|
40 |
||
41 |
lemma le_join_disj: "x \<sqsubseteq> y \<or> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<squnion> z" |
|
42 |
by (metis join_ge1 join_ge2 le_trans) |
|
43 |
||
44 |
end |
|
45 |
||
46 |
instantiation "fun" :: (type, preord) preord |
|
47 |
begin |
|
48 |
||
49 |
definition "f \<sqsubseteq> g = (\<forall>x. f x \<sqsubseteq> g x)" |
|
50 |
||
51 |
instance |
|
52 |
proof |
|
53 |
case goal2 thus ?case by (metis le_fun_def preord_class.le_trans) |
|
54 |
qed (simp_all add: le_fun_def) |
|
55 |
||
56 |
end |
|
57 |
||
58 |
||
49396 | 59 |
instantiation "fun" :: (type, semilattice) semilattice |
47613 | 60 |
begin |
61 |
||
62 |
definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)" |
|
63 |
definition "\<top> = (\<lambda>x. \<top>)" |
|
64 |
||
65 |
lemma join_apply[simp]: "(f \<squnion> g) x = f x \<squnion> g x" |
|
66 |
by (simp add: join_fun_def) |
|
67 |
||
68 |
instance |
|
69 |
proof |
|
70 |
qed (simp_all add: le_fun_def Top_fun_def) |
|
71 |
||
72 |
end |
|
73 |
||
74 |
||
75 |
instantiation acom :: (preord) preord |
|
76 |
begin |
|
77 |
||
78 |
fun le_acom :: "('a::preord)acom \<Rightarrow> 'a acom \<Rightarrow> bool" where |
|
79 |
"le_acom (SKIP {S}) (SKIP {S'}) = (S \<sqsubseteq> S')" | |
|
80 |
"le_acom (x ::= e {S}) (x' ::= e' {S'}) = (x=x' \<and> e=e' \<and> S \<sqsubseteq> S')" | |
|
81 |
"le_acom (C1;C2) (D1;D2) = (C1 \<sqsubseteq> D1 \<and> C2 \<sqsubseteq> D2)" | |
|
49095 | 82 |
"le_acom (IF b THEN {p1} C1 ELSE {p2} C2 {S}) (IF b' THEN {q1} D1 ELSE {q2} D2 {S'}) = |
83 |
(b=b' \<and> p1 \<sqsubseteq> q1 \<and> C1 \<sqsubseteq> D1 \<and> p2 \<sqsubseteq> q2 \<and> C2 \<sqsubseteq> D2 \<and> S \<sqsubseteq> S')" | |
|
84 |
"le_acom ({I} WHILE b DO {p} C {P}) ({I'} WHILE b' DO {p'} C' {P'}) = |
|
85 |
(b=b' \<and> p \<sqsubseteq> p' \<and> C \<sqsubseteq> C' \<and> I \<sqsubseteq> I' \<and> P \<sqsubseteq> P')" | |
|
47613 | 86 |
"le_acom _ _ = False" |
87 |
||
88 |
lemma [simp]: "SKIP {S} \<sqsubseteq> C \<longleftrightarrow> (\<exists>S'. C = SKIP {S'} \<and> S \<sqsubseteq> S')" |
|
89 |
by (cases C) auto |
|
90 |
||
91 |
lemma [simp]: "x ::= e {S} \<sqsubseteq> C \<longleftrightarrow> (\<exists>S'. C = x ::= e {S'} \<and> S \<sqsubseteq> S')" |
|
92 |
by (cases C) auto |
|
93 |
||
94 |
lemma [simp]: "C1;C2 \<sqsubseteq> C \<longleftrightarrow> (\<exists>D1 D2. C = D1;D2 \<and> C1 \<sqsubseteq> D1 \<and> C2 \<sqsubseteq> D2)" |
|
95 |
by (cases C) auto |
|
96 |
||
49095 | 97 |
lemma [simp]: "IF b THEN {p1} C1 ELSE {p2} C2 {S} \<sqsubseteq> C \<longleftrightarrow> |
98 |
(\<exists>q1 q2 D1 D2 S'. C = IF b THEN {q1} D1 ELSE {q2} D2 {S'} \<and> |
|
99 |
p1 \<sqsubseteq> q1 \<and> C1 \<sqsubseteq> D1 \<and> p2 \<sqsubseteq> q2 \<and> C2 \<sqsubseteq> D2 \<and> S \<sqsubseteq> S')" |
|
47613 | 100 |
by (cases C) auto |
101 |
||
49095 | 102 |
lemma [simp]: "{I} WHILE b DO {p} C {P} \<sqsubseteq> W \<longleftrightarrow> |
103 |
(\<exists>I' p' C' P'. W = {I'} WHILE b DO {p'} C' {P'} \<and> p \<sqsubseteq> p' \<and> C \<sqsubseteq> C' \<and> I \<sqsubseteq> I' \<and> P \<sqsubseteq> P')" |
|
47613 | 104 |
by (cases W) auto |
105 |
||
106 |
instance |
|
107 |
proof |
|
108 |
case goal1 thus ?case by (induct x) auto |
|
109 |
next |
|
110 |
case goal2 thus ?case |
|
111 |
apply(induct x y arbitrary: z rule: le_acom.induct) |
|
112 |
apply (auto intro: le_trans) |
|
113 |
done |
|
114 |
qed |
|
115 |
||
116 |
end |
|
117 |
||
118 |
||
119 |
instantiation option :: (preord)preord |
|
120 |
begin |
|
121 |
||
122 |
fun le_option where |
|
123 |
"Some x \<sqsubseteq> Some y = (x \<sqsubseteq> y)" | |
|
124 |
"None \<sqsubseteq> y = True" | |
|
125 |
"Some _ \<sqsubseteq> None = False" |
|
126 |
||
127 |
lemma [simp]: "(x \<sqsubseteq> None) = (x = None)" |
|
128 |
by (cases x) simp_all |
|
129 |
||
130 |
lemma [simp]: "(Some x \<sqsubseteq> u) = (\<exists>y. u = Some y \<and> x \<sqsubseteq> y)" |
|
131 |
by (cases u) auto |
|
132 |
||
133 |
instance proof |
|
134 |
case goal1 show ?case by(cases x, simp_all) |
|
135 |
next |
|
136 |
case goal2 thus ?case |
|
137 |
by(cases z, simp, cases y, simp, cases x, auto intro: le_trans) |
|
138 |
qed |
|
139 |
||
140 |
end |
|
141 |
||
142 |
instantiation option :: (join)join |
|
143 |
begin |
|
144 |
||
145 |
fun join_option where |
|
146 |
"Some x \<squnion> Some y = Some(x \<squnion> y)" | |
|
147 |
"None \<squnion> y = y" | |
|
148 |
"x \<squnion> None = x" |
|
149 |
||
150 |
lemma join_None2[simp]: "x \<squnion> None = x" |
|
151 |
by (cases x) simp_all |
|
152 |
||
153 |
instance .. |
|
154 |
||
155 |
end |
|
156 |
||
49396 | 157 |
instantiation option :: (semilattice)semilattice |
47613 | 158 |
begin |
159 |
||
160 |
definition "\<top> = Some \<top>" |
|
161 |
||
162 |
instance proof |
|
163 |
case goal1 thus ?case by(cases x, simp, cases y, simp_all) |
|
164 |
next |
|
165 |
case goal2 thus ?case by(cases y, simp, cases x, simp_all) |
|
166 |
next |
|
167 |
case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all) |
|
168 |
next |
|
169 |
case goal4 thus ?case by(cases x, simp_all add: Top_option_def) |
|
170 |
qed |
|
171 |
||
172 |
end |
|
173 |
||
49396 | 174 |
class bot = preord + |
175 |
fixes bot :: "'a" ("\<bottom>") |
|
176 |
assumes bot[simp]: "\<bottom> \<sqsubseteq> x" |
|
47613 | 177 |
|
49396 | 178 |
instantiation option :: (preord)bot |
47613 | 179 |
begin |
180 |
||
49396 | 181 |
definition bot_option :: "'a option" where |
47613 | 182 |
"\<bottom> = None" |
183 |
||
184 |
instance |
|
185 |
proof |
|
49396 | 186 |
case goal1 thus ?case by(auto simp: bot_option_def) |
47613 | 187 |
qed |
188 |
||
189 |
end |
|
190 |
||
191 |
||
192 |
definition bot :: "com \<Rightarrow> 'a option acom" where |
|
193 |
"bot c = anno None c" |
|
194 |
||
195 |
lemma bot_least: "strip C = c \<Longrightarrow> bot c \<sqsubseteq> C" |
|
196 |
by(induct C arbitrary: c)(auto simp: bot_def) |
|
197 |
||
198 |
lemma strip_bot[simp]: "strip(bot c) = c" |
|
199 |
by(simp add: bot_def) |
|
200 |
||
201 |
||
202 |
subsubsection "Post-fixed point iteration" |
|
203 |
||
49464 | 204 |
definition pfp :: "(('a::preord) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where |
47613 | 205 |
"pfp f = while_option (\<lambda>x. \<not> f x \<sqsubseteq> x) f" |
206 |
||
207 |
lemma pfp_pfp: assumes "pfp f x0 = Some x" shows "f x \<sqsubseteq> x" |
|
208 |
using while_option_stop[OF assms[simplified pfp_def]] by simp |
|
209 |
||
49464 | 210 |
lemma while_least: |
211 |
assumes "\<forall>x\<in>L.\<forall>y\<in>L. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y" and "\<forall>x. x \<in> L \<longrightarrow> f x \<in> L" |
|
212 |
and "\<forall>x \<in> L. b \<sqsubseteq> x" and "b \<in> L" and "f q \<sqsubseteq> q" and "q \<in> L" |
|
213 |
and "while_option P f b = Some p" |
|
214 |
shows "p \<sqsubseteq> q" |
|
215 |
using while_option_rule[OF _ assms(7)[unfolded pfp_def], |
|
216 |
where P = "%x. x \<in> L \<and> x \<sqsubseteq> q"] |
|
217 |
by (metis assms(1-6) le_trans) |
|
47613 | 218 |
|
49464 | 219 |
lemma pfp_inv: |
220 |
"pfp f x = Some y \<Longrightarrow> (\<And>x. P x \<Longrightarrow> P(f x)) \<Longrightarrow> P x \<Longrightarrow> P y" |
|
221 |
unfolding pfp_def by (metis (lifting) while_option_rule) |
|
47613 | 222 |
|
223 |
lemma strip_pfp: |
|
224 |
assumes "\<And>x. g(f x) = g x" and "pfp f x0 = Some x" shows "g x = g x0" |
|
49464 | 225 |
using pfp_inv[OF assms(2), where P = "%x. g x = g x0"] assms(1) by simp |
47613 | 226 |
|
227 |
||
228 |
subsection "Abstract Interpretation" |
|
229 |
||
230 |
definition \<gamma>_fun :: "('a \<Rightarrow> 'b set) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b)set" where |
|
231 |
"\<gamma>_fun \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(F x)}" |
|
232 |
||
233 |
fun \<gamma>_option :: "('a \<Rightarrow> 'b set) \<Rightarrow> 'a option \<Rightarrow> 'b set" where |
|
234 |
"\<gamma>_option \<gamma> None = {}" | |
|
235 |
"\<gamma>_option \<gamma> (Some a) = \<gamma> a" |
|
236 |
||
237 |
text{* The interface for abstract values: *} |
|
238 |
||
239 |
locale Val_abs = |
|
49396 | 240 |
fixes \<gamma> :: "'av::semilattice \<Rightarrow> val set" |
47613 | 241 |
assumes mono_gamma: "a \<sqsubseteq> b \<Longrightarrow> \<gamma> a \<subseteq> \<gamma> b" |
242 |
and gamma_Top[simp]: "\<gamma> \<top> = UNIV" |
|
243 |
fixes num' :: "val \<Rightarrow> 'av" |
|
244 |
and plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av" |
|
245 |
assumes gamma_num': "n : \<gamma>(num' n)" |
|
246 |
and gamma_plus': |
|
247 |
"n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1+n2 : \<gamma>(plus' a1 a2)" |
|
248 |
||
249 |
type_synonym 'av st = "(vname \<Rightarrow> 'av)" |
|
250 |
||
49396 | 251 |
locale Abs_Int_Fun = Val_abs \<gamma> for \<gamma> :: "'av::semilattice \<Rightarrow> val set" |
47613 | 252 |
begin |
253 |
||
254 |
fun aval' :: "aexp \<Rightarrow> 'av st \<Rightarrow> 'av" where |
|
255 |
"aval' (N n) S = num' n" | |
|
256 |
"aval' (V x) S = S x" | |
|
257 |
"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)" |
|
258 |
||
259 |
fun step' :: "'av st option \<Rightarrow> 'av st option acom \<Rightarrow> 'av st option acom" |
|
260 |
where |
|
261 |
"step' S (SKIP {P}) = (SKIP {S})" | |
|
262 |
"step' S (x ::= e {P}) = |
|
263 |
x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(S(x := aval' e S))}" | |
|
264 |
"step' S (C1; C2) = step' S C1; step' (post C1) C2" | |
|
49344 | 265 |
"step' S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) = |
266 |
IF b THEN {S} step' P1 C1 ELSE {S} step' P2 C2 {post C1 \<squnion> post C2}" | |
|
267 |
"step' S ({I} WHILE b DO {P} C {Q}) = |
|
268 |
{S \<squnion> post C} WHILE b DO {I} step' P C {I}" |
|
47613 | 269 |
|
270 |
definition AI :: "com \<Rightarrow> 'av st option acom option" where |
|
49464 | 271 |
"AI c = pfp (step' \<top>) (bot c)" |
47613 | 272 |
|
273 |
||
274 |
lemma strip_step'[simp]: "strip(step' S C) = strip C" |
|
275 |
by(induct C arbitrary: S) (simp_all add: Let_def) |
|
276 |
||
277 |
||
49497 | 278 |
abbreviation \<gamma>\<^isub>s :: "'av st \<Rightarrow> state set" |
279 |
where "\<gamma>\<^isub>s == \<gamma>_fun \<gamma>" |
|
47613 | 280 |
|
281 |
abbreviation \<gamma>\<^isub>o :: "'av st option \<Rightarrow> state set" |
|
49497 | 282 |
where "\<gamma>\<^isub>o == \<gamma>_option \<gamma>\<^isub>s" |
47613 | 283 |
|
284 |
abbreviation \<gamma>\<^isub>c :: "'av st option acom \<Rightarrow> state set acom" |
|
285 |
where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o" |
|
286 |
||
49497 | 287 |
lemma gamma_s_Top[simp]: "\<gamma>\<^isub>s Top = UNIV" |
47613 | 288 |
by(simp add: Top_fun_def \<gamma>_fun_def) |
289 |
||
290 |
lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o Top = UNIV" |
|
291 |
by (simp add: Top_option_def) |
|
292 |
||
293 |
(* FIXME (maybe also le \<rightarrow> sqle?) *) |
|
294 |
||
49497 | 295 |
lemma mono_gamma_s: "f1 \<sqsubseteq> f2 \<Longrightarrow> \<gamma>\<^isub>s f1 \<subseteq> \<gamma>\<^isub>s f2" |
47613 | 296 |
by(auto simp: le_fun_def \<gamma>_fun_def dest: mono_gamma) |
297 |
||
298 |
lemma mono_gamma_o: |
|
299 |
"S1 \<sqsubseteq> S2 \<Longrightarrow> \<gamma>\<^isub>o S1 \<subseteq> \<gamma>\<^isub>o S2" |
|
49497 | 300 |
by(induction S1 S2 rule: le_option.induct)(simp_all add: mono_gamma_s) |
47613 | 301 |
|
302 |
lemma mono_gamma_c: "C1 \<sqsubseteq> C2 \<Longrightarrow> \<gamma>\<^isub>c C1 \<le> \<gamma>\<^isub>c C2" |
|
303 |
by (induction C1 C2 rule: le_acom.induct) (simp_all add:mono_gamma_o) |
|
304 |
||
305 |
text{* Soundness: *} |
|
306 |
||
49497 | 307 |
lemma aval'_sound: "s : \<gamma>\<^isub>s S \<Longrightarrow> aval a s : \<gamma>(aval' a S)" |
47613 | 308 |
by (induct a) (auto simp: gamma_num' gamma_plus' \<gamma>_fun_def) |
309 |
||
310 |
lemma in_gamma_update: |
|
49497 | 311 |
"\<lbrakk> s : \<gamma>\<^isub>s S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>s(S(x := a))" |
47613 | 312 |
by(simp add: \<gamma>_fun_def) |
313 |
||
314 |
lemma step_preserves_le: |
|
315 |
"\<lbrakk> S \<subseteq> \<gamma>\<^isub>o S'; C \<le> \<gamma>\<^isub>c C' \<rbrakk> \<Longrightarrow> step S C \<le> \<gamma>\<^isub>c (step' S' C')" |
|
316 |
proof(induction C arbitrary: C' S S') |
|
317 |
case SKIP thus ?case by(auto simp:SKIP_le map_acom_SKIP) |
|
318 |
next |
|
319 |
case Assign thus ?case |
|
320 |
by (fastforce simp: Assign_le map_acom_Assign intro: aval'_sound in_gamma_update |
|
321 |
split: option.splits del:subsetD) |
|
322 |
next |
|
47818 | 323 |
case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq) |
47613 | 324 |
by (metis le_post post_map_acom) |
325 |
next |
|
49095 | 326 |
case (If b p1 C1 p2 C2 P) |
327 |
then obtain q1 q2 D1 D2 P' where |
|
328 |
"C' = IF b THEN {q1} D1 ELSE {q2} D2 {P'}" |
|
329 |
"p1 \<subseteq> \<gamma>\<^isub>o q1" "p2 \<subseteq> \<gamma>\<^isub>o q2" "P \<subseteq> \<gamma>\<^isub>o P'" "C1 \<le> \<gamma>\<^isub>c D1" "C2 \<le> \<gamma>\<^isub>c D2" |
|
47613 | 330 |
by (fastforce simp: If_le map_acom_If) |
331 |
moreover have "post C1 \<subseteq> \<gamma>\<^isub>o(post D1 \<squnion> post D2)" |
|
332 |
by (metis (no_types) `C1 \<le> \<gamma>\<^isub>c D1` join_ge1 le_post mono_gamma_o order_trans post_map_acom) |
|
333 |
moreover have "post C2 \<subseteq> \<gamma>\<^isub>o(post D1 \<squnion> post D2)" |
|
334 |
by (metis (no_types) `C2 \<le> \<gamma>\<^isub>c D2` join_ge2 le_post mono_gamma_o order_trans post_map_acom) |
|
335 |
ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>o S'` by (simp add: If.IH subset_iff) |
|
336 |
next |
|
49095 | 337 |
case (While I b p1 C1 P) |
338 |
then obtain D1 I' p1' P' where |
|
339 |
"C' = {I'} WHILE b DO {p1'} D1 {P'}" |
|
340 |
"I \<subseteq> \<gamma>\<^isub>o I'" "p1 \<subseteq> \<gamma>\<^isub>o p1'" "P \<subseteq> \<gamma>\<^isub>o P'" "C1 \<le> \<gamma>\<^isub>c D1" |
|
47613 | 341 |
by (fastforce simp: map_acom_While While_le) |
342 |
moreover have "S \<union> post C1 \<subseteq> \<gamma>\<^isub>o (S' \<squnion> post D1)" |
|
343 |
using `S \<subseteq> \<gamma>\<^isub>o S'` le_post[OF `C1 \<le> \<gamma>\<^isub>c D1`, simplified] |
|
344 |
by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_gamma_o order_trans) |
|
345 |
ultimately show ?case by (simp add: While.IH subset_iff) |
|
49095 | 346 |
|
47613 | 347 |
qed |
348 |
||
349 |
lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C" |
|
350 |
proof(simp add: CS_def AI_def) |
|
49464 | 351 |
assume 1: "pfp (step' \<top>) (bot c) = Some C" |
352 |
have 2: "step' \<top> C \<sqsubseteq> C" by(rule pfp_pfp[OF 1]) |
|
47613 | 353 |
have 3: "strip (\<gamma>\<^isub>c (step' \<top> C)) = c" |
49464 | 354 |
by(simp add: strip_pfp[OF _ 1]) |
48759
ff570720ba1c
Improved complete lattice formalisation - no more index set.
nipkow
parents:
47818
diff
changeset
|
355 |
have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> C)" |
47613 | 356 |
proof(rule lfp_lowerbound[simplified,OF 3]) |
357 |
show "step UNIV (\<gamma>\<^isub>c (step' \<top> C)) \<le> \<gamma>\<^isub>c (step' \<top> C)" |
|
358 |
proof(rule step_preserves_le[OF _ _]) |
|
359 |
show "UNIV \<subseteq> \<gamma>\<^isub>o \<top>" by simp |
|
360 |
show "\<gamma>\<^isub>c (step' \<top> C) \<le> \<gamma>\<^isub>c C" by(rule mono_gamma_c[OF 2]) |
|
361 |
qed |
|
362 |
qed |
|
48759
ff570720ba1c
Improved complete lattice formalisation - no more index set.
nipkow
parents:
47818
diff
changeset
|
363 |
with 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" |
47613 | 364 |
by (blast intro: mono_gamma_c order_trans) |
365 |
qed |
|
366 |
||
367 |
end |
|
368 |
||
369 |
||
370 |
subsubsection "Monotonicity" |
|
371 |
||
372 |
lemma mono_post: "C1 \<sqsubseteq> C2 \<Longrightarrow> post C1 \<sqsubseteq> post C2" |
|
373 |
by(induction C1 C2 rule: le_acom.induct) (auto) |
|
374 |
||
375 |
locale Abs_Int_Fun_mono = Abs_Int_Fun + |
|
376 |
assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2" |
|
377 |
begin |
|
378 |
||
379 |
lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'" |
|
380 |
by(induction e)(auto simp: le_fun_def mono_plus') |
|
381 |
||
382 |
lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> S(x := a) \<sqsubseteq> S'(x := a')" |
|
383 |
by(simp add: le_fun_def) |
|
384 |
||
385 |
lemma mono_step': "S1 \<sqsubseteq> S2 \<Longrightarrow> C1 \<sqsubseteq> C2 \<Longrightarrow> step' S1 C1 \<sqsubseteq> step' S2 C2" |
|
386 |
apply(induction C1 C2 arbitrary: S1 S2 rule: le_acom.induct) |
|
387 |
apply (auto simp: Let_def mono_update mono_aval' mono_post le_join_disj |
|
388 |
split: option.split) |
|
389 |
done |
|
390 |
||
391 |
end |
|
392 |
||
393 |
text{* Problem: not executable because of the comparison of abstract states, |
|
394 |
i.e. functions, in the post-fixedpoint computation. *} |
|
395 |
||
396 |
end |