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;
paulson@9172
     1
(*  Title: 	Provers/make_elim.ML
paulson@9172
     2
    ID:         $Id$
paulson@9172
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@9172
     4
    Copyright   2000  University of Cambridge
paulson@9172
     5
paulson@9172
     6
Classical version of Tactic.make_elim
paulson@9172
     7
paulson@9172
     8
In classical logic, we can make stronger elimination rules using this version.
paulson@9172
     9
For instance, the HOL rule injD is transformed into
paulson@9172
    10
    [| inj ?f; ~ ?W ==> ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W
paulson@9172
    11
while Tactic.make_elim would yield the weaker rule
paulson@9172
    12
    [| inj ?f; ?f ?x = ?f ?y; ?x = ?y ==> PROP ?W |] ==> PROP ?W
paulson@9172
    13
Such rules can cause Fast_tac to fail and Blast_tac to report "PROOF FAILED"
paulson@9172
    14
*)
paulson@9172
    15
paulson@9172
    16
signature MAKE_ELIM_DATA =
paulson@9172
    17
sig
paulson@9172
    18
  val classical	: thm		(* (~P ==> P) ==> P *)
paulson@9172
    19
end;
paulson@9172
    20
paulson@9172
    21
functor Make_Elim_Fun(Data: MAKE_ELIM_DATA)  =
paulson@9172
    22
struct
paulson@9172
    23
paulson@9172
    24
local
paulson@9172
    25
    val cla_dist_concl = prove_goal (the_context ())
paulson@9172
    26
       "[| ~Z_ ==> PROP X_; PROP Y_ ==> Z_;  PROP X_ ==> PROP Y_ |] ==> Z_"
paulson@9172
    27
       (fn [premx,premz,premy] =>
paulson@9172
    28
	    ([(rtac Data.classical 1),
paulson@9172
    29
	      (etac (premx RS premy RS premz) 1)]))
paulson@9172
    30
paulson@9172
    31
    fun compose_extra nsubgoal (tha,i,thb) =
paulson@9172
    32
	Seq.list_of (bicompose false (false,tha,nsubgoal) i thb)
paulson@9172
    33
paulson@9172
    34
in
paulson@9172
    35
paulson@9172
    36
fun make_elim rl =
paulson@9172
    37
    let fun making (i,rl) =
paulson@9172
    38
	case compose_extra 2 (cla_dist_concl,i,rl) of
paulson@9172
    39
	    [] => rl
paulson@9172
    40
	  | rl'::_ => making (i+1,rl')
paulson@9172
    41
    in  making (2, hd (compose_extra 1 (rl, 1, revcut_rl)))  end
paulson@9172
    42
    handle THM _ => (*in default, use the previous version, which never fails*)
paulson@9172
    43
             Tactic.make_elim rl;
paulson@9172
    44
paulson@9172
    45
end
paulson@9172
    46
 
paulson@9172
    47
end;