optimize local "def"s by treating them as definitions

--- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Aug 02 19:15:15 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Aug 03 01:16:08 2010 +0200
@@ -180,7 +180,7 @@
 fun plazy f = Pretty.blk (0, pstrs (f ()))
 
 fun pick_them_nits_in_term deadline state (params : params) auto i n step
-                           subst orig_assm_ts orig_t =
+                           subst assm_ts orig_t =
   let
     val timer = Timer.startRealTimer ()
     val thy = Proof.theory_of state
@@ -223,7 +223,7 @@
       if passed_deadline deadline then raise TimeLimit.TimeOut
       else raise Interrupt
 
-    val orig_assm_ts = if assms orelse auto then orig_assm_ts else []
+    val assm_ts = if assms orelse auto then assm_ts else []
     val _ =
       if step = 0 then
         print_m (fn () => "Nitpicking formula...")
@@ -233,13 +233,18 @@
                 (if i <> 1 orelse n <> 1 then
                    "subgoal " ^ string_of_int i ^ " of " ^ string_of_int n
                  else
-                   "goal")) [Logic.list_implies (orig_assm_ts, orig_t)]))
+                   "goal")) [Logic.list_implies (assm_ts, orig_t)]))
     val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
                 else orig_t
-    val assms_t = Logic.mk_conjunction_list (neg_t :: orig_assm_ts)
-    val (assms_t, evals) =
-      assms_t :: evals |> merge_type_vars ? merge_type_vars_in_terms
-                       |> pairf hd tl
+    val tfree_table =
+      if merge_type_vars then
+        merged_type_var_table_for_terms (neg_t :: assm_ts @ evals)
+      else
+        []
+    val neg_t = merge_type_vars_in_term merge_type_vars tfree_table neg_t
+    val assm_ts = map (merge_type_vars_in_term merge_type_vars tfree_table)
+                      assm_ts
+    val evals = map (merge_type_vars_in_term merge_type_vars tfree_table) evals
     val original_max_potential = max_potential
     val original_max_genuine = max_genuine
     val max_bisim_depth = fold Integer.max bisim_depths ~1
@@ -269,11 +274,11 @@
        skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
        unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
        constr_cache = Unsynchronized.ref []}
-    val frees = Term.add_frees assms_t []
-    val _ = null (Term.add_tvars assms_t []) orelse
+    val frees = fold Term.add_frees (neg_t :: assm_ts) []
+    val _ = null (fold Term.add_tvars (neg_t :: assm_ts) []) orelse
             raise NOT_SUPPORTED "schematic type variables"
     val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms,
-         binarize) = preprocess_term hol_ctxt finitizes monos assms_t
+         binarize) = preprocess_formulas hol_ctxt finitizes monos assm_ts neg_t
     val got_all_user_axioms =
       got_all_mono_user_axioms andalso no_poly_user_axioms
 
@@ -589,6 +594,7 @@
         val genuine_means_genuine =
           got_all_user_axioms andalso none_true wfs andalso
           sound_finitizes andalso codatatypes_ok
