src/Provers/make_elim.ML
author wenzelm
Thu Jul 27 11:44:29 2000 +0200 (2000-07-27 ago)
changeset 9449 2f814053a6cc
parent 9172 2dbb80d4fdb7
child 12605 c198367640f6
permissions -rw-r--r--
intro_elim_tac: bimatch_from;
     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;