|
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{* Make assignment rule executable: *} |
|
11 declare step.simps(2)[code del] |
|
12 lemma [code]: "step S (x ::= e {P}) = (x ::= e {(%s. s(x := aval e s)) ` S})" |
|
13 by auto |
|
14 declare step.simps(1,3-)[code] |
|
15 |
|
16 text{* The example: *} |
|
17 definition "c = WHILE Less (V ''x'') (N 3) |
|
18 DO ''x'' ::= Plus (V ''x'') (N 2)" |
|
19 definition c0 :: "state set acom" where "c0 = anno {} c" |
|
20 |
|
21 definition "show_acom xs = map_acom (\<lambda>S. show_state xs ` S)" |
|
22 |
|
23 text{* Collecting semantics: *} |
|
24 value "show_acom [''x''] (((step {%x. 0}) ^^ 1) c0)" |
|
25 value "show_acom [''x''] (((step {%x. 0}) ^^ 2) c0)" |
|
26 value "show_acom [''x''] (((step {%x. 0}) ^^ 3) c0)" |
|
27 value "show_acom [''x''] (((step {%x. 0}) ^^ 4) c0)" |
|
28 value "show_acom [''x''] (((step {%x. 0}) ^^ 5) c0)" |
|
29 value "show_acom [''x''] (((step {%x. 0}) ^^ 6) c0)" |
|
30 |
|
31 text{* Small-step semantics: *} |
|
32 value "show_acom [''x''] (((step {}) ^^ 0) (step {%x. 0} c0))" |
|
33 value "show_acom [''x''] (((step {}) ^^ 1) (step {%x. 0} c0))" |
|
34 value "show_acom [''x''] (((step {}) ^^ 2) (step {%x. 0} c0))" |
|
35 value "show_acom [''x''] (((step {}) ^^ 3) (step {%x. 0} c0))" |
|
36 value "show_acom [''x''] (((step {}) ^^ 4) (step {%x. 0} c0))" |
|
37 value "show_acom [''x''] (((step {}) ^^ 5) (step {%x. 0} c0))" |
|
38 |
|
39 |
|
40 end |