4

发布答案跟进问题

Brian 提供了一个答案，建议的解决方案是使用提升和转移。但是，我找不到足够的关于提升和转移的教程信息来了解如何调整他的答案以完成我需要做的事情。

在这里，我在黑暗中工作，并使用作为即插即用模板给出的答案来提出这个后续问题。

我初始代码中的命令为我typedef trivAlg = "{x::sT. x = emS}"提供了一个新类型，它是母类型的子集sT。

我有我的会员操作员consts inP :: "sT => sT => bool"，所以在我对提升和转移的天真看法中，因为我的monoid_add0 已被定义为常量emS::sT，我可以做出这样的声明，(emS::sT) inP emS我想做这样的事情：

theorem "~((0::trivAlg) inP 0)"

所以，我尝试使用提升让我的操作员使用这样inP的类型trivAlg：

lift_definition inP_trivAlg :: "trivAlg => trivAlg => bool"
  is "% x y. (x inP y)" 
  by simp

theorem "~((0::trivAlg) inP 0)"

theorem "(emS::trivAlg) = emS"

theorem但是，由于我使用的类型sT与我的使用trivAlg不兼容，因此我遇到了类型冲突。

如果可以添加答案以向我展示如何让我inP使用类型，trivAlg我将不胜感激。或者，也许我离题了。

（原始）问题的预备知识

我有我的 type sT，它代表“一切都是一个集合”。到目前为止，我所有的常量和操作符都是用单一类型定义的sT。例如，我的空集、成员运算符和联合运算符定义如下：

consts emS :: "sT"
consts inP :: "sT => sT => bool"
consts geU :: "sT => sT"

我现在正在做一些早期调查，以了解我是否可以将 my与Groups.thysT中的广义组联系起来。

从HOL 文档中，我试图从 Groups 的 4.2、4.3 和 4.4 节以及 Nat 的 15.2 和 15.3 节中获取示例。

在这里，我几乎要回答我的问题，但我不知道我是否在问一个聪明的问题。我想我知道的是，解决方案可能只使用语言环境、子语言环境和解释，而不是类型类。

我一直在看locales.pdf和classes.pdf，所以我知道语言环境和类是交织在一起的。我也一直在查看IsarMathLib以了解在那里如何使用语言环境、子语言环境和解释。

问题

我的问题是，在下面我的微不足道的代数结构中trivAlg，这是一个用 定义的新类型typedef，我如何使用类型类进行设置，以便我可以将我的常量（例如emS，上面列出的）inP与geUtype 的元素一起使用trivAlg？

在我列出下面的代码之后，我会问一些关于Groups.thy中特定代码行的问题。

编码

typedef trivAlg = "{x::sT. x = emS}"
  by auto

instantiation trivAlg :: zero
begin
definition trivAlg_zero:
  "0 = Abs_trivAlg emS"
instance ..
end

instantiation trivAlg :: monoid_add
begin
definition plus_trivAlg:
  "m + n = (Abs_trivAlg emS)" 
instance proof
  fix n m q :: trivAlg
  show "(n + m) + q = n + (m + q)"
    by(metis plus_trivAlg)
  show "0 + n = n"
    apply(induct n) apply(auto)
    by(metis plus_trivAlg)
  show "n + 0  = n"
    apply(induct n) apply(auto)
    by(metis plus_trivAlg)
qed
end

theorem
  "((n::trivAlg) + m) + q = n + (m + q)"
  by(metis plus_trivAlg)

theorem
  "((0::trivAlg) + 0) = 0"
  by(metis monoid_add_class.add.left_neutral)

关于 Groups.thy 的后续问题

在 Groups.thy 的第 151 到 155 行，有以下代码：

class semigroup_add = plus +
  assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)"

sublocale semigroup_add < add!: semigroup plus proof
qed (fact add_assoc)

没有一个文档可以教我如何使用类、语言环境、子语言环境和解释，所以我不知道它到底告诉了我什么。

如果我想使用semigroup_addGroups.thy 中的那个，我可以选择将它用作类型类还是区域设置？

4

2 回答 2

3

要获得对 type 的相应操作trivAlg，可能最简单的方法是使用 Isabelle 的 Lifting 包；然后，您可以使用 Transfer 包来证明类实例。这是一个例子：

typedef trivAlg = "{x::sT. x = emS}"
  by auto

setup_lifting type_definition_trivAlg

instantiation trivAlg :: zero
begin
lift_definition zero_trivAlg :: "trivAlg" is "emS" .
instance ..
end

instantiation trivAlg :: monoid_add
begin
lift_definition plus_trivAlg :: "trivAlg => trivAlg => trivAlg"
  is "% x y. emS"
by simp

instance proof
  fix n m q :: trivAlg
  show "(n + m) + q = n + (m + q)"
    by transfer simp
  show "0 + n = n"
    by transfer simp
  show "n + 0  = n"
    by transfer simp
qed
end
于 2013-04-08T22:51:55.030 回答
1

如果我不知道语法的含义，那么简单的事情会害死我，并且学习 Isabelle/HOL 的大部分内容是“长时间盯着多个示例”，这并不是说 Isabelle 相对于其他证明助理。

在这里，我完成了关于如何实际使用 Brian 给我的东西的问题。

MyinP实际上是 function 的二进制表示法in_P :: sT => sT => bool，这就是我想要提升到 type的内容trivAlg，尽管我不确定我刚刚正确使用了“lift”这个术语。

从Isabelle 用户列表中，我找到了一个显示 HOLunion运算符提升的示例。同样，我in_P这样举起我的：

lift_definition in_P_trivAlg :: "trivAlg => trivAlg => bool"
  is "in_P :: sT => sT => bool" 
  by simp

在我之前的尝试和错误尝试中，我一直在使用 my inP，它只是一个符号，它并没有陷入lift_definition引入一个全新的功能。那些事情终于发生在我身上，而不是“试错”，我通过in_P_trivAlg智能使用这个功能得到了“试错”：

theorem "~(in_P_trivAlg 0 0)"
  by(metis 
    Ax_em 
    in_P_trivAlg.rep_eq 
    zero_trivAlg.rep_eq)

这表示空集不包含自身。这很好，并告诉我我走在正确的轨道上，考虑到 0 已被定义为emS，它被定义为公理Ax_em，不包含任何元素 。

我现在需要弄清楚如何重载我的成员运算符符号\<in>\<^isub>\iota>。直到现在，重载符号并不重要，因为我需要不重载大多数标准符号，例如\<in>.

看起来我需要重命名定理，例如in_P_trivAlg.rep_eq，而我刚刚从“我可以为一个定理定义多个名称吗？”中得到答案。.

从RealVector.thy，我现在看到使用lemmas命令进行了很多重命名，例如

text {* Recover original theorem names *}

lemmas scaleR_left_commute = real_vector.scale_left_commute
lemmas scaleR_zero_left = real_vector.scale_zero_left
...

如果不是我刚刚提供了一个链接的 Stackoveflow 答案，那么该代码的目的对我来说毫无意义。

于 2013-04-09T15:54:31.627 回答