equal
deleted
inserted
replaced
7 datatype val = Iv int | Rv real |
7 datatype val = Iv int | Rv real |
8 |
8 |
9 type_synonym vname = string |
9 type_synonym vname = string |
10 type_synonym state = "vname \<Rightarrow> val" |
10 type_synonym state = "vname \<Rightarrow> val" |
11 |
11 |
|
12 text_raw{*\snip{aexptDef}{0}{2}{% *} |
12 datatype aexp = Ic int | Rc real | V vname | Plus aexp aexp |
13 datatype aexp = Ic int | Rc real | V vname | Plus aexp aexp |
|
14 text_raw{*}%endsnip*} |
13 |
15 |
14 inductive taval :: "aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool" where |
16 inductive taval :: "aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool" where |
15 "taval (Ic i) s (Iv i)" | |
17 "taval (Ic i) s (Iv i)" | |
16 "taval (Rc r) s (Rv r)" | |
18 "taval (Rc r) s (Rv r)" | |
17 "taval (V x) s (s x)" | |
19 "taval (V x) s (s x)" | |