renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary

--- a/doc-src/Nitpick/nitpick.tex	Tue Oct 27 15:55:36 2009 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Tue Oct 27 16:52:06 2009 +0100
@@ -1836,14 +1836,14 @@
 
 \nopagebreak
 {\small See also \textit{card} (\S\ref{scope-of-search}),
-\textit{coalesce\_type\_vars} (\S\ref{scope-of-search}), and \textit{verbose}
+\textit{merge\_type\_vars} (\S\ref{scope-of-search}), and \textit{verbose}
 (\S\ref{output-format}).}
 
 \opsmart{mono}{non\_box}
 Specifies the default monotonicity setting to use. This can be overridden on a
 per-type basis using the \textit{mono}~\qty{type} option described above.
 
-\opfalse{coalesce\_type\_vars}{dont\_coalesce\_type\_vars}
+\opfalse{merge\_type\_vars}{dont\_merge\_type\_vars}
 Specifies whether type variables with the same sort constraints should be
 merged. Setting this option to \textit{true} can reduce the number of scopes
 tried and the size of the generated Kodkod formulas, but it also diminishes the
@@ -2220,7 +2220,7 @@
 \nopagebreak
 {\small See also \textit{auto} (\S\ref{mode-of-operation}).}
 
-\opt{tac\_timeout}{time}{$\mathbf{500}$ ms}
+\opt{tac\_timeout}{time}{$\mathbf{500}$\,ms}
 Specifies the maximum amount of time that the \textit{auto} tactic should use
 when checking a counterexample, and similarly that \textit{lexicographic\_order}
 and \textit{sizechange} should use when checking whether a (co)in\-duc\-tive
@@ -2467,6 +2467,12 @@
 representation of functions synthesized by Isabelle, which is an implementation
 detail.
 
+\item[$\bullet$] Nitpick maintains a global cache of wellformedness conditions,
+which can become invalid if you change the definition of an inductive predicate
+that is registered in the cache. To clear the cache,
+run Nitpick with the \textit{tac\_timeout} option set to a new value (e.g.,
+501$\,\textit{ms}$).
+
 \item[$\bullet$] Nitpick produces spurious counterexamples when invoked after a
 \textbf{guess} command in a structured proof.
 

--- a/src/HOL/Nitpick.thy	Tue Oct 27 15:55:36 2009 +0100
+++ b/src/HOL/Nitpick.thy	Tue Oct 27 16:52:06 2009 +0100
@@ -28,7 +28,6 @@
 
 typedecl bisim_iterator
 
-(* FIXME: use axiomatization (here and elsewhere) *)
 axiomatization unknown :: 'a
            and undefined_fast_The :: 'a
            and undefined_fast_Eps :: 'a
@@ -118,12 +117,16 @@
  apply (simp only: unit.cases)
 by simp
 
+declare unit.cases [nitpick_simp del]
+
 lemma nat_case_def [nitpick_def]:
 "nat_case x f n \<equiv> if n = 0 then x else f (n - 1)"
 apply (rule eq_reflection)
 by (case_tac n) auto
 
-lemmas dvd_def = dvd_eq_mod_eq_0 [THEN eq_reflection, nitpick_def]
+declare nat.cases [nitpick_simp del]
+
+lemmas [nitpick_def] = dvd_eq_mod_eq_0 [THEN eq_reflection]
 
 lemma list_size_simp [nitpick_simp]:
 "list_size f xs = (if xs = [] then 0
@@ -207,6 +210,21 @@
 definition of_frac :: "'a \<Rightarrow> 'b\<Colon>{inverse,ring_1}" where
 "of_frac q \<equiv> of_int (num q) / of_int (denom q)"
 
+(* While Nitpick normally avoids to unfold definitions for locales, it
+   unfortunately needs to unfold them when dealing with the following built-in
+   constants. A cleaner approach would be to change "Nitpick_HOL" and
+   "Nitpick_Nits" so that they handle the unexpanded overloaded constants
+   directly, but this is slightly more tricky to implement. *)
+lemmas [nitpick_def] = div_int_inst.div_int div_int_inst.mod_int
+    div_nat_inst.div_nat div_nat_inst.mod_nat lower_semilattice_fun_inst.inf_fun
+    minus_fun_inst.minus_fun minus_int_inst.minus_int minus_nat_inst.minus_nat
+    one_int_inst.one_int one_nat_inst.one_nat ord_fun_inst.less_eq_fun
+    ord_int_inst.less_eq_int ord_int_inst.less_int ord_nat_inst.less_eq_nat
+    ord_nat_inst.less_nat plus_int_inst.plus_int plus_nat_inst.plus_nat
+    times_int_inst.times_int times_nat_inst.times_nat uminus_int_inst.uminus_int
+    upper_semilattice_fun_inst.sup_fun zero_int_inst.zero_int
+    zero_nat_inst.zero_nat
+
 use "Tools/Nitpick/kodkod.ML"
 use "Tools/Nitpick/kodkod_sat.ML"
 use "Tools/Nitpick/nitpick_util.ML"
