48765
|
1 |
theory Collecting_Examples
|
51566
|
2 |
imports Collecting Vars
|
48765
|
3 |
begin
|
|
4 |
|
51566
|
5 |
subsection "Pretty printing state sets"
|
|
6 |
|
48765
|
7 |
text{* Tweak code generation to work with sets of non-equality types: *}
|
|
8 |
declare insert_code[code del] union_coset_filter[code del]
|
|
9 |
lemma insert_code [code]: "insert x (set xs) = set (x#xs)"
|
|
10 |
by simp
|
|
11 |
|
51566
|
12 |
text{* Collect variables in acom: *}
|
|
13 |
fun cvars :: "'a acom \<Rightarrow> vname set" where
|
|
14 |
"cvars (SKIP {P})= {}" |
|
|
15 |
"cvars (x::=e {P}) = {x} \<union> vars e" |
|
|
16 |
"cvars (c1;c2) = cvars c1 \<union> cvars c2" |
|
|
17 |
"cvars (IF b THEN {P1} c1 ELSE {P2} c2 {Q}) = vars b \<union> cvars c1 \<union> cvars c2" |
|
|
18 |
"cvars ({I} WHILE b DO {P} c {Q}) = vars b \<union> cvars c"
|
|
19 |
|
|
20 |
text{* Compensate for the fact that sets may now have duplicates: *}
|
|
21 |
definition compact :: "'a set \<Rightarrow> 'a set" where
|
|
22 |
"compact X = X"
|
|
23 |
|
|
24 |
lemma [code]: "compact(set xs) = set(remdups xs)"
|
|
25 |
by(simp add: compact_def)
|
|
26 |
|
|
27 |
definition "vars_acom = compact o cvars"
|
|
28 |
|
|
29 |
text{* In order to display commands annotated with state sets, states must be
|
|
30 |
translated into a printable format as sets of variable-state pairs, for the
|
|
31 |
variables in the command: *}
|
51040
|
32 |
|
|
33 |
definition show_acom ::
|
51566
|
34 |
"state set acom \<Rightarrow> (vname*val)set set acom" where
|
|
35 |
"show_acom C = map_acom (\<lambda>S. (\<lambda>s. (\<lambda>x. (x, s x)) ` (vars_acom C)) ` S) C"
|
51040
|
36 |
|
|
37 |
|
51566
|
38 |
subsection "Examples"
|
|
39 |
|
|
40 |
definition "c0 = WHILE Less (V ''x'') (N 3)
|
48765
|
41 |
DO ''x'' ::= Plus (V ''x'') (N 2)"
|
51566
|
42 |
definition C0 :: "state set acom" where "C0 = anno {} c0"
|
48765
|
43 |
|
|
44 |
text{* Collecting semantics: *}
|
50821
|
45 |
|
51566
|
46 |
value "show_acom (((step {<>}) ^^ 1) C0)"
|
|
47 |
value "show_acom (((step {<>}) ^^ 2) C0)"
|
|
48 |
value "show_acom (((step {<>}) ^^ 3) C0)"
|
|
49 |
value "show_acom (((step {<>}) ^^ 4) C0)"
|
|
50 |
value "show_acom (((step {<>}) ^^ 5) C0)"
|
|
51 |
value "show_acom (((step {<>}) ^^ 6) C0)"
|
|
52 |
value "show_acom (((step {<>}) ^^ 7) C0)"
|
|
53 |
value "show_acom (((step {<>}) ^^ 8) C0)"
|
48765
|
54 |
|
|
55 |
text{* Small-step semantics: *}
|
51566
|
56 |
value "show_acom (((step {}) ^^ 0) (step {<>} C0))"
|
|
57 |
value "show_acom (((step {}) ^^ 1) (step {<>} C0))"
|
|
58 |
value "show_acom (((step {}) ^^ 2) (step {<>} C0))"
|
|
59 |
value "show_acom (((step {}) ^^ 3) (step {<>} C0))"
|
|
60 |
value "show_acom (((step {}) ^^ 4) (step {<>} C0))"
|
|
61 |
value "show_acom (((step {}) ^^ 5) (step {<>} C0))"
|
|
62 |
value "show_acom (((step {}) ^^ 6) (step {<>} C0))"
|
|
63 |
value "show_acom (((step {}) ^^ 7) (step {<>} C0))"
|
|
64 |
value "show_acom (((step {}) ^^ 8) (step {<>} C0))"
|
48765
|
65 |
|
|
66 |
end
|