Email Gateway (Apr 11 2023 at 10:25): Email Gateway (Apr 11 2023 at 10:25):From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Hi,
We have a case where an introduction rule cannot be applied with the
intro tactic (in an apply-style backwards-directed proof) but the same
rule can be successfully applied with the rule tactic. Based on my
(perhaps overly simplistic) mental model of what these tactics do I would
have expected intro to successfully progress a proof in any context where
rule does. Is this incorrect? What are the additional circumstances in
which intro can fail?
Thanks,
Dominic
Email Gateway (Apr 11 2023 at 13:49):From: Manuel Eberl <manuel@pruvisto.org>
Hard to say without concrete context, but one thing I can think of off
the top of my head: "rule" will instantiate schematic variables; "intro"
will not. So if the rule application requires instantiating schematic
variables, that would explain the behaviour. I would have thought this
would be documented in isar-ref, but apparently it isn't.
The behaviour of these proof methods can indeed be a bit confusion. Also
e.g. the behaviour of rule/intro w.r.t. chained facts (and in fact the
semantics of chained facts) is a frequent source of confusion for people
when they start writing Isar proofs.
Manuel
Email Gateway (Apr 11 2023 at 14:04):From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Yes, it appears from off-list suggestions from other people that schematic
variables are to blame for the difference in behaviour between the tactics
in our case. Unfortunately there does not appear to be an out-of-the-box
proof method (or is there?) that maximally applies a set of introduction
rules, like intro, works well with chained facts without needing an
explicit insertion step, and instantiates schematics like rule. Both
intro thms and (rule thms)+ only seem to satisfy two out of the three
requirements, albeit a different two.
Thanks,
Dom
Email Gateway (Apr 11 2023 at 14:22):From: Peter Lammich <lammich@in.tum.de>
You could use Eisbach and rule_tac which automatically inlines chained
facts (if inlining them is what you mean by "working well"):
imports ... "HOL-Eisbach.Eisbach" ...
...
apply (repeat_new ‹rule_tac thms›)
Last updated: Apr 26 2024 at 16:20 UTC