+        fun assms_prop () = Logic.mk_conjunction_list (neg_t :: assm_ts)
       in
         (pprint (Pretty.chunks
              [Pretty.blk (0,
@@ -604,7 +610,7 @@
          if genuine then
            (if check_genuine andalso standard then
               case prove_hol_model scope tac_timeout free_names sel_names
-                                   rel_table bounds assms_t of
+                                   rel_table bounds (assms_prop ()) of
                 SOME true =>
                 print ("Confirmation by \"auto\": The above " ^
                        das_wort_model ^ " is really genuine.")
@@ -665,7 +671,8 @@
               if check_potential then
                 let
                   val status = prove_hol_model scope tac_timeout free_names
-                                              sel_names rel_table bounds assms_t
+                                               sel_names rel_table bounds
+                                               (assms_prop ())
                 in
                   (case status of
                      SOME true => print ("Confirmation by \"auto\": The \
@@ -953,7 +960,7 @@
              error "Nitpick was interrupted."
 
 fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
-                      step subst orig_assm_ts orig_t =
+                      step subst assm_ts orig_t =
   let val warning_m = if auto then K () else warning in
     if getenv "KODKODI" = "" then
       (* The "expect" argument is deliberately ignored if Kodkodi is missing so
@@ -967,7 +974,7 @@
         val outcome as (outcome_code, _) =
           time_limit (if debug then NONE else timeout)
               (pick_them_nits_in_term deadline state params auto i n step subst
-                                      orig_assm_ts) orig_t
+                                      assm_ts) orig_t
           handle TOO_LARGE (_, details) =>
                  (warning ("Limit reached: " ^ details ^ "."); unknown_outcome)
                | TOO_SMALL (_, details) =>

--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Aug 02 19:15:15 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 03 01:16:08 2010 +0200
@@ -210,7 +210,8 @@
   val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term
   val equational_fun_axioms : hol_context -> styp -> term list
   val is_equational_fun_surely_complete : hol_context -> styp -> bool
-  val merge_type_vars_in_terms : term list -> term list
+  val merged_type_var_table_for_terms : term list -> (sort * string) list
+  val merge_type_vars_in_term : bool -> (sort * string) list -> term -> term
   val ground_types_in_type : hol_context -> bool -> typ -> typ list
   val ground_types_in_terms : hol_context -> bool -> term list -> typ list
 end;
@@ -2172,7 +2173,7 @@
 
 (** Type preprocessing **)
 
-fun merge_type_vars_in_terms ts =
+fun merged_type_var_table_for_terms ts =
   let
     fun add_type (TFree (s, S)) table =
         (case AList.lookup (op =) table S of
@@ -2181,10 +2182,13 @@
            else table
          | NONE => (S, s) :: table)
       | add_type _ table = table
-    val table = fold (fold_types (fold_atyps add_type)) ts []
-    fun coalesce (TFree (_, S)) = TFree (AList.lookup (op =) table S |> the, S)
-      | coalesce T = T
-  in map (map_types (map_atyps coalesce)) ts end
+  in fold (fold_types (fold_atyps add_type)) ts [] end
+
+fun merge_type_vars_in_term merge_type_vars table =
+  merge_type_vars
+  ? map_types (map_atyps
+        (fn TFree (_, S) => TFree (AList.lookup (op =) table S |> the, S)
+          | T => T))
 
 fun add_ground_types hol_ctxt binarize =
   let

--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Aug 02 19:15:15 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Aug 03 01:16:08 2010 +0200
@@ -8,9 +8,9 @@
 signature NITPICK_PREPROC =
 sig
   type hol_context = Nitpick_HOL.hol_context
-  val preprocess_term :
+  val preprocess_formulas :
     hol_context -> (typ option * bool option) list
-    -> (typ option * bool option) list -> term
+    -> (typ option * bool option) list -> term list -> term
     -> term list * term list * bool * bool * bool
 end;
 
@@ -854,6 +854,26 @@
 
 (** Axiom selection **)
 
+fun defined_free_by_assumption t =
+  let
+    fun do_equals t1 t2 =
+      if exists_subterm (curry (op aconv) t1) t2 then NONE else SOME t1
+  in
+    case t of
+      Const (@{const_name "=="}, _) $ (t1 as Free _) $ t2 => do_equals t1 t2
+    | @{const Trueprop} $ (Const (@{const_name "=="}, _)
+                           $ (t1 as Free _) $ t2) =>
+      do_equals t1 t2
+    | _ => NONE
+  end
+
+fun assumption_exclusively_defines_free assm_ts t =
+  case defined_free_by_assumption t of
+    SOME t1 =>
+    length (filter ((fn SOME t1' => t1 aconv t1' | NONE => false)
+                     o defined_free_by_assumption) assm_ts) = 1
+  | NONE => false
+
 fun all_table_entries table = Symtab.fold (append o snd) table []
 fun extra_table table s = Symtab.make [(s, all_table_entries table)]
 
@@ -868,13 +888,13 @@
 fun axioms_for_term
         (hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms,
                       fast_descrs, evals, def_table, nondef_table,
-                      choice_spec_table, user_nondefs, ...}) t =
+                      choice_spec_table, user_nondefs, ...}) assm_ts neg_t =
   let
     type accumulator = styp list * (term list * term list)
     fun add_axiom get app depth t (accum as (xs, axs)) =
       let
         val t = t |> unfold_defs_in_term hol_ctxt
-                  |> skolemize_term_and_more hol_ctxt ~1
+                  |> skolemize_term_and_more hol_ctxt ~1 (*### why ~1? *)
       in
         if is_trivial_equation t then
           accum
@@ -1008,15 +1028,21 @@
       List.partition (null o Term.hidden_polymorphism) user_nondefs
     val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals))
                            evals
+    val (def_assm_ts, nondef_assm_ts) =
+      List.partition (assumption_exclusively_defines_free assm_ts) assm_ts
     val (xs, (defs, nondefs)) =
-      ([], ([], [])) |> add_axioms_for_term 1 t 
-                     |> fold_rev (add_def_axiom 1) eval_axioms
-                     |> user_axioms = SOME true
-                        ? fold (add_nondef_axiom 1) mono_user_nondefs
+      ([], ([], []))
+      |> add_axioms_for_term 1 neg_t
+      |> fold_rev (add_def_axiom 1) def_assm_ts
+      |> fold_rev (add_nondef_axiom 1) nondef_assm_ts
+      |> fold_rev (add_def_axiom 1) eval_axioms
+      |> user_axioms = SOME true ? fold (add_nondef_axiom 1) mono_user_nondefs
     val defs = defs @ special_congruence_axioms hol_ctxt xs
     val got_all_mono_user_axioms =
       (user_axioms = SOME true orelse null mono_user_nondefs)
-  in (t :: nondefs, defs, got_all_mono_user_axioms, null poly_user_nondefs) end
+  in
+    (neg_t :: nondefs, defs, got_all_mono_user_axioms, null poly_user_nondefs)
+  end
 
 (** Simplification of constructor/selector terms **)
 
@@ -1235,15 +1261,16 @@
 
 val max_skolem_depth = 3
 
-fun preprocess_term (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs,
-                                  boxes, ...}) finitizes monos t =
+fun preprocess_formulas
+        (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs, boxes,
+                      ...}) finitizes monos assm_ts neg_t =
   let
     val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
-      t |> unfold_defs_in_term hol_ctxt
-        |> close_form
-        |> skolemize_term_and_more hol_ctxt max_skolem_depth
-        |> specialize_consts_in_term hol_ctxt 0
-        |> axioms_for_term hol_ctxt
+      neg_t |> unfold_defs_in_term hol_ctxt
+            |> close_form
+            |> skolemize_term_and_more hol_ctxt max_skolem_depth
+            |> specialize_consts_in_term hol_ctxt 0
+            |> axioms_for_term hol_ctxt assm_ts
     val binarize =
       is_standard_datatype thy stds nat_T andalso
       case binary_ints of