src/Provers/make_elim.ML
 author wenzelm Sat, 01 Jul 2000 19:55:22 +0200 changeset 9230 17ae63f82ad8 parent 9172 2dbb80d4fdb7 child 12605 c198367640f6 permissions -rw-r--r--
GPLed;
```
(*  Title: 	Provers/make_elim.ML
ID:         \$Id\$
Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory

Classical version of Tactic.make_elim

In classical logic, we can make stronger elimination rules using this version.
For instance, the HOL rule injD is transformed into
[| inj ?f; ~ ?W ==> ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W
while Tactic.make_elim would yield the weaker rule
[| inj ?f; ?f ?x = ?f ?y; ?x = ?y ==> PROP ?W |] ==> PROP ?W
Such rules can cause Fast_tac to fail and Blast_tac to report "PROOF FAILED"
*)

signature MAKE_ELIM_DATA =
sig
val classical	: thm		(* (~P ==> P) ==> P *)
end;

functor Make_Elim_Fun(Data: MAKE_ELIM_DATA)  =
struct

local
val cla_dist_concl = prove_goal (the_context ())
"[| ~Z_ ==> PROP X_; PROP Y_ ==> Z_;  PROP X_ ==> PROP Y_ |] ==> Z_"
(fn [premx,premz,premy] =>
([(rtac Data.classical 1),
(etac (premx RS premy RS premz) 1)]))

fun compose_extra nsubgoal (tha,i,thb) =
Seq.list_of (bicompose false (false,tha,nsubgoal) i thb)

in

fun make_elim rl =
let fun making (i,rl) =
case compose_extra 2 (cla_dist_concl,i,rl) of
[] => rl
| rl'::_ => making (i+1,rl')
in  making (2, hd (compose_extra 1 (rl, 1, revcut_rl)))  end
handle THM _ => (*in default, use the previous version, which never fails*)
Tactic.make_elim rl;

end

end;
```