为什么 Isabelle/HOL 2018 显示错误但没有错误信息？

Question

对于一个 uni 项目，我正在使用 Iabelle/HOL 2018 进行证明。应用明显的结果时出现错误。但是，此错误并未说明发生了什么问题。

一开始以为是统一问题。但是当我简化后发现这是我完全不理解的行为。

我有一个最小的例子如下：

我将命题公式定义为 type1，然后我有一个简单地收集每个子公式的尾递归函数。可能有更好的方法来做到这一点。我只是试图以最简单的方式复制错误。然后我想证明一个简单的等式（我已经在我的代码中证明了这一点，在这里我只是简化了 "sorry"）然后我想在其他一些证明中使用这个事实，但是它似乎并不适用事实证明，即使我将它添加到简单集。甚至，直接应用它对我不起作用。

代码如下：

theory test
  imports Main
begin

datatype 'a type1 = 
    Bot
    | Atm 'a
    | Neg "'a type1"
    | Imp "'a type1" "'a type1"

fun func :: "'a type1 ⇒ ('a type1) list list ⇒ ('a type1) list list"
  where
    "func Bot acc = acc"
  | "func (Atm p) acc = acc"
  | "func (Neg p) acc = func p ([Neg p] # acc)"
  | "func (Imp p q) acc = func q (func p ([Imp p q] # acc))"

lemma lemma1 [simp]:
  "func p acc = func p [] @ acc"
  sorry

lemma lemma2:
  "func p acc = func p acc"
proof -
  have "func p acc = func p [] @ acc" by auto
  show ?thesis sorry
qed

end

在我看来这应该没问题。然而，在 lemma2 证明的第一行我得到了一个错误。但是没有对 "failed to finish proof" 或类似的错误的解释。

有谁知道我做错了什么？或者有没有人有类似的问题或行为？

Answer 1

引自书'A Proof Assistant for Higher-Order Logic'："In its most basic form, simplification means the repeated application of equations from left to right ... Only equations that really simplify, like rev (rev xs) = xs and xs @ [] = xs, should be declared as default simplification rules."（还有其他有价值的资源可以解释这个问题，例如官方Isabelle/Isar参考手册或教科书'Concrete Semantics with Isabelle/HOL'） .因此，lemma1 不是默认简化规则的好选择，将其添加到简化集会导致不终止，如您的示例所示。

如果你想在另一个证明中使用 lemma1，也许你可以使用类似于

的东西

have "func p acc = func p [] @ acc by (rule lemma1)"

或仅将简单规则重写为

func p [] @ acc = func p acc.

但是，一般来说，在引入新的简单规则时需要非常小心，尤其是在全局理论环境中。

为什么 Isabelle/HOL 2018 显示错误但没有错误信息？

Why is Isabelle/HOL 2018 showing error without error message?

isabelle