Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Exception THM 0 raised (line 86 of tactic.ML)

Email Gateway (Aug 22 2022 at 15:07):

From: Sebastiaan Joosten <sjcjoosten@gmail.com>
Hi all,

in playing around with 'fun', I ran into the following exception:

exception THM 0 raised (line 86 of "tactic.ML"):
rule_by_tactic

The code that caused this was:
fun foo where
"foo True False False False = True"
|"foo False True False False = True"
|"foo False False True False = True"
|"foo False False False True = True"
|"foo _ _ _ _ = False"

The same happens if I just write:
function (sequential) foo where
"foo True False False False = True"
|"foo False True False False = True"
|"foo False False True False = True"
|"foo False False False True = True"
|"foo _ _ _ _ = False" sorry

I hope this is not intended behavior?

Best,

Sebastiaan

Email Gateway (Aug 22 2022 at 15:11):

From: Lars Hupel <hupel@in.tum.de>
Hi Sebastiaan,

definitely not. I poked around for a little and it turns out the
exception happens in the "after qed" step, as can be observed here:

function (sequential) foo where
"foo True False False False = True"
|"foo False True False False = True"
|"foo False False True False = True"
|"foo False False False True = True"
|"foo _ _ _ _ = False"
apply pat_completeness
apply auto
done

The exception is raised on "done".

There are not many calls to "rule_by_tactic" in the Isabelle sources.
I'll poke the person who wrote them and let them proceed here.

Cheers
Lars

Email Gateway (Aug 22 2022 at 15:11):

From: Makarius <makarius@sketis.net>
BTW, the isar-ref manual section 5.10 contains some hints about
ML_exception_debugger and a few other options.

The easiest way is to compile all of Isabelle Pure + HOL with debugger
information and then run the example.

Makarius

Email Gateway (Aug 22 2022 at 15:12):

From: Manuel Eberl <eberlm@in.tum.de>
As I was afraid, this one was my fault again. Sorry about that!

I just pushed 115bcddf2ea2 in order to resolve these kinds of problems.
I will also put re-examining this code more closely on my To Do list; I
wrote this many years ago and thought it should be quite robust at the
time, but after re-reading it now, I suspect it could use more polishing.

Cheers,

Manuel

Email Gateway (Aug 22 2022 at 15:12):

From: Makarius <makarius@sketis.net>
BTW, in Isabelle changelog messages, the keyword "tuned" means the
change does not change the meaning (e.g. polishing, stylistic improvements).

I've occasionally seen such commits from people at TUM using that word
for a more significant change, but that is a diversion from decades of
Isabelle history. (More and more Isabelle lore is getting lost.)

In situations as above, I usually say something like "proper generation
of elimination rules in function package", occasionally with some hints
about what was actually wrong (e.g. a small/abstract example).

Makarius

Last updated: Apr 25 2024 at 20:15 UTC