added option show_mode_inference; added splitting of conjunctions in expand_tuples

--- a/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -6,8 +6,16 @@
 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
@@ -73,9 +81,16 @@
 
 (* 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
@@ -89,16 +104,25 @@
   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
@@ -122,6 +146,7 @@
 };
 
 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
 
@@ -141,7 +166,7 @@
 
 fun print_step options s =
   if show_steps options then tracing s else ()
-  
+
 
 (* tuple processing *)
 
@@ -190,8 +215,12 @@
     val intro'''' = Simplifier.full_simplify
       (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''''
   in
-    intro''''
+    intro'''''
   end
 
 

--- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -132,7 +132,7 @@
     val th = th
       |> inline_equations thy
       |> Pred_Compile_Set.unfold_set_notation
-      (*  |> AxClass.unoverload thy *)
+      |> AxClass.unoverload thy
     val (const, th) =
       if is_equationlike th then
         let

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -67,12 +67,12 @@
   };  
   type moded_clause = term list * (indprem * tmode) list
   type 'a pred_mode_table = (string * (mode * 'a) list) list
-  val infer_modes : theory -> (string * mode list) list
+  val infer_modes : Predicate_Compile_Aux.options -> theory -> (string * mode list) list
     -> (string * mode list) list
     -> string list
     -> (string * (term list * indprem list) list) list
     -> (moded_clause list) pred_mode_table
-  val infer_modes_with_generator : theory -> (string * mode list) list
+  val infer_modes_with_generator : Predicate_Compile_Aux.options -> theory -> (string * mode list) list
     -> (string * mode list) list
     -> string list
     -> (string * (term list * indprem list) list) list
@@ -411,6 +411,14 @@
     val _ = tracing (cat_lines (map print_pred pred_mode_table))
   in () end;
 
+fun string_of_prem thy (Prem (ts, p)) =
+    (Syntax.string_of_term_global thy (list_comb (p, ts))) ^ "(premise)"
+  | string_of_prem thy (Negprem (ts, p)) =
+    (Syntax.string_of_term_global thy (HOLogic.mk_not (list_comb (p, ts)))) ^ "(negative premise)"
+  | string_of_prem thy (Sidecond t) =
+    (Syntax.string_of_term_global thy t) ^ "(sidecondition)"
+  | string_of_prem thy _ = error "string_of_prem: unexpected input"
+
 fun string_of_moded_prem thy (Prem (ts, p), tmode) =
     (Syntax.string_of_term_global thy (list_comb (p, ts))) ^
     "(" ^ (string_of_tmode tmode) ^ ")"
@@ -426,15 +434,20 @@
     (Syntax.string_of_term_global thy t) ^
     "(sidecond mode: " ^ string_of_smode is ^ ")"    
   | string_of_moded_prem _ _ = error "string_of_moded_prem: unimplemented"
-     
+
 fun print_moded_clauses thy =
-  let        
+  let
     fun string_of_clause pred mode clauses =
       cat_lines (map (fn (ts, prems) => (space_implode " --> "
         (map (string_of_moded_prem thy) prems)) ^ " --> " ^ pred ^ " "
         ^ (space_implode " " (map (Syntax.string_of_term_global thy) ts))) clauses)
   in print_pred_mode_table string_of_clause thy end;
 
+fun string_of_clause thy pred (ts, prems) =
+  (space_implode " --> "
+  (map (string_of_prem thy) prems)) ^ " --> " ^ pred ^ " "
+   ^ (space_implode " " (map (Syntax.string_of_term_global thy) ts))
+
 fun print_compiled_terms thy =
   print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term_global thy) thy
     
@@ -1139,19 +1152,26 @@
     else NONE
   end;
 
-fun check_modes_pred with_generator thy param_vs clauses modes gen_modes (p, ms) =
+fun print_failed_mode options thy modes p m rs i =
+  if show_mode_inference options then
+    let
+      val _ = Output.tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
+      p ^ " violates mode " ^ string_of_mode m)
+      val _ = Output.tracing (string_of_clause thy p (nth rs i))
+    in () end
+  else ()
+
+fun check_modes_pred options with_generator thy param_vs clauses modes gen_modes (p, ms) =
   let val SOME rs = AList.lookup (op =) clauses p
   in (p, List.filter (fn m => case find_index
     (is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of
       ~1 => true
-    | i => (tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
-      p ^ " violates mode " ^ string_of_mode m);
-        tracing (commas (map (Syntax.string_of_term_global thy) (fst (nth rs i)))); false)) ms)
+    | i => (print_failed_mode options thy modes p m rs i; false)) ms)
   end;
 
 fun get_modes_pred with_generator thy param_vs clauses modes gen_modes (p, ms) =
   let
-    val SOME rs = AList.lookup (op =) clauses p 
+    val SOME rs = AList.lookup (op =) clauses p
   in
     (p, map (fn m =>
       (m, map (the o check_mode_clause with_generator thy param_vs modes gen_modes m) rs)) ms)
@@ -1161,11 +1181,11 @@
   let val y = f x
   in if x = y then x else fixp f y end;
 
-fun infer_modes thy extra_modes all_modes param_vs clauses =
+fun infer_modes options thy extra_modes all_modes param_vs clauses =
   let
     val modes =
       fixp (fn modes =>
-        map (check_modes_pred false thy param_vs clauses (modes @ extra_modes) []) modes)
+        map (check_modes_pred options false thy param_vs clauses (modes @ extra_modes) []) modes)
           all_modes
   in
     map (get_modes_pred false thy param_vs clauses (modes @ extra_modes) []) modes
@@ -1178,16 +1198,16 @@
     | SOME vs' => (k, vs \\ vs'))
     :: remove_from rem xs
     
-fun infer_modes_with_generator thy extra_modes all_modes param_vs clauses =
+fun infer_modes_with_generator options thy extra_modes all_modes param_vs clauses =
   let
     val prednames = map fst clauses
     val extra_modes = all_modes_of thy
     val gen_modes = all_generator_modes_of thy
       |> filter_out (fn (name, _) => member (op =) prednames name)
-    val starting_modes = remove_from extra_modes all_modes 
+    val starting_modes = remove_from extra_modes all_modes
     val modes =
       fixp (fn modes =>
-        map (check_modes_pred true thy param_vs clauses extra_modes (gen_modes @ modes)) modes)
+        map (check_modes_pred options true thy param_vs clauses extra_modes (gen_modes @ modes)) modes)
          starting_modes 
   in
     map (get_modes_pred true thy param_vs clauses extra_modes (gen_modes @ modes)) modes
@@ -2294,7 +2314,7 @@
     val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) =
       prepare_intrs thy prednames (maps (intros_of thy) prednames)
     val _ = print_step options "Infering modes..."
-    val moded_clauses = #infer_modes steps thy extra_modes all_modes param_vs clauses 
+    val moded_clauses = #infer_modes steps options thy extra_modes all_modes param_vs clauses 
     val modes : (string * ((int * int list option) list option list * (int * int list option) list) list) list = map (fn (p, mps) => (p, map fst mps)) moded_clauses
     val all_smodes : (((int * int list option) list) list) list = map (map snd) (map snd modes)
     val _ = case expected_modes of