"4.6 Isabelle/HOL에서의 프로그래밍과 증명"의 연습 4.6에있는 보조 정리를 증명하려면 어떻게해야합니까?

Question

저는 "4.6 Isabelle/HOL에서의 프로그래밍과 증명"에서 Exercise 4.6을 풀려고합니다. 목록을 집합으로 변환하고 보조 정리 "x ∈ elems xs ⟹ ∃ ys zs . xs = ys @ x # zs ∧ x ∉ elems ys"을 증명하는 함수 elems :: "'a list ⇒ 'a set"을 정의 할 것을 요구합니다. 지금까지, 나는 지금까지 온 :이 시점에서

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은 일부 기본 규칙을 적용하기위한 것입니다. 위의 증거에서, 이사벨은 당신이 실존 적 도입을 수행하기를 원한다는 것을 알 수 없습니다. 따라서 예를 들어 proof (intro exI)과 같은 이름을 계속 사용하여 시스템에 명시 적으로 알리고 싶을 수 있습니다. 나는 희망

,이