9172

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 classical : thm (* (~P ==> P) ==> P *)


19 
end;


20 


21 
functor Make_Elim_Fun(Data: MAKE_ELIM_DATA) =


22 
struct


23 


24 
local


25 
val cla_dist_concl = prove_goal (the_context ())


26 
"[ ~Z_ ==> PROP X_; PROP Y_ ==> Z_; PROP X_ ==> PROP Y_ ] ==> Z_"


27 
(fn [premx,premz,premy] =>


28 
([(rtac Data.classical 1),


29 
(etac (premx RS premy RS premz) 1)]))


30 


31 
fun compose_extra nsubgoal (tha,i,thb) =


32 
Seq.list_of (bicompose false (false,tha,nsubgoal) i thb)


33 


34 
in


35 


36 
fun make_elim rl =


37 
let fun making (i,rl) =


38 
case compose_extra 2 (cla_dist_concl,i,rl) of


39 
[] => rl


40 
 rl'::_ => making (i+1,rl')


41 
in making (2, hd (compose_extra 1 (rl, 1, revcut_rl))) end


42 
handle THM _ => (*in default, use the previous version, which never fails*)


43 
Tactic.make_elim rl;


44 


45 
end


46 


47 
end;
