# HG changeset patch
# User nipkow
# Date 1315975741 -7200
# Node ID b80108b346a957be8f1fe0616da79c6c85cae0d3
# Parent  884d27ede438d5143b073d99ff2330a6c0f51ac4
cleand up AbsInt fixpoint iteration; tuned syntax

diff -r 884d27ede438 -r b80108b346a9 src/HOL/IMP/AExp.thy
--- a/src/HOL/IMP/AExp.thy	Tue Sep 13 07:13:49 2011 +0200
+++ b/src/HOL/IMP/AExp.thy	Wed Sep 14 06:49:01 2011 +0200
@@ -16,33 +16,37 @@
 "aval (Plus a1 a2) s = aval a1 s + aval a2 s"
 
 
-value "aval (Plus (V ''x'') (N 5)) (%x. if x = ''x'' then 7 else 0)"
+value "aval (Plus (V ''x'') (N 5)) (\<lambda>x. if x = ''x'' then 7 else 0)"
 
 text {* The same state more concisely: *}
-value "aval (Plus (V ''x'') (N 5)) ((%x. 0) (''x'':= 7))"
+value "aval (Plus (V ''x'') (N 5)) ((\<lambda>x. 0) (''x'':= 7))"
 
 text {* A little syntax magic to write larger states compactly: *}
 
-definition
-  "null_heap \<equiv> \<lambda>x. 0"
+definition null_state ("<>") where
+  "null_state \<equiv> \<lambda>x. 0"
 syntax 
   "_State" :: "updbinds => 'a" ("<_>")
 translations
-  "_State ms" => "_Update (CONST null_heap) ms"
+  "_State ms" => "_Update <> ms"
 
 text {* 
   We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly:
 *}
-lemma "<a := Suc 0, b := 2> = (null_heap (a := Suc 0)) (b := 2)"
+lemma "<a := Suc 0, b := 2> = (<> (a := Suc 0)) (b := 2)"
   by (rule refl)
 
 value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>"
 
+
 text {* Variables that are not mentioned in the state are 0 by default in 
   the @{term "<a := b::int>"} syntax: 
-*}   
+*}
 value "aval (Plus (V ''x'') (N 5)) <''y'' := 7>"
 
+text{* Note that this @{text"<\<dots>>"} syntax works for any function space
+@{text"\<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2"} where @{text "\<tau>\<^isub>2"} has a @{text 0}. *}
+
 
 subsection "Optimization"
 
@@ -71,16 +75,11 @@
 "plus a (N i) = (if i=0 then a else Plus a (N i))" |
 "plus a1 a2 = Plus a1 a2"
 
-code_thms plus
-code_thms plus
-
-(* FIXME: dropping subsumed code eqns?? *)
 lemma aval_plus[simp]:
   "aval (plus a1 a2) s = aval a1 s + aval a2 s"
 apply(induct a1 a2 rule: plus.induct)
 apply simp_all (* just for a change from auto *)
 done
-code_thms plus
 
 fun asimp :: "aexp \<Rightarrow> aexp" where
 "asimp (N n) = N n" |
diff -r 884d27ede438 -r b80108b346a9 src/HOL/IMP/AbsInt0.thy
--- a/src/HOL/IMP/AbsInt0.thy	Tue Sep 13 07:13:49 2011 +0200
+++ b/src/HOL/IMP/AbsInt0.thy	Wed Sep 14 06:49:01 2011 +0200
@@ -32,7 +32,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 = iter_above (AI c) 3 S"
 
 lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
 proof(induct c arbitrary: s t S0)
@@ -47,9 +47,8 @@
     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"
