1.1 --- a/doc-src/Nitpick/nitpick.tex Thu Aug 05 22:29:43 2010 +0200
1.2 +++ b/doc-src/Nitpick/nitpick.tex Fri Aug 06 11:37:33 2010 +0200
1.3 @@ -2864,16 +2864,19 @@
1.4 \textbf{by}~(\textit{auto simp}:~\textit{prec\_def})
1.5 \postw
1.6
1.7 -Such theorems are considered bad style because they rely on the internal
1.8 -representation of functions synthesized by Isabelle, which is an implementation
1.9 +Such theorems are generally considered bad style because they rely on the
1.10 +internal representation of functions synthesized by Isabelle, an implementation
1.11 detail.
1.12
1.13 \item[$\bullet$] Similarly, Nitpick might find spurious counterexamples for
1.14 theorems that rely on the use of the indefinite description operator internally
1.15 by \textbf{specification} and \textbf{quot\_type}.
1.16
1.17 -\item[$\bullet$] Axioms that restrict the possible values of the
1.18 -\textit{undefined} constant are in general ignored.
1.19 +\item[$\bullet$] Axioms or definitions that restrict the possible values of the
1.20 +\textit{undefined} constant or other partially specified built-in Isabelle
1.21 +constants (e.g., \textit{Abs\_} and \textit{Rep\_} constants) are in general
1.22 +ignored. Again, such nonconservative extensions are generally considered bad
1.23 +style.
1.24
1.25 \item[$\bullet$] Nitpick maintains a global cache of wellfoundedness conditions,
1.26 which can become invalid if you change the definition of an inductive predicate
2.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Aug 05 22:29:43 2010 +0200
2.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Aug 06 11:37:33 2010 +0200
2.3 @@ -240,13 +240,14 @@
2.4 else orig_t
2.5 val tfree_table =
2.6 if merge_type_vars then
2.7 - merged_type_var_table_for_terms (neg_t :: assm_ts @ evals)
2.8 + merged_type_var_table_for_terms thy (neg_t :: assm_ts @ evals)
2.9 else
2.10 []
2.11 - val neg_t = merge_type_vars_in_term merge_type_vars tfree_table neg_t
2.12 - val assm_ts = map (merge_type_vars_in_term merge_type_vars tfree_table)
2.13 + val neg_t = merge_type_vars_in_term thy merge_type_vars tfree_table neg_t
2.14 + val assm_ts = map (merge_type_vars_in_term thy merge_type_vars tfree_table)
2.15 assm_ts
2.16 - val evals = map (merge_type_vars_in_term merge_type_vars tfree_table) evals
2.17 + val evals = map (merge_type_vars_in_term thy merge_type_vars tfree_table)
2.18 + evals
2.19 val original_max_potential = max_potential
2.20 val original_max_genuine = max_genuine
2.21 val max_bisim_depth = fold Integer.max bisim_depths ~1
2.22 @@ -364,14 +365,25 @@
2.23 exists (curry (op =) T o domain_type o type_of) sel_names
2.24 val all_Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
2.25 |> sort Term_Ord.typ_ord
2.26 - val _ = if verbose andalso binary_ints = SOME true andalso
2.27 - exists (member (op =) [nat_T, int_T]) all_Ts then
2.28 - print_v (K "The option \"binary_ints\" will be ignored because \
2.29 - \of the presence of rationals, reals, \"Suc\", \
2.30 - \\"gcd\", or \"lcm\" in the problem or because of the \
2.31 - \\"non_std\" option.")
2.32 - else
2.33 - ()
2.34 + val _ =
2.35 + if verbose andalso binary_ints = SOME true andalso
2.36 + exists (member (op =) [nat_T, int_T]) all_Ts then
2.37 + print_v (K "The option \"binary_ints\" will be ignored because of the \
2.38 + \presence of rationals, reals, \"Suc\", \"gcd\", or \"lcm\" \
2.39 + \in the problem or because of the \"non_std\" option.")
2.40 + else
2.41 + ()
2.42 + val _ =
2.43 + if not auto andalso
2.44 + exists (fn Type (@{type_name Datatype.node}, _) => true | _ => false)
2.45 + all_Ts then
2.46 + print_m (K ("Warning: The problem involves directly or indirectly the \
2.47 + \internal type " ^ quote @{type_name Datatype.node} ^
2.48 + ". This type is very Nitpick-unfriendly, and its presence \
2.49 + \usually indicates either a failure in abstraction or a \
2.50 + \bug in Nitpick."))
2.51 + else
2.52 + ()
2.53 val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts
2.54 val _ =
2.55 if verbose andalso not unique_scope then
3.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Aug 05 22:29:43 2010 +0200
3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Aug 06 11:37:33 2010 +0200
3.3 @@ -113,8 +113,8 @@
3.4 val dest_n_tuple : int -> term -> term list
3.5 val is_real_datatype : theory -> string -> bool
3.6 val is_standard_datatype : theory -> (typ option * bool) list -> typ -> bool
3.7 + val is_codatatype : theory -> typ -> bool
3.8 val is_quot_type : theory -> typ -> bool
3.9 - val is_codatatype : theory -> typ -> bool
3.10 val is_pure_typedef : Proof.context -> typ -> bool
3.11 val is_univ_typedef : Proof.context -> typ -> bool
3.12 val is_datatype : Proof.context -> (typ option * bool) list -> typ -> bool
3.13 @@ -212,8 +212,10 @@
3.14 val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term
3.15 val equational_fun_axioms : hol_context -> styp -> term list
3.16 val is_equational_fun_surely_complete : hol_context -> styp -> bool
3.17 - val merged_type_var_table_for_terms : term list -> (sort * string) list
3.18 - val merge_type_vars_in_term : bool -> (sort * string) list -> term -> term
3.19 + val merged_type_var_table_for_terms :
3.20 + theory -> term list -> (sort * string) list
3.21 + val merge_type_vars_in_term :
3.22 + theory -> bool -> (sort * string) list -> term -> term
3.23 val ground_types_in_type : hol_context -> bool -> typ -> typ list
3.24 val ground_types_in_terms : hol_context -> bool -> term list -> typ list
3.25 end;
3.26 @@ -638,17 +640,19 @@
3.27 in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
3.28 fun unregister_codatatype co_T = register_codatatype co_T "" []
3.29
3.30 -fun is_quot_type thy (Type (s, _)) =
3.31 - is_some (Quotient_Info.quotdata_lookup_raw thy s)
3.32 - | is_quot_type _ _ = false
3.33 fun is_codatatype thy (Type (s, _)) =
3.34 not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
3.35 |> Option.map snd |> these))
3.36 | is_codatatype _ _ = false
3.37 +fun is_real_quot_type thy (Type (s, _)) =
3.38 + is_some (Quotient_Info.quotdata_lookup_raw thy s)
3.39 + | is_real_quot_type _ _ = false
3.40 +fun is_quot_type thy T =
3.41 + is_real_quot_type thy T andalso not (is_codatatype thy T)
3.42 fun is_pure_typedef ctxt (T as Type (s, _)) =
3.43 let val thy = ProofContext.theory_of ctxt in
3.44 is_typedef ctxt s andalso
3.45 - not (is_real_datatype thy s orelse is_quot_type thy T orelse
3.46 + not (is_real_datatype thy s orelse is_real_quot_type thy T orelse
3.47 is_codatatype thy T orelse is_record_type T orelse
3.48 is_integer_like_type T)
3.49 end
3.50 @@ -679,7 +683,7 @@
3.51 fun is_datatype ctxt stds (T as Type (s, _)) =
3.52 let val thy = ProofContext.theory_of ctxt in
3.53 (is_typedef ctxt s orelse is_codatatype thy T orelse T = @{typ ind} orelse
3.54 - is_quot_type thy T) andalso not (is_basic_datatype thy stds s)
3.55 + is_real_quot_type thy T) andalso not (is_basic_datatype thy stds s)
3.56 end
3.57 | is_datatype _ _ _ = false
3.58
3.59 @@ -716,15 +720,19 @@
3.60 SOME {Rep_name, ...} => s = Rep_name
3.61 | NONE => false)
3.62 | is_rep_fun _ _ = false
3.63 -fun is_quot_abs_fun ctxt
3.64 - (x as (_, Type (@{type_name fun}, [_, Type (s', _)]))) =
3.65 - (try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s'
3.66 - = SOME (Const x))
3.67 +fun is_quot_abs_fun ctxt (x as (_, Type (@{type_name fun},
3.68 + [_, abs_T as Type (s', _)]))) =
3.69 + let val thy = ProofContext.theory_of ctxt in
3.70 + (try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s'
3.71 + = SOME (Const x)) andalso not (is_codatatype thy abs_T)
3.72 + end
3.73 | is_quot_abs_fun _ _ = false
3.74 -fun is_quot_rep_fun ctxt
3.75 - (x as (_, Type (@{type_name fun}, [Type (s', _), _]))) =
3.76 - (try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s'
3.77 - = SOME (Const x))
3.78 +fun is_quot_rep_fun ctxt (x as (_, Type (@{type_name fun},
3.79 + [abs_T as Type (s', _), _]))) =
3.80 + let val thy = ProofContext.theory_of ctxt in
3.81 + (try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s'
3.82 + = SOME (Const x)) andalso not (is_codatatype thy abs_T)
3.83 + end
3.84 | is_quot_rep_fun _ _ = false
3.85
3.86 fun mate_of_rep_fun ctxt (x as (_, Type (@{type_name fun},
3.87 @@ -911,7 +919,7 @@
3.88 val T' = (Record.get_extT_fields thy T
3.89 |> apsnd single |> uncurry append |> map snd) ---> T
3.90 in [(s', T')] end
3.91 - else if is_quot_type thy T then
3.92 + else if is_real_quot_type thy T then
3.93 [(@{const_name Quot}, rep_type_for_quot_type thy T --> T)]
3.94 else case typedef_info ctxt s of
3.95 SOME {abs_type, rep_type, Abs_name, ...} =>
3.96 @@ -2255,21 +2263,25 @@
3.97
3.98 (** Type preprocessing **)
3.99
3.100 -fun merged_type_var_table_for_terms ts =
3.101 +fun merged_type_var_table_for_terms thy ts =
3.102 let
3.103 - fun add_type (TFree (s, S)) table =
3.104 - (case AList.lookup (op =) table S of
3.105 - SOME s' =>
3.106 - if string_ord (s', s) = LESS then AList.update (op =) (S, s') table
3.107 - else table
3.108 - | NONE => (S, s) :: table)
3.109 - | add_type _ table = table
3.110 - in fold (fold_types (fold_atyps add_type)) ts [] end
3.111 + fun add (s, S) table =
3.112 + table
3.113 + |> (case AList.lookup (Sign.subsort thy o swap) table S of
3.114 + SOME _ => I
3.115 + | NONE =>
3.116 + filter_out (fn (S', _) => Sign.subsort thy (S, S'))
3.117 + #> cons (S, s))
3.118 + val tfrees = [] |> fold Term.add_tfrees ts
3.119 + |> sort (string_ord o pairself fst)
3.120 + in [] |> fold add tfrees |> rev end
3.121
3.122 -fun merge_type_vars_in_term merge_type_vars table =
3.123 +fun merge_type_vars_in_term thy merge_type_vars table =
3.124 merge_type_vars
3.125 ? map_types (map_atyps
3.126 - (fn TFree (_, S) => TFree (AList.lookup (op =) table S |> the, S)
3.127 + (fn TFree (_, S) =>
3.128 + TFree (table |> find_first (fn (S', _) => Sign.subsort thy (S', S))
3.129 + |> the |> swap)
3.130 | T => T))
3.131
3.132 fun add_ground_types hol_ctxt binarize =
4.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Aug 05 22:29:43 2010 +0200
4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Aug 06 11:37:33 2010 +0200
4.3 @@ -902,7 +902,7 @@
4.4 |> (fn dtypes' =>
4.5 dtypes'
4.6 |> length dtypes' > datatype_sym_break
4.7 - ? (sort (rev_order o datatype_ord)
4.8 + ? (sort (datatype_ord o swap)
4.9 #> take datatype_sym_break)))
4.10
4.11 fun sel_axiom_for_sel hol_ctxt binarize j0
5.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Aug 05 22:29:43 2010 +0200
5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Aug 06 11:37:33 2010 +0200
5.3 @@ -960,31 +960,25 @@
5.4 fold (add_nondef_axiom depth)
5.5 (nondef_props_for_const thy true choice_spec_table x) accum
5.6 else if is_abs_fun ctxt x then
5.7 - if is_quot_type thy (range_type T) then
5.8 - accum
5.9 - else
5.10 - accum |> fold (add_nondef_axiom depth)
5.11 - (nondef_props_for_const thy false nondef_table x)
5.12 - |> (is_funky_typedef thy (range_type T) orelse
5.13 - range_type T = nat_T)
5.14 - ? fold (add_maybe_def_axiom depth)
5.15 - (nondef_props_for_const thy true
5.16 + accum |> fold (add_nondef_axiom depth)
5.17 + (nondef_props_for_const thy false nondef_table x)
5.18 + |> (is_funky_typedef thy (range_type T) orelse
5.19 + range_type T = nat_T)
5.20 + ? fold (add_maybe_def_axiom depth)
5.21 + (nondef_props_for_const thy true
5.22 (extra_table def_table s) x)
5.23 else if is_rep_fun ctxt x then
5.24 - if is_quot_type thy (domain_type T) then
5.25 - accum
5.26 - else
5.27 - accum |> fold (add_nondef_axiom depth)
5.28 - (nondef_props_for_const thy false nondef_table x)
5.29 - |> (is_funky_typedef thy (range_type T) orelse
5.30 - range_type T = nat_T)
5.31 - ? fold (add_maybe_def_axiom depth)
5.32 - (nondef_props_for_const thy true
5.33 + accum |> fold (add_nondef_axiom depth)
5.34 + (nondef_props_for_const thy false nondef_table x)
5.35 + |> (is_funky_typedef thy (range_type T) orelse
5.36 + range_type T = nat_T)
5.37 + ? fold (add_maybe_def_axiom depth)
5.38 + (nondef_props_for_const thy true
5.39 (extra_table def_table s) x)
5.40 - |> add_axioms_for_term depth
5.41 - (Const (mate_of_rep_fun ctxt x))
5.42 - |> fold (add_def_axiom depth)
5.43 - (inverse_axioms_for_rep_fun ctxt x)
5.44 + |> add_axioms_for_term depth
5.45 + (Const (mate_of_rep_fun ctxt x))
5.46 + |> fold (add_def_axiom depth)
5.47 + (inverse_axioms_for_rep_fun ctxt x)
5.48 else if s = @{const_name TYPE} then
5.49 accum
5.50 else case def_of_const thy def_table x of