src/Provers/make_elim.ML
 author nipkow Fri May 17 11:25:07 2002 +0200 (2002-05-17 ago) changeset 13157 4a4599f78f18 parent 12605 c198367640f6 child 15570 8d8c70b41bab permissions -rw-r--r--
allowed more general split rules to cope with div/mod 2
1 (*  Title: 	Provers/make_elim.ML
2     ID:         \$Id\$
3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
4     Copyright   2000  University of Cambridge
6 Classical version of Tactic.make_elim
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 *)
16 signature MAKE_ELIM_DATA =
17 sig
18   val classical	: thm		(* (~P ==> P) ==> P *)
19 end;
21 functor Make_Elim_Fun(Data: MAKE_ELIM_DATA)  =
22 struct
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)]))
31     fun compose_extra nsubgoal (tha,i,thb) =
32 	Seq.list_of (bicompose false (false,tha,nsubgoal) i thb)
34 in
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
43     handle (*in default, use the previous version, which never fails*)
44 	   THM _ => Tactic.make_elim rl | LIST _ => Tactic.make_elim rl;
46 end
48 end;