Theory BExp

theory BExp imports AExp begin

subsection "Boolean Expressions"

datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp

fun bval :: "bexp ⇒ state ⇒ bool" where
"bval (Bc v) s = v" |
"bval (Not b) s = (¬ bval b s)" |
"bval (And b⇩1 b⇩2) s = (bval b⇩1 s ∧ bval b⇩2 s)" |
"bval (Less a⇩1 a⇩2) s = (aval a⇩1 s < aval a⇩2 s)"

value "bval (Less (V ''x'') (Plus (N 3) (V ''y'')))
            <''x'' := 3, ''y'' := 1>"
 
end