Isabelle : complement of datatype

0
votes
datatype aaa = A | B
lemma "(a ~= A) --> (a = B)"

How to prove this basic lemma? I'm relatively new to Isabelle, and the problem is confusing.

1
isabelle
Another strategy to try as a beginner is to use sledgehammer. For this kind of lemma, it'll definitely quickly come back with a proof. – larsrh

1 Answers

1
votes

Via case-analysis on a:

by (cases a, auto)