0
我是新的Isabelle/Hol用戶，我對使用Isabelle中的現有定義存在一些困惑。我必須在我的模型中定義完整的晶格結構和完整的偏序（CPO）結構。我發現這些定義已經作爲HOLCF Porder.Thy和Lattice.thy中的類存在。所以如果我想將這些定義包含在我的模型中，我應該如何繼續？像我複製粘貼所有的定義或有一個特定的命令？使用Isabelle中的現有定義/ Hol
感謝
A
回答
0
在你自己的理論的頭，你可以導入其他理論。完整的格子已經存在於理論中（如果你使用HOL，你通常會導入）。其他理論可以使用~~/src/HOL/...（Isabelle自動將~~替換爲Isabelle安裝的主路徑）引用。
對於精確的語法，我建議通過prog-prove閱讀，特別是§2.1。
相關問題
- 1. Isabelle/HOL中的Int理論問題
- 2. Isabelle/HOL中的向量轉置
- 3. 如何從Isabelle/HOL生成LaTeX？
- 4. 你如何在Isabelle/HOL中使用誘導與戰術/ Isar？
- 5. Isabelle/HOL：'simp'的證明是緩慢的，'value'是瞬時的
- 6. 在Isabelle中定義quotient_type
- 7. Isabelle：如何使用矩陣
- 8. 自定義Isabelle語法打破現有語法
- 9. 在證明isabelle/hol中的解釋時的多態「修復」語句
- 10. 在Isabelle中定義3乘3矩陣
- 11. 在Isabelle中定義重載常量
- 12. libisabelle與現有的Isabelle安裝
- 13. 在Isabelle中定義用於乘法的初始遞歸
- 14. 在Isabelle中的實例化定理
- 15. Isabelle：矩陣的功效（A^n）？
- 16. 如何在android中使用現有的/預定義的表格？
- 17. 在Linux上構建Isabelle ARM
- 18. 在界面生成器中使用現有的自定義UIView
- 19. Isabelle中的文檔編寫
- 20. Isabelle中的（*> *）是什麼？
- 21. Isabelle：如何打印1 + 2的結果？
- 22. 生成Isabelle HTML文檔*無需校樣*
- 23. 試圖瞭解在伊莎貝爾「語法」關鍵字/ HOL
- 24. 如何證明時/在伊莎貝爾/ HOL
- 25. 如何在Isabelle/jEdit中輸入集合論的符號？
- 26. Isabelle - Nitpick - 自動使用見證值
- 27. 如何在不使用類的現有C＃程序中使用自定義類？
- 28. 有沒有辦法使用Object.keys（）來實現Nashorn JSObject的自定義實現？
- 29. Isabelle：多項式次數乘以常數
- 30. 使用Isabelle開發版本有什麼缺點？
謝謝larsh爲您的答案，我已經移植完成Latices和完整的部分秩序的理論，我的混淆是如何啓動他們在我的模型，我困惑地方和類風格，所以我在尋找對於一個簡單明確的例子來說明它是如何完成的，現在我只是定義了另一個calss cpo_T來表示一個名爲T +的cpo結構，它是關於函數連續性的定義，但我不確定它是如何完成的 class cpo_T = cpo + 假設c：「鏈C⟹（⨆i。f（C i））= f（⨆i。C i）」 開始 結束pdf不回答我的問題 –