author | nipkow |
Mon, 15 Jan 2018 10:46:41 +0100 | |
changeset 67437 | a6bf7167c5e1 |
parent 67406 | 23307fd33906 |
child 68778 | 4566bac4517d |
permissions | -rw-r--r-- |
48765 | 1 |
theory Collecting_Examples |
51566 | 2 |
imports Collecting Vars |
48765 | 3 |
begin |
4 |
||
51566 | 5 |
subsection "Pretty printing state sets" |
6 |
||
67406 | 7 |
text\<open>Tweak code generation to work with sets of non-equality types:\<close> |
48765 | 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 |
||
67406 | 12 |
text\<open>Compensate for the fact that sets may now have duplicates:\<close> |
51566 | 13 |
definition compact :: "'a set \<Rightarrow> 'a set" where |
14 |
"compact X = X" |
|
15 |
||
16 |
lemma [code]: "compact(set xs) = set(remdups xs)" |
|
17 |
by(simp add: compact_def) |
|
18 |
||
51698 | 19 |
definition "vars_acom = compact o vars o strip" |
51566 | 20 |
|
67406 | 21 |
text\<open>In order to display commands annotated with state sets, states must be |
51566 | 22 |
translated into a printable format as sets of variable-state pairs, for the |
67406 | 23 |
variables in the command:\<close> |
51040 | 24 |
|
52019
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51698
diff
changeset
|
25 |
definition show_acom :: "state set acom \<Rightarrow> (vname*val)set set acom" where |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51698
diff
changeset
|
26 |
"show_acom C = |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51698
diff
changeset
|
27 |
annotate (\<lambda>p. (\<lambda>s. (\<lambda>x. (x, s x)) ` (vars_acom C)) ` anno C p) (strip C)" |
51040 | 28 |
|
29 |
||
51566 | 30 |
subsection "Examples" |
31 |
||
32 |
definition "c0 = WHILE Less (V ''x'') (N 3) |
|
48765 | 33 |
DO ''x'' ::= Plus (V ''x'') (N 2)" |
67437 | 34 |
|
35 |
definition C0 :: "state set acom" where "C0 = annotate (\<lambda>p. {}) c0" |
|
48765 | 36 |
|
67406 | 37 |
text\<open>Collecting semantics:\<close> |
50821 | 38 |
|
67437 | 39 |
value "show_acom (((step {<>}) ^^ 0) C0)" |
51566 | 40 |
value "show_acom (((step {<>}) ^^ 1) C0)" |
41 |
value "show_acom (((step {<>}) ^^ 2) C0)" |
|
42 |
value "show_acom (((step {<>}) ^^ 3) C0)" |
|
43 |
value "show_acom (((step {<>}) ^^ 4) C0)" |
|
44 |
value "show_acom (((step {<>}) ^^ 5) C0)" |
|
45 |
value "show_acom (((step {<>}) ^^ 6) C0)" |
|
46 |
value "show_acom (((step {<>}) ^^ 7) C0)" |
|
47 |
value "show_acom (((step {<>}) ^^ 8) C0)" |
|
48765 | 48 |
|
67406 | 49 |
text\<open>Small-step semantics:\<close> |
51566 | 50 |
value "show_acom (((step {}) ^^ 0) (step {<>} C0))" |
51 |
value "show_acom (((step {}) ^^ 1) (step {<>} C0))" |
|
52 |
value "show_acom (((step {}) ^^ 2) (step {<>} C0))" |
|
53 |
value "show_acom (((step {}) ^^ 3) (step {<>} C0))" |
|
54 |
value "show_acom (((step {}) ^^ 4) (step {<>} C0))" |
|
55 |
value "show_acom (((step {}) ^^ 5) (step {<>} C0))" |
|
56 |
value "show_acom (((step {}) ^^ 6) (step {<>} C0))" |
|
57 |
value "show_acom (((step {}) ^^ 7) (step {<>} C0))" |
|
58 |
value "show_acom (((step {}) ^^ 8) (step {<>} C0))" |
|
48765 | 59 |
|
60 |
end |