1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 theory Abs_Int1_ITP |
|
4 imports Abs_State_ITP |
|
5 begin |
|
6 |
|
7 subsection "Computable Abstract Interpretation" |
|
8 |
|
9 text{* Abstract interpretation over type @{text st} instead of |
|
10 functions. *} |
|
11 |
|
12 context Gamma |
|
13 begin |
|
14 |
|
15 fun aval' :: "aexp \<Rightarrow> 'av st \<Rightarrow> 'av" where |
|
16 "aval' (N n) S = num' n" | |
|
17 "aval' (V x) S = lookup S x" | |
|
18 "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)" |
|
19 |
|
20 lemma aval'_sound: "s : \<gamma>\<^sub>f S \<Longrightarrow> aval a s : \<gamma>(aval' a S)" |
|
21 by (induction a) (auto simp: gamma_num' gamma_plus' \<gamma>_st_def lookup_def) |
|
22 |
|
23 end |
|
24 |
|
25 text{* The for-clause (here and elsewhere) only serves the purpose of fixing |
|
26 the name of the type parameter @{typ 'av} which would otherwise be renamed to |
|
27 @{typ 'a}. *} |
|
28 |
|
29 locale Abs_Int = Gamma where \<gamma>=\<gamma> for \<gamma> :: "'av::SL_top \<Rightarrow> val set" |
|
30 begin |
|
31 |
|
32 fun step' :: "'av st option \<Rightarrow> 'av st option acom \<Rightarrow> 'av st option acom" where |
|
33 "step' S (SKIP {P}) = (SKIP {S})" | |
|
34 "step' S (x ::= e {P}) = |
|
35 x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S))}" | |
|
36 "step' S (c1;; c2) = step' S c1;; step' (post c1) c2" | |
|
37 "step' S (IF b THEN c1 ELSE c2 {P}) = |
|
38 (let c1' = step' S c1; c2' = step' S c2 |
|
39 in IF b THEN c1' ELSE c2' {post c1 \<squnion> post c2})" | |
|
40 "step' S ({Inv} WHILE b DO c {P}) = |
|
41 {S \<squnion> post c} WHILE b DO step' Inv c {Inv}" |
|
42 |
|
43 definition AI :: "com \<Rightarrow> 'av st option acom option" where |
|
44 "AI = lpfp\<^sub>c (step' \<top>)" |
|
45 |
|
46 |
|
47 lemma strip_step'[simp]: "strip(step' S c) = strip c" |
|
48 by(induct c arbitrary: S) (simp_all add: Let_def) |
|
49 |
|
50 |
|
51 text{* Soundness: *} |
|
52 |
|
53 lemma in_gamma_update: |
|
54 "\<lbrakk> s : \<gamma>\<^sub>f S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^sub>f(update S x a)" |
|
55 by(simp add: \<gamma>_st_def lookup_update) |
|
56 |
|
57 text{* The soundness proofs are textually identical to the ones for the step |
|
58 function operating on states as functions. *} |
|
59 |
|
60 lemma step_preserves_le: |
|
61 "\<lbrakk> S \<subseteq> \<gamma>\<^sub>o S'; c \<le> \<gamma>\<^sub>c c' \<rbrakk> \<Longrightarrow> step S c \<le> \<gamma>\<^sub>c (step' S' c')" |
|
62 proof(induction c arbitrary: c' S S') |
|
63 case SKIP thus ?case by(auto simp:SKIP_le map_acom_SKIP) |
|
64 next |
|
65 case Assign thus ?case |
|
66 by (fastforce simp: Assign_le map_acom_Assign intro: aval'_sound in_gamma_update |
|
67 split: option.splits del:subsetD) |
|
68 next |
|
69 case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq) |
|
70 by (metis le_post post_map_acom) |
|
71 next |
|
72 case (If b c1 c2 P) |
|
73 then obtain c1' c2' P' where |
|
74 "c' = IF b THEN c1' ELSE c2' {P'}" |
|
75 "P \<subseteq> \<gamma>\<^sub>o P'" "c1 \<le> \<gamma>\<^sub>c c1'" "c2 \<le> \<gamma>\<^sub>c c2'" |
|
76 by (fastforce simp: If_le map_acom_If) |
|
77 moreover have "post c1 \<subseteq> \<gamma>\<^sub>o(post c1' \<squnion> post c2')" |
|
78 by (metis (no_types) `c1 \<le> \<gamma>\<^sub>c c1'` join_ge1 le_post mono_gamma_o order_trans post_map_acom) |
|
79 moreover have "post c2 \<subseteq> \<gamma>\<^sub>o(post c1' \<squnion> post c2')" |
|
80 by (metis (no_types) `c2 \<le> \<gamma>\<^sub>c c2'` join_ge2 le_post mono_gamma_o order_trans post_map_acom) |
|
81 ultimately show ?case using `S \<subseteq> \<gamma>\<^sub>o S'` by (simp add: If.IH subset_iff) |
|
82 next |
|
83 case (While I b c1 P) |
|
84 then obtain c1' I' P' where |
|
85 "c' = {I'} WHILE b DO c1' {P'}" |
|
86 "I \<subseteq> \<gamma>\<^sub>o I'" "P \<subseteq> \<gamma>\<^sub>o P'" "c1 \<le> \<gamma>\<^sub>c c1'" |
|
87 by (fastforce simp: map_acom_While While_le) |
|
88 moreover have "S \<union> post c1 \<subseteq> \<gamma>\<^sub>o (S' \<squnion> post c1')" |
|
89 using `S \<subseteq> \<gamma>\<^sub>o S'` le_post[OF `c1 \<le> \<gamma>\<^sub>c c1'`, simplified] |
|
90 by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_gamma_o order_trans) |
|
91 ultimately show ?case by (simp add: While.IH subset_iff) |
|
92 qed |
|
93 |
|
94 lemma AI_sound: "AI c = Some c' \<Longrightarrow> CS c \<le> \<gamma>\<^sub>c c'" |
|
95 proof(simp add: CS_def AI_def) |
|
96 assume 1: "lpfp\<^sub>c (step' \<top>) c = Some c'" |
|
97 have 2: "step' \<top> c' \<sqsubseteq> c'" by(rule lpfpc_pfp[OF 1]) |
|
98 have 3: "strip (\<gamma>\<^sub>c (step' \<top> c')) = c" |
|
99 by(simp add: strip_lpfpc[OF _ 1]) |
|
100 have "lfp (step UNIV) c \<le> \<gamma>\<^sub>c (step' \<top> c')" |
|
101 proof(rule lfp_lowerbound[simplified,OF 3]) |
|
102 show "step UNIV (\<gamma>\<^sub>c (step' \<top> c')) \<le> \<gamma>\<^sub>c (step' \<top> c')" |
|
103 proof(rule step_preserves_le[OF _ _]) |
|
104 show "UNIV \<subseteq> \<gamma>\<^sub>o \<top>" by simp |
|
105 show "\<gamma>\<^sub>c (step' \<top> c') \<le> \<gamma>\<^sub>c c'" by(rule mono_gamma_c[OF 2]) |
|
106 qed |
|
107 qed |
|
108 from this 2 show "lfp (step UNIV) c \<le> \<gamma>\<^sub>c c'" |
|
109 by (blast intro: mono_gamma_c order_trans) |
|
110 qed |
|
111 |
|
112 end |
|
113 |
|
114 |
|
115 subsubsection "Monotonicity" |
|
116 |
|
117 locale Abs_Int_mono = Abs_Int + |
|
118 assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2" |
|
119 begin |
|
120 |
|
121 lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'" |
|
122 by(induction e) (auto simp: le_st_def lookup_def mono_plus') |
|
123 |
|
124 lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> update S x a \<sqsubseteq> update S' x a'" |
|
125 by(auto simp add: le_st_def lookup_def update_def) |
|
126 |
|
127 lemma mono_step': "S \<sqsubseteq> S' \<Longrightarrow> c \<sqsubseteq> c' \<Longrightarrow> step' S c \<sqsubseteq> step' S' c'" |
|
128 apply(induction c c' arbitrary: S S' rule: le_acom.induct) |
|
129 apply (auto simp: Let_def mono_update mono_aval' mono_post le_join_disj |
|
130 split: option.split) |
|
131 done |
|
132 |
|
133 end |
|
134 |
|
135 |
|
136 subsubsection "Ascending Chain Condition" |
|
137 |
|
138 abbreviation "strict r == r \<inter> -(r^-1)" |
|
139 abbreviation "acc r == wf((strict r)^-1)" |
|
140 |
|
141 lemma strict_inv_image: "strict(inv_image r f) = inv_image (strict r) f" |
|
142 by(auto simp: inv_image_def) |
|
143 |
|
144 lemma acc_inv_image: |
|
145 "acc r \<Longrightarrow> acc (inv_image r f)" |
|
146 by (metis converse_inv_image strict_inv_image wf_inv_image) |
|
147 |
|
148 text{* ACC for option type: *} |
|
149 |
|
150 lemma acc_option: assumes "acc {(x,y::'a::preord). x \<sqsubseteq> y}" |
|
151 shows "acc {(x,y::'a::preord option). x \<sqsubseteq> y}" |
|
152 proof(auto simp: wf_eq_minimal) |
|
153 fix xo :: "'a option" and Qo assume "xo : Qo" |
|
154 let ?Q = "{x. Some x \<in> Qo}" |
|
155 show "\<exists>yo\<in>Qo. \<forall>zo. yo \<sqsubseteq> zo \<and> ~ zo \<sqsubseteq> yo \<longrightarrow> zo \<notin> Qo" (is "\<exists>zo\<in>Qo. ?P zo") |
|
156 proof cases |
|
157 assume "?Q = {}" |
|
158 hence "?P None" by auto |
|
159 moreover have "None \<in> Qo" using `?Q = {}` `xo : Qo` |
|
160 by auto (metis not_Some_eq) |
|
161 ultimately show ?thesis by blast |
|
162 next |
|
163 assume "?Q \<noteq> {}" |
|
164 with assms show ?thesis |
|
165 apply(auto simp: wf_eq_minimal) |
|
166 apply(erule_tac x="?Q" in allE) |
|
167 apply auto |
|
168 apply(rule_tac x = "Some z" in bexI) |
|
169 by auto |
|
170 qed |
|
171 qed |
|
172 |
|
173 text{* ACC for abstract states, via measure functions. *} |
|
174 |
|
175 lemma measure_st: assumes "(strict{(x,y::'a::SL_top). x \<sqsubseteq> y})^-1 <= measure m" |
|
176 and "\<forall>x y::'a::SL_top. x \<sqsubseteq> y \<and> y \<sqsubseteq> x \<longrightarrow> m x = m y" |
|
177 shows "(strict{(S,S'::'a::SL_top st). S \<sqsubseteq> S'})^-1 \<subseteq> |
|
178 measure(%fd. \<Sum>x| x\<in>set(dom fd) \<and> ~ \<top> \<sqsubseteq> fun fd x. m(fun fd x)+1)" |
|
179 proof- |
|
180 { fix S S' :: "'a st" assume "S \<sqsubseteq> S'" "~ S' \<sqsubseteq> S" |
|
181 let ?X = "set(dom S)" let ?Y = "set(dom S')" |
|
182 let ?f = "fun S" let ?g = "fun S'" |
|
183 let ?X' = "{x:?X. ~ \<top> \<sqsubseteq> ?f x}" let ?Y' = "{y:?Y. ~ \<top> \<sqsubseteq> ?g y}" |
|
184 from `S \<sqsubseteq> S'` have "ALL y:?Y'\<inter>?X. ?f y \<sqsubseteq> ?g y" |
|
185 by(auto simp: le_st_def lookup_def) |
|
186 hence 1: "ALL y:?Y'\<inter>?X. m(?g y)+1 \<le> m(?f y)+1" |
|
187 using assms(1,2) by(fastforce) |
|
188 from `~ S' \<sqsubseteq> S` obtain u where u: "u : ?X" "~ lookup S' u \<sqsubseteq> ?f u" |
|
189 by(auto simp: le_st_def) |
|
190 hence "u : ?X'" by simp (metis preord_class.le_trans top) |
|
191 have "?Y'-?X = {}" using `S \<sqsubseteq> S'` by(fastforce simp: le_st_def lookup_def) |
|
192 have "?Y'\<inter>?X <= ?X'" apply auto |
|
193 apply (metis `S \<sqsubseteq> S'` le_st_def lookup_def preord_class.le_trans) |
|
194 done |
|
195 have "(\<Sum>y\<in>?Y'. m(?g y)+1) = (\<Sum>y\<in>(?Y'-?X) \<union> (?Y'\<inter>?X). m(?g y)+1)" |
|
196 by (metis Un_Diff_Int) |
|
197 also have "\<dots> = (\<Sum>y\<in>?Y'\<inter>?X. m(?g y)+1)" |
|
198 using `?Y'-?X = {}` by (metis Un_empty_left) |
|
199 also have "\<dots> < (\<Sum>x\<in>?X'. m(?f x)+1)" |
|
200 proof cases |
|
201 assume "u \<in> ?Y'" |
|
202 hence "m(?g u) < m(?f u)" using assms(1) `S \<sqsubseteq> S'` u |
|
203 by (fastforce simp: le_st_def lookup_def) |
|
204 have "(\<Sum>y\<in>?Y'\<inter>?X. m(?g y)+1) < (\<Sum>y\<in>?Y'\<inter>?X. m(?f y)+1)" |
|
205 using `u:?X` `u:?Y'` `m(?g u) < m(?f u)` |
|
206 by(fastforce intro!: sum_strict_mono_ex1[OF _ 1]) |
|
207 also have "\<dots> \<le> (\<Sum>y\<in>?X'. m(?f y)+1)" |
|
208 by(simp add: sum_mono3[OF _ `?Y'\<inter>?X <= ?X'`]) |
|
209 finally show ?thesis . |
|
210 next |
|
211 assume "u \<notin> ?Y'" |
|
212 with `?Y'\<inter>?X <= ?X'` have "?Y'\<inter>?X - {u} <= ?X' - {u}" by blast |
|
213 have "(\<Sum>y\<in>?Y'\<inter>?X. m(?g y)+1) = (\<Sum>y\<in>?Y'\<inter>?X - {u}. m(?g y)+1)" |
|
214 proof- |
|
215 have "?Y'\<inter>?X = ?Y'\<inter>?X - {u}" using `u \<notin> ?Y'` by auto |
|
216 thus ?thesis by metis |
|
217 qed |
|
218 also have "\<dots> < (\<Sum>y\<in>?Y'\<inter>?X-{u}. m(?g y)+1) + (\<Sum>y\<in>{u}. m(?f y)+1)" by simp |
|
219 also have "(\<Sum>y\<in>?Y'\<inter>?X-{u}. m(?g y)+1) \<le> (\<Sum>y\<in>?Y'\<inter>?X-{u}. m(?f y)+1)" |
|
220 using 1 by(blast intro: sum_mono) |
|
221 also have "\<dots> \<le> (\<Sum>y\<in>?X'-{u}. m(?f y)+1)" |
|
222 by(simp add: sum_mono3[OF _ `?Y'\<inter>?X-{u} <= ?X'-{u}`]) |
|
223 also have "\<dots> + (\<Sum>y\<in>{u}. m(?f y)+1)= (\<Sum>y\<in>(?X'-{u}) \<union> {u}. m(?f y)+1)" |
|
224 using `u:?X'` by(subst sum.union_disjoint[symmetric]) auto |
|
225 also have "\<dots> = (\<Sum>x\<in>?X'. m(?f x)+1)" |
|
226 using `u : ?X'` by(simp add:insert_absorb) |
|
227 finally show ?thesis by (blast intro: add_right_mono) |
|
228 qed |
|
229 finally have "(\<Sum>y\<in>?Y'. m(?g y)+1) < (\<Sum>x\<in>?X'. m(?f x)+1)" . |
|
230 } thus ?thesis by(auto simp add: measure_def inv_image_def) |
|
231 qed |
|
232 |
|
233 text{* ACC for acom. First the ordering on acom is related to an ordering on |
|
234 lists of annotations. *} |
|
235 |
|
236 (* FIXME mv and add [simp] *) |
|
237 lemma listrel_Cons_iff: |
|
238 "(x#xs, y#ys) : listrel r \<longleftrightarrow> (x,y) \<in> r \<and> (xs,ys) \<in> listrel r" |
|
239 by (blast intro:listrel.Cons) |
|
240 |
|
241 lemma listrel_app: "(xs1,ys1) : listrel r \<Longrightarrow> (xs2,ys2) : listrel r |
|
242 \<Longrightarrow> (xs1@xs2, ys1@ys2) : listrel r" |
|
243 by(auto simp add: listrel_iff_zip) |
|
244 |
|
245 lemma listrel_app_same_size: "size xs1 = size ys1 \<Longrightarrow> size xs2 = size ys2 \<Longrightarrow> |
|
246 (xs1@xs2, ys1@ys2) : listrel r \<longleftrightarrow> |
|
247 (xs1,ys1) : listrel r \<and> (xs2,ys2) : listrel r" |
|
248 by(auto simp add: listrel_iff_zip) |
|
249 |
|
250 lemma listrel_converse: "listrel(r^-1) = (listrel r)^-1" |
|
251 proof- |
|
252 { fix xs ys |
|
253 have "(xs,ys) : listrel(r^-1) \<longleftrightarrow> (ys,xs) : listrel r" |
|
254 apply(induct xs arbitrary: ys) |
|
255 apply (fastforce simp: listrel.Nil) |
|
256 apply (fastforce simp: listrel_Cons_iff) |
|
257 done |
|
258 } thus ?thesis by auto |
|
259 qed |
|
260 |
|
261 (* It would be nice to get rid of refl & trans and build them into the proof *) |
|
262 lemma acc_listrel: fixes r :: "('a*'a)set" assumes "refl r" and "trans r" |
|
263 and "acc r" shows "acc (listrel r - {([],[])})" |
|
264 proof- |
|
265 have refl: "!!x. (x,x) : r" using `refl r` unfolding refl_on_def by blast |
|
266 have trans: "!!x y z. (x,y) : r \<Longrightarrow> (y,z) : r \<Longrightarrow> (x,z) : r" |
|
267 using `trans r` unfolding trans_def by blast |
|
268 from assms(3) obtain mx :: "'a set \<Rightarrow> 'a" where |
|
269 mx: "!!S x. x:S \<Longrightarrow> mx S : S \<and> (\<forall>y. (mx S,y) : strict r \<longrightarrow> y \<notin> S)" |
|
270 by(simp add: wf_eq_minimal) metis |
|
271 let ?R = "listrel r - {([], [])}" |
|
272 { fix Q and xs :: "'a list" |
|
273 have "xs \<in> Q \<Longrightarrow> \<exists>ys. ys\<in>Q \<and> (\<forall>zs. (ys, zs) \<in> strict ?R \<longrightarrow> zs \<notin> Q)" |
|
274 (is "_ \<Longrightarrow> \<exists>ys. ?P Q ys") |
|
275 proof(induction xs arbitrary: Q rule: length_induct) |
|
276 case (1 xs) |
|
277 { have "!!ys Q. size ys < size xs \<Longrightarrow> ys : Q \<Longrightarrow> EX ms. ?P Q ms" |
|
278 using "1.IH" by blast |
|
279 } note IH = this |
|
280 show ?case |
|
281 proof(cases xs) |
|
282 case Nil with `xs : Q` have "?P Q []" by auto |
|
283 thus ?thesis by blast |
|
284 next |
|
285 case (Cons x ys) |
|
286 let ?Q1 = "{a. \<exists>bs. size bs = size ys \<and> a#bs : Q}" |
|
287 have "x : ?Q1" using `xs : Q` Cons by auto |
|
288 from mx[OF this] obtain m1 where |
|
289 1: "m1 \<in> ?Q1 \<and> (\<forall>y. (m1,y) \<in> strict r \<longrightarrow> y \<notin> ?Q1)" by blast |
|
290 then obtain ms1 where "size ms1 = size ys" "m1#ms1 : Q" by blast+ |
|
291 hence "size ms1 < size xs" using Cons by auto |
|
292 let ?Q2 = "{bs. \<exists>m1'. (m1',m1):r \<and> (m1,m1'):r \<and> m1'#bs : Q \<and> size bs = size ms1}" |
|
293 have "ms1 : ?Q2" using `m1#ms1 : Q` by(blast intro: refl) |
|
294 from IH[OF `size ms1 < size xs` this] |
|
295 obtain ms where 2: "?P ?Q2 ms" by auto |
|
296 then obtain m1' where m1': "(m1',m1) : r \<and> (m1,m1') : r \<and> m1'#ms : Q" |
|
297 by blast |
|
298 hence "\<forall>ab. (m1'#ms,ab) : strict ?R \<longrightarrow> ab \<notin> Q" using 1 2 |
|
299 apply (auto simp: listrel_Cons_iff) |
|
300 apply (metis `length ms1 = length ys` listrel_eq_len trans) |
|
301 by (metis `length ms1 = length ys` listrel_eq_len trans) |
|
302 with m1' show ?thesis by blast |
|
303 qed |
|
304 qed |
|
305 } |
|
306 thus ?thesis unfolding wf_eq_minimal by (metis converse_iff) |
|
307 qed |
|
308 |
|
309 |
|
310 lemma le_iff_le_annos: "c1 \<sqsubseteq> c2 \<longleftrightarrow> |
|
311 (annos c1, annos c2) : listrel{(x,y). x \<sqsubseteq> y} \<and> strip c1 = strip c2" |
|
312 apply(induct c1 c2 rule: le_acom.induct) |
|
313 apply (auto simp: listrel.Nil listrel_Cons_iff listrel_app size_annos_same2) |
|
314 apply (metis listrel_app_same_size size_annos_same)+ |
|
315 done |
|
316 |
|
317 lemma le_acom_subset_same_annos: |
|
318 "(strict{(c,c'::'a::preord acom). c \<sqsubseteq> c'})^-1 \<subseteq> |
|
319 (strict(inv_image (listrel{(a,a'::'a). a \<sqsubseteq> a'} - {([],[])}) annos))^-1" |
|
320 by(auto simp: le_iff_le_annos) |
|
321 |
|
322 lemma acc_acom: "acc {(a,a'::'a::preord). a \<sqsubseteq> a'} \<Longrightarrow> |
|
323 acc {(c,c'::'a acom). c \<sqsubseteq> c'}" |
|
324 apply(rule wf_subset[OF _ le_acom_subset_same_annos]) |
|
325 apply(rule acc_inv_image[OF acc_listrel]) |
|
326 apply(auto simp: refl_on_def trans_def intro: le_trans) |
|
327 done |
|
328 |
|
329 text{* Termination of the fixed-point finders, assuming monotone functions: *} |
|
330 |
|
331 lemma pfp_termination: |
|
332 fixes x0 :: "'a::preord" |
|
333 assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "acc {(x::'a,y). x \<sqsubseteq> y}" |
|
334 and "x0 \<sqsubseteq> f x0" shows "EX x. pfp f x0 = Some x" |
|
335 proof(simp add: pfp_def, rule wf_while_option_Some[where P = "%x. x \<sqsubseteq> f x"]) |
|
336 show "wf {(x, s). (s \<sqsubseteq> f s \<and> \<not> f s \<sqsubseteq> s) \<and> x = f s}" |
|
337 by(rule wf_subset[OF assms(2)]) auto |
|
338 next |
|
339 show "x0 \<sqsubseteq> f x0" by(rule assms) |
|
340 next |
|
341 fix x assume "x \<sqsubseteq> f x" thus "f x \<sqsubseteq> f(f x)" by(rule mono) |
|
342 qed |
|
343 |
|
344 lemma lpfpc_termination: |
|
345 fixes f :: "(('a::SL_top)option acom \<Rightarrow> 'a option acom)" |
|
346 assumes "acc {(x::'a,y). x \<sqsubseteq> y}" and "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" |
|
347 and "\<And>c. strip(f c) = strip c" |
|
348 shows "\<exists>c'. lpfp\<^sub>c f c = Some c'" |
|
349 unfolding lpfp\<^sub>c_def |
|
350 apply(rule pfp_termination) |
|
351 apply(erule assms(2)) |
|
352 apply(rule acc_acom[OF acc_option[OF assms(1)]]) |
|
353 apply(simp add: bot_acom assms(3)) |
|
354 done |
|
355 |
|
356 context Abs_Int_mono |
|
357 begin |
|
358 |
|
359 lemma AI_Some_measure: |
|
360 assumes "(strict{(x,y::'a). x \<sqsubseteq> y})^-1 <= measure m" |
|
361 and "\<forall>x y::'a. x \<sqsubseteq> y \<and> y \<sqsubseteq> x \<longrightarrow> m x = m y" |
|
362 shows "\<exists>c'. AI c = Some c'" |
|
363 unfolding AI_def |
|
364 apply(rule lpfpc_termination) |
|
365 apply(rule wf_subset[OF wf_measure measure_st[OF assms]]) |
|
366 apply(erule mono_step'[OF le_refl]) |
|
367 apply(rule strip_step') |
|
368 done |
|
369 |
|
370 end |
|
371 |
|
372 end |
|