# HG changeset patch
# User nipkow
# Date 1360751324 -3600
# Node ID faf7f0d4f9eb2b6be547577d5482eedccebd3918
# Parent  3775bf0ea5b884f4c02459a6d7ec0b6e5e92006b
tuned state display

diff -r 3775bf0ea5b8 -r faf7f0d4f9eb src/HOL/IMP/AExp.thy
--- 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:
diff -r 3775bf0ea5b8 -r faf7f0d4f9eb src/HOL/IMP/Collecting_Examples.thy
--- 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)"