Theory xor_cal

(*
Title:  Allen's qualitative temporal calculus
Author:  Fadoua Ghourabi (fadouaghourabi@gmail.com)
Affiliation: Ochanomizu University, Japan
*)

theory xor_cal

imports

  Main

begin
definition xor::"bool ⇒ bool ⇒ bool" (infixl ‹⊕› 60)
where "xor A B ≡ (A ∧ ¬B) ∨ (¬A ∧ B)"

declare xor_def [simp]

interpretation bool:semigroup "(⊕) "
proof
{ fix a b c show "a ⊕ b ⊕ c = a ⊕ (b ⊕ c)" by auto}
qed

lemma xor_distr_L [simp]:"A ⊕ (B ⊕ C) = (A∧¬B∧¬C)∨(A∧B∧C)∨(¬A∧B∧¬C)∨(¬A∧¬B∧C)"
by auto

lemma xor_distr_R [simp]:"(A ⊕ B) ⊕ C = A ⊕ (B ⊕ C)"
by auto

end