src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML

 *)
 
 structure Predicate_Compile_Aux =
 struct
 
+(* general syntactic functions *)
+
+(*Like dest_conj, but flattens conjunctions however nested*)
+fun conjuncts_aux (Const ("op &", _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
+  | conjuncts_aux t conjs = t::conjs;
+
+fun conjuncts t = conjuncts_aux t [];
+
 (* syntactic functions *)
- 
+
 fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
   | is_equationlike_term (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _)) = true
   | is_equationlike_term _ = false
   
 val is_equationlike = is_equationlike_term o prop_of 

 
 (* introduction rule combinators *)
 
 (* combinators to apply a function to all literals of an introduction rules *)
 
-(*
 fun map_atoms f intro = 
-*)
+  let
+    val (literals, head) = Logic.strip_horn intro
+    fun appl t = (case t of
+        (@{term "Not"} $ t') => HOLogic.mk_not (f t')
+      | _ => f t)
+  in
+    Logic.list_implies
+      (map (HOLogic.mk_Trueprop o appl o HOLogic.dest_Trueprop) literals, head)
+  end
 
 fun fold_atoms f intro s =
   let
     val (literals, head) = Logic.strip_horn intro
     fun appl t s = (case t of

 
 fun fold_map_atoms f intro s =
   let
     val (literals, head) = Logic.strip_horn intro
     fun appl t s = (case t of
-      (@{term "Not"} $ t') =>
-        let
-          val (t'', s') = f t' s
-        in (@{term "Not"} $ t'', s') end
+      (@{term "Not"} $ t') => apfst HOLogic.mk_not (f t' s)
       | _ => f t s)
     val (literals', s') = fold_map appl (map HOLogic.dest_Trueprop literals) s
   in
     (Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s')
   end;
-  
+
+fun maps_premises f intro =
+  let
+    val (premises, head) = Logic.strip_horn intro
+  in
+    Logic.list_implies (maps f premises, head)
+  end
+  
+(* lifting term operations to theorems *)
+
+fun map_term thy f th =
+  setmp quick_and_dirty true (SkipProof.make_thm thy) (f (prop_of th))
+
 (*
 fun equals_conv lhs_cv rhs_cv ct =
   case Thm.term_of ct of
     Const ("==", _) $ _ $ _ => Conv.arg_conv cv ct  
   | _ => error "equals_conv"  

   inductify : bool,
   rpred : bool
 };
 
 fun show_steps (Options opt) = #show_steps opt
+fun show_mode_inference (Options opt) = #show_mode_inference opt
 fun show_intermediate_results (Options opt) = #show_intermediate_results opt
 fun show_proof_trace (Options opt) = #show_proof_trace opt
 
 fun is_inductify (Options opt) = #inductify opt
 fun is_rpred (Options opt) = #rpred opt

 }
 
 
 fun print_step options s =
   if show_steps options then tracing s else ()
-  
+
 
 (* tuple processing *)
 
 fun expand_tuples thy intro =
   let

     val intro'' = Thm.instantiate (T_insts, t_insts') intro
     val [intro'''] = Variable.export ctxt3 ctxt [intro'']
     val intro'''' = Simplifier.full_simplify
       (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}])
       intro'''
-  in
-    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''''
+  in
+    intro'''''
   end
 
 
 
 end;