"4.6 Isabelle/HOLのプログラミングと証明"のエクササイズ4.6で補題を証明するにはどうしたらいいですか？

Question

私は "プログラミングとIsabelle/HOLの検証"でエクササイズ4.6を解決しようとしています。リストを集合に変換する関数elems :: "'a list ⇒ 'a set"を定義し、補助詞"x ∈ elems xs ⟹ ∃ ys zs . xs = ys @ x # zs ∧ x ∉ elems ys"を証明するよう求めます。これまでのところ、私は遠くに来ました：

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 
    ⟨…⟩ 

この時点で、「最初の証明方法を適用できませんでした」というエラーメッセージが表示されます。目標は?case、提案は∃ ys zs . u # us = ys @ x # zs ∧ x ∉ elems ysなので、具体的証人については∃の下にその命題を示すことで、存在論的命題を証明することが可能でなければなりません。

Answer 1

proofの問題点は、proofはデフォルトのルールを適用することです。上記の証拠では、Isabelleは、あなたが実在の紹介をしたいと思うことを理解できません。たとえば、proof (intro exI)のようなものを続けるなど、システムに明示的に伝えたいと思うかもしれません。

私は願って、これはなぜイザベルがこれを把握することはできません、 ルネ