Abstract interpretation is now based uniformly on annotated programs,
including a collecting and a small step semantics
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/ACom.thy Thu Nov 24 19:58:37 2011 +0100
@@ -0,0 +1,84 @@
+(* Author: Tobias Nipkow *)
+
+theory ACom
+imports Com
+begin
+
+(* is there a better place? *)
+definition "show_state xs s = [(x,s x). x \<leftarrow> xs]"
+
+section "Annotated Commands"
+
+datatype 'a acom =
+ SKIP 'a ("SKIP {_}") |
+ Assign vname aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
+ Semi "('a acom)" "('a acom)" ("_;//_" [60, 61] 60) |
+ If bexp "('a acom)" "('a acom)" 'a
+ ("(IF _/ THEN _/ ELSE _//{_})" [0, 0, 61, 0] 61) |
+ While 'a bexp "('a acom)" 'a
+ ("({_}//WHILE _/ DO (_)//{_})" [0, 0, 61, 0] 61)
+
+fun post :: "'a acom \<Rightarrow>'a" where
+"post (SKIP {P}) = P" |
+"post (x ::= e {P}) = P" |
+"post (c1; c2) = post c2" |
+"post (IF b THEN c1 ELSE c2 {P}) = P" |
+"post ({Inv} WHILE b DO c {P}) = P"
+
+fun strip :: "'a acom \<Rightarrow> com" where
+"strip (SKIP {a}) = com.SKIP" |
+"strip (x ::= e {a}) = (x ::= e)" |
+"strip (c1;c2) = (strip c1; strip c2)" |
+"strip (IF b THEN c1 ELSE c2 {a}) = (IF b THEN strip c1 ELSE strip c2)" |
+"strip ({a1} WHILE b DO c {a2}) = (WHILE b DO strip c)"
+
+fun anno :: "'a \<Rightarrow> com \<Rightarrow> 'a acom" where
+"anno a com.SKIP = SKIP {a}" |
+"anno a (x ::= e) = (x ::= e {a})" |
+"anno a (c1;c2) = (anno a c1; anno a c2)" |
+"anno a (IF b THEN c1 ELSE c2) =
+ (IF b THEN anno a c1 ELSE anno a c2 {a})" |
+"anno a (WHILE b DO c) =
+ ({a} WHILE b DO anno a c {a})"
+
+fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where
+"map_acom f (SKIP {a}) = SKIP {f a}" |
+"map_acom f (x ::= e {a}) = (x ::= e {f a})" |
+"map_acom f (c1;c2) = (map_acom f c1; map_acom f c2)" |
+"map_acom f (IF b THEN c1 ELSE c2 {a}) =
+ (IF b THEN map_acom f c1 ELSE map_acom f c2 {f a})" |
+"map_acom f ({a1} WHILE b DO c {a2}) =
+ ({f a1} WHILE b DO map_acom f c {f a2})"
+
+
+lemma post_map_acom[simp]: "post(map_acom f c) = f(post c)"
+by (induction c) simp_all
+
+lemma strip_acom[simp]: "strip (map_acom f c) = strip c"
+by (induction c) auto
+
+
+lemma strip_anno[simp]: "strip (anno a c) = c"
+by(induct c) simp_all
+
+lemma strip_eq_SKIP: "strip c = com.SKIP \<longleftrightarrow> (EX P. c = SKIP {P})"
+by (cases c) simp_all
+
+lemma strip_eq_Assign: "strip c = x::=e \<longleftrightarrow> (EX P. c = x::=e {P})"
+by (cases c) simp_all
+
+lemma strip_eq_Semi:
+ "strip c = c1;c2 \<longleftrightarrow> (EX d1 d2. c = d1;d2 & strip d1 = c1 & strip d2 = c2)"
+by (cases c) simp_all
+
+lemma strip_eq_If:
+ "strip c = IF b THEN c1 ELSE c2 \<longleftrightarrow>
+ (EX d1 d2 P. c = IF b THEN d1 ELSE d2 {P} & strip d1 = c1 & strip d2 = c2)"
+by (cases c) simp_all
+
+lemma strip_eq_While:
+ "strip c = WHILE b DO c1 \<longleftrightarrow>
+ (EX I d1 P. c = {I} WHILE b DO d1 {P} & strip d1 = c1)"
+by (cases c) simp_all
+
+end
--- 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
--- a/src/HOL/IMP/Abs_Int0_const.thy Wed Nov 23 23:31:32 2011 +0100
+++ b/src/HOL/IMP/Abs_Int0_const.thy Thu Nov 24 19:58:37 2011 +0100
@@ -1,7 +1,7 @@
(* Author: Tobias Nipkow *)
theory Abs_Int0_const
-imports Abs_Int0
+imports Abs_Int0 Abs_Int_Tests
begin
subsection "Constant Propagation"
@@ -53,6 +53,7 @@
interpretation Val_abs rep_cval Const plus_cval
+defines aval'_const is aval'
proof
case goal1 thus ?case
by(cases a, cases b, simp, simp, cases b, simp, simp)
@@ -67,43 +68,20 @@
interpretation Abs_Int rep_cval Const plus_cval
defines AI_const is AI
-and aval'_const is aval'
and step_const is step
proof qed
-text{* Straight line code: *}
-definition "test1_const =
- ''y'' ::= N 7;
- ''z'' ::= Plus (V ''y'') (N 2);
- ''y'' ::= Plus (V ''x'') (N 0)"
-text{* Conditional: *}
-definition "test2_const =
- IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 5"
-
-text{* Conditional, test is ignored: *}
-definition "test3_const =
- ''x'' ::= N 42;
- IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6"
+text{* Monotonicity: *}
-text{* While: *}
-definition "test4_const =
- ''x'' ::= N 0; WHILE Bc True DO ''x'' ::= N 0"
-
-text{* While, test is ignored: *}
-definition "test5_const =
- ''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
+interpretation Abs_Int_mono rep_cval Const plus_cval
+proof
+ case goal1 thus ?case
+ by(auto simp: plus_cval_cases split: cval.split)
+qed
-text{* Iteration is needed: *}
-definition "test6_const =
- ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 2;
- WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y''; ''y'' ::= V ''z'')"
-text{* More iteration would be needed: *}
-definition "test7_const =
- ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 0; ''u'' ::= N 3;
- WHILE Less (V ''x'') (N 1)
- DO (''x'' ::= V ''y''; ''y'' ::= V ''z''; ''z'' ::= V ''u'')"
+subsubsection "Tests"
value [code] "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test1_const))"
value [code] "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test1_const))"
@@ -129,14 +107,5 @@
value [code] "show_acom_opt (AI_const test5_const)"
value [code] "show_acom_opt (AI_const test6_const)"
-value [code] "show_acom_opt (AI_const test7_const)"
-
-text{* Monotonicity: *}
-
-interpretation Abs_Int_mono rep_cval Const plus_cval
-proof
- case goal1 thus ?case
- by(auto simp: plus_cval_cases split: cval.split)
-qed
end
--- a/src/HOL/IMP/Abs_Int0_fun.thy Wed Nov 23 23:31:32 2011 +0100
+++ b/src/HOL/IMP/Abs_Int0_fun.thy Thu Nov 24 19:58:37 2011 +0100
@@ -3,57 +3,11 @@
header "Abstract Interpretation"
theory Abs_Int0_fun
-imports "~~/src/HOL/ex/Interpretation_with_Defs" Big_Step
+imports "~~/src/HOL/ex/Interpretation_with_Defs"
"~~/src/HOL/Library/While_Combinator"
+ Collecting
begin
-subsection "Annotated Commands"
-
-datatype 'a acom =
- SKIP 'a ("SKIP {_}") |
- Assign vname aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
- Semi "('a acom)" "('a acom)" ("_;//_" [60, 61] 60) |
- If bexp "('a acom)" "('a acom)" 'a
- ("(IF _/ THEN _/ ELSE _//{_})" [0, 0, 61, 0] 61) |
- While 'a bexp "('a acom)" 'a
- ("({_}//WHILE _/ DO (_)//{_})" [0, 0, 61, 0] 61)
-
-fun post :: "'a acom \<Rightarrow>'a" where
-"post (SKIP {P}) = P" |
-"post (x ::= e {P}) = P" |
-"post (c1; c2) = post c2" |
-"post (IF b THEN c1 ELSE c2 {P}) = P" |
-"post ({Inv} WHILE b DO c {P}) = P"
-
-fun strip :: "'a acom \<Rightarrow> com" where
-"strip (SKIP {a}) = com.SKIP" |
-"strip (x ::= e {a}) = (x ::= e)" |
-"strip (c1;c2) = (strip c1; strip c2)" |
-"strip (IF b THEN c1 ELSE c2 {a}) = (IF b THEN strip c1 ELSE strip c2)" |
-"strip ({a1} WHILE b DO c {a2}) = (WHILE b DO strip c)"
-
-fun anno :: "'a \<Rightarrow> com \<Rightarrow> 'a acom" where
-"anno a com.SKIP = SKIP {a}" |
-"anno a (x ::= e) = (x ::= e {a})" |
-"anno a (c1;c2) = (anno a c1; anno a c2)" |
-"anno a (IF b THEN c1 ELSE c2) =
- (IF b THEN anno a c1 ELSE anno a c2 {a})" |
-"anno a (WHILE b DO c) =
- ({a} WHILE b DO anno a c {a})"
-
-lemma strip_anno[simp]: "strip (anno a c) = c"
-by(induct c) simp_all
-
-fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where
-"map_acom f (SKIP {a}) = SKIP {f a}" |
-"map_acom f (x ::= e {a}) = (x ::= e {f a})" |
-"map_acom f (c1;c2) = (map_acom f c1; map_acom f c2)" |
-"map_acom f (IF b THEN c1 ELSE c2 {a}) =
- (IF b THEN map_acom f c1 ELSE map_acom f c2 {f a})" |
-"map_acom f ({a1} WHILE b DO c {a2}) =
- ({f a1} WHILE b DO map_acom f c {f a2})"
-
-
subsection "Orderings"
class preord =
@@ -159,31 +113,29 @@
subsubsection "Lifting"
-datatype 'a up = Bot | Up 'a
-
-instantiation up :: (SL_top)SL_top
+instantiation option :: (SL_top)SL_top
begin
-fun le_up where
-"Up x \<sqsubseteq> Up y = (x \<sqsubseteq> y)" |
-"Bot \<sqsubseteq> y = True" |
-"Up _ \<sqsubseteq> Bot = False"
+fun le_option where
+"Some x \<sqsubseteq> Some y = (x \<sqsubseteq> y)" |
+"None \<sqsubseteq> y = True" |
+"Some _ \<sqsubseteq> None = False"
-lemma [simp]: "(x \<sqsubseteq> Bot) = (x = Bot)"
+lemma [simp]: "(x \<sqsubseteq> None) = (x = None)"
by (cases x) simp_all
-lemma [simp]: "(Up x \<sqsubseteq> u) = (\<exists>y. u = Up y & x \<sqsubseteq> y)"
+lemma [simp]: "(Some x \<sqsubseteq> u) = (\<exists>y. u = Some y & x \<sqsubseteq> y)"
by (cases u) auto
-fun join_up where
-"Up x \<squnion> Up y = Up(x \<squnion> y)" |
-"Bot \<squnion> y = y" |
-"x \<squnion> Bot = x"
+fun join_option where
+"Some x \<squnion> Some y = Some(x \<squnion> y)" |
+"None \<squnion> y = y" |
+"x \<squnion> None = x"
-lemma [simp]: "x \<squnion> Bot = x"
+lemma [simp]: "x \<squnion> None = x"
by (cases x) simp_all
-definition "\<top> = Up \<top>"
+definition "\<top> = Some \<top>"
instance proof
case goal1 show ?case by(cases x, simp_all)
@@ -197,13 +149,13 @@
next
case goal5 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
next
- case goal6 thus ?case by(cases x, simp_all add: Top_up_def)
+ case goal6 thus ?case by(cases x, simp_all add: Top_option_def)
qed
end
-definition bot_acom :: "com \<Rightarrow> ('a::SL_top)up acom" ("\<bottom>\<^sub>c") where
-"\<bottom>\<^sub>c = anno Bot"
+definition bot_acom :: "com \<Rightarrow> ('a::SL_top)option acom" ("\<bottom>\<^sub>c") where
+"\<bottom>\<^sub>c = anno None"
lemma strip_bot_acom[simp]: "strip(\<bottom>\<^sub>c c) = c"
by(simp add: bot_acom_def)
@@ -246,7 +198,7 @@
qed
definition
- lpfp\<^isub>c :: "(('a::SL_top)up acom \<Rightarrow> 'a up acom) \<Rightarrow> com \<Rightarrow> 'a up acom option" where
+ lpfp\<^isub>c :: "(('a::SL_top)option acom \<Rightarrow> 'a option acom) \<Rightarrow> com \<Rightarrow> 'a option acom option" where
"lpfp\<^isub>c f c = pfp f (\<bottom>\<^sub>c c)"
lemma lpfpc_pfp: "lpfp\<^isub>c f c0 = Some c \<Longrightarrow> f c \<sqsubseteq> c"
@@ -275,30 +227,21 @@
definition rep_fun :: "('a \<Rightarrow> 'b set) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b)set" where
"rep_fun rep F = {f. \<forall>x. f x \<in> rep(F x)}"
-fun rep_up :: "('a \<Rightarrow> 'b set) \<Rightarrow> 'a up \<Rightarrow> 'b set" where
-"rep_up rep Bot = {}" |
-"rep_up rep (Up a) = rep a"
+fun rep_option :: "('a \<Rightarrow> 'b set) \<Rightarrow> 'a option \<Rightarrow> 'b set" where
+"rep_option rep None = {}" |
+"rep_option rep (Some a) = rep a"
text{* The interface for abstract values: *}
locale Val_abs =
-fixes rep :: "'a::SL_top \<Rightarrow> val set"
- assumes le_rep: "a \<sqsubseteq> b \<Longrightarrow> rep a \<subseteq> rep b"
- and rep_Top: "rep \<top> = UNIV"
+fixes rep :: "'a::SL_top \<Rightarrow> val set" ("\<gamma>")
+ assumes mono_rep: "a \<sqsubseteq> b \<Longrightarrow> \<gamma> a \<subseteq> \<gamma> b"
+ and rep_Top[simp]: "\<gamma> \<top> = UNIV"
fixes num' :: "val \<Rightarrow> 'a"
and plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
- assumes rep_num': "n : rep(num' n)"
+ assumes rep_num': "n : \<gamma>(num' n)"
and rep_plus':
- "n1 : rep a1 \<Longrightarrow> n2 : rep a2 \<Longrightarrow> n1+n2 : rep(plus' a1 a2)"
-begin
-
-abbreviation in_rep (infix "<:" 50)
- where "x <: a == x : rep a"
-
-lemma in_rep_Top[simp]: "x <: \<top>"
-by(simp add: rep_Top)
-
-end
+ "n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1+n2 : \<gamma>(plus' a1 a2)"
type_synonym 'a st = "(vname \<Rightarrow> 'a)"
@@ -310,18 +253,18 @@
"aval' (V x) S = 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"
+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(S(x := aval' e S))}" |
+ x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(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}) =
IF b THEN step S c1 ELSE step S c2 {post c1 \<squnion> post c2}" |
"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>)"
@@ -329,76 +272,102 @@
by(induct c arbitrary: S) (simp_all add: Let_def)
-text{*Lifting @{text "<:"} to other types: *}
-
-abbreviation fun_in_rep :: "state \<Rightarrow> 'a st \<Rightarrow> bool" (infix "<:f" 50) where
-"s <:f S == s \<in> rep_fun rep S"
-
-notation fun_in_rep (infix "<:\<^sub>f" 50)
-
-lemma fun_in_rep_le: "s <:f S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:f T"
-by(auto simp add: rep_fun_def le_fun_def dest: le_rep)
+abbreviation rep_f :: "'a st \<Rightarrow> state set" ("\<gamma>\<^isub>f")
+where "\<gamma>\<^isub>f == rep_fun \<gamma>"
-abbreviation up_in_rep :: "state \<Rightarrow> 'a st up \<Rightarrow> bool" (infix "<:up" 50) where
-"s <:up S == s : rep_up (rep_fun rep) S"
-
-notation (output) up_in_rep (infix "<:\<^sub>u\<^sub>p" 50)
+abbreviation rep_u :: "'a st option \<Rightarrow> state set" ("\<gamma>\<^isub>u")
+where "\<gamma>\<^isub>u == rep_option \<gamma>\<^isub>f"
-lemma up_fun_in_rep_le: "s <:up S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:up T"
-by (cases S) (auto intro:fun_in_rep_le)
+abbreviation rep_c :: "'a st option acom \<Rightarrow> state set acom" ("\<gamma>\<^isub>c")
+where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>u"
-lemma in_rep_Top_fun: "s <:f Top"
+lemma rep_f_Top[simp]: "\<gamma>\<^isub>f Top = UNIV"
by(simp add: Top_fun_def rep_fun_def)
-lemma in_rep_Top_up: "s <:up Top"
-by(simp add: Top_up_def in_rep_Top_fun)
+lemma rep_u_Top[simp]: "\<gamma>\<^isub>u Top = UNIV"
+by (simp add: Top_option_def)
+
+(* FIXME (maybe also le \<rightarrow> sqle?) *)
+lemma mono_rep_f: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>f f \<subseteq> \<gamma>\<^isub>f g"
+by(auto simp: le_fun_def rep_fun_def dest: mono_rep)
+
+lemma mono_rep_u:
+ "sa \<sqsubseteq> sa' \<Longrightarrow> \<gamma>\<^isub>u sa \<subseteq> \<gamma>\<^isub>u sa'"
+by(induction sa sa' rule: le_option.induct)(simp_all add: mono_rep_f)
+
+lemma mono_rep_c: "ca \<sqsubseteq> ca' \<Longrightarrow> \<gamma>\<^isub>c ca \<le> \<gamma>\<^isub>c ca'"
+by (induction ca ca' rule: le_acom.induct) (simp_all add:mono_rep_u)
text{* Soundness: *}
-lemma aval'_sound: "s <:f S \<Longrightarrow> aval a s <: aval' a S"
+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_fun_def)
-lemma in_rep_update: "\<lbrakk> s <:f S; i <: a \<rbrakk> \<Longrightarrow> s(x := i) <:f S(x := a)"
+lemma in_rep_update:
+ "\<lbrakk> s : \<gamma>\<^isub>f S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>f(S(x := a))"
by(simp add: rep_fun_def)
-lemma step_sound:
- "\<lbrakk> step S c \<sqsubseteq> c; (strip c,s) \<Rightarrow> t; s <:up S \<rbrakk>
- \<Longrightarrow> t <:up post c"
-proof(induction c arbitrary: S s t)
+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 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 `S \<subseteq> \<gamma>\<^isub>u sa` 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
@@ -417,7 +386,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
--- a/src/HOL/IMP/Abs_Int1.thy Wed Nov 23 23:31:32 2011 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy Thu Nov 24 19:58:37 2011 +0100
@@ -1,7 +1,7 @@
(* Author: Tobias Nipkow *)
theory Abs_Int1
-imports Abs_Int0_const
+imports Abs_Int0
begin
instantiation prod :: (preord,preord) preord
@@ -37,20 +37,19 @@
end
-
locale Val_abs1_rep =
Val_abs rep num' plus'
- for rep :: "'a::L_top_bot \<Rightarrow> val set" and num' plus' +
+ for rep :: "'a::L_top_bot \<Rightarrow> val set" ("\<gamma>") and num' plus' +
assumes inter_rep_subset_rep_meet:
"rep a1 \<inter> rep a2 \<subseteq> rep(a1 \<sqinter> a2)"
-and rep_Bot: "rep \<bottom> = {}"
+and rep_Bot[simp]: "rep \<bottom> = {}"
begin
-lemma in_rep_meet: "x <: a1 \<Longrightarrow> x <: a2 \<Longrightarrow> x <: a1 \<sqinter> a2"
+lemma in_rep_meet: "x : \<gamma> a1 \<Longrightarrow> x : \<gamma> a2 \<Longrightarrow> x : \<gamma>(a1 \<sqinter> a2)"
by (metis IntI inter_rep_subset_rep_meet set_mp)
-lemma rep_meet[simp]: "rep(a1 \<sqinter> a2) = rep a1 \<inter> rep a2"
-by (metis equalityI inter_rep_subset_rep_meet le_inf_iff le_rep meet_le1 meet_le2)
+lemma rep_meet[simp]: "\<gamma>(a1 \<sqinter> a2) = \<gamma> a1 \<inter> \<gamma> a2"
+by (metis equalityI inter_rep_subset_rep_meet le_inf_iff mono_rep meet_le1 meet_le2)
end
@@ -59,76 +58,74 @@
fixes filter_plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
and filter_less' :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
assumes filter_plus': "filter_plus' a a1 a2 = (a1',a2') \<Longrightarrow>
- n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: a \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
+ n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1+n2 : \<gamma> a \<Longrightarrow> n1 : \<gamma> a1' \<and> n2 : \<gamma> a2'"
and filter_less': "filter_less' (n1<n2) a1 a2 = (a1',a2') \<Longrightarrow>
- n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
+ n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1 : \<gamma> a1' \<and> n2 : \<gamma> a2'"
locale Abs_Int1 = Val_abs1
begin
-lemma in_rep_join_UpI: "s <:up S1 | s <:up S2 \<Longrightarrow> s <:up S1 \<squnion> S2"
-by (metis join_ge1 join_ge2 up_fun_in_rep_le)
+lemma in_rep_join_UpI: "s : \<gamma>\<^isub>u S1 | s : \<gamma>\<^isub>u S2 \<Longrightarrow> s : \<gamma>\<^isub>u(S1 \<squnion> S2)"
+by (metis (no_types) join_ge1 join_ge2 mono_rep_u set_rev_mp)
-fun aval' :: "aexp \<Rightarrow> 'a st up \<Rightarrow> 'a" where
-"aval' _ Bot = \<bottom>" |
-"aval' (N n) _ = num' n" |
-"aval' (V x) (Up S) = lookup S x" |
-"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
+fun aval'' :: "aexp \<Rightarrow> 'a st option \<Rightarrow> 'a" where
+"aval'' e None = \<bottom>" |
+"aval'' e (Some sa) = aval' e sa"
-lemma aval'_sound: "s <:up S \<Longrightarrow> aval a s <: aval' a S"
-by(induct a)(auto simp: rep_num' rep_plus' in_rep_up_iff lookup_def rep_st_def)
+lemma aval''_sound: "s : \<gamma>\<^isub>u S \<Longrightarrow> aval a s : \<gamma>(aval'' a S)"
+by(cases S)(simp add: aval'_sound)+
subsubsection "Backward analysis"
-fun afilter :: "aexp \<Rightarrow> 'a \<Rightarrow> 'a st up \<Rightarrow> 'a st up" where
-"afilter (N n) a S = (if n <: a then S else Bot)" |
-"afilter (V x) a S = (case S of Bot \<Rightarrow> Bot | Up S \<Rightarrow>
+fun afilter :: "aexp \<Rightarrow> 'a \<Rightarrow> 'a st option \<Rightarrow> 'a st option" where
+"afilter (N n) a S = (if n : \<gamma> a then S else None)" |
+"afilter (V x) a S = (case S of None \<Rightarrow> None | Some S \<Rightarrow>
let a' = lookup S x \<sqinter> a in
- if a' \<sqsubseteq> \<bottom> then Bot else Up(update S x a'))" |
+ if a' \<sqsubseteq> \<bottom> then None else Some(update S x a'))" |
"afilter (Plus e1 e2) a S =
- (let (a1,a2) = filter_plus' a (aval' e1 S) (aval' e2 S)
+ (let (a1,a2) = filter_plus' a (aval'' e1 S) (aval'' e2 S)
in afilter e1 a1 (afilter e2 a2 S))"
-text{* The test for @{const Bot} in the @{const V}-case is important: @{const
-Bot} indicates that a variable has no possible values, i.e.\ that the current
+text{* The test for @{const bot} in the @{const V}-case is important: @{const
+bot} indicates that a variable has no possible values, i.e.\ that the current
program point is unreachable. But then the abstract state should collapse to
-@{const bot}. Put differently, we maintain the invariant that in an abstract
-state all variables are mapped to non-@{const Bot} values. Otherwise the
-(pointwise) join of two abstract states, one of which contains @{const Bot}
-values, may produce too large a result, thus making the analysis less
-precise. *}
+@{const None}. Put differently, we maintain the invariant that in an abstract
+state of the form @{term"Some s"}, all variables are mapped to non-@{const
+bot} values. Otherwise the (pointwise) join of two abstract states, one of
+which contains @{const bot} values, may produce too large a result, thus
+making the analysis less precise. *}
-fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'a st up \<Rightarrow> 'a st up" where
-"bfilter (Bc v) res S = (if v=res then S else Bot)" |
+fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'a st option \<Rightarrow> 'a st option" where
+"bfilter (Bc v) res S = (if v=res then S else None)" |
"bfilter (Not b) res S = bfilter b (\<not> res) S" |
"bfilter (And b1 b2) res S =
(if res then bfilter b1 True (bfilter b2 True S)
else bfilter b1 False S \<squnion> bfilter b2 False S)" |
"bfilter (Less e1 e2) res S =
- (let (res1,res2) = filter_less' res (aval' e1 S) (aval' e2 S)
+ (let (res1,res2) = filter_less' res (aval'' e1 S) (aval'' e2 S)
in afilter e1 res1 (afilter e2 res2 S))"
-lemma afilter_sound: "s <:up S \<Longrightarrow> aval e s <: a \<Longrightarrow> s <:up afilter e a S"
+lemma afilter_sound: "s : \<gamma>\<^isub>u S \<Longrightarrow> aval e s : \<gamma> a \<Longrightarrow> s : \<gamma>\<^isub>u (afilter e a S)"
proof(induction e arbitrary: a S)
case N thus ?case by simp
next
case (V x)
- obtain S' where "S = Up S'" and "s <:f S'" using `s <:up S`
+ obtain S' where "S = Some S'" and "s : \<gamma>\<^isub>f S'" using `s : \<gamma>\<^isub>u S`
by(auto simp: in_rep_up_iff)
- moreover hence "s x <: lookup S' x" by(simp add: rep_st_def)
- moreover have "s x <: a" using V by simp
+ moreover hence "s x : \<gamma> (lookup S' x)" by(simp add: rep_st_def)
+ moreover have "s x : \<gamma> a" using V by simp
ultimately show ?case using V(1)
by(simp add: lookup_update Let_def rep_st_def)
- (metis le_rep emptyE in_rep_meet rep_Bot subset_empty)
+ (metis mono_rep emptyE in_rep_meet rep_Bot subset_empty)
next
case (Plus e1 e2) thus ?case
- using filter_plus'[OF _ aval'_sound[OF Plus(3)] aval'_sound[OF Plus(3)]]
+ using filter_plus'[OF _ aval''_sound[OF Plus(3)] aval''_sound[OF Plus(3)]]
by (auto split: prod.split)
qed
-lemma bfilter_sound: "s <:up S \<Longrightarrow> bv = bval b s \<Longrightarrow> s <:up bfilter b bv S"
+lemma bfilter_sound: "s : \<gamma>\<^isub>u S \<Longrightarrow> bv = bval b s \<Longrightarrow> s : \<gamma>\<^isub>u(bfilter b bv S)"
proof(induction b arbitrary: S bv)
case Bc thus ?case by simp
next
@@ -138,16 +135,15 @@
next
case (Less e1 e2) thus ?case
by (auto split: prod.split)
- (metis afilter_sound filter_less' aval'_sound Less)
+ (metis afilter_sound filter_less' aval''_sound Less)
qed
-fun step :: "'a st up \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom"
+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 (Up 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 (bfilter b True S) c1; c2' = step (bfilter b False S) c2
@@ -157,7 +153,7 @@
WHILE b DO step (bfilter b True Inv) c
{bfilter b False 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>)"
lemma strip_step[simp]: "strip(step S c) = strip c"
@@ -166,68 +162,73 @@
subsubsection "Soundness"
-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 While_final_False: "(WHILE b DO c, s) \<Rightarrow> t \<Longrightarrow> \<not> bval b t"
-by(induct "WHILE b DO c" s t rule: big_step_induct) simp_all
-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)
+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 split: up.splits)
- by (metis aval'_sound fun_in_rep_le in_rep_update rep_up.simps(2))
+ by (fastforce simp: strip_eq_Assign intro: aval'_sound in_rep_update
+ split: option.splits del:subsetD)
next
- case Semi thus ?case by simp blast
+ case Semi thus ?case apply (auto simp: strip_eq_Semi)
+ by (metis le_post post_map_acom)
next
- case (If b c1 c2 S0)
- show ?case
- proof cases
- assume "bval b s"
- with If.prems have 1: "step (bfilter b True S) c1 \<sqsubseteq> c1"
- and 2: "(strip c1, s) \<Rightarrow> t" and 3: "post c1 \<sqsubseteq> S0" by(auto simp: Let_def)
- from If.IH(1)[OF 1 2 bfilter_sound[OF `s <:up S`]] `bval b s` 3
- show ?thesis by simp (metis up_fun_in_rep_le)
- next
- assume "\<not> bval b s"
- with If.prems have 1: "step (bfilter b False S) c2 \<sqsubseteq> c2"
- and 2: "(strip c2, s) \<Rightarrow> t" and 3: "post c2 \<sqsubseteq> S0" by(auto simp: Let_def)
- from If.IH(2)[OF 1 2 bfilter_sound[OF `s <:up S`]] `\<not> bval b s` 3
- show ?thesis by simp (metis up_fun_in_rep_le)
- qed
+ 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 `S \<subseteq> \<gamma>\<^isub>u sa`
+ by (simp add: If.IH subset_iff bfilter_sound)
next
- case (While Inv b c P)
- from While.prems have inv: "step (bfilter b True Inv) c \<sqsubseteq> c"
- and "post c \<sqsubseteq> Inv" and "S \<sqsubseteq> Inv" and "bfilter b False 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` bfilter_sound[OF `s1 <:up Inv`]] `post c \<sqsubseteq> Inv`]] `bval b s1`
- show ?case by simp
- qed
- } note Inv = this
- from While.prems(2) have "(WHILE b DO strip c, s) \<Rightarrow> t" and "\<not> bval b t"
- by(auto dest: While_final_False)
- from Inv[OF this(1) up_fun_in_rep_le[OF `s <:up S` `S \<sqsubseteq> Inv`]]
- have "t <:up Inv" .
- from up_fun_in_rep_le[OF bfilter_sound[OF this] `bfilter b False Inv \<sqsubseteq> P`]
- show ?case using `\<not> bval b t` by simp
+ 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 bfilter_sound)
qed
-lemma AI_sound: "\<lbrakk> AI c = Some c'; (c,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> t <:up post c'"
-unfolding AI_def
-by (metis in_rep_Top_up lpfpc_pfp step_sound strip_lpfpc strip_step)
-(*
-by(metis step_sound[of "\<top>" c' s t] strip_lpfp strip_step
- lpfp_pfp mono_def mono_step[OF le_refl] in_rep_Top_up)
-*)
+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
@@ -242,39 +243,44 @@
begin
lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'"
+by(induction e) (auto simp: le_st_def lookup_def mono_plus')
+
+lemma mono_aval'': "S \<sqsubseteq> S' \<Longrightarrow> aval'' e S \<sqsubseteq> aval'' e S'"
apply(cases S)
apply simp
apply(cases S')
apply simp
-apply simp
-by(induction e) (auto simp: le_st_def lookup_def mono_plus')
+by (simp add: mono_aval')
lemma mono_afilter: "r \<sqsubseteq> r' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> afilter e r S \<sqsubseteq> afilter e r' S'"
apply(induction e arbitrary: r r' S S')
-apply(auto simp: Let_def split: up.splits prod.splits)
-apply (metis le_rep subsetD)
+apply(auto simp: Let_def split: option.splits prod.splits)
+apply (metis mono_rep subsetD)
apply(drule_tac x = "list" in mono_lookup)
apply (metis mono_meet le_trans)
-apply (metis mono_meet mono_lookup mono_update le_trans)
-apply(metis mono_aval' mono_filter_plus'[simplified le_prod_def] fst_conv snd_conv)
+apply (metis mono_meet mono_lookup mono_update)
+apply(metis mono_aval'' mono_filter_plus'[simplified le_prod_def] fst_conv snd_conv)
done
lemma mono_bfilter: "S \<sqsubseteq> S' \<Longrightarrow> bfilter b r S \<sqsubseteq> bfilter b r S'"
apply(induction b arbitrary: r S S')
apply(auto simp: le_trans[OF _ join_ge1] le_trans[OF _ join_ge2] split: prod.splits)
-apply(metis mono_aval' mono_afilter mono_filter_less'[simplified le_prod_def] fst_conv snd_conv)
+apply(metis mono_aval'' mono_afilter mono_filter_less'[simplified le_prod_def] fst_conv snd_conv)
done
lemma post_le_post: "c \<sqsubseteq> c' \<Longrightarrow> post c \<sqsubseteq> post c'"
by (induction c c' rule: le_acom.induct) simp_all
-lemma mono_step: "S \<sqsubseteq> S' \<Longrightarrow> c \<sqsubseteq> c' \<Longrightarrow> step S c \<sqsubseteq> step S' c'"
+lemma mono_step_aux: "S \<sqsubseteq> S' \<Longrightarrow> c \<sqsubseteq> c' \<Longrightarrow> step S c \<sqsubseteq> step S' c'"
apply(induction c c' arbitrary: S S' rule: le_acom.induct)
apply (auto simp: post_le_post Let_def mono_bfilter mono_update mono_aval' le_join_disj
- split: up.split)
+ split: option.split)
done
+lemma mono_step: "mono (step S)"
+by(simp add: mono_def mono_step_aux[OF le_refl])
+
end
end
--- a/src/HOL/IMP/Abs_Int1_ivl.thy Wed Nov 23 23:31:32 2011 +0100
+++ b/src/HOL/IMP/Abs_Int1_ivl.thy Thu Nov 24 19:58:37 2011 +0100
@@ -1,7 +1,7 @@
(* Author: Tobias Nipkow *)
theory Abs_Int1_ivl
-imports Abs_Int1
+imports Abs_Int1 Abs_Int_Tests
begin
subsection "Interval Analysis"
@@ -117,10 +117,10 @@
instance
proof
case goal1 thus ?case
- by (simp add:meet_ivl_def empty_def meet_ivl_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)
+ by (simp add:meet_ivl_def empty_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)
next
case goal2 thus ?case
- by (simp add:meet_ivl_def empty_def meet_ivl_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)
+ by (simp add: empty_def meet_ivl_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)
next
case goal3 thus ?case
by (cases x, cases y, cases z, auto simp add: le_ivl_def meet_ivl_def empty_def le_option_def max_option_def min_option_def split: option.splits if_splits)
@@ -161,6 +161,7 @@
else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
interpretation Val_abs rep_ivl num_ivl plus_ivl
+defines aval_ivl is aval'
proof
case goal1 thus ?case
by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
@@ -208,72 +209,9 @@
and bfilter_ivl is bfilter
and step_ivl is step
and AI_ivl is AI
-and aval_ivl is aval'
+and aval_ivl' is aval''
proof qed
-definition "test1_ivl =
- ''y'' ::= N 7;
- IF Less (V ''x'') (V ''y'')
- THEN ''y'' ::= Plus (V ''y'') (V ''x'')
- ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
-
-value [code] "show_acom_opt (AI_ivl test1_ivl)"
-
-value [code] "show_acom_opt (AI_const test3_const)"
-value [code] "show_acom_opt (AI_ivl test3_const)"
-
-value [code] "show_acom_opt (AI_const test4_const)"
-value [code] "show_acom_opt (AI_ivl test4_const)"
-
-value [code] "show_acom_opt (AI_ivl test6_const)"
-
-definition "test2_ivl =
- WHILE Less (V ''x'') (N 100)
- DO ''x'' ::= Plus (V ''x'') (N 1)"
-
-value [code] "show_acom_opt (AI_ivl test2_ivl)"
-value [code] "show_acom (((step_ivl \<top>)^^0) (\<bottom>\<^sub>c test2_ivl))"
-value [code] "show_acom (((step_ivl \<top>)^^1) (\<bottom>\<^sub>c test2_ivl))"
-value [code] "show_acom (((step_ivl \<top>)^^2) (\<bottom>\<^sub>c test2_ivl))"
-
-text{* Fixed point reached in 2 steps. Not so if the start value of x is known: *}
-
-definition "test3_ivl =
- ''x'' ::= N 7;
- WHILE Less (V ''x'') (N 100)
- DO ''x'' ::= Plus (V ''x'') (N 1)"
-
-value [code] "show_acom_opt (AI_ivl test3_ivl)"
-value [code] "show_acom (((step_ivl \<top>)^^0) (\<bottom>\<^sub>c test3_ivl))"
-value [code] "show_acom (((step_ivl \<top>)^^1) (\<bottom>\<^sub>c test3_ivl))"
-value [code] "show_acom (((step_ivl \<top>)^^2) (\<bottom>\<^sub>c test3_ivl))"
-value [code] "show_acom (((step_ivl \<top>)^^3) (\<bottom>\<^sub>c test3_ivl))"
-value [code] "show_acom (((step_ivl \<top>)^^4) (\<bottom>\<^sub>c test3_ivl))"
-
-text{* Takes as many iterations as the actual execution. Would diverge if
-loop did not terminate. Worse still, as the following example shows: even if
-the actual execution terminates, the analysis may not: *}
-
-definition "test4_ivl =
- ''x'' ::= N 0; ''y'' ::= N 100; ''z'' ::= Plus (V ''x'') (V ''y'');
- WHILE Less (V ''x'') (N 11)
- DO (''x'' ::= Plus (V ''x'') (N 1); ''y'' ::= Plus (V ''y'') (N -1))"
-
-text{* The value of y keeps decreasing as the analysis is iterated, no matter
-how long: *}
-
-value [code] "show_acom (((step_ivl \<top>)^^50) (\<bottom>\<^sub>c test4_ivl))"
-
-definition "test5_ivl =
- ''x'' ::= N 0; ''y'' ::= N 0;
- WHILE Less (V ''x'') (N 1000)
- DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"
-value [code] "show_acom_opt (AI_ivl test5_ivl)"
-
-text{* Again, the analysis would not terminate: *}
-definition "test6_ivl =
- ''x'' ::= N 0;
- WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
text{* Monotonicity: *}
@@ -291,4 +229,41 @@
by(auto simp add: empty_def le_ivl_def le_option_def min_option_def max_option_def split: option.splits)
qed
+
+subsubsection "Tests"
+
+value [code] "show_acom_opt (AI_ivl test1_ivl)"
+
+text{* Better than @{text AI_const}: *}
+value [code] "show_acom_opt (AI_ivl test3_const)"
+value [code] "show_acom_opt (AI_ivl test4_const)"
+value [code] "show_acom_opt (AI_ivl test6_const)"
+
+value [code] "show_acom_opt (AI_ivl test2_ivl)"
+value [code] "show_acom (((step_ivl \<top>)^^0) (\<bottom>\<^sub>c test2_ivl))"
+value [code] "show_acom (((step_ivl \<top>)^^1) (\<bottom>\<^sub>c test2_ivl))"
+value [code] "show_acom (((step_ivl \<top>)^^2) (\<bottom>\<^sub>c test2_ivl))"
+
+text{* Fixed point reached in 2 steps. Not so if the start value of x is known: *}
+
+value [code] "show_acom_opt (AI_ivl test3_ivl)"
+value [code] "show_acom (((step_ivl \<top>)^^0) (\<bottom>\<^sub>c test3_ivl))"
+value [code] "show_acom (((step_ivl \<top>)^^1) (\<bottom>\<^sub>c test3_ivl))"
+value [code] "show_acom (((step_ivl \<top>)^^2) (\<bottom>\<^sub>c test3_ivl))"
+value [code] "show_acom (((step_ivl \<top>)^^3) (\<bottom>\<^sub>c test3_ivl))"
+value [code] "show_acom (((step_ivl \<top>)^^4) (\<bottom>\<^sub>c test3_ivl))"
+
+text{* Takes as many iterations as the actual execution. Would diverge if
+loop did not terminate. Worse still, as the following example shows: even if
+the actual execution terminates, the analysis may not. The value of y keeps
+decreasing as the analysis is iterated, no matter how long: *}
+
+value [code] "show_acom (((step_ivl \<top>)^^50) (\<bottom>\<^sub>c test4_ivl))"
+
+text{* Relationships between variables are NOT captured: *}
+value [code] "show_acom_opt (AI_ivl test5_ivl)"
+
+text{* Again, the analysis would not terminate: *}
+value [code] "show_acom (((step_ivl \<top>)^^50) (\<bottom>\<^sub>c test6_ivl))"
+
end
--- a/src/HOL/IMP/Abs_Int2.thy Wed Nov 23 23:31:32 2011 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy Thu Nov 24 19:58:37 2011 +0100
@@ -64,32 +64,32 @@
end
-instantiation up :: (WN)WN
+instantiation option :: (WN)WN
begin
-fun widen_up where
-"widen_up Bot x = x" |
-"widen_up x Bot = x" |
-"widen_up (Up x) (Up y) = Up(x \<nabla> y)"
+fun widen_option where
+"None \<nabla> x = x" |
+"x \<nabla> None = x" |
+"(Some x) \<nabla> (Some y) = Some(x \<nabla> y)"
-fun narrow_up where
-"narrow_up Bot x = Bot" |
-"narrow_up x Bot = Bot" |
-"narrow_up (Up x) (Up y) = Up(x \<triangle> y)"
+fun narrow_option where
+"None \<triangle> x = None" |
+"x \<triangle> None = None" |
+"(Some x) \<triangle> (Some y) = Some(x \<triangle> y)"
instance
proof
case goal1 show ?case
- by(induct x y rule: widen_up.induct) (simp_all add: widen1)
+ by(induct x y rule: widen_option.induct) (simp_all add: widen1)
next
case goal2 show ?case
- by(induct x y rule: widen_up.induct) (simp_all add: widen2)
+ by(induct x y rule: widen_option.induct) (simp_all add: widen2)
next
case goal3 thus ?case
- by(induct x y rule: narrow_up.induct) (simp_all add: narrow1)
+ by(induct x y rule: narrow_option.induct) (simp_all add: narrow1)
next
case goal4 thus ?case
- by(induct x y rule: narrow_up.induct) (simp_all add: narrow2)
+ by(induct x y rule: narrow_option.induct) (simp_all add: narrow2)
qed
end
@@ -129,7 +129,7 @@
"prefp f = while_option (\<lambda>x. \<not> x \<sqsubseteq> f x) f"
definition
- pfp_WN :: "(('a::WN)up acom \<Rightarrow> 'a up acom) \<Rightarrow> com \<Rightarrow> 'a up acom option"
+ pfp_WN :: "(('a::WN)option acom \<Rightarrow> 'a option acom) \<Rightarrow> com \<Rightarrow> 'a option acom option"
where "pfp_WN f c = (case lpfp\<^isub>c (\<lambda>c. c \<nabla>\<^sub>c f c) c of None \<Rightarrow> None
| Some c' \<Rightarrow> prefp (\<lambda>c. c \<triangle>\<^sub>c f c) c')"
@@ -183,13 +183,26 @@
locale Abs_Int2 = Abs_Int1_mono rep for rep :: "'a::{WN,L_top_bot} \<Rightarrow> val set"
begin
-definition AI_WN :: "com \<Rightarrow> 'a st up acom option" where
+definition AI_WN :: "com \<Rightarrow> 'a st option acom option" where
"AI_WN = pfp_WN (step \<top>)"
-lemma AI_sound: "\<lbrakk> AI_WN c = Some c'; (c,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> t <:up post c'"
-unfolding AI_WN_def
-by(metis step_sound[of "\<top>" c' s t] strip_pfp_WN strip_step
- pfp_WN_pfp mono_def mono_step[OF le_refl] in_rep_Top_up)
+lemma AI_WN_sound: "AI_WN c = Some c' \<Longrightarrow> CS UNIV c \<le> \<gamma>\<^isub>c c'"
+proof(simp add: CS_def AI_WN_def)
+ assume 1: "pfp_WN (step \<top>) c = Some c'"
+ from pfp_WN_pfp[OF allI[OF strip_step] mono_step 1]
+ have 2: "step \<top> c' \<sqsubseteq> c'" .
+ have 3: "strip (\<gamma>\<^isub>c (step \<top> c')) = c" by(simp add: strip_pfp_WN[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
@@ -198,12 +211,16 @@
defines AI_ivl' is AI_WN
proof qed
-value [code] "show_acom_opt (AI_ivl test3_ivl)"
-value [code] "show_acom_opt (AI_ivl' test3_ivl)"
+
+subsubsection "Tests"
definition "step_up_ivl n = ((\<lambda>c. c \<nabla>\<^sub>c step_ivl \<top> c)^^n)"
definition "step_down_ivl n = ((\<lambda>c. c \<triangle>\<^sub>c step_ivl \<top> c)^^n)"
+text{* For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as
+the loop took to execute. In contrast, @{const AI_ivl} converges in a
+constant number of steps: *}
+
value [code] "show_acom (step_up_ivl 1 (\<bottom>\<^sub>c test3_ivl))"
value [code] "show_acom (step_up_ivl 2 (\<bottom>\<^sub>c test3_ivl))"
value [code] "show_acom (step_up_ivl 3 (\<bottom>\<^sub>c test3_ivl))"
@@ -213,6 +230,8 @@
value [code] "show_acom (step_down_ivl 2 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))"
value [code] "show_acom (step_down_ivl 3 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))"
+text{* Now all the analyses terminate: *}
+
value [code] "show_acom_opt (AI_ivl' test4_ivl)"
value [code] "show_acom_opt (AI_ivl' test5_ivl)"
value [code] "show_acom_opt (AI_ivl' test6_ivl)"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int_Tests.thy Thu Nov 24 19:58:37 2011 +0100
@@ -0,0 +1,68 @@
+theory Abs_Int_Tests
+imports ACom
+begin
+
+subsection "Test Programs"
+
+text{* For constant propagation: *}
+
+text{* Straight line code: *}
+definition "test1_const =
+ ''y'' ::= N 7;
+ ''z'' ::= Plus (V ''y'') (N 2);
+ ''y'' ::= Plus (V ''x'') (N 0)"
+
+text{* Conditional: *}
+definition "test2_const =
+ IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 5"
+
+text{* Conditional, test is relevant: *}
+definition "test3_const =
+ ''x'' ::= N 42;
+ IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6"
+
+text{* While: *}
+definition "test4_const =
+ ''x'' ::= N 0; WHILE Bc True DO ''x'' ::= N 0"
+
+text{* While, test is relevant: *}
+definition "test5_const =
+ ''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
+
+text{* Iteration is needed: *}
+definition "test6_const =
+ ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 2;
+ WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y''; ''y'' ::= V ''z'')"
+
+text{* For intervals: *}
+
+definition "test1_ivl =
+ ''y'' ::= N 7;
+ IF Less (V ''x'') (V ''y'')
+ THEN ''y'' ::= Plus (V ''y'') (V ''x'')
+ ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
+
+definition "test2_ivl =
+ WHILE Less (V ''x'') (N 100)
+ DO ''x'' ::= Plus (V ''x'') (N 1)"
+
+definition "test3_ivl =
+ ''x'' ::= N 7;
+ WHILE Less (V ''x'') (N 100)
+ DO ''x'' ::= Plus (V ''x'') (N 1)"
+
+definition "test4_ivl =
+ ''x'' ::= N 0; ''y'' ::= N 100; ''z'' ::= Plus (V ''x'') (V ''y'');
+ WHILE Less (V ''x'') (N 11)
+ DO (''x'' ::= Plus (V ''x'') (N 1); ''y'' ::= Plus (V ''y'') (N -1))"
+
+definition "test5_ivl =
+ ''x'' ::= N 0; ''y'' ::= N 0;
+ WHILE Less (V ''x'') (N 1000)
+ DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"
+
+definition "test6_ivl =
+ ''x'' ::= N 0;
+ WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
+
+end
--- a/src/HOL/IMP/Abs_State.thy Wed Nov 23 23:31:32 2011 +0100
+++ b/src/HOL/IMP/Abs_State.thy Thu Nov 24 19:58:37 2011 +0100
@@ -19,11 +19,7 @@
definition "show_st S = [(x,fun S x). x \<leftarrow> sort(dom S)]"
-fun show_st_up where
-"show_st_up Bot = Bot" |
-"show_st_up (Up S) = Up(show_st S)"
-
-definition "show_acom = map_acom show_st_up"
+definition "show_acom = map_acom (Option.map show_st)"
definition "show_acom_opt = Option.map show_acom"
definition "lookup F x = (if x : set(dom F) then fun F x else \<top>)"
@@ -65,32 +61,37 @@
context Val_abs
begin
-abbreviation fun_in_rep :: "state \<Rightarrow> 'a st \<Rightarrow> bool" (infix "<:f" 50) where
-"s <:f S == s \<in> rep_st rep S"
+abbreviation rep_f :: "'a st \<Rightarrow> state set" ("\<gamma>\<^isub>f")
+where "\<gamma>\<^isub>f == rep_st rep"
-notation fun_in_rep (infix "<:\<^sub>f" 50)
+abbreviation rep_u :: "'a st option \<Rightarrow> state set" ("\<gamma>\<^isub>u")
+where "\<gamma>\<^isub>u == rep_option \<gamma>\<^isub>f"
-lemma fun_in_rep_le: "s <:f S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:f T"
-apply(auto simp add: rep_st_def le_st_def dest: le_rep)
-by (metis in_rep_Top le_rep lookup_def subsetD)
+abbreviation rep_c :: "'a st option acom \<Rightarrow> state set acom" ("\<gamma>\<^isub>c")
+where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>u"
-abbreviation in_rep_up :: "state \<Rightarrow> 'a st up \<Rightarrow> bool" (infix "<:up" 50)
-where "s <:up S == s : rep_up (rep_st rep) S"
+lemma rep_f_Top[simp]: "rep_f Top = UNIV"
+by(auto simp: Top_st_def rep_st_def lookup_def)
+
+lemma rep_u_Top[simp]: "rep_u Top = UNIV"
+by (simp add: Top_option_def)
-notation (output) in_rep_up (infix "<:\<^sub>u\<^sub>p" 50)
+(* FIXME (maybe also le \<rightarrow> sqle?) *)
+
+lemma mono_rep_f: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>f f \<subseteq> \<gamma>\<^isub>f g"
+apply(simp add:rep_st_def subset_iff lookup_def le_st_def split: if_splits)
+by (metis UNIV_I mono_rep rep_Top subsetD)
-lemma up_fun_in_rep_le: "s <:up S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:up T"
-by (cases S) (auto intro:fun_in_rep_le)
+lemma mono_rep_u:
+ "sa \<sqsubseteq> sa' \<Longrightarrow> \<gamma>\<^isub>u sa \<subseteq> \<gamma>\<^isub>u sa'"
+by(induction sa sa' rule: le_option.induct)(simp_all add: mono_rep_f)
-lemma in_rep_up_iff: "x <:up u \<longleftrightarrow> (\<exists>u'. u = Up u' \<and> x <:f u')"
+lemma mono_rep_c: "ca \<sqsubseteq> ca' \<Longrightarrow> \<gamma>\<^isub>c ca \<le> \<gamma>\<^isub>c ca'"
+by (induction ca ca' rule: le_acom.induct) (simp_all add:mono_rep_u)
+
+lemma in_rep_up_iff: "x : rep_option r u \<longleftrightarrow> (\<exists>u'. u = Some u' \<and> x : r u')"
by (cases u) auto
-lemma in_rep_Top_fun: "s <:f \<top>"
-by(simp add: rep_st_def lookup_def Top_st_def)
-
-lemma in_rep_Top_up: "s <:up \<top>"
-by(simp add: Top_up_def in_rep_Top_fun)
-
end
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Collecting.thy Thu Nov 24 19:58:37 2011 +0100
@@ -0,0 +1,180 @@
+theory Collecting
+imports Complete_Lattice_ix ACom
+begin
+
+subsection "Collecting Semantics of Commands"
+
+subsubsection "Annotated commands as a complete lattice"
+
+(* Orderings could also be lifted generically (thus subsuming the
+instantiation for preord and order), but then less_eq_acom would need to
+become a definition, eg less_eq_acom = lift2 less_eq, and then proofs would
+need to unfold this defn first. *)
+
+instantiation acom :: (order) order
+begin
+
+fun less_eq_acom :: "('a::order)acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
+"less_eq_acom (SKIP {S}) (SKIP {S'}) = (S \<le> S')" |
+"less_eq_acom (x ::= e {S}) (x' ::= e' {S'}) = (x=x' \<and> e=e' \<and> S \<le> S')" |
+"less_eq_acom (c1;c2) (c1';c2') = (less_eq_acom c1 c1' \<and> less_eq_acom c2 c2')" |
+"less_eq_acom (IF b THEN c1 ELSE c2 {S}) (IF b' THEN c1' ELSE c2' {S'}) =
+ (b=b' \<and> less_eq_acom c1 c1' \<and> less_eq_acom c2 c2' \<and> S \<le> S')" |
+"less_eq_acom ({Inv} WHILE b DO c {P}) ({Inv'} WHILE b' DO c' {P'}) =
+ (b=b' \<and> less_eq_acom c c' \<and> Inv \<le> Inv' \<and> P \<le> P')" |
+"less_eq_acom _ _ = False"
+
+lemma SKIP_le: "SKIP {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = SKIP {S'} \<and> S \<le> S')"
+by (cases c) auto
+
+lemma Assign_le: "x ::= e {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = x ::= e {S'} \<and> S \<le> S')"
+by (cases c) auto
+
+lemma Semi_le: "c1;c2 \<le> c \<longleftrightarrow> (\<exists>c1' c2'. c = c1';c2' \<and> c1 \<le> c1' \<and> c2 \<le> c2')"
+by (cases c) auto
+
+lemma If_le: "IF b THEN c1 ELSE c2 {S} \<le> c \<longleftrightarrow>
+ (\<exists>c1' c2' S'. c= IF b THEN c1' ELSE c2' {S'} \<and> c1 \<le> c1' \<and> c2 \<le> c2' \<and> S \<le> S')"
+by (cases c) auto
+
+lemma While_le: "{Inv} WHILE b DO c {P} \<le> w \<longleftrightarrow>
+ (\<exists>Inv' c' P'. w = {Inv'} WHILE b DO c' {P'} \<and> c \<le> c' \<and> Inv \<le> Inv' \<and> P \<le> P')"
+by (cases w) auto
+
+definition less_acom :: "'a acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
+"less_acom x y = (x \<le> y \<and> \<not> y \<le> x)"
+
+instance
+proof
+ case goal1 show ?case by(simp add: less_acom_def)
+next
+ case goal2 thus ?case by (induct x) auto
+next
+ case goal3 thus ?case
+ apply(induct x y arbitrary: z rule: less_eq_acom.induct)
+ apply (auto intro: le_trans simp: SKIP_le Assign_le Semi_le If_le While_le)
+ done
+next
+ case goal4 thus ?case
+ apply(induct x y rule: less_eq_acom.induct)
+ apply (auto intro: le_antisym)
+ done
+qed
+
+end
+
+fun lift :: "('a set set \<Rightarrow> 'a set) \<Rightarrow> com \<Rightarrow> 'a set acom set \<Rightarrow> 'a set acom"
+where
+"lift F com.SKIP M = (SKIP {F {P. SKIP {P} : M}})" |
+"lift F (x ::= a) M = (x ::= a {F {P. x::=a {P} : M}})" |
+"lift F (c1;c2) M =
+ (lift F c1 {c1. \<exists>c2. c1;c2 : M}); (lift F c2 {c2. \<exists>c1. c1;c2 : M})" |
+"lift F (IF b THEN c1 ELSE c2) M =
+ IF b THEN lift F c1 {c1. \<exists>c2 P. IF b THEN c1 ELSE c2 {P} : M}
+ ELSE lift F c2 {c2. \<exists>c1 P. IF b THEN c1 ELSE c2 {P} : M}
+ {F {P. \<exists>c1 c2. IF b THEN c1 ELSE c2 {P} : M}}" |
+"lift F (WHILE b DO c) M =
+ {F {I. \<exists>c P. {I} WHILE b DO c {P} : M}}
+ WHILE b DO lift F c {c. \<exists>I P. {I} WHILE b DO c {P} : M}
+ {F {P. \<exists>I c. {I} WHILE b DO c {P} : M}}"
+
+interpretation Complete_Lattice_ix strip "lift Inter"
+proof
+ case goal1
+ have "a:A \<Longrightarrow> lift Inter (strip a) A \<le> a"
+ proof(induction a arbitrary: A)
+ case Semi from Semi.prems show ?case by(fastforce intro!: Semi.IH)
+ next
+ case If from If.prems show ?case by(fastforce intro!: If.IH)
+ next
+ case While from While.prems show ?case by(fastforce intro!: While.IH)
+ qed auto
+ with goal1 show ?case by auto
+next
+ case goal2
+ thus ?case
+ proof(induction b arbitrary: i A)
+ case Semi from Semi.prems show ?case by (fastforce intro!: Semi.IH)
+ next
+ case If from If.prems show ?case by (fastforce intro!: If.IH)
+ next
+ case While from While.prems show ?case by(fastforce intro: While.IH)
+ qed fastforce+
+next
+ case goal3
+ thus ?case
+ proof(induction i arbitrary: A)
+ case Semi from Semi.prems show ?case by (fastforce intro!: Semi.IH)
+ next
+ case If from If.prems show ?case by (fastforce intro!: If.IH)
+ next
+ case While from While.prems show ?case by(fastforce intro: While.IH)
+ qed auto
+qed
+
+lemma le_post: "c \<le> d \<Longrightarrow> post c \<le> post d"
+by(induction c d rule: less_eq_acom.induct) auto
+
+lemma le_strip: "c \<le> d \<Longrightarrow> strip c = strip d"
+by(induction c d rule: less_eq_acom.induct) auto
+
+lemma le_SKIP_iff: "c \<le> SKIP {P'} \<longleftrightarrow> (EX P. c = SKIP {P} \<and> P \<le> P')"
+by (cases c) simp_all
+
+lemma le_Assign_iff: "c \<le> x::=e {P'} \<longleftrightarrow> (EX P. c = x::=e {P} \<and> P \<le> P')"
+by (cases c) simp_all
+
+lemma le_Semi_iff: "c \<le> d1;d2 \<longleftrightarrow> (EX c1 c2. c = c1;c2 \<and> c1 \<le> d1 \<and> c2 \<le> d2)"
+by (cases c) simp_all
+
+lemma le_If_iff: "c \<le> IF b THEN d1 ELSE d2 {P'} \<longleftrightarrow>
+ (EX c1 c2 P. c = IF b THEN c1 ELSE c2 {P} \<and> c1 \<le> d1 \<and> c2 \<le> d2 \<and> P \<le> P')"
+by (cases c) simp_all
+
+lemma le_While_iff: "c \<le> {I'} WHILE b DO d {P'} \<longleftrightarrow>
+ (EX I c' P. c = {I} WHILE b DO c' {P} \<and> I \<le> I' \<and> c' \<le> d \<and> P \<le> P')"
+by (cases c) auto
+
+
+subsubsection "Collecting semantics"
+
+fun step_cs :: "state set \<Rightarrow> state set acom \<Rightarrow> state set acom" where
+"step_cs S (SKIP {P}) = (SKIP {S})" |
+"step_cs S (x ::= e {P}) =
+ (x ::= e {{s'. EX s:S. s' = s(x := aval e s)}})" |
+"step_cs S (c1; c2) = step_cs S c1; step_cs (post c1) c2" |
+"step_cs S (IF b THEN c1 ELSE c2 {P}) =
+ IF b THEN step_cs {s:S. bval b s} c1 ELSE step_cs {s:S. \<not> bval b s} c2
+ {post c1 \<union> post c2}" |
+"step_cs S ({Inv} WHILE b DO c {P}) =
+ {S \<union> post c} WHILE b DO (step_cs {s:Inv. bval b s} c) {{s:Inv. \<not> bval b s}}"
+
+definition CS :: "state set \<Rightarrow> com \<Rightarrow> state set acom" where
+"CS S c = lfp c (step_cs S)"
+
+lemma mono_step_cs_aux: "x \<le> y \<Longrightarrow> S \<subseteq> T \<Longrightarrow> step_cs S x \<le> step_cs T y"
+proof(induction x y arbitrary: S T rule: less_eq_acom.induct)
+ case 2 thus ?case by fastforce
+next
+ case 3 thus ?case by(simp add: le_post)
+next
+ case 4 thus ?case by(simp add: subset_iff)(metis le_post set_mp)+
+next
+ case 5 thus ?case by(simp add: subset_iff) (metis le_post set_mp)
+qed auto
+
+lemma mono_step_cs: "mono (step_cs S)"
+by(blast intro: monoI mono_step_cs_aux)
+
+lemma strip_step_cs: "strip(step_cs S c) = strip c"
+by (induction c arbitrary: S) auto
+
+lemmas lfp_cs_unfold = lfp_unfold[OF strip_step_cs mono_step_cs]
+
+lemma CS_unfold: "CS S c = step_cs S (CS S c)"
+by (metis CS_def lfp_cs_unfold)
+
+lemma strip_CS[simp]: "strip(CS S c) = c"
+by(simp add: CS_def)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Collecting1.thy Thu Nov 24 19:58:37 2011 +0100
@@ -0,0 +1,225 @@
+theory Collecting1
+imports Collecting
+begin
+
+subsection "A small step semantics on annotated commands"
+
+text{* The idea: the state is propagated through the annotated command as an
+annotation @{term "Some s"}, all other annotations are @{const None}. *}
+
+fun join :: "'a option \<Rightarrow> 'a option \<Rightarrow> 'a option" where
+"join None x = x" |
+"join x None = x"
+
+definition bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> state option \<Rightarrow> state option" where
+"bfilter b r so =
+ (case so of None \<Rightarrow> None | Some s \<Rightarrow> if bval b s = r then Some s else None)"
+
+lemma bfilter_None[simp]: "bfilter b r None = None"
+by(simp add: bfilter_def split: option.split)
+
+fun step1 :: "state option \<Rightarrow> state option acom \<Rightarrow> state option acom" where
+"step1 so (SKIP {P}) = SKIP {so}" |
+"step1 so (x::=e {P}) =
+ x ::= e {case so of None \<Rightarrow> None | Some s \<Rightarrow> Some(s(x := aval e s))}" |
+"step1 so (c1;c2) = step1 so c1; step1 (post c1) c2" |
+"step1 so (IF b THEN c1 ELSE c2 {P}) =
+ IF b THEN step1 (bfilter b True so) c1
+ ELSE step1 (bfilter b False so) c2
+ {join (post c1) (post c2)}" |
+"step1 so ({I} WHILE b DO c {P}) =
+ {join so (post c)}
+ WHILE b DO step1 (bfilter b True I) c
+ {bfilter b False I}"
+
+definition "show_acom xs = map_acom (Option.map (show_state xs))"
+
+definition
+ "p1 = ''x'' ::= N 2; IF Less (V ''x'') (N 3) THEN ''x'' ::= N 1 ELSE com.SKIP"
+
+definition "p2 =
+ ''x'' ::= N 0; WHILE Less (V ''x'') (N 2) DO ''x'' ::= Plus (V ''x'') (N 1)"
+
+value "show_acom [''x'']
+ (((step1 None)^^6) (step1 (Some <>) (anno None p2)))"
+
+subsubsection "Relating the small step and the collecting semantics"
+
+hide_const (open) set
+
+abbreviation set :: "'a option acom \<Rightarrow> 'a set acom" where
+"set == map_acom Option.set"
+
+definition some :: "'a option \<Rightarrow> nat" where
+"some opt = (case opt of Some x \<Rightarrow> 1 | None \<Rightarrow> 0)"
+
+lemma some[simp]: "some None = 0 \<and> some (Some x) = 1"
+by(simp add: some_def split:option.split)
+
+fun somes :: "'a option acom \<Rightarrow> nat" where
+"somes(SKIP {p}) = some p" |
+"somes(x::=e {p}) = some p" |
+"somes(c1;c2) = somes c1 + somes c2" |
+"somes(IF b THEN c1 ELSE c2 {p}) = somes c1 + somes c2 + some p" |
+"somes({i} WHILE b DO c {p}) = some i + somes c + some p"
+
+lemma some_anno_None: "somes(anno None c) = 0"
+by(induction c) auto
+
+lemma some_post: "some(post co) \<le> somes co"
+by(induction co) auto
+
+lemma some_join:
+ "some so1 + some so2 \<le> 1 \<Longrightarrow> some(join so1 so2) = some so1 + some so2"
+by(simp add: some_def split: option.splits)
+
+lemma somes_step1: "some so + somes co \<le> 1 \<Longrightarrow>
+ somes(step1 so co) + some(post co) = some so + somes co"
+proof(induction co arbitrary: so)
+ case SKIP thus ?case by simp
+next
+ case Assign thus ?case by (simp split:option.split)
+next
+ case (Semi co1 _)
+ from Semi.prems Semi.IH(1)[of so] Semi.IH(2)[of "post co1"]
+ show ?case by simp
+next
+ case (If b)
+ from If.prems If.IH(1)[of "bfilter b True so"]
+ If.prems If.IH(2)[of "bfilter b False so"]
+ show ?case
+ by (auto simp: bfilter_def some_join split:option.split)
+next
+ case (While i b c p)
+ from While.prems While.IH[of "bfilter b True i"]
+ show ?case
+ by(auto simp: bfilter_def some_join split:option.split)
+qed
+
+lemma post_map_acom[simp]: "post(map_acom f c) = f(post c)"
+by(induction c) auto
+
+lemma join_eq_Some: "some so1 + some so2 \<le> 1 \<Longrightarrow>
+ join so1 so2 = Some s =
+ (so1 = Some s & so2 = None | so1 = None & so2 = Some s)"
+apply(cases so1) apply simp
+apply(cases so2) apply auto
+done
+
+lemma set_bfilter:
+ "Option.set (bfilter b r so) = {s : Option.set so. bval b s = r}"
+by(auto simp: bfilter_def split: option.splits)
+
+lemma set_join: "some so1 + some so2 \<le> 1 \<Longrightarrow>
+ Option.set (join so1 so2) = Option.set so1 \<union> Option.set so2"
+apply(cases so1) apply simp
+apply(cases so2) apply auto
+done
+
+lemma add_le1_iff: "m + n \<le> (Suc 0) \<longleftrightarrow> (m=0 \<and> n\<le>1 | m\<le>1 & n=0)"
+by arith
+
+lemma some_0_iff: "some opt = 0 \<longleftrightarrow> opt = None"
+by(auto simp add: some_def split: option.splits)
+
+lemma some_le1[simp]: "some x \<le> Suc 0"
+by(auto simp add: some_def split: option.splits)
+
+lemma step1_preserves_le:
+ "\<lbrakk> step_cs S cs = cs; Option.set so \<subseteq> S; set co \<le> cs;
+ somes co + some so \<le> 1 \<rbrakk> \<Longrightarrow>
+ set(step1 so co) \<le> cs"
+proof(induction co arbitrary: S cs so)
+ case SKIP thus ?case by (clarsimp simp: SKIP_le)
+next
+ case Assign thus ?case by (fastforce simp: Assign_le split: option.splits)
+next
+ case (Semi co1 co2)
+ from Semi.prems show ?case using some_post[of co1]
+ by (fastforce simp add: Semi_le add_le1_iff Semi.IH dest: le_post)
+next
+ case (If _ co1 co2)
+ from If.prems show ?case
+ using some_post[of co1] some_post[of co2]
+ by (fastforce simp: If_le add_le1_iff some_0_iff set_bfilter subset_iff
+ join_eq_Some If.IH dest: le_post)
+next
+ case (While _ _ co)
+ from While.prems show ?case
+ using some_post[of co]
+ by (fastforce simp: While_le set_bfilter subset_iff join_eq_Some
+ add_le1_iff some_0_iff While.IH dest: le_post)
+qed
+
+lemma step1_None_preserves_le:
+ "\<lbrakk> step_cs S cs = cs; set co \<le> cs; somes co \<le> 1 \<rbrakk> \<Longrightarrow>
+ set(step1 None co) \<le> cs"
+by(auto dest: step1_preserves_le[of _ _ None])
+
+lemma step1_Some_preserves_le:
+ "\<lbrakk> step_cs S cs = cs; s : S; set co \<le> cs; somes co = 0 \<rbrakk> \<Longrightarrow>
+ set(step1 (Some s) co) \<le> cs"
+by(auto dest: step1_preserves_le[of _ _ "Some s"])
+
+lemma steps_None_preserves_le: assumes "step_cs S cs = cs"
+shows "set co \<le> cs \<Longrightarrow> somes co \<le> 1 \<Longrightarrow> set ((step1 None ^^ n) co) \<le> cs"
+proof(induction n arbitrary: co)
+ case 0 thus ?case by simp
+next
+ case (Suc n) thus ?case
+ using somes_step1[of None co] step1_None_preserves_le[OF assms Suc.prems]
+ by(simp add:funpow_swap1 Suc.IH)
+qed
+
+
+definition steps :: "state \<Rightarrow> com \<Rightarrow> nat \<Rightarrow> state option acom" where
+"steps s c n = ((step1 None)^^n) (step1 (Some s) (anno None c))"
+
+lemma steps_approx_fix_step_cs: assumes "step_cs S cs = cs" and "s:S"
+shows "set (steps s (strip cs) n) \<le> cs"
+proof-
+ { fix c have "somes (anno None c) = 0" by(induction c) auto }
+ note somes_None = this
+ let ?cNone = "anno None (strip cs)"
+ have "set ?cNone \<le> cs" by(induction cs) auto
+ from step1_Some_preserves_le[OF assms this somes_None]
+ have 1: "set(step1 (Some s) ?cNone) \<le> cs" .
+ have 2: "somes (step1 (Some s) ?cNone) \<le> 1"
+ using some_post somes_step1[of "Some s" ?cNone]
+ by (simp add:some_anno_None[of "strip cs"])
+ from steps_None_preserves_le[OF assms(1) 1 2]
+ show ?thesis by(simp add: steps_def)
+qed
+
+theorem steps_approx_CS: "s:S \<Longrightarrow> set (steps s c n) \<le> CS S c"
+by (metis CS_unfold steps_approx_fix_step_cs strip_CS)
+
+lemma While_final_False: "(WHILE b DO c, s) \<Rightarrow> t \<Longrightarrow> \<not> bval b t"
+by(induct "WHILE b DO c" s t rule: big_step_induct) simp_all
+
+lemma step_cs_complete:
+ "\<lbrakk> step_cs S c = c; (strip c,s) \<Rightarrow> t; s:S \<rbrakk> \<Longrightarrow> t : post c"
+proof(induction c arbitrary: S s t)
+ case (While Inv b c P)
+ from While.prems have inv: "step_cs {s:Inv. bval b s} c = c"
+ and "post c \<subseteq> Inv" and "S \<subseteq> Inv" and "{s:Inv. \<not> bval b s} \<subseteq> P" by(auto)
+ { fix s t have "(WHILE b DO strip c,s) \<Rightarrow> t \<Longrightarrow> s : Inv \<Longrightarrow> t : 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) While.IH[OF inv `(strip c, s1) \<Rightarrow> s2`]
+ `s1 : Inv` `post c \<subseteq> Inv` `bval b s1`
+ show ?case by auto
+ qed
+ } note Inv = this
+ from While.prems(2) have "(WHILE b DO strip c, s) \<Rightarrow> t" and "\<not> bval b t"
+ by(auto dest: While_final_False)
+ from Inv[OF this(1)] `s : S` `S \<subseteq> Inv` have "t : Inv" by blast
+ with `{s:Inv. \<not> bval b s} \<subseteq> P` show ?case using `\<not> bval b t` by auto
+qed auto
+
+theorem CS_complete: "\<lbrakk> (c,s) \<Rightarrow> t; s:S \<rbrakk> \<Longrightarrow> t : post(CS S c)"
+by (metis CS_unfold step_cs_complete strip_CS)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Collecting_list.thy Thu Nov 24 19:58:37 2011 +0100
@@ -0,0 +1,25 @@
+theory Collecting_list
+imports ACom
+begin
+
+subsection "Executable Collecting Semantics on lists"
+
+fun step_cs :: "state list \<Rightarrow> state list acom \<Rightarrow> state list acom" where
+"step_cs S (SKIP {P}) = (SKIP {S})" |
+"step_cs S (x ::= e {P}) =
+ (x ::= e {[s(x := aval e s). s \<leftarrow> S]})" |
+"step_cs S (c1; c2) = step_cs S c1; step_cs (post c1) c2" |
+"step_cs S (IF b THEN c1 ELSE c2 {P}) =
+ IF b THEN step_cs [s \<leftarrow> S. bval b s] c1 ELSE step_cs [s\<leftarrow>S. \<not> bval b s] c2
+ {post c1 @ post c2}" |
+"step_cs S ({Inv} WHILE b DO c {P}) =
+ {S @ post c} WHILE b DO (step_cs [s\<leftarrow>Inv. bval b s] c) {[s\<leftarrow>Inv. \<not> bval b s]}"
+
+definition "c = WHILE Less (V ''x'') (N 2) DO ''x'' ::= Plus (V ''x'') (N 1)"
+definition "c0 = anno [] c"
+
+definition "show_acom xs = map_acom (map (show_state xs))"
+
+value "show_acom [''x''] (((step_cs [<>]) ^^ 6) c0)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Complete_Lattice_ix.thy Thu Nov 24 19:58:37 2011 +0100
@@ -0,0 +1,55 @@
+theory Complete_Lattice_ix
+imports Main
+begin
+
+text{* A complete lattice is an ordered type where every set of elements has
+a greatest lower (and thus also a leats upper) bound. Sets are the
+prototypical complete lattice where the greatest lower bound is
+intersection. Sometimes that set of all elements of a type is not a complete
+lattice although all elements of the same shape form a complete lattice, for
+example lists of the same length, where the list elements come from a
+complete lattice. We will have exactly this situation with annotated
+commands. This theory introduces a slightly generalised version of complete
+lattices where elements have an ``index'' and only the set of elements with
+the same index form a complete lattice; the type as a whole is a disjoint
+union of complete lattices. Because sets are not types, this requires a
+special treatment. *}
+
+locale Complete_Lattice_ix =
+fixes ix :: "'a::order \<Rightarrow> 'i"
+and Glb :: "'i \<Rightarrow> 'a set \<Rightarrow> 'a"
+assumes Glb_lower: "\<forall>a\<in>A. ix a = i \<Longrightarrow> a \<in> A \<Longrightarrow> (Glb i A) \<le> a"
+and Glb_greatest: "\<forall>a\<in>A. b \<le> a \<Longrightarrow> ix b = i \<Longrightarrow> b \<le> (Glb i A)"
+and ix_Glb: "\<forall>a\<in>A. ix a = i \<Longrightarrow> ix(Glb i A) = i"
+begin
+
+definition lfp :: "'i \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" where
+"lfp i f = Glb i {a. ix a = i \<and> f a \<le> a}"
+
+lemma index_lfp[simp]: "ix(lfp i f) = i"
+by(simp add: lfp_def ix_Glb)
+
+lemma lfp_lowerbound:
+ "\<lbrakk> ix a = i; f a \<le> a \<rbrakk> \<Longrightarrow> lfp i f \<le> a"
+by (auto simp add: lfp_def intro: Glb_lower)
+
+lemma lfp_greatest:
+ "\<lbrakk> ix a = i; \<And>u. \<lbrakk>ix u = i; f u \<le> u\<rbrakk> \<Longrightarrow> a \<le> u \<rbrakk> \<Longrightarrow> a \<le> lfp i f"
+by (auto simp add: lfp_def intro: Glb_greatest)
+
+lemma lfp_unfold: assumes "\<And>x. ix(f x) = ix x"
+and mono: "mono f" shows "lfp i f = f (lfp i f)"
+proof-
+ note assms(1)[simp]
+ have 1: "f (lfp i f) \<le> lfp i f"
+ apply(rule lfp_greatest)
+ apply(simp)
+ by (blast intro: lfp_lowerbound monoD[OF mono] order_trans)
+ have "lfp i f \<le> f (lfp i f)"
+ by (fastforce intro: 1 monoD[OF mono] lfp_lowerbound)
+ with 1 show ?thesis by(blast intro: order_antisym)
+qed
+
+end
+
+end