Isar 증명에서`presume`을 언제 사용 하시겠습니까?

Question

Isar에는 assume 외에 presume 명령을 사용하여 Isar 증명 블록에 사실을 소개합니다. 내가 볼 수 있고 문서에서 읽을 수있는 것으로부터 가정 (추정?)을 명시 적으로 목표에 나열 할 필요가 없으며 가정 된 진술이 다른 목표에서 따름을 보여주는 사례를 추가하는 것으로 보입니다.

질문은 다음과 같습니다. 대신 assume을 사용하고, presume으로 어떤 유용한 트릭을 사용할 수 있습니까?

Answer 1

presume을 사용하면 Iser 언어를 더 표현하기가 어렵습니다. presume을 사용하여 모든 증명을 assume으로 만 재구성 할 수 있기 때문입니다. 그럼에도 불구하고, 적어도 두 (더 많거나 적은 일반)를 사용하는 경우가 있습니다 : 당신이 상처처럼 presume를 사용할 수 있기 때문에

첫째, presume 때때로, 더 자연스러운 교정을에 연결됩니다. 예를 들어

는, 증명서 상태가 두 골 A ==> C 및 B ==> C을 가지고 당신 있다고 가정하고, 일부 E는 현재 컨텍스트의 현재 상황과 E의 사실과 사실 의미 부여 A에서와 B에서 증거를 다음과 수 C. 다음과 같이 presume를 사용하면 증명을 구성 할 수 있습니다 다음과 같이

이

presume E 
    show C <proof using E and facts> 
    thus C . 
next 
    assume A 
    thus E <proof using A and facts> 
    thus E . 
next 
    assume B 
    thus E <proof using A and facts> 
    thus E . 

assume 스타일이 보인다 : presume와

assume A 
    hence E <proof using A and facts> 
    show C <proof using E and facts> 
next 
    assume B 
    hence E <proof using B and facts> 
    show C <proof using E and facts> 

, 증거의 구조는 더 명시 적입니다 : 분명히, 우리 만 결과를 표시하려면 E이 필요하며 이것은 증거의 흥미로운 부분 일 수 있습니다. 또한 스타일에서는 E이 C을 두 번 포함한다는 증명을해야합니다. 물론 이것은 항상 보조 정리로 분해 될 수 있지만, 증명이 상황에서 많은 사실을 필요로한다면, 그것은 추악해질 수 있습니다.

두 번째로 presume을 사용할 수 있으며 교정 오류는 assume 및 show에 입력 오류를 찾을 수 있습니다. 당신이

fix x 
assume A and B and C and D and E 
show F 

을 가지고 있지만 이사벨은 show 즉, 당신은 아마 가정 또는 골 문에 일부 오타가 어떤 목표를 해결하지 않을 것이다 있음을 알려줍니다 가정하자. 이제 assume 번을 presume으로 변경하세요. show이 여전히 실패하면 실수는 목표 진술 문에서 어딘가에 있습니다. 그렇지 않으면 아마 가정의 어딘가에있을 것입니다. show 증명을 sorry으로 닫고 apply_end(assumption)+으로 가정을 해제하십시오. 그것이 통일 될 수 없다는 가정하에 멈출 것입니다. 아마도 이것은 잘못된 것입니다.