--- a/src/HOL/IMP/AbsInt0.thy Sat Sep 17 03:37:14 2011 +0200
+++ b/src/HOL/IMP/AbsInt0.thy Sat Sep 17 04:41:44 2011 +0200
@@ -10,9 +10,9 @@
functions. *}
locale Abs_Int = Val_abs +
-fixes pfp_above :: "('a astate \<Rightarrow> 'a astate) \<Rightarrow> 'a astate \<Rightarrow> 'a astate"
-assumes pfp: "f(pfp_above f x0) \<sqsubseteq> pfp_above f x0"
-assumes above: "x0 \<sqsubseteq> pfp_above f x0"
+fixes pfp :: "('a astate \<Rightarrow> 'a astate) \<Rightarrow> 'a astate \<Rightarrow> 'a astate"
+assumes pfp: "f(pfp f x0) \<sqsubseteq> pfp f x0"
+assumes above: "x0 \<sqsubseteq> pfp f x0"
begin
fun aval' :: "aexp \<Rightarrow> 'a astate \<Rightarrow> 'a" where
@@ -35,7 +35,7 @@
"AI (x ::= a) S = update S x (aval' a S)" |
"AI (c1;c2) S = AI c2 (AI c1 S)" |
"AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
-"AI (WHILE b DO c) S = pfp_above (AI c) S"
+"AI (WHILE b DO c) S = pfp (AI c) S"
lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
proof(induct c arbitrary: s t S0)
@@ -50,7 +50,7 @@
by (metis AI.simps(4) IfE astate_in_rep_le join_ge1 join_ge2)
next
case (While b c)
- let ?P = "pfp_above (AI c) S0"
+ let ?P = "pfp (AI c) S0"
{ fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
proof(induct "WHILE b DO c" s t rule: big_step_induct)
case WhileFalse thus ?case by simp
--- a/src/HOL/IMP/AbsInt0_const.thy Sat Sep 17 03:37:14 2011 +0200
+++ b/src/HOL/IMP/AbsInt0_const.thy Sat Sep 17 04:41:44 2011 +0200
@@ -61,10 +61,10 @@
by(cases a1, cases a2, simp, simp, cases a2, simp, simp)
qed
-interpretation Abs_Int rep_cval Const plus_cval "(iter_above 3)"
+interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)"
defines AI_const is AI
and aval'_const is aval'
-proof qed (auto simp: iter_above_pfp)
+proof qed (auto simp: iter'_pfp_above)
text{* Straight line code: *}
definition "test1_const =
--- a/src/HOL/IMP/AbsInt0_fun.thy Sat Sep 17 03:37:14 2011 +0200
+++ b/src/HOL/IMP/AbsInt0_fun.thy Sat Sep 17 04:41:44 2011 +0200
@@ -41,16 +41,15 @@
apply (simp)
done
-definition iter_above :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
-"iter_above n f x0 = iter n (\<lambda>x. x0 \<squnion> f x) x0"
+abbreviation iter' :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
+"iter' n f x0 == iter n (\<lambda>x. x0 \<squnion> f x) x0"
-lemma iter_above_pfp:
-shows "f(iter_above n f x0) \<sqsubseteq> iter_above n f x0" and "x0 \<sqsubseteq> iter_above n f x0"
-using iter_pfp[of "\<lambda>x. x0 \<squnion> f x"]
-by(auto simp add: iter_above_def)
+lemma iter'_pfp_above:
+ "f(iter' n f x0) \<sqsubseteq> iter' n f x0" "x0 \<sqsubseteq> iter' n f x0"
+using iter_pfp[of "\<lambda>x. x0 \<squnion> f x"] by auto
text{* So much for soundness. But how good an approximation of the post-fixed
-point does @{const iter_above} yield? *}
+point does @{const iter} yield? *}
lemma iter_funpow: "iter n f x \<noteq> Top \<Longrightarrow> \<exists>k. iter n f x = (f^^k) x"
apply(induct n arbitrary: x)
@@ -59,19 +58,17 @@
apply(metis funpow.simps(1) id_def)
by (metis funpow.simps(2) funpow_swap1 o_apply)
-text{* For monotone @{text f}, @{term "iter_above f n x0"} yields the least
+text{* For monotone @{text f}, @{term "iter f n x0"} yields the least
post-fixed point above @{text x0}, unless it yields @{text Top}. *}
lemma iter_least_pfp:
-assumes mono: "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter_above n f x0 \<noteq> Top"
-and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "iter_above n f x0 \<sqsubseteq> p"
+assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter n f x0 \<noteq> Top"
+and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "iter n f x0 \<sqsubseteq> p"
proof-
- let ?F = "\<lambda>x. x0 \<squnion> f x"
- obtain k where "iter_above n f x0 = (?F^^k) x0"
- using iter_funpow `iter_above n f x0 \<noteq> Top`
- by(fastforce simp add: iter_above_def)
+ obtain k where "iter n f x0 = (f^^k) x0"
+ using iter_funpow[OF `iter n f x0 \<noteq> Top`] by blast
moreover
- { fix n have "(?F^^n) x0 \<sqsubseteq> p"
+ { fix n have "(f^^n) x0 \<sqsubseteq> p"
proof(induct n)
case 0 show ?case by(simp add: `x0 \<sqsubseteq> p`)
next
@@ -81,24 +78,6 @@
} ultimately show ?thesis by simp
qed
-lemma chain: assumes "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
-shows "((\<lambda>x. x0 \<squnion> f x)^^i) x0 \<sqsubseteq> ((\<lambda>x. x0 \<squnion> f x)^^(i+1)) x0"
-apply(induct i)
- apply simp
-apply simp
-by (metis assms join_ge2 le_trans)
-
-lemma iter_above_almost_fp:
-assumes mono: "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter_above n f x0 \<noteq> Top"
-shows "iter_above n f x0 \<sqsubseteq> x0 \<squnion> f(iter_above n f x0)"
-proof-
- let ?p = "iter_above n f x0"
- obtain k where 1: "?p = ((\<lambda>x. x0 \<squnion> f x)^^k) x0"
- using iter_funpow `?p \<noteq> Top`
- by(fastforce simp add: iter_above_def)
- thus ?thesis using chain mono by simp
-qed
-
end
text{* The interface of abstract values: *}
@@ -149,9 +128,9 @@
type_synonym 'a st = "name \<Rightarrow> 'a"
locale Abs_Int_Fun = Val_abs +
-fixes pfp_above :: "('a st \<Rightarrow> 'a st) \<Rightarrow> 'a st \<Rightarrow> 'a st"
-assumes pfp: "f(pfp_above f x0) \<sqsubseteq> pfp_above f x0"
-assumes above: "x0 \<sqsubseteq> pfp_above f x0"
+fixes pfp :: "('a st \<Rightarrow> 'a st) \<Rightarrow> 'a st \<Rightarrow> 'a st"
+assumes pfp: "f(pfp f x) \<sqsubseteq> pfp f x"
+assumes above: "x \<sqsubseteq> pfp f x"
begin
fun aval' :: "aexp \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a" where
@@ -173,7 +152,7 @@
"AI (x ::= a) S = S(x := aval' a S)" |
"AI (c1;c2) S = AI c2 (AI c1 S)" |
"AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
-"AI (WHILE b DO c) S = pfp_above (AI c) S"
+"AI (WHILE b DO c) S = pfp (AI c) S"
lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
proof(induct c arbitrary: s t S0)
@@ -186,7 +165,7 @@
case If thus ?case by(auto simp: in_rep_join)
next
case (While b c)
- let ?P = "pfp_above (AI c) S0"
+ let ?P = "pfp (AI c) S0"
{ fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
proof(induct "WHILE b DO c" s t rule: big_step_induct)
case WhileFalse thus ?case by simp
--- a/src/HOL/IMP/AbsInt1.thy Sat Sep 17 03:37:14 2011 +0200
+++ b/src/HOL/IMP/AbsInt1.thy Sat Sep 17 04:41:44 2011 +0200
@@ -83,9 +83,9 @@
locale Abs_Int1 = Val_abs1 +
-fixes pfp_above :: "('a astate up \<Rightarrow> 'a astate up) \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up"
-assumes pfp: "f(pfp_above f x0) \<sqsubseteq> pfp_above f x0"
-assumes above: "x0 \<sqsubseteq> pfp_above f x0"
+fixes pfp :: "('a astate up \<Rightarrow> 'a astate up) \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up"
+assumes pfp: "f(pfp f x0) \<sqsubseteq> pfp f x0"
+assumes above: "x0 \<sqsubseteq> pfp f x0"
begin
(* FIXME avoid duplicating this defn *)
@@ -178,7 +178,7 @@
"AI (IF b THEN c1 ELSE c2) S =
AI c1 (bfilter b True S) \<squnion> AI c2 (bfilter b False S)" |
"AI (WHILE b DO c) S =
- bfilter b False (pfp_above (\<lambda>S. AI c (bfilter b True S)) S)"
+ bfilter b False (pfp (\<lambda>S. AI c (bfilter b True S)) S)"
lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <:: S \<Longrightarrow> t <:: AI c S"
proof(induct c arbitrary: s t S)
@@ -192,7 +192,7 @@
case If thus ?case by (auto simp: in_rep_join_UpI bfilter_sound)
next
case (While b c)
- let ?P = "pfp_above (\<lambda>S. AI c (bfilter b True S)) S"
+ let ?P = "pfp (\<lambda>S. AI c (bfilter b True S)) S"
{ fix s t
have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <:: ?P \<Longrightarrow>
t <:: bfilter b False ?P"
--- a/src/HOL/IMP/AbsInt1_ivl.thy Sat Sep 17 03:37:14 2011 +0200
+++ b/src/HOL/IMP/AbsInt1_ivl.thy Sat Sep 17 04:41:44 2011 +0200
@@ -190,12 +190,12 @@
qed
interpretation
- Abs_Int1 rep_ivl num_ivl plus_ivl inv_plus_ivl inv_less_ivl "(iter_above 3)"
+ Abs_Int1 rep_ivl num_ivl plus_ivl inv_plus_ivl inv_less_ivl "(iter' 3)"
defines afilter_ivl is afilter
and bfilter_ivl is bfilter
and AI_ivl is AI
and aval_ivl is aval'
-proof qed (auto simp: iter_above_pfp)
+proof qed (auto simp: iter'_pfp_above)
fun list_up where
--- a/src/HOL/IMP/AbsInt2.thy Sat Sep 17 03:37:14 2011 +0200
+++ b/src/HOL/IMP/AbsInt2.thy Sat Sep 17 04:41:44 2011 +0200
@@ -40,15 +40,15 @@
apply (simp add: Let_def)
done
-definition iter_above :: "nat \<Rightarrow> nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
-"iter_above m n f x =
+definition iter' :: "nat \<Rightarrow> nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
+"iter' m n f x =
(let f' = (\<lambda>y. x \<squnion> f y) in iter_down f' n (iter_up f' m x))"
-lemma iter_above_pfp:
-shows "f(iter_above m n f x0) \<sqsubseteq> iter_above m n f x0"
-and "x0 \<sqsubseteq> iter_above m n f x0"
+lemma iter'_pfp_above:
+shows "f(iter' m n f x0) \<sqsubseteq> iter' m n f x0"
+and "x0 \<sqsubseteq> iter' m n f x0"
using iter_up_pfp[of "\<lambda>x. x0 \<squnion> f x"] iter_down_pfp[of "\<lambda>x. x0 \<squnion> f x"]
-by(auto simp add: iter_above_def Let_def)
+by(auto simp add: iter'_def Let_def)
end
@@ -126,12 +126,12 @@
end
interpretation
- Abs_Int1 rep_ivl num_ivl plus_ivl inv_plus_ivl inv_less_ivl "(iter_above 3 2)"
+ Abs_Int1 rep_ivl num_ivl plus_ivl inv_plus_ivl inv_less_ivl "(iter' 3 2)"
defines afilter_ivl' is afilter
and bfilter_ivl' is bfilter
and AI_ivl' is AI
and aval_ivl' is aval'
-proof qed (auto simp: iter_above_pfp)
+proof qed (auto simp: iter'_pfp_above)
value [code] "list_up(AI_ivl' test3_ivl Top)"
value [code] "list_up(AI_ivl' test4_ivl Top)"