이사벨 (Isabelle)에서 증명하면서 부 목적을 건너 뛰기

Question

나는 정리를 증명하려고 노력하고 있지만 부차적 인 목표에 갇혀있다. (내가 건너 뛰고 나중에 증명하는 것을 선호한다.) 어떻게 내가 이것을 건너 뛰고 다른 사람들을 증명할 수 있을까요?

먼저, oops과 sorry을 시도했지만 둘 다 (부 목적이 아닌) 전체 증명을 중단합니다. 나는 또한 보조 목표를 더미 보조 정리 (sorry으로 증명 된 가정)에 넣으려고 시도했지만 (apply (rule [my dummy lemma])) 다른 보조 목표에도 더미 보조 정리를 적용합니다 (첫 번째 목표뿐만 아니라).

Answer 1

그것은 주로 유물을 사용하고 있는지 (유감스럽게 생각하십니까;) 적용 스타일인지 또는 입증을 위해 올바른 구조화 된 Isar를 사용하는지에 따라 달라집니다. 나는 두 가지 스타일 모두를 다룰 수있는 작은 예를 제시 할 것이다. 당신이 A 및 B 단지 잠재적으로 거대한 공식의 자리 표시 자 역할을

lemma "A & B" 

을 증명하고 싶었 가정합니다. 당신은 같은 것을 할 것

으로 구조화 된 증거 ​​:이 스타일로,

proof 
    show "A" sorry 
next 
    show "B" sorry 
qed 

즉 당신은 하위 목표에 대한 증거를 생략 할 sorry를 사용할 수 있습니다.

에 적용 할 스타일의 프런트에 subgoal n를 이동 적용 스타일의 명령 prefer n도 있습니다

apply (rule conjI) 
defer -- "moves the first subgoal to the last position" 
apply (*proof for subgoal "B"*) 
apply (*proof for subgoal "A"*) 

을 할 수 있습니다.