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: Dec 07 2023 at 08:19 UTC