2
이사벨에서 사례 분석을 어떻게 적용합니까? 나는 유도를 위해 사용되는 apply (induct x)과 비슷한 것을 찾고 있었다.이사벨 (Isabelle) 사례 분석
A
답변
3
사례 분석은 대개 cases 방법으로 수행됩니다 (Isabelle2014의 Isabelle/Isar Reference manual 색인에서 사례 (방법) 참조). 초보자 인 경우 자습서 Programming and Proving in Isabelle/HOL을 사용하는 것이 좋습니다.
Isabelle 2014 이후 문서는 문서 패널의 Isabelle/jEdit IDE에서도 사용할 수 있습니다.
'증명'과 '적용'모두 임의의 증명 방법을 사용합니다. 그러나'proof'는 구조화 된 증명을 시작합니다. 'apply'는 (구조화되지 않은) 증명 스크립트를 만드는데 사용될 수 있습니다. 이사벨에게 처음 온 사람이라면 구조화 된 증명 스타일에 익숙해지는 것이 좋습니다. 특별한 경우 구별과 유도는 구조화되지 않은 증명에서 매우 지저분 해집니다. –
두 링크가 모두 손상되었습니다. :-( –
지금 수정되었습니다. 두 매뉴얼 모두 웹 페이지와 Isabelle 내부에서 직접 사용할 수 있습니다. –