1.1 --- a/src/HOL/IMP/AExp.thy	Fri Aug 05 14:16:44 2011 +0200
     1.2 +++ b/src/HOL/IMP/AExp.thy	Thu Aug 04 16:49:57 2011 +0200
     1.3 @@ -23,40 +23,25 @@
     1.4  
     1.5  text {* A little syntax magic to write larger states compactly: *}
     1.6  
     1.7 -nonterminal funlets and funlet
     1.8 -
     1.9 -syntax
    1.10 -  "_funlet"  :: "['a, 'a] => funlet"             ("_ /->/ _")
    1.11 -   ""         :: "funlet => funlets"             ("_")
    1.12 -  "_Funlets" :: "[funlet, funlets] => funlets"   ("_,/ _")
    1.13 -  "_Fun"     :: "funlets => 'a => 'b"            ("(1[_])")
    1.14 -  "_FunUpd"  :: "['a => 'b, funlets] => 'a => 'b" ("_/'(_')" [900,0]900)
    1.15 -
    1.16 -syntax (xsymbols)
    1.17 -  "_funlet"  :: "['a, 'a] => funlet"             ("_ /\<rightarrow>/ _")
    1.18 -
    1.19  definition
    1.20    "null_heap \<equiv> \<lambda>x. 0"
    1.21 -
    1.22 +syntax 
    1.23 +  "_State" :: "updbinds => 'a" ("<_>")
    1.24  translations
    1.25 -  "_FunUpd m (_Funlets xy ms)"  == "_FunUpd (_FunUpd m xy) ms"
    1.26 -  "_FunUpd m (_funlet  x y)"    == "m(x := y)"
    1.27 -  "_Fun ms"                     == "_FunUpd (CONST null_heap) ms"
    1.28 -  "_Fun (_Funlets ms1 ms2)"     <= "_FunUpd (_Fun ms1) ms2"
    1.29 -  "_Funlets ms1 (_Funlets ms2 ms3)" <= "_Funlets (_Funlets ms1 ms2) ms3"
    1.30 +  "_State ms" => "_Update (CONST null_heap) ms"
    1.31  
    1.32  text {* 
    1.33    We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly:
    1.34  *}
    1.35 -lemma "[a \<rightarrow> Suc 0, b \<rightarrow> 2] = (null_heap (a := Suc 0)) (b := 2)"
    1.36 +lemma "<a := Suc 0, b := 2> = (null_heap (a := Suc 0)) (b := 2)"
    1.37    by (rule refl)
    1.38  
    1.39 -value "aval (Plus (V ''x'') (N 5)) [''x'' \<rightarrow> 7]"
    1.40 +value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>"
    1.41  
    1.42  text {* Variables that are not mentioned in the state are 0 by default in 
    1.43 -  the @{term "[a \<rightarrow> b::int]"} syntax: 
    1.44 +  the @{term "<a := b::int>"} syntax: 
    1.45  *}   
    1.46 -value "aval (Plus (V ''x'') (N 5)) [''y'' \<rightarrow> 7]"
    1.47 +value "aval (Plus (V ''x'') (N 5)) <''y'' := 7>"
    1.48  
    1.49  
    1.50  subsection "Optimization"

     2.1 --- a/src/HOL/IMP/ASM.thy	Fri Aug 05 14:16:44 2011 +0200
     2.2 +++ b/src/HOL/IMP/ASM.thy	Thu Aug 04 16:49:57 2011 +0200
     2.3 @@ -25,7 +25,7 @@
     2.4  "aexec (i#is) s stk = aexec is s (aexec1 i s stk)"
     2.5  
     2.6  value "aexec [LOADI 5, LOAD ''y'', ADD]
     2.7 - [''x'' \<rightarrow> 42, ''y'' \<rightarrow> 43] [50]"
     2.8 + <''x'' := 42, ''y'' := 43> [50]"
     2.9  
    2.10  lemma aexec_append[simp]:
    2.11    "aexec (is1@is2) s stk = aexec is2 s (aexec is1 s stk)"

     3.1 --- a/src/HOL/IMP/BExp.thy	Fri Aug 05 14:16:44 2011 +0200
     3.2 +++ b/src/HOL/IMP/BExp.thy	Thu Aug 04 16:49:57 2011 +0200
     3.3 @@ -11,7 +11,7 @@
     3.4  "bval (Less a1 a2) s = (aval a1 s < aval a2 s)"
     3.5  
     3.6  value "bval (Less (V ''x'') (Plus (N 3) (V ''y'')))
     3.7 -            [''x'' \<rightarrow> 3, ''y'' \<rightarrow> 1]"
     3.8 +            <''x'' := 3, ''y'' := 1>"
     3.9  
    3.10  
    3.11  subsection "Optimization"

     4.1 --- a/src/HOL/IMP/Big_Step.thy	Fri Aug 05 14:16:44 2011 +0200
     4.2 +++ b/src/HOL/IMP/Big_Step.thy	Thu Aug 04 16:49:57 2011 +0200
     4.3 @@ -42,13 +42,13 @@
     4.4  text{* We need to translate the result state into a list
     4.5  to display it. *}
     4.6  
     4.7 -values "{map t [''x''] |t. (SKIP, [''x'' \<rightarrow> 42]) \<Rightarrow> t}"
     4.8 +values "{map t [''x''] |t. (SKIP, <''x'' := 42>) \<Rightarrow> t}"
     4.9  
    4.10 -values "{map t [''x''] |t. (''x'' ::= N 2, [''x'' \<rightarrow> 42]) \<Rightarrow> t}"
    4.11 +values "{map t [''x''] |t. (''x'' ::= N 2, <''x'' := 42>) \<Rightarrow> t}"
    4.12  
    4.13  values "{map t [''x'',''y''] |t.
    4.14    (WHILE Less (V ''x'') (V ''y'') DO (''x'' ::= Plus (V ''x'') (N 5)),
    4.15 -   [''x'' \<rightarrow> 0, ''y'' \<rightarrow> 13]) \<Rightarrow> t}"
    4.16 +   <''x'' := 0, ''y'' := 13>) \<Rightarrow> t}"
    4.17  
    4.18  
    4.19  text{* Proof automation: *}

     5.1 --- a/src/HOL/IMP/Compiler.thy	Fri Aug 05 14:16:44 2011 +0200
     5.2 +++ b/src/HOL/IMP/Compiler.thy	Thu Aug 04 16:49:57 2011 +0200
     5.3 @@ -88,7 +88,7 @@
     5.4  values
     5.5    "{(i,map t [''x'',''y''],stk) | i t stk.
     5.6      [LOAD ''y'', STORE ''x''] \<turnstile>
     5.7 -    (0, [''x'' \<rightarrow> 3, ''y'' \<rightarrow> 4], []) \<rightarrow>* (i,t,stk)}"
     5.8 +    (0, <''x'' := 3, ''y'' := 4>, []) \<rightarrow>* (i,t,stk)}"
     5.9  
    5.10  
    5.11  subsection{* Verification infrastructure *}
    5.12 @@ -112,7 +112,7 @@
    5.13    "ADD \<turnstile>i c \<rightarrow> c' = 
    5.14    (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, (hd2 stk + hd stk) # tl2 stk))"
    5.15    "STORE x \<turnstile>i c \<rightarrow> c' = 
    5.16 -  (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s(x \<rightarrow> hd stk), tl stk))"
    5.17 +  (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s(x := hd stk), tl stk))"
    5.18    "JMP n \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1 + n, s, stk))"
    5.19     "JMPFLESS n \<turnstile>i c \<rightarrow> c' = 
    5.20    (\<exists>i s stk. c = (i, s, stk) \<and> 

     6.1 --- a/src/HOL/IMP/Small_Step.thy	Fri Aug 05 14:16:44 2011 +0200
     6.2 +++ b/src/HOL/IMP/Small_Step.thy	Thu Aug 04 16:49:57 2011 +0200
     6.3 @@ -27,7 +27,7 @@
     6.4  
     6.5  values "{(c',map t [''x'',''y'',''z'']) |c' t.
     6.6     (''x'' ::= V ''z''; ''y'' ::= V ''x'',
     6.7 -    [''x'' \<rightarrow> 3, ''y'' \<rightarrow> 7, ''z'' \<rightarrow> 5]) \<rightarrow>* (c',t)}"
     6.8 +    <''x'' := 3, ''y'' := 7, ''z'' := 5>) \<rightarrow>* (c',t)}"
     6.9  
    6.10  
    6.11  subsection{* Proof infrastructure *}