theory week03B_demo_automation imports Main begin definition xor :: "bool \ bool \ bool" where "xor A B \ (A \ \B) \ (\A \ B)" lemma xorI [intro!]: "\ \A; B\ \ False; \B \ A \ \ xor A B" apply (unfold xor_def) apply blast done lemma xorE: "\ xor A B; \A; \B\ \ R; \\A; B\ \ R \ \ R" apply (unfold xor_def) apply blast done lemma "xor A A = False" by (blast elim!: xorE) declare xorE [elim!] lemma "xor A B = xor B A" by blast end