src/HOL/Tools/ATP/atp_translate.ML
changeset 44399 cd1e32b8d4c4
parent 44398 d21f7e330ec8
child 44402 f0bc74b9161e
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     1.3 @@ -85,7 +85,6 @@
     1.4    val new_skolem_var_name_from_const : string -> string
     1.5    val atp_irrelevant_consts : string list
     1.6    val atp_schematic_consts_of : term -> typ list Symtab.table
     1.7 -  val is_locality_global : locality -> bool
     1.8    val type_enc_from_string : soundness -> string -> type_enc
     1.9    val is_type_enc_higher_order : type_enc -> bool
    1.10    val polymorphism_of_type_enc : type_enc -> polymorphism
    1.11 @@ -521,12 +520,6 @@
    1.12    General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
    1.13    Chained
    1.14  
    1.15 -(* (quasi-)underapproximation of the truth *)
    1.16 -fun is_locality_global Local = false
    1.17 -  | is_locality_global Assum = false
    1.18 -  | is_locality_global Chained = false
    1.19 -  | is_locality_global _ = true
    1.20 -
    1.21  datatype order = First_Order | Higher_Order
    1.22  datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
    1.23  datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
    1.24 @@ -673,12 +666,10 @@
    1.25  
    1.26  fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
    1.27  
    1.28 -val type_instance = Sign.typ_instance o Proof_Context.theory_of
    1.29 -
    1.30  fun insert_type ctxt get_T x xs =
    1.31    let val T = get_T x in
    1.32 -    if exists (curry (type_instance ctxt) T o get_T) xs then xs
    1.33 -    else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs
    1.34 +    if exists (type_instance ctxt T o get_T) xs then xs
    1.35 +    else x :: filter_out (type_generalization ctxt T o get_T) xs
    1.36    end
    1.37  
    1.38  (* The Booleans indicate whether all type arguments should be kept. *)
    1.39 @@ -1081,41 +1072,52 @@
    1.40  
    1.41  (** Finite and infinite type inference **)
    1.42  
    1.43 +type monotonicity_info =
    1.44 +  {maybe_finite_Ts : typ list,
    1.45 +   surely_finite_Ts : typ list,
    1.46 +   maybe_infinite_Ts : typ list,
    1.47 +   surely_infinite_Ts : typ list,
    1.48 +   maybe_nonmono_Ts : typ list}
    1.49 +
    1.50  (* These types witness that the type classes they belong to allow infinite
    1.51     models and hence that any types with these type classes is monotonic. *)
    1.52  val known_infinite_types =
    1.53    [@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}]
    1.54  
    1.55 -fun is_type_infinite ctxt soundness locality T =
    1.56 +fun is_type_surely_infinite' ctxt soundness cached_Ts T =
    1.57    (* Unlike virtually any other polymorphic fact whose type variables can be
    1.58       instantiated by a known infinite type, extensionality actually encodes a
    1.59       cardinality constraints. *)
    1.60    soundness <> Sound andalso
    1.61 -  is_type_surely_infinite ctxt
    1.62 -      (if soundness = Unsound andalso locality <> Extensionality then
    1.63 -         known_infinite_types
    1.64 -       else
    1.65 -         []) T
    1.66 +  is_type_surely_infinite ctxt (soundness = Unsound) cached_Ts T
    1.67  
    1.68  (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
    1.69     dangerous because their "exhaust" properties can easily lead to unsound ATP
    1.70     proofs. On the other hand, all HOL infinite types can be given the same
    1.71     models in first-order logic (via Löwenheim-Skolem). *)
    1.72  
    1.73 -fun should_encode_type _ _ All_Types _ = true
    1.74 -  | should_encode_type ctxt nonmono_Ts (Noninf_Nonmono_Types soundness) T =
    1.75 -    exists (curry (type_instance ctxt) T) nonmono_Ts andalso
    1.76 -    not (is_type_infinite ctxt soundness General T)
    1.77 -  | should_encode_type ctxt nonmono_Ts Fin_Nonmono_Types T =
    1.78 -    exists (curry (type_instance ctxt) T) nonmono_Ts andalso
    1.79 -    is_type_surely_finite ctxt T
    1.80 +fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true
    1.81 +  | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
    1.82 +                             maybe_nonmono_Ts, ...}
    1.83 +                       (Noninf_Nonmono_Types soundness) T =
    1.84 +    exists (type_instance ctxt T) maybe_nonmono_Ts andalso
    1.85 +    not (exists (type_instance ctxt T) surely_infinite_Ts orelse
    1.86 +         (not (member (type_aconv ctxt) maybe_finite_Ts T) andalso
    1.87 +          is_type_surely_infinite' ctxt soundness surely_infinite_Ts T))
    1.88 +  | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
    1.89 +                             maybe_nonmono_Ts, ...}
    1.90 +                       Fin_Nonmono_Types T =
    1.91 +    exists (type_instance ctxt T) maybe_nonmono_Ts andalso
    1.92 +    (exists (type_instance ctxt T) surely_finite_Ts orelse
    1.93 +     (not (member (type_aconv ctxt) maybe_infinite_Ts T) andalso
    1.94 +      is_type_surely_finite ctxt T))
    1.95    | should_encode_type _ _ _ _ = false
    1.96  
    1.97 -fun should_predicate_on_type ctxt nonmono_Ts
    1.98 -        (Guards (_, level, heaviness)) should_predicate_on_var T =
    1.99 -    (heaviness = Heavyweight orelse should_predicate_on_var ()) andalso
   1.100 -    should_encode_type ctxt nonmono_Ts level T
   1.101 -  | should_predicate_on_type _ _ _ _ _ = false
   1.102 +fun should_guard_type ctxt mono (Guards (_, level, heaviness)) should_guard_var
   1.103 +                      T =
   1.104 +    (heaviness = Heavyweight orelse should_guard_var ()) andalso
   1.105 +    should_encode_type ctxt mono level T
   1.106 +  | should_guard_type _ _ _ _ _ = false
   1.107  
   1.108  fun is_var_or_bound_var (IConst ((s, _), _, _)) =
   1.109      String.isPrefix bound_var_prefix s
   1.110 @@ -1128,19 +1130,18 @@
   1.111    Elsewhere
   1.112  
   1.113  fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
   1.114 -  | should_tag_with_type ctxt nonmono_Ts (Tags (_, level, heaviness)) site
   1.115 -                         u T =
   1.116 +  | should_tag_with_type ctxt mono (Tags (_, level, heaviness)) site u T =
   1.117      (case heaviness of
   1.118 -       Heavyweight => should_encode_type ctxt nonmono_Ts level T
   1.119 +       Heavyweight => should_encode_type ctxt mono level T
   1.120       | Lightweight =>
   1.121         case (site, is_var_or_bound_var u) of
   1.122 -         (Eq_Arg _, true) => should_encode_type ctxt nonmono_Ts level T
   1.123 +         (Eq_Arg _, true) => should_encode_type ctxt mono level T
   1.124         | _ => false)
   1.125    | should_tag_with_type _ _ _ _ _ _ = false
   1.126  
   1.127 -fun homogenized_type ctxt nonmono_Ts level =
   1.128 +fun homogenized_type ctxt mono level =
   1.129    let
   1.130 -    val should_encode = should_encode_type ctxt nonmono_Ts level
   1.131 +    val should_encode = should_encode_type ctxt mono level
   1.132      fun homo 0 T = if should_encode T then T else homo_infinite_type
   1.133        | homo ary (Type (@{type_name fun}, [T1, T2])) =
   1.134          homo 0 T1 --> homo (ary - 1) T2
   1.135 @@ -1157,8 +1158,8 @@
   1.136      fun consider_var_arity const_T var_T max_ary =
   1.137        let
   1.138          fun iter ary T =
   1.139 -          if ary = max_ary orelse type_instance ctxt (var_T, T) orelse
   1.140 -             type_instance ctxt (T, var_T) then
   1.141 +          if ary = max_ary orelse type_instance ctxt var_T T orelse
   1.142 +             type_instance ctxt T var_T then
   1.143              ary
   1.144            else
   1.145              iter (ary + 1) (range_type T)
   1.146 @@ -1574,20 +1575,20 @@
   1.147    | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
   1.148      accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
   1.149    | is_var_positively_naked_in_term _ _ _ _ = true
   1.150 -fun should_predicate_on_var_in_formula pos phi (SOME true) name =
   1.151 +fun should_guard_var_in_formula pos phi (SOME true) name =
   1.152      formula_fold pos (is_var_positively_naked_in_term name) phi false
   1.153 -  | should_predicate_on_var_in_formula _ _ _ _ = true
   1.154 +  | should_guard_var_in_formula _ _ _ _ = true
   1.155  
   1.156  fun mk_aterm format type_enc name T_args args =
   1.157    ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
   1.158  
   1.159 -fun tag_with_type ctxt format nonmono_Ts type_enc pos T tm =
   1.160 +fun tag_with_type ctxt format mono type_enc pos T tm =
   1.161    IConst (type_tag, T --> T, [T])
   1.162    |> enforce_type_arg_policy_in_iterm ctxt format type_enc
   1.163 -  |> ho_term_from_iterm ctxt format nonmono_Ts type_enc (Top_Level pos)
   1.164 +  |> ho_term_from_iterm ctxt format mono type_enc (Top_Level pos)
   1.165    |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
   1.166         | _ => raise Fail "unexpected lambda-abstraction")
   1.167 -and ho_term_from_iterm ctxt format nonmono_Ts type_enc =
   1.168 +and ho_term_from_iterm ctxt format mono type_enc =
   1.169    let
   1.170      fun aux site u =
   1.171        let
   1.172 @@ -1613,25 +1614,24 @@
   1.173            | IApp _ => raise Fail "impossible \"IApp\""
   1.174          val T = ityp_of u
   1.175        in
   1.176 -        t |> (if should_tag_with_type ctxt nonmono_Ts type_enc site u T then
   1.177 -                tag_with_type ctxt format nonmono_Ts type_enc pos T
   1.178 +        t |> (if should_tag_with_type ctxt mono type_enc site u T then
   1.179 +                tag_with_type ctxt format mono type_enc pos T
   1.180                else
   1.181                  I)
   1.182        end
   1.183    in aux end
   1.184 -and formula_from_iformula ctxt format nonmono_Ts type_enc
   1.185 -                          should_predicate_on_var =
   1.186 +and formula_from_iformula ctxt format mono type_enc should_guard_var =
   1.187    let
   1.188 -    val do_term = ho_term_from_iterm ctxt format nonmono_Ts type_enc o Top_Level
   1.189 +    val do_term = ho_term_from_iterm ctxt format mono type_enc o Top_Level
   1.190      val do_bound_type =
   1.191        case type_enc of
   1.192          Simple_Types (_, level) =>
   1.193 -        homogenized_type ctxt nonmono_Ts level 0
   1.194 +        homogenized_type ctxt mono level 0
   1.195          #> ho_type_from_typ format type_enc false 0 #> SOME
   1.196        | _ => K NONE
   1.197      fun do_out_of_bound_type pos phi universal (name, T) =
   1.198 -      if should_predicate_on_type ctxt nonmono_Ts type_enc
   1.199 -             (fn () => should_predicate_on_var pos phi universal name) T then
   1.200 +      if should_guard_type ctxt mono type_enc
   1.201 +             (fn () => should_guard_var pos phi universal name) T then
   1.202          IVar (name, T)
   1.203          |> type_guard_iterm ctxt format type_enc T
   1.204          |> do_term pos |> AAtom |> SOME
   1.205 @@ -1663,13 +1663,13 @@
   1.206  (* Each fact is given a unique fact number to avoid name clashes (e.g., because
   1.207     of monomorphization). The TPTP explicitly forbids name clashes, and some of
   1.208     the remote provers might care. *)
   1.209 -fun formula_line_for_fact ctxt format prefix encode freshen pos nonmono_Ts
   1.210 -        type_enc (j, {name, locality, kind, iformula, atomic_types}) =
   1.211 +fun formula_line_for_fact ctxt format prefix encode freshen pos mono type_enc
   1.212 +                          (j, {name, locality, kind, iformula, atomic_types}) =
   1.213    (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind,
   1.214     iformula
   1.215     |> close_iformula_universally
   1.216 -   |> formula_from_iformula ctxt format nonmono_Ts type_enc
   1.217 -                            should_predicate_on_var_in_formula
   1.218 +   |> formula_from_iformula ctxt format mono type_enc
   1.219 +                            should_guard_var_in_formula
   1.220                              (if pos then SOME true else NONE)
   1.221     |> bound_tvars type_enc atomic_types
   1.222     |> close_formula_universally,
   1.223 @@ -1704,11 +1704,11 @@
   1.224                           (fo_literal_from_arity_literal concl_lits))
   1.225             |> close_formula_universally, isabelle_info introN, NONE)
   1.226  
   1.227 -fun formula_line_for_conjecture ctxt format nonmono_Ts type_enc
   1.228 +fun formula_line_for_conjecture ctxt format mono type_enc
   1.229          ({name, kind, iformula, atomic_types, ...} : translated_formula) =
   1.230    Formula (conjecture_prefix ^ name, kind,
   1.231 -           formula_from_iformula ctxt format nonmono_Ts type_enc
   1.232 -               should_predicate_on_var_in_formula (SOME false)
   1.233 +           formula_from_iformula ctxt format mono type_enc
   1.234 +               should_guard_var_in_formula (SOME false)
   1.235                 (close_iformula_universally iformula)
   1.236             |> bound_tvars type_enc atomic_types
   1.237             |> close_formula_universally, NONE, NONE)
   1.238 @@ -1785,48 +1785,80 @@
   1.239                | _ => fold add_undefined_const (var_types ())))
   1.240    end
   1.241  
   1.242 +(* We add "bool" in case the helper "True_or_False" is included later. *)
   1.243 +val default_mono =
   1.244 +  {maybe_finite_Ts = [@{typ bool}],
   1.245 +   surely_finite_Ts = [@{typ bool}],
   1.246 +   maybe_infinite_Ts = known_infinite_types,
   1.247 +   surely_infinite_Ts = known_infinite_types,
   1.248 +   maybe_nonmono_Ts = [@{typ bool}]}
   1.249 +
   1.250  (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
   1.251     out with monotonicity" paper presented at CADE 2011. *)
   1.252 -fun add_iterm_nonmonotonic_types _ _ _ (SOME false) _ = I
   1.253 -  | add_iterm_nonmonotonic_types ctxt level locality _
   1.254 -        (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) =
   1.255 -    (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
   1.256 -     (case level of
   1.257 +fun add_iterm_mononotonicity_info _ _ (SOME false) _ mono = mono
   1.258 +  | add_iterm_mononotonicity_info ctxt level _
   1.259 +        (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2))
   1.260 +        (mono as {maybe_finite_Ts, surely_finite_Ts, maybe_infinite_Ts,
   1.261 +                  surely_infinite_Ts, maybe_nonmono_Ts}) =
   1.262 +    if is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] then
   1.263 +      case level of
   1.264          Noninf_Nonmono_Types soundness =>
   1.265 -        (* The second conjunct about globality is not strictly necessary, but it
   1.266 -           helps prevent finding proofs that are only sound "modulo
   1.267 -           infiniteness". For example, if the conjecture is
   1.268 -           "EX x y::nat. x ~= y", its untyped negation "ALL x y. x = y" would
   1.269 -           lead to a nonsensical proof that we can't replay. *)
   1.270 -        not (is_type_infinite ctxt soundness locality T
   1.271 -             (* andalso is_locality_global locality *))
   1.272 -      | Fin_Nonmono_Types => is_type_surely_finite ctxt T
   1.273 -      | _ => true)) ? insert_type ctxt I T
   1.274 -  | add_iterm_nonmonotonic_types _ _ _ _ _ = I
   1.275 -fun add_fact_nonmonotonic_types ctxt level
   1.276 -        ({kind, locality, iformula, ...} : translated_formula) =
   1.277 +        if exists (type_instance ctxt T) surely_infinite_Ts orelse
   1.278 +           member (type_aconv ctxt) maybe_finite_Ts T then
   1.279 +          mono
   1.280 +        else if is_type_surely_infinite' ctxt soundness surely_infinite_Ts
   1.281 +                                         T then
   1.282 +          {maybe_finite_Ts = maybe_finite_Ts,
   1.283 +           surely_finite_Ts = surely_finite_Ts,
   1.284 +           maybe_infinite_Ts = maybe_infinite_Ts,
   1.285 +           surely_infinite_Ts = surely_infinite_Ts |> insert_type ctxt I T,
   1.286 +           maybe_nonmono_Ts = maybe_nonmono_Ts}
   1.287 +        else
   1.288 +          {maybe_finite_Ts = maybe_finite_Ts |> insert (type_aconv ctxt) T,
   1.289 +           surely_finite_Ts = surely_finite_Ts,
   1.290 +           maybe_infinite_Ts = maybe_infinite_Ts,
   1.291 +           surely_infinite_Ts = surely_infinite_Ts,
   1.292 +           maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
   1.293 +      | Fin_Nonmono_Types =>
   1.294 +        if exists (type_instance ctxt T) surely_finite_Ts orelse
   1.295 +           member (type_aconv ctxt) maybe_infinite_Ts T then
   1.296 +          mono
   1.297 +        else if is_type_surely_finite ctxt T then
   1.298 +          {maybe_finite_Ts = maybe_finite_Ts,
   1.299 +           surely_finite_Ts = surely_finite_Ts |> insert_type ctxt I T,
   1.300 +           maybe_infinite_Ts = maybe_infinite_Ts,
   1.301 +           surely_infinite_Ts = surely_infinite_Ts,
   1.302 +           maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
   1.303 +        else
   1.304 +          {maybe_finite_Ts = maybe_finite_Ts,
   1.305 +           surely_finite_Ts = surely_finite_Ts,
   1.306 +           maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_aconv ctxt) T,
   1.307 +           surely_infinite_Ts = surely_infinite_Ts,
   1.308 +           maybe_nonmono_Ts = maybe_nonmono_Ts}
   1.309 +      | _ => mono
   1.310 +    else
   1.311 +      mono
   1.312 +  | add_iterm_mononotonicity_info _ _ _ _ mono = mono
   1.313 +fun add_fact_mononotonicity_info ctxt level
   1.314 +        ({kind, iformula, ...} : translated_formula) =
   1.315    formula_fold (SOME (kind <> Conjecture))
   1.316 -               (add_iterm_nonmonotonic_types ctxt level locality) iformula
   1.317 -fun nonmonotonic_types_for_facts ctxt type_enc facts =
   1.318 +               (add_iterm_mononotonicity_info ctxt level) iformula
   1.319 +fun mononotonicity_info_for_facts ctxt type_enc facts =
   1.320    let val level = level_of_type_enc type_enc in
   1.321 -    if is_type_level_monotonicity_based level then
   1.322 -      [] |> fold (add_fact_nonmonotonic_types ctxt level) facts
   1.323 -         (* We must add "bool" in case the helper "True_or_False" is added
   1.324 -            later. *)
   1.325 -         |> insert_type ctxt I @{typ bool}
   1.326 -    else
   1.327 -      []
   1.328 +    default_mono
   1.329 +    |> is_type_level_monotonicity_based level
   1.330 +       ? fold (add_fact_mononotonicity_info ctxt level) facts
   1.331    end
   1.332  
   1.333  (* FIXME: do the right thing for existentials! *)
   1.334 -fun formula_line_for_guards_mono_type ctxt format nonmono_Ts type_enc T =
   1.335 +fun formula_line_for_guards_mono_type ctxt format mono type_enc T =
   1.336    Formula (guards_sym_formula_prefix ^
   1.337             ascii_of (mangled_type format type_enc T),
   1.338             Axiom,
   1.339             IConst (`make_bound_var "X", T, [])
   1.340             |> type_guard_iterm ctxt format type_enc T
   1.341             |> AAtom
   1.342 -           |> formula_from_iformula ctxt format nonmono_Ts type_enc
   1.343 +           |> formula_from_iformula ctxt format mono type_enc
   1.344                                      (K (K (K (K true)))) (SOME true)
   1.345             |> bound_tvars type_enc (atyps_of T)
   1.346             |> close_formula_universally,
   1.347 @@ -1838,27 +1870,25 @@
   1.348    |> bound_tvars type_enc atomic_Ts
   1.349    |> close_formula_universally
   1.350  
   1.351 -fun formula_line_for_tags_mono_type ctxt format nonmono_Ts type_enc T =
   1.352 +fun formula_line_for_tags_mono_type ctxt format mono type_enc T =
   1.353    let val x_var = ATerm (`make_bound_var "X", []) in
   1.354      Formula (tags_sym_formula_prefix ^
   1.355               ascii_of (mangled_type format type_enc T),
   1.356               Axiom,
   1.357               eq_formula type_enc (atyps_of T) false
   1.358 -                        (tag_with_type ctxt format nonmono_Ts type_enc NONE T
   1.359 -                                       x_var)
   1.360 +                        (tag_with_type ctxt format mono type_enc NONE T x_var)
   1.361                          x_var,
   1.362               isabelle_info simpN, NONE)
   1.363    end
   1.364  
   1.365 -fun problem_lines_for_mono_types ctxt format nonmono_Ts type_enc Ts =
   1.366 +fun problem_lines_for_mono_types ctxt format mono type_enc Ts =
   1.367    case type_enc of
   1.368      Simple_Types _ => []
   1.369    | Guards _ =>
   1.370 -    map (formula_line_for_guards_mono_type ctxt format nonmono_Ts type_enc) Ts
   1.371 -  | Tags _ =>
   1.372 -    map (formula_line_for_tags_mono_type ctxt format nonmono_Ts type_enc) Ts
   1.373 +    map (formula_line_for_guards_mono_type ctxt format mono type_enc) Ts
   1.374 +  | Tags _ => map (formula_line_for_tags_mono_type ctxt format mono type_enc) Ts
   1.375  
   1.376 -fun decl_line_for_sym ctxt format nonmono_Ts type_enc s
   1.377 +fun decl_line_for_sym ctxt format mono type_enc s
   1.378                        (s', T_args, T, pred_sym, ary, _) =
   1.379    let
   1.380      val (T_arg_Ts, level) =
   1.381 @@ -1867,12 +1897,12 @@
   1.382        | _ => (replicate (length T_args) homo_infinite_type, No_Types)
   1.383    in
   1.384      Decl (sym_decl_prefix ^ s, (s, s'),
   1.385 -          (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
   1.386 +          (T_arg_Ts ---> (T |> homogenized_type ctxt mono level ary))
   1.387            |> ho_type_from_typ format type_enc pred_sym (length T_arg_Ts + ary))
   1.388    end
   1.389  
   1.390 -fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind nonmono_Ts
   1.391 -        type_enc n s j (s', T_args, T, _, ary, in_conj) =
   1.392 +fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono type_enc n s
   1.393 +                                     j (s', T_args, T, _, ary, in_conj) =
   1.394    let
   1.395      val (kind, maybe_negate) =
   1.396        if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
   1.397 @@ -1886,7 +1916,7 @@
   1.398      val sym_needs_arg_types = exists (curry (op =) dummyT) T_args
   1.399      fun should_keep_arg_type T =
   1.400        sym_needs_arg_types andalso
   1.401 -      should_predicate_on_type ctxt nonmono_Ts type_enc (K true) T
   1.402 +      should_guard_type ctxt mono type_enc (K true) T
   1.403      val bound_Ts =
   1.404        arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE)
   1.405    in
   1.406 @@ -1896,7 +1926,7 @@
   1.407               |> fold (curry (IApp o swap)) bounds
   1.408               |> type_guard_iterm ctxt format type_enc res_T
   1.409               |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
   1.410 -             |> formula_from_iformula ctxt format nonmono_Ts type_enc
   1.411 +             |> formula_from_iformula ctxt format mono type_enc
   1.412                                        (K (K (K (K true)))) (SOME true)
   1.413               |> n > 1 ? bound_tvars type_enc (atyps_of T)
   1.414               |> close_formula_universally
   1.415 @@ -1904,8 +1934,8 @@
   1.416               isabelle_info introN, NONE)
   1.417    end
   1.418  
   1.419 -fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind
   1.420 -        nonmono_Ts type_enc n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
   1.421 +fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind mono
   1.422 +        type_enc n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
   1.423    let
   1.424      val ident_base =
   1.425        tags_sym_formula_prefix ^ s ^
   1.426 @@ -1920,8 +1950,8 @@
   1.427      val cst = mk_aterm format type_enc (s, s') T_args
   1.428      val eq = maybe_negate oo eq_formula type_enc (atyps_of T) pred_sym
   1.429      val should_encode =
   1.430 -      should_encode_type ctxt nonmono_Ts (level_of_type_enc type_enc)
   1.431 -    val tag_with = tag_with_type ctxt format nonmono_Ts type_enc NONE
   1.432 +      should_encode_type ctxt mono (level_of_type_enc type_enc)
   1.433 +    val tag_with = tag_with_type ctxt format mono type_enc NONE
   1.434      val add_formula_for_res =
   1.435        if should_encode res_T then
   1.436          cons (Formula (ident_base ^ "_res", kind,
   1.437 @@ -1949,19 +1979,19 @@
   1.438  
   1.439  fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
   1.440  
   1.441 -fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts type_enc
   1.442 +fun problem_lines_for_sym_decls ctxt format conj_sym_kind mono type_enc
   1.443                                  (s, decls) =
   1.444    case type_enc of
   1.445      Simple_Types _ =>
   1.446 -    decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_enc s)
   1.447 +    decls |> map (decl_line_for_sym ctxt format mono type_enc s)
   1.448    | Guards (_, level, _) =>
   1.449      let
   1.450        val decls =
   1.451          case decls of
   1.452            decl :: (decls' as _ :: _) =>
   1.453            let val T = result_type_of_decl decl in
   1.454 -            if forall (curry (type_instance ctxt o swap) T
   1.455 -                       o result_type_of_decl) decls' then
   1.456 +            if forall (type_generalization ctxt T o result_type_of_decl)
   1.457 +                      decls' then
   1.458                [decl]
   1.459              else
   1.460                decls
   1.461 @@ -1969,12 +1999,12 @@
   1.462          | _ => decls
   1.463        val n = length decls
   1.464        val decls =
   1.465 -        decls |> filter (should_encode_type ctxt nonmono_Ts level
   1.466 +        decls |> filter (should_encode_type ctxt mono level
   1.467                           o result_type_of_decl)
   1.468      in
   1.469        (0 upto length decls - 1, decls)
   1.470 -      |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind
   1.471 -                                                 nonmono_Ts type_enc n s)
   1.472 +      |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono
   1.473 +                                                 type_enc n s)
   1.474      end
   1.475    | Tags (_, _, heaviness) =>
   1.476      (case heaviness of
   1.477 @@ -1983,26 +2013,26 @@
   1.478         let val n = length decls in
   1.479           (0 upto n - 1 ~~ decls)
   1.480           |> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format
   1.481 -                      conj_sym_kind nonmono_Ts type_enc n s)
   1.482 +                      conj_sym_kind mono type_enc n s)
   1.483         end)
   1.484  
   1.485 -fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
   1.486 -                                     type_enc sym_decl_tab =
   1.487 +fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc
   1.488 +                                     sym_decl_tab =
   1.489    let
   1.490      val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
   1.491      val mono_Ts =
   1.492        if polymorphism_of_type_enc type_enc = Polymorphic then
   1.493          syms |> maps (map result_type_of_decl o snd)
   1.494 -             |> filter_out (should_encode_type ctxt nonmono_Ts
   1.495 +             |> filter_out (should_encode_type ctxt mono
   1.496                                  (level_of_type_enc type_enc))
   1.497               |> rpair [] |-> fold (insert_type ctxt I)
   1.498        else
   1.499          []
   1.500      val mono_lines =
   1.501 -      problem_lines_for_mono_types ctxt format nonmono_Ts type_enc mono_Ts
   1.502 +      problem_lines_for_mono_types ctxt format mono type_enc mono_Ts
   1.503      val decl_lines =
   1.504        fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
   1.505 -                                                     nonmono_Ts type_enc)
   1.506 +                                                     mono type_enc)
   1.507                 syms []
   1.508    in mono_lines @ decl_lines end
   1.509  
   1.510 @@ -2063,7 +2093,7 @@
   1.511        translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
   1.512                           hyp_ts concl_t facts
   1.513      val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
   1.514 -    val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_enc
   1.515 +    val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
   1.516      val repair = repair_fact ctxt format type_enc sym_tab
   1.517      val (conjs, facts) = (conjs, facts) |> pairself (map repair)
   1.518      val repaired_sym_tab =
   1.519 @@ -2074,12 +2104,12 @@
   1.520      val sym_decl_lines =
   1.521        (conjs, helpers @ facts)
   1.522        |> sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
   1.523 -      |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
   1.524 +      |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
   1.525                                                 type_enc
   1.526      val helper_lines =
   1.527        0 upto length helpers - 1 ~~ helpers
   1.528 -      |> map (formula_line_for_fact ctxt format helper_prefix I false true
   1.529 -                                    nonmono_Ts type_enc)
   1.530 +      |> map (formula_line_for_fact ctxt format helper_prefix I false true mono
   1.531 +                                    type_enc)
   1.532        |> (if needs_type_tag_idempotence type_enc then
   1.533              cons (type_tag_idempotence_fact ())
   1.534            else
   1.535 @@ -2090,15 +2120,14 @@
   1.536        [(explicit_declsN, sym_decl_lines),
   1.537         (factsN,
   1.538          map (formula_line_for_fact ctxt format fact_prefix ascii_of
   1.539 -                                   (not exporter) (not exporter) nonmono_Ts
   1.540 +                                   (not exporter) (not exporter) mono
   1.541                                     type_enc)
   1.542              (0 upto length facts - 1 ~~ facts)),
   1.543         (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
   1.544         (aritiesN, map formula_line_for_arity_clause arity_clauses),
   1.545         (helpersN, helper_lines),
   1.546         (conjsN,
   1.547 -        map (formula_line_for_conjecture ctxt format nonmono_Ts type_enc)
   1.548 -            conjs),
   1.549 +        map (formula_line_for_conjecture ctxt format mono type_enc) conjs),
   1.550         (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs))]
   1.551      val problem =
   1.552        problem