added support for "Abs_" and "Rep_" functions on quotient types
authorblanchet
Thu Aug 05 18:00:50 2010 +0200 (2010-08-05)
changeset 38207792b78e355e7
parent 38206 78403fcd0ec5
child 38208 10417cd47448
added support for "Abs_" and "Rep_" functions on quotient types
doc-src/Nitpick/nitpick.tex
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
     1.1 --- a/doc-src/Nitpick/nitpick.tex	Thu Aug 05 15:44:54 2010 +0200
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Thu Aug 05 18:00:50 2010 +0200
     1.3 @@ -2860,6 +2860,10 @@
     1.4  representation of functions synthesized by Isabelle, which is an implementation
     1.5  detail.
     1.6  
     1.7 +\item[$\bullet$] Similarly, Nitpick might find spurious counterexamples for
     1.8 +theorems that rely on the use of the indefinite description operator internally
     1.9 +by \textbf{specification} and \textbf{quot\_type}.
    1.10 +
    1.11  \item[$\bullet$] Axioms that restrict the possible values of the
    1.12  \textit{undefined} constant are in general ignored.
    1.13  
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Aug 05 15:44:54 2010 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Aug 05 18:00:50 2010 +0200
     2.3 @@ -1637,6 +1637,9 @@
     2.4                select_nth_constr_arg ctxt stds x (Bound 0) n res_T), [])
     2.5        | select_nth_constr_arg_with_args depth Ts x (t :: ts) n res_T =
     2.6          (select_nth_constr_arg ctxt stds x (do_term depth Ts t) n res_T, ts)
     2.7 +    and quot_rep_of depth Ts abs_T rep_T ts =
     2.8 +      select_nth_constr_arg_with_args depth Ts
     2.9 +          (@{const_name Quot}, rep_T --> abs_T) ts 0 rep_T
    2.10      and do_const depth Ts t (x as (s, T)) ts =
    2.11        case AList.lookup (op =) ersatz_table s of
    2.12          SOME s' =>
    2.13 @@ -1681,11 +1684,7 @@
    2.14                                           rep_T --> rep_T) $ Bound 0)), ts)
    2.15                  end
    2.16                else if is_quot_rep_fun ctxt x then
    2.17 -                let
    2.18 -                  val abs_T = domain_type T
    2.19 -                  val rep_T = range_type T
    2.20 -                  val x' = (@{const_name Quot}, rep_T --> abs_T)
    2.21 -                in select_nth_constr_arg_with_args depth Ts x' ts 0 rep_T end
    2.22 +                quot_rep_of depth Ts (domain_type T) (range_type T) ts
    2.23                else if is_record_get thy x then
    2.24                  case length ts of
    2.25                    0 => (do_term depth Ts (eta_expand Ts t 1), [])
    2.26 @@ -1698,13 +1697,40 @@
    2.27                              (do_term depth Ts (hd ts))
    2.28                              (do_term depth Ts (nth ts 1)), [])
    2.29                  | n => (do_term depth Ts (eta_expand Ts t (2 - n)), [])
    2.30 +              else if is_abs_fun ctxt x andalso
    2.31 +                      is_quot_type thy (range_type T) then
    2.32 +                let
    2.33 +                  val abs_T = range_type T
    2.34 +                  val rep_T = domain_type (domain_type T)
    2.35 +                  val eps_fun = Const (@{const_name Eps},
    2.36 +                                       (rep_T --> bool_T) --> rep_T)
    2.37 +                  val normal_fun = 
    2.38 +                    Const (quot_normal_name_for_type ctxt abs_T,
    2.39 +                           rep_T --> rep_T)
    2.40 +                  val abs_fun = Const (@{const_name Quot}, rep_T --> abs_T)
    2.41 +                in
    2.42 +                  (Abs (Name.uu, rep_T --> bool_T,
    2.43 +                        abs_fun $ (normal_fun $ (eps_fun $ Bound 0)))
    2.44 +                   |> do_term (depth + 1) Ts, ts)
    2.45 +                end
    2.46                else if is_rep_fun ctxt x then
    2.47                  let val x' = mate_of_rep_fun ctxt x in
    2.48                    if is_constr ctxt stds x' then
    2.49                      select_nth_constr_arg_with_args depth Ts x' ts 0
    2.50                                                      (range_type T)
    2.51 +                  else if is_quot_type thy (domain_type T) then
    2.52 +                    let
    2.53 +                      val abs_T = domain_type T
    2.54 +                      val rep_T = domain_type (range_type T)
    2.55 +                      val (rep_fun, _) = quot_rep_of depth Ts abs_T rep_T []
    2.56 +                      val equiv_rel = equiv_relation_for_quot_type thy abs_T
    2.57 +                    in
    2.58 +                      (Abs (Name.uu, abs_T, equiv_rel $ (rep_fun $ Bound 0)),
    2.59 +                       ts)
    2.60 +                    end
    2.61                    else
    2.62 -                    (Const x, ts)
    2.63 +                    raise TERM ("Nitpick_HOL.unfold_defs_in_term.do_const",
    2.64 +                                [Const x])
    2.65                  end
    2.66                else if is_equational_fun_but_no_plain_def hol_ctxt x orelse
    2.67                        is_choice_spec_fun hol_ctxt x then
    2.68 @@ -1866,12 +1892,13 @@
    2.69      val y_var = Var (("y", 0), rep_T)
    2.70      val x = (@{const_name Quot}, rep_T --> abs_T)
    2.71      val sel_a_t = select_nth_constr_arg ctxt stds x a_var 0 rep_T
    2.72 -    val normal_t = Const (quot_normal_name_for_type ctxt abs_T, rep_T --> rep_T)
    2.73 -    val normal_x = normal_t $ x_var
    2.74 -    val normal_y = normal_t $ y_var
    2.75 +    val normal_fun =
    2.76 +      Const (quot_normal_name_for_type ctxt abs_T, rep_T --> rep_T)
    2.77 +    val normal_x = normal_fun $ x_var
    2.78 +    val normal_y = normal_fun $ y_var
    2.79      val is_unknown_t = Const (@{const_name is_unknown}, rep_T --> bool_T)
    2.80    in
    2.81 -    [Logic.mk_equals (normal_t $ sel_a_t, sel_a_t),
    2.82 +    [Logic.mk_equals (normal_fun $ sel_a_t, sel_a_t),
    2.83       Logic.list_implies
    2.84           ([@{const Not} $ (is_unknown_t $ normal_x),
    2.85             @{const Not} $ (is_unknown_t $ normal_y),
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Aug 05 15:44:54 2010 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Aug 05 18:00:50 2010 +0200
     3.3 @@ -779,7 +779,7 @@
     3.4           (Const (step_name, T --> T) $ Const (unprefix step_prefix s, T),
     3.5            format_type default_format default_format T)
     3.6         else if String.isPrefix quot_normal_prefix s then
     3.7 -         let val t = Const (nitpick_prefix ^ "normalize quotient type", T) in
     3.8 +         let val t = Const (nitpick_prefix ^ "quotient normal form", T) in
     3.9             (t, format_term_type thy def_table formats t)
    3.10           end
    3.11         else if String.isPrefix skolem_prefix s then
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Aug 05 15:44:54 2010 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Aug 05 18:00:50 2010 +0200
     4.3 @@ -961,7 +961,7 @@
     4.4                      (nondef_props_for_const thy true choice_spec_table x) accum
     4.5               else if is_abs_fun ctxt x then
     4.6                 if is_quot_type thy (range_type T) then
     4.7 -                 raise NOT_SUPPORTED "\"Abs_\" function of quotient type"
     4.8 +                 accum
     4.9                 else
    4.10                   accum |> fold (add_nondef_axiom depth)
    4.11                                 (nondef_props_for_const thy false nondef_table x)
    4.12 @@ -972,7 +972,7 @@
    4.13                                                      (extra_table def_table s) x)
    4.14               else if is_rep_fun ctxt x then
    4.15                 if is_quot_type thy (domain_type T) then
    4.16 -                 raise NOT_SUPPORTED "\"Rep_\" function of quotient type"
    4.17 +                 accum
    4.18                 else
    4.19                   accum |> fold (add_nondef_axiom depth)
    4.20                                 (nondef_props_for_const thy false nondef_table x)