--- 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" |
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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. *}
--- 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'"
--- 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
--- 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
--- 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