equal
deleted
inserted
replaced
34 Hence the function @{text"value"} takes an additional parameter, an |
34 Hence the function @{text"value"} takes an additional parameter, an |
35 \emph{environment} of type @{typ"nat => bool"}, which maps variables to their |
35 \emph{environment} of type @{typ"nat => bool"}, which maps variables to their |
36 values: |
36 values: |
37 *} |
37 *} |
38 |
38 |
39 consts value :: "boolex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool"; |
39 consts "value" :: "boolex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool"; |
40 primrec |
40 primrec |
41 "value (Const b) env = b" |
41 "value (Const b) env = b" |
42 "value (Var x) env = env x" |
42 "value (Var x) env = env x" |
43 "value (Neg b) env = (\<not> value b env)" |
43 "value (Neg b) env = (\<not> value b env)" |
44 "value (And b c) env = (value b env \<and> value c env)"; |
44 "value (And b c) env = (value b env \<and> value c env)"; |