# HG changeset patch
# User bulwahn
# Date 1285255365 -7200
# Node ID b3644e40f66135bfd642a4db2a0dea9a362151f3
# Parent  5e57675b7e40503b7f45276bd4b68a4199c73ca1
removing unneccessary expansion procedure for elimination rules; removing obsolete elim preprocessing; tuned

diff -r 5e57675b7e40 -r b3644e40f661 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Sep 23 17:22:44 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Sep 23 17:22:45 2010 +0200
@@ -146,7 +146,6 @@
   val imp_prems_conv : conv -> conv
   (* simple transformations *)
   val expand_tuples : theory -> thm -> thm
-  val expand_tuples_elim : Proof.context -> thm -> thm
   val eta_contract_ho_arguments : theory -> thm -> thm
   val remove_equalities : theory -> thm -> thm
   val remove_pointless_clauses : thm -> thm list
@@ -860,56 +859,6 @@
   then Conv.arg_conv (Conv.abs_conv (all_params_conv cv o #2) ctxt) ct
   else cv ctxt ct;
   
-fun expand_tuples_elim ctxt elimrule =
-  let
-    val thy = ProofContext.theory_of ctxt
-    val ((_, [elimrule]), ctxt1) = Variable.import false [elimrule] ctxt
-    val prems = Thm.prems_of elimrule
-    val nargs = length (snd (strip_comb (HOLogic.dest_Trueprop (hd prems))))
-    fun preprocess_case t =
-      let
-        val (param_names, param_Ts)  = split_list (Logic.strip_params t)
-        val prop = Logic.list_implies (Logic.strip_assums_hyp t, Logic.strip_assums_concl t)
-        val (free_names, ctxt2) = Variable.variant_fixes param_names ctxt1
-        val frees = map Free (free_names ~~ param_Ts)
-        val prop' = subst_bounds (rev frees, prop)
-        val (eqs, prems) = chop nargs (Logic.strip_imp_prems prop')
-        val rhss = map (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop) eqs
-        val (pats, prop'', ctxt2) = fold 
-          rewrite_prem (map HOLogic.dest_Trueprop prems)
-            (rewrite_args rhss ([], prop', ctxt2)) 
-        val new_frees = fold Term.add_frees (frees @ map snd pats) [] (* FIXME: frees are not minimal and not ordered *)
-      in
-        fold Logic.all (map Free new_frees) prop''
-      end
-    val cases' = map preprocess_case (tl prems)
-    val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule)
-    val tac = (fn _ => Skip_Proof.cheat_tac thy)
-    val eq = Goal.prove ctxt1 [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) tac
-    val exported_elimrule' = Thm.equal_elim eq elimrule |> singleton (Variable.export ctxt1 ctxt)
-    val elimrule'' = Conv.fconv_rule (imp_prems_conv (all_params_conv (fn ctxt => Conv.concl_conv nargs 
-      (Simplifier.full_rewrite
-        (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]))) ctxt1)) 
-      exported_elimrule'
-    (* splitting conjunctions introduced by Pair_eq*)
-    fun split_conj prem =
-      map HOLogic.mk_Trueprop (conjuncts (HOLogic.dest_Trueprop prem))
-    fun map_cases f t =
-      let
-        val (prems, concl) = Logic.strip_horn t
-        val ([pred], prems') = chop 1 prems
-        fun map_params f t =
-          let
-            val prop = Logic.list_implies (Logic.strip_assums_hyp t, Logic.strip_assums_concl t)
-          in Term.list_all (Logic.strip_params t, f prop) end 
-        val prems'' = map (map_params f) prems'
-      in
-        Logic.list_implies (pred :: prems'', concl)
-      end
-    val elimrule''' = map_term thy (map_cases (maps_premises split_conj)) elimrule''
-   in
-     elimrule'''
-  end
 (** eta contract higher-order arguments **)
 
 fun eta_contract_ho_arguments thy intro =
diff -r 5e57675b7e40 -r b3644e40f661 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Sep 23 17:22:44 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Sep 23 17:22:45 2010 +0200
@@ -627,36 +627,8 @@
 
 fun preprocess_intro thy = expand_tuples thy #> preprocess_equality thy
 
-fun preprocess_equality_elim ctxt elimrule =
-  let
-    fun replace_eqs (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, T) $ lhs $ rhs)) =
-       HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
-     | replace_eqs t = t
-    val thy = ProofContext.theory_of ctxt
-    val ((_, [elimrule]), ctxt') = Variable.import false [elimrule] ctxt
-    val prems = Thm.prems_of elimrule
-    val nargs = length (snd (strip_comb (HOLogic.dest_Trueprop (hd prems))))
-    fun preprocess_case t =
-      let
-        val params = Logic.strip_params t
-        val (assums1, assums2) = chop nargs (Logic.strip_assums_hyp t)
-        val assums_hyp' = assums1 @ (map replace_eqs assums2)
-      in
-        list_all (params, Logic.list_implies (assums_hyp', Logic.strip_assums_concl t))
-      end
-    val cases' = map preprocess_case (tl prems)
-    val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule)
-    val bigeq = (Thm.symmetric (Conv.implies_concl_conv
-      (MetaSimplifier.rewrite true [@{thm Predicate.eq_is_eq}])
-        (cterm_of thy elimrule')))
-    val tac = (fn _ => Skip_Proof.cheat_tac thy)
-    val eq = Goal.prove ctxt' [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) tac
-  in
-    Thm.equal_elim eq elimrule |> singleton (Variable.export ctxt' ctxt)
-  end;
+(* fetching introduction rules or registering introduction rules *)
 
-fun preprocess_elim ctxt = expand_tuples_elim ctxt #> preprocess_equality_elim ctxt
-  
 val no_compilation = ([], ([], []))
 
 fun fetch_pred_data ctxt name =