theory week03A_demo_automation imports Main begin

definition 
  xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
  "xor A B \<equiv> (A \<and> \<not>B) \<or> (\<not>A \<and> B)"

lemma xorI:
  "A \<or> B \<Longrightarrow> \<not> (A \<and> B) \<Longrightarrow> xor A B"
  sorry

lemma xorE:
  "\<lbrakk> xor A B; \<lbrakk>A; \<not>B\<rbrakk> \<Longrightarrow> R; \<lbrakk>\<not>A; B\<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
  sorry


lemma "xor A A = False"
  apply blast
  done

lemma "xor A B = xor B A"
  oops

end