merged
authornipkow
Wed Sep 14 06:49:24 2011 +0200 (2011-09-14)
changeset 449241a5811bfe837
parent 44922 14f7da460ce8
parent 44923 b80108b346a9
child 44925 1db6baa40b0e
child 44926 de3ed037c9a5
child 44932 7c93ee993cae
merged
     1.1 --- a/src/HOL/IMP/AExp.thy	Tue Sep 13 17:25:19 2011 -0700
     1.2 +++ b/src/HOL/IMP/AExp.thy	Wed Sep 14 06:49:24 2011 +0200
     1.3 @@ -16,33 +16,37 @@
     1.4  "aval (Plus a1 a2) s = aval a1 s + aval a2 s"
     1.5  
     1.6  
     1.7 -value "aval (Plus (V ''x'') (N 5)) (%x. if x = ''x'' then 7 else 0)"
     1.8 +value "aval (Plus (V ''x'') (N 5)) (\<lambda>x. if x = ''x'' then 7 else 0)"
     1.9  
    1.10  text {* The same state more concisely: *}
    1.11 -value "aval (Plus (V ''x'') (N 5)) ((%x. 0) (''x'':= 7))"
    1.12 +value "aval (Plus (V ''x'') (N 5)) ((\<lambda>x. 0) (''x'':= 7))"
    1.13  
    1.14  text {* A little syntax magic to write larger states compactly: *}
    1.15  
    1.16 -definition
    1.17 -  "null_heap \<equiv> \<lambda>x. 0"
    1.18 +definition null_state ("<>") where
    1.19 +  "null_state \<equiv> \<lambda>x. 0"
    1.20  syntax 
    1.21    "_State" :: "updbinds => 'a" ("<_>")
    1.22  translations
    1.23 -  "_State ms" => "_Update (CONST null_heap) ms"
    1.24 +  "_State ms" => "_Update <> ms"
    1.25  
    1.26  text {* 
    1.27    We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly:
    1.28  *}
    1.29 -lemma "<a := Suc 0, b := 2> = (null_heap (a := Suc 0)) (b := 2)"
    1.30 +lemma "<a := Suc 0, b := 2> = (<> (a := Suc 0)) (b := 2)"
    1.31    by (rule refl)
    1.32  
    1.33  value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>"
    1.34  
    1.35 +
    1.36  text {* Variables that are not mentioned in the state are 0 by default in 
    1.37    the @{term "<a := b::int>"} syntax: 
    1.38 -*}   
    1.39 +*}
    1.40  value "aval (Plus (V ''x'') (N 5)) <''y'' := 7>"
    1.41  
    1.42 +text{* Note that this @{text"<\<dots>>"} syntax works for any function space
    1.43 +@{text"\<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2"} where @{text "\<tau>\<^isub>2"} has a @{text 0}. *}
    1.44 +
    1.45  
    1.46  subsection "Optimization"
    1.47  
    1.48 @@ -71,16 +75,11 @@
    1.49  "plus a (N i) = (if i=0 then a else Plus a (N i))" |
    1.50  "plus a1 a2 = Plus a1 a2"
    1.51  
    1.52 -code_thms plus
    1.53 -code_thms plus
    1.54 -
    1.55 -(* FIXME: dropping subsumed code eqns?? *)
    1.56  lemma aval_plus[simp]:
    1.57    "aval (plus a1 a2) s = aval a1 s + aval a2 s"
    1.58  apply(induct a1 a2 rule: plus.induct)
    1.59  apply simp_all (* just for a change from auto *)
    1.60  done
    1.61 -code_thms plus
    1.62  
    1.63  fun asimp :: "aexp \<Rightarrow> aexp" where
    1.64  "asimp (N n) = N n" |
     2.1 --- a/src/HOL/IMP/AbsInt0.thy	Tue Sep 13 17:25:19 2011 -0700
     2.2 +++ b/src/HOL/IMP/AbsInt0.thy	Wed Sep 14 06:49:24 2011 +0200
     2.3 @@ -32,7 +32,7 @@
     2.4  "AI (x ::= a) S = update S x (aval' a S)" |
     2.5  "AI (c1;c2) S = AI c2 (AI c1 S)" |
     2.6  "AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
     2.7 -"AI (WHILE b DO c) S = pfp_above (AI c) S"
     2.8 +"AI (WHILE b DO c) S = iter_above (AI c) 3 S"
     2.9  
    2.10  lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
    2.11  proof(induct c arbitrary: s t S0)
    2.12 @@ -47,9 +47,8 @@
    2.13      by (metis AI.simps(4) IfE astate_in_rep_le join_ge1 join_ge2)
    2.14  next
    2.15    case (While b c)
    2.16 -  let ?P = "pfp_above (AI c) S0"
    2.17 -  have pfp: "AI c ?P \<sqsubseteq> ?P" and "S0 \<sqsubseteq> ?P"
    2.18 -    by(simp_all add: SL_top_class.pfp_above_pfp)
    2.19 +  let ?P = "iter_above (AI c) 3 S0"
    2.20 +  have pfp: "AI c ?P \<sqsubseteq> ?P" and "S0 \<sqsubseteq> ?P" by(simp_all add: iter_above_pfp)
    2.21    { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
    2.22      proof(induct "WHILE b DO c" s t rule: big_step_induct)
    2.23        case WhileFalse thus ?case by simp
     3.1 --- a/src/HOL/IMP/AbsInt0_fun.thy	Tue Sep 13 17:25:19 2011 -0700
     3.2 +++ b/src/HOL/IMP/AbsInt0_fun.thy	Wed Sep 14 06:49:24 2011 +0200
     3.3 @@ -31,47 +31,45 @@
     3.4  lemma join_le_iff[simp]: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
     3.5  by (metis join_ge1 join_ge2 join_least le_trans)
     3.6  
     3.7 -fun bpfp where
     3.8 -"bpfp f 0 _ = Top" |
     3.9 -"bpfp f (Suc n) x = (if f x \<sqsubseteq> x then x else bpfp f n (f x))"
    3.10 +fun iter where
    3.11 +"iter f 0 _ = Top" |
    3.12 +"iter f (Suc n) x = (if f x \<sqsubseteq> x then x else iter f n (f x))"
    3.13  
    3.14 -definition "pfp f = bpfp f 3"
    3.15 -
    3.16 -lemma postfixedpoint: "f(bpfp f n x) \<sqsubseteq> bpfp f n x"
    3.17 +lemma iter_pfp: "f(iter f n x) \<sqsubseteq> iter f n x"
    3.18  apply (induct n arbitrary: x)
    3.19   apply (simp)
    3.20  apply (simp)
    3.21  done
    3.22  
    3.23 -lemma bpfp_funpow: "bpfp f n x \<noteq> Top \<Longrightarrow> EX k. bpfp f n x = (f^^k) x"
    3.24 +definition "iter_above f n x0 = iter (\<lambda>x. x0 \<squnion> f x) n x0"
    3.25 +
    3.26 +lemma iter_above_pfp:
    3.27 +shows "f(iter_above f n x0) \<sqsubseteq> iter_above f n x0" and "x0 \<sqsubseteq> iter_above f n x0"
    3.28 +using iter_pfp[of "\<lambda>x. x0 \<squnion> f x"]
    3.29 +by(auto simp add: iter_above_def)
    3.30 +
    3.31 +text{* So much for soundness. But how good an approximation of the post-fixed
    3.32 +point does @{const iter_above} yield? *}
    3.33 +
    3.34 +lemma iter_funpow: "iter f n x \<noteq> Top \<Longrightarrow> EX k. iter f n x = (f^^k) x"
    3.35  apply(induct n arbitrary: x)
    3.36 -apply simp
    3.37 -apply simp
    3.38 + apply simp
    3.39  apply (auto)
    3.40  apply(rule_tac x=0 in exI)
    3.41  apply simp
    3.42  by (metis funpow.simps(2) funpow_swap1 o_apply)
    3.43  
    3.44 -lemma pfp_funpow: "pfp f x \<noteq> Top \<Longrightarrow> EX k. pfp f x = (f^^k) x"
    3.45 -by(simp add: pfp_def bpfp_funpow)
    3.46 -
    3.47 -abbreviation (input) lift (infix "\<up>" 65) where "f\<up>x0 == (%x. x0 \<squnion> f x)"
    3.48 -
    3.49 -definition "pfp_above f x0 = pfp (f\<up>x0) x0"
    3.50 +text{* For monotone @{text f}, @{term "iter_above f n x0"} yields the least
    3.51 +post-fixed point above @{text x0}, unless it yields @{text Top}. *}
    3.52  
    3.53 -lemma pfp_above_pfp:
    3.54 -shows "f(pfp_above f x0) \<sqsubseteq> pfp_above f x0" and "x0 \<sqsubseteq> pfp_above f x0"
    3.55 -using postfixedpoint[of "lift f x0"]
    3.56 -by(auto simp add: pfp_above_def pfp_def)
    3.57 -
    3.58 -lemma least_pfp:
    3.59 -assumes mono: "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "pfp_above f x0 \<noteq> Top"
    3.60 -and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "pfp_above f x0 \<sqsubseteq> p"
    3.61 +lemma iter_least_pfp:
    3.62 +assumes mono: "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter_above f n x0 \<noteq> Top"
    3.63 +and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "iter_above f n x0 \<sqsubseteq> p"
    3.64  proof-
    3.65 -  let ?F = "lift f x0"
    3.66 -  obtain k where "pfp_above f x0 = (?F^^k) x0"
    3.67 -    using pfp_funpow `pfp_above f x0 \<noteq> Top`
    3.68 -    by(fastforce simp add: pfp_above_def)
    3.69 +  let ?F = "\<lambda>x. x0 \<squnion> f x"
    3.70 +  obtain k where "iter_above f n x0 = (?F^^k) x0"
    3.71 +    using iter_funpow `iter_above f n x0 \<noteq> Top`
    3.72 +    by(fastforce simp add: iter_above_def)
    3.73    moreover
    3.74    { fix n have "(?F^^n) x0 \<sqsubseteq> p"
    3.75      proof(induct n)
    3.76 @@ -84,20 +82,20 @@
    3.77  qed
    3.78  
    3.79  lemma chain: assumes "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
    3.80 -shows "((f\<up>x0)^^i) x0 \<sqsubseteq> ((f\<up>x0)^^(i+1)) x0"
    3.81 +shows "((\<lambda>x. x0 \<squnion> f x)^^i) x0 \<sqsubseteq> ((\<lambda>x. x0 \<squnion> f x)^^(i+1)) x0"
    3.82  apply(induct i)
    3.83   apply simp
    3.84  apply simp
    3.85  by (metis assms join_ge2 le_trans)
    3.86  
    3.87 -lemma pfp_almost_fp:
    3.88 -assumes mono: "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "pfp_above f x0 \<noteq> Top"
    3.89 -shows "pfp_above f x0 \<sqsubseteq> x0 \<squnion> f(pfp_above f x0)"
    3.90 +lemma iter_above_almost_fp:
    3.91 +assumes mono: "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter_above f n x0 \<noteq> Top"
    3.92 +shows "iter_above f n x0 \<sqsubseteq> x0 \<squnion> f(iter_above f n x0)"
    3.93  proof-
    3.94 -  let ?p = "pfp_above f x0"
    3.95 -  obtain k where 1: "?p = ((f\<up>x0)^^k) x0"
    3.96 -    using pfp_funpow `?p \<noteq> Top`
    3.97 -    by(fastforce simp add: pfp_above_def)
    3.98 +  let ?p = "iter_above f n x0"
    3.99 +  obtain k where 1: "?p = ((\<lambda>x. x0 \<squnion> f x)^^k) x0"
   3.100 +    using iter_funpow `?p \<noteq> Top`
   3.101 +    by(fastforce simp add: iter_above_def)
   3.102    thus ?thesis using chain mono by simp
   3.103  qed
   3.104  
   3.105 @@ -157,7 +155,7 @@
   3.106  "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
   3.107  
   3.108  abbreviation fun_in_rep (infix "<:" 50) where
   3.109 -"f <: F == ALL x. f x <: F x"
   3.110 +"f <: F == \<forall>x. f x <: F x"
   3.111  
   3.112  lemma fun_in_rep_le: "(s::state) <: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <: T"
   3.113  by (metis le_fun_def le_rep subsetD)
   3.114 @@ -170,7 +168,7 @@
   3.115  "AI (x ::= a) S = S(x := aval' a S)" |
   3.116  "AI (c1;c2) S = AI c2 (AI c1 S)" |
   3.117  "AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
   3.118 -"AI (WHILE b DO c) S = pfp_above (AI c) S"
   3.119 +"AI (WHILE b DO c) S = iter_above (AI c) 3 S"
   3.120  
   3.121  lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
   3.122  proof(induct c arbitrary: s t S0)
   3.123 @@ -183,14 +181,13 @@
   3.124    case If thus ?case by(auto simp: in_rep_join)
   3.125  next
   3.126    case (While b c)
   3.127 -  let ?P = "pfp_above (AI c) S0"
   3.128 -  have pfp: "AI c ?P \<sqsubseteq> ?P" and "S0 \<sqsubseteq> ?P"
   3.129 -    by(simp_all add: SL_top_class.pfp_above_pfp)
   3.130 +  let ?P = "iter_above (AI c) 3 S0"
   3.131 +  have pfp: "AI c ?P \<sqsubseteq> ?P" and "S0 \<sqsubseteq> ?P" by (simp_all add: iter_above_pfp)
   3.132    { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
   3.133      proof(induct "WHILE b DO c" s t rule: big_step_induct)
   3.134        case WhileFalse thus ?case by simp
   3.135      next
   3.136 -      case WhileTrue thus ?case using While.hyps pfp fun_in_rep_le by metis
   3.137 +      case WhileTrue thus ?case by(metis While.hyps pfp fun_in_rep_le)
   3.138      qed
   3.139    }
   3.140    with fun_in_rep_le[OF `s <: S0` `S0 \<sqsubseteq> ?P`]
   3.141 @@ -204,10 +201,4 @@
   3.142  i.e. functions, in the post-fixedpoint computation. Need to implement
   3.143  abstract states concretely. *}
   3.144  
   3.145 -
   3.146 -(* Exercises: show that <= is a preorder if
   3.147 -1. v1 <= v2  =  rep v1 <= rep v2
   3.148 -2. v1 <= v2  =  ALL x. lookup v1 x <= lookup v2 x
   3.149 -*)
   3.150 -
   3.151  end
     4.1 --- a/src/HOL/IMP/AbsInt1.thy	Tue Sep 13 17:25:19 2011 -0700
     4.2 +++ b/src/HOL/IMP/AbsInt1.thy	Wed Sep 14 06:49:24 2011 +0200
     4.3 @@ -167,7 +167,7 @@
     4.4  "AI (IF b THEN c1 ELSE c2) S =
     4.5    AI c1 (bfilter b True S) \<squnion> AI c2 (bfilter b False S)" |
     4.6  "AI (WHILE b DO c) S =
     4.7 -  bfilter b False (pfp_above (%S. AI c (bfilter b True S)) S)"
     4.8 +  bfilter b False (iter_above (\<lambda>S. AI c (bfilter b True S)) 3 S)"
     4.9  
    4.10  lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <:: S \<Longrightarrow> t <:: AI c S"
    4.11  proof(induct c arbitrary: s t S)
    4.12 @@ -181,9 +181,9 @@
    4.13    case If thus ?case by (auto simp: in_rep_join_UpI bfilter_sound)
    4.14  next
    4.15    case (While b c)
    4.16 -  let ?P = "pfp_above (%S. AI c (bfilter b True S)) S"
    4.17 +  let ?P = "iter_above (\<lambda>S. AI c (bfilter b True S)) 3 S"
    4.18    have pfp: "AI c (bfilter b True ?P) \<sqsubseteq> ?P" and "S \<sqsubseteq> ?P"
    4.19 -    by (rule pfp_above_pfp(1), rule pfp_above_pfp(2))
    4.20 +    by (rule iter_above_pfp(1), rule iter_above_pfp(2))
    4.21    { fix s t
    4.22      have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <:: ?P \<Longrightarrow>
    4.23            t <:: bfilter b False ?P"
    4.24 @@ -200,20 +200,6 @@
    4.25    show ?case by simp
    4.26  qed
    4.27  
    4.28 -text{* Exercise: *}
    4.29 -
    4.30 -lemma afilter_strict: "afilter e res bot = bot"
    4.31 -by (induct e arbitrary: res) simp_all
    4.32 -
    4.33 -lemma bfilter_strict: "bfilter b res bot = bot"
    4.34 -by (induct b arbitrary: res) (simp_all add: afilter_strict)
    4.35 -
    4.36 -lemma pfp_strict: "f bot = bot \<Longrightarrow> pfp_above f bot = bot"
    4.37 -by(simp add: pfp_above_def pfp_def eval_nat_numeral)
    4.38 -
    4.39 -lemma AI_strict: "AI c bot = bot"
    4.40 -by(induct c) (simp_all add: bfilter_strict pfp_strict)
    4.41 -
    4.42  end
    4.43  
    4.44  end
     5.1 --- a/src/HOL/IMP/AbsInt1_ivl.thy	Tue Sep 13 17:25:19 2011 -0700
     5.2 +++ b/src/HOL/IMP/AbsInt1_ivl.thy	Wed Sep 14 06:49:24 2011 +0200
     5.3 @@ -153,7 +153,7 @@
     5.4      by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
     5.5  qed
     5.6  
     5.7 -interpretation Val_abs rep_ivl "%n. I (Some n) (Some n)" plus_ivl
     5.8 +interpretation Val_abs rep_ivl "\<lambda>n. I (Some n) (Some n)" plus_ivl
     5.9  proof
    5.10    case goal1 thus ?case by(simp add: rep_ivl_def)
    5.11  next
    5.12 @@ -169,7 +169,7 @@
    5.13    case goal2 show ?case by(auto simp add: Bot_ivl_def rep_ivl_def empty_def)
    5.14  qed
    5.15  
    5.16 -interpretation Val_abs1 rep_ivl "%n. I (Some n) (Some n)" plus_ivl inv_plus_ivl inv_less_ivl
    5.17 +interpretation Val_abs1 rep_ivl "\<lambda>n. I (Some n) (Some n)" plus_ivl inv_plus_ivl inv_less_ivl
    5.18  proof
    5.19    case goal1 thus ?case
    5.20      by(auto simp add: inv_plus_ivl_def)
    5.21 @@ -180,7 +180,7 @@
    5.22        auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
    5.23  qed
    5.24  
    5.25 -interpretation Abs_Int1 rep_ivl "%n. I (Some n) (Some n)" plus_ivl inv_plus_ivl inv_less_ivl
    5.26 +interpretation Abs_Int1 rep_ivl "\<lambda>n. I (Some n) (Some n)" plus_ivl inv_plus_ivl inv_less_ivl
    5.27  defines afilter_ivl is afilter
    5.28  and bfilter_ivl is bfilter
    5.29  and AI_ivl is AI
     6.1 --- a/src/HOL/IMP/Astate.thy	Tue Sep 13 17:25:19 2011 -0700
     6.2 +++ b/src/HOL/IMP/Astate.thy	Wed Sep 14 06:49:24 2011 +0200
     6.3 @@ -30,9 +30,9 @@
     6.4  
     6.5  definition
     6.6  "join_astate F G =
     6.7 - FunDom (%x. fun F x \<squnion> fun G x) ([x\<leftarrow>dom F. x : set(dom G)])"
     6.8 + FunDom (\<lambda>x. fun F x \<squnion> fun G x) ([x\<leftarrow>dom F. x : set(dom G)])"
     6.9  
    6.10 -definition "Top = FunDom (%x. Top) []"
    6.11 +definition "Top = FunDom (\<lambda>x. Top) []"
    6.12  
    6.13  instance
    6.14  proof
     7.1 --- a/src/HOL/IMP/Big_Step.thy	Tue Sep 13 17:25:19 2011 -0700
     7.2 +++ b/src/HOL/IMP/Big_Step.thy	Wed Sep 14 06:49:24 2011 +0200
     7.3 @@ -37,7 +37,7 @@
     7.4  text{* For inductive definitions we need command
     7.5         \texttt{values} instead of \texttt{value}. *}
     7.6  
     7.7 -values "{t. (SKIP, %_. 0) \<Rightarrow> t}"
     7.8 +values "{t. (SKIP, \<lambda>_. 0) \<Rightarrow> t}"
     7.9  
    7.10  text{* We need to translate the result state into a list
    7.11  to display it. *}
     8.1 --- a/src/HOL/IMP/Live.thy	Tue Sep 13 17:25:19 2011 -0700
     8.2 +++ b/src/HOL/IMP/Live.thy	Wed Sep 14 06:49:24 2011 +0200
     8.3 @@ -153,7 +153,6 @@
     8.4      where "(bury ?w X,t2) \<Rightarrow> t3" "s3 = t3 on X"
     8.5      by auto
     8.6    with `bval b t1` `(bury c (L ?w X), t1) \<Rightarrow> t2` show ?case by auto
     8.7 -    (* FIXME why does s/h fail here? *)
     8.8  qed
     8.9  
    8.10  corollary final_bury_sound: "(c,s) \<Rightarrow> s' \<Longrightarrow> (bury c UNIV,s) \<Rightarrow> s'"
     9.1 --- a/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy	Tue Sep 13 17:25:19 2011 -0700
     9.2 +++ b/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy	Wed Sep 14 06:49:24 2011 +0200
     9.3 @@ -31,10 +31,9 @@
     9.4  
     9.5  code_pred big_step .
     9.6  
     9.7 -(* FIXME: example state syntax *)
     9.8  values "{map t [''x'',''y'',''z''] |t. 
     9.9 -          (\<lambda>p. SKIP) \<turnstile> (CALL ''p'', (%_. 0)(''x'' := 42, ''y'' := 43)) \<Rightarrow> t}"
    9.10 +          (\<lambda>p. SKIP) \<turnstile> (CALL ''p'', <''x'' := 42, ''y'' := 43>) \<Rightarrow> t}"
    9.11  
    9.12 -values "{map t [''x'',''y'',''z''] |t. (\<lambda>p. SKIP) \<turnstile> (test_com, (%_. 0)) \<Rightarrow> t}"
    9.13 +values "{map t [''x'',''y'',''z''] |t. (\<lambda>p. SKIP) \<turnstile> (test_com, <>) \<Rightarrow> t}"
    9.14  
    9.15  end
    10.1 --- a/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy	Tue Sep 13 17:25:19 2011 -0700
    10.2 +++ b/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy	Wed Sep 14 06:49:24 2011 +0200
    10.3 @@ -33,11 +33,9 @@
    10.4  
    10.5  code_pred big_step .
    10.6  
    10.7 +values "{map t [''x'', ''y'', ''z''] |t. 
    10.8 +            [] \<turnstile> (CALL ''p'', <''x'' := 42, ''y'' := 43>) \<Rightarrow> t}"
    10.9  
   10.10 -(* FIXME: example state syntax *)
   10.11 -values "{map t [''x'', ''y'', ''z''] |t. 
   10.12 -            [] \<turnstile> (CALL ''p'', (%_. 0)(''x'' := 42, ''y'' := 43)) \<Rightarrow> t}"
   10.13 -
   10.14 -values "{map t [''x'', ''y'', ''z''] |t. [] \<turnstile> (test_com, (%_. 0) ) \<Rightarrow> t}"
   10.15 +values "{map t [''x'', ''y'', ''z''] |t. [] \<turnstile> (test_com, <>) \<Rightarrow> t}"
   10.16  
   10.17  end
    11.1 --- a/src/HOL/IMP/Procs_Stat_Vars_Stat.thy	Tue Sep 13 17:25:19 2011 -0700
    11.2 +++ b/src/HOL/IMP/Procs_Stat_Vars_Stat.thy	Wed Sep 14 06:49:24 2011 +0200
    11.3 @@ -44,10 +44,11 @@
    11.4  
    11.5  code_pred big_step .
    11.6  
    11.7 -values "{map t [0,1] |t. ([], \<lambda>n. 0, 0) \<turnstile> (CALL ''p'', nth [42, 43]) \<Rightarrow> t}"
    11.8 +
    11.9 +values "{map t [0,1] |t. ([], <>, 0) \<turnstile> (CALL ''p'', nth [42, 43]) \<Rightarrow> t}"
   11.10  
   11.11 -(* FIXME: syntax *)
   11.12 -values "{map t [0, 1, 2] |t. ([], (\<lambda>_. 3)(''x'' := 0, ''y'' := 1,''z'' := 2), 0) \<turnstile> (test_com, (%_. 0)) \<Rightarrow> t}"
   11.13 -
   11.14 +values "{map t [0, 1, 2] |t.
   11.15 +  ([], <''x'' := 0, ''y'' := 1,''z'' := 2>, 0)
   11.16 +  \<turnstile> (test_com, <>) \<Rightarrow> t}"
   11.17  
   11.18  end