adding splitting of conjuncts in assumptions as forward rule on theorems; replacing term transformation for splitting conjuncts by theorem transformation; removing obsolete functions; tuned

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Sep 29 10:33:15 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Sep 29 10:33:15 2010 +0200
@@ -145,6 +145,7 @@
   (* conversions *)
   val imp_prems_conv : conv -> conv
   (* simple transformations *)
+  val split_conjuncts_in_assms : Proof.context -> thm -> thm
   val expand_tuples : theory -> thm -> thm
   val eta_contract_ho_arguments : theory -> thm -> thm
   val remove_equalities : theory -> thm -> thm
@@ -821,6 +822,19 @@
     val (_, args) = strip_comb atom
   in rewrite_args args end
 
+fun split_conjuncts_in_assms ctxt th =
+  let
+    val ((_, [fixed_th]), ctxt') = Variable.import false [th] ctxt 
+    fun split_conjs i nprems th =
+      if i > nprems then th
+      else
+        case try Drule.RSN (@{thm conjI}, (i, th)) of
+          SOME th' => split_conjs i (nprems+1) th'
+        | NONE => split_conjs (i+1) nprems th
+  in
+    singleton (Variable.export ctxt' ctxt) (split_conjs 1 (Thm.nprems_of fixed_th) fixed_th)
+  end
+  
 fun expand_tuples thy intro =
   let
     val ctxt = ProofContext.init_global thy
@@ -840,9 +854,7 @@
       (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}])
       intro'''
     (* splitting conjunctions introduced by Pair_eq*)
-    fun split_conj prem =
-      map HOLogic.mk_Trueprop (conjuncts (HOLogic.dest_Trueprop prem))
-    val intro''''' = map_term thy (maps_premises split_conj) intro''''
+    val intro''''' = split_conjuncts_in_assms ctxt intro''''
   in
     intro'''''
   end

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Wed Sep 29 10:33:15 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Wed Sep 29 10:33:15 2010 +0200
@@ -256,34 +256,18 @@
   #> Conv.fconv_rule nnf_conv 
   #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm ex_disj_distrib}])
 
-fun split_conjs thy t =
-  let 
-    fun split_conjunctions (Const (@{const_name HOL.conj}, _) $ t1 $ t2) =
-    (split_conjunctions t1) @ (split_conjunctions t2)
-    | split_conjunctions t = [t]
-  in
-    map HOLogic.mk_Trueprop (split_conjunctions (HOLogic.dest_Trueprop t))
-  end
-
 fun rewrite_intros thy =
   Simplifier.full_simplify (HOL_basic_ss addsimps [@{thm all_not_ex}])
   #> Simplifier.full_simplify
     (HOL_basic_ss addsimps (tl @{thms bool_simps}) addsimps @{thms nnf_simps})
-  #> map_term thy (maps_premises (split_conjs thy))
+  #> split_conjuncts_in_assms (ProofContext.init_global thy)
 
 fun print_specs options thy msg ths =
   if show_intermediate_results options then
     (tracing (msg); tracing (commas (map (Display.string_of_thm_global thy) ths)))
   else
     ()
-(*
-fun split_cases thy th =
-  let
-    
-  in
-    map_term thy th
-  end
-*)
+
 fun preprocess options (constname, specs) thy =
 (*  case Predicate_Compile_Data.processed_specs thy constname of
     SOME specss => (specss, thy)
@@ -292,7 +276,7 @@
       val ctxt = ProofContext.init_global thy
       val intros =
         if forall is_pred_equation specs then 
-          map (map_term thy (maps_premises (split_conjs thy))) (introrulify thy (map rewrite specs))
+          map (split_conjuncts_in_assms ctxt) (introrulify thy (map rewrite specs))
         else if forall (is_intro constname) specs then
           map (rewrite_intros thy) specs
         else