考慮理論
theory Scratch imports Main
begin
notepad
begin
fix P and f g h :: "int ⇒ int"
assume prems: "P f" "P g" "P h"
assume comp: "⋀ f g. P f ⟹ P g ⟹ P (λ x. f (g x))"
have "
我有點驚訝， value "let x = SOME n. n ∈ {1::int,2} in x = x"
回報True。 β擴張和α重命名後，該術語與以下內容相同： value "(SOME na. na ∈ {1::int,2}) = (SOME nb. nb ∈ {1::int,2})"
我不明白爲什麼這種平等應該成立。爲什麼選擇na的值應該與nb的值相同？
我發現record ⦇ field := value ⦈表示法在我用它在過程中更改record的類型參數時無法正常工作。爲了澄清我的意思，請看下面的例子：由於錯誤類型 theory Scratch imports
Main
begin
record 'a john =
apple :: 'a
banana :: int
definition f :: "na
如果我寫一個非平凡的遞歸函數（即使用function而不是fun），那麼代碼生成器拒絕執行我的功能，除非我提供終止證明 - 即使是sorry防爆足夠。這是我最小的工作示例（不用擔心foo函數的內容，它只是一個不平凡的終止證明隨機函數）： theory Misc imports
Main
"~~/src/HOL/Library/Code_Target_Numeral"
begi
伊莎貝爾的新品牌，以及一般的HOL編程。 教科書中的練習之一是： 定義一個遞歸函數double :: nat⇒nat並證明double m = add m m。 im仍然試圖定義它，但我無法弄清楚。， 這是我迄今爲止所做的。 fun double :: "nat => nat" where
"double 0 = 0" | //my base case
"double (n) = //I do
我努力證明我的inductive_set滿足必要的單調性要求。有人能告訴我在這裏做錯了嗎？ theory Scratch imports Main begin
consts foo :: "'a set ⇒ 'a set"
lemma foo_mono [mono]:
"x ⊆ y ⟶ foo x ⊆ foo y"
sorry
inductive_set blah :: "'a s