-  have pfp: "AI c ?P \<sqsubseteq> ?P" and "S0 \<sqsubseteq> ?P"
-    by(simp_all add: SL_top_class.pfp_above_pfp)
+  let ?P = "iter_above (AI c) 3 S0"
+  have pfp: "AI c ?P \<sqsubseteq> ?P" and "S0 \<sqsubseteq> ?P" by(simp_all add: iter_above_pfp)
   { 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 884d27ede438 -r b80108b346a9 src/HOL/IMP/AbsInt0_fun.thy
--- a/src/HOL/IMP/AbsInt0_fun.thy	Tue Sep 13 07:13:49 2011 +0200
+++ b/src/HOL/IMP/AbsInt0_fun.thy	Wed Sep 14 06:49:01 2011 +0200
@@ -31,47 +31,45 @@
 lemma join_le_iff[simp]: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
 by (metis join_ge1 join_ge2 join_least le_trans)
 
-fun bpfp where
-"bpfp f 0 _ = Top" |
-"bpfp f (Suc n) x = (if f x \<sqsubseteq> x then x else bpfp f n (f x))"
+fun iter where
+"iter f 0 _ = Top" |
+"iter f (Suc n) x = (if f x \<sqsubseteq> x then x else iter f n (f x))"
 
-definition "pfp f = bpfp f 3"
-
-lemma postfixedpoint: "f(bpfp f n x) \<sqsubseteq> bpfp f n x"
+lemma iter_pfp: "f(iter f n x) \<sqsubseteq> iter f n x"
 apply (induct n arbitrary: x)
  apply (simp)
 apply (simp)
 done
 
-lemma bpfp_funpow: "bpfp f n x \<noteq> Top \<Longrightarrow> EX k. bpfp f n x = (f^^k) x"
+definition "iter_above f n x0 = iter (\<lambda>x. x0 \<squnion> f x) n x0"
+
+lemma iter_above_pfp:
+shows "f(iter_above f n x0) \<sqsubseteq> iter_above f n x0" and "x0 \<sqsubseteq> iter_above f n x0"
+using iter_pfp[of "\<lambda>x. x0 \<squnion> f x"]
+by(auto simp add: iter_above_def)
+
+text{* So much for soundness. But how good an approximation of the post-fixed
+point does @{const iter_above} yield? *}
+
+lemma iter_funpow: "iter f n x \<noteq> Top \<Longrightarrow> EX k. iter f n x = (f^^k) x"
 apply(induct n arbitrary: x)
-apply simp
-apply simp
+ apply simp
 apply (auto)
 apply(rule_tac x=0 in exI)
 apply simp
 by (metis funpow.simps(2) funpow_swap1 o_apply)
 
-lemma pfp_funpow: "pfp f x \<noteq> Top \<Longrightarrow> EX k. pfp f x = (f^^k) x"
-by(simp add: pfp_def bpfp_funpow)
-
-abbreviation (input) lift (infix "\<up>" 65) where "f\<up>x0 == (%x. x0 \<squnion> f x)"
-
-definition "pfp_above f x0 = pfp (f\<up>x0) x0"
+text{* For monotone @{text f}, @{term "iter_above f n x0"} yields the least
+post-fixed point above @{text x0}, unless it yields @{text Top}. *}
 
-lemma pfp_above_pfp:
-shows "f(pfp_above f x0) \<sqsubseteq> pfp_above f x0" and "x0 \<sqsubseteq> pfp_above f x0"
-using postfixedpoint[of "lift f x0"]
-by(auto simp add: pfp_above_def pfp_def)
-
-lemma least_pfp:
-assumes mono: "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "pfp_above f x0 \<noteq> Top"
-and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "pfp_above f x0 \<sqsubseteq> p"
+lemma iter_least_pfp:
+assumes mono: "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter_above f n x0 \<noteq> Top"
+and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "iter_above f n x0 \<sqsubseteq> p"
 proof-
-  let ?F = "lift f x0"
-  obtain k where "pfp_above f x0 = (?F^^k) x0"
-    using pfp_funpow `pfp_above f x0 \<noteq> Top`
-    by(fastforce simp add: pfp_above_def)
+  let ?F = "\<lambda>x. x0 \<squnion> f x"
+  obtain k where "iter_above f n x0 = (?F^^k) x0"
+    using iter_funpow `iter_above f n x0 \<noteq> Top`
+    by(fastforce simp add: iter_above_def)
   moreover
   { fix n have "(?F^^n) x0 \<sqsubseteq> p"
     proof(induct n)
@@ -84,20 +82,20 @@
 qed
 
 lemma chain: assumes "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
-shows "((f\<up>x0)^^i) x0 \<sqsubseteq> ((f\<up>x0)^^(i+1)) x0"
+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 pfp_almost_fp:
-assumes mono: "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "pfp_above f x0 \<noteq> Top"
-shows "pfp_above f x0 \<sqsubseteq> x0 \<squnion> f(pfp_above f x0)"
+lemma iter_above_almost_fp:
+assumes mono: "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter_above f n x0 \<noteq> Top"
+shows "iter_above f n x0 \<sqsubseteq> x0 \<squnion> f(iter_above f n x0)"
 proof-
-  let ?p = "pfp_above f x0"
-  obtain k where 1: "?p = ((f\<up>x0)^^k) x0"
-    using pfp_funpow `?p \<noteq> Top`
-    by(fastforce simp add: pfp_above_def)
+  let ?p = "iter_above f n 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
 
@@ -157,7 +155,7 @@
 "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
 
 abbreviation fun_in_rep (infix "<:" 50) where
-"f <: F == ALL x. f x <: F x"
+"f <: F == \<forall>x. f x <: F x"
 
 lemma fun_in_rep_le: "(s::state) <: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <: T"
 by (metis le_fun_def le_rep subsetD)
@@ -170,7 +168,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 = iter_above (AI c) 3 S"
 
 lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
 proof(induct c arbitrary: s t S0)
@@ -183,14 +181,13 @@
   case If thus ?case by(auto simp: in_rep_join)
 next
   case (While b c)
-  let ?P = "pfp_above (AI c) S0"
-  have pfp: "AI c ?P \<sqsubseteq> ?P" and "S0 \<sqsubseteq> ?P"
-    by(simp_all add: SL_top_class.pfp_above_pfp)
+  let ?P = "iter_above (AI c) 3 S0"
+  have pfp: "AI c ?P \<sqsubseteq> ?P" and "S0 \<sqsubseteq> ?P" by (simp_all add: iter_above_pfp)
   { 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
     next
-      case WhileTrue thus ?case using While.hyps pfp fun_in_rep_le by metis
+      case WhileTrue thus ?case by(metis While.hyps pfp fun_in_rep_le)
     qed
   }
   with fun_in_rep_le[OF `s <: S0` `S0 \<sqsubseteq> ?P`]
@@ -204,10 +201,4 @@
 i.e. functions, in the post-fixedpoint computation. Need to implement
 abstract states concretely. *}
 
-
-(* Exercises: show that <= is a preorder if
-1. v1 <= v2  =  rep v1 <= rep v2
-2. v1 <= v2  =  ALL x. lookup v1 x <= lookup v2 x
-*)
-
 end
diff -r 884d27ede438 -r b80108b346a9 src/HOL/IMP/AbsInt1.thy
--- a/src/HOL/IMP/AbsInt1.thy	Tue Sep 13 07:13:49 2011 +0200
+++ b/src/HOL/IMP/AbsInt1.thy	Wed Sep 14 06:49:01 2011 +0200
@@ -167,7 +167,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 (%S. AI c (bfilter b True S)) S)"
+  bfilter b False (iter_above (\<lambda>S. AI c (bfilter b True S)) 3 S)"
 
 lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <:: S \<Longrightarrow> t <:: AI c S"
 proof(induct c arbitrary: s t S)
