|
0
|
1 |
(** Generalized elimination rules **)
|
|
|
2 |
|
|
|
3 |
(*Generalized elimination for two conclusions*)
|
|
927
|
4 |
val prems = goal proto_pure_thy
|
|
0
|
5 |
"[| PROP U ==> PROP VA; \
|
|
|
6 |
\ PROP U ==> PROP VB; \
|
|
|
7 |
\ PROP U; \
|
|
|
8 |
\ [| PROP VA; PROP VB |] ==> PROP W \
|
|
|
9 |
\ |] ==> PROP W";
|
|
|
10 |
by (REPEAT (resolve_tac prems 1));
|
|
|
11 |
val general_elim2_rl = result();
|
|
|
12 |
|
|
|
13 |
fun make_elim2 (rl1,rl2) = standard (rl2 COMP rl1 COMP general_elim2_rl);
|
|
|
14 |
fun elim2_tac (rl1,rl2) = eresolve_tac [rl2 COMP rl1 COMP general_elim2_rl];
|
|
|
15 |
|
|
|
16 |
|
|
|
17 |
(*For example, make_elim2(conjunct1,conjunct2)
|
|
|
18 |
yields conjunction elimination *)
|