Isabelle/Isar에 여러 변수가있는 실존 적 명제를 효과적으로 증명하려면 어떻게해야합니까?

Question

Isabelle/Isar에 보조제 ∃ n m k . [n, m, k] = [2, 3, 5]을 증명하고 싶다고 말합니다. 45 페이지의 이자벨/HOL 튜토리얼에 제안 내가 가서 경우 다음과 같이 내 증거는 같습니다

물론

lemma "∃ n m k . [n, m, k] = [2, 3, 5]" 
proof 
    show "∃ m k . [2, m, k] = [2, 3, 5]" 
    proof 
    show "∃ k . [2, 3, k] = [2, 3, 5]" 
    proof 
     show "[2, 3, 5] = [2, 3, 5]" by simp 
    qed 
    qed 
qed 

,이 너무 장황. 증명이 간결하고 읽기 쉽도록 위와 같은 명제를 어떻게 증명할 수 있습니까?

Answer 1

한 번 한정어 소개 규칙을 여러 번 적용하여 한 번에 여러 개의 존재 한정 기호를 도입 할 수 있습니다. 예를 들어, 증명 방법 (rule exI)+은 모든 가장 바깥에 존재하는 한정어를 도입합니다.

lemma "∃n m k. [n, m, k] = [2, 3, 5]" 
proof(rule exI)+ 
    show "[2, 3, 5] = [2, 3, 5]" by simp 
qed 

또는 먼저 인스턴스화 된 속성을 명시한 다음 자동 증명 메서드를 사용하여 인스턴스화를 수행 할 수 있습니다. 일반적으로 blast은 simplefier를 호출하지 않기 때문에 잘 작동합니다. 귀하의 예에서는 숫자가 과부하되기 때문에 유형 주석을 추가해야합니다.

lemma "∃n m k :: nat. [n, m, k] = [2, 3, 5]" 
proof - 
    have "[2, 3, 5 :: nat] = [2, 3, 5]" by simp 
    then show ?thesis by blast 
qed