1 (* Title: Provers/make_elim.ML |
1 (* Title: Provers/make_elim.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 2000 University of Cambridge |
4 Copyright 2000 University of Cambridge |
5 |
5 |
6 Classical version of Tactic.make_elim |
6 Classical version of Tactic.make_elim |
7 |
7 |
8 In classical logic, we can make stronger elimination rules using this version. |
8 In classical logic, we can make stronger elimination rules using this version. |
13 Such rules can cause Fast_tac to fail and Blast_tac to report "PROOF FAILED" |
13 Such rules can cause Fast_tac to fail and Blast_tac to report "PROOF FAILED" |
14 *) |
14 *) |
15 |
15 |
16 signature MAKE_ELIM_DATA = |
16 signature MAKE_ELIM_DATA = |
17 sig |
17 sig |
18 val classical : thm (* (~P ==> P) ==> P *) |
18 val cla_dist_concl: thm (*"[| ~Z ==> PROP X; PROP Y ==> Z; PROP X ==> PROP Y |] ==> Z"*) |
19 end; |
19 end; |
20 |
20 |
21 functor Make_Elim_Fun(Data: MAKE_ELIM_DATA) = |
21 functor Make_Elim_Fun(Data: MAKE_ELIM_DATA) = |
22 struct |
22 struct |
23 |
23 |
24 local |
24 fun make_elim rl = |
25 val cla_dist_concl = prove_goal (the_context ()) |
25 let |
26 "[| ~Z_ ==> PROP X_; PROP Y_ ==> Z_; PROP X_ ==> PROP Y_ |] ==> Z_" |
26 fun compose_extra nsubgoal (tha,i,thb) = |
27 (fn [premx,premz,premy] => |
27 Seq.list_of (bicompose false (false,tha,nsubgoal) i thb) |
28 ([(rtac Data.classical 1), |
28 val revcut_rl' = Drule.incr_indexes rl revcut_rl |
29 (etac (premx RS premy RS premz) 1)])) |
|
30 |
29 |
31 fun compose_extra nsubgoal (tha,i,thb) = |
30 fun making (i,rl) = |
32 Seq.list_of (bicompose false (false,tha,nsubgoal) i thb) |
31 case compose_extra 2 (Data.cla_dist_concl,i,rl) of |
33 |
32 [] => rl (*terminates by clash of variables!*) |
34 in |
33 | rl'::_ => making (i+1,rl') |
35 |
|
36 fun make_elim rl = |
|
37 let val revcut_rl' = incr_indexes_wrt [] [] [] [rl] revcut_rl |
|
38 fun making (i,rl) = |
|
39 case compose_extra 2 (cla_dist_concl,i,rl) of |
|
40 [] => rl (*terminates by clash of variables!*) |
|
41 | rl'::_ => making (i+1,rl') |
|
42 in making (2, hd (compose_extra 1 (rl, 1, revcut_rl'))) end |
34 in making (2, hd (compose_extra 1 (rl, 1, revcut_rl'))) end |
43 handle (*in default, use the previous version, which never fails*) |
35 handle (*in default, use the previous version, which never fails*) |
44 THM _ => Tactic.make_elim rl | Empty => Tactic.make_elim rl; |
36 THM _ => Tactic.make_elim rl | Empty => Tactic.make_elim rl; |
45 |
37 |
46 end |
|
47 |
|
48 end; |
38 end; |