# HG changeset patch
# User nipkow
# Date 1316227304 -7200
# Node ID f136409c2ceff573fdd738f95534151d47bcd22e
# Parent  b62559f085bcbb3743027610bf927f0b99df3606
tuned post fixpoint setup

diff -r b62559f085bc -r f136409c2cef src/HOL/IMP/AbsInt0.thy
--- 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
diff -r b62559f085bc -r f136409c2cef src/HOL/IMP/AbsInt0_const.thy
--- 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 =
diff -r b62559f085bc -r f136409c2cef src/HOL/IMP/AbsInt0_fun.thy
--- 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
diff -r b62559f085bc -r f136409c2cef src/HOL/IMP/AbsInt1.thy
--- 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"
diff -r b62559f085bc -r f136409c2cef src/HOL/IMP/AbsInt1_ivl.thy
--- 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
diff -r b62559f085bc -r f136409c2cef src/HOL/IMP/AbsInt2.thy
--- 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)"