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