isabelle

1熱度

2回答

我在伊莎貝爾 datatype bc_t = B | C 定義的數據類型之後，並沒有看到如何證明下列基本引理 lemma "∀ x::bc_t . (x=B ⟶ x≠C)" 在證明經過假設B≠C清晰度： lemma "⟦B≠C; x=B⟧ ⟹ x≠C" by metis 有沒有一種方法來證明引理沒有明確的譴責離子B和C是不同的？更新：作爲曼努埃爾EBERL在答案註釋所建議的，問題是

2熱度

1回答

Isabelle：版本的性能問題Isabelle2013-2

我在Isabelle（即最新版本Isabelle2013-2）中遇到性能問題。我使用Isabelle/JEdit，基於新界面。所以之前的情況是我的表現有些麻煩。但現在情況變得更糟了，因爲有時我需要等10秒才能進入正確的狀態。隨着時間的推移，性能問題會變得更糟，因爲我必須在一小時左右後重新啓動Isabelle。我懷疑是我可以更好地配置Isabelle或應用一些提高性能的技巧。硬件：最近 CP

0熱度

1回答

伊莎貝爾：梅蒂斯：證明狀態包含通用排序{}

梅蒂斯給我的警告： Metis: Proof state contains the universal sort {} ("HOL/Tools/Metis/metis_tactic.ML") 這是什麼意思的警告？這是否表明metis證據比沒有警告的「不健康」？

5熱度

2回答

有沒有辦法自動拆分連接？

我想在伊莎貝爾證明A /\ B /\ C /\ D /\ E /\ F。我如何在proof(rule ...)中自動將子目標分成6個子目標，然後我可以單獨證明它們？當然，我可以寫proof(rule conjI) 5次，但也許有一個更優雅的方式來分裂一步？

4熱度

2回答

證明A ==>乙==>ç==>乙在伊莎貝爾

我困惑有關伊莎貝爾證明 A ==> B ==> C ==> B 。顯然你可以 apply simp 但我怎麼能證明這與使用規則？或者，有沒有辦法轉儲使用的規則simp？謝謝。

2熱度

2回答

在伊莎貝爾使用「find_theorems」

我想找到定理。我在Isabelle/Isar reference manual閱讀find_theorems部分： find_theorems標準檢索從理論或證明方面匹配的是給定的搜索標準的事實。標準name: p選擇完全合格的名稱匹配模式p的所有定理，其可能包含「*」通配符。標準intro， elim分別，和dest匹配當前目標作爲導入該選擇的定理，消除或破壞規則。準則solves返回

2熱度

1回答

壞名伊莎貝爾

結合當進入以下定義 datatype env = "nat => 'a option" 伊莎貝爾/ jEdit的顯示了一個感嘆號，並說 Legacy feature! Bad name binding: "nat => 'a option" 這是什麼問題，我如何可以解決此類型的代名詞？更新：即使 datatype 'a env = "nat => 'a option" ，這是更好的理

1熱度

1回答

Isabelle：阻止分裂元組

如何阻止simp方法將元組拆分爲多個元素？示例。如果我寫 fun foo where "foo z = blah z" lemma "∃z :: nat × nat × nat × nat × nat. foo z" 證明狀態∃z. foo z。如果我再寫 apply (simp) 證明狀態變成∃a aa ab ac b. blah (a, aa, ab, ac, b)。我喜歡simp

2熱度

1回答

伊莎貝爾：「結構化」和「應用式」證據

之間的轉換有兩種樣式伊莎貝爾證明：舊的「適用」的風格，證明僅僅是一個 apply (this method) apply (that method) 陳述鏈，和新的「結構化」伊薩爾風格。我自己，我覺得有用; 「應用」風格更加簡潔，因此適用於無趣的技術語法，而「結構化」風格則適用於主要定理。有時我喜歡從一種風格切換到另一種風格，中等防護。從「應用」風格切換到「結構化」風格很簡單：我只需在我的

0熱度

2回答

伊莎貝爾：「介紹IMPI」

如果我的目標狀態是foo ==> bar --> qux的對面，我知道我可以使用語句 apply (intro impI) 產生目標狀態foo ==> bar ==> qux。那另一個方向呢？哪個命令會讓我回到目標狀態foo ==> bar --> qux？我想出了迄今爲止最好的是 apply (rule_tac P="bar" in rev_mp, assumption, thin_tac