--- 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
--- 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
--- 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 =
--- 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
--- 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