Jakub Kądziołka (Mar 12 2021 at 02:45): Jakub Kądziołka (Mar 12 2021 at 02:45):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 rule and 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.
Manuel Eberl (Mar 12 2021 at 08:34):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…
Manuel Eberl (Mar 12 2021 at 08:35):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: Apr 19 2024 at 01:05 UTC