--- a/src/HOL/IMP/Abs_Int0.thy Mon Oct 10 20:14:25 2011 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy Wed Oct 12 09:16:30 2011 +0200
@@ -9,10 +9,7 @@
text{* Abstract interpretation over type @{text astate} instead of
functions. *}
-locale Abs_Int = Val_abs +
-fixes pfp :: "('a st up acom \<Rightarrow> 'a st up acom) \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom"
-assumes pfp: "\<forall>c. strip(f c) = strip c \<Longrightarrow> f(pfp f c) \<sqsubseteq> pfp f c"
-and strip_pfp: "\<forall>c. strip(f c) = strip c \<Longrightarrow> strip(pfp f c) = strip c"
+locale Abs_Int = Val_abs
begin
fun aval' :: "aexp \<Rightarrow> 'a st \<Rightarrow> 'a" where
@@ -31,27 +28,15 @@
"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
+"AI = lpfp\<^isub>c (step \<top>)"
+
+
lemma strip_step[simp]: "strip(step S c) = strip c"
by(induct c arbitrary: S) (simp_all add: Let_def)
-definition AI :: "com \<Rightarrow> 'a st up acom" where
-"AI c = pfp (step Top) (bot_acom c)"
-
-subsubsection "Monotonicity"
-
-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_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> update S x a \<sqsubseteq> update S' x a'"
-by(auto simp add: le_st_def lookup_def update_def)
-
-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)
-done
-
-subsubsection "Soundness"
+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)
@@ -92,10 +77,29 @@
by simp (metis `s <:up S` `S \<sqsubseteq> Inv` `Inv \<sqsubseteq> P` up_fun_in_rep_le)
qed
-lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> t <:up post(AI c)"
-by(fastforce simp: AI_def strip_pfp in_rep_Top_up intro: step_sound pfp)
+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)
end
+subsubsection "Monotonicity"
+
+locale Abs_Int_mono = Abs_Int +
+assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
+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_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> update S x a \<sqsubseteq> update S' x a'"
+by(auto simp add: le_st_def lookup_def update_def)
+
+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)
+done
+
end
+
+end
--- a/src/HOL/IMP/Abs_Int0_const.thy Mon Oct 10 20:14:25 2011 +0200
+++ b/src/HOL/IMP/Abs_Int0_const.thy Wed Oct 12 09:16:30 2011 +0200
@@ -51,33 +51,25 @@
end
-interpretation Rep rep_cval
+
+interpretation Val_abs rep_cval Const plus_cval
proof
case goal1 thus ?case
by(cases a, cases b, simp, simp, cases b, simp, simp)
next
case goal2 show ?case by(simp add: Top_cval_def)
-qed
-
-interpretation Val_abs rep_cval Const plus_cval
-proof
- case goal1 show ?case by simp
next
- case goal2 thus ?case
- by(auto simp: plus_cval_cases split: cval.split)
+ case goal3 show ?case by simp
next
- case goal3 thus ?case
+ case goal4 thus ?case
by(auto simp: plus_cval_cases split: cval.split)
qed
-text{* Could set the limit of the number of iterations to an arbitrarily
-large number because all ascending chains in this semilattice are finite. *}
-
-interpretation Abs_Int rep_cval Const plus_cval "(iter 15)"
+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 (auto simp: iter_pfp strip_iter)
+proof qed
text{* Straight line code: *}
definition "test1_const =
@@ -113,28 +105,20 @@
WHILE Less (V ''x'') (N 1)
DO (''x'' ::= V ''y''; ''y'' ::= V ''z''; ''z'' ::= V ''u'')"
-text{* For readability: *}
-translations "x" <= "CONST V x"
-translations "x" <= "CONST N x"
-translations "x" <= "CONST Const x"
-translations "x < y" <= "CONST Less x y"
-translations "x" <= "CONST B x"
-translations "x" <= "CONST Up x"
-
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))"
value [code] "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test1_const))"
value [code] "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test1_const))"
-value [code] "show_acom (AI_const test1_const)"
+value [code] "show_acom_opt (AI_const test1_const)"
-value [code] "show_acom (AI_const test2_const)"
-value [code] "show_acom (AI_const test3_const)"
+value [code] "show_acom_opt (AI_const test2_const)"
+value [code] "show_acom_opt (AI_const test3_const)"
value [code] "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test4_const))"
value [code] "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test4_const))"
value [code] "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test4_const))"
value [code] "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test4_const))"
-value [code] "show_acom (AI_const test4_const)"
+value [code] "show_acom_opt (AI_const test4_const)"
value [code] "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test5_const))"
value [code] "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test5_const))"
@@ -142,9 +126,17 @@
value [code] "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test5_const))"
value [code] "show_acom (((step_const \<top>)^^4) (\<bottom>\<^sub>c test5_const))"
value [code] "show_acom (((step_const \<top>)^^5) (\<bottom>\<^sub>c test5_const))"
-value [code] "show_acom (AI_const test5_const)"
+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)"
-value [code] "show_acom (AI_const test6_const)"
-value [code] "show_acom (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 Mon Oct 10 20:14:25 2011 +0200
+++ b/src/HOL/IMP/Abs_Int0_fun.thy Wed Oct 12 09:16:30 2011 +0200
@@ -4,6 +4,7 @@
theory Abs_Int0_fun
imports "~~/src/HOL/ex/Interpretation_with_Defs" Big_Step
+ "~~/src/HOL/Library/While_Combinator"
begin
subsection "Annotated Commands"
@@ -155,15 +156,6 @@
end
-definition Top_acom :: "com \<Rightarrow> ('a::SL_top) acom" ("\<top>\<^sub>c") where
-"\<top>\<^sub>c = anno \<top>"
-
-lemma strip_Top_acom[simp]: "strip (\<top>\<^sub>c c) = c"
-by(simp add: Top_acom_def)
-
-lemma le_Top_acomp[simp]: "strip c' = c \<Longrightarrow> c' \<sqsubseteq> \<top>\<^sub>c c"
-by(induct c' arbitrary: c) (auto simp: Top_acom_def)
-
subsubsection "Lifting"
@@ -216,23 +208,69 @@
lemma strip_bot_acom[simp]: "strip(\<bottom>\<^sub>c c) = c"
by(simp add: bot_acom_def)
+lemma bot_acom[rule_format]: "strip c' = c \<longrightarrow> \<bottom>\<^sub>c c \<sqsubseteq> c'"
+apply(induct c arbitrary: c')
+apply (simp_all add: bot_acom_def)
+ apply(induct_tac c')
+ apply simp_all
+ apply(induct_tac c')
+ apply simp_all
+ apply(induct_tac c')
+ apply simp_all
+ apply(induct_tac c')
+ apply simp_all
+ apply(induct_tac c')
+ apply simp_all
+done
-subsection "Absract Interpretation"
+
+subsubsection "Post-fixed point iteration"
-text{* The representation of abstract by a set of concrete values: *}
+definition
+ pfp :: "(('a::preord) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
+"pfp f = while_option (\<lambda>x. \<not> f x \<sqsubseteq> x) f"
+
+lemma pfp_pfp: assumes "pfp f x0 = Some x" shows "f x \<sqsubseteq> x"
+using while_option_stop[OF assms[simplified pfp_def]] by simp
-locale Rep =
-fixes rep :: "'a::SL_top \<Rightarrow> 'b set"
-assumes le_rep: "a \<sqsubseteq> b \<Longrightarrow> rep a \<subseteq> rep b"
-and rep_Top: "rep \<top> = UNIV"
-begin
+lemma pfp_least:
+assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
+and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" and "pfp f x0 = Some x" shows "x \<sqsubseteq> p"
+proof-
+ { fix x assume "x \<sqsubseteq> p"
+ hence "f x \<sqsubseteq> f p" by(rule mono)
+ from this `f p \<sqsubseteq> p` have "f x \<sqsubseteq> p" by(rule le_trans)
+ }
+ thus "x \<sqsubseteq> p" using assms(2-) while_option_rule[where P = "%x. x \<sqsubseteq> p"]
+ unfolding pfp_def by blast
+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 f c = pfp f (\<bottom>\<^sub>c c)"
+
+lemma lpfpc_pfp: "lpfp\<^isub>c f c0 = Some c \<Longrightarrow> f c \<sqsubseteq> c"
+by(simp add: pfp_pfp lpfp\<^isub>c_def)
-abbreviation in_rep (infix "<:" 50) where "x <: a == x : rep a"
+lemma strip_pfp:
+assumes "\<And>x. g(f x) = g x" and "pfp f x0 = Some x" shows "g x = g x0"
+using assms while_option_rule[where P = "%x. g x = g x0" and c = f]
+unfolding pfp_def by metis
+
+lemma strip_lpfpc: assumes "\<And>c. strip(f c) = strip c" and "lpfp\<^isub>c f c = Some c'"
+shows "strip c' = c"
+using assms(1) strip_pfp[OF _ assms(2)[simplified lpfp\<^isub>c_def]]
+by(metis strip_bot_acom)
-lemma in_rep_Top[simp]: "x <: \<top>"
-by(simp add: rep_Top)
+lemma lpfpc_least:
+assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
+and "strip p = c0" and "f p \<sqsubseteq> p" and lp: "lpfp\<^isub>c f c0 = Some c" shows "c \<sqsubseteq> p"
+using pfp_least[OF _ _ bot_acom[OF `strip p = c0`] lp[simplified lpfp\<^isub>c_def]]
+ mono `f p \<sqsubseteq> p`
+by blast
-end
+
+subsection "Abstract Interpretation"
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)}"
@@ -243,72 +281,28 @@
text{* The interface for abstract values: *}
-(* FIXME: separate Rep interface needed? *)
-locale Val_abs = Rep rep for rep :: "'a::SL_top \<Rightarrow> val set" +
+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 num' :: "val \<Rightarrow> 'a"
and plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
-assumes rep_num': "n <: num' n"
-and rep_plus': "n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: plus' a1 a2"
-and mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
-
-
-subsubsection "Post-fixed point iteration"
-
-fun iter :: "nat \<Rightarrow> (('a::SL_top) acom \<Rightarrow> 'a acom) \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
-"iter 0 f c = \<top>\<^sub>c (strip c)" |
-"iter (Suc n) f c = (let fc = f c in if fc \<sqsubseteq> c then c else iter n f fc)"
-(* code lemma?? *)
-
-lemma strip_iter: assumes "\<forall>c. strip(f c) = strip c"
-shows "strip(iter n f c) = strip c"
-apply (induction n arbitrary: c)
- apply (metis iter.simps(1) strip_Top_acom)
-apply (simp add:Let_def)
-by (metis assms)
-
-lemma iter_pfp: assumes "\<forall>c. strip(f c) = strip c"
-shows "f(iter n f c) \<sqsubseteq> iter n f c"
-apply (induction n arbitrary: c)
- apply(simp add: assms)
-apply (simp add:Let_def)
-done
+ assumes rep_num': "n : rep(num' n)"
+ and rep_plus':
+ "n1 : rep a1 \<Longrightarrow> n2 : rep a2 \<Longrightarrow> n1+n2 : rep(plus' a1 a2)"
+begin
-lemma iter_funpow: assumes "\<forall>c. strip(f c) = strip c"
-shows "iter n f x \<noteq> \<top>\<^sub>c (strip x) \<Longrightarrow> \<exists>k. iter n f x = (f^^k) x"
-apply(induction n arbitrary: x)
- apply simp
-apply (auto simp: Let_def assms)
- apply(metis funpow.simps(1) id_def)
-by (metis assms funpow.simps(2) funpow_swap1 o_apply)
-
-text{* For monotone @{text f}, @{term "iter f n x0"} yields the least
-post-fixed point above @{text x0}, unless it yields @{text Top}. *}
+abbreviation in_rep (infix "<:" 50)
+ where "x <: a == x : rep a"
-lemma iter_least_pfp:
-assumes strip: "\<forall>c. strip(f c) = strip c"
-and mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
-and not_top: "iter n f x0 \<noteq> \<top>\<^sub>c (strip x0)"
-and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "iter n f x0 \<sqsubseteq> p"
-proof-
- obtain k where "iter n f x0 = (f^^k) x0"
- using iter_funpow[OF strip not_top] by blast
- moreover
- { fix n have "(f^^n) x0 \<sqsubseteq> p"
- proof(induction n)
- case 0 show ?case by(simp add: `x0 \<sqsubseteq> p`)
- next
- case (Suc n) thus ?case
- by (simp add: `x0 \<sqsubseteq> p`)(metis Suc `f p \<sqsubseteq> p` le_trans mono)
- qed
- } ultimately show ?thesis by simp
-qed
+lemma in_rep_Top[simp]: "x <: \<top>"
+by(simp add: rep_Top)
+
+end
type_synonym 'a st = "(name \<Rightarrow> 'a)"
-locale Abs_Int_Fun = Val_abs +
-fixes pfp :: "('a st up acom \<Rightarrow> 'a st up acom) \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom"
-assumes pfp: "f(pfp f c) \<sqsubseteq> pfp f c"
-and strip_pfp: "\<forall>c. strip(f c) = strip c \<Longrightarrow> strip(pfp f c) = strip c"
+locale Abs_Int_Fun = Val_abs
begin
fun aval' :: "aexp \<Rightarrow> 'a st \<Rightarrow> 'a" where
@@ -316,24 +310,26 @@
"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" where
+fun step :: "'a st up \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up 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))}" |
"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
- in IF b THEN c1' ELSE c2' {post c1 \<squnion> post c2})" |
+ 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
+"AI = lpfp\<^isub>c (step \<top>)"
+
+
lemma strip_step[simp]: "strip(step S c) = strip c"
by(induct c arbitrary: S) (simp_all add: Let_def)
-definition AI :: "com \<Rightarrow> 'a st up acom" where
-"AI c = pfp (step \<top>) (\<bottom>\<^sub>c c)"
-
+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"
@@ -358,20 +354,7 @@
by(simp add: Top_up_def in_rep_Top_fun)
-subsubsection "Monotonicity"
-
-lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'"
-by(induction e)(auto simp: le_fun_def mono_plus')
-
-lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> S(x := a) \<sqsubseteq> S'(x := a')"
-by(simp add: le_fun_def)
-
-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)
-done
-
-subsubsection "Soundness"
+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_fun_def)
@@ -380,7 +363,8 @@
by(simp add: rep_fun_def)
lemma step_sound:
- "step S c \<sqsubseteq> c \<Longrightarrow> (strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up S \<Longrightarrow> t <:up post c"
+ "\<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)
case SKIP thus ?case
by simp (metis skipE up_fun_in_rep_le)
@@ -412,8 +396,29 @@
by simp (metis `s <:up S` `S \<sqsubseteq> Inv` `Inv \<sqsubseteq> P` up_fun_in_rep_le)
qed
-lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> t <:up post(AI c)"
-by(auto simp: AI_def strip_pfp in_rep_Top_up intro: step_sound pfp)
+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)
+
+end
+
+
+subsubsection "Monotonicity"
+
+locale Abs_Int_Fun_mono = Abs_Int_Fun +
+assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
+begin
+
+lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'"
+by(induction e)(auto simp: le_fun_def mono_plus')
+
+lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> S(x := a) \<sqsubseteq> S'(x := a')"
+by(simp add: le_fun_def)
+
+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)
+done
end
--- a/src/HOL/IMP/Abs_Int1.thy Mon Oct 10 20:14:25 2011 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy Wed Oct 12 09:16:30 2011 +0200
@@ -30,10 +30,19 @@
and meet_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
and meet_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
assumes bot[simp]: "\<bottom> \<sqsubseteq> x"
+begin
-locale Rep1 = Rep rep for rep :: "'a::L_top_bot \<Rightarrow> 'b set" +
-assumes inter_rep_subset_rep_meet: "rep a1 \<inter> rep a2 \<subseteq> rep(a1 \<sqinter> a2)"
- -- "this means the meet is precise"
+lemma mono_meet: "x \<sqsubseteq> x' \<Longrightarrow> y \<sqsubseteq> y' \<Longrightarrow> x \<sqinter> y \<sqsubseteq> x' \<sqinter> y'"
+by (metis meet_greatest meet_le1 meet_le2 le_trans)
+
+end
+
+
+locale Val_abs1_rep =
+ Val_abs rep num' plus'
+ for rep :: "'a::L_top_bot \<Rightarrow> val set" and num' plus' +
+assumes inter_rep_subset_rep_meet:
+ "rep a1 \<inter> rep a2 \<subseteq> rep(a1 \<sqinter> a2)"
and rep_Bot: "rep \<bottom> = {}"
begin
@@ -43,29 +52,19 @@
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 mono_meet: "x \<sqsubseteq> x' \<Longrightarrow> y \<sqsubseteq> y' \<Longrightarrow> x \<sqinter> y \<sqsubseteq> x' \<sqinter> y'"
-by (metis meet_greatest meet_le1 meet_le2 le_trans)
-
end
-locale Val_abs1 = Val_abs rep num' plus' + Rep1 rep
- for rep :: "'a::L_top_bot \<Rightarrow> int set" and num' plus' +
+locale Val_abs1 = Val_abs1_rep +
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'"
and filter_less': "filter_less' (n1<n2) a1 a2 = (a1',a2') \<Longrightarrow>
n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
-and mono_filter_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> r \<sqsubseteq> r' \<Longrightarrow>
- filter_plus' r a1 a2 \<sqsubseteq> filter_plus' r' b1 b2"
-and mono_filter_less': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow>
- filter_less' bv a1 a2 \<sqsubseteq> filter_less' bv b1 b2"
+
-locale Abs_Int1 = Val_abs1 +
-fixes pfp :: "('a st up acom \<Rightarrow> 'a st up acom) \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom"
-assumes pfp: "\<forall>c. strip(f c) = strip c \<Longrightarrow> mono f \<Longrightarrow> f(pfp f c) \<sqsubseteq> pfp f c"
-and strip_pfp: "\<forall>c. strip(f c) = strip c \<Longrightarrow> strip(pfp f c) = strip c"
+locale Abs_Int1 = Val_abs1
begin
lemma in_rep_join_UpI: "s <:up S1 | s <:up S2 \<Longrightarrow> s <:up S1 \<squnion> S2"
@@ -78,7 +77,9 @@
"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
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)
+by(induct a)(auto simp: rep_num' rep_plus' in_rep_up_iff lookup_def rep_st_def)
+
+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)" |
@@ -141,7 +142,8 @@
qed
-fun step :: "'a st up \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom" where
+fun step :: "'a st up \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom"
+ where
"step S (SKIP {P}) = (SKIP {S})" |
"step S (x ::= e {P}) =
x ::= e {case S of Bot \<Rightarrow> Bot
@@ -155,51 +157,13 @@
WHILE b DO step (bfilter b True Inv) c
{bfilter b False Inv}"
+definition AI :: "com \<Rightarrow> 'a st up acom option" where
+"AI = lpfp\<^isub>c (step \<top>)"
+
lemma strip_step[simp]: "strip(step S c) = strip c"
by(induct c arbitrary: S) (simp_all add: Let_def)
-definition AI :: "com \<Rightarrow> 'a st up acom" where
-"AI c = pfp (step \<top>) (\<bottom>\<^sub>c c)"
-
-
-subsubsection "Monotonicity"
-
-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')
-
-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(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)
-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)
-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'"
-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)
-done
-
-
subsubsection "Soundness"
lemma in_rep_update: "\<lbrakk> s <:f S; i <: a \<rbrakk> \<Longrightarrow> s(x := i) <:f update S x a"
@@ -257,9 +221,59 @@
show ?case using `\<not> bval b t` by simp
qed
-lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> t <:up post(AI c)"
-by(fastforce simp: AI_def strip_pfp mono_def in_rep_Top_up
- intro: step_sound pfp mono_step[OF le_refl])
+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)
+*)
+end
+
+
+subsubsection "Monotonicity"
+
+locale Abs_Int1_mono = Abs_Int1 +
+assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
+and mono_filter_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> r \<sqsubseteq> r' \<Longrightarrow>
+ filter_plus' r a1 a2 \<sqsubseteq> filter_plus' r' b1 b2"
+and mono_filter_less': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow>
+ filter_less' bv a1 a2 \<sqsubseteq> filter_less' bv b1 b2"
+begin
+
+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')
+
+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(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)
+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)
+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'"
+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)
+done
end
--- a/src/HOL/IMP/Abs_Int1_ivl.thy Mon Oct 10 20:14:25 2011 +0200
+++ b/src/HOL/IMP/Abs_Int1_ivl.thy Wed Oct 12 09:16:30 2011 +0200
@@ -160,26 +160,20 @@
I (max_option False (l1 + Some 1) l2) h2)
else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
-interpretation Rep rep_ivl
+interpretation Val_abs rep_ivl num_ivl plus_ivl
proof
case goal1 thus ?case
by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
next
case goal2 show ?case by(simp add: rep_ivl_def Top_ivl_def)
+next
+ case goal3 thus ?case by(simp add: rep_ivl_def num_ivl_def)
+next
+ case goal4 thus ?case
+ by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits)
qed
-interpretation Val_abs rep_ivl num_ivl plus_ivl
-proof
- case goal1 thus ?case by(simp add: rep_ivl_def num_ivl_def)
-next
- case goal2 thus ?case
- by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits)
-next
- case goal3 thus ?case
- by(auto simp: plus_ivl_def le_ivl_def le_option_def empty_def split: if_splits ivl.splits option.splits)
-qed
-
-interpretation Rep1 rep_ivl
+interpretation Val_abs1_rep rep_ivl num_ivl plus_ivl
proof
case goal1 thus ?case
by(auto simp add: rep_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
@@ -206,23 +200,16 @@
case goal2 thus ?case
by(cases a1, cases a2,
auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
-next
- case goal3 thus ?case
- by(auto simp: filter_plus_ivl_def le_prod_def mono_meet mono_minus_ivl)
-next
- case goal4 thus ?case
- apply(cases a1, cases b1, cases a2, cases b2, auto simp: le_prod_def)
- by(auto simp add: empty_def le_ivl_def le_option_def min_option_def max_option_def split: option.splits)
qed
interpretation
- Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter 20)"
+ Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
defines afilter_ivl is afilter
and bfilter_ivl is bfilter
and step_ivl is step
and AI_ivl is AI
and aval_ivl is aval'
-proof qed (auto simp: iter_pfp strip_iter)
+proof qed
definition "test1_ivl =
''y'' ::= N 7;
@@ -230,50 +217,78 @@
THEN ''y'' ::= Plus (V ''y'') (V ''x'')
ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
-value [code] "show_acom (AI_ivl test1_ivl)"
+value [code] "show_acom_opt (AI_ivl test1_ivl)"
-value [code] "show_acom (AI_const test3_const)"
-value [code] "show_acom (AI_ivl test3_const)"
+value [code] "show_acom_opt (AI_const test3_const)"
+value [code] "show_acom_opt (AI_ivl test3_const)"
-value [code] "show_acom (AI_const test4_const)"
-value [code] "show_acom (AI_ivl test4_const)"
+value [code] "show_acom_opt (AI_const test4_const)"
+value [code] "show_acom_opt (AI_ivl test4_const)"
-value [code] "show_acom (AI_ivl test6_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 (AI_ivl test2_ivl)"
+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 (AI_ivl test3_ivl)"
+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))"
-value [code] "show_acom(AI_ivl test4_ivl)"
+
+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 1001)
+ WHILE Less (V ''x'') (N 1000)
DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"
-value [code] "show_acom(AI_ivl test5_ivl)"
+value [code] "show_acom_opt (AI_ivl test5_ivl)"
-text{* Nontermination not detected: *}
+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)"
-value [code] "show_acom(AI_ivl test6_ivl)"
+
+text{* Monotonicity: *}
+
+interpretation
+ Abs_Int1_mono rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
+proof
+ case goal1 thus ?case
+ by(auto simp: plus_ivl_def le_ivl_def le_option_def empty_def split: if_splits ivl.splits option.splits)
+next
+ case goal2 thus ?case
+ by(auto simp: filter_plus_ivl_def le_prod_def mono_meet mono_minus_ivl)
+next
+ case goal3 thus ?case
+ apply(cases a1, cases b1, cases a2, cases b2, auto simp: le_prod_def)
+ by(auto simp add: empty_def le_ivl_def le_option_def min_option_def max_option_def split: option.splits)
+qed
end
--- a/src/HOL/IMP/Abs_Int2.thy Mon Oct 10 20:14:25 2011 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy Wed Oct 12 09:16:30 2011 +0200
@@ -9,7 +9,8 @@
class WN = SL_top +
fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)
-assumes widen: "y \<sqsubseteq> x \<nabla> y"
+assumes widen1: "x \<sqsubseteq> x \<nabla> y"
+assumes widen2: "y \<sqsubseteq> x \<nabla> y"
fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
@@ -49,12 +50,15 @@
instance
proof
case goal1 thus ?case
- by(simp add: widen_st_def le_st_def lookup_def widen)
+ by(simp add: widen_st_def le_st_def lookup_def widen1)
next
case goal2 thus ?case
+ by(simp add: widen_st_def le_st_def lookup_def widen2)
+next
+ case goal3 thus ?case
by(auto simp: narrow_st_def le_st_def lookup_def narrow1)
next
- case goal3 thus ?case
+ case goal4 thus ?case
by(auto simp: narrow_st_def le_st_def lookup_def narrow2)
qed
@@ -76,12 +80,15 @@
instance
proof
case goal1 show ?case
- by(induct x y rule: widen_up.induct) (simp_all add: widen)
+ by(induct x y rule: widen_up.induct) (simp_all add: widen1)
next
- case goal2 thus ?case
+ case goal2 show ?case
+ by(induct x y rule: widen_up.induct) (simp_all add: widen2)
+next
+ case goal3 thus ?case
by(induct x y rule: narrow_up.induct) (simp_all add: narrow1)
next
- case goal3 thus ?case
+ case goal4 thus ?case
by(induct x y rule: narrow_up.induct) (simp_all add: narrow2)
qed
@@ -102,115 +109,112 @@
abbreviation narrow_acom :: "('a::WN)acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" (infix "\<triangle>\<^sub>c" 65)
where "narrow_acom == map2_acom (op \<triangle>)"
+lemma widen1_acom: "strip c = strip c' \<Longrightarrow> c \<sqsubseteq> c \<nabla>\<^sub>c c'"
+by(induct c c' rule: le_acom.induct)(simp_all add: widen1)
+
+lemma widen2_acom: "strip c = strip c' \<Longrightarrow> c' \<sqsubseteq> c \<nabla>\<^sub>c c'"
+by(induct c c' rule: le_acom.induct)(simp_all add: widen2)
+
lemma narrow1_acom: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle>\<^sub>c y"
by(induct y x rule: le_acom.induct) (simp_all add: narrow1)
lemma narrow2_acom: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle>\<^sub>c y \<sqsubseteq> x"
by(induct y x rule: le_acom.induct) (simp_all add: narrow2)
-fun iter_up :: "(('a::WN)acom \<Rightarrow> 'a acom) \<Rightarrow> nat \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
-"iter_up f 0 x = \<top>\<^sub>c (strip x)" |
-"iter_up f (Suc n) x =
- (let fx = f x in if fx \<sqsubseteq> x then x else iter_up f n (x \<nabla>\<^sub>c fx))"
-abbreviation
- iter_down :: "(('a::WN)acom \<Rightarrow> 'a acom) \<Rightarrow> nat \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
-"iter_down f n x == ((\<lambda>x. x \<triangle>\<^sub>c f x)^^n) x"
+subsubsection "Post-fixed point computation"
definition
- iter' :: "nat \<Rightarrow> nat \<Rightarrow> (('a::WN)acom \<Rightarrow> 'a acom) \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
-"iter' m n f x = iter_down f n (iter_up f m x)"
+ prefp :: "(('a::preord) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
+"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"
+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')"
lemma strip_map2_acom:
"strip c1 = strip c2 \<Longrightarrow> strip(map2_acom f c1 c2) = strip c1"
by(induct f c1 c2 rule: map2_acom.induct) simp_all
-lemma strip_iter_up: assumes "\<forall>c. strip(f c) = strip c"
-shows "strip(iter_up f n c) = strip c"
-apply (induction n arbitrary: c)
- apply (metis iter_up.simps(1) strip_Top_acom snd_conv)
-apply (simp add:Let_def)
-by (metis assms strip_map2_acom)
-
-lemma iter_up_pfp: assumes "\<forall>c. strip(f c) = strip c"
-shows "f(iter_up f n c) \<sqsubseteq> iter_up f n c"
-apply (induction n arbitrary: c)
- apply(simp add: assms)
-apply (simp add:Let_def)
-done
-
-lemma strip_iter_down: assumes "\<forall>c. strip(f c) = strip c"
-shows "strip(iter_down f n c) = strip c"
-apply (induction n arbitrary: c)
- apply(simp)
-apply (simp add: strip_map2_acom assms)
-done
+lemma lpfp_step_up_pfp:
+ "\<lbrakk> \<forall>c. strip(f c) = strip c; lpfp\<^isub>c (\<lambda>c. c \<nabla>\<^sub>c f c) c = Some c' \<rbrakk> \<Longrightarrow> f c' \<sqsubseteq> c'"
+by (metis (no_types) assms lpfpc_pfp le_trans widen2_acom)
lemma iter_down_pfp: assumes "mono f" and "f x0 \<sqsubseteq> x0"
-defines "x n == iter_down f n x0"
-shows "f(x n) \<sqsubseteq> x n"
-proof (induction n)
- case 0 show ?case by (simp add: x_def assms(2))
-next
- case (Suc n)
- have "f (x (Suc n)) = f(x n \<triangle>\<^sub>c f(x n))" by(simp add: x_def)
- also have "\<dots> \<sqsubseteq> f(x n)" by(rule monoD[OF `mono f` narrow2_acom[OF Suc]])
- also have "\<dots> \<sqsubseteq> x n \<triangle>\<^sub>c f(x n)" by(rule narrow1_acom[OF Suc])
- also have "\<dots> = x(Suc n)" by(simp add: x_def)
- finally show ?case .
-qed
-
-lemma iter_down_down: assumes "mono f" and "f x0 \<sqsubseteq> x0"
-defines "x n == iter_down f n x0"
-shows "x n \<sqsubseteq> x0"
-proof (induction n)
- case 0 show ?case by(simp add: x_def)
-next
- case (Suc n)
- have "x(Suc n) = x n \<triangle>\<^sub>c f(x n)" by(simp add: x_def)
- also have "\<dots> \<sqsubseteq> x n" unfolding x_def
- by(rule narrow2_acom[OF iter_down_pfp[OF assms(1), OF assms(2)]])
- also have "\<dots> \<sqsubseteq> x0" by(rule Suc)
- finally show ?case .
+and "prefp (\<lambda>c. c \<triangle>\<^sub>c f c) x0 = Some x"
+shows "f x \<sqsubseteq> x \<and> x \<sqsubseteq> x0" (is "?P x")
+proof-
+ { fix x assume "?P x"
+ note 1 = conjunct1[OF this] and 2 = conjunct2[OF this]
+ let ?x' = "x \<triangle>\<^sub>c f x"
+ have "?P ?x'"
+ proof
+ have "f ?x' \<sqsubseteq> f x" by(rule monoD[OF `mono f` narrow2_acom[OF 1]])
+ also have "\<dots> \<sqsubseteq> ?x'" by(rule narrow1_acom[OF 1])
+ finally show "f ?x' \<sqsubseteq> ?x'" .
+ have "?x' \<sqsubseteq> x" by (rule narrow2_acom[OF 1])
+ also have "x \<sqsubseteq> x0" by(rule 2)
+ finally show "?x' \<sqsubseteq> x0" .
+ qed
+ }
+ with while_option_rule[where P = ?P, OF _ assms(3)[simplified prefp_def]]
+ assms(2) le_refl
+ show ?thesis by blast
qed
-lemma iter'_pfp: assumes "\<forall>c. strip (f c) = strip c" and "mono f"
-shows "f (iter' m n f c) \<sqsubseteq> iter' m n f c"
-using iter_up_pfp[of f] iter_down_pfp[of f]
-by(auto simp add: iter'_def Let_def assms)
+lemma pfp_WN_pfp:
+ "\<lbrakk> \<forall>c. strip (f c) = strip c; mono f; pfp_WN f c = Some c' \<rbrakk> \<Longrightarrow> f c' \<sqsubseteq> c'"
+unfolding pfp_WN_def
+by (auto dest: iter_down_pfp lpfp_step_up_pfp split: option.splits)
+
+lemma strip_while: fixes f :: "'a acom \<Rightarrow> 'a acom"
+assumes "\<forall>c. strip (f c) = strip c" and "while_option P f c = Some c'"
+shows "strip c' = strip c"
+using while_option_rule[where P = "\<lambda>c'. strip c' = strip c", OF _ assms(2)]
+by (metis assms(1))
-lemma strip_iter': assumes "\<forall>c. strip(f c) = strip c"
-shows "strip(iter' m n f c) = strip c"
-by(simp add: iter'_def strip_iter_down strip_iter_up assms)
+lemma strip_pfp_WN:
+ "\<lbrakk> \<forall>c. strip(f c) = strip c; pfp_WN f c = Some c' \<rbrakk> \<Longrightarrow> strip c' = c"
+apply(auto simp add: pfp_WN_def prefp_def split: option.splits)
+by (metis (no_types) strip_lpfpc strip_map2_acom strip_while)
+
+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
+"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)
+
+end
interpretation
- Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 20 5)"
-defines afilter_ivl' is afilter
-and bfilter_ivl' is bfilter
-and step_ivl' is step
-and AI_ivl' is AI
-and aval_ivl' is aval'
-proof qed (auto simp: iter'_pfp strip_iter')
+ Abs_Int2 num_ivl plus_ivl filter_plus_ivl filter_less_ivl rep_ivl
+defines AI_ivl' is AI_WN
+proof qed
-value [code] "show_acom (AI_ivl test3_ivl)"
-value [code] "show_acom (AI_ivl' test3_ivl)"
+value [code] "show_acom_opt (AI_ivl test3_ivl)"
+value [code] "show_acom_opt (AI_ivl' test3_ivl)"
+
+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)"
-definition "step_up n = ((\<lambda>c. c \<nabla>\<^sub>c step_ivl \<top> c)^^n)"
-definition "step_down n = ((\<lambda>c. c \<triangle>\<^sub>c step_ivl \<top> c)^^n)"
+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))"
+value [code] "show_acom (step_up_ivl 4 (\<bottom>\<^sub>c test3_ivl))"
+value [code] "show_acom (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl))"
+value [code] "show_acom (step_down_ivl 1 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))"
+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)))"
-value [code] "show_acom (step_up 1 (\<bottom>\<^sub>c test3_ivl))"
-value [code] "show_acom (step_up 2 (\<bottom>\<^sub>c test3_ivl))"
-value [code] "show_acom (step_up 3 (\<bottom>\<^sub>c test3_ivl))"
-value [code] "show_acom (step_up 4 (\<bottom>\<^sub>c test3_ivl))"
-value [code] "show_acom (step_up 5 (\<bottom>\<^sub>c test3_ivl))"
-value [code] "show_acom (step_down 1 (step_up 5 (\<bottom>\<^sub>c test3_ivl)))"
-value [code] "show_acom (step_down 2 (step_up 5 (\<bottom>\<^sub>c test3_ivl)))"
-value [code] "show_acom (step_down 3 (step_up 5 (\<bottom>\<^sub>c test3_ivl)))"
-
-value [code] "show_acom (AI_ivl' test4_ivl)"
-value [code] "show_acom (AI_ivl' test5_ivl)"
-value [code] "show_acom (AI_ivl' test6_ivl)"
+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)"
end
--- a/src/HOL/IMP/Abs_State.thy Mon Oct 10 20:14:25 2011 +0200
+++ b/src/HOL/IMP/Abs_State.thy Wed Oct 12 09:16:30 2011 +0200
@@ -24,6 +24,7 @@
"show_st_up (Up S) = Up(show_st S)"
definition "show_acom = map_acom show_st_up"
+definition "show_acom_opt = Option.map show_acom"
definition "lookup F x = (if x : set(dom F) then fun F x else \<top>)"
@@ -61,10 +62,10 @@
lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> update S x a \<sqsubseteq> update S' x a'"
by(auto simp add: le_st_def lookup_def update_def)
-context Rep
+context Val_abs
begin
-abbreviation fun_in_rep :: "(name \<Rightarrow> 'b) \<Rightarrow> 'a st \<Rightarrow> bool" (infix "<:f" 50) where
+abbreviation fun_in_rep :: "state \<Rightarrow> 'a st \<Rightarrow> bool" (infix "<:f" 50) where
"s <:f S == s \<in> rep_st rep S"
notation fun_in_rep (infix "<:\<^sub>f" 50)
@@ -73,7 +74,7 @@
apply(auto simp add: rep_st_def le_st_def dest: le_rep)
by (metis in_rep_Top le_rep lookup_def subsetD)
-abbreviation in_rep_up :: "(name \<Rightarrow> 'b) \<Rightarrow> 'a st up \<Rightarrow> bool" (infix "<:up" 50)
+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"
notation (output) in_rep_up (infix "<:\<^sub>u\<^sub>p" 50)