# HG changeset patch # User blanchet # Date 1256658726 -3600 # Node ID cba22e2999d5d2620966339a98baadeb60f48957 # Parent f9ff11344ec4a351b8c51d90d67abc86d4ac7c8d renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary diff -r f9ff11344ec4 -r cba22e2999d5 doc-src/Nitpick/nitpick.tex --- 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. diff -r f9ff11344ec4 -r cba22e2999d5 src/HOL/Nitpick.thy --- 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 \ 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 \ 'b\{inverse,ring_1}" where "of_frac q \ 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 diff -r f9ff11344ec4 -r cba22e2999d5 src/HOL/Tools/Nitpick/HISTORY --- 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) diff -r f9ff11344ec4 -r cba22e2999d5 src/HOL/Tools/Nitpick/nitpick.ML --- 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 diff -r f9ff11344ec4 -r cba22e2999d5 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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 = diff -r f9ff11344ec4 -r cba22e2999d5 src/HOL/Tools/Nitpick/nitpick_isar.ML --- 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,