저는 Isabelle을 처음 접했고 Isabelle과 함께 제공되는 thy 파일 조직에 당황 스럽습니다.Isabelle과 함께 제공되는 thy 파일의 구성
~~src/HOL에 동일한 지식 체계를 사용하는 일부 파일은 왜 ~~src/HOL/<theoryname>에 있습니까?
예. GCD가 ~~src/HOL인데 ~~src/HOL/Number_Theory이 아닌 이유는 무엇입니까?
비슷한 질문 : ex 폴더와 ~~src/HOL의 Isar_Examples 폴더의 차이점은 무엇입니까? 그들을 합병하는 것이 더 자연스럽지 않습니까?
또한, ~~src/HOL에서 document 폴더는 무엇입니까?
이사벨 (Isabelle)은 거의 30 세이며 그 당시 상당히 바뀌 었습니다. 예를 들어 GCD.thy 파일은 12 년 전에 작성되었으며 상수는 gcd :: nat ⇒ nat ⇒ nat입니다. 그 당시에는 Number_Theory 디렉토리가 존재하지 않았다고 생각합니다. 사실, HOL/Number_Theory은 최근에 잘못된 이름이었습니다. 나는 Florian Haftmann과 함께 지난 몇 년 동안 그것의 많은 부분을 재구성했으며, 이제는 GCD와 소수성과 같은 것들이 숫자뿐만 아니라 어떤 계승 반지에서도 정의됩니다. 더 나은 분류는 HOL/Algebra이지만, 이미 다른 형식화에 의해 이미 취해진 것입니다.이 형식화는 우리가 한 것보다 훨씬 다른 (더 추상적 인) 풍미가 있습니다.
그래서 배포판 조직의 대부분은 역사적인 사고였습니다. 때로 사람들은 일을 일반화/정리/재편성 할 것이지만 때로는 이런 이유로 인해 이상하게 배치 된 이론이 있습니다.
은 불과 몇 하위 디렉토리를 언급합니다 :HOL/Number_TheoryHOL/Algebra에에 관련된 개념이다.HOL/Analysis입니다.HOL/ProbabilityHOL/LibraryHOL/Decision_Procs에있는에가 '버튼을 누르면에 본질적 속성의 전문 클래스 (예를 들어, 근사 실제 기능, 선형 실제 연산)에 대한 몇 가지 의사 결정 절차가 포함되어 있습니다 증명의 정리 '.HOL/Word은 유한 크기 정수 (즉 고정 비트 길이)에 대한 사실을 포함합니다.HOL/ex은 모든 종류의 항목을 포함합니다. 저는이 디렉토리가 AFP가 존재하기 전에 모든 종류의 작고 전문화 된 개발을 할 수있는 곳이라고 생각합니다.Isar_Examples은 Makarius Wenzel이 구조화 된 언어 인 Isar의 기능을 보여주기 위해 본질적으로 사용 된 것으로 생각합니다. 즉, 멋지게 구조화 된 Isar 증명을 작성하는 일반적인 패턴 및 사례 연구입니다.ROOT 파일은 세션으로 지정되며, 이는 묶어 놓을 이론 모음입니다. 예를 들어, HOL 이미지는 시작시 기본적으로 Isabelle이로드하는 이미지이므로 모든 기본 이론이 다시 처리 될 때까지 몇 분 동안 기다릴 필요가 없습니다. 예 : HOL/Analysis의 자료를 사용하는 경우 HOL-Analysis 세션 이미지를 작성하고 isabelle jedit -l HOL-Analysis으로로드하여 Isabelle을 시작할 때마다 모든 이론을 빌드 할 때까지 기다릴 필요가 없도록하는 것이 좋습니다.document 디렉토리는 ROOT 파일과 함께 작동합니다. 여기에는 Isabelle의 LaTeX 출력이 임베드 된 LaTeX 템플릿이 포함되어 있으며, 일부 PDF (증명 개요 및 증명 문서)가 생성됩니다. 개인적으로, 나는이 코드를 매우 유용하다고 생각하지 않는다. (제 생각에는 Isabelle/jEdit에서 코드를 직접 보는 것이 더 쉽다.)문서 준비 및 세션에 대한 자세한 내용은 the Isabelle systems manual에서 확인할 수 있습니다.