Email Gateway (Aug 19 2022 at 13:20): Email Gateway (Aug 19 2022 at 13:20):From: John Wickerson <johnwickerson@cantab.net>
Hi,
I've just stated my theorem, typed "apply(induct rule: ...)" and then typed "apply(auto)" to see what Isabelle could manage on its own. All that happened was that my output window turned a strange blue colour, Isabelle said "Enter MATCH" and proceeded to output lots of random variable names. What's going on? And more importantly, what should I do to stop this happening?
Thanks,
John
Email Gateway (Aug 19 2022 at 13:20):From: Lawrence Paulson <lp15@cam.ac.uk>
This is uncommon, but can happen especially if you have complicated universally-quantified assumptions. Try simp_all instead, and then force or blast on one subgoal at a time.
Larry Paulson
Email Gateway (Aug 19 2022 at 13:20):From: Manuel Eberl <eberlm@in.tum.de>
Could you please elaborate on what exactly is happening here? I've been
wondering about this myself for ages. Is it some kind of issue with
higher order unification?
Cheers,
Manuel Eberl
Email Gateway (Aug 19 2022 at 13:20):From: Lawrence Paulson <lp15@cam.ac.uk>
Yes, it’s higher order unification behaving badly. There’s no simple way to control it; better to avoid the situation as I suggested.
Larry Paulson
Last updated: Apr 20 2024 at 08:16 UTC