@@ -231,10 +249,10 @@
 hide (open) type bisim_iterator pair_box fun_box
 hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
     wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
-    The_psimp Eps_psimp unit_case_def nat_case_def dvd_def list_size_simp
-    nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def
-    one_frac_def num_def denom_def norm_frac_def frac_def plus_frac_def
-    times_frac_def uminus_frac_def number_of_frac_def inverse_frac_def
-    less_eq_frac_def of_frac_def
+    The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
+    nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
+    num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def
+    uminus_frac_def number_of_frac_def inverse_frac_def less_eq_frac_def
+    of_frac_def
 
 end

--- a/src/HOL/Tools/Nitpick/HISTORY	Tue Oct 27 15:55:36 2009 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY	Tue Oct 27 16:52:06 2009 +0100
@@ -6,6 +6,7 @@
     "nitpick_ind_intro" to "nitpick_intro"
   * Replaced "special_depth" and "skolemize_depth" options by "specialize"
     and "skolemize"
+  * Renamed "coalesce_type_vars" to "merge_type_vars"
   * Fixed monotonicity check
 
 Version 1.2.2 (16 Oct 2009)

--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Oct 27 15:55:36 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Oct 27 16:52:06 2009 +0100
@@ -23,7 +23,7 @@
     overlord: bool,
     user_axioms: bool option,
     assms: bool,
-    coalesce_type_vars: bool,
+    merge_type_vars: bool,
     destroy_constrs: bool,
     specialize: bool,
     skolemize: bool,
@@ -88,7 +88,7 @@
   overlord: bool,
   user_axioms: bool option,
   assms: bool,
-  coalesce_type_vars: bool,
+  merge_type_vars: bool,
   destroy_constrs: bool,
   specialize: bool,
   skolemize: bool,
