考慮下面的語言環境定義： locale my_locale =
fixes a :: nat
assumes "a > 0"
begin
definition "f n ≡ a + n"
lemma f_pos: "f x > 0"
sorry
end
在伊薩爾，如果我試圖用f定義或引理f_pos工作，語言環境的假設和固定變量都向我隱瞞。例如，thm
最近了解到how to drop an unwanted premise in an apply-style proof，我現在想知道如何刪除不需要的變量變量。也就是說，假設我有目標 1. !!x y z. A ⟹ B ⟹ C
其中y不A，B或C出現。我如何將它轉換爲以下內容？ 1. !!x z. A ⟹ B ⟹ C
我們假設我們正在使用一對類型爲('a × 'a)並定義一個fun併爲其設置模式匹配。 fun test :: "('a × 'a) ⇒ 'a ⇒ bool" where "test (a,b) c = True"
如果我現在有('a × 'a)類型的變量a_b，我怎麼能代替它變成了對錶示(a,b)在應用樣式的證明。例如，顯示以下引理的最佳方式是什麼？如何將test a_b c替換爲test (
鑑於我有一個非常簡單的代碼生成定義。它僅在某些情況下被定義，否則會引發運行時異常。 definition "blubb a = (if P a then True else undefined)"
現在我想顯示blubb正確。應該忽略拋出異常的情況（從我的觀點來看，不是數學觀點）。然而，我最終得到一個子目標，它假設X是undefined的一些任意值。下面的引理或多或少地等同於子目標。我想顯示F