1 (* Title: Provers/make_elim.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 2000 University of Cambridge |
|
5 |
|
6 Classical version of Tactic.make_elim |
|
7 |
|
8 In classical logic, we can make stronger elimination rules using this version. |
|
9 For instance, the HOL rule injD is transformed into |
|
10 [| inj ?f; ~ ?W ==> ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W |
|
11 while Tactic.make_elim would yield the weaker rule |
|
12 [| inj ?f; ?f ?x = ?f ?y; ?x = ?y ==> PROP ?W |] ==> PROP ?W |
|
13 Such rules can cause Fast_tac to fail and Blast_tac to report "PROOF FAILED" |
|
14 *) |
|
15 |
|
16 signature MAKE_ELIM_DATA = |
|
17 sig |
|
18 val cla_dist_concl: thm (*"[| ~Z ==> PROP X; PROP Y ==> Z; PROP X ==> PROP Y |] ==> Z"*) |
|
19 end; |
|
20 |
|
21 functor Make_Elim_Fun(Data: MAKE_ELIM_DATA) = |
|
22 struct |
|
23 |
|
24 fun make_elim rl = |
|
25 let |
|
26 fun compose_extra nsubgoal (tha,i,thb) = |
|
27 Seq.list_of (bicompose false (false,tha,nsubgoal) i thb) |
|
28 val revcut_rl' = Drule.incr_indexes rl revcut_rl |
|
29 |
|
30 fun making (i,rl) = |
|
31 case compose_extra 2 (Data.cla_dist_concl,i,rl) of |
|
32 [] => rl (*terminates by clash of variables!*) |
|
33 | rl'::_ => making (i+1,rl') |
|
34 in making (2, hd (compose_extra 1 (rl, 1, revcut_rl'))) end |
|
35 handle (*in default, use the previous version, which never fails*) |
|
36 THM _ => Tactic.make_elim rl | Empty => Tactic.make_elim rl; |
|
37 |
|
38 end; |
|