isabelle

1熱度

1回答

~~/src/HOL/Word/Word.thy中有一個稱爲word_rsplit的功能。 definition word_rsplit :: "'a :: len0 word => 'b :: len word list" where "word_rsplit w = map word_of_int (bin_rsplit (len_of TYPE ('b)) (len_of

4熱度

3回答

如何啓用「追蹤」在伊莎貝爾/ jEdit

我是vim風扇，但只有emacs有此Isabelle/HOL環境。的jEdit是偉大的，但我不能在emacs的使用 using [[simp_trace=true]] 等。如何啓用「追蹤」jEdit？

0熱度

1回答

Isabelle：多項式次數乘以常數

我正在與圖書館HOL/Library/Polynomial.thy合作。一個簡單的屬性不起作用。例如，中2x *2度等於2x程度 - 我如何證明引理（即去掉「對不起」）： lemma mylemma: fixes y :: "('a::comm_ring_1 poly)" and x :: "('a::comm_ring_1)" shows "1 = 1" (* dummy

1熱度

1回答

證明氣泡排序是由詞條排序

我已經試過證明樂趣bubble_main是有序的，但沒有辦法似乎工作。請問這裏有人能幫我證明引理is_ordered (bubble_main L)。我剛剛刪除了我以前的所有引理，因爲似乎沒有任何幫助Isabelle找到一個證明。這裏是我的代碼/理論：所有的 text{*check if the list is ordered ascendant*} fun is_sorted :: "na

1熱度

1回答

Isabelle：矩陣的功效（A^n）？

有在Cartesian_Euclidean_Space矩陣乘法定義（在目錄HOL/Multivariate_Analysis「）： definition matrix_matrix_mult :: "('a::semiring_1) ^'n^'m ⇒ 'a ^'p^'n ⇒ 'a^'p ^'m" (infixl "**" 70) where "m ** m' == (χ i j

2熱度

1回答

伊莎貝爾瑣碎的問題：「馬克斯（S :: NAT設置）= 0」意味着S的所有元素都爲零

我試圖證明如下含義： lemma Max_lemma: fixes s::nat and S :: "nat set" shows " ((Max S) = (0::nat)) ⟹ (∀ s ∈ S . (s = 0))" sorry (* Note: I added additional parentheses just to be sure.*) 我想這將

10熱度

1回答

如何從Isabelle/HOL生成LaTeX？

如何使用Isabelle/HOL從我的源文件文件自動生成LaTeX？伊莎貝爾/ HOL的tutorial.pdf非常漂亮。我要在LaTeX上寫一篇文章，裏面有很多Isabelle代碼。

3熱度

2回答

Isabelle中的文檔編寫

我想使用isabelle build -D xxx從Isabelle .thy文件中生成LaTeX .tex文件。但Isabelle檢查所有理論依賴關係，並且必須涉及所有相關的.thy文件。是否有可能我隨便用.thy文件有語法錯誤產生.tex文件？事實上，我只需要它的一部分來寫一篇論文。

1熱度

1回答

轉移更高訂單目標

我試圖使用轉移包爲自定義數據類型建立歸納規則，但apply transfer不適用於我。下面是一個簡單的例子： theory TransferHO imports Main begin typedef pos = "{x :: nat. x > 0}" by blast setup_lifting type_definition_pos lift_definition one :: po

3熱度

1回答

如何證明時/在伊莎貝爾/ HOL

我有這樣的C代碼： while(p->next) p = p->next; 我想證明，無論列表有多長，當這個循環結束，p->next等於NULL，並EIP指的是這個循環之後的下一條指令。但我不能。有沒有人知道如何證明在Isabelle/HOL？