1section \<open>Tactic for instantiating existentials\<close> 2theory Inst_Existentials 3 imports Main 4begin 5 6text \<open> 7 Coinduction proofs in Isabelle often lead to proof obligations with nested conjunctions and 8 existential quantifiers, e.g. \<^prop>\<open>\<exists>x y. P x y \<and> (\<exists>z. Q x y z)\<close> . 9 10 The following tactic allows instantiating these existentials with a given list of witnesses. 11\<close> 12 13ML_file \<open>inst_existentials.ML\<close> 14 15method_setup inst_existentials = \<open> 16 Scan.lift (Scan.repeat Parse.term) >> 17 (fn ts => fn ctxt => SIMPLE_METHOD' (Inst_Existentials.tac ctxt 18 (map (Syntax.read_term ctxt) ts))) 19\<close> 20 21end