--- a/doc-src/Nitpick/nitpick.tex Thu Aug 05 15:44:54 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex Thu Aug 05 18:00:50 2010 +0200
@@ -2860,6 +2860,10 @@
representation of functions synthesized by Isabelle, which is 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.
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Aug 05 15:44:54 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Aug 05 18:00:50 2010 +0200
@@ -1637,6 +1637,9 @@
select_nth_constr_arg ctxt stds x (Bound 0) n res_T), [])
| select_nth_constr_arg_with_args depth Ts x (t :: ts) n res_T =
(select_nth_constr_arg ctxt stds x (do_term depth Ts t) n res_T, ts)
+ and quot_rep_of depth Ts abs_T rep_T ts =
+ select_nth_constr_arg_with_args depth Ts
+ (@{const_name Quot}, rep_T --> abs_T) ts 0 rep_T
and do_const depth Ts t (x as (s, T)) ts =
case AList.lookup (op =) ersatz_table s of
SOME s' =>
@@ -1681,11 +1684,7 @@
rep_T --> rep_T) $ Bound 0)), ts)
end
else if is_quot_rep_fun ctxt x then
- let
- val abs_T = domain_type T
- val rep_T = range_type T
- val x' = (@{const_name Quot}, rep_T --> abs_T)
- in select_nth_constr_arg_with_args depth Ts x' ts 0 rep_T end
+ quot_rep_of depth Ts (domain_type T) (range_type T) ts
else if is_record_get thy x then
case length ts of
0 => (do_term depth Ts (eta_expand Ts t 1), [])
@@ -1698,13 +1697,40 @@
(do_term depth Ts (hd ts))
(do_term depth Ts (nth ts 1)), [])
| n => (do_term depth Ts (eta_expand Ts t (2 - n)), [])
+ else if is_abs_fun ctxt x andalso
+ is_quot_type thy (range_type T) then
+ let
+ val abs_T = range_type T
+ val rep_T = domain_type (domain_type T)
+ val eps_fun = Const (@{const_name Eps},
+ (rep_T --> bool_T) --> rep_T)
+ val normal_fun =
+ Const (quot_normal_name_for_type ctxt abs_T,
+ rep_T --> rep_T)
+ val abs_fun = Const (@{const_name Quot}, rep_T --> abs_T)
+ in
+ (Abs (Name.uu, rep_T --> bool_T,
+ abs_fun $ (normal_fun $ (eps_fun $ Bound 0)))
+ |> do_term (depth + 1) Ts, ts)
+ end
else if is_rep_fun ctxt x then
let val x' = mate_of_rep_fun ctxt x in
if is_constr ctxt stds x' then
select_nth_constr_arg_with_args depth Ts x' ts 0
(range_type T)
+ else if is_quot_type thy (domain_type T) then
+ let
+ val abs_T = domain_type T
+ val rep_T = domain_type (range_type T)
+ val (rep_fun, _) = quot_rep_of depth Ts abs_T rep_T []
+ val equiv_rel = equiv_relation_for_quot_type thy abs_T
+ in
+ (Abs (Name.uu, abs_T, equiv_rel $ (rep_fun $ Bound 0)),
+ ts)
+ end
else
- (Const x, ts)
+ raise TERM ("Nitpick_HOL.unfold_defs_in_term.do_const",
+ [Const x])
end
else if is_equational_fun_but_no_plain_def hol_ctxt x orelse
is_choice_spec_fun hol_ctxt x then
@@ -1866,12 +1892,13 @@
val y_var = Var (("y", 0), rep_T)
val x = (@{const_name Quot}, rep_T --> abs_T)
val sel_a_t = select_nth_constr_arg ctxt stds x a_var 0 rep_T
- val normal_t = Const (quot_normal_name_for_type ctxt abs_T, rep_T --> rep_T)
- val normal_x = normal_t $ x_var
- val normal_y = normal_t $ y_var
+ val normal_fun =
+ Const (quot_normal_name_for_type ctxt abs_T, rep_T --> rep_T)
+ val normal_x = normal_fun $ x_var
+ val normal_y = normal_fun $ y_var
val is_unknown_t = Const (@{const_name is_unknown}, rep_T --> bool_T)
in
- [Logic.mk_equals (normal_t $ sel_a_t, sel_a_t),
+ [Logic.mk_equals (normal_fun $ sel_a_t, sel_a_t),
Logic.list_implies
([@{const Not} $ (is_unknown_t $ normal_x),
@{const Not} $ (is_unknown_t $ normal_y),
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Aug 05 15:44:54 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Aug 05 18:00:50 2010 +0200
@@ -779,7 +779,7 @@
(Const (step_name, T --> T) $ Const (unprefix step_prefix s, T),
format_type default_format default_format T)
else if String.isPrefix quot_normal_prefix s then
- let val t = Const (nitpick_prefix ^ "normalize quotient type", T) in
+ let val t = Const (nitpick_prefix ^ "quotient normal form", T) in
(t, format_term_type thy def_table formats t)
end
else if String.isPrefix skolem_prefix s then
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Aug 05 15:44:54 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Aug 05 18:00:50 2010 +0200
@@ -961,7 +961,7 @@
(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
- raise NOT_SUPPORTED "\"Abs_\" function of quotient type"
+ accum
else
accum |> fold (add_nondef_axiom depth)
(nondef_props_for_const thy false nondef_table x)
@@ -972,7 +972,7 @@
(extra_table def_table s) x)
else if is_rep_fun ctxt x then
if is_quot_type thy (domain_type T) then
- raise NOT_SUPPORTED "\"Rep_\" function of quotient type"
+ accum
else
accum |> fold (add_nondef_axiom depth)
(nondef_props_for_const thy false nondef_table x)