How can I prove irreflexivity of an inductively defined relation in Isabelle?

Question

Consider as an example the following definition of inequality of natural numbers in Isabelle:

inductive unequal :: "nat ⇒ nat ⇒ bool" where
  zero_suc: "unequal 0 (Suc _)" |
  suc_zero: "unequal (Suc _) 0" |
  suc_suc:  "unequal n m ⟹ unequal (Suc n) (Suc m)"

I want to prove irreflexivity of unequal, that is, ¬ unequal n n. For illustration purposes let me first prove the contrived lemma ¬ unequal (n + m) (n + m):

lemma "¬ unequal (n + m) (n + m)"
proof
  assume "unequal (n + m) (n + m)"
  then show False
  proof (induction "n + m" "n + m" arbitrary: n m)
    case zero_suc
    then show False by simp
  next
    case suc_zero
    then show False by simp
  next
    case suc_suc
    then show False by presburger
  qed
qed

In the first two cases, False must be deduced from the assumptions 0 = n + m and Suc _ = n + m, which is trivial.

I would expect that the proof of ¬ unequal n n can be done in an analogous way, that is, according to the following pattern:

lemma "¬ unequal n n"
proof
  assume "unequal n n"
  then show False
  proof (induction n n arbitrary: n)
    case zero_suc
    then show False sorry
  next
    case suc_zero
    then show False sorry
  next
    case suc_suc
    then show False sorry
  qed
qed

In particular, I would expect that in the first two cases, I get the assumptions 0 = n and Suc _ = n. However, I get no assumptions at all, meaning that I am asked to prove False from nothing. Why is this and how can I conduct the proof of inequality?

Answer 1

You are inducting over unequal. Instead, you should induct over n, like this:

lemma "¬ (unequal n n)"
proof (induct n)
  case 0
  then show ?case sorry
next
  case (Suc n)
  then show ?case sorry
qed

Then we can use Sledgehammer on each of the subgoals marked with sorry. Sledgehammer (with CVC4) recommends us to complete the proof as follows:

lemma "¬ (unequal n n)"
proof (induct n)
  case 0
  then show ?case using unequal.cases by blast
next
  case (Suc n)
  then show ?case using unequal.cases by blast
qed 

Answer 2

The induction method handles variable instantiations and non-variable instantiations differently. A non-variable instantiation t is a shorthand for x ≡ t where x is a fresh variable. As a result, induction is done on x, and the context additionally contains the definition x ≡ t.

Therefore, (induction "n + m" "n + m" arbitrary: n m) in the first proof is equivalent to (induction k ≡ "n + m" l ≡ "n + m" arbitrary: n m) with the effect described above. To get this effect for the second proof, you have to replace (induction n n arbitrary: n) with (induction k ≡ n l ≡ n arbitrary: n). The assumptions will actually become so simple that the pre-simplifier, which is run by the induction method, can derive False from them. As a result, there will be no cases left to prove, and you can replace the whole inner proof–qed block with by (induction k ≡ n l ≡ n arbitrary: n).