improved precision of infinite "shallow" datatypes in Nitpick;
authorblanchet
Thu Feb 25 16:33:39 2010 +0100 (2010-02-25)
changeset 3538529f81babefd7
parent 35384 88dbcfe75c45
child 35386 45a4e19d3ebd
improved precision of infinite "shallow" datatypes in Nitpick;
e.g. strings used for variable names, instead of an opaque type
doc-src/Nitpick/nitpick.tex
src/HOL/Nitpick_Examples/Mono_Nits.thy
src/HOL/Tools/Nitpick/HISTORY
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_peephole.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Nitpick/nitpick_rep.ML
src/HOL/Tools/Nitpick/nitpick_scope.ML
src/HOL/Tools/Nitpick/nitpick_util.ML
     1.1 --- a/doc-src/Nitpick/nitpick.tex	Thu Feb 25 10:08:44 2010 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Thu Feb 25 16:33:39 2010 +0100
     1.3 @@ -472,7 +472,7 @@
     1.4  \prew
     1.5  \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
     1.6  \textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount]
     1.7 -\slshape Warning: The conjecture either trivially holds for the given scopes or (more likely) lies outside Nitpick's supported
     1.8 +\slshape Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported
     1.9  fragment. Only potential counterexamples may be found. \\[2\smallskipamount]
    1.10  Nitpick found a potential counterexample: \\[2\smallskipamount]
    1.11  \hbox{}\qquad Free variable: \nopagebreak \\
     2.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Feb 25 10:08:44 2010 +0100
     2.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Feb 25 16:33:39 2010 +0100
     2.3 @@ -30,8 +30,7 @@
     2.4     special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
     2.5     wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
     2.6  (* term -> bool *)
     2.7 -val is_mono = Nitpick_Mono.formulas_monotonic hol_ctxt false @{typ 'a}
     2.8 -                                              Nitpick_Mono.Plus [] []
     2.9 +val is_mono = Nitpick_Mono.formulas_monotonic hol_ctxt false @{typ 'a} [] []
    2.10  fun is_const t =
    2.11    let val T = fastype_of t in
    2.12      is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t),
     3.1 --- a/src/HOL/Tools/Nitpick/HISTORY	Thu Feb 25 10:08:44 2010 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/HISTORY	Thu Feb 25 16:33:39 2010 +0100
     3.3 @@ -5,6 +5,8 @@
     3.4    * Added support for quotient types
     3.5    * Added support for local definitions
     3.6    * Optimized "Multiset.multiset"
     3.7 +  * Improved precision of infinite datatypes whose constructors don't appear
     3.8 +    in the formula to falsify based on a monotonicity analysis
     3.9    * Fixed soundness bugs related to "destroy_constrs" optimization and record
    3.10      getters
    3.11    * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Feb 25 10:08:44 2010 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Feb 25 16:33:39 2010 +0100
     4.3 @@ -332,21 +332,36 @@
     4.4  *)
     4.5  
     4.6      val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
     4.7 +    (* typ list -> string -> string *)
     4.8 +    fun monotonicity_message Ts extra =
     4.9 +      let val ss = map (quote o string_for_type ctxt) Ts in
    4.10 +        "The type" ^ plural_s_for_list ss ^ " " ^
    4.11 +        space_implode " " (serial_commas "and" ss) ^ " " ^
    4.12 +        (if none_true monos then
    4.13 +           "passed the monotonicity test"
    4.14 +         else
    4.15 +           (if length ss = 1 then "is" else "are") ^ " considered monotonic") ^
    4.16 +        ". " ^ extra
    4.17 +      end
    4.18      (* typ -> bool *)
    4.19      fun is_type_always_monotonic T =
    4.20        (is_datatype thy stds T andalso not (is_quot_type thy T) andalso
    4.21         (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
    4.22        is_number_type thy T orelse is_bit_type T
    4.23 +    fun is_type_actually_monotonic T =
    4.24 +      formulas_monotonic hol_ctxt binarize T (def_ts, nondef_ts, core_t)
    4.25      fun is_type_monotonic T =
    4.26        unique_scope orelse
    4.27        case triple_lookup (type_match thy) monos T of
    4.28          SOME (SOME b) => b
    4.29 -      | _ => is_type_always_monotonic T orelse
    4.30 -             formulas_monotonic hol_ctxt binarize T (def_ts, nondef_ts, core_t)
    4.31 -    fun is_deep_datatype T =
    4.32 -      is_datatype thy stds T andalso
    4.33 -      (not standard orelse T = nat_T orelse is_word_type T orelse
    4.34 -       exists (curry (op =) T o domain_type o type_of) sel_names)
    4.35 +      | _ => is_type_always_monotonic T orelse is_type_actually_monotonic T
    4.36 +    fun is_type_finitizable T =
    4.37 +      case triple_lookup (type_match thy) monos T of
    4.38 +        SOME (SOME false) => false
    4.39 +      | _ => is_type_actually_monotonic T
    4.40 +    fun is_datatype_deep T =
    4.41 +      not standard orelse T = nat_T orelse is_word_type T orelse
    4.42 +      exists (curry (op =) T o domain_type o type_of) sel_names
    4.43      val all_Ts = ground_types_in_terms hol_ctxt binarize
    4.44                                         (core_t :: def_ts @ nondef_ts)
    4.45                   |> sort TermOrd.typ_ord
    4.46 @@ -363,23 +378,21 @@
    4.47          case filter_out is_type_always_monotonic mono_Ts of
    4.48            [] => ()
    4.49          | interesting_mono_Ts =>
    4.50 -          print_v (fn () =>
    4.51 -                      let
    4.52 -                        val ss = map (quote o string_for_type ctxt)
    4.53 -                                     interesting_mono_Ts
    4.54 -                      in
    4.55 -                        "The type" ^ plural_s_for_list ss ^ " " ^
    4.56 -                        space_implode " " (serial_commas "and" ss) ^ " " ^
    4.57 -                        (if none_true monos then
    4.58 -                           "passed the monotonicity test"
    4.59 -                         else
    4.60 -                           (if length ss = 1 then "is" else "are") ^
    4.61 -                           " considered monotonic") ^
    4.62 -                        ". Nitpick might be able to skip some scopes."
    4.63 -                      end)
    4.64 +          print_v (K (monotonicity_message interesting_mono_Ts
    4.65 +                         "Nitpick might be able to skip some scopes."))
    4.66        else
    4.67          ()
    4.68 -    val deep_dataTs = filter is_deep_datatype all_Ts
    4.69 +    val (deep_dataTs, shallow_dataTs) =
    4.70 +      all_Ts |> filter (is_datatype thy stds) |> List.partition is_datatype_deep
    4.71 +    val finitizable_dataTs =
    4.72 +      shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
    4.73 +                     |> filter is_type_finitizable
    4.74 +    val _ =
    4.75 +      if verbose andalso not (null finitizable_dataTs) then
    4.76 +        print_v (K (monotonicity_message finitizable_dataTs
    4.77 +                        "Nitpick can use a more precise finite encoding."))
    4.78 +      else
    4.79 +        ()
    4.80      (* This detection code is an ugly hack. Fortunately, it is used only to
    4.81         provide a hint to the user. *)
    4.82      (* string * (Rule_Cases.T * bool) -> bool *)
    4.83 @@ -446,7 +459,7 @@
    4.84                                         string_of_int j0))
    4.85                           (Typtab.dest ofs)
    4.86  *)
    4.87 -        val all_exact = forall (is_exact_type datatypes) all_Ts
    4.88 +        val all_exact = forall (is_exact_type datatypes true) all_Ts
    4.89          (* nut list -> rep NameTable.table -> nut list * rep NameTable.table *)
    4.90          val repify_consts = choose_reps_for_consts scope all_exact
    4.91          val main_j0 = offset_of_type ofs bool_T
    4.92 @@ -907,6 +920,7 @@
    4.93      val (skipped, the_scopes) =
    4.94        all_scopes hol_ctxt binarize sym_break cards_assigns maxes_assigns
    4.95                   iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
    4.96 +                 finitizable_dataTs
    4.97      val _ = if skipped > 0 then
    4.98                print_m (fn () => "Too many scopes. Skipping " ^
    4.99                                  string_of_int skipped ^ " scope" ^
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Feb 25 10:08:44 2010 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Feb 25 16:33:39 2010 +0100
     5.3 @@ -151,7 +151,7 @@
     5.4    val card_of_type : (typ * int) list -> typ -> int
     5.5    val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
     5.6    val bounded_exact_card_of_type :
     5.7 -    hol_context -> int -> int -> (typ * int) list -> typ -> int
     5.8 +    hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int
     5.9    val is_finite_type : hol_context -> typ -> bool
    5.10    val special_bounds : term list -> (indexname * typ) list
    5.11    val is_funky_typedef : theory -> typ -> bool
    5.12 @@ -1047,13 +1047,16 @@
    5.13                      card_of_type assigns T
    5.14                      handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
    5.15                             default_card)
    5.16 -(* hol_context -> int -> (typ * int) list -> typ -> int *)
    5.17 -fun bounded_exact_card_of_type hol_ctxt max default_card assigns T =
    5.18 +(* hol_context -> typ list -> int -> (typ * int) list -> typ -> int *)
    5.19 +fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card
    5.20 +                               assigns T =
    5.21    let
    5.22      (* typ list -> typ -> int *)
    5.23      fun aux avoid T =
    5.24        (if member (op =) avoid T then
    5.25           0
    5.26 +       else if member (op =) finitizable_dataTs T then
    5.27 +         raise SAME ()
    5.28         else case T of
    5.29           Type ("fun", [T1, T2]) =>
    5.30           let
    5.31 @@ -1097,7 +1100,7 @@
    5.32  
    5.33  (* hol_context -> typ -> bool *)
    5.34  fun is_finite_type hol_ctxt T =
    5.35 -  bounded_exact_card_of_type hol_ctxt 1 2 [] T <> 0
    5.36 +  bounded_exact_card_of_type hol_ctxt [] 1 2 [] T <> 0
    5.37  
    5.38  (* term -> bool *)
    5.39  fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Feb 25 10:08:44 2010 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Feb 25 16:33:39 2010 +0100
     6.3 @@ -255,10 +255,10 @@
     6.4       ("int_divide", tabulate_int_op2 debug univ_card (int_card, j0) isa_div)
     6.5     else if x = nat_less_rel then
     6.6       ("nat_less", tabulate_nat_op2 debug univ_card (nat_card, j0)
     6.7 -                                   (int_for_bool o op <))
     6.8 +                                   (int_from_bool o op <))
     6.9     else if x = int_less_rel then
    6.10       ("int_less", tabulate_int_op2 debug univ_card (int_card, j0)
    6.11 -                                   (int_for_bool o op <))
    6.12 +                                   (int_from_bool o op <))
    6.13     else if x = gcd_rel then
    6.14       ("gcd", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_gcd)
    6.15     else if x = lcm_rel then
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Feb 25 10:08:44 2010 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Feb 25 16:33:39 2010 +0100
     7.3 @@ -288,7 +288,7 @@
     7.4                                    T1 --> (T1 --> T2) --> T1 --> T2)
     7.5          (* (term * term) list -> term *)
     7.6          fun aux [] =
     7.7 -            if maybe_opt andalso not (is_complete_type datatypes T1) then
     7.8 +            if maybe_opt andalso not (is_complete_type datatypes false T1) then
     7.9                insert_const $ Const (unrep, T1) $ empty_const
    7.10              else
    7.11                empty_const
    7.12 @@ -312,7 +312,7 @@
    7.13                 Const (@{const_name None}, _) => aux' ps
    7.14               | _ => update_const $ aux' ps $ t1 $ t2)
    7.15          fun aux ps =
    7.16 -          if not (is_complete_type datatypes T1) then
    7.17 +          if not (is_complete_type datatypes false T1) then
    7.18              update_const $ aux' ps $ Const (unrep, T1)
    7.19              $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2'))
    7.20            else
    7.21 @@ -537,7 +537,7 @@
    7.22            val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1
    7.23            val ts2 =
    7.24              map (fn js => term_for_rep seen T2 T2 (Atom (2, 0))
    7.25 -                                       [[int_for_bool (member (op =) jss js)]])
    7.26 +                                       [[int_from_bool (member (op =) jss js)]])
    7.27                  jss1
    7.28          in make_fun false T1 T2 T' ts1 ts2 end
    7.29        | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, R2)) jss =
    7.30 @@ -707,12 +707,13 @@
    7.31             Pretty.str "=",
    7.32             Pretty.enum "," "{" "}"
    7.33                 (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
    7.34 -                (if complete then [] else [Pretty.str unrep]))])
    7.35 +                (if fun_from_pair complete false then []
    7.36 +                 else [Pretty.str unrep]))])
    7.37      (* typ -> dtype_spec list *)
    7.38      fun integer_datatype T =
    7.39        [{typ = T, card = card_of_type card_assigns T, co = false,
    7.40 -        standard = true, complete = false, concrete = true, deep = true,
    7.41 -        constrs = []}]
    7.42 +        standard = true, complete = (false, false), concrete = (true, true),
    7.43 +        deep = true, constrs = []}]
    7.44        handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
    7.45      val (codatatypes, datatypes) =
    7.46        datatypes |> filter #deep |> List.partition #co
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Feb 25 10:08:44 2010 +0100
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Feb 25 16:33:39 2010 +0100
     8.3 @@ -26,22 +26,27 @@
     8.4  
     8.5  type literal = var * sign
     8.6  
     8.7 -datatype ctype =
     8.8 -  CAlpha |
     8.9 -  CFun of ctype * sign_atom * ctype |
    8.10 -  CPair of ctype * ctype |
    8.11 -  CType of string * ctype list |
    8.12 -  CRec of string * typ list
    8.13 +datatype mtyp =
    8.14 +  MAlpha |
    8.15 +  MFun of mtyp * sign_atom * mtyp |
    8.16 +  MPair of mtyp * mtyp |
    8.17 +  MType of string * mtyp list |
    8.18 +  MRec of string * typ list
    8.19  
    8.20 -type cdata =
    8.21 +datatype mterm =
    8.22 +  MAtom of term * mtyp |
    8.23 +  MAbs of string * typ * mtyp * sign_atom * mterm |
    8.24 +  MApp of mterm * mterm
    8.25 +
    8.26 +type mdata =
    8.27    {hol_ctxt: hol_context,
    8.28     binarize: bool,
    8.29     alpha_T: typ,
    8.30     max_fresh: int Unsynchronized.ref,
    8.31 -   datatype_cache: ((string * typ list) * ctype) list Unsynchronized.ref,
    8.32 -   constr_cache: (styp * ctype) list Unsynchronized.ref}
    8.33 +   datatype_cache: ((string * typ list) * mtyp) list Unsynchronized.ref,
    8.34 +   constr_cache: (styp * mtyp) list Unsynchronized.ref}
    8.35  
    8.36 -exception CTYPE of string * ctype list
    8.37 +exception MTYPE of string * mtyp list
    8.38  
    8.39  (* string -> unit *)
    8.40  fun print_g (_ : string) = ()
    8.41 @@ -70,55 +75,92 @@
    8.42  (* literal -> string *)
    8.43  fun string_for_literal (x, sn) = string_for_var x ^ " = " ^ string_for_sign sn
    8.44  
    8.45 -val bool_C = CType (@{type_name bool}, [])
    8.46 +val bool_M = MType (@{type_name bool}, [])
    8.47 +val irrelevant_M = MType (nitpick_prefix ^ "irrelevant", [])
    8.48  
    8.49 -(* ctype -> bool *)
    8.50 -fun is_CRec (CRec _) = true
    8.51 -  | is_CRec _ = false
    8.52 +(* mtyp -> bool *)
    8.53 +fun is_MRec (MRec _) = true
    8.54 +  | is_MRec _ = false
    8.55 +(* mtyp -> mtyp * sign_atom * mtyp *)
    8.56 +fun dest_MFun (MFun z) = z
    8.57 +  | dest_MFun M = raise MTYPE ("Nitpick_Mono.dest_MFun", [M])
    8.58  
    8.59  val no_prec = 100
    8.60 -val prec_CFun = 1
    8.61 -val prec_CPair = 2
    8.62  
    8.63 -(* tuple_set -> int *)
    8.64 -fun precedence_of_ctype (CFun _) = prec_CFun
    8.65 -  | precedence_of_ctype (CPair _) = prec_CPair
    8.66 -  | precedence_of_ctype _ = no_prec
    8.67 +(* mtyp -> int *)
    8.68 +fun precedence_of_mtype (MFun _) = 1
    8.69 +  | precedence_of_mtype (MPair _) = 2
    8.70 +  | precedence_of_mtype _ = no_prec
    8.71  
    8.72 -(* ctype -> string *)
    8.73 -val string_for_ctype =
    8.74 +(* mtyp -> string *)
    8.75 +val string_for_mtype =
    8.76    let
    8.77 -    (* int -> ctype -> string *)
    8.78 -    fun aux outer_prec C =
    8.79 +    (* int -> mtyp -> string *)
    8.80 +    fun aux outer_prec M =
    8.81        let
    8.82 -        val prec = precedence_of_ctype C
    8.83 +        val prec = precedence_of_mtype M
    8.84          val need_parens = (prec < outer_prec)
    8.85        in
    8.86          (if need_parens then "(" else "") ^
    8.87 -        (case C of
    8.88 -           CAlpha => "\<alpha>"
    8.89 -         | CFun (C1, a, C2) =>
    8.90 -           aux (prec + 1) C1 ^ " \<Rightarrow>\<^bsup>" ^
    8.91 -           string_for_sign_atom a ^ "\<^esup> " ^ aux prec C2
    8.92 -         | CPair (C1, C2) => aux (prec + 1) C1 ^ " \<times> " ^ aux prec C2
    8.93 -         | CType (s, []) =>
    8.94 +        (case M of
    8.95 +           MAlpha => "\<alpha>"
    8.96 +         | MFun (M1, a, M2) =>
    8.97 +           aux (prec + 1) M1 ^ " \<Rightarrow>\<^bsup>" ^
    8.98 +           string_for_sign_atom a ^ "\<^esup> " ^ aux prec M2
    8.99 +         | MPair (M1, M2) => aux (prec + 1) M1 ^ " \<times> " ^ aux prec M2
   8.100 +         | MType (s, []) =>
   8.101             if s = @{type_name prop} orelse s = @{type_name bool} then "o" else s
   8.102 -         | CType (s, Cs) => "(" ^ commas (map (aux 0) Cs) ^ ") " ^ s
   8.103 -         | CRec (s, _) => "[" ^ s ^ "]") ^
   8.104 +         | MType (s, Ms) => "(" ^ commas (map (aux 0) Ms) ^ ") " ^ s
   8.105 +         | MRec (s, _) => "[" ^ s ^ "]") ^
   8.106          (if need_parens then ")" else "")
   8.107        end
   8.108    in aux 0 end
   8.109  
   8.110 -(* ctype -> ctype list *)
   8.111 -fun flatten_ctype (CPair (C1, C2)) = maps flatten_ctype [C1, C2]
   8.112 -  | flatten_ctype (CType (_, Cs)) = maps flatten_ctype Cs
   8.113 -  | flatten_ctype C = [C]
   8.114 +(* mtyp -> mtyp list *)
   8.115 +fun flatten_mtype (MPair (M1, M2)) = maps flatten_mtype [M1, M2]
   8.116 +  | flatten_mtype (MType (_, Ms)) = maps flatten_mtype Ms
   8.117 +  | flatten_mtype M = [M]
   8.118 +
   8.119 +(* mterm -> bool *)
   8.120 +fun precedence_of_mterm (MAtom _) = no_prec
   8.121 +  | precedence_of_mterm (MAbs _) = 1
   8.122 +  | precedence_of_mterm (MApp _) = 2
   8.123  
   8.124 -(* hol_context -> bool -> typ -> cdata *)
   8.125 -fun initial_cdata hol_ctxt binarize alpha_T =
   8.126 +(* Proof.context -> mterm -> string *)
   8.127 +fun string_for_mterm ctxt =
   8.128 +  let
   8.129 +    (* mtype -> string *)
   8.130 +    fun mtype_annotation M = "\<^bsup>" ^ string_for_mtype M ^ "\<^esup>"
   8.131 +    (* int -> mterm -> string *)
   8.132 +    fun aux outer_prec m =
   8.133 +      let
   8.134 +        val prec = precedence_of_mterm m
   8.135 +        val need_parens = (prec < outer_prec)
   8.136 +      in
   8.137 +        (if need_parens then "(" else "") ^
   8.138 +        (case m of
   8.139 +           MAtom (t, M) => Syntax.string_of_term ctxt t ^ mtype_annotation M
   8.140 +         | MAbs (s, _, M, a, m) =>
   8.141 +           "\<lambda>" ^ s ^ mtype_annotation M ^ ".\<^bsup>" ^
   8.142 +           string_for_sign_atom a ^ "\<^esup> " ^ aux prec m
   8.143 +         | MApp (m1, m2) => aux prec m1 ^ " " ^ aux (prec + 1) m2) ^
   8.144 +        (if need_parens then ")" else "")
   8.145 +      end
   8.146 +  in aux 0 end
   8.147 +
   8.148 +(* mterm -> mtyp *)
   8.149 +fun mtype_of_mterm (MAtom (_, M)) = M
   8.150 +  | mtype_of_mterm (MAbs (_, _, M, a, m)) = MFun (M, a, mtype_of_mterm m)
   8.151 +  | mtype_of_mterm (MApp (m1, _)) =
   8.152 +    case mtype_of_mterm m1 of
   8.153 +      MFun (_, _, M12) => M12
   8.154 +    | M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1])
   8.155 +
   8.156 +(* hol_context -> bool -> typ -> mdata *)
   8.157 +fun initial_mdata hol_ctxt binarize alpha_T =
   8.158    ({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T,
   8.159      max_fresh = Unsynchronized.ref 0, datatype_cache = Unsynchronized.ref [],
   8.160 -    constr_cache = Unsynchronized.ref []} : cdata)
   8.161 +    constr_cache = Unsynchronized.ref []} : mdata)
   8.162  
   8.163  (* typ -> typ -> bool *)
   8.164  fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) =
   8.165 @@ -126,177 +168,179 @@
   8.166                          exists (could_exist_alpha_subtype alpha_T) Ts)
   8.167    | could_exist_alpha_subtype alpha_T T = (T = alpha_T)
   8.168  (* theory -> typ -> typ -> bool *)
   8.169 -fun could_exist_alpha_sub_ctype _ (alpha_T as TFree _) T =
   8.170 +fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T =
   8.171      could_exist_alpha_subtype alpha_T T
   8.172 -  | could_exist_alpha_sub_ctype thy alpha_T T =
   8.173 +  | could_exist_alpha_sub_mtype thy alpha_T T =
   8.174      (T = alpha_T orelse is_datatype thy [(NONE, true)] T)
   8.175  
   8.176 -(* ctype -> bool *)
   8.177 -fun exists_alpha_sub_ctype CAlpha = true
   8.178 -  | exists_alpha_sub_ctype (CFun (C1, _, C2)) =
   8.179 -    exists exists_alpha_sub_ctype [C1, C2]
   8.180 -  | exists_alpha_sub_ctype (CPair (C1, C2)) =
   8.181 -    exists exists_alpha_sub_ctype [C1, C2]
   8.182 -  | exists_alpha_sub_ctype (CType (_, Cs)) = exists exists_alpha_sub_ctype Cs
   8.183 -  | exists_alpha_sub_ctype (CRec _) = true
   8.184 +(* mtyp -> bool *)
   8.185 +fun exists_alpha_sub_mtype MAlpha = true
   8.186 +  | exists_alpha_sub_mtype (MFun (M1, _, M2)) =
   8.187 +    exists exists_alpha_sub_mtype [M1, M2]
   8.188 +  | exists_alpha_sub_mtype (MPair (M1, M2)) =
   8.189 +    exists exists_alpha_sub_mtype [M1, M2]
   8.190 +  | exists_alpha_sub_mtype (MType (_, Ms)) = exists exists_alpha_sub_mtype Ms
   8.191 +  | exists_alpha_sub_mtype (MRec _) = true
   8.192  
   8.193 -(* ctype -> bool *)
   8.194 -fun exists_alpha_sub_ctype_fresh CAlpha = true
   8.195 -  | exists_alpha_sub_ctype_fresh (CFun (_, V _, _)) = true
   8.196 -  | exists_alpha_sub_ctype_fresh (CFun (_, _, C2)) =
   8.197 -    exists_alpha_sub_ctype_fresh C2
   8.198 -  | exists_alpha_sub_ctype_fresh (CPair (C1, C2)) =
   8.199 -    exists exists_alpha_sub_ctype_fresh [C1, C2]
   8.200 -  | exists_alpha_sub_ctype_fresh (CType (_, Cs)) =
   8.201 -    exists exists_alpha_sub_ctype_fresh Cs
   8.202 -  | exists_alpha_sub_ctype_fresh (CRec _) = true
   8.203 +(* mtyp -> bool *)
   8.204 +fun exists_alpha_sub_mtype_fresh MAlpha = true
   8.205 +  | exists_alpha_sub_mtype_fresh (MFun (_, V _, _)) = true
   8.206 +  | exists_alpha_sub_mtype_fresh (MFun (_, _, M2)) =
   8.207 +    exists_alpha_sub_mtype_fresh M2
   8.208 +  | exists_alpha_sub_mtype_fresh (MPair (M1, M2)) =
   8.209 +    exists exists_alpha_sub_mtype_fresh [M1, M2]
   8.210 +  | exists_alpha_sub_mtype_fresh (MType (_, Ms)) =
   8.211 +    exists exists_alpha_sub_mtype_fresh Ms
   8.212 +  | exists_alpha_sub_mtype_fresh (MRec _) = true
   8.213  
   8.214 -(* string * typ list -> ctype list -> ctype *)
   8.215 -fun constr_ctype_for_binders z Cs =
   8.216 -  fold_rev (fn C => curry3 CFun C (S Minus)) Cs (CRec z)
   8.217 +(* string * typ list -> mtyp list -> mtyp *)
   8.218 +fun constr_mtype_for_binders z Ms =
   8.219 +  fold_rev (fn M => curry3 MFun M (S Minus)) Ms (MRec z)
   8.220  
   8.221 -(* ((string * typ list) * ctype) list -> ctype list -> ctype -> ctype *)
   8.222 -fun repair_ctype _ _ CAlpha = CAlpha
   8.223 -  | repair_ctype cache seen (CFun (C1, a, C2)) =
   8.224 -    CFun (repair_ctype cache seen C1, a, repair_ctype cache seen C2)
   8.225 -  | repair_ctype cache seen (CPair Cp) =
   8.226 -    CPair (pairself (repair_ctype cache seen) Cp)
   8.227 -  | repair_ctype cache seen (CType (s, Cs)) =
   8.228 -    CType (s, maps (flatten_ctype o repair_ctype cache seen) Cs)
   8.229 -  | repair_ctype cache seen (CRec (z as (s, _))) =
   8.230 +(* ((string * typ list) * mtyp) list -> mtyp list -> mtyp -> mtyp *)
   8.231 +fun repair_mtype _ _ MAlpha = MAlpha
   8.232 +  | repair_mtype cache seen (MFun (M1, a, M2)) =
   8.233 +    MFun (repair_mtype cache seen M1, a, repair_mtype cache seen M2)
   8.234 +  | repair_mtype cache seen (MPair Mp) =
   8.235 +    MPair (pairself (repair_mtype cache seen) Mp)
   8.236 +  | repair_mtype cache seen (MType (s, Ms)) =
   8.237 +    MType (s, maps (flatten_mtype o repair_mtype cache seen) Ms)
   8.238 +  | repair_mtype cache seen (MRec (z as (s, _))) =
   8.239      case AList.lookup (op =) cache z |> the of
   8.240 -      CRec _ => CType (s, [])
   8.241 -    | C => if member (op =) seen C then CType (s, [])
   8.242 -           else repair_ctype cache (C :: seen) C
   8.243 +      MRec _ => MType (s, [])
   8.244 +    | M => if member (op =) seen M then MType (s, [])
   8.245 +           else repair_mtype cache (M :: seen) M
   8.246  
   8.247 -(* ((string * typ list) * ctype) list Unsynchronized.ref -> unit *)
   8.248 +(* ((string * typ list) * mtyp) list Unsynchronized.ref -> unit *)
   8.249  fun repair_datatype_cache cache =
   8.250    let
   8.251 -    (* (string * typ list) * ctype -> unit *)
   8.252 -    fun repair_one (z, C) =
   8.253 +    (* (string * typ list) * mtyp -> unit *)
   8.254 +    fun repair_one (z, M) =
   8.255        Unsynchronized.change cache
   8.256 -          (AList.update (op =) (z, repair_ctype (!cache) [] C))
   8.257 +          (AList.update (op =) (z, repair_mtype (!cache) [] M))
   8.258    in List.app repair_one (rev (!cache)) end
   8.259  
   8.260 -(* (typ * ctype) list -> (styp * ctype) list Unsynchronized.ref -> unit *)
   8.261 +(* (typ * mtyp) list -> (styp * mtyp) list Unsynchronized.ref -> unit *)
   8.262  fun repair_constr_cache dtype_cache constr_cache =
   8.263    let
   8.264 -    (* styp * ctype -> unit *)
   8.265 -    fun repair_one (x, C) =
   8.266 +    (* styp * mtyp -> unit *)
   8.267 +    fun repair_one (x, M) =
   8.268        Unsynchronized.change constr_cache
   8.269 -          (AList.update (op =) (x, repair_ctype dtype_cache [] C))
   8.270 +          (AList.update (op =) (x, repair_mtype dtype_cache [] M))
   8.271    in List.app repair_one (!constr_cache) end
   8.272  
   8.273 -(* cdata -> typ -> ctype *)
   8.274 -fun fresh_ctype_for_type ({hol_ctxt as {thy, ...}, binarize, alpha_T, max_fresh,
   8.275 -                           datatype_cache, constr_cache, ...} : cdata) =
   8.276 +(* mdata -> typ -> typ -> mtyp * sign_atom * mtyp *)
   8.277 +fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) T1 T2 =
   8.278    let
   8.279 -    (* typ -> typ -> ctype *)
   8.280 -    fun do_fun T1 T2 =
   8.281 -      let
   8.282 -        val C1 = do_type T1
   8.283 -        val C2 = do_type T2
   8.284 -        val a = if is_boolean_type (body_type T2) andalso
   8.285 -                   exists_alpha_sub_ctype_fresh C1 then
   8.286 -                  V (Unsynchronized.inc max_fresh)
   8.287 -                else
   8.288 -                  S Minus
   8.289 -      in CFun (C1, a, C2) end
   8.290 -    (* typ -> ctype *)
   8.291 -    and do_type T =
   8.292 +    val M1 = fresh_mtype_for_type mdata T1
   8.293 +    val M2 = fresh_mtype_for_type mdata T2
   8.294 +    val a = if is_boolean_type (body_type T2) andalso
   8.295 +               exists_alpha_sub_mtype_fresh M1 then
   8.296 +              V (Unsynchronized.inc max_fresh)
   8.297 +            else
   8.298 +              S Minus
   8.299 +  in (M1, a, M2) end
   8.300 +(* mdata -> typ -> mtyp *)
   8.301 +and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T,
   8.302 +                                    datatype_cache, constr_cache, ...}) =
   8.303 +  let
   8.304 +    (* typ -> typ -> mtyp *)
   8.305 +    val do_fun = MFun oo fresh_mfun_for_fun_type mdata
   8.306 +    (* typ -> mtyp *)
   8.307 +    fun do_type T =
   8.308        if T = alpha_T then
   8.309 -        CAlpha
   8.310 +        MAlpha
   8.311        else case T of
   8.312          Type ("fun", [T1, T2]) => do_fun T1 T2
   8.313        | Type (@{type_name fun_box}, [T1, T2]) => do_fun T1 T2
   8.314 -      | Type ("*", [T1, T2]) => CPair (pairself do_type (T1, T2))
   8.315 +      | Type ("*", [T1, T2]) => MPair (pairself do_type (T1, T2))
   8.316        | Type (z as (s, _)) =>
   8.317 -        if could_exist_alpha_sub_ctype thy alpha_T T then
   8.318 +        if could_exist_alpha_sub_mtype thy alpha_T T then
   8.319            case AList.lookup (op =) (!datatype_cache) z of
   8.320 -            SOME C => C
   8.321 +            SOME M => M
   8.322            | NONE =>
   8.323              let
   8.324 -              val _ = Unsynchronized.change datatype_cache (cons (z, CRec z))
   8.325 +              val _ = Unsynchronized.change datatype_cache (cons (z, MRec z))
   8.326                val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
   8.327 -              val (all_Cs, constr_Cs) =
   8.328 -                fold_rev (fn (_, T') => fn (all_Cs, constr_Cs) =>
   8.329 +              val (all_Ms, constr_Ms) =
   8.330 +                fold_rev (fn (_, T') => fn (all_Ms, constr_Ms) =>
   8.331                               let
   8.332 -                               val binder_Cs = map do_type (binder_types T')
   8.333 -                               val new_Cs = filter exists_alpha_sub_ctype_fresh
   8.334 -                                                   binder_Cs
   8.335 -                               val constr_C = constr_ctype_for_binders z
   8.336 -                                                                       binder_Cs
   8.337 +                               val binder_Ms = map do_type (binder_types T')
   8.338 +                               val new_Ms = filter exists_alpha_sub_mtype_fresh
   8.339 +                                                   binder_Ms
   8.340 +                               val constr_M = constr_mtype_for_binders z
   8.341 +                                                                       binder_Ms
   8.342                               in
   8.343 -                               (union (op =) new_Cs all_Cs,
   8.344 -                                constr_C :: constr_Cs)
   8.345 +                               (union (op =) new_Ms all_Ms,
   8.346 +                                constr_M :: constr_Ms)
   8.347                               end)
   8.348                           xs ([], [])
   8.349 -              val C = CType (s, all_Cs)
   8.350 +              val M = MType (s, all_Ms)
   8.351                val _ = Unsynchronized.change datatype_cache
   8.352 -                          (AList.update (op =) (z, C))
   8.353 +                          (AList.update (op =) (z, M))
   8.354                val _ = Unsynchronized.change constr_cache
   8.355 -                          (append (xs ~~ constr_Cs))
   8.356 +                          (append (xs ~~ constr_Ms))
   8.357              in
   8.358 -              if forall (not o is_CRec o snd) (!datatype_cache) then
   8.359 +              if forall (not o is_MRec o snd) (!datatype_cache) then
   8.360                  (repair_datatype_cache datatype_cache;
   8.361                   repair_constr_cache (!datatype_cache) constr_cache;
   8.362                   AList.lookup (op =) (!datatype_cache) z |> the)
   8.363                else
   8.364 -                C
   8.365 +                M
   8.366              end
   8.367          else
   8.368 -          CType (s, [])
   8.369 -      | _ => CType (Refute.string_of_typ T, [])
   8.370 +          MType (s, [])
   8.371 +      | _ => MType (Refute.string_of_typ T, [])
   8.372    in do_type end
   8.373  
   8.374 -(* ctype -> ctype list *)
   8.375 -fun prodC_factors (CPair (C1, C2)) = maps prodC_factors [C1, C2]
   8.376 -  | prodC_factors C = [C]
   8.377 -(* ctype -> ctype list * ctype *)
   8.378 -fun curried_strip_ctype (CFun (C1, S Minus, C2)) =
   8.379 -    curried_strip_ctype C2 |>> append (prodC_factors C1)
   8.380 -  | curried_strip_ctype C = ([], C)
   8.381 -(* string -> ctype -> ctype *)
   8.382 -fun sel_ctype_from_constr_ctype s C =
   8.383 -  let val (arg_Cs, dataC) = curried_strip_ctype C in
   8.384 -    CFun (dataC, S Minus,
   8.385 -          case sel_no_from_name s of ~1 => bool_C | n => nth arg_Cs n)
   8.386 +(* mtyp -> mtyp list *)
   8.387 +fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2]
   8.388 +  | prodM_factors M = [M]
   8.389 +(* mtyp -> mtyp list * mtyp *)
   8.390 +fun curried_strip_mtype (MFun (M1, S Minus, M2)) =
   8.391 +    curried_strip_mtype M2 |>> append (prodM_factors M1)
   8.392 +  | curried_strip_mtype M = ([], M)
   8.393 +(* string -> mtyp -> mtyp *)
   8.394 +fun sel_mtype_from_constr_mtype s M =
   8.395 +  let val (arg_Ms, dataM) = curried_strip_mtype M in
   8.396 +    MFun (dataM, S Minus,
   8.397 +          case sel_no_from_name s of ~1 => bool_M | n => nth arg_Ms n)
   8.398    end
   8.399  
   8.400 -(* cdata -> styp -> ctype *)
   8.401 -fun ctype_for_constr (cdata as {hol_ctxt = {thy, ...}, alpha_T, constr_cache,
   8.402 +(* mdata -> styp -> mtyp *)
   8.403 +fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_cache,
   8.404                                  ...}) (x as (_, T)) =
   8.405 -  if could_exist_alpha_sub_ctype thy alpha_T T then
   8.406 +  if could_exist_alpha_sub_mtype thy alpha_T T then
   8.407      case AList.lookup (op =) (!constr_cache) x of
   8.408 -      SOME C => C
   8.409 +      SOME M => M
   8.410      | NONE => if T = alpha_T then
   8.411 -                let val C = fresh_ctype_for_type cdata T in
   8.412 -                  (Unsynchronized.change constr_cache (cons (x, C)); C)
   8.413 +                let val M = fresh_mtype_for_type mdata T in
   8.414 +                  (Unsynchronized.change constr_cache (cons (x, M)); M)
   8.415                  end
   8.416                else
   8.417 -                (fresh_ctype_for_type cdata (body_type T);
   8.418 +                (fresh_mtype_for_type mdata (body_type T);
   8.419                   AList.lookup (op =) (!constr_cache) x |> the)
   8.420    else
   8.421 -    fresh_ctype_for_type cdata T
   8.422 -fun ctype_for_sel (cdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
   8.423 +    fresh_mtype_for_type mdata T
   8.424 +fun mtype_for_sel (mdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
   8.425    x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
   8.426 -    |> ctype_for_constr cdata |> sel_ctype_from_constr_ctype s
   8.427 +    |> mtype_for_constr mdata |> sel_mtype_from_constr_mtype s
   8.428  
   8.429 -(* literal list -> ctype -> ctype *)
   8.430 -fun instantiate_ctype lits =
   8.431 +(* literal list -> mtyp -> mtyp *)
   8.432 +fun instantiate_mtype lits =
   8.433    let
   8.434 -    (* ctype -> ctype *)
   8.435 -    fun aux CAlpha = CAlpha
   8.436 -      | aux (CFun (C1, V x, C2)) =
   8.437 +    (* mtyp -> mtyp *)
   8.438 +    fun aux MAlpha = MAlpha
   8.439 +      | aux (MFun (M1, V x, M2)) =
   8.440          let
   8.441            val a = case AList.lookup (op =) lits x of
   8.442                      SOME sn => S sn
   8.443                    | NONE => V x
   8.444 -        in CFun (aux C1, a, aux C2) end
   8.445 -      | aux (CFun (C1, a, C2)) = CFun (aux C1, a, aux C2)
   8.446 -      | aux (CPair Cp) = CPair (pairself aux Cp)
   8.447 -      | aux (CType (s, Cs)) = CType (s, map aux Cs)
   8.448 -      | aux (CRec z) = CRec z
   8.449 +        in MFun (aux M1, a, aux M2) end
   8.450 +      | aux (MFun (M1, a, M2)) = MFun (aux M1, a, aux M2)
   8.451 +      | aux (MPair Mp) = MPair (pairself aux Mp)
   8.452 +      | aux (MType (s, Ms)) = MType (s, map aux Ms)
   8.453 +      | aux (MRec z) = MRec z
   8.454    in aux end
   8.455  
   8.456  datatype comp_op = Eq | Leq
   8.457 @@ -346,98 +390,98 @@
   8.458    | do_sign_atom_comp cmp xs a1 a2 (lits, comps) =
   8.459      SOME (lits, insert (op =) (a1, a2, cmp, xs) comps)
   8.460  
   8.461 -(* comp -> var list -> ctype -> ctype -> (literal list * comp list) option
   8.462 +(* comp -> var list -> mtyp -> mtyp -> (literal list * comp list) option
   8.463     -> (literal list * comp list) option *)
   8.464 -fun do_ctype_comp _ _ _ _ NONE = NONE
   8.465 -  | do_ctype_comp _ _ CAlpha CAlpha accum = accum
   8.466 -  | do_ctype_comp Eq xs (CFun (C11, a1, C12)) (CFun (C21, a2, C22))
   8.467 +fun do_mtype_comp _ _ _ _ NONE = NONE
   8.468 +  | do_mtype_comp _ _ MAlpha MAlpha accum = accum
   8.469 +  | do_mtype_comp Eq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22))
   8.470                    (SOME accum) =
   8.471 -     accum |> do_sign_atom_comp Eq xs a1 a2 |> do_ctype_comp Eq xs C11 C21
   8.472 -           |> do_ctype_comp Eq xs C12 C22
   8.473 -  | do_ctype_comp Leq xs (CFun (C11, a1, C12)) (CFun (C21, a2, C22))
   8.474 +     accum |> do_sign_atom_comp Eq xs a1 a2 |> do_mtype_comp Eq xs M11 M21
   8.475 +           |> do_mtype_comp Eq xs M12 M22
   8.476 +  | do_mtype_comp Leq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22))
   8.477                    (SOME accum) =
   8.478 -    (if exists_alpha_sub_ctype C11 then
   8.479 +    (if exists_alpha_sub_mtype M11 then
   8.480         accum |> do_sign_atom_comp Leq xs a1 a2
   8.481 -             |> do_ctype_comp Leq xs C21 C11
   8.482 +             |> do_mtype_comp Leq xs M21 M11
   8.483               |> (case a2 of
   8.484                     S Minus => I
   8.485 -                 | S Plus => do_ctype_comp Leq xs C11 C21
   8.486 -                 | V x => do_ctype_comp Leq (x :: xs) C11 C21)
   8.487 +                 | S Plus => do_mtype_comp Leq xs M11 M21
   8.488 +                 | V x => do_mtype_comp Leq (x :: xs) M11 M21)
   8.489       else
   8.490         SOME accum)
   8.491 -    |> do_ctype_comp Leq xs C12 C22
   8.492 -  | do_ctype_comp cmp xs (C1 as CPair (C11, C12)) (C2 as CPair (C21, C22))
   8.493 +    |> do_mtype_comp Leq xs M12 M22
   8.494 +  | do_mtype_comp cmp xs (M1 as MPair (M11, M12)) (M2 as MPair (M21, M22))
   8.495                    accum =
   8.496 -    (accum |> fold (uncurry (do_ctype_comp cmp xs)) [(C11, C21), (C12, C22)]
   8.497 +    (accum |> fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)]
   8.498       handle Library.UnequalLengths =>
   8.499 -            raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2]))
   8.500 -  | do_ctype_comp _ _ (CType _) (CType _) accum =
   8.501 +            raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2]))
   8.502 +  | do_mtype_comp _ _ (MType _) (MType _) accum =
   8.503      accum (* no need to compare them thanks to the cache *)
   8.504 -  | do_ctype_comp _ _ C1 C2 _ =
   8.505 -    raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2])
   8.506 +  | do_mtype_comp _ _ M1 M2 _ =
   8.507 +    raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2])
   8.508  
   8.509 -(* comp_op -> ctype -> ctype -> constraint_set -> constraint_set *)
   8.510 -fun add_ctype_comp _ _ _ UnsolvableCSet = UnsolvableCSet
   8.511 -  | add_ctype_comp cmp C1 C2 (CSet (lits, comps, sexps)) =
   8.512 -    (print_g ("*** Add " ^ string_for_ctype C1 ^ " " ^ string_for_comp_op cmp ^
   8.513 -              " " ^ string_for_ctype C2);
   8.514 -     case do_ctype_comp cmp [] C1 C2 (SOME (lits, comps)) of
   8.515 +(* comp_op -> mtyp -> mtyp -> constraint_set -> constraint_set *)
   8.516 +fun add_mtype_comp _ _ _ UnsolvableCSet = UnsolvableCSet
   8.517 +  | add_mtype_comp cmp M1 M2 (CSet (lits, comps, sexps)) =
   8.518 +    (print_g ("*** Add " ^ string_for_mtype M1 ^ " " ^ string_for_comp_op cmp ^
   8.519 +              " " ^ string_for_mtype M2);
   8.520 +     case do_mtype_comp cmp [] M1 M2 (SOME (lits, comps)) of
   8.521         NONE => (print_g "**** Unsolvable"; UnsolvableCSet)
   8.522       | SOME (lits, comps) => CSet (lits, comps, sexps))
   8.523  
   8.524 -(* ctype -> ctype -> constraint_set -> constraint_set *)
   8.525 -val add_ctypes_equal = add_ctype_comp Eq
   8.526 -val add_is_sub_ctype = add_ctype_comp Leq
   8.527 +(* mtyp -> mtyp -> constraint_set -> constraint_set *)
   8.528 +val add_mtypes_equal = add_mtype_comp Eq
   8.529 +val add_is_sub_mtype = add_mtype_comp Leq
   8.530  
   8.531 -(* sign -> sign_expr -> ctype -> (literal list * sign_expr list) option
   8.532 +(* sign -> sign_expr -> mtyp -> (literal list * sign_expr list) option
   8.533     -> (literal list * sign_expr list) option *)
   8.534 -fun do_notin_ctype_fv _ _ _ NONE = NONE
   8.535 -  | do_notin_ctype_fv Minus _ CAlpha accum = accum
   8.536 -  | do_notin_ctype_fv Plus [] CAlpha _ = NONE
   8.537 -  | do_notin_ctype_fv Plus [(x, sn)] CAlpha (SOME (lits, sexps)) =
   8.538 +fun do_notin_mtype_fv _ _ _ NONE = NONE
   8.539 +  | do_notin_mtype_fv Minus _ MAlpha accum = accum
   8.540 +  | do_notin_mtype_fv Plus [] MAlpha _ = NONE
   8.541 +  | do_notin_mtype_fv Plus [(x, sn)] MAlpha (SOME (lits, sexps)) =
   8.542      SOME lits |> do_literal (x, sn) |> Option.map (rpair sexps)
   8.543 -  | do_notin_ctype_fv Plus sexp CAlpha (SOME (lits, sexps)) =
   8.544 +  | do_notin_mtype_fv Plus sexp MAlpha (SOME (lits, sexps)) =
   8.545      SOME (lits, insert (op =) sexp sexps)
   8.546 -  | do_notin_ctype_fv sn sexp (CFun (C1, S sn', C2)) accum =
   8.547 +  | do_notin_mtype_fv sn sexp (MFun (M1, S sn', M2)) accum =
   8.548      accum |> (if sn' = Plus andalso sn = Plus then
   8.549 -                do_notin_ctype_fv Plus sexp C1
   8.550 +                do_notin_mtype_fv Plus sexp M1
   8.551                else
   8.552                  I)
   8.553            |> (if sn' = Minus orelse sn = Plus then
   8.554 -                do_notin_ctype_fv Minus sexp C1
   8.555 +                do_notin_mtype_fv Minus sexp M1
   8.556                else
   8.557                  I)
   8.558 -          |> do_notin_ctype_fv sn sexp C2
   8.559 -  | do_notin_ctype_fv Plus sexp (CFun (C1, V x, C2)) accum =
   8.560 +          |> do_notin_mtype_fv sn sexp M2
   8.561 +  | do_notin_mtype_fv Plus sexp (MFun (M1, V x, M2)) accum =
   8.562      accum |> (case do_literal (x, Minus) (SOME sexp) of
   8.563                  NONE => I
   8.564 -              | SOME sexp' => do_notin_ctype_fv Plus sexp' C1)
   8.565 -          |> do_notin_ctype_fv Minus sexp C1
   8.566 -          |> do_notin_ctype_fv Plus sexp C2
   8.567 -  | do_notin_ctype_fv Minus sexp (CFun (C1, V x, C2)) accum =
   8.568 +              | SOME sexp' => do_notin_mtype_fv Plus sexp' M1)
   8.569 +          |> do_notin_mtype_fv Minus sexp M1
   8.570 +          |> do_notin_mtype_fv Plus sexp M2
   8.571 +  | do_notin_mtype_fv Minus sexp (MFun (M1, V x, M2)) accum =
   8.572      accum |> (case do_literal (x, Plus) (SOME sexp) of
   8.573                  NONE => I
   8.574 -              | SOME sexp' => do_notin_ctype_fv Plus sexp' C1)
   8.575 -          |> do_notin_ctype_fv Minus sexp C2
   8.576 -  | do_notin_ctype_fv sn sexp (CPair (C1, C2)) accum =
   8.577 -    accum |> fold (do_notin_ctype_fv sn sexp) [C1, C2]
   8.578 -  | do_notin_ctype_fv sn sexp (CType (_, Cs)) accum =
   8.579 -    accum |> fold (do_notin_ctype_fv sn sexp) Cs
   8.580 -  | do_notin_ctype_fv _ _ C _ =
   8.581 -    raise CTYPE ("Nitpick_Mono.do_notin_ctype_fv", [C])
   8.582 +              | SOME sexp' => do_notin_mtype_fv Plus sexp' M1)
   8.583 +          |> do_notin_mtype_fv Minus sexp M2
   8.584 +  | do_notin_mtype_fv sn sexp (MPair (M1, M2)) accum =
   8.585 +    accum |> fold (do_notin_mtype_fv sn sexp) [M1, M2]
   8.586 +  | do_notin_mtype_fv sn sexp (MType (_, Ms)) accum =
   8.587 +    accum |> fold (do_notin_mtype_fv sn sexp) Ms
   8.588 +  | do_notin_mtype_fv _ _ M _ =
   8.589 +    raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M])
   8.590  
   8.591 -(* sign -> ctype -> constraint_set -> constraint_set *)
   8.592 -fun add_notin_ctype_fv _ _ UnsolvableCSet = UnsolvableCSet
   8.593 -  | add_notin_ctype_fv sn C (CSet (lits, comps, sexps)) =
   8.594 -    (print_g ("*** Add " ^ string_for_ctype C ^ " is right-" ^
   8.595 +(* sign -> mtyp -> constraint_set -> constraint_set *)
   8.596 +fun add_notin_mtype_fv _ _ UnsolvableCSet = UnsolvableCSet
   8.597 +  | add_notin_mtype_fv sn M (CSet (lits, comps, sexps)) =
   8.598 +    (print_g ("*** Add " ^ string_for_mtype M ^ " is right-" ^
   8.599                (case sn of Minus => "unique" | Plus => "total") ^ ".");
   8.600 -     case do_notin_ctype_fv sn [] C (SOME (lits, sexps)) of
   8.601 +     case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of
   8.602         NONE => (print_g "**** Unsolvable"; UnsolvableCSet)
   8.603       | SOME (lits, sexps) => CSet (lits, comps, sexps))
   8.604  
   8.605 -(* ctype -> constraint_set -> constraint_set *)
   8.606 -val add_ctype_is_right_unique = add_notin_ctype_fv Minus
   8.607 -val add_ctype_is_right_total = add_notin_ctype_fv Plus
   8.608 +(* mtyp -> constraint_set -> constraint_set *)
   8.609 +val add_mtype_is_right_unique = add_notin_mtype_fv Minus
   8.610 +val add_mtype_is_right_total = add_notin_mtype_fv Plus
   8.611  
   8.612  val bool_from_minus = true
   8.613  
   8.614 @@ -516,209 +560,228 @@
   8.615        | _ => NONE
   8.616      end
   8.617  
   8.618 -type ctype_schema = ctype * constraint_set
   8.619 -type ctype_context =
   8.620 -  {bounds: ctype list,
   8.621 -   frees: (styp * ctype) list,
   8.622 -   consts: (styp * ctype) list}
   8.623 +type mtype_schema = mtyp * constraint_set
   8.624 +type mtype_context =
   8.625 +  {bounds: mtyp list,
   8.626 +   frees: (styp * mtyp) list,
   8.627 +   consts: (styp * mtyp) list}
   8.628  
   8.629 -type accumulator = ctype_context * constraint_set
   8.630 +type accumulator = mtype_context * constraint_set
   8.631  
   8.632  val initial_gamma = {bounds = [], frees = [], consts = []}
   8.633  val unsolvable_accum = (initial_gamma, UnsolvableCSet)
   8.634  
   8.635 -(* ctype -> ctype_context -> ctype_context *)
   8.636 -fun push_bound C {bounds, frees, consts} =
   8.637 -  {bounds = C :: bounds, frees = frees, consts = consts}
   8.638 -(* ctype_context -> ctype_context *)
   8.639 +(* mtyp -> mtype_context -> mtype_context *)
   8.640 +fun push_bound M {bounds, frees, consts} =
   8.641 +  {bounds = M :: bounds, frees = frees, consts = consts}
   8.642 +(* mtype_context -> mtype_context *)
   8.643  fun pop_bound {bounds, frees, consts} =
   8.644    {bounds = tl bounds, frees = frees, consts = consts}
   8.645    handle List.Empty => initial_gamma
   8.646  
   8.647 -(* cdata -> term -> accumulator -> ctype * accumulator *)
   8.648 -fun consider_term (cdata as {hol_ctxt = {thy, ctxt, stds, fast_descrs,
   8.649 +(* mdata -> term -> accumulator -> mterm * accumulator *)
   8.650 +fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, fast_descrs,
   8.651                                           def_table, ...},
   8.652                               alpha_T, max_fresh, ...}) =
   8.653    let
   8.654 -    (* typ -> ctype *)
   8.655 -    val ctype_for = fresh_ctype_for_type cdata
   8.656 -    (* ctype -> ctype *)
   8.657 -    fun pos_set_ctype_for_dom C =
   8.658 -      CFun (C, S (if exists_alpha_sub_ctype C then Plus else Minus), bool_C)
   8.659 -    (* typ -> accumulator -> ctype * accumulator *)
   8.660 -    fun do_quantifier T (gamma, cset) =
   8.661 +    (* typ -> typ -> mtyp * sign_atom * mtyp *)
   8.662 +    val mfun_for = fresh_mfun_for_fun_type mdata
   8.663 +    (* typ -> mtyp *)
   8.664 +    val mtype_for = fresh_mtype_for_type mdata
   8.665 +    (* mtyp -> mtyp *)
   8.666 +    fun pos_set_mtype_for_dom M =
   8.667 +      MFun (M, S (if exists_alpha_sub_mtype M then Plus else Minus), bool_M)
   8.668 +    (* typ -> accumulator -> mterm * accumulator *)
   8.669 +    fun do_all T (gamma, cset) =
   8.670        let
   8.671 -        val abs_C = ctype_for (domain_type (domain_type T))
   8.672 -        val body_C = ctype_for (range_type T)
   8.673 +        val abs_M = mtype_for (domain_type (domain_type T))
   8.674 +        val body_M = mtype_for (range_type T)
   8.675        in
   8.676 -        (CFun (CFun (abs_C, S Minus, body_C), S Minus, body_C),
   8.677 -         (gamma, cset |> add_ctype_is_right_total abs_C))
   8.678 +        (MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M),
   8.679 +         (gamma, cset |> add_mtype_is_right_total abs_M))
   8.680        end
   8.681      fun do_equals T (gamma, cset) =
   8.682 -      let val C = ctype_for (domain_type T) in
   8.683 -        (CFun (C, S Minus, CFun (C, V (Unsynchronized.inc max_fresh),
   8.684 -                                 ctype_for (nth_range_type 2 T))),
   8.685 -         (gamma, cset |> add_ctype_is_right_unique C))
   8.686 +      let val M = mtype_for (domain_type T) in
   8.687 +        (MFun (M, S Minus, MFun (M, V (Unsynchronized.inc max_fresh),
   8.688 +                                 mtype_for (nth_range_type 2 T))),
   8.689 +         (gamma, cset |> add_mtype_is_right_unique M))
   8.690        end
   8.691      fun do_robust_set_operation T (gamma, cset) =
   8.692        let
   8.693          val set_T = domain_type T
   8.694 -        val C1 = ctype_for set_T
   8.695 -        val C2 = ctype_for set_T
   8.696 -        val C3 = ctype_for set_T
   8.697 +        val M1 = mtype_for set_T
   8.698 +        val M2 = mtype_for set_T
   8.699 +        val M3 = mtype_for set_T
   8.700        in
   8.701 -        (CFun (C1, S Minus, CFun (C2, S Minus, C3)),
   8.702 -         (gamma, cset |> add_is_sub_ctype C1 C3 |> add_is_sub_ctype C2 C3))
   8.703 +        (MFun (M1, S Minus, MFun (M2, S Minus, M3)),
   8.704 +         (gamma, cset |> add_is_sub_mtype M1 M3 |> add_is_sub_mtype M2 M3))
   8.705        end
   8.706      fun do_fragile_set_operation T (gamma, cset) =
   8.707        let
   8.708          val set_T = domain_type T
   8.709 -        val set_C = ctype_for set_T
   8.710 -        (* typ -> ctype *)
   8.711 -        fun custom_ctype_for (T as Type ("fun", [T1, T2])) =
   8.712 -            if T = set_T then set_C
   8.713 -            else CFun (custom_ctype_for T1, S Minus, custom_ctype_for T2)
   8.714 -          | custom_ctype_for T = ctype_for T
   8.715 +        val set_M = mtype_for set_T
   8.716 +        (* typ -> mtyp *)
   8.717 +        fun custom_mtype_for (T as Type ("fun", [T1, T2])) =
   8.718 +            if T = set_T then set_M
   8.719 +            else MFun (custom_mtype_for T1, S Minus, custom_mtype_for T2)
   8.720 +          | custom_mtype_for T = mtype_for T
   8.721        in
   8.722 -        (custom_ctype_for T, (gamma, cset |> add_ctype_is_right_unique set_C))
   8.723 +        (custom_mtype_for T, (gamma, cset |> add_mtype_is_right_unique set_M))
   8.724        end
   8.725 -    (* typ -> accumulator -> ctype * accumulator *)
   8.726 +    (* typ -> accumulator -> mtyp * accumulator *)
   8.727      fun do_pair_constr T accum =
   8.728 -      case ctype_for (nth_range_type 2 T) of
   8.729 -        C as CPair (a_C, b_C) =>
   8.730 -        (CFun (a_C, S Minus, CFun (b_C, S Minus, C)), accum)
   8.731 -      | C => raise CTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [C])
   8.732 -    (* int -> typ -> accumulator -> ctype * accumulator *)
   8.733 +      case mtype_for (nth_range_type 2 T) of
   8.734 +        M as MPair (a_M, b_M) =>
   8.735 +        (MFun (a_M, S Minus, MFun (b_M, S Minus, M)), accum)
   8.736 +      | M => raise MTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [M])
   8.737 +    (* int -> typ -> accumulator -> mtyp * accumulator *)
   8.738      fun do_nth_pair_sel n T =
   8.739 -      case ctype_for (domain_type T) of
   8.740 -        C as CPair (a_C, b_C) =>
   8.741 -        pair (CFun (C, S Minus, if n = 0 then a_C else b_C))
   8.742 -      | C => raise CTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [C])
   8.743 -    val unsolvable = (CType ("unsolvable", []), unsolvable_accum)
   8.744 -    (* typ -> term -> accumulator -> ctype * accumulator *)
   8.745 -    fun do_bounded_quantifier abs_T bound_t body_t accum =
   8.746 +      case mtype_for (domain_type T) of
   8.747 +        M as MPair (a_M, b_M) =>
   8.748 +        pair (MFun (M, S Minus, if n = 0 then a_M else b_M))
   8.749 +      | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M])
   8.750 +    (* mtyp * accumulator *)
   8.751 +    val mtype_unsolvable = (irrelevant_M, unsolvable_accum)
   8.752 +    (* term -> mterm * accumulator *)
   8.753 +    fun mterm_unsolvable t = (MAtom (t, irrelevant_M), unsolvable_accum)
   8.754 +    (* term -> string -> typ -> term -> term -> term -> accumulator
   8.755 +       -> mterm * accumulator *)
   8.756 +    fun do_bounded_quantifier t0 abs_s abs_T connective_t bound_t body_t accum =
   8.757        let
   8.758 -        val abs_C = ctype_for abs_T
   8.759 -        val (bound_C, accum) = accum |>> push_bound abs_C |> do_term bound_t
   8.760 -        val expected_bound_C = pos_set_ctype_for_dom abs_C
   8.761 +        val abs_M = mtype_for abs_T
   8.762 +        val (bound_m, accum) = accum |>> push_bound abs_M |> do_term bound_t
   8.763 +        val expected_bound_M = pos_set_mtype_for_dom abs_M
   8.764 +        val (body_m, accum) =
   8.765 +          accum ||> add_mtypes_equal expected_bound_M (mtype_of_mterm bound_m)
   8.766 +                |> do_term body_t ||> apfst pop_bound
   8.767 +        val bound_M = mtype_of_mterm bound_m
   8.768 +        val (M1, a, M2) = dest_MFun bound_M
   8.769        in
   8.770 -        accum ||> add_ctypes_equal expected_bound_C bound_C |> do_term body_t
   8.771 -              ||> apfst pop_bound
   8.772 +        (MApp (MAtom (t0, MFun (bound_M, S Minus, bool_M)),
   8.773 +               MAbs (abs_s, abs_T, M1, a,
   8.774 +                     MApp (MApp (MAtom (connective_t, irrelevant_M),
   8.775 +                                 MApp (bound_m, MAtom (Bound 0, M1))),
   8.776 +                           body_m))), accum)
   8.777        end
   8.778 -    (* term -> accumulator -> ctype * accumulator *)
   8.779 -    and do_term _ (_, UnsolvableCSet) = unsolvable
   8.780 +    (* term -> accumulator -> mterm * accumulator *)
   8.781 +    and do_term t (_, UnsolvableCSet) = mterm_unsolvable t
   8.782        | do_term t (accum as (gamma as {bounds, frees, consts}, cset)) =
   8.783          (case t of
   8.784             Const (x as (s, T)) =>
   8.785             (case AList.lookup (op =) consts x of
   8.786 -              SOME C => (C, accum)
   8.787 +              SOME M => (M, accum)
   8.788              | NONE =>
   8.789                if not (could_exist_alpha_subtype alpha_T T) then
   8.790 -                (ctype_for T, accum)
   8.791 +                (mtype_for T, accum)
   8.792                else case s of
   8.793 -                @{const_name all} => do_quantifier T accum
   8.794 +                @{const_name all} => do_all T accum
   8.795                | @{const_name "=="} => do_equals T accum
   8.796 -              | @{const_name All} => do_quantifier T accum
   8.797 -              | @{const_name Ex} => do_quantifier T accum
   8.798 +              | @{const_name All} => do_all T accum
   8.799 +              | @{const_name Ex} =>
   8.800 +                do_term (@{const Not}
   8.801 +                         $ (HOLogic.eq_const (domain_type T)
   8.802 +                            $ Abs (Name.uu, T, @{const False}))) accum
   8.803 +                |>> mtype_of_mterm
   8.804                | @{const_name "op ="} => do_equals T accum
   8.805 -              | @{const_name The} => (print_g "*** The"; unsolvable)
   8.806 -              | @{const_name Eps} => (print_g "*** Eps"; unsolvable)
   8.807 +              | @{const_name The} => (print_g "*** The"; mtype_unsolvable)
   8.808 +              | @{const_name Eps} => (print_g "*** Eps"; mtype_unsolvable)
   8.809                | @{const_name If} =>
   8.810                  do_robust_set_operation (range_type T) accum
   8.811 -                |>> curry3 CFun bool_C (S Minus)
   8.812 +                |>> curry3 MFun bool_M (S Minus)
   8.813                | @{const_name Pair} => do_pair_constr T accum
   8.814                | @{const_name fst} => do_nth_pair_sel 0 T accum
   8.815                | @{const_name snd} => do_nth_pair_sel 1 T accum 
   8.816                | @{const_name Id} =>
   8.817 -                (CFun (ctype_for (domain_type T), S Minus, bool_C), accum)
   8.818 +                (MFun (mtype_for (domain_type T), S Minus, bool_M), accum)
   8.819                | @{const_name insert} =>
   8.820                  let
   8.821                    val set_T = domain_type (range_type T)
   8.822 -                  val C1 = ctype_for (domain_type set_T)
   8.823 -                  val C1' = pos_set_ctype_for_dom C1
   8.824 -                  val C2 = ctype_for set_T
   8.825 -                  val C3 = ctype_for set_T
   8.826 +                  val M1 = mtype_for (domain_type set_T)
   8.827 +                  val M1' = pos_set_mtype_for_dom M1
   8.828 +                  val M2 = mtype_for set_T
   8.829 +                  val M3 = mtype_for set_T
   8.830                  in
   8.831 -                  (CFun (C1, S Minus, CFun (C2, S Minus, C3)),
   8.832 -                   (gamma, cset |> add_ctype_is_right_unique C1
   8.833 -                                |> add_is_sub_ctype C1' C3
   8.834 -                                |> add_is_sub_ctype C2 C3))
   8.835 +                  (MFun (M1, S Minus, MFun (M2, S Minus, M3)),
   8.836 +                   (gamma, cset |> add_mtype_is_right_unique M1
   8.837 +                                |> add_is_sub_mtype M1' M3
   8.838 +                                |> add_is_sub_mtype M2 M3))
   8.839                  end
   8.840                | @{const_name converse} =>
   8.841                  let
   8.842                    val x = Unsynchronized.inc max_fresh
   8.843 -                  (* typ -> ctype *)
   8.844 -                  fun ctype_for_set T =
   8.845 -                    CFun (ctype_for (domain_type T), V x, bool_C)
   8.846 -                  val ab_set_C = domain_type T |> ctype_for_set
   8.847 -                  val ba_set_C = range_type T |> ctype_for_set
   8.848 -                in (CFun (ab_set_C, S Minus, ba_set_C), accum) end
   8.849 +                  (* typ -> mtyp *)
   8.850 +                  fun mtype_for_set T =
   8.851 +                    MFun (mtype_for (domain_type T), V x, bool_M)
   8.852 +                  val ab_set_M = domain_type T |> mtype_for_set
   8.853 +                  val ba_set_M = range_type T |> mtype_for_set
   8.854 +                in (MFun (ab_set_M, S Minus, ba_set_M), accum) end
   8.855                | @{const_name trancl} => do_fragile_set_operation T accum
   8.856 -              | @{const_name rtrancl} => (print_g "*** rtrancl"; unsolvable)
   8.857 +              | @{const_name rtrancl} =>
   8.858 +                (print_g "*** rtrancl"; mtype_unsolvable)
   8.859                | @{const_name finite} =>
   8.860 -                let val C1 = ctype_for (domain_type (domain_type T)) in
   8.861 -                  (CFun (pos_set_ctype_for_dom C1, S Minus, bool_C), accum)
   8.862 +                let val M1 = mtype_for (domain_type (domain_type T)) in
   8.863 +                  (MFun (pos_set_mtype_for_dom M1, S Minus, bool_M), accum)
   8.864                  end
   8.865                | @{const_name rel_comp} =>
   8.866                  let
   8.867                    val x = Unsynchronized.inc max_fresh
   8.868 -                  (* typ -> ctype *)
   8.869 -                  fun ctype_for_set T =
   8.870 -                    CFun (ctype_for (domain_type T), V x, bool_C)
   8.871 -                  val bc_set_C = domain_type T |> ctype_for_set
   8.872 -                  val ab_set_C = domain_type (range_type T) |> ctype_for_set
   8.873 -                  val ac_set_C = nth_range_type 2 T |> ctype_for_set
   8.874 +                  (* typ -> mtyp *)
   8.875 +                  fun mtype_for_set T =
   8.876 +                    MFun (mtype_for (domain_type T), V x, bool_M)
   8.877 +                  val bc_set_M = domain_type T |> mtype_for_set
   8.878 +                  val ab_set_M = domain_type (range_type T) |> mtype_for_set
   8.879 +                  val ac_set_M = nth_range_type 2 T |> mtype_for_set
   8.880                  in
   8.881 -                  (CFun (bc_set_C, S Minus, CFun (ab_set_C, S Minus, ac_set_C)),
   8.882 +                  (MFun (bc_set_M, S Minus, MFun (ab_set_M, S Minus, ac_set_M)),
   8.883                     accum)
   8.884                  end
   8.885                | @{const_name image} =>
   8.886                  let
   8.887 -                  val a_C = ctype_for (domain_type (domain_type T))
   8.888 -                  val b_C = ctype_for (range_type (domain_type T))
   8.889 +                  val a_M = mtype_for (domain_type (domain_type T))
   8.890 +                  val b_M = mtype_for (range_type (domain_type T))
   8.891                  in
   8.892 -                  (CFun (CFun (a_C, S Minus, b_C), S Minus,
   8.893 -                         CFun (pos_set_ctype_for_dom a_C, S Minus,
   8.894 -                               pos_set_ctype_for_dom b_C)), accum)
   8.895 +                  (MFun (MFun (a_M, S Minus, b_M), S Minus,
   8.896 +                         MFun (pos_set_mtype_for_dom a_M, S Minus,
   8.897 +                               pos_set_mtype_for_dom b_M)), accum)
   8.898                  end
   8.899                | @{const_name Sigma} =>
   8.900                  let
   8.901                    val x = Unsynchronized.inc max_fresh
   8.902 -                  (* typ -> ctype *)
   8.903 -                  fun ctype_for_set T =
   8.904 -                    CFun (ctype_for (domain_type T), V x, bool_C)
   8.905 +                  (* typ -> mtyp *)
   8.906 +                  fun mtype_for_set T =
   8.907 +                    MFun (mtype_for (domain_type T), V x, bool_M)
   8.908                    val a_set_T = domain_type T
   8.909 -                  val a_C = ctype_for (domain_type a_set_T)
   8.910 -                  val b_set_C = ctype_for_set (range_type (domain_type
   8.911 +                  val a_M = mtype_for (domain_type a_set_T)
   8.912 +                  val b_set_M = mtype_for_set (range_type (domain_type
   8.913                                                                 (range_type T)))
   8.914 -                  val a_set_C = ctype_for_set a_set_T
   8.915 -                  val a_to_b_set_C = CFun (a_C, S Minus, b_set_C)
   8.916 -                  val ab_set_C = ctype_for_set (nth_range_type 2 T)
   8.917 +                  val a_set_M = mtype_for_set a_set_T
   8.918 +                  val a_to_b_set_M = MFun (a_M, S Minus, b_set_M)
   8.919 +                  val ab_set_M = mtype_for_set (nth_range_type 2 T)
   8.920                  in
   8.921 -                  (CFun (a_set_C, S Minus,
   8.922 -                         CFun (a_to_b_set_C, S Minus, ab_set_C)), accum)
   8.923 +                  (MFun (a_set_M, S Minus,
   8.924 +                         MFun (a_to_b_set_M, S Minus, ab_set_M)), accum)
   8.925                  end
   8.926                | @{const_name Tha} =>
   8.927                  let
   8.928 -                  val a_C = ctype_for (domain_type (domain_type T))
   8.929 -                  val a_set_C = pos_set_ctype_for_dom a_C
   8.930 -                in (CFun (a_set_C, S Minus, a_C), accum) end
   8.931 +                  val a_M = mtype_for (domain_type (domain_type T))
   8.932 +                  val a_set_M = pos_set_mtype_for_dom a_M
   8.933 +                in (MFun (a_set_M, S Minus, a_M), accum) end
   8.934                | @{const_name FunBox} =>
   8.935 -                let val dom_C = ctype_for (domain_type T) in
   8.936 -                  (CFun (dom_C, S Minus, dom_C), accum)
   8.937 +                let val dom_M = mtype_for (domain_type T) in
   8.938 +                  (MFun (dom_M, S Minus, dom_M), accum)
   8.939                  end
   8.940                | _ =>
   8.941                  if s = @{const_name minus_class.minus} andalso
   8.942                     is_set_type (domain_type T) then
   8.943                    let
   8.944                      val set_T = domain_type T
   8.945 -                    val left_set_C = ctype_for set_T
   8.946 -                    val right_set_C = ctype_for set_T
   8.947 +                    val left_set_M = mtype_for set_T
   8.948 +                    val right_set_M = mtype_for set_T
   8.949                    in
   8.950 -                    (CFun (left_set_C, S Minus,
   8.951 -                           CFun (right_set_C, S Minus, left_set_C)),
   8.952 -                     (gamma, cset |> add_ctype_is_right_unique right_set_C
   8.953 -                                  |> add_is_sub_ctype right_set_C left_set_C))
   8.954 +                    (MFun (left_set_M, S Minus,
   8.955 +                           MFun (right_set_M, S Minus, left_set_M)),
   8.956 +                     (gamma, cset |> add_mtype_is_right_unique right_set_M
   8.957 +                                  |> add_is_sub_mtype right_set_M left_set_M))
   8.958                    end
   8.959                  else if s = @{const_name ord_class.less_eq} andalso
   8.960                          is_set_type (domain_type T) then
   8.961 @@ -729,34 +792,37 @@
   8.962                    do_robust_set_operation T accum
   8.963                  else if is_sel s then
   8.964                    if constr_name_for_sel_like s = @{const_name FunBox} then
   8.965 -                    let val dom_C = ctype_for (domain_type T) in
   8.966 -                      (CFun (dom_C, S Minus, dom_C), accum)
   8.967 +                    let val dom_M = mtype_for (domain_type T) in
   8.968 +                      (MFun (dom_M, S Minus, dom_M), accum)
   8.969                      end
   8.970                    else
   8.971 -                    (ctype_for_sel cdata x, accum)
   8.972 +                    (mtype_for_sel mdata x, accum)
   8.973                  else if is_constr thy stds x then
   8.974 -                  (ctype_for_constr cdata x, accum)
   8.975 +                  (mtype_for_constr mdata x, accum)
   8.976                  else if is_built_in_const thy stds fast_descrs x then
   8.977                    case def_of_const thy def_table x of
   8.978 -                    SOME t' => do_term t' accum
   8.979 -                  | NONE => (print_g ("*** built-in " ^ s); unsolvable)
   8.980 +                    SOME t' => do_term t' accum |>> mtype_of_mterm
   8.981 +                  | NONE => (print_g ("*** built-in " ^ s); mtype_unsolvable)
   8.982                  else
   8.983 -                  let val C = ctype_for T in
   8.984 -                    (C, ({bounds = bounds, frees = frees,
   8.985 -                          consts = (x, C) :: consts}, cset))
   8.986 -                  end)
   8.987 +                  let val M = mtype_for T in
   8.988 +                    (M, ({bounds = bounds, frees = frees,
   8.989 +                          consts = (x, M) :: consts}, cset))
   8.990 +                  end) |>> curry MAtom t
   8.991           | Free (x as (_, T)) =>
   8.992             (case AList.lookup (op =) frees x of
   8.993 -              SOME C => (C, accum)
   8.994 +              SOME M => (M, accum)
   8.995              | NONE =>
   8.996 -              let val C = ctype_for T in
   8.997 -                (C, ({bounds = bounds, frees = (x, C) :: frees,
   8.998 +              let val M = mtype_for T in
   8.999 +                (M, ({bounds = bounds, frees = (x, M) :: frees,
  8.1000                        consts = consts}, cset))
  8.1001 -              end)
  8.1002 -         | Var _ => (print_g "*** Var"; unsolvable)
  8.1003 -         | Bound j => (nth bounds j, accum)
  8.1004 -         | Abs (_, T, @{const False}) => (ctype_for (T --> bool_T), accum)
  8.1005 -         | Abs (_, T, t') =>
  8.1006 +              end) |>> curry MAtom t
  8.1007 +         | Var _ => (print_g "*** Var"; mterm_unsolvable t)
  8.1008 +         | Bound j => (MAtom (t, nth bounds j), accum)
  8.1009 +         | Abs (s, T, t' as @{const False}) =>
  8.1010 +           let val (M1, a, M2) = mfun_for T bool_T in
  8.1011 +             (MAbs (s, T, M1, a, MAtom (t', M2)), accum)
  8.1012 +           end
  8.1013 +         | Abs (s, T, t') =>
  8.1014             ((case t' of
  8.1015                 t1' $ Bound 0 =>
  8.1016                 if not (loose_bvar1 (t1', 0)) then
  8.1017 @@ -766,43 +832,37 @@
  8.1018               | _ => raise SAME ())
  8.1019              handle SAME () =>
  8.1020                     let
  8.1021 -                     val C = ctype_for T
  8.1022 -                     val (C', accum) = do_term t' (accum |>> push_bound C)
  8.1023 -                   in (CFun (C, S Minus, C'), accum |>> pop_bound) end)
  8.1024 -         | Const (@{const_name All}, _)
  8.1025 -           $ Abs (_, T', @{const "op -->"} $ (t1 $ Bound 0) $ t2) =>
  8.1026 -           do_bounded_quantifier T' t1 t2 accum
  8.1027 -         | Const (@{const_name Ex}, _)
  8.1028 -           $ Abs (_, T', @{const "op &"} $ (t1 $ Bound 0) $ t2) =>
  8.1029 -           do_bounded_quantifier T' t1 t2 accum
  8.1030 +                     val M = mtype_for T
  8.1031 +                     val (m', accum) = do_term t' (accum |>> push_bound M)
  8.1032 +                   in (MAbs (s, T, M, S Minus, m'), accum |>> pop_bound) end)
  8.1033 +         | (t0 as Const (@{const_name All}, _))
  8.1034 +           $ Abs (s', T', (t10 as @{const "op -->"}) $ (t11 $ Bound 0) $ t12) =>
  8.1035 +           do_bounded_quantifier t0 s' T' t10 t11 t12 accum
  8.1036 +         | (t0 as Const (@{const_name Ex}, _))
  8.1037 +           $ Abs (s', T', (t10 as @{const "op &"}) $ (t11 $ Bound 0) $ t12) =>
  8.1038 +           do_bounded_quantifier t0 s' T' t10 t11 t12 accum
  8.1039           | Const (@{const_name Let}, _) $ t1 $ t2 =>
  8.1040             do_term (betapply (t2, t1)) accum
  8.1041           | t1 $ t2 =>
  8.1042             let
  8.1043 -             val (C1, accum) = do_term t1 accum
  8.1044 -             val (C2, accum) = do_term t2 accum
  8.1045 +             val (m1, accum) = do_term t1 accum
  8.1046 +             val (m2, accum) = do_term t2 accum
  8.1047             in
  8.1048               case accum of
  8.1049 -               (_, UnsolvableCSet) => unsolvable
  8.1050 -             | _ => case C1 of
  8.1051 -                      CFun (C11, _, C12) =>
  8.1052 -                      (C12, accum ||> add_is_sub_ctype C2 C11)
  8.1053 -                    | _ => raise CTYPE ("Nitpick_Mono.consider_term.do_term \
  8.1054 -                                        \(op $)", [C1])
  8.1055 +               (_, UnsolvableCSet) => mterm_unsolvable t
  8.1056 +             | _ => (MApp (m1, m2), accum)
  8.1057             end)
  8.1058 -        |> tap (fn (C, _) =>
  8.1059 -                   print_g ("  \<Gamma> \<turnstile> " ^
  8.1060 -                            Syntax.string_of_term ctxt t ^ " : " ^
  8.1061 -                            string_for_ctype C))
  8.1062 +        |> tap (fn (m, _) => print_g ("  \<Gamma> \<turnstile> " ^
  8.1063 +                                      string_for_mterm ctxt m))
  8.1064    in do_term end
  8.1065  
  8.1066 -(* cdata -> sign -> term -> accumulator -> accumulator *)
  8.1067 -fun consider_general_formula (cdata as {hol_ctxt = {ctxt, ...}, ...}) =
  8.1068 +(* mdata -> sign -> term -> accumulator -> accumulator *)
  8.1069 +fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, ...}) =
  8.1070    let
  8.1071 -    (* typ -> ctype *)
  8.1072 -    val ctype_for = fresh_ctype_for_type cdata
  8.1073 -    (* term -> accumulator -> ctype * accumulator *)
  8.1074 -    val do_term = consider_term cdata
  8.1075 +    (* typ -> mtyp *)
  8.1076 +    val mtype_for = fresh_mtype_for_type mdata
  8.1077 +    (* term -> accumulator -> mtyp * accumulator *)
  8.1078 +    val do_term = apfst mtype_of_mterm oo consider_term mdata
  8.1079      (* sign -> term -> accumulator -> accumulator *)
  8.1080      fun do_formula _ _ (_, UnsolvableCSet) = unsolvable_accum
  8.1081        | do_formula sn t (accum as (gamma, cset)) =
  8.1082 @@ -813,25 +873,25 @@
  8.1083            (* string -> typ -> term -> accumulator *)
  8.1084            fun do_quantifier quant_s abs_T body_t =
  8.1085              let
  8.1086 -              val abs_C = ctype_for abs_T
  8.1087 +              val abs_M = mtype_for abs_T
  8.1088                val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
  8.1089 -              val cset = cset |> side_cond ? add_ctype_is_right_total abs_C
  8.1090 +              val cset = cset |> side_cond ? add_mtype_is_right_total abs_M
  8.1091              in
  8.1092 -              (gamma |> push_bound abs_C, cset)
  8.1093 +              (gamma |> push_bound abs_M, cset)
  8.1094                |> do_co_formula body_t |>> pop_bound
  8.1095              end
  8.1096            (* typ -> term -> accumulator *)
  8.1097            fun do_bounded_quantifier abs_T body_t =
  8.1098 -            accum |>> push_bound (ctype_for abs_T) |> do_co_formula body_t
  8.1099 +            accum |>> push_bound (mtype_for abs_T) |> do_co_formula body_t
  8.1100                    |>> pop_bound
  8.1101            (* term -> term -> accumulator *)
  8.1102            fun do_equals t1 t2 =
  8.1103              case sn of
  8.1104                Plus => do_term t accum |> snd
  8.1105              | Minus => let
  8.1106 -                         val (C1, accum) = do_term t1 accum
  8.1107 -                         val (C2, accum) = do_term t2 accum
  8.1108 -                       in accum ||> add_ctypes_equal C1 C2 end
  8.1109 +                         val (M1, accum) = do_term t1 accum
  8.1110 +                         val (M2, accum) = do_term t2 accum
  8.1111 +                       in accum ||> add_mtypes_equal M1 M2 end
  8.1112          in
  8.1113            case t of
  8.1114              Const (s0 as @{const_name all}, _) $ Abs (_, T1, t1) =>
  8.1115 @@ -849,8 +909,13 @@
  8.1116            | Const (@{const_name Ex}, _)
  8.1117              $ Abs (_, T1, t1 as @{const "op &"} $ (_ $ Bound 0) $ _) =>
  8.1118              do_bounded_quantifier T1 t1
  8.1119 -          | Const (s0 as @{const_name Ex}, _) $ Abs (_, T1, t1) =>
  8.1120 -            do_quantifier s0 T1 t1
  8.1121 +          | Const (s0 as @{const_name Ex}, T0) $ (t1 as Abs (_, T1, t1')) =>
  8.1122 +            (case sn of
  8.1123 +               Plus => do_quantifier s0 T1 t1'
  8.1124 +             | Minus =>
  8.1125 +               do_term (@{const Not}
  8.1126 +                        $ (HOLogic.eq_const (domain_type T0) $ t1
  8.1127 +                           $ Abs (Name.uu, T1, @{const False}))) accum |> snd)
  8.1128            | Const (@{const_name "op ="}, _) $ t1 $ t2 => do_equals t1 t2
  8.1129            | @{const "op &"} $ t1 $ t2 =>
  8.1130              accum |> do_co_formula t1 |> do_co_formula t2
  8.1131 @@ -882,32 +947,32 @@
  8.1132    |> (forall (member (op =) harmless_consts o original_name o fst)
  8.1133        orf exists (member (op =) bounteous_consts o fst))
  8.1134  
  8.1135 -(* cdata -> sign -> term -> accumulator -> accumulator *)
  8.1136 -fun consider_nondefinitional_axiom (cdata as {hol_ctxt, ...}) sn t =
  8.1137 -  not (is_harmless_axiom hol_ctxt t) ? consider_general_formula cdata sn t
  8.1138 +(* mdata -> sign -> term -> accumulator -> accumulator *)
  8.1139 +fun consider_nondefinitional_axiom (mdata as {hol_ctxt, ...}) sn t =
  8.1140 +  not (is_harmless_axiom hol_ctxt t) ? consider_general_formula mdata sn t
  8.1141  
  8.1142 -(* cdata -> term -> accumulator -> accumulator *)
  8.1143 -fun consider_definitional_axiom (cdata as {hol_ctxt as {thy, ...}, ...}) t =
  8.1144 +(* mdata -> term -> accumulator -> accumulator *)
  8.1145 +fun consider_definitional_axiom (mdata as {hol_ctxt as {thy, ...}, ...}) t =
  8.1146    if not (is_constr_pattern_formula thy t) then
  8.1147 -    consider_nondefinitional_axiom cdata Plus t
  8.1148 +    consider_nondefinitional_axiom mdata Plus t
  8.1149    else if is_harmless_axiom hol_ctxt t then
  8.1150      I
  8.1151    else
  8.1152      let
  8.1153 -      (* term -> accumulator -> ctype * accumulator *)
  8.1154 -      val do_term = consider_term cdata
  8.1155 +      (* term -> accumulator -> mtyp * accumulator *)
  8.1156 +      val do_term = apfst mtype_of_mterm oo consider_term mdata
  8.1157        (* typ -> term -> accumulator -> accumulator *)
  8.1158        fun do_all abs_T body_t accum =
  8.1159 -        let val abs_C = fresh_ctype_for_type cdata abs_T in
  8.1160 -          accum |>> push_bound abs_C |> do_formula body_t |>> pop_bound
  8.1161 +        let val abs_M = fresh_mtype_for_type mdata abs_T in
  8.1162 +          accum |>> push_bound abs_M |> do_formula body_t |>> pop_bound
  8.1163          end
  8.1164        (* term -> term -> accumulator -> accumulator *)
  8.1165        and do_implies t1 t2 = do_term t1 #> snd #> do_formula t2
  8.1166        and do_equals t1 t2 accum =
  8.1167          let
  8.1168 -          val (C1, accum) = do_term t1 accum
  8.1169 -          val (C2, accum) = do_term t2 accum
  8.1170 -        in accum ||> add_ctypes_equal C1 C2 end
  8.1171 +          val (M1, accum) = do_term t1 accum
  8.1172 +          val (M2, accum) = do_term t2 accum
  8.1173 +        in accum ||> add_mtypes_equal M1 M2 end
  8.1174        (* term -> accumulator -> accumulator *)
  8.1175        and do_formula _ (_, UnsolvableCSet) = unsolvable_accum
  8.1176          | do_formula t accum =
  8.1177 @@ -926,15 +991,15 @@
  8.1178                               \do_formula", [t])
  8.1179      in do_formula t end
  8.1180  
  8.1181 -(* Proof.context -> literal list -> term -> ctype -> string *)
  8.1182 -fun string_for_ctype_of_term ctxt lits t C =
  8.1183 +(* Proof.context -> literal list -> term -> mtyp -> string *)
  8.1184 +fun string_for_mtype_of_term ctxt lits t M =
  8.1185    Syntax.string_of_term ctxt t ^ " : " ^
  8.1186 -  string_for_ctype (instantiate_ctype lits C)
  8.1187 +  string_for_mtype (instantiate_mtype lits M)
  8.1188  
  8.1189 -(* theory -> literal list -> ctype_context -> unit *)
  8.1190 -fun print_ctype_context ctxt lits ({frees, consts, ...} : ctype_context) =
  8.1191 -  map (fn (x, C) => string_for_ctype_of_term ctxt lits (Free x) C) frees @
  8.1192 -  map (fn (x, C) => string_for_ctype_of_term ctxt lits (Const x) C) consts
  8.1193 +(* theory -> literal list -> mtype_context -> unit *)
  8.1194 +fun print_mtype_context ctxt lits ({frees, consts, ...} : mtype_context) =
  8.1195 +  map (fn (x, M) => string_for_mtype_of_term ctxt lits (Free x) M) frees @
  8.1196 +  map (fn (x, M) => string_for_mtype_of_term ctxt lits (Const x) M) consts
  8.1197    |> cat_lines |> print_g
  8.1198  
  8.1199  (* hol_context -> bool -> typ -> term list * term list * term -> bool *)
  8.1200 @@ -942,20 +1007,20 @@
  8.1201                         (def_ts, nondef_ts, core_t) =
  8.1202    let
  8.1203      val _ = print_g ("****** Monotonicity analysis: " ^
  8.1204 -                     string_for_ctype CAlpha ^ " is " ^
  8.1205 +                     string_for_mtype MAlpha ^ " is " ^
  8.1206                       Syntax.string_of_typ ctxt alpha_T)
  8.1207 -    val cdata as {max_fresh, constr_cache, ...} =
  8.1208 -      initial_cdata hol_ctxt binarize alpha_T
  8.1209 +    val mdata as {max_fresh, constr_cache, ...} =
  8.1210 +      initial_mdata hol_ctxt binarize alpha_T
  8.1211      val (gamma as {frees, consts, ...}, cset) =
  8.1212        (initial_gamma, slack)
  8.1213 -      |> fold (consider_definitional_axiom cdata) def_ts
  8.1214 -      |> fold (consider_nondefinitional_axiom cdata Plus) nondef_ts
  8.1215 -      |> consider_general_formula cdata Plus core_t
  8.1216 +      |> fold (consider_definitional_axiom mdata) def_ts
  8.1217 +      |> fold (consider_nondefinitional_axiom mdata Plus) nondef_ts
  8.1218 +      |> consider_general_formula mdata Plus core_t
  8.1219    in
  8.1220      case solve (!max_fresh) cset of
  8.1221 -      SOME lits => (print_ctype_context ctxt lits gamma; true)
  8.1222 +      SOME lits => (print_mtype_context ctxt lits gamma; true)
  8.1223      | _ => false
  8.1224    end
  8.1225 -  handle CTYPE (loc, Cs) => raise BAD (loc, commas (map string_for_ctype Cs))
  8.1226 +  handle MTYPE (loc, Ms) => raise BAD (loc, commas (map string_for_mtype Ms))
  8.1227  
  8.1228  end;
     9.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu Feb 25 10:08:44 2010 +0100
     9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu Feb 25 16:33:39 2010 +0100
     9.3 @@ -1031,7 +1031,7 @@
     9.4              if is_opt_rep R then
     9.5                triad_fn (fn polar => s_op2 Subset T (Formula polar) u1 u2)
     9.6              else if opt andalso polar = Pos andalso
     9.7 -                    not (is_concrete_type datatypes (type_of u1)) then
     9.8 +                    not (is_concrete_type datatypes true (type_of u1)) then
     9.9                Cst (False, T, Formula Pos)
    9.10              else
    9.11                s_op2 Subset T R u1 u2
    9.12 @@ -1057,7 +1057,7 @@
    9.13                else opt_opt_case ()
    9.14            in
    9.15              if unsound orelse polar = Neg orelse
    9.16 -               is_concrete_type datatypes (type_of u1) then
    9.17 +               is_concrete_type datatypes true (type_of u1) then
    9.18                case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of
    9.19                  (true, true) => opt_opt_case ()
    9.20                | (true, false) => hybrid_case u1'
    9.21 @@ -1159,7 +1159,7 @@
    9.22                  let val quant_u = s_op2 oper T (Formula polar) u1' u2' in
    9.23                    if def orelse
    9.24                       (unsound andalso (polar = Pos) = (oper = All)) orelse
    9.25 -                     is_complete_type datatypes (type_of u1) then
    9.26 +                     is_complete_type datatypes true (type_of u1) then
    9.27                      quant_u
    9.28                    else
    9.29                      let
    9.30 @@ -1202,7 +1202,7 @@
    9.31                        else unopt_R |> opt ? opt_rep ofs T
    9.32                val u = Op2 (oper, T, R, u1', sub u2)
    9.33              in
    9.34 -              if is_complete_type datatypes T orelse not opt1 then
    9.35 +              if is_complete_type datatypes true T orelse not opt1 then
    9.36                  u
    9.37                else
    9.38                  let
    10.1 --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Thu Feb 25 10:08:44 2010 +0100
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Thu Feb 25 16:33:39 2010 +0100
    10.3 @@ -126,7 +126,7 @@
    10.4  val norm_frac_rel = (4, 0)
    10.5  
    10.6  (* int -> bool -> rel_expr *)
    10.7 -fun atom_for_bool j0 = Atom o Integer.add j0 o int_for_bool
    10.8 +fun atom_for_bool j0 = Atom o Integer.add j0 o int_from_bool
    10.9  (* bool -> formula *)
   10.10  fun formula_for_bool b = if b then True else False
   10.11  
    11.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Feb 25 10:08:44 2010 +0100
    11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Feb 25 16:33:39 2010 +0100
    11.3 @@ -168,7 +168,6 @@
    11.4      | (Type (new_s, new_Ts as [new_T1, new_T2]),
    11.5         Type (old_s, old_Ts as [old_T1, old_T2])) =>
    11.6        if old_s = @{type_name fun_box} orelse
    11.7 -         old_s = @{type_name fin_fun} orelse
    11.8           old_s = @{type_name pair_box} orelse old_s = "*" then
    11.9          case constr_expand hol_ctxt old_T t of
   11.10            Const (old_s, _) $ t1 =>
    12.1 --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML	Thu Feb 25 10:08:44 2010 +0100
    12.2 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML	Thu Feb 25 16:33:39 2010 +0100
    12.3 @@ -299,7 +299,7 @@
    12.4       | z => Func z)
    12.5    | best_non_opt_set_rep_for_type scope T = best_one_rep_for_type scope T
    12.6  fun best_set_rep_for_type (scope as {datatypes, ...}) T =
    12.7 -  (if is_exact_type datatypes T then best_non_opt_set_rep_for_type
    12.8 +  (if is_exact_type datatypes true T then best_non_opt_set_rep_for_type
    12.9     else best_opt_set_rep_for_type) scope T
   12.10  fun best_non_opt_symmetric_reps_for_fun_type (scope as {ofs, ...})
   12.11                                               (Type ("fun", [T1, T2])) =
    13.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Thu Feb 25 10:08:44 2010 +0100
    13.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Thu Feb 25 16:33:39 2010 +0100
    13.3 @@ -23,8 +23,8 @@
    13.4      card: int,
    13.5      co: bool,
    13.6      standard: bool,
    13.7 -    complete: bool,
    13.8 -    concrete: bool,
    13.9 +    complete: bool * bool,
   13.10 +    concrete: bool * bool,
   13.11      deep: bool,
   13.12      constrs: constr_spec list}
   13.13  
   13.14 @@ -39,9 +39,9 @@
   13.15  
   13.16    val datatype_spec : dtype_spec list -> typ -> dtype_spec option
   13.17    val constr_spec : dtype_spec list -> styp -> constr_spec
   13.18 -  val is_complete_type : dtype_spec list -> typ -> bool
   13.19 -  val is_concrete_type : dtype_spec list -> typ -> bool
   13.20 -  val is_exact_type : dtype_spec list -> typ -> bool
   13.21 +  val is_complete_type : dtype_spec list -> bool -> typ -> bool
   13.22 +  val is_concrete_type : dtype_spec list -> bool -> typ -> bool
   13.23 +  val is_exact_type : dtype_spec list -> bool -> typ -> bool
   13.24    val offset_of_type : int Typtab.table -> typ -> int
   13.25    val spec_of_type : scope -> typ -> int * int
   13.26    val pretties_for_scope : scope -> bool -> Pretty.T list
   13.27 @@ -51,7 +51,7 @@
   13.28    val all_scopes :
   13.29      hol_context -> bool -> int -> (typ option * int list) list
   13.30      -> (styp option * int list) list -> (styp option * int list) list
   13.31 -    -> int list -> int list -> typ list -> typ list -> typ list
   13.32 +    -> int list -> int list -> typ list -> typ list -> typ list -> typ list
   13.33      -> int * scope list
   13.34  end;
   13.35  
   13.36 @@ -74,8 +74,8 @@
   13.37    card: int,
   13.38    co: bool,
   13.39    standard: bool,
   13.40 -  complete: bool,
   13.41 -  concrete: bool,
   13.42 +  complete: bool * bool,
   13.43 +  concrete: bool * bool,
   13.44    deep: bool,
   13.45    constrs: constr_spec list}
   13.46  
   13.47 @@ -105,22 +105,24 @@
   13.48        SOME c => c
   13.49      | NONE => constr_spec dtypes x
   13.50  
   13.51 -(* dtype_spec list -> typ -> bool *)
   13.52 -fun is_complete_type dtypes (Type ("fun", [T1, T2])) =
   13.53 -    is_concrete_type dtypes T1 andalso is_complete_type dtypes T2
   13.54 -  | is_complete_type dtypes (Type ("*", Ts)) =
   13.55 -    forall (is_complete_type dtypes) Ts
   13.56 -  | is_complete_type dtypes T =
   13.57 +(* dtype_spec list -> bool -> typ -> bool *)
   13.58 +fun is_complete_type dtypes facto (Type ("fun", [T1, T2])) =
   13.59 +    is_concrete_type dtypes facto T1 andalso is_complete_type dtypes facto T2
   13.60 +  | is_complete_type dtypes facto (Type ("*", Ts)) =
   13.61 +    forall (is_complete_type dtypes facto) Ts
   13.62 +  | is_complete_type dtypes facto T =
   13.63      not (is_integer_like_type T) andalso not (is_bit_type T) andalso
   13.64 -    #complete (the (datatype_spec dtypes T))
   13.65 +    fun_from_pair (#complete (the (datatype_spec dtypes T))) facto
   13.66      handle Option.Option => true
   13.67 -and is_concrete_type dtypes (Type ("fun", [T1, T2])) =
   13.68 -    is_complete_type dtypes T1 andalso is_concrete_type dtypes T2
   13.69 -  | is_concrete_type dtypes (Type ("*", Ts)) =
   13.70 -    forall (is_concrete_type dtypes) Ts
   13.71 -  | is_concrete_type dtypes T =
   13.72 -    #concrete (the (datatype_spec dtypes T)) handle Option.Option => true
   13.73 -fun is_exact_type dtypes = is_complete_type dtypes andf is_concrete_type dtypes
   13.74 +and is_concrete_type dtypes facto (Type ("fun", [T1, T2])) =
   13.75 +    is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2
   13.76 +  | is_concrete_type dtypes facto (Type ("*", Ts)) =
   13.77 +    forall (is_concrete_type dtypes facto) Ts
   13.78 +  | is_concrete_type dtypes facto T =
   13.79 +    fun_from_pair (#concrete (the (datatype_spec dtypes T))) facto
   13.80 +    handle Option.Option => true
   13.81 +fun is_exact_type dtypes facto =
   13.82 +  is_complete_type dtypes facto andf is_concrete_type dtypes facto
   13.83  
   13.84  (* int Typtab.table -> typ -> int *)
   13.85  fun offset_of_type ofs T =
   13.86 @@ -461,15 +463,18 @@
   13.87       explicit_max = max, total = total} :: constrs
   13.88    end
   13.89  
   13.90 -(* hol_context -> (typ * int) list -> typ -> bool *)
   13.91 -fun has_exact_card hol_ctxt card_assigns T =
   13.92 +(* hol_context -> bool -> typ list -> (typ * int) list -> typ -> bool *)
   13.93 +fun has_exact_card hol_ctxt facto finitizable_dataTs card_assigns T =
   13.94    let val card = card_of_type card_assigns T in
   13.95 -    card = bounded_exact_card_of_type hol_ctxt (card + 1) 0 card_assigns T
   13.96 +    card = bounded_exact_card_of_type hol_ctxt
   13.97 +               (if facto then finitizable_dataTs else []) (card + 1) 0
   13.98 +               card_assigns T
   13.99    end
  13.100  
  13.101 -(* hol_context -> bool -> typ list -> scope_desc -> typ * int -> dtype_spec *)
  13.102 +(* hol_context -> bool -> typ list -> typ list -> scope_desc -> typ * int
  13.103 +   -> dtype_spec *)
  13.104  fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, stds, ...}) binarize
  13.105 -        deep_dataTs (desc as (card_assigns, _)) (T, card) =
  13.106 +        deep_dataTs finitizable_dataTs (desc as (card_assigns, _)) (T, card) =
  13.107    let
  13.108      val deep = member (op =) deep_dataTs T
  13.109      val co = is_codatatype thy T
  13.110 @@ -478,10 +483,16 @@
  13.111      val self_recs = map (is_self_recursive_constr_type o snd) xs
  13.112      val (num_self_recs, num_non_self_recs) =
  13.113        List.partition I self_recs |> pairself length
  13.114 -    val complete = has_exact_card hol_ctxt card_assigns T
  13.115 -    val concrete = is_word_type T orelse
  13.116 -                   (xs |> maps (binder_types o snd) |> maps binder_types
  13.117 -                       |> forall (has_exact_card hol_ctxt card_assigns))
  13.118 +    (* bool -> bool *)
  13.119 +    fun is_complete facto =
  13.120 +      has_exact_card hol_ctxt facto finitizable_dataTs card_assigns T
  13.121 +    fun is_concrete facto =
  13.122 +      is_word_type T orelse
  13.123 +      xs |> maps (binder_types o snd) |> maps binder_types
  13.124 +         |> forall (has_exact_card hol_ctxt facto finitizable_dataTs
  13.125 +                                   card_assigns)
  13.126 +    val complete = pair_from_fun is_complete
  13.127 +    val concrete = pair_from_fun is_concrete
  13.128      (* int -> int *)
  13.129      fun sum_dom_cards max =
  13.130        map (domain_card max card_assigns o snd) xs |> Integer.sum
  13.131 @@ -494,13 +505,15 @@
  13.132       concrete = concrete, deep = deep, constrs = constrs}
  13.133    end
  13.134  
  13.135 -(* hol_context -> bool -> int -> typ list -> scope_desc -> scope *)
  13.136 +(* hol_context -> bool -> int -> typ list -> typ list -> scope_desc -> scope *)
  13.137  fun scope_from_descriptor (hol_ctxt as {thy, stds, ...}) binarize sym_break
  13.138 -                          deep_dataTs (desc as (card_assigns, _)) =
  13.139 +                          deep_dataTs finitizable_dataTs
  13.140 +                          (desc as (card_assigns, _)) =
  13.141    let
  13.142      val datatypes =
  13.143        map (datatype_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs
  13.144 -               desc) (filter (is_datatype thy stds o fst) card_assigns)
  13.145 +                                               finitizable_dataTs desc)
  13.146 +          (filter (is_datatype thy stds o fst) card_assigns)
  13.147      val bits = card_of_type card_assigns @{typ signed_bit} - 1
  13.148                 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
  13.149                        card_of_type card_assigns @{typ unsigned_bit}
  13.150 @@ -530,10 +543,10 @@
  13.151  
  13.152  (* hol_context -> bool -> int -> (typ option * int list) list
  13.153     -> (styp option * int list) list -> (styp option * int list) list -> int list
  13.154 -   -> typ list -> typ list -> typ list -> int * scope list *)
  13.155 +   -> typ list -> typ list -> typ list ->typ list -> int * scope list *)
  13.156  fun all_scopes (hol_ctxt as {thy, ...}) binarize sym_break cards_assigns
  13.157                 maxes_assigns iters_assigns bitss bisim_depths mono_Ts nonmono_Ts
  13.158 -               deep_dataTs =
  13.159 +               deep_dataTs finitizable_dataTs =
  13.160    let
  13.161      val cards_assigns = repair_cards_assigns_wrt_boxing thy mono_Ts
  13.162                                                          cards_assigns
  13.163 @@ -550,7 +563,7 @@
  13.164      (length all - length head,
  13.165       descs |> length descs <= distinct_threshold ? distinct (op =)
  13.166             |> map (scope_from_descriptor hol_ctxt binarize sym_break
  13.167 -                                         deep_dataTs))
  13.168 +                                         deep_dataTs finitizable_dataTs))
  13.169    end
  13.170  
  13.171  end;
    14.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu Feb 25 10:08:44 2010 +0100
    14.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu Feb 25 16:33:39 2010 +0100
    14.3 @@ -20,7 +20,9 @@
    14.4    val nitpick_prefix : string
    14.5    val curry3 : ('a * 'b * 'c -> 'd) -> 'a -> 'b -> 'c -> 'd
    14.6    val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c
    14.7 -  val int_for_bool : bool -> int
    14.8 +  val pair_from_fun : (bool -> 'a) -> 'a * 'a
    14.9 +  val fun_from_pair : 'a * 'a -> bool -> 'a
   14.10 +  val int_from_bool : bool -> int
   14.11    val nat_minus : int -> int -> int
   14.12    val reasonable_power : int -> int -> int
   14.13    val exact_log : int -> int -> int
   14.14 @@ -84,8 +86,13 @@
   14.15  (* ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c *)
   14.16  fun pairf f g x = (f x, g x)
   14.17  
   14.18 +(* (bool -> 'a) -> 'a * 'a *)
   14.19 +fun pair_from_fun f = (f false, f true)
   14.20 +(* 'a * 'a -> bool -> 'a *)
   14.21 +fun fun_from_pair (f, t) b = if b then t else f
   14.22 +
   14.23  (* bool -> int *)
   14.24 -fun int_for_bool b = if b then 1 else 0
   14.25 +fun int_from_bool b = if b then 1 else 0
   14.26  (* int -> int -> int *)
   14.27  fun nat_minus i j = if i > j then i - j else 0
   14.28