Stream: General

Topic: unification in induction tactic

view this post on Zulip Sebastian Sturm (Sep 16 2019 at 13:12):

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.

view this post on Zulip Mathias Fleury (Sep 18 2019 at 07:07):

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 21 2024 at 12:33 UTC