1.1 --- a/src/HOL/IMP/Collecting_Examples.thy	Wed Mar 27 22:36:03 2013 +0100
     1.2 +++ b/src/HOL/IMP/Collecting_Examples.thy	Thu Mar 28 15:45:08 2013 +0100
     1.3 @@ -1,46 +1,66 @@
     1.4  theory Collecting_Examples
     1.5 -imports Collecting
     1.6 +imports Collecting Vars
     1.7  begin
     1.8  
     1.9 +subsection "Pretty printing state sets"
    1.10 +
    1.11  text{* Tweak code generation to work with sets of non-equality types: *}
    1.12  declare insert_code[code del] union_coset_filter[code del]
    1.13  lemma insert_code [code]:  "insert x (set xs) = set (x#xs)"
    1.14  by simp
    1.15  
    1.16 -text{* In order to display commands annotated with state sets,
    1.17 -states must be translated into a printable format as sets of pairs,
    1.18 -for a given set of variable names. This is what @{text show_acom} does: *}
    1.19 +text{* Collect variables in acom: *}
    1.20 +fun cvars :: "'a acom \<Rightarrow> vname set" where
    1.21 +"cvars (SKIP {P})= {}" |
    1.22 +"cvars (x::=e {P}) = {x} \<union> vars e" |
    1.23 +"cvars (c1;c2) = cvars c1 \<union> cvars c2" |
    1.24 +"cvars (IF b THEN {P1} c1 ELSE {P2} c2 {Q}) = vars b \<union> cvars c1 \<union> cvars c2" |
    1.25 +"cvars ({I} WHILE b DO {P} c {Q}) = vars b \<union> cvars c"
    1.26 +
    1.27 +text{* Compensate for the fact that sets may now have duplicates: *}
    1.28 +definition compact :: "'a set \<Rightarrow> 'a set" where
    1.29 +"compact X = X"
    1.30 +
    1.31 +lemma [code]: "compact(set xs) = set(remdups xs)"
    1.32 +by(simp add: compact_def)
    1.33 +
    1.34 +definition "vars_acom = compact o cvars"
    1.35 +
    1.36 +text{* In order to display commands annotated with state sets, states must be
    1.37 +translated into a printable format as sets of variable-state pairs, for the
    1.38 +variables in the command: *}
    1.39  
    1.40  definition show_acom ::
    1.41 -  "vname set \<Rightarrow> state set acom \<Rightarrow> (vname*val)set set acom" where
    1.42 -"show_acom X = map_acom (\<lambda>S. (\<lambda>s. (\<lambda>x. (x, s x)) ` X) ` S)"
    1.43 +  "state set acom \<Rightarrow> (vname*val)set set acom" where
    1.44 +"show_acom C = map_acom (\<lambda>S. (\<lambda>s. (\<lambda>x. (x, s x)) ` (vars_acom C)) ` S) C"
    1.45  
    1.46  
    1.47 -text{* The example: *}
    1.48 -definition "c = WHILE Less (V ''x'') (N 3)
    1.49 +subsection "Examples"
    1.50 +
    1.51 +definition "c0 = WHILE Less (V ''x'') (N 3)
    1.52                  DO ''x'' ::= Plus (V ''x'') (N 2)"
    1.53 -definition C0 :: "state set acom" where "C0 = anno {} c"
    1.54 +definition C0 :: "state set acom" where "C0 = anno {} c0"
    1.55  
    1.56  text{* Collecting semantics: *}
    1.57  
    1.58 -value "show_acom {''x''} (((step {<>}) ^^ 1) C0)"
    1.59 -value "show_acom {''x''} (((step {<>}) ^^ 2) C0)"
    1.60 -value "show_acom {''x''} (((step {<>}) ^^ 3) C0)"
    1.61 -value "show_acom {''x''} (((step {<>}) ^^ 4) C0)"
    1.62 -value "show_acom {''x''} (((step {<>}) ^^ 5) C0)"
    1.63 -value "show_acom {''x''} (((step {<>}) ^^ 6) C0)"
    1.64 -value "show_acom {''x''} (((step {<>}) ^^ 7) C0)"
    1.65 -value "show_acom {''x''} (((step {<>}) ^^ 8) C0)"
    1.66 +value "show_acom (((step {<>}) ^^ 1) C0)"
    1.67 +value "show_acom (((step {<>}) ^^ 2) C0)"
    1.68 +value "show_acom (((step {<>}) ^^ 3) C0)"
    1.69 +value "show_acom (((step {<>}) ^^ 4) C0)"
    1.70 +value "show_acom (((step {<>}) ^^ 5) C0)"
    1.71 +value "show_acom (((step {<>}) ^^ 6) C0)"
    1.72 +value "show_acom (((step {<>}) ^^ 7) C0)"
    1.73 +value "show_acom (((step {<>}) ^^ 8) C0)"
    1.74  
    1.75  text{* Small-step semantics: *}
    1.76 -value "show_acom {''x''} (((step {}) ^^ 0) (step {<>} C0))"
    1.77 -value "show_acom {''x''} (((step {}) ^^ 1) (step {<>} C0))"
    1.78 -value "show_acom {''x''} (((step {}) ^^ 2) (step {<>} C0))"
    1.79 -value "show_acom {''x''} (((step {}) ^^ 3) (step {<>} C0))"
    1.80 -value "show_acom {''x''} (((step {}) ^^ 4) (step {<>} C0))"
    1.81 -value "show_acom {''x''} (((step {}) ^^ 5) (step {<>} C0))"
    1.82 -value "show_acom {''x''} (((step {}) ^^ 6) (step {<>} C0))"
    1.83 -value "show_acom {''x''} (((step {}) ^^ 7) (step {<>} C0))"
    1.84 -value "show_acom {''x''} (((step {}) ^^ 8) (step {<>} C0))"
    1.85 +value "show_acom (((step {}) ^^ 0) (step {<>} C0))"
    1.86 +value "show_acom (((step {}) ^^ 1) (step {<>} C0))"
    1.87 +value "show_acom (((step {}) ^^ 2) (step {<>} C0))"
    1.88 +value "show_acom (((step {}) ^^ 3) (step {<>} C0))"
    1.89 +value "show_acom (((step {}) ^^ 4) (step {<>} C0))"
    1.90 +value "show_acom (((step {}) ^^ 5) (step {<>} C0))"
    1.91 +value "show_acom (((step {}) ^^ 6) (step {<>} C0))"
    1.92 +value "show_acom (((step {}) ^^ 7) (step {<>} C0))"
    1.93 +value "show_acom (((step {}) ^^ 8) (step {<>} C0))"
    1.94  
    1.95  end