Überprüfung der Kommutativität von hinzufügen, Take 2

Question

Diese Frage ist eine Follow-up auf die folgende Frage isabelle proving commutativity for add, meine Follow-up war zu lang, um ein Kommentar zu sein. Das Problem, wie angegeben war, die Kommutativität der Add-Funktion definiert wie folgt anzuzeigen:

fun add :: "nat ⇒ nat ⇒ nat" where 
    "add 0 n = n" | 
    "add (Suc m) n = Suc(add m n)" 

Versuch

theorem "add m n = add n m" 
apply(induct_tac m) 
apply(auto) 

stecken bleibt (auf dem induktiven Fall) wegen einer fehlenden Lemma. Ich wurde neugierig auf dieses Problem und erforschte alternative (wenn auch weniger effiziente) Wege, es zu beweisen. Angenommen definierten wir das Lemma

lemma Lemma1 [simp]: "add n (Suc 0) = Suc n 

, die Isabelle durch Induktion automatisch nachweisen kann, dann der induktive Schritt ist

Suc (add k m) = add m (Suc k) 

zu beweisen, die wir von Hand tun könnten als

Suc (add k m) 
= Suc (add m k) by the IH 
= add (add m k) (Suc 0) by Lemma1 <-- 
= add m (add k (Suc 0)) by associativity (already proved) 
= add m (Suc k) by the Lemma1 --> 

folgen jedoch , Isabelle ist nicht in der Lage, dies zu beweisen, und es scheint, dass der Vereinfacher in der zweiten Zeile festsitzt. Unter Verwendung der offensicht- licheren Methode anstelle von Lemma1 ist der Proof jedoch erfolgreich. Es scheint in der Lage zu sein, Lemma2 in beiden Richtungen zu verwenden, aber nicht das oben definierte Lemma1. Weiß jemand warum? Ich fühle mich wie ich offensichtlich irgendwo etwas mit Blick auf bin ..

Bemerkungen: Mir ist klar, nur die simplifier tatsächlich Definitionen gelten etc in eine Richtung, sondern nutzen Heuristiken, um zu versuchen und beiden Seiten der Gleichung auf den gleichen Begriff

Answer 1

Lemma2 zu reduzieren wie Sie nicht in beide Richtungen verwendet, kann sehen, wenn Sie versuchen, den Beweis manuell mit subst Schritte zu tun:

theorem commutativity2: 
"add n m = add m n" 
apply (induct n) 
apply (subst Lemma0) 
apply (subst add.simps(1)) 
apply (rule refl) 

(* ⋀n. add n m = add m n ⟹ add (Suc n) m = add m (Suc n) *) 
apply (subst add.simps(2)) 
(* ⋀n. add n m = add m n ⟹ Suc (add n m) = add m (Suc n) *) 
apply (erule ssubst) 
(* ⋀n. Suc (add m n) = add m (Suc n) *) 
apply (subst Lemma2) 
(* ⋀n. Suc (add m n) = Suc (add m n) *) 
apply (rule refl) 
done 

Es ist nur auf der rechten Seite der Ziel-Gleichung zu arbeiten, aber immer noch Lemma1 mit aus links nach rechts.

Wenn Sie den Beweis, wie in Ihrem Handbuch Beweis tun möchten, können Sie auch tun es leicht in Isabelle:

theorem commutativity: 
"add m n = add n m" 
proof (induct m) 
    show "add 0 n = add n 0" using Lemma0 by simp 
next case (Suc k) 
    have  "add (Suc k) n 
       = Suc (add k n)" by simp 
    also have "... = Suc (add n k)" using Suc.hyps by simp 
    also have "... = add (add n k) (Suc 0)" using Lemma1 by simp 
    also have "... = add n (add k (Suc 0))" using associativity by simp 
    also have "... = add n (Suc k)" using Lemma1 by simp 
    finally show ?case . 
qed 

EDIT:

Ein manueller Beweis zeigt, warum dies nicht mit Lemma1 funktioniert: Beim ersten Rewrite muss Lemma 1 von rechts nach links verwendet werden ([symmetric]).

theorem commutativity3: 
"add n m = add m n" 
apply (induct n) 
apply (subst Lemma0) 
apply (subst add.simps(1)) 
apply (rule refl) 

(* ⋀n. add n m = add m n ⟹ add (Suc n) m = add m (Suc n) *) 
apply (subst Lemma1[symmetric]) back 
(* ⋀n. add n m = add m n ⟹ add (Suc n) m = add m (add n (Suc 0)) *) 
apply (subst associativity) 
(* ⋀n. add n m = add m n ⟹ add (Suc n) m = add (add m n) (Suc 0) *) 
apply (subst Lemma1) 
(* ⋀n. add n m = add m n ⟹ add (Suc n) m = Suc (add m n) *) 
apply (erule subst) 
(* ⋀n. add (Suc n) m = Suc (add n m) *) 
apply (subst add.simps(2)) 
(* ⋀n. Suc (add n m) = Suc (add n m) *) 
apply (rule refl) 
done