我对总和中的 if 语句有疑问。

我在另一个关于isabelle 中的 if 语句的问题中检查了解决方案， 但它没有帮助。

这是一个例子：

我如何证明“对不起”所在的引理？

矩阵和 A * 1 *A ** mat 1`之间有什么区别？**and

例子：

我不确定，但我认为有时如果我有一个前置函数，我的证明会更容易，例如，如果已知变量不为零。

我不知道一个很好的例子，但也许在这里：{ fix n have "(n::nat) > 0 ⟹ (∑i<n. f i) = Predecessor n" sorry }

可能是因为这不是一个好主意，所以库中没有前置函数。

有没有办法模拟前任功能或类似功能？

我想到了这个例子：

如何阻止该simp方法将元组拆分为其组件？

例子。如果我写

证明状态是∃z. foo z。如果我再写

证明状态变为∃a aa ab ac b. blah (a, aa, ab, ac, b)。我喜欢它simp已经扩展foo到blah，但我宁愿它保持我的变量不变z。

在这里，我要求证明 Isabelle 元逻辑合取消除规则。

下面的来源包含我的评论，这些评论解释了我在做什么。在理论上，有两对元假定义和连词消除规则。两对如下：

• falseH, andH_E1, 和
• falseM, andM_E1.

我的andM连词(P ==> Q ==> falseM) ==> falseM)形式是 ，我无法简单地证明这种形式。

将来，我计划使用类似于andM上述的元逻辑运算符来复制 HOL.thy 自然演绎规则。作为其中的一部分，运算符==>将被视为原始运算符。因为 Pure 运算符!!在与 相同的意义上也是原始的==>，所以我猜我可能无法开发有助于我使用元假定义的规则!!P. PROP P，因为我在下面使用它。不过，我可能是错的。

这不像我必须有falseM我在下面尝试使用的，因为falseH有利于simp已经与 HOL 结合使用的魔法，双关语不是故意的。虽然我不必拥有它，但拥有它会很好。

更新 (131211)

我用三件事对此进行了更新，其中两件事与 Andreas 的回答有关，即需要排除中间公理。我在下面所说的并不是对任何事情的真正答案，并且可以接受更多评论，因为我在简单的事情上可能会出错。

我把我的冗长评论放在这里是为了巩固一些与我的问题的核心思想相关的想法，即如何使用元逻辑假来定义元逻辑运算符。

1. 我展示了我认为我将如何在语言环境中添加排除中间的元逻辑公理。
2. 我展示了是什么让我理解了我需要什么形式的排中公理。大多数文献都会说排中是P or not P，这是具有欺骗性的，因为我很少考虑排中，因为它已经根深蒂固了我的思想。
3. 我注意到这"(P &&& Q) ==> P是由conjunctionD1in证明的conjunction.ML，而展开的版本是由 证明的meta_allE。我想知道为什么不能操纵内部而不是外部andM，!!以便可以证明它。

将元逻辑排除在语言环境中

因此，Adreas 指出 Isabelle/Pure 没有排中，而我需要它，从而为我节省了几个月，可能至少一年，甚至可能是多年徒劳无功的计划。这有助于回答我的相关问题，并帮助我更了解 Isabelle/Pure 是什么。

如果强制我使用 HOL 排除中间，我会使用False, 而不是(!!P. P::bool).

如果我想要一个元假，我想我会在这样的语言环境中添加一个元逻辑排除中间：

就像我说的，这不是一个答案，因为我必须解决它。

从 Andreas 提供的证明中，有classical来自 HOL：

像这样的 HOL 定理的证明步骤告诉我元逻辑版本需要什么。我通过提供 locale axiom 做了简单的部分t_or_f。其余的只是简单的工作。

伊莎贝尔/纯没有排除中间

在这里，我不只是为了说话而说话，我有时会这样做，但我投入了我的努力，以了解==作为被排斥的中间人所需要的一部分。我可能需要再看一遍这一切，所以也许它不会对我不利。

首先，跳到我接下来要说的关于 HOL 引理的内容之前excluded_middle，一个人，尤其是我，也会想考虑这个 HOL.thy公理，第 171 行：

Andreas 指出排中律是必需的，而 Pure 没有提供它。这是HOL.thy名为 的定理 excluded_middle，第 604 行：

类似地，我将其声明为一个元逻辑定理falseM，其中我的元或是(P ==> falseM) ==> Q，元非是P ==> falseM。

如果元或符号被定义为掩盖它实际上是什么，逻辑新手（当然不是我）可能不会将其识别为“如果 P 为假，则 P 为假”，而不是需要什么，“如果 P 不为假，那么它一定是真的”。

更新（131213）：我把这个放进去是因为我忘记了我为什么做某事，然后当我试图通过逻辑重新工作时，我想我搞砸了，当我没有搞砸的时候，虽然我的逻辑意识可能没有已经完成。

我实际上并没有实现 的元逻辑版本~P | P，而是P | ~P. 如果它不明显，可能是，我使用基于真值表的蕴涵定义以及德摩根定律，并使用逻辑的基本定理，这最终对我来说必须是正确的。

但是，我现在正在对排中公理进行事后研究，这使得我使用的事实P | ~P不太可接受，因为它变成了"((P ==> falseM) ==> falseM) ==> P"，这涉及双重否定，我隐约记得这与这一切有关。直到现在，我一生中从来没有关心过排中。这应该是建构主义者的想法。

我做出这个转换实际上是很幸运的，因为这让我看到了=in的重要性True_or_False。

一个有意义的定理将是“不是（P 而不是 P）”（或者会吗？）。所以我在 meta-and 表达式中 替换(P ==> falseM)。Q(P ==> Q ==> falseM) ==> falseM

这已经完全发挥了逻辑傻瓜的红色警报，因为falseM 不必扩展。现在，我陈述相同的定理，但没有 bool变量和没有，以明确表示它与orfalseM无关。falseMbool

回到我一开始跳到的内容，我现在看到一个关键的区别是运算符=被用于True_or_False.

现在，我陈述一个元逻辑形式，True_or_False它使用 operator ==，元或 as (P ==> falseM) ==> Q，真部分为(P == (falseM ==> falseM))，假部分为(P == falseM)。

这终于让我得到了一个有意义的排中元逻辑陈述，其中falseM需要扩展。我无法证明这一点，这本身没有任何意义，或者反驳它，这意味着我可能完全糊涂了。

这说明了为什么我必须学习大量低级逻辑才能与定理助手一起工作，而我的最终目标是高级数学，传统上不需要这种知识。

没有很好地理解没有排除中间的重要性最终杀死了我，除其他外。

为什么可以"(P &&& Q) ==> P"证明以上？

上面的方法还是有(P &&& Q) ==> P可以证明的意义的linarith，在presburger哪里是这样的：&&&pure_thy.ML

我的 meta-and, using falseM，实际上只是将 use!!从外部移动到内部，曾经falseM被扩展。

在这里，我证明了元和消除的扩展术语，并使用Pure.conjunctiond1.

规则conjunctionD1在conjunction.ML，似乎forall_elim_vars 正在照顾运营商!!，我想这只是在做同样的事情meta_allE。

我可以使用标准的 Meta-And，但 Meta-And 不是目标

我比较了连词消除规则的两个扩展版本。第一项使用标准&&&，第二项使用我的andM。

使用&&&可以很容易地证明第一项meta_allE，如上所示。

在我看来，我应该能够将第二项操纵成第一项的形式，但我不知道。如果这是真的，那么我不需要为这个定理添加排中公理。在学习了很多自然演绎之后，我会知道，就像我需要的那样。

如果我的目标只是元逻辑运算符，我会使用&&&，但这不是我的目标。我的目标是定义一个 meta-false 用于缩写元逻辑运算符。我试图稍微扩展 Isabelle/Pure 的自然演绎框架，而不是复制所有的 HOL。

我从这个问题中得到的主要价​​值是，我现在知道我需要注意是否需要排除中间公理。如果我想要一个元假，那么我似乎需要一个排中公理。

这是我离开的地方。感谢您的帮助，请原谅冗长的补充。

Isabelle 有两种证明方式：旧的“应用”方式，证明只是一个链

声明，以及新的“结构化”Isar 风格。我自己，我觉得两者都很有用；“应用”风格更简洁，因此对于无趣的技术引理很方便，而“结构化”风格对于主要定理很方便。

有时我喜欢从一种风格切换到另一种风格，中等证明。从“应用”样式切换到“结构化”样式很容易：我只是插入

在我的应用链中。我的问题是：如何从“结构化”样式切换回“应用”样式？

举一个更具体的例子：假设我有五个子目标。我发出一些“应用”指令来发送前两个子目标。然后我开始进行结构化证明以省去第三个证明。我还有两个子目标：我如何为这些返回“应用”样式？

如果我的目标状态是foo ==> bar --> qux，我知道我可以使用该语句

让出目标状态foo ==> bar ==> qux。另一个方向呢？哪个命令会让我回到目标状态foo ==> bar --> qux？

---

到目前为止我想出的最好的是

但这很笨拙，我想知道是否有更好的方法。

假设我有一个关于简单归纳定义集的引理：

（对我来说，保留“⋀x y”位很重要，因为引理实际上是在说明我的证明处于长应用链中间的状态。）

我在开始证明这个引理时遇到了麻烦。我想通过规则归纳来进行。

第一次尝试

我试着写

但这不起作用：该induct方法失败。我发现我可以通过修复x并y明确地解决这个问题，然后调用该induct方法，如下所示：

但是，由于我实际上处于应用链的中间，因此我宁愿不输入结构化证明块。

第二次尝试

我尝试使用该induct_tac方法，但不幸induct_tac的是没有foo.induct以我想要的方式应用该规则。如果我输入

那么第一个子目标是

这不是我想要的：我想要qux x []而不是qux x y. 该induct方法做到了这一点，但还有其他问题，如上所述。

据我了解，Isabelle 中的矩阵本质上是函数并且具有任意维度。在这种情况下，定义一个方阵（n x n矩阵）并不容易。此外，在纸上证明中，可以在证明中使用平方的维度“n”。但我如何在伊莎贝尔做到这一点？

莱布尼茨公式：

我的纸上证明：

这是我的伊莎贝尔证明的相关摘录：

在这种情况下我能做什么？

---

更新：

您的 C 类型是 ('a ^ 'n ^ 'n) 的受限版本，似乎是 > yours 的自定义类型，因为我在尝试使用它时遇到错误，即使在导入 > Polynomial.thy 之后也是如此。但也许它是在其他一些 HOL 理论中定义的。

不幸的是，我没有在我的代码示例中编写包含，请参阅更新的示例。但它不是自定义类型，导入“Polynomial.thy”和“Determinants”就足够了。（我测试了 Isabelle 版本 2013-1 和 2013-2。）

如果您使用的是矩阵的自定义定义，那么您很有可能在很大程度上是靠自己的。

我不相信我正在使用矩阵的自定义定义。库Determinants(~~/src/HOL/Multivariate_Analysis/Determinants) 具有以下行列式定义：
definition det:: "'a::comm_ring_1^'n^'n ⇒ 'a" where .... 所以库使用矩阵的概念作为向量的向量。如果我的戒指是多项式的，它不应该在我眼中产生影响。

无论如何，对于诸如 ('a ^ 'n ^ 'n) 之类的类型，在我看来，您应该能够编写一个函数来返回矩阵大小的值。因此，如果 (p ^ n ^ n) 是一个矩阵，其中 n 是一个集合，那么 n 的基数可能就是您在问题中想要的 n。

这让我走上了正确的道路。我目前的猜测是以下定义很有帮助：

card中定义Finite_Set。

我在 Isabelle 中定义了以下数据类型

并且看不到如何证明以下基本引理

在假设下B≠C，证明通过：

有没有一种方法可以在没有明确假设的情况下证明引理B并且C是不同的？

更新：正如 Manuel Eberl 在对答案的评论中建议的那样，问题是由错误的简化规则（带有[simp]属性的引理，此处省略）导致简化过程循环并因此忽略自动生成的简化规则B≠C，C≠B（在bs_t.simps,正如克里斯在他的回答中指出的那样）。正如 gc44 的回答一样，simp在正常情况下足以证明引理。