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