|
68630
|
1 |
section \<open>Tactic for instantiating existentials\<close>
|
|
|
2 |
theory Inst_Existentials
|
|
|
3 |
imports Main
|
|
|
4 |
begin
|
|
|
5 |
|
|
|
6 |
text \<open>
|
|
|
7 |
Coinduction proofs in Isabelle often lead to proof obligations with nested conjunctions and
|
|
|
8 |
existential quantifiers, e.g. @{prop "\<exists>x y. P x y \<and> (\<exists>z. Q x y z)"} .
|
|
|
9 |
|
|
|
10 |
The following tactic allows instantiating these existentials with a given list of witnesses.
|
|
|
11 |
\<close>
|
|
|
12 |
|
|
|
13 |
ML_file \<open>inst_existentials.ML\<close>
|
|
|
14 |
|
|
|
15 |
method_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 |
|
|
|
21 |
end |