Wie kann ich Irreflexität einer induktiv definierten Beziehung in Isabelle nachweisen?

Question

Betrachten wir als Beispiel die folgende Definition von Ungleichheit der natürlichen Zahlen 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 Irreflexivität von unequal beweisen wollen, das heißt, ¬ unequal n n. Für die Zwecke Abbildung lassen beweisen mir zuerst die erfundene 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 den ersten beiden Fällen False müssen aus den Annahmen abgeleitet werden 0 = n + m und Suc _ = n + m, die trivial ist.

Ich würde erwarten, dass der Nachweis von ¬ unequal n n kann in analoger Weise durchgeführt werden, das heißt, nach dem folgende Muster:

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 

Insbesondere würde ich erwarten, dass in den ersten beiden Fällen, I die Annahmen 0 = n und Suc _ = n erhalten. Jedoch bekomme ich überhaupt keine Annahmen, was bedeutet, dass ich gebeten werde, False aus dem Nichts zu beweisen. Warum ist das und wie kann ich den Beweis für Ungleichheit erbringen?

Answer 1

Die induction Methode unterschiedlich variable instantiations und nicht-variable instantiations abwickelt. Eine nichtvariable Instanziierung t ist eine Kurzschrift für x ≡ t, wobei x eine frische Variable ist. Als Ergebnis wird die Induktion unter x durchgeführt, und der Kontext enthält zusätzlich die Definition x ≡ t.

Daher entspricht (induction "n + m" "n + m" arbitrary: n m) im ersten Beweis (induction k ≡ "n + m" l ≡ "n + m" arbitrary: n m) mit dem oben beschriebenen Effekt. Um diesen Effekt für den zweiten Beweis zu erhalten, müssen Sie (induction n n arbitrary: n) durch (induction k ≡ n l ≡ n arbitrary: n) ersetzen. Die Annahmen werden tatsächlich so einfach werden, dass der Vorvereiniger, der von der induction-Methode ausgeführt wird, False von ihnen ableiten kann. Als Ergebnis werden keine Fälle mehr zu beweisen sein, und Sie können den gesamten inneren proof -Block durch by (induction k ≡ n l ≡ n arbitrary: n) ersetzen.

Answer 2

Sie induzieren über unequal. Stattdessen sollten Sie über n, wie diese induct:

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

Dann können wir Vorschlaghammer auf jeder der mit sorry markiert subgoals verwenden. Vorschlaghammer (mit CVC4) empfiehlt uns den Beweis zu vervollständigen, wie folgt:

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