@@ -181,9 +181,9 @@
   case If thus ?case by (auto simp: in_rep_join_UpI bfilter_sound)
 next
   case (While b c)
-  let ?P = "pfp_above (%S. AI c (bfilter b True S)) S"
+  let ?P = "iter_above (\<lambda>S. AI c (bfilter b True S)) 3 S"
   have pfp: "AI c (bfilter b True ?P) \<sqsubseteq> ?P" and "S \<sqsubseteq> ?P"
-    by (rule pfp_above_pfp(1), rule pfp_above_pfp(2))
+    by (rule iter_above_pfp(1), rule iter_above_pfp(2))
   { fix s t
     have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <:: ?P \<Longrightarrow>
           t <:: bfilter b False ?P"
@@ -200,20 +200,6 @@
   show ?case by simp
 qed
 
-text{* Exercise: *}
-
-lemma afilter_strict: "afilter e res bot = bot"
-by (induct e arbitrary: res) simp_all
-
-lemma bfilter_strict: "bfilter b res bot = bot"
-by (induct b arbitrary: res) (simp_all add: afilter_strict)
-
-lemma pfp_strict: "f bot = bot \<Longrightarrow> pfp_above f bot = bot"
-by(simp add: pfp_above_def pfp_def eval_nat_numeral)
-
-lemma AI_strict: "AI c bot = bot"
-by(induct c) (simp_all add: bfilter_strict pfp_strict)
-
 end
 
 end
diff -r 884d27ede438 -r b80108b346a9 src/HOL/IMP/AbsInt1_ivl.thy
--- a/src/HOL/IMP/AbsInt1_ivl.thy	Tue Sep 13 07:13:49 2011 +0200
+++ b/src/HOL/IMP/AbsInt1_ivl.thy	Wed Sep 14 06:49:01 2011 +0200
@@ -153,7 +153,7 @@
     by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
 qed
 
-interpretation Val_abs rep_ivl "%n. I (Some n) (Some n)" plus_ivl
+interpretation Val_abs rep_ivl "\<lambda>n. I (Some n) (Some n)" plus_ivl
 proof
   case goal1 thus ?case by(simp add: rep_ivl_def)
 next
@@ -169,7 +169,7 @@
   case goal2 show ?case by(auto simp add: Bot_ivl_def rep_ivl_def empty_def)
 qed
 
-interpretation Val_abs1 rep_ivl "%n. I (Some n) (Some n)" plus_ivl inv_plus_ivl inv_less_ivl
+interpretation Val_abs1 rep_ivl "\<lambda>n. I (Some n) (Some n)" plus_ivl inv_plus_ivl inv_less_ivl
 proof
   case goal1 thus ?case
     by(auto simp add: inv_plus_ivl_def)
@@ -180,7 +180,7 @@
       auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
 qed
 
-interpretation Abs_Int1 rep_ivl "%n. I (Some n) (Some n)" plus_ivl inv_plus_ivl inv_less_ivl
+interpretation Abs_Int1 rep_ivl "\<lambda>n. I (Some n) (Some n)" plus_ivl inv_plus_ivl inv_less_ivl
 defines afilter_ivl is afilter
 and bfilter_ivl is bfilter
 and AI_ivl is AI
diff -r 884d27ede438 -r b80108b346a9 src/HOL/IMP/Astate.thy
--- a/src/HOL/IMP/Astate.thy	Tue Sep 13 07:13:49 2011 +0200
+++ b/src/HOL/IMP/Astate.thy	Wed Sep 14 06:49:01 2011 +0200
@@ -30,9 +30,9 @@
 
 definition
 "join_astate F G =
- FunDom (%x. fun F x \<squnion> fun G x) ([x\<leftarrow>dom F. x : set(dom G)])"
+ FunDom (\<lambda>x. fun F x \<squnion> fun G x) ([x\<leftarrow>dom F. x : set(dom G)])"
 
-definition "Top = FunDom (%x. Top) []"
+definition "Top = FunDom (\<lambda>x. Top) []"
 
 instance
 proof
diff -r 884d27ede438 -r b80108b346a9 src/HOL/IMP/Big_Step.thy
--- a/src/HOL/IMP/Big_Step.thy	Tue Sep 13 07:13:49 2011 +0200
+++ b/src/HOL/IMP/Big_Step.thy	Wed Sep 14 06:49:01 2011 +0200
@@ -37,7 +37,7 @@
 text{* For inductive definitions we need command
        \texttt{values} instead of \texttt{value}. *}
 
-values "{t. (SKIP, %_. 0) \<Rightarrow> t}"
+values "{t. (SKIP, \<lambda>_. 0) \<Rightarrow> t}"
 
 text{* We need to translate the result state into a list
 to display it. *}
diff -r 884d27ede438 -r b80108b346a9 src/HOL/IMP/Live.thy
--- a/src/HOL/IMP/Live.thy	Tue Sep 13 07:13:49 2011 +0200
+++ b/src/HOL/IMP/Live.thy	Wed Sep 14 06:49:01 2011 +0200
@@ -153,7 +153,6 @@
     where "(bury ?w X,t2) \<Rightarrow> t3" "s3 = t3 on X"
     by auto
   with `bval b t1` `(bury c (L ?w X), t1) \<Rightarrow> t2` show ?case by auto
-    (* FIXME why does s/h fail here? *)
 qed
 
 corollary final_bury_sound: "(c,s) \<Rightarrow> s' \<Longrightarrow> (bury c UNIV,s) \<Rightarrow> s'"
diff -r 884d27ede438 -r b80108b346a9 src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy
--- a/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy	Tue Sep 13 07:13:49 2011 +0200
+++ b/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy	Wed Sep 14 06:49:01 2011 +0200
@@ -31,10 +31,9 @@
 
 code_pred big_step .
 
-(* FIXME: example state syntax *)
 values "{map t [''x'',''y'',''z''] |t. 
-          (\<lambda>p. SKIP) \<turnstile> (CALL ''p'', (%_. 0)(''x'' := 42, ''y'' := 43)) \<Rightarrow> t}"
+          (\<lambda>p. SKIP) \<turnstile> (CALL ''p'', <''x'' := 42, ''y'' := 43>) \<Rightarrow> t}"
 
