48765
|
1 |
theory Collecting_Examples
|
|
2 |
imports Collecting
|
|
3 |
begin
|
|
4 |
|
|
5 |
text{* Tweak code generation to work with sets of non-equality types: *}
|
|
6 |
declare insert_code[code del] union_coset_filter[code del]
|
|
7 |
lemma insert_code [code]: "insert x (set xs) = set (x#xs)"
|
|
8 |
by simp
|
|
9 |
|
|
10 |
text{* The example: *}
|
|
11 |
definition "c = WHILE Less (V ''x'') (N 3)
|
|
12 |
DO ''x'' ::= Plus (V ''x'') (N 2)"
|
50766
|
13 |
definition C0 :: "state set acom" where "C0 = anno {} c"
|
48765
|
14 |
|
|
15 |
definition "show_acom xs = map_acom (\<lambda>S. show_state xs ` S)"
|
|
16 |
|
|
17 |
text{* Collecting semantics: *}
|
50821
|
18 |
|
|
19 |
value "show_acom [''x''] (((step {<>}) ^^ 1) C0)"
|
|
20 |
value "show_acom [''x''] (((step {<>}) ^^ 2) C0)"
|
|
21 |
value "show_acom [''x''] (((step {<>}) ^^ 3) C0)"
|
|
22 |
value "show_acom [''x''] (((step {<>}) ^^ 4) C0)"
|
|
23 |
value "show_acom [''x''] (((step {<>}) ^^ 5) C0)"
|
|
24 |
value "show_acom [''x''] (((step {<>}) ^^ 6) C0)"
|
|
25 |
value "show_acom [''x''] (((step {<>}) ^^ 7) C0)"
|
|
26 |
value "show_acom [''x''] (((step {<>}) ^^ 8) C0)"
|
48765
|
27 |
|
|
28 |
text{* Small-step semantics: *}
|
50821
|
29 |
value "show_acom [''x''] (((step {}) ^^ 0) (step {<>} C0))"
|
|
30 |
value "show_acom [''x''] (((step {}) ^^ 1) (step {<>} C0))"
|
|
31 |
value "show_acom [''x''] (((step {}) ^^ 2) (step {<>} C0))"
|
|
32 |
value "show_acom [''x''] (((step {}) ^^ 3) (step {<>} C0))"
|
|
33 |
value "show_acom [''x''] (((step {}) ^^ 4) (step {<>} C0))"
|
|
34 |
value "show_acom [''x''] (((step {}) ^^ 5) (step {<>} C0))"
|
|
35 |
value "show_acom [''x''] (((step {}) ^^ 6) (step {<>} C0))"
|
|
36 |
value "show_acom [''x''] (((step {}) ^^ 7) (step {<>} C0))"
|
|
37 |
value "show_acom [''x''] (((step {}) ^^ 8) (step {<>} C0))"
|
48765
|
38 |
|
|
39 |
end
|