isabelle

1熱度

1回答

說我有一個引理mylem: foo ?a = bar ?a，我需要它適用於具有的foo，例如出現兩次進球baz (foo (f p q)) (foo (g r s))，但只限於其中一個位置。我知道有兩種方法可以做到這一點，而不必寫出所有p，q ...，這可能是複雜的表達式。使用apply (subst mylem)接着back命令適當數量的（這裏，零或一）。使用apply (subst myl

4熱度

3回答

證明（排除disjE）嵌套脫節

在伊薩爾式伊莎貝爾證明，這很好地工作：這裏 from `a ∨ b` have foo proof assume a show foo sorry next assume b show foo sorry qed 通過proof調用的隱含規則是rule conjE。但是，我應該把有什麼使它的不僅僅是一個脫節的工作： from `a ∨ b ∨ c`

4熱度

1回答

如何在Isabelle/jEdit的假設中顯示括號？

當目標由伊莎貝爾在ProofGeneral顯示，假設被渲染爲具有身邊括號像這樣：在伊莎貝爾/ jEdit的，然而，這似乎已經改變到元蘊涵箭頭：雖然我理解前者是有點不標準，我覺得更容易閱讀。有沒有辦法修改Isabelle/jEdit的行爲來打印舊的ProofGeneral風格的目標？

1熱度

2回答

Isabelle的代碼生成：容器的抽象引理？

我正在試驗代碼生成器。我的理論包含了編碼不變的數據類型： typedef small = "{x::nat. x < 10}" morphisms to_nat small by (rule exI[where x = 0], simp) definition "is_one x ⟷ x = small 1" 現在我想導出代碼is_one。看來，我首先要建立數據類型的代碼生成如下

1熱度

1回答

一個固定的元組參數

歸納謂詞假設我們有一些謂詞 definition someP :: "('a × 'a) ⇒ 'a ⇒ 'a ⇒ bool" 和inductive在它 inductive my_inductive :: "('a × 'a) ⇒ 'a ⇒ bool" for "a_b" where basecase: "fst a_b = a ⟹ my_inductive a_b a" | stepca

4熱度

1回答

如何隱藏定義的常量

當我導入帶有定義常量（用於遞歸函數或定義）的理論文件（如f）時，如何在當前理論文件中隱藏這樣的常量？換句話說，我想確保f是一個自由變量。我不想更改導入的文件。

2熱度

1回答

如何隱藏多重定義的常量

此問題擴展了問題How to hide defined constants。我進口理論A，B和C，也許在未來也D，E ... 所有的理論定義一個函數f。我想在我現有的理論中隱藏f的定義，而不改變導入的理論。當我寫term f我得到A.f。當我將hide_const (open) f添加到我當前的理論中時，隱藏了A.f，但現在我得到B.f爲f。我怎樣才能完全隱藏f？我需要類似(hide_cons

0熱度

2回答

與伊莎貝爾的代碼生成工作：數據細化和高階函數

這是Isabelle's Code generation: Abstraction lemmas for containers?後續：我想在下面的理論the_question生成代碼： theory Scratch imports Main begin typedef small = "{x::nat. x < 10}" morphisms to_nat small by (rul

1熱度

1回答

如何在Isabelle中顯示校樣的時間信息

我有一個證明by eval，它有點慢，我想優化代碼。爲了不盲目地這樣做，如果jEdit可以顯示執行by eval證明所需的時間，那將是非常好的。 Isabelle 2013可能嗎？

2熱度

2回答

什麼類型的定義在當地環境中是合法的？

在伊莎貝爾的NEWS文件，我發現命令「的typedef」現在工作的地方理論範圍內 - 不會對參數和假設引進的依賴，這是不可能在伊莎貝爾/純/ HOL。請注意，邏輯環境可能包含對本地typedefs的多種解釋（不同的非空洞證明），即使在全球理論上下文中也是如此。（可追溯到Isabelle2009-2）。這是關於typedef和當地理論背景的最新消息嗎？此外，「不引入對參數或假設的依賴」的限