Theory Xor

theory Xor
  imports Main
begin

section‹XOR›
text‹Entweder Oder›
definition xor :: "bool ⇒ bool ⇒ bool" (infixr "⊕" 59) where
  "a ⊕ b ≡ ¬ (a ⟷ b)"

lemma "(a ⊕ b) = (¬ (a ⟷ b))" by(simp add: xor_def)
lemma xor2: "(a ⊕ b) = ((a ∧ ¬b) ∨ (¬a ∧ b))" by(auto simp add: xor_def)
lemma xor3: "(a ⊕ b) = (a ≠ b)" by(auto simp add: xor_def)
lemma xor4: "(a ⊕ b) = (a = (¬b))" by(auto simp add: xor_def)
lemma xor5: "(a ⊕ b) = ((a ∨ b) ∧ ¬(a ∧ b))" by(auto simp add: xor_def)

text‹Entweder-Oder ist stärker als nur Oder:›
lemma xor_imp_or: "a ⊕ b ⟹ a ∨ b"
  by(simp add: xor5)

end