16 |
16 |
17 axiomatization |
17 axiomatization |
18 Arg :: loc and |
18 Arg :: loc and |
19 Res :: loc |
19 Res :: loc |
20 |
20 |
21 datatype vname = Glb glb | Loc loc |
21 datatype_new vname = Glb glb | Loc loc |
22 type_synonym globs = "glb => val" |
22 type_synonym globs = "glb => val" |
23 type_synonym locals = "loc => val" |
23 type_synonym locals = "loc => val" |
24 datatype state = st globs locals |
24 datatype_new state = st globs locals |
25 (* for the meta theory, the following would be sufficient: |
25 (* for the meta theory, the following would be sufficient: |
26 typedecl state |
26 typedecl state |
27 consts st :: "[globs , locals] => state" |
27 consts st :: "[globs , locals] => state" |
28 *) |
28 *) |
29 type_synonym aexp = "state => val" |
29 type_synonym aexp = "state => val" |
30 type_synonym bexp = "state => bool" |
30 type_synonym bexp = "state => bool" |
31 |
31 |
32 typedecl pname |
32 typedecl pname |
33 |
33 |
34 datatype com |
34 datatype_new com |
35 = SKIP |
35 = SKIP |
36 | Ass vname aexp ("_:==_" [65, 65 ] 60) |
36 | Ass vname aexp ("_:==_" [65, 65 ] 60) |
37 | Local loc aexp com ("LOCAL _:=_ IN _" [65, 0, 61] 60) |
37 | Local loc aexp com ("LOCAL _:=_ IN _" [65, 0, 61] 60) |
38 | Semi com com ("_;; _" [59, 60 ] 59) |
38 | Semi com com ("_;; _" [59, 60 ] 59) |
39 | Cond bexp com com ("IF _ THEN _ ELSE _" [65, 60, 61] 60) |
39 | Cond bexp com com ("IF _ THEN _ ELSE _" [65, 60, 61] 60) |