들어오는 모든 사실을 사용하는 초기 증명 방법

Question

목표가 있다고 가정합니다. A ⟹ B ⟹ C ⟹ G 목표는 다루기 힘들며 (일부 증명 의무 조항에서 생성 됨) 개발 과정에서 여러 번 비슷한 모양으로 나타납니다.

목표를 단순화하기 위해 보조자 foo을 작성합니다. 모양은 A ⟹ C ⟹ (P ⟹ Q) ⟹ G입니다.

나는

case goal42 
    thus ?case 
    proof (rule foo) 
    assume P 
    show Q sorry 
    qed 

을 쓸 수 있도록하고 싶습니다하지만 foo이 B를 사용하지 않기 때문에이 실패합니다. 무엇 작동하는

case goal42 
    thus ?case 
    apply - 
    apply (erule (1) eqvt_lam_case) 
    proof- 
    assume P 
    show Q sorry 
    qed 

입니다하지만, 적용 스크립트의 중간에 proof 개방이 스타일은 나쁜 관행으로 간주됩니다.

rule과 비슷한 방법이 수신되는 사실을 규칙의 가설과 대조하는 데 약간 똑똑합니까? 이상적으로 foo에있는 consumes 2 매개 변수를 읽고 얼마나 많은 가설이 일치해야하는지 파악하십시오.

Answer 1

rule 방법은 매우 사실적입니다. 그 전치사 intro 및 elim은 연쇄 사실이 맞지 않는 경우 불평하지 않습니다. intro이 일치하지 않습니다. elim ...은 대략 apply - apply(erule ...)+에 해당하므로 찾고있는 내용과 비슷할 수 있습니다. 하지만 elim에 여러 가정을 일치시키는 방법을 알지 못하며 elim은 주어진 규칙을 최대한 길게 적용하려고 시도합니다. 이는 원하는 것이 아닐 수도 있습니다.

그러나 나머지 목표에 대한 Isar 증명을 열었으므로 증명을 재정렬하고 문제를 피할 수 있습니다.

case goal42 
{ assume P 
    show Q sorry } 
with goal42 show ?case by-(erule (2) eqvt_lam_case) 

나는 (내가 아는 한, 사용하지 않을 수도 있지만) rule_tac` 거의 rule``처럼 작동하지만, 올바른 순서로 체인 될 가정을 필요로하지 않는 '것을 추가 할해야