equal
deleted
inserted
replaced
4 |
4 |
5 subsection "Arithmetic Expressions" |
5 subsection "Arithmetic Expressions" |
6 |
6 |
7 datatype val = Iv int | Rv real |
7 datatype val = Iv int | Rv real |
8 |
8 |
9 type_synonym name = string |
9 type_synonym vname = string |
10 type_synonym state = "name \<Rightarrow> val" |
10 type_synonym state = "vname \<Rightarrow> val" |
11 |
11 |
12 datatype aexp = Ic int | Rc real | V name | Plus aexp aexp |
12 datatype aexp = Ic int | Rc real | V vname | Plus aexp aexp |
13 |
13 |
14 inductive taval :: "aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool" where |
14 inductive taval :: "aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool" where |
15 "taval (Ic i) s (Iv i)" | |
15 "taval (Ic i) s (Iv i)" | |
16 "taval (Rc r) s (Rv r)" | |
16 "taval (Rc r) s (Rv r)" | |
17 "taval (V x) s (s x)" | |
17 "taval (V x) s (s x)" | |
39 subsection "Syntax of Commands" |
39 subsection "Syntax of Commands" |
40 (* a copy of Com.thy - keep in sync! *) |
40 (* a copy of Com.thy - keep in sync! *) |
41 |
41 |
42 datatype |
42 datatype |
43 com = SKIP |
43 com = SKIP |
44 | Assign name aexp ("_ ::= _" [1000, 61] 61) |
44 | Assign vname aexp ("_ ::= _" [1000, 61] 61) |
45 | Semi com com ("_; _" [60, 61] 60) |
45 | Semi com com ("_; _" [60, 61] 60) |
46 | If bexp com com ("IF _ THEN _ ELSE _" [0, 0, 61] 61) |
46 | If bexp com com ("IF _ THEN _ ELSE _" [0, 0, 61] 61) |
47 | While bexp com ("WHILE _ DO _" [0, 61] 61) |
47 | While bexp com ("WHILE _ DO _" [0, 61] 61) |
48 |
48 |
49 |
49 |
66 |
66 |
67 subsection "The Type System" |
67 subsection "The Type System" |
68 |
68 |
69 datatype ty = Ity | Rty |
69 datatype ty = Ity | Rty |
70 |
70 |
71 type_synonym tyenv = "name \<Rightarrow> ty" |
71 type_synonym tyenv = "vname \<Rightarrow> ty" |
72 |
72 |
73 inductive atyping :: "tyenv \<Rightarrow> aexp \<Rightarrow> ty \<Rightarrow> bool" |
73 inductive atyping :: "tyenv \<Rightarrow> aexp \<Rightarrow> ty \<Rightarrow> bool" |
74 ("(1_/ \<turnstile>/ (_ :/ _))" [50,0,50] 50) |
74 ("(1_/ \<turnstile>/ (_ :/ _))" [50,0,50] 50) |
75 where |
75 where |
76 Ic_ty: "\<Gamma> \<turnstile> Ic i : Ity" | |
76 Ic_ty: "\<Gamma> \<turnstile> Ic i : Ity" | |