Wie kann ich das Lemma in Übung 4.6 in "Programmieren und Prüfen in Isabelle/HOL" nachweisen?

Question

Ich versuche Aufgabe 4.6 in "Programmieren und Prüfen in Isabelle/HOL" zu lösen. Es fragt nach einer Funktion elems :: "'a list ⇒ 'a set", die eine Liste in eine Menge konvertiert und das Lemma "x ∈ elems xs ⟹ ∃ ys zs . xs = ys @ x # zs ∧ x ∉ elems ys" zu beweisen. Bisher habe ich so weit gekommen:

fun elems :: "'a list ⇒ 'a set" where 
    "elems [] = {}" | 
    "elems (x # xs) = {x} ∪ elems xs" 

lemma first_occ: "x ∈ elems xs ⟹ ∃ ys zs . xs = ys @ x # zs ∧ x ∉ elems ys" 
proof (induction xs) 
    case Nil 
    thus ?case by simp 
next 
    case (Cons u us) 
    show ?case 
    proof cases 
    assume "x = u" 
    thus ?case 
    proof 
    ⟨…⟩ 

An diesem Punkt, erhalte ich die Fehlermeldung „Fehler beim anfänglichen Nachweis-Methode anwenden“. Das ist seltsam, denn das Ziel, ?case, ist der Vorschlag ∃ ys zs . u # us = ys @ x # zs ∧ x ∉ elems ys, und es sollte möglich sein, Existenzvorschläge zu beweisen, indem man den Vorschlag unter der ∃ für einen bestimmten Zeugen zeigt.

Answer 1

das Problem mit Ihrer Linie proof ist, dass es proof ist gemeint, einige Standardregel anzuwenden. In dem obigen Beweis kann Isabelle nicht herausfinden, dass Sie eine existenzielle Einführung machen wollen. Sie möchten dem System das explizit mitteilen, dies zu tun, z. B. indem Sie mit etwas wie proof (intro exI) fortfahren.

Ich hoffe, das hilft, René