Consider the following (schematic) Isabelle snippets.
inductive P :: "nat set ⇒ bool" where
P1: "P U1 ⟹ P U2 ⟹ P (U1∪U2)"
have "P (A ∪ B)" .
hence ?Q proof (induction rule: P.induct)
case H:(P1 U1 U2)
My problem is, that in
H I have no premise connecting
U1 U2 and
A B. How can I push Isabelle to generate the equality
A∪B = U1∪U2 or something similar is such a case.
I guess you already have found an answer, but if not, you can influence the heuristic that selects variables with:
hence Q proof (induction "A\<union>B" rule: P.induct) case H:(P1 U1 U2) thm H (* prints P U1 U1 = A ∪ B ⟹ Q P U2 U2 = A ∪ B ⟹ Q U1 ∪ U2 = A ∪ B *)
Last updated: Aug 15 2022 at 02:13 UTC