问题标签 [isar]

证明一个简单的定理我在证明中遇到了元级含义。可以拥有它们还是可以避免它们？如果我应该处理它们，这是正确的方法吗？

我想这可以更容易地证明，但我想要一个结构化的证明。

我的一些当地人有很多假设，非常类似于对数据类型的归纳（这就是假设的来源）。在解释这样的语言环境时，命名案例会非常方便。我如何实现以下工作？

我刚刚写了这段代码：

其中step.intros实际上只有 5 个引理。有没有一种方便的方法来避免这种重复，即看起来像下面这样的东西？

假设我在 Isabelle/HOL 中有以下表达式：

这应该为 Person 和 Car 类型建模，它们之间有两个关系，命名为 drive 和 owns，还有 Person 的 age 属性。

我想说每个有车的人肯定会开车，而且开车的人都大于17岁，所以限制条件：

在 Isabelle 中定义此类约束的最佳方法是什么，从某种意义上说，假设这些约束成立，我可以证明模型的某些属性？

我在伊莎贝尔有以下代码：

自动证明方法工作正常并证明了引理！当我想将引理中前提的第一部分分解为定义 C1 时，如下所示：

auto方法无法在以下代码中证明：

为什么会这样？如果我在分解第一个假设的方式上做错了——我这样做是为了组织假设看起来整洁和结构化——不影响证明方法的最佳方法是什么（自动）功能。

谢谢

假设我在 Isabelle 中有以下代码：

在上面的代码中， simp 方法证明了引理。我有兴趣查看并打印出简化方法用来证明这个引理的详细（重写/简化）步骤（并且可能能够对所有其他证明方法做同样的事情）。这怎么可能？

我正在使用带有 JEdit 编辑器的 isabelle 2014。

非常感谢

假设我在 Isabelle 中有以下代码：

当我想对 A 和 B 使用联合操作时，如下所示：

由于 A 和 B 是不同类型的集合，因此我得到了类型冲突的错误，这是有道理的！作为一种解决方法，我想将强制转换 A 和 B 都输入为“type3”类型的集合，这样我就可以对它们应用联合操作。在这个具体的例子中，这种类型转换在 isabelle 中是如何实现的，以及一般情况下是如何实现的。

谢谢

我在伊莎贝尔有以下代码：

当我想对 A 和 B 使用联合操作时，如下所示：

由于 A 和 B 是不同类型的集合，因此我得到了类型冲突的错误，这是有道理的！

我想知道是否有任何对应的集合操作，他们隐含地将其操作数视为纯集合（即忽略它们的类型），因此像 A ∩' B 这样的东西成为可能（∩' 在上述意义上是 ∩ 操作对应物）。

PS：另一种解决方法是类型转换，我在这里将其作为一个单独的问题编写，以更好地组织我的问题。

谢谢

关于 Isabelle 中的子类型的问题在这里非常冗长。所以我的简单问题是，如果我将 A 定义如下，我如何将类型 B 定义为 A 的子类型：

通过这样做，我想让 B 类型的元素可以访问在 A 上定义的所有操作和关系（它们未在此处打印）。

一个更复杂的例子是将 B 和 C 定义为 A 的子类型，这样 B 和 C 是不相交的，并且 A 的每个元素要么属于 B 类型，要么属于 C 类型。

谢谢

我问了一系列问题以达到我可以在 Isabelle 中定义以下简单模型的目的，但我仍然坚持得到我想要的东西。我尝试用一​​个例子非常简要地描述这个问题：

例子：

假设我有两个类Person和Car，Person 拥有汽车并驾驶汽车。所以我需要以下类型/集：

人

车

拥有 （*拥有将人的元素与汽车相关联*）

驱动器 （*驱动器也将人的元素与汽车相关联*）

问题：

我想在 Isabelle 中制定上述示例是一种提供以下灵活性的方式：

1. 使我能够定义一些约束；例如：如果一个人拥有一辆车，他/她肯定会开车。我可以通过使用来自这里的友好答案来做到这一点。

2. 让我能够定义一个新的集合/类型，即C，其元素是Car和owns元素的不相交并集。这是我坚持的第一个地方：Car和owns是不同的类型，那么我该如何合并它们？

3. 能够在数（2）个中多次继续该过程；例如，定义一个新的类型/集合，即D ，它是C和驱动器的不相交并集。

在数字（2）和（3）中，我想保留新定义的集合/类型的元素的属性/特征；例如，如果我要为 Person定义一个属性age （请参见此处），我希望C的元素保留此属性，因为我可以访问C中类型为 Person 的元素的此属性。因此，如果 o1 是C中类型为owns的元素，我想访问与 o1 相关的源（即 Person）和目标（Car）。

我将不胜感激任何意见和建议。