# HG changeset patch
# User nipkow
# Date 1344677465 -7200
# Node ID fb1ed5230abcbf4ec87b52e122e91021065cfbd1
# Parent  4fe0920d5049effa6fd61cf648338084542ff780
special code with lists no longer necessary, use sets

diff -r 4fe0920d5049 -r fb1ed5230abc src/HOL/IMP/Collecting_Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Collecting_Examples.thy	Sat Aug 11 11:31:05 2012 +0200
@@ -0,0 +1,40 @@
+theory Collecting_Examples
+imports Collecting
+begin
+
+text{* Tweak code generation to work with sets of non-equality types: *}
+declare insert_code[code del] union_coset_filter[code del]
+lemma insert_code [code]:  "insert x (set xs) = set (x#xs)"
+by simp
+
+text{* Make assignment rule executable: *}
+declare step.simps(2)[code del]
+lemma [code]: "step S (x ::= e {P}) = (x ::= e {(%s. s(x := aval e s)) ` S})"
+by auto
+declare step.simps(1,3-)[code]
+
+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. show_state xs ` S)"
+
+text{* Collecting semantics: *}
+value "show_acom [''x''] (((step {%x. 0}) ^^ 1) c0)"
+value "show_acom [''x''] (((step {%x. 0}) ^^ 2) c0)"
+value "show_acom [''x''] (((step {%x. 0}) ^^ 3) c0)"
+value "show_acom [''x''] (((step {%x. 0}) ^^ 4) c0)"
+value "show_acom [''x''] (((step {%x. 0}) ^^ 5) c0)"
+value "show_acom [''x''] (((step {%x. 0}) ^^ 6) c0)"
+
+text{* Small-step semantics: *}
+value "show_acom [''x''] (((step {}) ^^ 0) (step {%x. 0} c0))"
+value "show_acom [''x''] (((step {}) ^^ 1) (step {%x. 0} c0))"
+value "show_acom [''x''] (((step {}) ^^ 2) (step {%x. 0} c0))"
+value "show_acom [''x''] (((step {}) ^^ 3) (step {%x. 0} c0))"
+value "show_acom [''x''] (((step {}) ^^ 4) (step {%x. 0} c0))"
+value "show_acom [''x''] (((step {}) ^^ 5) (step {%x. 0} c0))"
+
+
+end
diff -r 4fe0920d5049 -r fb1ed5230abc src/HOL/IMP/Collecting_list.thy
--- a/src/HOL/IMP/Collecting_list.thy	Fri Aug 10 22:25:45 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-theory Collecting_list
-imports ACom
-begin
-
-subsection "Executable Collecting Semantics on lists"
-
-fun step :: "state list \<Rightarrow> state list acom \<Rightarrow> state list acom" where
-"step S (SKIP {P}) = (SKIP {S})" |
-"step S (x ::= e {P}) =
-  (x ::= e {[s(x := aval e s). s \<leftarrow> S]})" |
-"step S (c1; c2) = step S c1; step (post c1) c2" |
-"step S (IF b THEN c1 ELSE c2 {P}) =
-   IF b THEN step [s \<leftarrow> S. bval b s] c1 ELSE step [s\<leftarrow>S. \<not> bval b s] c2
-   {post c1 @ post c2}" |
-"step S ({Inv} WHILE b DO c {P}) =
-  {S @ post c} WHILE b DO (step [s\<leftarrow>Inv. bval b s] c) {[s\<leftarrow>Inv. \<not> bval b s]}"
-
-
-text{* Examples: *}
-
-definition "c = WHILE Less (V ''x'') (N 3)
-                DO ''x'' ::= Plus (V ''x'') (N 2)"
-definition "c0 = anno [] c"
-
-definition "show_acom xs = map_acom (map (show_state xs))"
-
-
-text{* Collecting semantics: *}
-
-value "show_acom [''x''] (((step [<>]) ^^ 6) c0)"
-
-
-text{* Small step semantics: *}
-
-value "show_acom [''x''] (((step []) ^^ 5) (step [<>] c0))"
-
-end
diff -r 4fe0920d5049 -r fb1ed5230abc src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Aug 10 22:25:45 2012 +0200
+++ b/src/HOL/ROOT	Sat Aug 11 11:31:05 2012 +0200
@@ -92,7 +92,7 @@
     VC
     HoareT
     Collecting1
-    Collecting_list
+    Collecting_Examples
     Abs_Int_Tests
     Abs_Int1_parity
     Abs_Int1_const