isabelle

0熱度

1回答

這裏是一個簡單的類型系統，具有以下類型：any，void，integer，real，set。 datatype ty = AType | VType | IType | RType | SType ty 類型形成確半格： notation sup (infixl "⊔" 65) instantiation ty :: semilattice_sup begin in

0熱度

1回答

對碼公式的左邊

我需要使用nat_plus_commute.fold_set_fold_remdups碼公式，而不是Finite_Set.fold_def部分應用的不斷： interpretation nat_plus_commute: comp_fun_commute "plus :: nat ⇒ nat ⇒ nat" by standard auto declare Finite_Set.fol

2熱度

1回答

如何在函數中使用複雜模式？

下面是一個簡單的功能： fun divide :: "enat option ⇒ enat option ⇒ real option" where "divide (Some ∞) _ = None" | "divide _ (Some ∞) = None" | "divide _ (Some 0) = None" | "divide (Some a) (Some b) = Som

1熱度

2回答

如何查找數據類型的構造函數？

我特林與this one定義類推以下功能： fun int_divide :: "int option ⇒ int option ⇒ real option" where "int_divide _ (Some (int 0)) = None" | "int_divide (Some a) (Some b) = Some (a/b)" | "int_divide _ _ = None

0熱度

1回答

如何取代存在量化變量？

1熱度

1回答

你如何在Isabelle/HOL中使用誘導與戰術/ Isar？

我在努力理解爲什麼下面的每個例子都有效或者不起作用，並且更加抽象地說明誘導如何與戰術和Isar進行交互。我在編程工作4.3與最新的伊莎貝爾/ HOL在Windows 10中伊莎貝爾/ HOL（2016年12月）證明（2016-1）有8例：引理或者是長（包括明確的名稱）或簡短結構化（使用assumes和shows）或未結構化（使用箭頭），並且證明是結構化的（Isar）或非結構化的（戰術性的）。 t

0熱度

2回答

如何映射映射的鍵和值？

我需要定義將鍵映射和有限地圖的值轉換爲一組鍵 - 值對的一個函數： theory Test imports Main "~~/src/HOL/Library/Finite_Map" begin definition denorm :: "('a, 'b) fmap ⇒ ('a × 'b) fset" where "denorm m ≡ " end 的問題是，我不能

0熱度

1回答

如何在locale中定義歸納謂詞？

下面是一個簡單的語言環境的一個示例： locale test = fixes test_less_eq :: "'a ⇒ 'a ⇒ bool" begin inductive test_eq where "test_less_eq x y ⟹ test_less_eq y x ⟹ test_eq x y" end 它定義感應test_eq。它可以使用definit

0熱度

1回答

如何合併一組有限地圖？

我可以合併兩個有限的地圖如下： value "fmadd (fmap_of_list [(1::nat,2::nat)]) (fmap_of_list [(2::nat,3::nat)])" 但是，當我嘗試合併組映射： value "ffold fmadd fmempty {| fmap_of_list [(1::nat,2::nat)], fmap_o

0熱度

2回答

如何在Isabelle/jEdit中輸入集合論的符號？

如何在Isabelle/jEdit中輸入像∈，⊆，∪和∩這樣的符號？ Isabelle/HOL教程說，我應該輸入「：」，「< =」，「Un」和「Int」。但是，「< =」給出≤，其他符號根本不翻譯成任何符號。我到目前爲止看到的唯一選擇是輸入類似「>」中的「\ <」或其前綴，並用鼠標選擇所需的符號。但是，我想要一個僅鍵盤輸入法。