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;
```