--- a/src/HOL/IMP/Abs_Int0.thy Wed Nov 23 23:31:32 2011 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy Thu Nov 24 19:58:37 2011 +0100
@@ -6,10 +6,10 @@
subsection "Computable Abstract Interpretation"
-text{* Abstract interpretation over type @{text astate} instead of
+text{* Abstract interpretation over type @{text st} instead of
functions. *}
-locale Abs_Int = Val_abs
+context Val_abs
begin
fun aval' :: "aexp \<Rightarrow> 'a st \<Rightarrow> 'a" where
@@ -17,10 +17,18 @@
"aval' (V x) S = lookup S x" |
"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
-fun step :: "'a st up \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom" where
+lemma aval'_sound: "s : \<gamma>\<^isub>f S \<Longrightarrow> aval a s : \<gamma>(aval' a S)"
+by (induct a) (auto simp: rep_num' rep_plus' rep_st_def lookup_def)
+
+end
+
+locale Abs_Int = Val_abs
+begin
+
+fun step :: "'a st option \<Rightarrow> 'a st option acom \<Rightarrow> 'a st option acom" where
"step S (SKIP {P}) = (SKIP {S})" |
"step S (x ::= e {P}) =
- x ::= e {case S of Bot \<Rightarrow> Bot | Up S \<Rightarrow> Up(update S x (aval' e S))}" |
+ x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S))}" |
"step S (c1; c2) = step S c1; step (post c1) c2" |
"step S (IF b THEN c1 ELSE c2 {P}) =
(let c1' = step S c1; c2' = step S c2
@@ -28,7 +36,7 @@
"step S ({Inv} WHILE b DO c {P}) =
{S \<squnion> post c} WHILE b DO step Inv c {Inv}"
-definition AI :: "com \<Rightarrow> 'a st up acom option" where
+definition AI :: "com \<Rightarrow> 'a st option acom option" where
"AI = lpfp\<^isub>c (step \<top>)"
@@ -38,47 +46,73 @@
text{* Soundness: *}
-lemma aval'_sound: "s <:f S \<Longrightarrow> aval a s <: aval' a S"
-by (induct a) (auto simp: rep_num' rep_plus' rep_st_def lookup_def)
-
-lemma in_rep_update: "\<lbrakk> s <:f S; i <: a \<rbrakk> \<Longrightarrow> s(x := i) <:f update S x a"
+lemma in_rep_update:
+ "\<lbrakk> s : \<gamma>\<^isub>f S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>f(update S x a)"
by(simp add: rep_st_def lookup_update)
-lemma step_sound:
- "step S c \<sqsubseteq> c \<Longrightarrow> (strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up S \<Longrightarrow> t <:up post c"
-proof(induction c arbitrary: S s t)
+text{* The soundness proofs are textually identical to the ones for the step
+function operating on states as functions. *}
+
+lemma step_preserves_le2:
+ "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c; strip ca = c \<rbrakk>
+ \<Longrightarrow> step_cs S cs \<le> \<gamma>\<^isub>c (step sa ca)"
+proof(induction c arbitrary: cs ca S sa)
case SKIP thus ?case
- by simp (metis skipE up_fun_in_rep_le)
+ by(auto simp:strip_eq_SKIP)
next
case Assign thus ?case
- apply (auto simp del: fun_upd_apply simp: split: up.splits)
- by (metis aval'_sound fun_in_rep_le in_rep_update)
-next
- case Semi thus ?case by simp blast
+ by (fastforce simp: strip_eq_Assign intro: aval'_sound in_rep_update
+ split: option.splits del:subsetD)
next
- case (If b c1 c2 S0) thus ?case
- apply(auto simp: Let_def)
- apply (metis up_fun_in_rep_le)+
- done
+ case Semi thus ?case apply (auto simp: strip_eq_Semi)
+ by (metis le_post post_map_acom)
next
- case (While Inv b c P)
- from While.prems have inv: "step Inv c \<sqsubseteq> c"
- and "post c \<sqsubseteq> Inv" and "S \<sqsubseteq> Inv" and "Inv \<sqsubseteq> P" by(auto simp: Let_def)
- { fix s t have "(WHILE b DO strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up Inv \<Longrightarrow> t <:up Inv"
- proof(induction "WHILE b DO strip c" s t rule: big_step_induct)
- case WhileFalse thus ?case by simp
- next
- case (WhileTrue s1 s2 s3)
- from WhileTrue.hyps(5)[OF up_fun_in_rep_le[OF While.IH[OF inv `(strip c, s1) \<Rightarrow> s2` `s1 <:up Inv`] `post c \<sqsubseteq> Inv`]]
- show ?case .
- qed
- }
- thus ?case using While.prems(2)
- by simp (metis `s <:up S` `S \<sqsubseteq> Inv` `Inv \<sqsubseteq> P` up_fun_in_rep_le)
+ case (If b c1 c2)
+ then obtain cs1 cs2 ca1 ca2 P Pa where
+ "cs = IF b THEN cs1 ELSE cs2 {P}" "ca = IF b THEN ca1 ELSE ca2 {Pa}"
+ "P \<subseteq> \<gamma>\<^isub>u Pa" "cs1 \<le> \<gamma>\<^isub>c ca1" "cs2 \<le> \<gamma>\<^isub>c ca2"
+ "strip cs1 = c1" "strip ca1 = c1" "strip cs2 = c2" "strip ca2 = c2"
+ by (fastforce simp: strip_eq_If)
+ moreover have "post cs1 \<subseteq> \<gamma>\<^isub>u(post ca1 \<squnion> post ca2)"
+ by (metis (no_types) `cs1 \<le> \<gamma>\<^isub>c ca1` join_ge1 le_post mono_rep_u order_trans post_map_acom)
+ moreover have "post cs2 \<subseteq> \<gamma>\<^isub>u(post ca1 \<squnion> post ca2)"
+ by (metis (no_types) `cs2 \<le> \<gamma>\<^isub>c ca2` join_ge2 le_post mono_rep_u order_trans post_map_acom)
+ ultimately show ?case using If.prems(1) by (simp add: If.IH subset_iff)
+next
+ case (While b c1)
+ then obtain cs1 ca1 I P Ia Pa where
+ "cs = {I} WHILE b DO cs1 {P}" "ca = {Ia} WHILE b DO ca1 {Pa}"
+ "I \<subseteq> \<gamma>\<^isub>u Ia" "P \<subseteq> \<gamma>\<^isub>u Pa" "cs1 \<le> \<gamma>\<^isub>c ca1"
+ "strip cs1 = c1" "strip ca1 = c1"
+ by (fastforce simp: strip_eq_While)
+ moreover have "S \<union> post cs1 \<subseteq> \<gamma>\<^isub>u (sa \<squnion> post ca1)"
+ using `S \<subseteq> \<gamma>\<^isub>u sa` le_post[OF `cs1 \<le> \<gamma>\<^isub>c ca1`, simplified]
+ by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_rep_u order_trans)
+ ultimately show ?case by (simp add: While.IH subset_iff)
qed
-lemma AI_sound: "\<lbrakk> AI c = Some c'; (c,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> t <:up post c'"
-by (metis AI_def in_rep_Top_up lpfpc_pfp step_sound strip_lpfpc strip_step)
+lemma step_preserves_le:
+ "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c \<rbrakk>
+ \<Longrightarrow> step_cs S cs \<le> \<gamma>\<^isub>c(step sa ca)"
+by (metis le_strip step_preserves_le2 strip_acom)
+
+lemma AI_sound: "AI c = Some c' \<Longrightarrow> CS UNIV c \<le> \<gamma>\<^isub>c c'"
+proof(simp add: CS_def AI_def)
+ assume 1: "lpfp\<^isub>c (step \<top>) c = Some c'"
+ have 2: "step \<top> c' \<sqsubseteq> c'" by(rule lpfpc_pfp[OF 1])
+ have 3: "strip (\<gamma>\<^isub>c (step \<top> c')) = c"
+ by(simp add: strip_lpfpc[OF _ 1])
+ have "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c (step \<top> c')"
+ proof(rule lfp_lowerbound[OF 3])
+ show "step_cs UNIV (\<gamma>\<^isub>c (step \<top> c')) \<le> \<gamma>\<^isub>c (step \<top> c')"
+ proof(rule step_preserves_le[OF _ _ 3])
+ show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
+ show "\<gamma>\<^isub>c (step \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
+ qed
+ qed
+ from this 2 show "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c c'"
+ by (blast intro: mono_rep_c order_trans)
+qed
end
@@ -97,7 +131,7 @@
lemma step_mono: "S \<sqsubseteq> S' \<Longrightarrow> step S c \<sqsubseteq> step S' c"
apply(induction c arbitrary: S S')
-apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: up.split)
+apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: option.split)
done
end