I have a goal with the shape
∃l r. ?P l r. I would like to provide the expressions to be used for l and r. I can do it like this:
show ?thesis apply (rule exI[of _ "x # l"]) apply (rule exI[of _ r]) using `x ≠ a` * by auto
but that's really clumsy. Ideally I'd have a proof method with behavior in between
intro, in that it can deal with goals that have an extra assumption, but the rule is applied only once. For reference, here is the full proof:
lemma remove1_split: assumes "a ∈ set xs" shows "∃l r. xs = l @ a # r ∧ remove1 a xs = l @ r" using assms proof (induction xs) case (Cons x xs) show ?case proof cases assume "x = a" show ?thesis apply (rule exI[of _ ""]) using `x = a` by simp next assume "x ≠ a" then have "a ∈ set xs" using `a ∈ set (x # xs)` by simp then obtain l r where *: "xs = l @ a # r ∧ remove1 a xs = l @ r" using Cons.IH by auto show ?thesis apply (rule exI[of _ "x # l"]) apply (rule exI[of _ r]) using `x ≠ a` * by auto qed qed simp
by (rule exI[of _ ""]) (use `x = a` in auto) ... by (rule exI[of _ "x # l"], rule exI[of _ r]) (use `x ≠ a` * in auto)
Otherwise, you go for
apply (use `x ≠ a` * in ‹auto intro: exI[of _ "x # l"] exI[of _ r]›)
However, I don't believe that there is a rule that applies the theorems one-by-one.
I wrote a method called
inst_existentials for this once, it can be found e.g. in
HOL-Real_Asymp.Inst_Existentials. Perhaps I should put it in a more prominent place at some point…
It can also instantiate existentials nested inside conjunctions. I wrote it because in coinductive proofs, your goal can sometimes be of the shape that you have 6 existential quantifiers (sometimes nested in conjunctions) and once you instantiate them correctly the rest is automatic.
Last updated: Sep 25 2021 at 09:17 UTC