1.1 --- a/src/Provers/make_elim.ML Fri Dec 30 16:56:59 2005 +0100
1.2 +++ b/src/Provers/make_elim.ML Fri Dec 30 16:57:00 2005 +0100
1.3 @@ -1,6 +1,6 @@
1.4 -(* Title: Provers/make_elim.ML
1.5 +(* Title: Provers/make_elim.ML
1.6 ID: $Id$
1.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
1.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
1.9 Copyright 2000 University of Cambridge
1.10
1.11 Classical version of Tactic.make_elim
1.12 @@ -15,34 +15,24 @@
1.13
1.14 signature MAKE_ELIM_DATA =
1.15 sig
1.16 - val classical : thm (* (~P ==> P) ==> P *)
1.17 + val cla_dist_concl: thm (*"[| ~Z ==> PROP X; PROP Y ==> Z; PROP X ==> PROP Y |] ==> Z"*)
1.18 end;
1.19
1.20 functor Make_Elim_Fun(Data: MAKE_ELIM_DATA) =
1.21 struct
1.22
1.23 -local
1.24 - val cla_dist_concl = prove_goal (the_context ())
1.25 - "[| ~Z_ ==> PROP X_; PROP Y_ ==> Z_; PROP X_ ==> PROP Y_ |] ==> Z_"
1.26 - (fn [premx,premz,premy] =>
1.27 - ([(rtac Data.classical 1),
1.28 - (etac (premx RS premy RS premz) 1)]))
1.29 +fun make_elim rl =
1.30 + let
1.31 + fun compose_extra nsubgoal (tha,i,thb) =
1.32 + Seq.list_of (bicompose false (false,tha,nsubgoal) i thb)
1.33 + val revcut_rl' = Drule.incr_indexes rl revcut_rl
1.34
1.35 - fun compose_extra nsubgoal (tha,i,thb) =
1.36 - Seq.list_of (bicompose false (false,tha,nsubgoal) i thb)
1.37 -
1.38 -in
1.39 -
1.40 -fun make_elim rl =
1.41 - let val revcut_rl' = incr_indexes_wrt [] [] [] [rl] revcut_rl
1.42 - fun making (i,rl) =
1.43 - case compose_extra 2 (cla_dist_concl,i,rl) of
1.44 - [] => rl (*terminates by clash of variables!*)
1.45 - | rl'::_ => making (i+1,rl')
1.46 + fun making (i,rl) =
1.47 + case compose_extra 2 (Data.cla_dist_concl,i,rl) of
1.48 + [] => rl (*terminates by clash of variables!*)
1.49 + | rl'::_ => making (i+1,rl')
1.50 in making (2, hd (compose_extra 1 (rl, 1, revcut_rl'))) end
1.51 handle (*in default, use the previous version, which never fails*)
1.52 - THM _ => Tactic.make_elim rl | Empty => Tactic.make_elim rl;
1.53 + THM _ => Tactic.make_elim rl | Empty => Tactic.make_elim rl;
1.54
1.55 -end
1.56 -
1.57 end;