23 @{typ "((com option \<times> state) \<times> (com option \<times> state)) set"} |
23 @{typ "((com option \<times> state) \<times> (com option \<times> state)) set"} |
24 |
24 |
25 Some syntactic sugar that we will use to hide the |
25 Some syntactic sugar that we will use to hide the |
26 @{text option} part in configurations: |
26 @{text option} part in configurations: |
27 *} |
27 *} |
28 syntax |
28 abbreviation |
29 "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("<_,_>") |
29 angle :: "[com, state] \<Rightarrow> com option \<times> state" ("<_,_>") where |
30 "_angle2" :: "state \<Rightarrow> com option \<times> state" ("<_>") |
30 "<c,s> == (Some c, s)" |
31 |
31 abbreviation |
32 syntax (xsymbols) |
32 angle2 :: "state \<Rightarrow> com option \<times> state" ("<_>") where |
33 "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>") |
33 "<s> == (None, s)" |
34 "_angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>") |
34 |
35 |
35 notation (xsymbols) |
36 syntax (HTML output) |
36 angle ("\<langle>_,_\<rangle>") and |
37 "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>") |
37 angle2 ("\<langle>_\<rangle>") |
38 "_angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>") |
38 |
39 |
39 notation (HTML output) |
40 translations |
40 angle ("\<langle>_,_\<rangle>") and |
41 "\<langle>c,s\<rangle>" == "(Some c, s)" |
41 angle2 ("\<langle>_\<rangle>") |
42 "\<langle>s\<rangle>" == "(None, s)" |
|
43 |
42 |
44 text {* |
43 text {* |
45 Now, finally, we are set to write down the rules for our small step semantics: |
44 Now, finally, we are set to write down the rules for our small step semantics: |
46 *} |
45 *} |
47 inductive_set |
46 inductive_set |