added some missing well-annotatedness constraints to monotonicity calculus
authorblanchet
Mon Dec 06 13:33:09 2010 +0100 (2010-12-06)
changeset 410115c2f16eae066
parent 41010 1e5f382c48cc
child 41012 e5a23ffb5524
added some missing well-annotatedness constraints to monotonicity calculus
src/HOL/Tools/Nitpick/nitpick_mono.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     1.3 @@ -246,7 +246,7 @@
     1.4                  $ (Const (@{const_name unknown}, ran_T)) $ (t0 $ t1 $ t2 $ t3)))
     1.5    | fin_fun_body _ _ _ = NONE
     1.6  
     1.7 -(* ### FIXME: make sure wellformed! *)
     1.8 +(* ### FIXME: make sure well-annotated! *)
     1.9  
    1.10  fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) all_minus
    1.11                              T1 T2 =
    1.12 @@ -787,8 +787,6 @@
    1.13          <= length ts
    1.14        | _ => true
    1.15      val mtype_for = fresh_mtype_for_type mdata false
    1.16 -    fun plus_set_mtype_for_dom M =
    1.17 -      MFun (M, A (if exists_alpha_sub_mtype M then Fls else Gen), bool_M)
    1.18      fun do_all T (gamma, cset) =
    1.19        let
    1.20          val abs_M = mtype_for (domain_type (domain_type T))
    1.21 @@ -891,7 +889,10 @@
    1.22                    MFun (mtype_for (domain_type T), V x, bool_M)
    1.23                  val ab_set_M = domain_type T |> mtype_for_set
    1.24                  val ba_set_M = range_type T |> mtype_for_set
    1.25 -              in (MFun (ab_set_M, A Gen, ba_set_M), accum) end
    1.26 +              in
    1.27 +                (MFun (ab_set_M, A Gen, ba_set_M),
    1.28 +                 accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
    1.29 +              end
    1.30              | @{const_name trancl} => do_fragile_set_operation T accum
    1.31              | @{const_name rel_comp} =>
    1.32                let
    1.33 @@ -903,21 +904,24 @@
    1.34                  val ac_set_M = nth_range_type 2 T |> mtype_for_set
    1.35                in
    1.36                  (MFun (bc_set_M, A Gen, MFun (ab_set_M, A Gen, ac_set_M)),
    1.37 -                 accum)
    1.38 +                 accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
    1.39                end
    1.40              | @{const_name image} =>
    1.41                let
    1.42 +                val x = Unsynchronized.inc max_fresh
    1.43                  val a_M = mtype_for (domain_type (domain_type T))
    1.44                  val b_M = mtype_for (range_type (domain_type T))
    1.45                in
    1.46                  (MFun (MFun (a_M, A Gen, b_M), A Gen,
    1.47 -                       MFun (plus_set_mtype_for_dom a_M, A Gen,
    1.48 -                             plus_set_mtype_for_dom b_M)), accum)
    1.49 +                       MFun (MFun (a_M, V x, bool_M), A Gen,
    1.50 +                             MFun (b_M, V x, bool_M))),
    1.51 +                 accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
    1.52                end
    1.53              | @{const_name finite} =>
    1.54 -              let val M1 = mtype_for (domain_type (domain_type T)) in
    1.55 -                (MFun (plus_set_mtype_for_dom M1, A Gen, bool_M), accum)
    1.56 -              end
    1.57 +              let
    1.58 +                val M1 = mtype_for (domain_type (domain_type T))
    1.59 +                val a = if exists_alpha_sub_mtype M1 then Fls else Gen
    1.60 +              in (MFun (MFun (M1, A a, bool_M), A Gen, bool_M), accum) end
    1.61              | @{const_name Sigma} =>
    1.62                let
    1.63                  val x = Unsynchronized.inc max_fresh
    1.64 @@ -932,7 +936,7 @@
    1.65                  val ab_set_M = mtype_for_set (nth_range_type 2 T)
    1.66                in
    1.67                  (MFun (a_set_M, A Gen, MFun (a_to_b_set_M, A Gen, ab_set_M)),
    1.68 -                 accum)
    1.69 +                 accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
    1.70                end
    1.71              | _ =>
    1.72                if s = @{const_name safe_The} then