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

Question

For a uni project I'm working on a proof with Iabelle/HOL 2018. I'm getting an error when applying obvious results. However, this error is not stating anything about what is going wrong.

At first I thought it was an unification problem. But when I simplified it turned out to be a behavior I totally don't understand.

I have a minimal example which is as follows:

I define proposition formulas as type1 and then I have a tail-recursive function that simply collects each sub formula. There are probably better ways to do that. I just tried to replicate the error in the easiest way possible. Then I want to show a simple equality (I have proven that in my code, here I just simplify by "sorry") and then I want to use that fact in some other proof, however it doesn't seem to apply the proven fact, even though I added it to the simp set. Even, directly applying it doesn't work for me.

Here is the Code:

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

In my opinion this should be no problem. However, in the first line of the proof of lemma2 I get an error. But there is no explanation to the error such as "failed to finish proof" or anything similar.

Does anyone know what I'm doing wrong? Or did anyone have similar problems or behavior?

Quoting from the book 'A Proof Assistant for Higher-Order Logic': "In its most basic form, simplification means 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." As such, lemma1 is not a good choice for a default simplification rule and adding it to the simpset can lead to nontermination, as your example demonstrates. — user9716869
If you want to use lemma1 in another proof, perhaps, you can use something similar to have "func p acc = func p [] @ acc" by (rule lemma1) or merely rewrite the simp rule as func p [] @ acc = func p acc. However, in general, you need to be quite careful when introducing new simp rules, especially in the global theory context. — user9716869
I am glad I could help. However, please note that 'A Proof Assistant for Higher-Order Logic' is not a manual, but a textbook/tutorial. The official manual also explains this issue, but when I was beginning to learn Isabelle, I found it easier to learn from textbooks. So, I thought it may be more appropriate to mention it in the context of your question. Also, please note that the textbook that I mentioned is slightly outdated. So, it should also be used with care. There is another textbook, which is up-to-date with the recent developments: concrete-semantics.org. — user9716869

user9716869 user9716869 · Accepted Answer · 2019-07-24T13:31:44

Quoting from the book '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." (there are other valuable resources that explain this issue, e.g. the official Isabelle/Isar reference manual or the textbook 'Concrete Semantics with Isabelle/HOL'). Therefore, lemma1 is not a good choice for a default simplification rule and adding it to the simpset can lead to nontermination, as your example demonstrates.

If you would like to use lemma1 in another proof, perhaps, you can use something similar to

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

or merely rewrite the simp rule as

func p [] @ acc = func p acc.

However, in general, you need to be very careful when introducing new simp rules, especially in the global theory context.

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

1 Answers