在 Isabelle/HOL 中修复附加变量之前保存数据类型

如何解决在 Isabelle/HOL 中修复附加变量之前保存数据类型

我对 Isabelle 还很陌生，我在打字时遇到了一些麻烦：我想要两个独立但重叠的类型，比如“a”和“b”。将它们视为集合，我希望将 'b = 'a \cup {tau} 用于未出现在 'a 中的特定 tau。据我了解，您可以在 Isabelle 中使用“fixes tau :: 'a”扩展类型，但似乎原始类型 'a （没有 tau）丢失了： Current Isabelle code using fixes

我在以后的公式中需要这两种类型，那么有没有办法在将 tau 固定到它之前“保存”'a 的状态？

任何帮助将不胜感激！

解决方法

您误解了语言环境。修复引入了某种类型的常量。记住语言环境的含义：

locale t =
   fixes x
   assumes "P x"
begin

lemma b: Q 
  sorry

表示“!!x。P x ==> Q”。您没有扩展类型。

关于实际问题：您不能直接扩展类型或直接在 HOL 中表达。这是不可能的。在实践中扩展类型有两种解决方案：

• 一种数据类型 datatype 'a myunion = Either1 'a | Tau。在这种情况下，它实际上与 'a option 同构。
• 联合类型（参见 here for another SO question on the topic）