我最近開始使用Isabelle定理證明。因爲我想證明另一個引理，所以我想使用與在「HOL庫」中找到的引理「det_linear_row_setsum」中使用的不同的符號。更具體地說，我想用「χi j notation」而不是「χi」。我一直在嘗試制定一個等價的表達式，但還沒有弄明白。 (* ORIGINAL lemma from library *)
(* from HOL/Multivaria
我正在尋找一個自動定理證明系統，它可以證明這一點： 鱷魚帶芒人的孩子。男人讓鱷魚不要吃他的孩子。但鱷魚說：如果你會告訴我，我會把你的孩子交還給你，我將如何處理他。 解析解他看起來像這樣： X - 鱷魚會吃小孩 Ÿ - 男人的答案：鱷魚會吃小孩 〜意味着平等，！指的不是， - >暗示，+ OR; ((x~y)->!x) and ((x XOR y)->x) =
(x! and y +!x and
我試圖證明如下含義： 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.*)
我想這將
在我的伊莎貝爾理論上我有一個常數因子矩陣： ...
k :: 'n and c :: 'a
(χ i j. if j = k then c * (A $ i $ j) else A $ i $ j)
我可以計算轉置矩陣： (transpose (χ i j. if j = k then c * (A $ i $ j) else A $ i $ j))
在我眼裏後者應相當於 (χ i j
爲了掌握Coq的內容，我最終需要證明a=b -> nat_compare a b = Eq。 我可以做得到一個方便的開始： Coq < Theorem foo: forall (a:nat) (b:nat), a=b->nat_compare a b=Eq.
1 subgoal
============================
forall a b : nat, a = b ->
我做了一個叫做的記錄類型，並且我定義了一個合適的「是關係的子圖」。我想說明一組圖和子圖關係形成一個順序，即是類的一個實例。但我無法讓它工作。這是我最小的工作例如： theory John imports
Main
begin
typedecl node
record graph =
nodes :: "node set"
edges :: "(node ×
我希望爲Isabelle理論（例如HOL會話）生成HTML文檔，但不包含的校樣。 也就是說，我想產生像http://isabelle.in.tum.de/library/HOL/Nat.html 而是，例如網頁， lemma diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
(!!x y. P x y ==> P (Suc x)