1.1 --- a/src/HOL/Tools/res_axioms.ML	Tue Nov 21 04:30:17 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Tue Nov 21 12:50:15 2006 +0100
     1.3 @@ -8,9 +8,6 @@
     1.4  (*unused during debugging*)
     1.5  signature RES_AXIOMS =
     1.6    sig
     1.7 -  val elimRule_tac : thm -> Tactical.tactic
     1.8 -  val elimR2Fol : thm -> term
     1.9 -  val transform_elim : thm -> thm
    1.10    val cnf_axiom : (string * thm) -> thm list
    1.11    val cnf_name : string -> thm list
    1.12    val meta_cnf_axiom : thm -> thm list
    1.13 @@ -67,73 +64,19 @@
    1.14  
    1.15  (**** Transformation of Elimination Rules into First-Order Formulas****)
    1.16  
    1.17 -(* a tactic used to prove an elim-rule. *)
    1.18 -fun elimRule_tac th =
    1.19 -    (resolve_tac [impI,notI] 1) THEN (etac th 1) THEN REPEAT(fast_tac HOL_cs 1);
    1.20 +val cfalse = cterm_of HOL.thy HOLogic.false_const;
    1.21 +val ctp_false = cterm_of HOL.thy (HOLogic.mk_Trueprop HOLogic.false_const);
    1.22  
    1.23 -fun add_EX tm [] = tm
    1.24 -  | add_EX tm ((x,xtp)::xs) = add_EX (HOLogic.exists_const xtp $ Abs(x,xtp,tm)) xs;
    1.25 -
    1.26 -(*Checks for the premise ~P when the conclusion is P.*)
    1.27 -fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_)))
    1.28 -           (Const("Trueprop",_) $ Free(q,_)) = (p = q)
    1.29 -  | is_neg _ _ = false;
    1.30 -
    1.31 -exception ELIMR2FOL;
    1.32 -
    1.33 -(*Handles the case where the dummy "conclusion" variable appears negated in the
    1.34 -  premises, so the final consequent must be kept.*)
    1.35 -fun strip_concl' prems bvs (Const ("==>",_) $ P $ Q) =
    1.36 -      strip_concl' (HOLogic.dest_Trueprop P :: prems) bvs  Q
    1.37 -  | strip_concl' prems bvs P =
    1.38 -      let val P' = HOLogic.Not $ (HOLogic.dest_Trueprop P)
    1.39 -      in add_EX (foldr1 HOLogic.mk_conj (P'::prems)) bvs end;
    1.40 -
    1.41 -(*Recurrsion over the minor premise of an elimination rule. Final consequent
    1.42 -  is ignored, as it is the dummy "conclusion" variable.*)
    1.43 -fun strip_concl prems bvs concl (Const ("all", _) $ Abs (x,xtp,body)) =
    1.44 -      strip_concl prems ((x,xtp)::bvs) concl body
    1.45 -  | strip_concl prems bvs concl (Const ("==>",_) $ P $ Q) =
    1.46 -      if (is_neg P concl) then (strip_concl' prems bvs Q)
    1.47 -      else strip_concl (HOLogic.dest_Trueprop P::prems) bvs  concl Q
    1.48 -  | strip_concl prems bvs concl Q =
    1.49 -      if concl aconv Q andalso not (null prems) 
    1.50 -      then add_EX (foldr1 HOLogic.mk_conj prems) bvs
    1.51 -      else raise ELIMR2FOL (*expected conclusion not found!*)
    1.52 -
    1.53 -fun trans_elim (major,[],_) = HOLogic.Not $ major
    1.54 -  | trans_elim (major,minors,concl) =
    1.55 -      let val disjs = foldr1 HOLogic.mk_disj (map (strip_concl [] [] concl) minors)
    1.56 -      in  HOLogic.mk_imp (major, disjs)  end;
    1.57 -
    1.58 -(* convert an elim rule into an equivalent formula, of type term. *)
    1.59 -fun elimR2Fol elimR =
    1.60 -  let val elimR' = freeze_thm elimR
    1.61 -      val (prems,concl) = (prems_of elimR', concl_of elimR')
    1.62 -      val cv = case concl of    (*conclusion variable*)
    1.63 -                  Const("Trueprop",_) $ (v as Free(_,Type("bool",[]))) => v
    1.64 -                | v as Free(_, Type("prop",[])) => v
    1.65 -                | _ => raise ELIMR2FOL
    1.66 -  in case prems of
    1.67 -      [] => raise ELIMR2FOL
    1.68 -    | (Const("Trueprop",_) $ major) :: minors =>
    1.69 -        if member (op aconv) (term_frees major) cv then raise ELIMR2FOL
    1.70 -        else (trans_elim (major, minors, concl) handle TERM _ => raise ELIMR2FOL)
    1.71 -    | _ => raise ELIMR2FOL
    1.72 -  end;
    1.73 -
    1.74 -(* convert an elim-rule into an equivalent theorem that does not have the
    1.75 -   predicate variable.  Leave other theorems unchanged.*)
    1.76 +(*Converts an elim-rule into an equivalent theorem that does not have the
    1.77 +  predicate variable.  Leaves other theorems unchanged.  We simply instantiate the
    1.78 +  conclusion variable to False.*)
    1.79  fun transform_elim th =
    1.80 -    let val t = HOLogic.mk_Trueprop (elimR2Fol th)
    1.81 -    in 
    1.82 -        if Meson.too_many_clauses t then TrueI
    1.83 -        else Goal.prove_raw [] (cterm_of (sign_of_thm th) t) (fn _ => elimRule_tac th) 
    1.84 -    end
    1.85 -    handle ELIMR2FOL => th (*not an elimination rule*)
    1.86 -         | exn => (warning ("transform_elim failed: " ^ Toplevel.exn_message exn ^
    1.87 -                            " for theorem " ^ Thm.name_of_thm th ^ ": " ^ string_of_thm th); th)
    1.88 -
    1.89 +  case concl_of th of    (*conclusion variable*)
    1.90 +       Const("Trueprop",_) $ (v as Var(_,Type("bool",[]))) => 
    1.91 +           Thm.instantiate ([], [(cterm_of HOL.thy v, cfalse)]) th
    1.92 +    | v as Var(_, Type("prop",[])) => 
    1.93 +           Thm.instantiate ([], [(cterm_of HOL.thy v, ctp_false)]) th
    1.94 +    | _ => th;
    1.95  
    1.96  (**** Transformation of Clasets and Simpsets into First-Order Axioms ****)
    1.97