-values "{map t [''x'',''y'',''z''] |t. (\<lambda>p. SKIP) \<turnstile> (test_com, (%_. 0)) \<Rightarrow> t}"
+values "{map t [''x'',''y'',''z''] |t. (\<lambda>p. SKIP) \<turnstile> (test_com, <>) \<Rightarrow> t}"
 
 end
diff -r 884d27ede438 -r b80108b346a9 src/HOL/IMP/Procs_Stat_Vars_Dyn.thy
--- a/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy	Tue Sep 13 07:13:49 2011 +0200
+++ b/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy	Wed Sep 14 06:49:01 2011 +0200
@@ -33,11 +33,9 @@
 
 code_pred big_step .
 
+values "{map t [''x'', ''y'', ''z''] |t. 
+            [] \<turnstile> (CALL ''p'', <''x'' := 42, ''y'' := 43>) \<Rightarrow> t}"
 
-(* FIXME: example state syntax *)
-values "{map t [''x'', ''y'', ''z''] |t. 
-            [] \<turnstile> (CALL ''p'', (%_. 0)(''x'' := 42, ''y'' := 43)) \<Rightarrow> t}"
-
-values "{map t [''x'', ''y'', ''z''] |t. [] \<turnstile> (test_com, (%_. 0) ) \<Rightarrow> t}"
+values "{map t [''x'', ''y'', ''z''] |t. [] \<turnstile> (test_com, <>) \<Rightarrow> t}"
 
 end
