Theory Formula

section ‹Boolean Formulae›

theory Formula
imports Main
begin

  datatype 'a formula =
    False |
    True |
    Variable 'a |
    Negation "'a formula" |
    Conjunction "'a formula" "'a formula" |
    Disjunction "'a formula" "'a formula"

  primrec satisfies :: "'a set ⇒ 'a formula ⇒ bool" where
    "satisfies A False ⟷ HOL.False" |
    "satisfies A True ⟷ HOL.True" |
    "satisfies A (Variable a) ⟷ a ∈ A" |
    "satisfies A (Negation x) ⟷ ¬ satisfies A x" |
    "satisfies A (Conjunction x y) ⟷ satisfies A x ∧ satisfies A y" |
    "satisfies A (Disjunction x y) ⟷ satisfies A x ∨ satisfies A y"

end