equal
deleted
inserted
replaced
3 subsection "Boolean Expressions" |
3 subsection "Boolean Expressions" |
4 |
4 |
5 datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp |
5 datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp |
6 |
6 |
7 fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where |
7 fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where |
8 "bval (Bc v) _ = v" | |
8 "bval (Bc v) s = v" | |
9 "bval (Not b) s = (\<not> bval b s)" | |
9 "bval (Not b) s = (\<not> bval b s)" | |
10 "bval (And b1 b2) s = (if bval b1 s then bval b2 s else False)" | |
10 "bval (And b1 b2) s = (if bval b1 s then bval b2 s else False)" | |
11 "bval (Less a1 a2) s = (aval a1 s < aval a2 s)" |
11 "bval (Less a1 a2) s = (aval a1 s < aval a2 s)" |
12 |
12 |
13 value "bval (Less (V ''x'') (Plus (N 3) (V ''y''))) |
13 value "bval (Less (V ''x'') (Plus (N 3) (V ''y''))) |