subsection "Boolean Expressions"

theory BExp imports AExp begin

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

text_raw‹\snip{BExpbvaldef}{1}{2}{%›
fun bval :: "bexp → state → bool" where
"bval (Bc v) s = v" |
"bval (Not b) s = (¬ bval b s)" |
"bval (And b₁ b₂) s = (bval b₁ s ∧ bval b₂ s)" |
"bval (Less a₁ a₂) s = (aval a₁ s < aval a₂ s)"
text_raw‹}%endsnip›

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


subsection "Constant Folding"

text‹Optimizing constructors:›

text_raw‹\snip{BExplessdef}{0}{2}{%›
fun less :: "aexp → aexp → bexp" where
"less (N n₁) (N n₂) = Bc(n₁ < n₂)" |
"less a₁ a₂ = Less a₁ a₂"
text_raw‹}%endsnip›

lemma [simp]: "bval (less a1 a2) s = (aval a1 s < aval a2 s)"
apply(induction a1 a2 rule: less.induct)
apply simp_all
done

text_raw‹\snip{BExpanddef}{2}{2}{%›
fun "and" :: "bexp → bexp → bexp" where
"and (Bc True) b = b" |
"and b (Bc True) = b" |
"and (Bc False) b = Bc False" |
"and b (Bc False) = Bc False" |
"and b₁ b₂ = And b₁ b₂"
text_raw‹}%endsnip›

lemma bval_and[simp]: "bval (and b1 b2) s = (bval b1 s ∧ bval b2 s)"
apply(induction b1 b2 rule: and.induct)
apply simp_all
done

text_raw‹\snip{BExpnotdef}{2}{2}{%›
fun not :: "bexp → bexp" where
"not (Bc True) = Bc False" |
"not (Bc False) = Bc True" |
"not b = Not b"
text_raw‹}%endsnip›

lemma bval_not[simp]: "bval (not b) s = (¬ bval b s)"
apply(induction b rule: not.induct)
apply simp_all
done

text‹Now the overall optimizer:›

text_raw‹\snip{BExpbsimpdef}{0}{2}{%›
fun bsimp :: "bexp → bexp" where
"bsimp (Bc v) = Bc v" |
"bsimp (Not b) = not(bsimp b)" |
"bsimp (And b₁ b₂) = and (bsimp b₁) (bsimp b₂)" |
"bsimp (Less a₁ a₂) = less (asimp a₁) (asimp a₂)"
text_raw‹}%endsnip›

value "bsimp (And (Less (N 0) (N 1)) b)"

value "bsimp (And (Less (N 1) (N 0)) (Bc True))"

theorem "bval (bsimp b) s = bval b s"
apply(induction b)
apply simp_all
done

end