--- a/src/HOL/IMP/AExp.thy Wed Feb 13 09:04:47 2013 +0100
+++ b/src/HOL/IMP/AExp.thy Wed Feb 13 11:28:44 2013 +0100
@@ -32,7 +32,7 @@
syntax
"_State" :: "updbinds => 'a" ("<_>")
translations
- "_State ms" => "_Update <> ms"
+ "_State ms" == "_Update <> ms"
text {* \noindent
We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly:
--- a/src/HOL/IMP/Collecting_Examples.thy Wed Feb 13 09:04:47 2013 +0100
+++ b/src/HOL/IMP/Collecting_Examples.thy Wed Feb 13 11:28:44 2013 +0100
@@ -7,13 +7,20 @@
lemma insert_code [code]: "insert x (set xs) = set (x#xs)"
by simp
+text{* In order to display commands annotated with state sets,
+states must be translated into a printable format as lists of pairs,
+for a given set of variable names. This is what @{text show_acom} does: *}
+
+definition show_acom ::
+ "vname list \<Rightarrow> state set acom \<Rightarrow> (vname*val)list set acom" where
+"show_acom xs = map_acom (\<lambda>S. (\<lambda>s. map (\<lambda>x. (x, s x)) xs) ` S)"
+
+
text{* The example: *}
definition "c = WHILE Less (V ''x'') (N 3)
DO ''x'' ::= Plus (V ''x'') (N 2)"
definition C0 :: "state set acom" where "C0 = anno {} c"
-definition "show_acom xs = map_acom (\<lambda>S. (\<lambda>s. [(x,s x). x \<leftarrow> xs]) ` S)"
-
text{* Collecting semantics: *}
value "show_acom [''x''] (((step {<>}) ^^ 1) C0)"