Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Unifier trace in solve_direct

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

From: Peter Lammich <lammich@in.tum.de>
Hi List,

when I type solve_direct, it outputs a lot of unifier trace messages
"Enter MATCH" and "unification bound exceeded".

I think it is due to some lemma that I have proven, and that hapens to
have an unfortunately shaped conclusion.

How can I identify the lemma? Is there any general method?

If I have identified the lemma, how can I exclude it from solve_direct?

Thanks in advance for any hints,
Peter

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

From: Lars Noschinski <noschinl@in.tum.de>
On 31.07.2014 09:42, Peter Lammich wrote:

Hi List,

when I type solve_direct, it outputs a lot of unifier trace messages
"Enter MATCH" and "unification bound exceeded".

I think it is due to some lemma that I have proven, and that hapens to
have an unfortunately shaped conclusion.

How can I identify the lemma? Is there any general method?
solve_direct basically calls "find_theorems solves", which again tries
to solve the current goal with several tactics applied to "all"
theorems. Your best bet is to dive into the implementation of
Find_Theorems.filter_solves.
If I have identified the lemma, how can I exclude it from solve_direct?
You cannot. Except with concealing the lemma from the available fact
space, which is probably not what you want.

-- Lars

Last updated: Apr 23 2024 at 08:19 UTC