# HG changeset patch
# User kleing
# Date 1312469397 -7200
# Node ID d03f9f28d01d4fea055d61f39c2e0e5d679b6f6a
# Parent  322d1657c40c0083db4d053ff92930b7f74290b4
new state syntax with less conflicts

diff -r 322d1657c40c -r d03f9f28d01d src/HOL/IMP/AExp.thy
--- a/src/HOL/IMP/AExp.thy	Fri Aug 05 14:16:44 2011 +0200
+++ b/src/HOL/IMP/AExp.thy	Thu Aug 04 16:49:57 2011 +0200
@@ -23,40 +23,25 @@
 
 text {* A little syntax magic to write larger states compactly: *}
 
-nonterminal funlets and funlet
-
-syntax
-  "_funlet"  :: "['a, 'a] => funlet"             ("_ /->/ _")
-   ""         :: "funlet => funlets"             ("_")
-  "_Funlets" :: "[funlet, funlets] => funlets"   ("_,/ _")
-  "_Fun"     :: "funlets => 'a => 'b"            ("(1[_])")
-  "_FunUpd"  :: "['a => 'b, funlets] => 'a => 'b" ("_/'(_')" [900,0]900)
-
-syntax (xsymbols)
-  "_funlet"  :: "['a, 'a] => funlet"             ("_ /\<rightarrow>/ _")
-
 definition
   "null_heap \<equiv> \<lambda>x. 0"
-
+syntax 
+  "_State" :: "updbinds => 'a" ("<_>")
 translations
-  "_FunUpd m (_Funlets xy ms)"  == "_FunUpd (_FunUpd m xy) ms"
-  "_FunUpd m (_funlet  x y)"    == "m(x := y)"
-  "_Fun ms"                     == "_FunUpd (CONST null_heap) ms"
-  "_Fun (_Funlets ms1 ms2)"     <= "_FunUpd (_Fun ms1) ms2"
-  "_Funlets ms1 (_Funlets ms2 ms3)" <= "_Funlets (_Funlets ms1 ms2) ms3"
+  "_State ms" => "_Update (CONST null_heap) ms"
 
 text {* 
   We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly:
 *}
-lemma "[a \<rightarrow> Suc 0, b \<rightarrow> 2] = (null_heap (a := Suc 0)) (b := 2)"
+lemma "<a := Suc 0, b := 2> = (null_heap (a := Suc 0)) (b := 2)"
   by (rule refl)
 
-value "aval (Plus (V ''x'') (N 5)) [''x'' \<rightarrow> 7]"
+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 \<rightarrow> b::int]"} syntax: 
+  the @{term "<a := b::int>"} syntax: 
 *}   
-value "aval (Plus (V ''x'') (N 5)) [''y'' \<rightarrow> 7]"
+value "aval (Plus (V ''x'') (N 5)) <''y'' := 7>"
 
 
 subsection "Optimization"
diff -r 322d1657c40c -r d03f9f28d01d src/HOL/IMP/ASM.thy
--- a/src/HOL/IMP/ASM.thy	Fri Aug 05 14:16:44 2011 +0200
+++ b/src/HOL/IMP/ASM.thy	Thu Aug 04 16:49:57 2011 +0200
@@ -25,7 +25,7 @@
 "aexec (i#is) s stk = aexec is s (aexec1 i s stk)"
 
 value "aexec [LOADI 5, LOAD ''y'', ADD]
- [''x'' \<rightarrow> 42, ''y'' \<rightarrow> 43] [50]"
+ <''x'' := 42, ''y'' := 43> [50]"
 
 lemma aexec_append[simp]:
   "aexec (is1@is2) s stk = aexec is2 s (aexec is1 s stk)"
diff -r 322d1657c40c -r d03f9f28d01d src/HOL/IMP/BExp.thy
--- a/src/HOL/IMP/BExp.thy	Fri Aug 05 14:16:44 2011 +0200
+++ b/src/HOL/IMP/BExp.thy	Thu Aug 04 16:49:57 2011 +0200
@@ -11,7 +11,7 @@
 "bval (Less a1 a2) s = (aval a1 s < aval a2 s)"
 
 value "bval (Less (V ''x'') (Plus (N 3) (V ''y'')))
