equal
deleted
inserted
replaced
1 theory BExp imports AExp begin |
1 theory BExp imports AExp begin |
2 |
2 |
3 subsection "Boolean Expressions" |
3 subsection "Boolean Expressions" |
4 |
4 |
5 text_raw{*\snip{BExpbexpdef}{0}{1}{% *} |
|
6 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 |
7 text_raw{*}%endsnip*} |
|
8 |
6 |
9 text_raw{*\snip{BExpbvaldef}{1}{2}{% *} |
7 text_raw{*\snip{BExpbvaldef}{1}{2}{% *} |
10 fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where |
8 fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where |
11 "bval (Bc v) s = v" | |
9 "bval (Bc v) s = v" | |
12 "bval (Not b) s = (\<not> bval b s)" | |
10 "bval (Not b) s = (\<not> bval b s)" | |