Theory HOL-Real_Asymp.Inst_Existentials

section ‹Tactic for instantiating existentials›
theory Inst_Existentials
  imports Main
begin

text ‹
  Coinduction proofs in Isabelle often lead to proof obligations with nested conjunctions and
  existential quantifiers, e.g. propx y. P x y  (z. Q x y z) .

  The following tactic allows instantiating these existentials with a given list of witnesses.
›

ML_file ‹inst_existentials.ML›

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)))

end