diff -r 884d27ede438 -r b80108b346a9 src/HOL/IMP/Procs_Stat_Vars_Stat.thy
--- a/src/HOL/IMP/Procs_Stat_Vars_Stat.thy	Tue Sep 13 07:13:49 2011 +0200
+++ b/src/HOL/IMP/Procs_Stat_Vars_Stat.thy	Wed Sep 14 06:49:01 2011 +0200
@@ -44,10 +44,11 @@
 
 code_pred big_step .
 
-values "{map t [0,1] |t. ([], \<lambda>n. 0, 0) \<turnstile> (CALL ''p'', nth [42, 43]) \<Rightarrow> t}"
+
+values "{map t [0,1] |t. ([], <>, 0) \<turnstile> (CALL ''p'', nth [42, 43]) \<Rightarrow> t}"
 
-(* FIXME: syntax *)
-values "{map t [0, 1, 2] |t. ([], (\<lambda>_. 3)(''x'' := 0, ''y'' := 1,''z'' := 2), 0) \<turnstile> (test_com, (%_. 0)) \<Rightarrow> t}"
-
+values "{map t [0, 1, 2] |t.
+  ([], <''x'' := 0, ''y'' := 1,''z'' := 2>, 0)
+  \<turnstile> (test_com, <>) \<Rightarrow> t}"
 
 end