Email Gateway (Oct 13 2022 at 17:52): Email Gateway (Oct 13 2022 at 17:52):From: Lawrence Paulson <lp15@cam.ac.uk>
We are allowed to use the “induction” (or “induct”) proof method when there are side formulas in the goal:
lemma "P l ⟹ l ∈ lists X ⟹ map f l ∈ lists (f ` X)"
apply (induction l)
At least, it’s allowed if the induction rule comes from a datatype (here, “‘a list”). And occurrences of the induction variable are instantiated correctly in the resulting subgoals.
But the analogous step not allowed if the induction rule comes from an inductive definition:
lemma "True ⟹ l ∈ lists X ⟹ map f l ∈ lists (f ` X)"
apply (induction l rule: lists.induct)
Even though this side formula doesn’t mention the induction variable, the proof method still fails.
The behaviour is identical in the current repository version and in Isabelle2021-01. Note that the induction rules lists.induct and list.induct differ in form, since with an inductive definition the rule has an explicit major premise.
Larry
Email Gateway (Oct 13 2022 at 18:18):From: Manuel Eberl <manuel@pruvisto.org>
I think the real difference is that induction rules that come from
inductive predicates are declared with "consumes 1". Thus,
"lists.induct" expects the first premise to be of the form "_ ∈ lists _".
If you swap your two premises so that the "l ∈ lists X" is in the front
everything works.
Cheers,
Manuel
Email Gateway (Oct 14 2022 at 10:09):From: Lawrence Paulson <lp15@cam.ac.uk>
Thanks for the explanation. This looks like an example of the difference between early Isabelle (where the required assumption could be grabbed from anywhere, as still happens with erule, and you can even backtrack on the choice) and Isar, where facts can be piped in from the previous step and must be used in order.
Larry
Last updated: Apr 19 2024 at 08:19 UTC