# HG changeset patch # User blanchet # Date 1281087453 -7200 # Node ID 17d9808ed626b7c1640bd2148dc7f4b818e32f34 # Parent 8ed3a5fb4d25ec0610c04f58a868763d7b01a662# Parent 1c7d7eaebdf26dc9ea31204b23b367f01818063c merged diff -r 8ed3a5fb4d25 -r 17d9808ed626 doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Thu Aug 05 22:29:43 2010 +0200 +++ b/doc-src/Nitpick/nitpick.tex Fri Aug 06 11:37:33 2010 +0200 @@ -2864,16 +2864,19 @@ \textbf{by}~(\textit{auto simp}:~\textit{prec\_def}) \postw -Such theorems are considered bad style because they rely on the internal -representation of functions synthesized by Isabelle, which is an implementation +Such theorems are generally considered bad style because they rely on the +internal representation of functions synthesized by Isabelle, an implementation detail. \item[$\bullet$] Similarly, Nitpick might find spurious counterexamples for theorems that rely on the use of the indefinite description operator internally by \textbf{specification} and \textbf{quot\_type}. -\item[$\bullet$] Axioms that restrict the possible values of the -\textit{undefined} constant are in general ignored. +\item[$\bullet$] Axioms or definitions that restrict the possible values of the +\textit{undefined} constant or other partially specified built-in Isabelle +constants (e.g., \textit{Abs\_} and \textit{Rep\_} constants) are in general +ignored. Again, such nonconservative extensions are generally considered bad +style. \item[$\bullet$] Nitpick maintains a global cache of wellfoundedness conditions, which can become invalid if you change the definition of an inductive predicate diff -r 8ed3a5fb4d25 -r 17d9808ed626 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Aug 05 22:29:43 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Aug 06 11:37:33 2010 +0200 @@ -240,13 +240,14 @@ else orig_t val tfree_table = if merge_type_vars then - merged_type_var_table_for_terms (neg_t :: assm_ts @ evals) + merged_type_var_table_for_terms thy (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) + val neg_t = merge_type_vars_in_term thy merge_type_vars tfree_table neg_t + val assm_ts = map (merge_type_vars_in_term thy merge_type_vars tfree_table) assm_ts - val evals = map (merge_type_vars_in_term merge_type_vars tfree_table) evals + val evals = map (merge_type_vars_in_term thy 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 @@ -364,14 +365,25 @@ exists (curry (op =) T o domain_type o type_of) sel_names val all_Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts) |> sort Term_Ord.typ_ord - val _ = if verbose andalso binary_ints = SOME true andalso - exists (member (op =) [nat_T, int_T]) all_Ts then - print_v (K "The option \"binary_ints\" will be ignored because \ - \of the presence of rationals, reals, \"Suc\", \ - \\"gcd\", or \"lcm\" in the problem or because of the \ - \\"non_std\" option.") - else - () + val _ = + if verbose andalso binary_ints = SOME true andalso + exists (member (op =) [nat_T, int_T]) all_Ts then + print_v (K "The option \"binary_ints\" will be ignored because of the \ + \presence of rationals, reals, \"Suc\", \"gcd\", or \"lcm\" \ + \in the problem or because of the \"non_std\" option.") + else + () + val _ = + if not auto andalso + exists (fn Type (@{type_name Datatype.node}, _) => true | _ => false) + all_Ts then + print_m (K ("Warning: The problem involves directly or indirectly the \ + \internal type " ^ quote @{type_name Datatype.node} ^ + ". This type is very Nitpick-unfriendly, and its presence \ + \usually indicates either a failure in abstraction or a \ + \bug in Nitpick.")) + else + () val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts val _ = if verbose andalso not unique_scope then diff -r 8ed3a5fb4d25 -r 17d9808ed626 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Aug 05 22:29:43 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Aug 06 11:37:33 2010 +0200 @@ -113,8 +113,8 @@ val dest_n_tuple : int -> term -> term list val is_real_datatype : theory -> string -> bool val is_standard_datatype : theory -> (typ option * bool) list -> typ -> bool + val is_codatatype : theory -> typ -> bool val is_quot_type : theory -> typ -> bool - val is_codatatype : theory -> typ -> bool val is_pure_typedef : Proof.context -> typ -> bool val is_univ_typedef : Proof.context -> typ -> bool val is_datatype : Proof.context -> (typ option * bool) list -> typ -> bool @@ -212,8 +212,10 @@ 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 merged_type_var_table_for_terms : term list -> (sort * string) list - val merge_type_vars_in_term : bool -> (sort * string) list -> term -> term + val merged_type_var_table_for_terms : + theory -> term list -> (sort * string) list + val merge_type_vars_in_term : + theory -> 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; @@ -638,17 +640,19 @@ in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end fun unregister_codatatype co_T = register_codatatype co_T "" [] -fun is_quot_type thy (Type (s, _)) = - is_some (Quotient_Info.quotdata_lookup_raw thy s) - | is_quot_type _ _ = false fun is_codatatype thy (Type (s, _)) = not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s |> Option.map snd |> these)) | is_codatatype _ _ = false +fun is_real_quot_type thy (Type (s, _)) = + is_some (Quotient_Info.quotdata_lookup_raw thy s) + | is_real_quot_type _ _ = false +fun is_quot_type thy T = + is_real_quot_type thy T andalso not (is_codatatype thy T) fun is_pure_typedef ctxt (T as Type (s, _)) = let val thy = ProofContext.theory_of ctxt in is_typedef ctxt s andalso - not (is_real_datatype thy s orelse is_quot_type thy T orelse + not (is_real_datatype thy s orelse is_real_quot_type thy T orelse is_codatatype thy T orelse is_record_type T orelse is_integer_like_type T) end @@ -679,7 +683,7 @@ fun is_datatype ctxt stds (T as Type (s, _)) = let val thy = ProofContext.theory_of ctxt in (is_typedef ctxt s orelse is_codatatype thy T orelse T = @{typ ind} orelse - is_quot_type thy T) andalso not (is_basic_datatype thy stds s) + is_real_quot_type thy T) andalso not (is_basic_datatype thy stds s) end | is_datatype _ _ _ = false @@ -716,15 +720,19 @@ SOME {Rep_name, ...} => s = Rep_name | NONE => false) | is_rep_fun _ _ = false -fun is_quot_abs_fun ctxt - (x as (_, Type (@{type_name fun}, [_, Type (s', _)]))) = - (try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s' - = SOME (Const x)) +fun is_quot_abs_fun ctxt (x as (_, Type (@{type_name fun}, + [_, abs_T as Type (s', _)]))) = + let val thy = ProofContext.theory_of ctxt in + (try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s' + = SOME (Const x)) andalso not (is_codatatype thy abs_T) + end | is_quot_abs_fun _ _ = false -fun is_quot_rep_fun ctxt - (x as (_, Type (@{type_name fun}, [Type (s', _), _]))) = - (try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s' - = SOME (Const x)) +fun is_quot_rep_fun ctxt (x as (_, Type (@{type_name fun}, + [abs_T as Type (s', _), _]))) = + let val thy = ProofContext.theory_of ctxt in + (try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s' + = SOME (Const x)) andalso not (is_codatatype thy abs_T) + end | is_quot_rep_fun _ _ = false fun mate_of_rep_fun ctxt (x as (_, Type (@{type_name fun}, @@ -911,7 +919,7 @@ val T' = (Record.get_extT_fields thy T |> apsnd single |> uncurry append |> map snd) ---> T in [(s', T')] end - else if is_quot_type thy T then + else if is_real_quot_type thy T then [(@{const_name Quot}, rep_type_for_quot_type thy T --> T)] else case typedef_info ctxt s of SOME {abs_type, rep_type, Abs_name, ...} => @@ -2255,21 +2263,25 @@ (** Type preprocessing **) -fun merged_type_var_table_for_terms ts = +fun merged_type_var_table_for_terms thy ts = let - fun add_type (TFree (s, S)) table = - (case AList.lookup (op =) table S of - SOME s' => - if string_ord (s', s) = LESS then AList.update (op =) (S, s') table - else table - | NONE => (S, s) :: table) - | add_type _ table = table - in fold (fold_types (fold_atyps add_type)) ts [] end + fun add (s, S) table = + table + |> (case AList.lookup (Sign.subsort thy o swap) table S of + SOME _ => I + | NONE => + filter_out (fn (S', _) => Sign.subsort thy (S, S')) + #> cons (S, s)) + val tfrees = [] |> fold Term.add_tfrees ts + |> sort (string_ord o pairself fst) + in [] |> fold add tfrees |> rev end -fun merge_type_vars_in_term merge_type_vars table = +fun merge_type_vars_in_term thy merge_type_vars table = merge_type_vars ? map_types (map_atyps - (fn TFree (_, S) => TFree (AList.lookup (op =) table S |> the, S) + (fn TFree (_, S) => + TFree (table |> find_first (fn (S', _) => Sign.subsort thy (S', S)) + |> the |> swap) | T => T)) fun add_ground_types hol_ctxt binarize = diff -r 8ed3a5fb4d25 -r 17d9808ed626 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Aug 05 22:29:43 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Aug 06 11:37:33 2010 +0200 @@ -902,7 +902,7 @@ |> (fn dtypes' => dtypes' |> length dtypes' > datatype_sym_break - ? (sort (rev_order o datatype_ord) + ? (sort (datatype_ord o swap) #> take datatype_sym_break))) fun sel_axiom_for_sel hol_ctxt binarize j0 diff -r 8ed3a5fb4d25 -r 17d9808ed626 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Aug 05 22:29:43 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Aug 06 11:37:33 2010 +0200 @@ -960,31 +960,25 @@ fold (add_nondef_axiom depth) (nondef_props_for_const thy true choice_spec_table x) accum else if is_abs_fun ctxt x then - if is_quot_type thy (range_type T) then - accum - else - accum |> fold (add_nondef_axiom depth) - (nondef_props_for_const thy false nondef_table x) - |> (is_funky_typedef thy (range_type T) orelse - range_type T = nat_T) - ? fold (add_maybe_def_axiom depth) - (nondef_props_for_const thy true + accum |> fold (add_nondef_axiom depth) + (nondef_props_for_const thy false nondef_table x) + |> (is_funky_typedef thy (range_type T) orelse + range_type T = nat_T) + ? fold (add_maybe_def_axiom depth) + (nondef_props_for_const thy true (extra_table def_table s) x) else if is_rep_fun ctxt x then - if is_quot_type thy (domain_type T) then - accum - else - accum |> fold (add_nondef_axiom depth) - (nondef_props_for_const thy false nondef_table x) - |> (is_funky_typedef thy (range_type T) orelse - range_type T = nat_T) - ? fold (add_maybe_def_axiom depth) - (nondef_props_for_const thy true + accum |> fold (add_nondef_axiom depth) + (nondef_props_for_const thy false nondef_table x) + |> (is_funky_typedef thy (range_type T) orelse + range_type T = nat_T) + ? fold (add_maybe_def_axiom depth) + (nondef_props_for_const thy true (extra_table def_table s) x) - |> add_axioms_for_term depth - (Const (mate_of_rep_fun ctxt x)) - |> fold (add_def_axiom depth) - (inverse_axioms_for_rep_fun ctxt x) + |> add_axioms_for_term depth + (Const (mate_of_rep_fun ctxt x)) + |> fold (add_def_axiom depth) + (inverse_axioms_for_rep_fun ctxt x) else if s = @{const_name TYPE} then accum else case def_of_const thy def_table x of