@@ -175,7 +175,7 @@
     val ctxt = Proof.context_of state
     val {cards_assigns, maxes_assigns, iters_assigns, bisim_depths, boxes,
          monos, wfs, sat_solver, blocking, falsify, debug, verbose, overlord,
-         user_axioms, assms, coalesce_type_vars, destroy_constrs, specialize,
+         user_axioms, assms, merge_type_vars, destroy_constrs, specialize,
          skolemize, star_linear_preds, uncurry, fast_descrs, peephole_optim,
          tac_timeout, sym_break, sharing_depth, flatten_props, max_threads,
          show_skolems, show_datatypes, show_consts, evals, formats,
@@ -220,7 +220,7 @@
                     neg_t
     val (assms_t, evals) =
       assms_t :: evals
-      |> coalesce_type_vars ? coalesce_type_vars_in_terms
+      |> merge_type_vars ? merge_type_vars_in_terms
       |> hd pairf tl
     val original_max_potential = max_potential
     val original_max_genuine = max_genuine
@@ -778,11 +778,9 @@
                    case scope_count (do_filter (!generated_problems)) scope of
                      0 => I
                    | n =>
-                     if scope_count (do_filter (these (!checked_problems)))
-                                    scope = n then
-                       Integer.add 1
-                     else
-                       I) (!generated_scopes) 0
+                     scope_count (do_filter (these (!checked_problems)))
+                                 scope = n
+                     ? Integer.add 1) (!generated_scopes) 0
       in
         "Nitpick " ^ did_so_and_so ^
         (if is_some (!checked_problems) andalso total > 0 then

--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Oct 27 15:55:36 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Oct 27 16:52:06 2009 +0100
@@ -125,7 +125,7 @@
   val is_inductive_pred : extended_context -> styp -> bool
   val is_constr_pattern_lhs : theory -> term -> bool
   val is_constr_pattern_formula : theory -> term -> bool
-  val coalesce_type_vars_in_terms : term list -> term list
+  val merge_type_vars_in_terms : term list -> term list
   val ground_types_in_type : extended_context -> typ -> typ list
   val ground_types_in_terms : extended_context -> term list -> typ list
   val format_type : int list -> int list -> typ -> typ
@@ -1016,24 +1016,6 @@
       | do_eq _ = false
   in do_eq end
 
-(* This table is not pretty. A better approach would be to avoid expanding the
-   operators to their low-level definitions, but this would require dealing with
-   overloading. *)
-val built_in_built_in_defs =
-  [@{thm div_int_inst.div_int}, @{thm div_int_inst.mod_int},
-   @{thm div_nat_inst.div_nat}, @{thm div_nat_inst.mod_nat},
-   @{thm lower_semilattice_fun_inst.inf_fun}, @{thm minus_fun_inst.minus_fun},
-   @{thm minus_int_inst.minus_int}, @{thm minus_nat_inst.minus_nat},
-   @{thm one_int_inst.one_int}, @{thm one_nat_inst.one_nat},
-   @{thm ord_fun_inst.less_eq_fun}, @{thm ord_int_inst.less_eq_int},
-   @{thm ord_int_inst.less_int}, @{thm ord_nat_inst.less_eq_nat},
-   @{thm ord_nat_inst.less_nat}, @{thm plus_int_inst.plus_int},
-   @{thm plus_nat_inst.plus_nat}, @{thm times_int_inst.times_int},
-   @{thm times_nat_inst.times_nat}, @{thm uminus_int_inst.uminus_int},
-   @{thm upper_semilattice_fun_inst.sup_fun}, @{thm zero_int_inst.zero_int},
-   @{thm zero_nat_inst.zero_nat}]
-  |> map prop_of
-
 (* theory -> term list * term list * term list *)
 fun all_axioms_of thy =
   let
@@ -1054,8 +1036,7 @@
     val (built_in_nondefs, user_nondefs) =
       List.partition (is_typedef_axiom thy false) user_nondefs
       |>> append built_in_nondefs
-    val defs = built_in_built_in_defs @
-               (thy |> PureThy.all_thms_of
+    val defs = (thy |> PureThy.all_thms_of
                     |> filter (equal Thm.definitionK o Thm.get_kind o snd)
                     |> map (prop_of o snd) |> filter is_plain_definition) @
                user_defs @ built_in_defs
@@ -1309,10 +1290,6 @@
     |> fold_rev (curry absdummy) (func_Ts @ [dataT])
   end
 
-val redefined_in_Nitpick_thy =
-  [@{const_name option_case}, @{const_name nat_case}, @{const_name list_case},
-   @{const_name list_size}]
-
 (* theory -> string -> typ -> typ -> term -> term *)
 fun optimized_record_get thy s rec_T res_T t =
   let val constr_x = the_single (datatype_constrs thy rec_T) in
@@ -1382,7 +1359,6 @@
   (is_real_equational_fun ext_ctxt orf is_real_inductive_pred ext_ctxt
    orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
   andf (not o has_trivial_definition thy def_table)
-  andf (not o member (op =) redefined_in_Nitpick_thy o fst)
 
 (* term * term -> term *)
 fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
@@ -1879,9 +1855,7 @@
 (* extended_context -> styp -> term list *)
 fun raw_equational_fun_axioms (ext_ctxt as {thy, fast_descrs, simp_table,
                                             psimp_table, ...}) (x as (s, _)) =
-  if s mem redefined_in_Nitpick_thy then
-    []
-  else case def_props_for_const thy fast_descrs (!simp_table) x of
+  case def_props_for_const thy fast_descrs (!simp_table) x of
     [] => (case def_props_for_const thy fast_descrs psimp_table x of
              [] => [inductive_pred_axiom ext_ctxt x]
            | psimps => psimps)
@@ -1890,7 +1864,7 @@
 val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms
 
 (* term list -> term list *)
-fun coalesce_type_vars_in_terms ts =
+fun merge_type_vars_in_terms ts =
   let
     (* typ -> (sort * string) list -> (sort * string) list *)
     fun add_type (TFree (s, S)) table =

--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Oct 27 15:55:36 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Oct 27 16:52:06 2009 +0100
@@ -38,7 +38,7 @@
    ("falsify", ["true"]),
    ("user_axioms", ["smart"]),
    ("assms", ["true"]),
-   ("coalesce_type_vars", ["false"]),
+   ("merge_type_vars", ["false"]),
    ("destroy_constrs", ["true"]),
    ("specialize", ["true"]),
    ("skolemize", ["true"]),
@@ -75,7 +75,7 @@
    ("satisfy", "falsify"),
    ("no_user_axioms", "user_axioms"),
    ("no_assms", "assms"),
-   ("dont_coalesce_type_vars", "coalesce_type_vars"),
+   ("dont_merge_type_vars", "merge_type_vars"),
    ("dont_destroy_constrs", "destroy_constrs"),
    ("dont_specialize", "specialize"),
    ("dont_skolemize", "skolemize"),
@@ -305,7 +305,7 @@
     val overlord = lookup_bool "overlord"
     val user_axioms = lookup_bool_option "user_axioms"
     val assms = lookup_bool "assms"
-    val coalesce_type_vars = lookup_bool "coalesce_type_vars"
+    val merge_type_vars = lookup_bool "merge_type_vars"
     val destroy_constrs = lookup_bool "destroy_constrs"
     val specialize = lookup_bool "specialize"
     val skolemize = lookup_bool "skolemize"
@@ -341,7 +341,7 @@
      monos = monos, wfs = wfs, sat_solver = sat_solver, blocking = blocking,
      falsify = falsify, debug = debug, verbose = verbose, overlord = overlord,
      user_axioms = user_axioms, assms = assms,
-     coalesce_type_vars = coalesce_type_vars, destroy_constrs = destroy_constrs,
+     merge_type_vars = merge_type_vars, destroy_constrs = destroy_constrs,
      specialize = specialize, skolemize = skolemize,
      star_linear_preds = star_linear_preds, uncurry = uncurry,
      fast_descrs = fast_descrs, peephole_optim = peephole_optim,