# HG changeset patch
# User paulson
# Date 1164109815 -3600
# Node ID 77651b6d9d6c36a2aeb136b7273b91b66ab321ce
# Parent  7f3bb0d28bdd03a0531a5339cd100e81e238d76b
New transformation of eliminatino rules: we simply replace the final conclusion variable by False

diff -r 7f3bb0d28bdd -r 77651b6d9d6c src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Tue Nov 21 04:30:17 2006 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Tue Nov 21 12:50:15 2006 +0100
@@ -8,9 +8,6 @@
 (*unused during debugging*)
 signature RES_AXIOMS =
   sig
-  val elimRule_tac : thm -> Tactical.tactic
-  val elimR2Fol : thm -> term
-  val transform_elim : thm -> thm
   val cnf_axiom : (string * thm) -> thm list
   val cnf_name : string -> thm list
   val meta_cnf_axiom : thm -> thm list
@@ -67,73 +64,19 @@
 
 (**** Transformation of Elimination Rules into First-Order Formulas****)
 
-(* a tactic used to prove an elim-rule. *)
-fun elimRule_tac th =
-    (resolve_tac [impI,notI] 1) THEN (etac th 1) THEN REPEAT(fast_tac HOL_cs 1);
-
-fun add_EX tm [] = tm
-  | add_EX tm ((x,xtp)::xs) = add_EX (HOLogic.exists_const xtp $ Abs(x,xtp,tm)) xs;
-
-(*Checks for the premise ~P when the conclusion is P.*)
-fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_)))
-           (Const("Trueprop",_) $ Free(q,_)) = (p = q)
-  | is_neg _ _ = false;
-
-exception ELIMR2FOL;
-
-(*Handles the case where the dummy "conclusion" variable appears negated in the
-  premises, so the final consequent must be kept.*)
-fun strip_concl' prems bvs (Const ("==>",_) $ P $ Q) =
-      strip_concl' (HOLogic.dest_Trueprop P :: prems) bvs  Q
-  | strip_concl' prems bvs P =
-      let val P' = HOLogic.Not $ (HOLogic.dest_Trueprop P)
-      in add_EX (foldr1 HOLogic.mk_conj (P'::prems)) bvs end;
-
-(*Recurrsion over the minor premise of an elimination rule. Final consequent
-  is ignored, as it is the dummy "conclusion" variable.*)
-fun strip_concl prems bvs concl (Const ("all", _) $ Abs (x,xtp,body)) =
-      strip_concl prems ((x,xtp)::bvs) concl body
-  | strip_concl prems bvs concl (Const ("==>",_) $ P $ Q) =
-      if (is_neg P concl) then (strip_concl' prems bvs Q)
-      else strip_concl (HOLogic.dest_Trueprop P::prems) bvs  concl Q
-  | strip_concl prems bvs concl Q =
-      if concl aconv Q andalso not (null prems) 
-      then add_EX (foldr1 HOLogic.mk_conj prems) bvs
-      else raise ELIMR2FOL (*expected conclusion not found!*)
+val cfalse = cterm_of HOL.thy HOLogic.false_const;
+val ctp_false = cterm_of HOL.thy (HOLogic.mk_Trueprop HOLogic.false_const);
 
-fun trans_elim (major,[],_) = HOLogic.Not $ major
-  | trans_elim (major,minors,concl) =
-      let val disjs = foldr1 HOLogic.mk_disj (map (strip_concl [] [] concl) minors)
-      in  HOLogic.mk_imp (major, disjs)  end;
-
-(* convert an elim rule into an equivalent formula, of type term. *)
-fun elimR2Fol elimR =
-  let val elimR' = freeze_thm elimR
-      val (prems,concl) = (prems_of elimR', concl_of elimR')
-      val cv = case concl of    (*conclusion variable*)
-                  Const("Trueprop",_) $ (v as Free(_,Type("bool",[]))) => v
-                | v as Free(_, Type("prop",[])) => v
-                | _ => raise ELIMR2FOL
-  in case prems of
-      [] => raise ELIMR2FOL
-    | (Const("Trueprop",_) $ major) :: minors =>
-        if member (op aconv) (term_frees major) cv then raise ELIMR2FOL
-        else (trans_elim (major, minors, concl) handle TERM _ => raise ELIMR2FOL)
-    | _ => raise ELIMR2FOL
-  end;
-
-(* convert an elim-rule into an equivalent theorem that does not have the
-   predicate variable.  Leave other theorems unchanged.*)
+(*Converts an elim-rule into an equivalent theorem that does not have the
+  predicate variable.  Leaves other theorems unchanged.  We simply instantiate the
+  conclusion variable to False.*)
 fun transform_elim th =
-    let val t = HOLogic.mk_Trueprop (elimR2Fol th)
-    in 
-        if Meson.too_many_clauses t then TrueI
-        else Goal.prove_raw [] (cterm_of (sign_of_thm th) t) (fn _ => elimRule_tac th) 
-    end
-    handle ELIMR2FOL => th (*not an elimination rule*)
-         | exn => (warning ("transform_elim failed: " ^ Toplevel.exn_message exn ^
-                            " for theorem " ^ Thm.name_of_thm th ^ ": " ^ string_of_thm th); th)
-
+  case concl_of th of    (*conclusion variable*)
+       Const("Trueprop",_) $ (v as Var(_,Type("bool",[]))) => 
+           Thm.instantiate ([], [(cterm_of HOL.thy v, cfalse)]) th
+    | v as Var(_, Type("prop",[])) => 
+           Thm.instantiate ([], [(cterm_of HOL.thy v, ctp_false)]) th
+    | _ => th;
 
 (**** Transformation of Clasets and Simpsets into First-Order Axioms ****)