# HG changeset patch # User blanchet # Date 1281024050 -7200 # Node ID 792b78e355e7a37a831d608f7f56910509717643 # Parent 78403fcd0ec5c72de8c7acea5bce77575361c603 added support for "Abs_" and "Rep_" functions on quotient types diff -r 78403fcd0ec5 -r 792b78e355e7 doc-src/Nitpick/nitpick.tex --- 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. diff -r 78403fcd0ec5 -r 792b78e355e7 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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), diff -r 78403fcd0ec5 -r 792b78e355e7 src/HOL/Tools/Nitpick/nitpick_model.ML --- 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 diff -r 78403fcd0ec5 -r 792b78e355e7 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- 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)