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”。但是，“< =”给出≤，其他符号根本不翻译成任何符号。我到目前为止看到的唯一选择是输入类似“>”中的“\ <”或其前缀，并用鼠标选择所需的符号。但是，我想要一个仅键盘输入法。