--- a/src/HOL/IMP/AExp.thy Fri Aug 05 16:55:14 2011 +0200
+++ b/src/HOL/IMP/AExp.thy Fri Aug 05 17:22:28 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"
--- a/src/HOL/IMP/ASM.thy Fri Aug 05 16:55:14 2011 +0200
+++ b/src/HOL/IMP/ASM.thy Fri Aug 05 17:22:28 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)"
--- a/src/HOL/IMP/BExp.thy Fri Aug 05 16:55:14 2011 +0200
+++ b/src/HOL/IMP/BExp.thy Fri Aug 05 17:22:28 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"
--- a/src/HOL/IMP/Big_Step.thy Fri Aug 05 16:55:14 2011 +0200
+++ b/src/HOL/IMP/Big_Step.thy Fri Aug 05 17:22:28 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: *}
--- a/src/HOL/IMP/Compiler.thy Fri Aug 05 16:55:14 2011 +0200
+++ b/src/HOL/IMP/Compiler.thy Fri Aug 05 17:22:28 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>
--- a/src/HOL/IMP/Small_Step.thy Fri Aug 05 16:55:14 2011 +0200
+++ b/src/HOL/IMP/Small_Step.thy Fri Aug 05 17:22:28 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 *}