이자벨

Question

에서 ==> B ==> C ==> B를 증명 나는 이자벨에

A ==> B ==> C ==> B 

증명에 대해 의아해입니다. 분명히 당신은 할 수있다

apply simp 

그러나 나는 이것을 규칙을 사용하여 어떻게 증명할 수 있었느냐?

또는 규칙을 덤프하는 방법이 있습니까 simp? 감사.

Answer 1

증명이 실제로 어떻게 작동하는지 알고 싶다면 재미있는 전술과 자동 추론 도구를 처음부터 잊어 버려야합니다.

문 A ==> B ==> C ==> B (사용이 결합 ==> 특별) 이사벨의/이자벨에서의 증거 있도록/ISAR은 순수는 즉시 마찬가지입니다

lemma "A ==> B ==> C ==> B" . 

단지 그것 뿐이다

, . (by this을 abbreviates하는,하지만 this은 실제로 여기에 비어 있음).

약간 덜 진공적인 증명은 실제 Isabelle/HOL 연결 요소를 사용하므로 표준 소개 또는 제거 단계로 처리 할 수 ​​있습니다. 예 : 같은 :

lemma "A --> B --> C --> B" 
proof 
    show "B --> C --> B" 
    proof 
    assume b: B 
    show "C --> B" 
    proof 
     show B by (rule b) 
    qed 
    qed 
qed 

하지만 그리 재미 중 하나 : 당신이 끝날 때까지 그 다음 분해되는 지루한 의미를 구축 할 수 있습니다.

더 재미있는 Isabelle/Isar 증명을 찾으려면 웹 검색을하거나 시스템과 함께 제공되는 소스를 살펴보십시오. 전혀 임의의 예가 여기에 있습니다 : Drinker.

설명서가 너무 많습니다. 실제로는 너무 많습니다.

Answer 2

단순 추적을 사용할 수 있습니다. Proof General에서 Isabelle → Settings → Tracing → Trace Simplifier를 사용하면 jEdit에 대해 알지 못합니다.

편집 : simp이 문제를 해결하기 위해 다시 쓰기 규칙을 사용하지 않고 simp trace가 도움이되지 않으며 대신 전제에서 A, B 및 C를 "본다". 이 문맥의 컨텍스트는 A = True, B = True 및 C = True을 다시 작성한 다음 목표 B을 True으로 다시 작성하면 작업이 완료된 것입니다.

그러나 이와 같은 증명 문은 "B"이라는 목표와 일치하는 assumption 방법을 사용하는 것이 좋습니다. 아마도 이것을 rule을 사용하여 증명할 수있는 방법이 있지만 불필요하게 복잡 할 수 있습니다. assumption은 assume_tac을 사용하며 매우 기본 인 함수 Thm.assumption을 감싸는 포장지이므로 Isabelle에서 가장 기본적인 증거 방법 중 하나라고 할 수 있습니다. 그럼 by assumption으로 작성하십시오.