isabelle

0熱度

1回答

我想了解實施伊莎貝爾/ HOL線性邏輯：https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/ILL.html對於不syntax關鍵字代表什麼，什麼是代碼的意思是： syntax "_Trueprop" :: "single_seqe" ("((_)/ ⊢ (_))" [6,6] 5)

0熱度

1回答

有限域映射

我需要一個數據類型的有限映射。我使用典型的（部分）地圖，直到我在證明中碰到一個路障，只能通過引入一個finite (dom m)謂詞來修復。將這個事實進行到底是乏味的，那麼標準庫中是否有一些解決方案呢？

2熱度

1回答

證明兩個特定集合在Isabelle中具有相同的基數

我很難證明兩個集合具有相同的基數。以下所有集合都是有限的。首先假設我們已經設定了（M :: b集合）和函數foo ::「b集合⇒b集合⇒bool」使得（foo AC = foo BC⟷A = B）和對於M中的每一個A，實際上都有一個C，這樣foo A.C. 我試圖證明那張卡{S。 ∃A∈M。（S = {C.foo A C}）} = card M. 對此的非正式證明是顯而易見的，但我似乎無法

0熱度

1回答

如何HOLCF證明清單的雙重逆轉並沒有改變它

下面是一個簡單的理論寫在普通HOL： theory ToyList imports Main begin no_notation Nil ("[]") and Cons (infixr "#" 65) and append (infixr "@" 65) hide_type list hide_const rev datatype 'a list = Nil ("[]")

0熱度

1回答

如何分析假設中的if-expressions？

我試圖證明以下引理： lemma if_assumption: "(if a = 1 then 2 else 3) = 2 ⟹ a = 1" apply (cases "a = 1") apply simp_all 簡化後我得到以下公式： 3 = 2 ⟹ a ≠ 1 ⟹ False 如果表達式的結果等於2 IFF a等於1。所以，我猜測我可以以某種方式推斷這個事實。如

1熱度

1回答

如何在伊莎貝爾證明最大交換性質

我對伊莎貝爾非常新，所以請有憐憫。如何用此功能證明最大交換屬性？ fun max :: "nat => nat => nat" where "max 0 0 = 0" | "max (Suc x) 0 = Suc x" | "max 0 (Suc x) = Suc x" | "max (Suc x) (Suc y) = Suc (max x y)" lemma "max x y = m

0熱度

1回答

如何用重疊模式定義函數？

我試圖定義4值邏輯（假的，真實的，無效和錯誤）連詞功能： datatype 'a maybe = Just "'a" | Nothing | Error type_synonym bool4 = "bool maybe" abbreviation JF :: "bool4" where "JF ≡ Just False" abbreviation JT :: "bool4" where "

0熱度

1回答

收斂和向量理論

Isabelle/HOL中是否存在收斂理論？我需要定義∥x(t)∥ ⟶ 0 as t ⟶ ∞。此外，我正在尋找向量理論，我找到了矩陣理論，但我找不到向量之一，Isabelle/HOL中是否存在這樣的理論？乾杯。

1熱度

1回答

Isabelle/HOL：'simp'的證明是緩慢的，'value'是瞬時的

我是Isabelle/HOL的新手，仍然在研究鍛鍊練習。與此同時，我正在通過將這些證明技巧應用於組合詞的問題來鍛鍊。我觀察到一個非常不同的行爲（效率方面），在'價值'和'引理'之間。能解釋兩個命令之間的不同評估/搜索策略嗎？有沒有一種方法可以在「引理」的證明中使用「價值」的速度？當然，我在問，因爲我還沒有在文檔中找到答案（到目前爲止）。什麼是手冊，這種效率差異將被記錄和解釋？下面是重現問題

0熱度

1回答

Isabelle/HOL中的向量轉置

我找不到在Finite_Cartesian_Product理論中轉置(real,'n) vec類型向量的定義或引理。例如，如果矢量e = A x然後是e（e^T）的轉置導致轉置A和x（e^T = A^T x^T），我試圖用轉置矩陣和矢量來代替轉置矢量。我可以在Isabelle/HOL中做到這一點嗎？