src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 34982 7b8c366e34a2
parent 34936 c4f04bee79f3
child 34998 5e492a862b34
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Feb 01 14:12:12 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Feb 02 11:38:38 2010 +0100
     1.3 @@ -1,16 +1,17 @@
     1.4  (*  Title:      HOL/Tools/Nitpick/nitpick_mono.ML
     1.5      Author:     Jasmin Blanchette, TU Muenchen
     1.6 -    Copyright   2009
     1.7 +    Copyright   2009, 2010
     1.8  
     1.9  Monotonicity predicate for higher-order logic.
    1.10  *)
    1.11  
    1.12  signature NITPICK_MONO =
    1.13  sig
    1.14 +  datatype sign = Plus | Minus
    1.15    type extended_context = Nitpick_HOL.extended_context
    1.16  
    1.17    val formulas_monotonic :
    1.18 -    extended_context -> typ -> term list -> term list -> term -> bool
    1.19 +    extended_context -> typ -> sign -> term list -> term list -> term -> bool
    1.20  end;
    1.21  
    1.22  structure Nitpick_Mono : NITPICK_MONO =
    1.23 @@ -21,7 +22,7 @@
    1.24  
    1.25  type var = int
    1.26  
    1.27 -datatype sign = Pos | Neg
    1.28 +datatype sign = Plus | Minus
    1.29  datatype sign_atom = S of sign | V of var
    1.30  
    1.31  type literal = var * sign
    1.32 @@ -54,13 +55,13 @@
    1.33    if null xs then "" else "\<^bsub>" ^ string_for_vars sep xs ^ "\<^esub>"
    1.34  
    1.35  (* sign -> string *)
    1.36 -fun string_for_sign Pos = "+"
    1.37 -  | string_for_sign Neg = "-"
    1.38 +fun string_for_sign Plus = "+"
    1.39 +  | string_for_sign Minus = "-"
    1.40  
    1.41  (* sign -> sign -> sign *)
    1.42 -fun xor sn1 sn2 = if sn1 = sn2 then Pos else Neg
    1.43 +fun xor sn1 sn2 = if sn1 = sn2 then Plus else Minus
    1.44  (* sign -> sign *)
    1.45 -val negate = xor Neg
    1.46 +val negate = xor Minus
    1.47  
    1.48  (* sign_atom -> string *)
    1.49  fun string_for_sign_atom (S sn) = string_for_sign sn
    1.50 @@ -152,7 +153,7 @@
    1.51  
    1.52  (* string * typ list -> ctype list -> ctype *)
    1.53  fun constr_ctype_for_binders z Cs =
    1.54 -  fold_rev (fn C => curry3 CFun C (S Neg)) Cs (CRec z)
    1.55 +  fold_rev (fn C => curry3 CFun C (S Minus)) Cs (CRec z)
    1.56  
    1.57  (* ((string * typ list) * ctype) list -> ctype list -> ctype -> ctype *)
    1.58  fun repair_ctype _ _ CAlpha = CAlpha
    1.59 @@ -199,7 +200,7 @@
    1.60                     exists_alpha_sub_ctype_fresh C1 then
    1.61                    V (Unsynchronized.inc max_fresh)
    1.62                  else
    1.63 -                  S Neg
    1.64 +                  S Minus
    1.65        in CFun (C1, a, C2) end
    1.66      (* typ -> ctype *)
    1.67      and do_type T =
    1.68 @@ -252,13 +253,13 @@
    1.69  fun prodC_factors (CPair (C1, C2)) = maps prodC_factors [C1, C2]
    1.70    | prodC_factors C = [C]
    1.71  (* ctype -> ctype list * ctype *)
    1.72 -fun curried_strip_ctype (CFun (C1, S Neg, C2)) =
    1.73 +fun curried_strip_ctype (CFun (C1, S Minus, C2)) =
    1.74      curried_strip_ctype C2 |>> append (prodC_factors C1)
    1.75    | curried_strip_ctype C = ([], C)
    1.76  (* string -> ctype -> ctype *)
    1.77  fun sel_ctype_from_constr_ctype s C =
    1.78    let val (arg_Cs, dataC) = curried_strip_ctype C in
    1.79 -    CFun (dataC, S Neg,
    1.80 +    CFun (dataC, S Minus,
    1.81            case sel_no_from_name s of ~1 => bool_C | n => nth arg_Cs n)
    1.82    end
    1.83  
    1.84 @@ -268,8 +269,13 @@
    1.85    if could_exist_alpha_sub_ctype thy alpha_T T then
    1.86      case AList.lookup (op =) (!constr_cache) x of
    1.87        SOME C => C
    1.88 -    | NONE => (fresh_ctype_for_type cdata (body_type T);
    1.89 -               AList.lookup (op =) (!constr_cache) x |> the)
    1.90 +    | NONE => if T = alpha_T then
    1.91 +                let val C = fresh_ctype_for_type cdata T in
    1.92 +                  (Unsynchronized.change constr_cache (cons (x, C)); C)
    1.93 +                end
    1.94 +              else
    1.95 +                (fresh_ctype_for_type cdata (body_type T);
    1.96 +                 AList.lookup (op =) (!constr_cache) x |> the)
    1.97    else
    1.98      fresh_ctype_for_type cdata T
    1.99  fun ctype_for_sel (cdata as {ext_ctxt, ...}) (x as (s, _)) =
   1.100 @@ -332,9 +338,9 @@
   1.101       | _ => do_sign_atom_comp Eq [] a2 a1 accum)
   1.102    | do_sign_atom_comp Leq [] a1 a2 (accum as (lits, comps)) =
   1.103      (case (a1, a2) of
   1.104 -       (_, S Neg) => SOME accum
   1.105 -     | (S Pos, _) => SOME accum
   1.106 -     | (S Neg, S Pos) => NONE
   1.107 +       (_, S Minus) => SOME accum
   1.108 +     | (S Plus, _) => SOME accum
   1.109 +     | (S Minus, S Plus) => NONE
   1.110       | (V _, V _) => SOME (lits, insert (op =) (a1, a2, Leq, []) comps)
   1.111       | _ => do_sign_atom_comp Eq [] a1 a2 accum)
   1.112    | do_sign_atom_comp cmp xs a1 a2 (accum as (lits, comps)) =
   1.113 @@ -354,8 +360,8 @@
   1.114         accum |> do_sign_atom_comp Leq xs a1 a2
   1.115               |> do_ctype_comp Leq xs C21 C11
   1.116               |> (case a2 of
   1.117 -                   S Neg => I
   1.118 -                 | S Pos => do_ctype_comp Leq xs C11 C21
   1.119 +                   S Minus => I
   1.120 +                 | S Plus => do_ctype_comp Leq xs C11 C21
   1.121                   | V x => do_ctype_comp Leq (x :: xs) C11 C21)
   1.122       else
   1.123         SOME accum)
   1.124 @@ -386,29 +392,33 @@
   1.125  (* sign -> sign_expr -> ctype -> (literal list * sign_expr list) option
   1.126     -> (literal list * sign_expr list) option *)
   1.127  fun do_notin_ctype_fv _ _ _ NONE = NONE
   1.128 -  | do_notin_ctype_fv Neg _ CAlpha accum = accum
   1.129 -  | do_notin_ctype_fv Pos [] CAlpha _ = NONE
   1.130 -  | do_notin_ctype_fv Pos [(x, sn)] CAlpha (SOME (lits, sexps)) =
   1.131 +  | do_notin_ctype_fv Minus _ CAlpha accum = accum
   1.132 +  | do_notin_ctype_fv Plus [] CAlpha _ = NONE
   1.133 +  | do_notin_ctype_fv Plus [(x, sn)] CAlpha (SOME (lits, sexps)) =
   1.134      SOME lits |> do_literal (x, sn) |> Option.map (rpair sexps)
   1.135 -  | do_notin_ctype_fv Pos sexp CAlpha (SOME (lits, sexps)) =
   1.136 +  | do_notin_ctype_fv Plus sexp CAlpha (SOME (lits, sexps)) =
   1.137      SOME (lits, insert (op =) sexp sexps)
   1.138    | do_notin_ctype_fv sn sexp (CFun (C1, S sn', C2)) accum =
   1.139 -    accum |> (if sn' = Pos andalso sn = Pos then do_notin_ctype_fv Pos sexp C1
   1.140 -              else I)
   1.141 -          |> (if sn' = Neg orelse sn = Pos then do_notin_ctype_fv Neg sexp C1
   1.142 -              else I)
   1.143 +    accum |> (if sn' = Plus andalso sn = Plus then
   1.144 +                do_notin_ctype_fv Plus sexp C1
   1.145 +              else
   1.146 +                I)
   1.147 +          |> (if sn' = Minus orelse sn = Plus then
   1.148 +                do_notin_ctype_fv Minus sexp C1
   1.149 +              else
   1.150 +                I)
   1.151            |> do_notin_ctype_fv sn sexp C2
   1.152 -  | do_notin_ctype_fv Pos sexp (CFun (C1, V x, C2)) accum =
   1.153 -    accum |> (case do_literal (x, Neg) (SOME sexp) of
   1.154 +  | do_notin_ctype_fv Plus sexp (CFun (C1, V x, C2)) accum =
   1.155 +    accum |> (case do_literal (x, Minus) (SOME sexp) of
   1.156                  NONE => I
   1.157 -              | SOME sexp' => do_notin_ctype_fv Pos sexp' C1)
   1.158 -          |> do_notin_ctype_fv Neg sexp C1
   1.159 -          |> do_notin_ctype_fv Pos sexp C2
   1.160 -  | do_notin_ctype_fv Neg sexp (CFun (C1, V x, C2)) accum =
   1.161 -    accum |> (case do_literal (x, Pos) (SOME sexp) of
   1.162 +              | SOME sexp' => do_notin_ctype_fv Plus sexp' C1)
   1.163 +          |> do_notin_ctype_fv Minus sexp C1
   1.164 +          |> do_notin_ctype_fv Plus sexp C2
   1.165 +  | do_notin_ctype_fv Minus sexp (CFun (C1, V x, C2)) accum =
   1.166 +    accum |> (case do_literal (x, Plus) (SOME sexp) of
   1.167                  NONE => I
   1.168 -              | SOME sexp' => do_notin_ctype_fv Pos sexp' C1)
   1.169 -          |> do_notin_ctype_fv Neg sexp C2
   1.170 +              | SOME sexp' => do_notin_ctype_fv Plus sexp' C1)
   1.171 +          |> do_notin_ctype_fv Minus sexp C2
   1.172    | do_notin_ctype_fv sn sexp (CPair (C1, C2)) accum =
   1.173      accum |> fold (do_notin_ctype_fv sn sexp) [C1, C2]
   1.174    | do_notin_ctype_fv sn sexp (CType (_, Cs)) accum =
   1.175 @@ -420,14 +430,14 @@
   1.176  fun add_notin_ctype_fv _ _ UnsolvableCSet = UnsolvableCSet
   1.177    | add_notin_ctype_fv sn C (CSet (lits, comps, sexps)) =
   1.178      (print_g ("*** Add " ^ string_for_ctype C ^ " is right-" ^
   1.179 -              (case sn of Neg => "unique" | Pos => "total") ^ ".");
   1.180 +              (case sn of Minus => "unique" | Plus => "total") ^ ".");
   1.181       case do_notin_ctype_fv sn [] C (SOME (lits, sexps)) of
   1.182         NONE => (print_g "**** Unsolvable"; UnsolvableCSet)
   1.183       | SOME (lits, sexps) => CSet (lits, comps, sexps))
   1.184  
   1.185  (* ctype -> constraint_set -> constraint_set *)
   1.186 -val add_ctype_is_right_unique = add_notin_ctype_fv Neg
   1.187 -val add_ctype_is_right_total = add_notin_ctype_fv Pos
   1.188 +val add_ctype_is_right_unique = add_notin_ctype_fv Minus
   1.189 +val add_ctype_is_right_total = add_notin_ctype_fv Plus
   1.190  
   1.191  (* constraint_set -> constraint_set -> constraint_set *)
   1.192  fun unite (CSet (lits1, comps1, sexps1)) (CSet (lits2, comps2, sexps2)) =
   1.193 @@ -437,11 +447,11 @@
   1.194    | unite _ _ = UnsolvableCSet
   1.195  
   1.196  (* sign -> bool *)
   1.197 -fun bool_from_sign Pos = false
   1.198 -  | bool_from_sign Neg = true
   1.199 +fun bool_from_sign Plus = false
   1.200 +  | bool_from_sign Minus = true
   1.201  (* bool -> sign *)
   1.202 -fun sign_from_bool false = Pos
   1.203 -  | sign_from_bool true = Neg
   1.204 +fun sign_from_bool false = Plus
   1.205 +  | sign_from_bool true = Minus
   1.206  
   1.207  (* literal -> PropLogic.prop_formula *)
   1.208  fun prop_for_literal (x, sn) =
   1.209 @@ -460,10 +470,10 @@
   1.210      PropLogic.SAnd (prop_for_comp (a1, a2, Leq, []),
   1.211                      prop_for_comp (a2, a1, Leq, []))
   1.212    | prop_for_comp (a1, a2, Leq, []) =
   1.213 -    PropLogic.SOr (prop_for_sign_atom_eq (a1, Pos),
   1.214 -                   prop_for_sign_atom_eq (a2, Neg))
   1.215 +    PropLogic.SOr (prop_for_sign_atom_eq (a1, Plus),
   1.216 +                   prop_for_sign_atom_eq (a2, Minus))
   1.217    | prop_for_comp (a1, a2, cmp, xs) =
   1.218 -    PropLogic.SOr (prop_for_exists_eq xs Neg, prop_for_comp (a1, a2, cmp, []))
   1.219 +    PropLogic.SOr (prop_for_exists_eq xs Minus, prop_for_comp (a1, a2, cmp, []))
   1.220  
   1.221  (* var -> (int -> bool option) -> literal list -> literal list *)
   1.222  fun literals_from_assignments max_var assigns lits =
   1.223 @@ -491,7 +501,7 @@
   1.224  
   1.225  (* literal list -> unit *)
   1.226  fun print_solution lits =
   1.227 -  let val (pos, neg) = List.partition (curry (op =) Pos o snd) lits in
   1.228 +  let val (pos, neg) = List.partition (curry (op =) Plus o snd) lits in
   1.229      print_g ("*** Solution:\n" ^
   1.230               "+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^
   1.231               "-: " ^ commas (map (string_for_var o fst) neg))
   1.232 @@ -523,7 +533,7 @@
   1.233  type ctype_context =
   1.234    {bounds: ctype list,
   1.235     frees: (styp * ctype) list,
   1.236 -   consts: (styp * ctype_schema) list}
   1.237 +   consts: (styp * ctype) list}
   1.238  
   1.239  type accumulator = ctype_context * constraint_set
   1.240  
   1.241 @@ -546,20 +556,20 @@
   1.242      val ctype_for = fresh_ctype_for_type cdata
   1.243      (* ctype -> ctype *)
   1.244      fun pos_set_ctype_for_dom C =
   1.245 -      CFun (C, S (if exists_alpha_sub_ctype C then Pos else Neg), bool_C)
   1.246 +      CFun (C, S (if exists_alpha_sub_ctype C then Plus else Minus), bool_C)
   1.247      (* typ -> accumulator -> ctype * accumulator *)
   1.248      fun do_quantifier T (gamma, cset) =
   1.249        let
   1.250          val abs_C = ctype_for (domain_type (domain_type T))
   1.251          val body_C = ctype_for (range_type T)
   1.252        in
   1.253 -        (CFun (CFun (abs_C, S Neg, body_C), S Neg, body_C),
   1.254 +        (CFun (CFun (abs_C, S Minus, body_C), S Minus, body_C),
   1.255           (gamma, cset |> add_ctype_is_right_total abs_C))
   1.256        end
   1.257      fun do_equals T (gamma, cset) =
   1.258        let val C = ctype_for (domain_type T) in
   1.259 -        (CFun (C, S Neg, CFun (C, V (Unsynchronized.inc max_fresh),
   1.260 -                               ctype_for (nth_range_type 2 T))),
   1.261 +        (CFun (C, S Minus, CFun (C, V (Unsynchronized.inc max_fresh),
   1.262 +                                 ctype_for (nth_range_type 2 T))),
   1.263           (gamma, cset |> add_ctype_is_right_unique C))
   1.264        end
   1.265      fun do_robust_set_operation T (gamma, cset) =
   1.266 @@ -569,7 +579,7 @@
   1.267          val C2 = ctype_for set_T
   1.268          val C3 = ctype_for set_T
   1.269        in
   1.270 -        (CFun (C1, S Neg, CFun (C2, S Neg, C3)),
   1.271 +        (CFun (C1, S Minus, CFun (C2, S Minus, C3)),
   1.272           (gamma, cset |> add_is_sub_ctype C1 C3 |> add_is_sub_ctype C2 C3))
   1.273        end
   1.274      fun do_fragile_set_operation T (gamma, cset) =
   1.275 @@ -579,7 +589,7 @@
   1.276          (* typ -> ctype *)
   1.277          fun custom_ctype_for (T as Type ("fun", [T1, T2])) =
   1.278              if T = set_T then set_C
   1.279 -            else CFun (custom_ctype_for T1, S Neg, custom_ctype_for T2)
   1.280 +            else CFun (custom_ctype_for T1, S Minus, custom_ctype_for T2)
   1.281            | custom_ctype_for T = ctype_for T
   1.282        in
   1.283          (custom_ctype_for T, (gamma, cset |> add_ctype_is_right_unique set_C))
   1.284 @@ -588,13 +598,13 @@
   1.285      fun do_pair_constr T accum =
   1.286        case ctype_for (nth_range_type 2 T) of
   1.287          C as CPair (a_C, b_C) =>
   1.288 -        (CFun (a_C, S Neg, CFun (b_C, S Neg, C)), accum)
   1.289 +        (CFun (a_C, S Minus, CFun (b_C, S Minus, C)), accum)
   1.290        | C => raise CTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [C])
   1.291      (* int -> typ -> accumulator -> ctype * accumulator *)
   1.292      fun do_nth_pair_sel n T =
   1.293        case ctype_for (domain_type T) of
   1.294          C as CPair (a_C, b_C) =>
   1.295 -        pair (CFun (C, S Neg, if n = 0 then a_C else b_C))
   1.296 +        pair (CFun (C, S Minus, if n = 0 then a_C else b_C))
   1.297        | C => raise CTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [C])
   1.298      val unsolvable = (CType ("unsolvable", []), unsolvable_accum)
   1.299      (* typ -> term -> accumulator -> ctype * accumulator *)
   1.300 @@ -613,7 +623,7 @@
   1.301          (case t of
   1.302             Const (x as (s, T)) =>
   1.303             (case AList.lookup (op =) consts x of
   1.304 -              SOME (C, cset') => (C, (gamma, cset |> unite cset'))
   1.305 +              SOME C => (C, accum)
   1.306              | NONE =>
   1.307                if not (could_exist_alpha_subtype alpha_T T) then
   1.308                  (ctype_for T, accum)
   1.309 @@ -627,12 +637,12 @@
   1.310                | @{const_name Eps} => (print_g "*** Eps"; unsolvable)
   1.311                | @{const_name If} =>
   1.312                  do_robust_set_operation (range_type T) accum
   1.313 -                |>> curry3 CFun bool_C (S Neg)
   1.314 +                |>> curry3 CFun bool_C (S Minus)
   1.315                | @{const_name Pair} => do_pair_constr T accum
   1.316                | @{const_name fst} => do_nth_pair_sel 0 T accum
   1.317                | @{const_name snd} => do_nth_pair_sel 1 T accum 
   1.318                | @{const_name Id} =>
   1.319 -                (CFun (ctype_for (domain_type T), S Neg, bool_C), accum)
   1.320 +                (CFun (ctype_for (domain_type T), S Minus, bool_C), accum)
   1.321                | @{const_name insert} =>
   1.322                  let
   1.323                    val set_T = domain_type (range_type T)
   1.324 @@ -641,7 +651,7 @@
   1.325                    val C2 = ctype_for set_T
   1.326                    val C3 = ctype_for set_T
   1.327                  in
   1.328 -                  (CFun (C1, S Neg, CFun (C2, S Neg, C3)),
   1.329 +                  (CFun (C1, S Minus, CFun (C2, S Minus, C3)),
   1.330                     (gamma, cset |> add_ctype_is_right_unique C1
   1.331                                  |> add_is_sub_ctype C1' C3
   1.332                                  |> add_is_sub_ctype C2 C3))
   1.333 @@ -654,7 +664,7 @@
   1.334                      CFun (ctype_for (domain_type T), V x, bool_C)
   1.335                    val ab_set_C = domain_type T |> ctype_for_set
   1.336                    val ba_set_C = range_type T |> ctype_for_set
   1.337 -                in (CFun (ab_set_C, S Neg, ba_set_C), accum) end
   1.338 +                in (CFun (ab_set_C, S Minus, ba_set_C), accum) end
   1.339                | @{const_name trancl} => do_fragile_set_operation T accum
   1.340                | @{const_name rtrancl} => (print_g "*** rtrancl"; unsolvable)
   1.341                | @{const_name lower_semilattice_fun_inst.inf_fun} =>
   1.342 @@ -663,7 +673,7 @@
   1.343                  do_robust_set_operation T accum
   1.344                | @{const_name finite} =>
   1.345                  let val C1 = ctype_for (domain_type (domain_type T)) in
   1.346 -                  (CFun (pos_set_ctype_for_dom C1, S Neg, bool_C), accum)
   1.347 +                  (CFun (pos_set_ctype_for_dom C1, S Minus, bool_C), accum)
   1.348                  end
   1.349                | @{const_name rel_comp} =>
   1.350                  let
   1.351 @@ -675,7 +685,7 @@
   1.352                    val ab_set_C = domain_type (range_type T) |> ctype_for_set
   1.353                    val ac_set_C = nth_range_type 2 T |> ctype_for_set
   1.354                  in
   1.355 -                  (CFun (bc_set_C, S Neg, CFun (ab_set_C, S Neg, ac_set_C)),
   1.356 +                  (CFun (bc_set_C, S Minus, CFun (ab_set_C, S Minus, ac_set_C)),
   1.357                     accum)
   1.358                  end
   1.359                | @{const_name image} =>
   1.360 @@ -683,8 +693,8 @@
   1.361                    val a_C = ctype_for (domain_type (domain_type T))
   1.362                    val b_C = ctype_for (range_type (domain_type T))
   1.363                  in
   1.364 -                  (CFun (CFun (a_C, S Neg, b_C), S Neg,
   1.365 -                         CFun (pos_set_ctype_for_dom a_C, S Neg,
   1.366 +                  (CFun (CFun (a_C, S Minus, b_C), S Minus,
   1.367 +                         CFun (pos_set_ctype_for_dom a_C, S Minus,
   1.368                                 pos_set_ctype_for_dom b_C)), accum)
   1.369                  end
   1.370                | @{const_name Sigma} =>
   1.371 @@ -698,11 +708,11 @@
   1.372                    val b_set_C = ctype_for_set (range_type (domain_type
   1.373                                                                 (range_type T)))
   1.374                    val a_set_C = ctype_for_set a_set_T
   1.375 -                  val a_to_b_set_C = CFun (a_C, S Neg, b_set_C)
   1.376 +                  val a_to_b_set_C = CFun (a_C, S Minus, b_set_C)
   1.377                    val ab_set_C = ctype_for_set (nth_range_type 2 T)
   1.378                  in
   1.379 -                  (CFun (a_set_C, S Neg, CFun (a_to_b_set_C, S Neg, ab_set_C)),
   1.380 -                   accum)
   1.381 +                  (CFun (a_set_C, S Minus,
   1.382 +                         CFun (a_to_b_set_C, S Minus, ab_set_C)), accum)
   1.383                  end
   1.384                | @{const_name minus_fun_inst.minus_fun} =>
   1.385                  let
   1.386 @@ -710,8 +720,8 @@
   1.387                    val left_set_C = ctype_for set_T
   1.388                    val right_set_C = ctype_for set_T
   1.389                  in
   1.390 -                  (CFun (left_set_C, S Neg,
   1.391 -                         CFun (right_set_C, S Neg, left_set_C)),
   1.392 +                  (CFun (left_set_C, S Minus,
   1.393 +                         CFun (right_set_C, S Minus, left_set_C)),
   1.394                     (gamma, cset |> add_ctype_is_right_unique right_set_C
   1.395                                  |> add_is_sub_ctype right_set_C left_set_C))
   1.396                  end
   1.397 @@ -721,15 +731,15 @@
   1.398                  let
   1.399                    val a_C = ctype_for (domain_type (domain_type T))
   1.400                    val a_set_C = pos_set_ctype_for_dom a_C
   1.401 -                in (CFun (a_set_C, S Neg, a_C), accum) end
   1.402 +                in (CFun (a_set_C, S Minus, a_C), accum) end
   1.403                | @{const_name FunBox} =>
   1.404                  let val dom_C = ctype_for (domain_type T) in
   1.405 -                  (CFun (dom_C, S Neg, dom_C), accum)
   1.406 +                  (CFun (dom_C, S Minus, dom_C), accum)
   1.407                  end
   1.408                | _ => if is_sel s then
   1.409                         if constr_name_for_sel_like s = @{const_name FunBox} then
   1.410                           let val dom_C = ctype_for (domain_type T) in
   1.411 -                           (CFun (dom_C, S Neg, dom_C), accum)
   1.412 +                           (CFun (dom_C, S Minus, dom_C), accum)
   1.413                           end
   1.414                         else
   1.415                           (ctype_for_sel cdata x, accum)
   1.416 @@ -740,7 +750,10 @@
   1.417                           SOME t' => do_term t' accum
   1.418                         | NONE => (print_g ("*** built-in " ^ s); unsolvable)
   1.419                       else
   1.420 -                       (ctype_for T, accum))
   1.421 +                       let val C = ctype_for T in
   1.422 +                         (C, ({bounds = bounds, frees = frees,
   1.423 +                               consts = (x, C) :: consts}, cset))
   1.424 +                       end)
   1.425           | Free (x as (_, T)) =>
   1.426             (case AList.lookup (op =) frees x of
   1.427                SOME C => (C, accum)
   1.428 @@ -756,7 +769,7 @@
   1.429             let
   1.430               val C = ctype_for T
   1.431               val (C', accum) = do_term t' (accum |>> push_bound C)
   1.432 -           in (CFun (C, S Neg, C'), accum |>> pop_bound) end
   1.433 +           in (CFun (C, S Minus, C'), accum |>> pop_bound) end
   1.434           | Const (@{const_name All}, _)
   1.435             $ Abs (_, T', @{const "op -->"} $ (t1 $ Bound 0) $ t2) =>
   1.436             do_bounded_quantifier T' t1 t2 accum
   1.437 @@ -802,7 +815,7 @@
   1.438            fun do_quantifier quant_s abs_T body_t =
   1.439              let
   1.440                val abs_C = ctype_for abs_T
   1.441 -              val side_cond = ((sn = Neg) = (quant_s = @{const_name Ex}))
   1.442 +              val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
   1.443                val cset = cset |> side_cond ? add_ctype_is_right_total abs_C
   1.444              in
   1.445                (gamma |> push_bound abs_C, cset) |> do_co_formula body_t
   1.446 @@ -815,11 +828,11 @@
   1.447            (* term -> term -> accumulator *)
   1.448            fun do_equals t1 t2 =
   1.449              case sn of
   1.450 -              Pos => do_term t accum |> snd
   1.451 -            | Neg => let
   1.452 -                       val (C1, accum) = do_term t1 accum
   1.453 -                       val (C2, accum) = do_term t2 accum
   1.454 -                     in accum ||> add_ctypes_equal C1 C2 end
   1.455 +              Plus => do_term t accum |> snd
   1.456 +            | Minus => let
   1.457 +                         val (C1, accum) = do_term t1 accum
   1.458 +                         val (C2, accum) = do_term t2 accum
   1.459 +                       in accum ||> add_ctypes_equal C1 C2 end
   1.460          in
   1.461            case t of
   1.462              Const (s0 as @{const_name all}, _) $ Abs (_, T1, t1) =>
   1.463 @@ -876,7 +889,7 @@
   1.464  (* cdata -> term -> accumulator -> accumulator *)
   1.465  fun consider_definitional_axiom (cdata as {ext_ctxt as {thy, ...}, ...}) t =
   1.466    if not (is_constr_pattern_formula thy t) then
   1.467 -    consider_nondefinitional_axiom cdata Pos t
   1.468 +    consider_nondefinitional_axiom cdata Plus t
   1.469    else if is_harmless_axiom t then
   1.470      I
   1.471    else
   1.472 @@ -921,11 +934,11 @@
   1.473  (* theory -> literal list -> ctype_context -> unit *)
   1.474  fun print_ctype_context ctxt lits ({frees, consts, ...} : ctype_context) =
   1.475    map (fn (x, C) => string_for_ctype_of_term ctxt lits (Free x) C) frees @
   1.476 -  map (fn (x, (C, _)) => string_for_ctype_of_term ctxt lits (Const x) C) consts
   1.477 +  map (fn (x, C) => string_for_ctype_of_term ctxt lits (Const x) C) consts
   1.478    |> cat_lines |> print_g
   1.479  
   1.480 -(* extended_context -> typ -> term list -> term list -> term -> bool *)
   1.481 -fun formulas_monotonic (ext_ctxt as {ctxt, ...}) alpha_T def_ts nondef_ts
   1.482 +(* extended_context -> typ -> sign -> term list -> term list -> term -> bool *)
   1.483 +fun formulas_monotonic (ext_ctxt as {ctxt, ...}) alpha_T sn def_ts nondef_ts
   1.484                         core_t =
   1.485    let
   1.486      val _ = print_g ("****** " ^ string_for_ctype CAlpha ^ " is " ^
   1.487 @@ -934,8 +947,8 @@
   1.488      val (gamma, cset) =
   1.489        (initial_gamma, slack)
   1.490        |> fold (consider_definitional_axiom cdata) def_ts
   1.491 -      |> fold (consider_nondefinitional_axiom cdata Pos) nondef_ts
   1.492 -      |> consider_general_formula cdata Pos core_t
   1.493 +      |> fold (consider_nondefinitional_axiom cdata Plus) nondef_ts
   1.494 +      |> consider_general_formula cdata sn core_t
   1.495    in
   1.496      case solve (!max_fresh) cset of
   1.497        SOME lits => (print_ctype_context ctxt lits gamma; true)