addressed a quotient-type-related issue that arose with the port to "set"
authorblanchet
Sun Mar 04 23:20:43 2012 +0100 (2012-03-04)
changeset 468199b38f8527510
parent 46818 2a28e66e2e4c
child 46820 c656222c4dc1
addressed a quotient-type-related issue that arose with the port to "set"
src/HOL/Tools/Nitpick/nitpick_hol.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Mar 04 23:20:43 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Mar 04 23:20:43 2012 +0100
     1.3 @@ -744,8 +744,8 @@
     1.4      try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.AbsF) s'
     1.5      = SOME (Const x) andalso not (is_codatatype ctxt abs_T)
     1.6    | is_quot_abs_fun _ _ = false
     1.7 -fun is_quot_rep_fun ctxt (x as (s, Type (@{type_name fun},
     1.8 -                                         [abs_T as Type (abs_s, _), _]))) =
     1.9 +fun is_quot_rep_fun ctxt (s, Type (@{type_name fun},
    1.10 +                                   [abs_T as Type (abs_s, _), _])) =
    1.11      (case try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.RepF) abs_s of
    1.12         SOME (Const (s', _)) => s = s' andalso not (is_codatatype ctxt abs_T)
    1.13       | NONE => false)
    1.14 @@ -1767,16 +1767,21 @@
    1.15                        is_quot_type ctxt (range_type T) then
    1.16                  let
    1.17                    val abs_T = range_type T
    1.18 -                  val rep_T = domain_type (domain_type T)
    1.19 +                  val rep_T = elem_type (domain_type T)
    1.20                    val eps_fun = Const (@{const_name Eps},
    1.21                                         (rep_T --> bool_T) --> rep_T)
    1.22                    val normal_fun =
    1.23                      Const (quot_normal_name_for_type ctxt abs_T,
    1.24                             rep_T --> rep_T)
    1.25                    val abs_fun = Const (@{const_name Quot}, rep_T --> abs_T)
    1.26 +                  val pred =
    1.27 +                    Abs (Name.uu, rep_T,
    1.28 +                         Const (@{const_name Set.member},
    1.29 +                                rep_T --> domain_type T --> bool_T)
    1.30 +                         $ Bound 0 $ Bound 1)
    1.31                  in
    1.32 -                  (Abs (Name.uu, rep_T --> bool_T,
    1.33 -                        abs_fun $ (normal_fun $ (eps_fun $ Bound 0)))
    1.34 +                  (Abs (Name.uu, HOLogic.mk_setT rep_T,
    1.35 +                        abs_fun $ (normal_fun $ (eps_fun $ pred)))
    1.36                     |> do_term (depth + 1) Ts, ts)
    1.37                  end
    1.38                else if is_rep_fun ctxt x then