Theory Instantiate_Existentials

(* Author: Manuel Eberl *)
theory Instantiate_Existentials
  imports Main
begin

ML ‹
fun inst_existentials_tac ctxt [] = TRY o REPEAT_ALL_NEW (resolve_tac ctxt @{thms conjI})
  | inst_existentials_tac ctxt (t :: ts) =
      (TRY o REPEAT_ALL_NEW (resolve_tac ctxt @{thms conjI}))
      THEN_ALL_NEW (TRY o (
        let
          val inst = Drule.infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt t)]
          val thms = map inst @{thms exI bexI}
        in
          resolve_tac ctxt thms THEN' inst_existentials_tac ctxt ts
        end))
›

method_setup inst_existentials =
  ‹
  Scan.lift (Scan.repeat Parse.term) >>
      (fn ts => fn ctxt => SIMPLE_METHOD' (inst_existentials_tac ctxt
         (map (Syntax.read_term ctxt) ts)))
  ›

text ‹Test›
lemma
  "∃ x. ∃ y ∈ UNIV. (∃ z ∈ UNIV. x + y = (z::nat)) ∧ (∃ z. x + y = (z::nat))"
  by (inst_existentials "1 :: nat" "2 :: nat" "3 :: nat"; simp)

end