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

     2.1 --- a/src/HOL/Nitpick.thy	Tue Oct 27 15:55:36 2009 +0100
     2.2 +++ b/src/HOL/Nitpick.thy	Tue Oct 27 16:52:06 2009 +0100
     2.3 @@ -28,7 +28,6 @@
     2.4  
     2.5  typedecl bisim_iterator
     2.6  
     2.7 -(* FIXME: use axiomatization (here and elsewhere) *)
     2.8  axiomatization unknown :: 'a
     2.9             and undefined_fast_The :: 'a
    2.10             and undefined_fast_Eps :: 'a
    2.11 @@ -118,12 +117,16 @@
    2.12   apply (simp only: unit.cases)
    2.13  by simp
    2.14  
    2.15 +declare unit.cases [nitpick_simp del]
    2.16 +
    2.17  lemma nat_case_def [nitpick_def]:
    2.18  "nat_case x f n \<equiv> if n = 0 then x else f (n - 1)"
    2.19  apply (rule eq_reflection)
    2.20  by (case_tac n) auto
    2.21  
    2.22 -lemmas dvd_def = dvd_eq_mod_eq_0 [THEN eq_reflection, nitpick_def]
    2.23 +declare nat.cases [nitpick_simp del]
    2.24 +
    2.25 +lemmas [nitpick_def] = dvd_eq_mod_eq_0 [THEN eq_reflection]
    2.26  
    2.27  lemma list_size_simp [nitpick_simp]:
    2.28  "list_size f xs = (if xs = [] then 0
    2.29 @@ -207,6 +210,21 @@
    2.30  definition of_frac :: "'a \<Rightarrow> 'b\<Colon>{inverse,ring_1}" where
    2.31  "of_frac q \<equiv> of_int (num q) / of_int (denom q)"
    2.32  
    2.33 +(* While Nitpick normally avoids to unfold definitions for locales, it
    2.34 +   unfortunately needs to unfold them when dealing with the following built-in
    2.35 +   constants. A cleaner approach would be to change "Nitpick_HOL" and
    2.36 +   "Nitpick_Nits" so that they handle the unexpanded overloaded constants
    2.37 +   directly, but this is slightly more tricky to implement. *)
    2.38 +lemmas [nitpick_def] = div_int_inst.div_int div_int_inst.mod_int
    2.39 +    div_nat_inst.div_nat div_nat_inst.mod_nat lower_semilattice_fun_inst.inf_fun
    2.40 +    minus_fun_inst.minus_fun minus_int_inst.minus_int minus_nat_inst.minus_nat
    2.41 +    one_int_inst.one_int one_nat_inst.one_nat ord_fun_inst.less_eq_fun
    2.42 +    ord_int_inst.less_eq_int ord_int_inst.less_int ord_nat_inst.less_eq_nat
    2.43 +    ord_nat_inst.less_nat plus_int_inst.plus_int plus_nat_inst.plus_nat
    2.44 +    times_int_inst.times_int times_nat_inst.times_nat uminus_int_inst.uminus_int
    2.45 +    upper_semilattice_fun_inst.sup_fun zero_int_inst.zero_int
    2.46 +    zero_nat_inst.zero_nat
    2.47 +
    2.48  use "Tools/Nitpick/kodkod.ML"
    2.49  use "Tools/Nitpick/kodkod_sat.ML"
    2.50  use "Tools/Nitpick/nitpick_util.ML"
    2.51 @@ -231,10 +249,10 @@
    2.52  hide (open) type bisim_iterator pair_box fun_box
    2.53  hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
    2.54      wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
    2.55 -    The_psimp Eps_psimp unit_case_def nat_case_def dvd_def list_size_simp
    2.56 -    nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def
    2.57 -    one_frac_def num_def denom_def norm_frac_def frac_def plus_frac_def
    2.58 -    times_frac_def uminus_frac_def number_of_frac_def inverse_frac_def
    2.59 -    less_eq_frac_def of_frac_def
    2.60 +    The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
    2.61 +    nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
    2.62 +    num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def
    2.63 +    uminus_frac_def number_of_frac_def inverse_frac_def less_eq_frac_def
    2.64 +    of_frac_def
    2.65  
    2.66  end

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

     4.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Oct 27 15:55:36 2009 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Oct 27 16:52:06 2009 +0100
     4.3 @@ -23,7 +23,7 @@
     4.4      overlord: bool,
     4.5      user_axioms: bool option,
     4.6      assms: bool,
     4.7 -    coalesce_type_vars: bool,
     4.8 +    merge_type_vars: bool,
     4.9      destroy_constrs: bool,
    4.10      specialize: bool,
    4.11      skolemize: bool,
    4.12 @@ -88,7 +88,7 @@
    4.13    overlord: bool,
    4.14    user_axioms: bool option,
    4.15    assms: bool,
    4.16 -  coalesce_type_vars: bool,
    4.17 +  merge_type_vars: bool,
    4.18    destroy_constrs: bool,
    4.19    specialize: bool,
    4.20    skolemize: bool,
    4.21 @@ -175,7 +175,7 @@
    4.22      val ctxt = Proof.context_of state
    4.23      val {cards_assigns, maxes_assigns, iters_assigns, bisim_depths, boxes,
    4.24           monos, wfs, sat_solver, blocking, falsify, debug, verbose, overlord,
    4.25 -         user_axioms, assms, coalesce_type_vars, destroy_constrs, specialize,
    4.26 +         user_axioms, assms, merge_type_vars, destroy_constrs, specialize,
    4.27           skolemize, star_linear_preds, uncurry, fast_descrs, peephole_optim,
    4.28           tac_timeout, sym_break, sharing_depth, flatten_props, max_threads,
    4.29           show_skolems, show_datatypes, show_consts, evals, formats,
    4.30 @@ -220,7 +220,7 @@
    4.31                      neg_t
    4.32      val (assms_t, evals) =
    4.33        assms_t :: evals
    4.34 -      |> coalesce_type_vars ? coalesce_type_vars_in_terms
    4.35 +      |> merge_type_vars ? merge_type_vars_in_terms
    4.36        |> hd pairf tl
    4.37      val original_max_potential = max_potential
    4.38      val original_max_genuine = max_genuine
    4.39 @@ -778,11 +778,9 @@
    4.40                     case scope_count (do_filter (!generated_problems)) scope of
    4.41                       0 => I
    4.42                     | n =>
    4.43 -                     if scope_count (do_filter (these (!checked_problems)))
    4.44 -                                    scope = n then
    4.45 -                       Integer.add 1
    4.46 -                     else
    4.47 -                       I) (!generated_scopes) 0
    4.48 +                     scope_count (do_filter (these (!checked_problems)))
    4.49 +                                 scope = n
    4.50 +                     ? Integer.add 1) (!generated_scopes) 0
    4.51        in
    4.52          "Nitpick " ^ did_so_and_so ^
    4.53          (if is_some (!checked_problems) andalso total > 0 then

     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Oct 27 15:55:36 2009 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Oct 27 16:52:06 2009 +0100
     5.3 @@ -125,7 +125,7 @@
     5.4    val is_inductive_pred : extended_context -> styp -> bool
     5.5    val is_constr_pattern_lhs : theory -> term -> bool
     5.6    val is_constr_pattern_formula : theory -> term -> bool
     5.7 -  val coalesce_type_vars_in_terms : term list -> term list
     5.8 +  val merge_type_vars_in_terms : term list -> term list
     5.9    val ground_types_in_type : extended_context -> typ -> typ list
    5.10    val ground_types_in_terms : extended_context -> term list -> typ list
    5.11    val format_type : int list -> int list -> typ -> typ
    5.12 @@ -1016,24 +1016,6 @@
    5.13        | do_eq _ = false
    5.14    in do_eq end
    5.15  
    5.16 -(* This table is not pretty. A better approach would be to avoid expanding the
    5.17 -   operators to their low-level definitions, but this would require dealing with
    5.18 -   overloading. *)
    5.19 -val built_in_built_in_defs =
    5.20 -  [@{thm div_int_inst.div_int}, @{thm div_int_inst.mod_int},
    5.21 -   @{thm div_nat_inst.div_nat}, @{thm div_nat_inst.mod_nat},
    5.22 -   @{thm lower_semilattice_fun_inst.inf_fun}, @{thm minus_fun_inst.minus_fun},
    5.23 -   @{thm minus_int_inst.minus_int}, @{thm minus_nat_inst.minus_nat},
    5.24 -   @{thm one_int_inst.one_int}, @{thm one_nat_inst.one_nat},
    5.25 -   @{thm ord_fun_inst.less_eq_fun}, @{thm ord_int_inst.less_eq_int},
    5.26 -   @{thm ord_int_inst.less_int}, @{thm ord_nat_inst.less_eq_nat},
    5.27 -   @{thm ord_nat_inst.less_nat}, @{thm plus_int_inst.plus_int},
    5.28 -   @{thm plus_nat_inst.plus_nat}, @{thm times_int_inst.times_int},
    5.29 -   @{thm times_nat_inst.times_nat}, @{thm uminus_int_inst.uminus_int},
    5.30 -   @{thm upper_semilattice_fun_inst.sup_fun}, @{thm zero_int_inst.zero_int},
    5.31 -   @{thm zero_nat_inst.zero_nat}]
    5.32 -  |> map prop_of
    5.33 -
    5.34  (* theory -> term list * term list * term list *)
    5.35  fun all_axioms_of thy =
    5.36    let
    5.37 @@ -1054,8 +1036,7 @@
    5.38      val (built_in_nondefs, user_nondefs) =
    5.39        List.partition (is_typedef_axiom thy false) user_nondefs
    5.40        |>> append built_in_nondefs
    5.41 -    val defs = built_in_built_in_defs @
    5.42 -               (thy |> PureThy.all_thms_of
    5.43 +    val defs = (thy |> PureThy.all_thms_of
    5.44                      |> filter (equal Thm.definitionK o Thm.get_kind o snd)
    5.45                      |> map (prop_of o snd) |> filter is_plain_definition) @
    5.46                 user_defs @ built_in_defs
    5.47 @@ -1309,10 +1290,6 @@
    5.48      |> fold_rev (curry absdummy) (func_Ts @ [dataT])
    5.49    end
    5.50  
    5.51 -val redefined_in_Nitpick_thy =
    5.52 -  [@{const_name option_case}, @{const_name nat_case}, @{const_name list_case},
    5.53 -   @{const_name list_size}]
    5.54 -
    5.55  (* theory -> string -> typ -> typ -> term -> term *)
    5.56  fun optimized_record_get thy s rec_T res_T t =
    5.57    let val constr_x = the_single (datatype_constrs thy rec_T) in
    5.58 @@ -1382,7 +1359,6 @@
    5.59    (is_real_equational_fun ext_ctxt orf is_real_inductive_pred ext_ctxt
    5.60     orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
    5.61    andf (not o has_trivial_definition thy def_table)
    5.62 -  andf (not o member (op =) redefined_in_Nitpick_thy o fst)
    5.63  
    5.64  (* term * term -> term *)
    5.65  fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
    5.66 @@ -1879,9 +1855,7 @@
    5.67  (* extended_context -> styp -> term list *)
    5.68  fun raw_equational_fun_axioms (ext_ctxt as {thy, fast_descrs, simp_table,
    5.69                                              psimp_table, ...}) (x as (s, _)) =
    5.70 -  if s mem redefined_in_Nitpick_thy then
    5.71 -    []
    5.72 -  else case def_props_for_const thy fast_descrs (!simp_table) x of
    5.73 +  case def_props_for_const thy fast_descrs (!simp_table) x of
    5.74      [] => (case def_props_for_const thy fast_descrs psimp_table x of
    5.75               [] => [inductive_pred_axiom ext_ctxt x]
    5.76             | psimps => psimps)
    5.77 @@ -1890,7 +1864,7 @@
    5.78  val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms
    5.79  
    5.80  (* term list -> term list *)
    5.81 -fun coalesce_type_vars_in_terms ts =
    5.82 +fun merge_type_vars_in_terms ts =
    5.83    let
    5.84      (* typ -> (sort * string) list -> (sort * string) list *)
    5.85      fun add_type (TFree (s, S)) table =

     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Oct 27 15:55:36 2009 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Oct 27 16:52:06 2009 +0100
     6.3 @@ -38,7 +38,7 @@
     6.4     ("falsify", ["true"]),
     6.5     ("user_axioms", ["smart"]),
     6.6     ("assms", ["true"]),
     6.7 -   ("coalesce_type_vars", ["false"]),
     6.8 +   ("merge_type_vars", ["false"]),
     6.9     ("destroy_constrs", ["true"]),
    6.10     ("specialize", ["true"]),
    6.11     ("skolemize", ["true"]),
    6.12 @@ -75,7 +75,7 @@
    6.13     ("satisfy", "falsify"),
    6.14     ("no_user_axioms", "user_axioms"),
    6.15     ("no_assms", "assms"),
    6.16 -   ("dont_coalesce_type_vars", "coalesce_type_vars"),
    6.17 +   ("dont_merge_type_vars", "merge_type_vars"),
    6.18     ("dont_destroy_constrs", "destroy_constrs"),
    6.19     ("dont_specialize", "specialize"),
    6.20     ("dont_skolemize", "skolemize"),
    6.21 @@ -305,7 +305,7 @@
    6.22      val overlord = lookup_bool "overlord"
    6.23      val user_axioms = lookup_bool_option "user_axioms"
    6.24      val assms = lookup_bool "assms"
    6.25 -    val coalesce_type_vars = lookup_bool "coalesce_type_vars"
    6.26 +    val merge_type_vars = lookup_bool "merge_type_vars"
    6.27      val destroy_constrs = lookup_bool "destroy_constrs"
    6.28      val specialize = lookup_bool "specialize"
    6.29      val skolemize = lookup_bool "skolemize"
    6.30 @@ -341,7 +341,7 @@
    6.31       monos = monos, wfs = wfs, sat_solver = sat_solver, blocking = blocking,
    6.32       falsify = falsify, debug = debug, verbose = verbose, overlord = overlord,
    6.33       user_axioms = user_axioms, assms = assms,
    6.34 -     coalesce_type_vars = coalesce_type_vars, destroy_constrs = destroy_constrs,
    6.35 +     merge_type_vars = merge_type_vars, destroy_constrs = destroy_constrs,
    6.36       specialize = specialize, skolemize = skolemize,
    6.37       star_linear_preds = star_linear_preds, uncurry = uncurry,
    6.38       fast_descrs = fast_descrs, peephole_optim = peephole_optim,