-            [''x'' \<rightarrow> 3, ''y'' \<rightarrow> 1]"
+            <''x'' := 3, ''y'' := 1>"
 
 
 subsection "Optimization"
diff -r 322d1657c40c -r d03f9f28d01d src/HOL/IMP/Big_Step.thy
--- a/src/HOL/IMP/Big_Step.thy	Fri Aug 05 14:16:44 2011 +0200
+++ b/src/HOL/IMP/Big_Step.thy	Thu Aug 04 16:49:57 2011 +0200
@@ -42,13 +42,13 @@
 text{* We need to translate the result state into a list
 to display it. *}
 
-values "{map t [''x''] |t. (SKIP, [''x'' \<rightarrow> 42]) \<Rightarrow> t}"
+values "{map t [''x''] |t. (SKIP, <''x'' := 42>) \<Rightarrow> t}"
 
-values "{map t [''x''] |t. (''x'' ::= N 2, [''x'' \<rightarrow> 42]) \<Rightarrow> t}"
+values "{map t [''x''] |t. (''x'' ::= N 2, <''x'' := 42>) \<Rightarrow> t}"
 
 values "{map t [''x'',''y''] |t.
   (WHILE Less (V ''x'') (V ''y'') DO (''x'' ::= Plus (V ''x'') (N 5)),
-   [''x'' \<rightarrow> 0, ''y'' \<rightarrow> 13]) \<Rightarrow> t}"
+   <''x'' := 0, ''y'' := 13>) \<Rightarrow> t}"
 
 
 text{* Proof automation: *}
diff -r 322d1657c40c -r d03f9f28d01d src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Fri Aug 05 14:16:44 2011 +0200
+++ b/src/HOL/IMP/Compiler.thy	Thu Aug 04 16:49:57 2011 +0200
@@ -88,7 +88,7 @@
 values
   "{(i,map t [''x'',''y''],stk) | i t stk.
     [LOAD ''y'', STORE ''x''] \<turnstile>
-    (0, [''x'' \<rightarrow> 3, ''y'' \<rightarrow> 4], []) \<rightarrow>* (i,t,stk)}"
+    (0, <''x'' := 3, ''y'' := 4>, []) \<rightarrow>* (i,t,stk)}"
 
 
 subsection{* Verification infrastructure *}
@@ -112,7 +112,7 @@
   "ADD \<turnstile>i c \<rightarrow> c' = 
   (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, (hd2 stk + hd stk) # tl2 stk))"
   "STORE x \<turnstile>i c \<rightarrow> c' = 
-  (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s(x \<rightarrow> hd stk), tl stk))"
+  (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s(x := hd stk), tl stk))"
   "JMP n \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1 + n, s, stk))"
    "JMPFLESS n \<turnstile>i c \<rightarrow> c' = 
   (\<exists>i s stk. c = (i, s, stk) \<and> 
diff -r 322d1657c40c -r d03f9f28d01d src/HOL/IMP/Small_Step.thy
--- a/src/HOL/IMP/Small_Step.thy	Fri Aug 05 14:16:44 2011 +0200
+++ b/src/HOL/IMP/Small_Step.thy	Thu Aug 04 16:49:57 2011 +0200
@@ -27,7 +27,7 @@
 
 values "{(c',map t [''x'',''y'',''z'']) |c' t.
    (''x'' ::= V ''z''; ''y'' ::= V ''x'',
-    [''x'' \<rightarrow> 3, ''y'' \<rightarrow> 7, ''z'' \<rightarrow> 5]) \<rightarrow>* (c',t)}"
+    <''x'' := 3, ''y'' := 7, ''z'' := 5>) \<rightarrow>* (c',t)}"
 
 
 subsection{* Proof infrastructure *}