<commit_before>(*  Title: 	Provers/make_elim.ML
    ID:         $Id$
    Author: 	<NAME>, Cambridge University Computer Laboratory
    Copyright   2000  University of Cambridge

Classical version of Tactic.make_elim

In classical logic, we can make stronger elimination rules using this version.
For instance, the HOL rule injD is transformed into
    [| inj ?f; ~ ?W ==> ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W
while Tactic.make_elim would yield the weaker rule
    [| inj ?f; ?f ?x = ?f ?y; ?x = ?y ==> PROP ?W |] ==> PROP ?W
Such rules can cause Fast_tac to fail and Blast_tac to report "PROOF FAILED"
*)

signature MAKE_ELIM_DATA =
sig
  val classical	: thm		(* (~P ==> P) ==> P *)
end;

functor Make_Elim_Fun(Data: MAKE_ELIM_DATA)  =
struct

local
    val cla_dist_concl = prove_goal (the_context ())
       "[| ~Z_ ==> PROP X_; PROP Y_ ==> Z_;  PROP X_ ==> PROP Y_ |] ==> Z_"
       (fn [premx,premz,premy] =>
	    ([(rtac Data.classical 1),
	      (etac (premx RS premy RS premz) 1)]))

    fun compose_extra nsubgoal (tha,i,thb) =
	Seq.list_of (bicompose false (false,tha,nsubgoal) i thb)

in

fun make_elim rl =
    let fun making (i,rl) =
	case compose_extra 2 (cla_dist_concl,i,rl) of
	    [] => rl
	  | rl'::_ => making (i+1,rl')
    in  making (2, hd (compose_extra 1 (rl, 1, revcut_rl)))  end
    handle THM _ => (*in default, use the previous version, which never fails*)
             Tactic.make_elim rl;

end
 
end;<commit_msg>fixed variable-clash bug in make_elim<commit_after>(*  Title: 	Provers/make_elim.ML
    ID:         $Id$
    Author: 	<NAME>, Cambridge University Computer Laboratory
    Copyright   2000  University of Cambridge

Classical version of Tactic.make_elim

In classical logic, we can make stronger elimination rules using this version.
For instance, the HOL rule injD is transformed into
    [| inj ?f; ~ ?W ==> ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W
while Tactic.make_elim would yield the weaker rule
    [| inj ?f; ?f ?x = ?f ?y; ?x = ?y ==> PROP ?W |] ==> PROP ?W
Such rules can cause Fast_tac to fail and Blast_tac to report "PROOF FAILED"
*)

signature MAKE_ELIM_DATA =
sig
  val classical	: thm		(* (~P ==> P) ==> P *)
end;

functor Make_Elim_Fun(Data: MAKE_ELIM_DATA)  =
struct

local
    val cla_dist_concl = prove_goal (the_context ())
       "[| ~Z_ ==> PROP X_; PROP Y_ ==> Z_;  PROP X_ ==> PROP Y_ |] ==> Z_"
       (fn [premx,premz,premy] =>
	    ([(rtac Data.classical 1),
	      (etac (premx RS premy RS premz) 1)]))

    fun compose_extra nsubgoal (tha,i,thb) =
	Seq.list_of (bicompose false (false,tha,nsubgoal) i thb)

in

fun make_elim rl =
    let val revcut_rl' = incr_indexes_wrt [] [] [] [rl] revcut_rl
        fun making (i,rl) =
	    case compose_extra 2 (cla_dist_concl,i,rl) of
		[] => rl     (*terminates by clash of variables!*)
	      | rl'::_ => making (i+1,rl')
    in  making (2, hd (compose_extra 1 (rl, 1, revcut_rl')))  end
    handle (*in default, use the previous version, which never fails*)
	   THM _ => Tactic.make_elim rl | LIST _ => Tactic.make_elim rl;

end
 
end;
{'fraction_non_alphanumeric': 0.13611020006559527, 'fraction_numerical': 0.007215480485405051, 'mean_word_length': 3.1953232462173315, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 36, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5867212', 'n_tokens_mistral': 1218, 'n_tokens_neox': 1161, 'n_words': 372}