199 by(simp add: bot_def) |
199 by(simp add: bot_def) |
200 |
200 |
201 |
201 |
202 subsubsection "Post-fixed point iteration" |
202 subsubsection "Post-fixed point iteration" |
203 |
203 |
204 definition |
204 definition pfp :: "(('a::preord) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where |
205 pfp :: "(('a::preord) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where |
|
206 "pfp f = while_option (\<lambda>x. \<not> f x \<sqsubseteq> x) f" |
205 "pfp f = while_option (\<lambda>x. \<not> f x \<sqsubseteq> x) f" |
207 |
206 |
208 lemma pfp_pfp: assumes "pfp f x0 = Some x" shows "f x \<sqsubseteq> x" |
207 lemma pfp_pfp: assumes "pfp f x0 = Some x" shows "f x \<sqsubseteq> x" |
209 using while_option_stop[OF assms[simplified pfp_def]] by simp |
208 using while_option_stop[OF assms[simplified pfp_def]] by simp |
210 |
209 |
211 lemma pfp_least: |
210 lemma while_least: |
212 assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" |
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" |
213 and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" and "pfp f x0 = Some x" shows "x \<sqsubseteq> p" |
212 and "\<forall>x \<in> L. b \<sqsubseteq> x" and "b \<in> L" and "f q \<sqsubseteq> q" and "q \<in> L" |
214 proof- |
213 and "while_option P f b = Some p" |
215 { fix x assume "x \<sqsubseteq> p" |
214 shows "p \<sqsubseteq> q" |
216 hence "f x \<sqsubseteq> f p" by(rule mono) |
215 using while_option_rule[OF _ assms(7)[unfolded pfp_def], |
217 from this `f p \<sqsubseteq> p` have "f x \<sqsubseteq> p" by(rule le_trans) |
216 where P = "%x. x \<in> L \<and> x \<sqsubseteq> q"] |
218 } |
217 by (metis assms(1-6) le_trans) |
219 thus "x \<sqsubseteq> p" using assms(2-) while_option_rule[where P = "%x. x \<sqsubseteq> p"] |
218 |
220 unfolding pfp_def by blast |
219 lemma pfp_inv: |
221 qed |
220 "pfp f x = Some y \<Longrightarrow> (\<And>x. P x \<Longrightarrow> P(f x)) \<Longrightarrow> P x \<Longrightarrow> P y" |
222 |
221 unfolding pfp_def by (metis (lifting) while_option_rule) |
223 definition |
|
224 lpfp :: "('a::preord option acom \<Rightarrow> 'a option acom) \<Rightarrow> com \<Rightarrow> 'a option acom option" |
|
225 where "lpfp f c = pfp f (bot c)" |
|
226 |
|
227 lemma lpfpc_pfp: "lpfp f c = Some p \<Longrightarrow> f p \<sqsubseteq> p" |
|
228 by(simp add: pfp_pfp lpfp_def) |
|
229 |
222 |
230 lemma strip_pfp: |
223 lemma strip_pfp: |
231 assumes "\<And>x. g(f x) = g x" and "pfp f x0 = Some x" shows "g x = g x0" |
224 assumes "\<And>x. g(f x) = g x" and "pfp f x0 = Some x" shows "g x = g x0" |
232 using assms while_option_rule[where P = "%x. g x = g x0" and c = f] |
225 using pfp_inv[OF assms(2), where P = "%x. g x = g x0"] assms(1) by simp |
233 unfolding pfp_def by metis |
|
234 |
|
235 lemma strip_lpfp: assumes "\<And>C. strip(f C) = strip C" and "lpfp f c = Some C" |
|
236 shows "strip C = c" |
|
237 using assms(1) strip_pfp[OF _ assms(2)[simplified lpfp_def]] |
|
238 by(metis strip_bot) |
|
239 |
226 |
240 |
227 |
241 subsection "Abstract Interpretation" |
228 subsection "Abstract Interpretation" |
242 |
229 |
243 definition \<gamma>_fun :: "('a \<Rightarrow> 'b set) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b)set" where |
230 definition \<gamma>_fun :: "('a \<Rightarrow> 'b set) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b)set" where |
279 IF b THEN {S} step' P1 C1 ELSE {S} step' P2 C2 {post C1 \<squnion> post C2}" | |
266 IF b THEN {S} step' P1 C1 ELSE {S} step' P2 C2 {post C1 \<squnion> post C2}" | |
280 "step' S ({I} WHILE b DO {P} C {Q}) = |
267 "step' S ({I} WHILE b DO {P} C {Q}) = |
281 {S \<squnion> post C} WHILE b DO {I} step' P C {I}" |
268 {S \<squnion> post C} WHILE b DO {I} step' P C {I}" |
282 |
269 |
283 definition AI :: "com \<Rightarrow> 'av st option acom option" where |
270 definition AI :: "com \<Rightarrow> 'av st option acom option" where |
284 "AI = lpfp (step' \<top>)" |
271 "AI c = pfp (step' \<top>) (bot c)" |
285 |
272 |
286 |
273 |
287 lemma strip_step'[simp]: "strip(step' S C) = strip C" |
274 lemma strip_step'[simp]: "strip(step' S C) = strip C" |
288 by(induct C arbitrary: S) (simp_all add: Let_def) |
275 by(induct C arbitrary: S) (simp_all add: Let_def) |
289 |
276 |
359 |
346 |
360 qed |
347 qed |
361 |
348 |
362 lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C" |
349 lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C" |
363 proof(simp add: CS_def AI_def) |
350 proof(simp add: CS_def AI_def) |
364 assume 1: "lpfp (step' \<top>) c = Some C" |
351 assume 1: "pfp (step' \<top>) (bot c) = Some C" |
365 have 2: "step' \<top> C \<sqsubseteq> C" by(rule lpfpc_pfp[OF 1]) |
352 have 2: "step' \<top> C \<sqsubseteq> C" by(rule pfp_pfp[OF 1]) |
366 have 3: "strip (\<gamma>\<^isub>c (step' \<top> C)) = c" |
353 have 3: "strip (\<gamma>\<^isub>c (step' \<top> C)) = c" |
367 by(simp add: strip_lpfp[OF _ 1]) |
354 by(simp add: strip_pfp[OF _ 1]) |
368 have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> C)" |
355 have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> C)" |
369 proof(rule lfp_lowerbound[simplified,OF 3]) |
356 proof(rule lfp_lowerbound[simplified,OF 3]) |
370 show "step UNIV (\<gamma>\<^isub>c (step' \<top> C)) \<le> \<gamma>\<^isub>c (step' \<top> C)" |
357 show "step UNIV (\<gamma>\<^isub>c (step' \<top> C)) \<le> \<gamma>\<^isub>c (step' \<top> C)" |
371 proof(rule step_preserves_le[OF _ _]) |
358 proof(rule step_preserves_le[OF _ _]) |
372 show "UNIV \<subseteq> \<gamma>\<^isub>o \<top>" by simp |
359 show "UNIV \<subseteq> \<gamma>\<^isub>o \<top>" by simp |