src/HOL/Tools/ATP/atp_translate.ML
changeset 44399 cd1e32b8d4c4
parent 44398 d21f7e330ec8
child 44402 f0bc74b9161e
--- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
@@ -85,7 +85,6 @@
   val new_skolem_var_name_from_const : string -> string
   val atp_irrelevant_consts : string list
   val atp_schematic_consts_of : term -> typ list Symtab.table
-  val is_locality_global : locality -> bool
   val type_enc_from_string : soundness -> string -> type_enc
   val is_type_enc_higher_order : type_enc -> bool
   val polymorphism_of_type_enc : type_enc -> polymorphism
@@ -521,12 +520,6 @@
   General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
   Chained
 
-(* (quasi-)underapproximation of the truth *)
-fun is_locality_global Local = false
-  | is_locality_global Assum = false
-  | is_locality_global Chained = false
-  | is_locality_global _ = true
-
 datatype order = First_Order | Higher_Order
 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
 datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
@@ -673,12 +666,10 @@
 
 fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
 
-val type_instance = Sign.typ_instance o Proof_Context.theory_of
-
 fun insert_type ctxt get_T x xs =
   let val T = get_T x in
-    if exists (curry (type_instance ctxt) T o get_T) xs then xs
-    else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs
+    if exists (type_instance ctxt T o get_T) xs then xs
+    else x :: filter_out (type_generalization ctxt T o get_T) xs
   end
 
 (* The Booleans indicate whether all type arguments should be kept. *)
@@ -1081,41 +1072,52 @@
 
 (** Finite and infinite type inference **)
 
+type monotonicity_info =
+  {maybe_finite_Ts : typ list,
+   surely_finite_Ts : typ list,
+   maybe_infinite_Ts : typ list,
+   surely_infinite_Ts : typ list,
+   maybe_nonmono_Ts : typ list}
+
 (* These types witness that the type classes they belong to allow infinite
    models and hence that any types with these type classes is monotonic. *)
 val known_infinite_types =
   [@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}]
 
-fun is_type_infinite ctxt soundness locality T =
+fun is_type_surely_infinite' ctxt soundness cached_Ts T =
   (* Unlike virtually any other polymorphic fact whose type variables can be
      instantiated by a known infinite type, extensionality actually encodes a
      cardinality constraints. *)
   soundness <> Sound andalso
-  is_type_surely_infinite ctxt
-      (if soundness = Unsound andalso locality <> Extensionality then
-         known_infinite_types
-       else
-         []) T
+  is_type_surely_infinite ctxt (soundness = Unsound) cached_Ts T
 
 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
    dangerous because their "exhaust" properties can easily lead to unsound ATP
    proofs. On the other hand, all HOL infinite types can be given the same
    models in first-order logic (via Löwenheim-Skolem). *)
 
-fun should_encode_type _ _ All_Types _ = true
-  | should_encode_type ctxt nonmono_Ts (Noninf_Nonmono_Types soundness) T =
-    exists (curry (type_instance ctxt) T) nonmono_Ts andalso
-    not (is_type_infinite ctxt soundness General T)
-  | should_encode_type ctxt nonmono_Ts Fin_Nonmono_Types T =
-    exists (curry (type_instance ctxt) T) nonmono_Ts andalso
-    is_type_surely_finite ctxt T
+fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true
+  | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
+                             maybe_nonmono_Ts, ...}
+                       (Noninf_Nonmono_Types soundness) T =
+    exists (type_instance ctxt T) maybe_nonmono_Ts andalso
+    not (exists (type_instance ctxt T) surely_infinite_Ts orelse
+         (not (member (type_aconv ctxt) maybe_finite_Ts T) andalso
+          is_type_surely_infinite' ctxt soundness surely_infinite_Ts T))
+  | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
+                             maybe_nonmono_Ts, ...}
+                       Fin_Nonmono_Types T =
+    exists (type_instance ctxt T) maybe_nonmono_Ts andalso
+    (exists (type_instance ctxt T) surely_finite_Ts orelse
+     (not (member (type_aconv ctxt) maybe_infinite_Ts T) andalso
+      is_type_surely_finite ctxt T))
   | should_encode_type _ _ _ _ = false
 
-fun should_predicate_on_type ctxt nonmono_Ts
-        (Guards (_, level, heaviness)) should_predicate_on_var T =
-    (heaviness = Heavyweight orelse should_predicate_on_var ()) andalso
-    should_encode_type ctxt nonmono_Ts level T
-  | should_predicate_on_type _ _ _ _ _ = false
+fun should_guard_type ctxt mono (Guards (_, level, heaviness)) should_guard_var
+                      T =
+    (heaviness = Heavyweight orelse should_guard_var ()) andalso
+    should_encode_type ctxt mono level T
+  | should_guard_type _ _ _ _ _ = false
 
 fun is_var_or_bound_var (IConst ((s, _), _, _)) =
     String.isPrefix bound_var_prefix s
@@ -1128,19 +1130,18 @@
   Elsewhere
 
 fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
-  | should_tag_with_type ctxt nonmono_Ts (Tags (_, level, heaviness)) site
-                         u T =
+  | should_tag_with_type ctxt mono (Tags (_, level, heaviness)) site u T =
     (case heaviness of
-       Heavyweight => should_encode_type ctxt nonmono_Ts level T
+       Heavyweight => should_encode_type ctxt mono level T
      | Lightweight =>
        case (site, is_var_or_bound_var u) of
-         (Eq_Arg _, true) => should_encode_type ctxt nonmono_Ts level T
+         (Eq_Arg _, true) => should_encode_type ctxt mono level T
        | _ => false)
   | should_tag_with_type _ _ _ _ _ _ = false
 
-fun homogenized_type ctxt nonmono_Ts level =
+fun homogenized_type ctxt mono level =
   let
-    val should_encode = should_encode_type ctxt nonmono_Ts level
+    val should_encode = should_encode_type ctxt mono level
     fun homo 0 T = if should_encode T then T else homo_infinite_type
       | homo ary (Type (@{type_name fun}, [T1, T2])) =
         homo 0 T1 --> homo (ary - 1) T2
@@ -1157,8 +1158,8 @@
     fun consider_var_arity const_T var_T max_ary =
       let
         fun iter ary T =
-          if ary = max_ary orelse type_instance ctxt (var_T, T) orelse
-             type_instance ctxt (T, var_T) then
+          if ary = max_ary orelse type_instance ctxt var_T T orelse
+             type_instance ctxt T var_T then
             ary
           else
             iter (ary + 1) (range_type T)
@@ -1574,20 +1575,20 @@
   | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
     accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
   | is_var_positively_naked_in_term _ _ _ _ = true
-fun should_predicate_on_var_in_formula pos phi (SOME true) name =
+fun should_guard_var_in_formula pos phi (SOME true) name =
     formula_fold pos (is_var_positively_naked_in_term name) phi false
-  | should_predicate_on_var_in_formula _ _ _ _ = true
+  | should_guard_var_in_formula _ _ _ _ = true
 
 fun mk_aterm format type_enc name T_args args =
   ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
 
-fun tag_with_type ctxt format nonmono_Ts type_enc pos T tm =
+fun tag_with_type ctxt format mono type_enc pos T tm =
   IConst (type_tag, T --> T, [T])
   |> enforce_type_arg_policy_in_iterm ctxt format type_enc
-  |> ho_term_from_iterm ctxt format nonmono_Ts type_enc (Top_Level pos)
+  |> ho_term_from_iterm ctxt format mono type_enc (Top_Level pos)
   |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
        | _ => raise Fail "unexpected lambda-abstraction")
-and ho_term_from_iterm ctxt format nonmono_Ts type_enc =
+and ho_term_from_iterm ctxt format mono type_enc =
   let
     fun aux site u =
       let
@@ -1613,25 +1614,24 @@
           | IApp _ => raise Fail "impossible \"IApp\""
         val T = ityp_of u
       in
-        t |> (if should_tag_with_type ctxt nonmono_Ts type_enc site u T then
-                tag_with_type ctxt format nonmono_Ts type_enc pos T
+        t |> (if should_tag_with_type ctxt mono type_enc site u T then
+                tag_with_type ctxt format mono type_enc pos T
               else
                 I)
       end
   in aux end
-and formula_from_iformula ctxt format nonmono_Ts type_enc
-                          should_predicate_on_var =
+and formula_from_iformula ctxt format mono type_enc should_guard_var =
   let
-    val do_term = ho_term_from_iterm ctxt format nonmono_Ts type_enc o Top_Level
+    val do_term = ho_term_from_iterm ctxt format mono type_enc o Top_Level
     val do_bound_type =
       case type_enc of
         Simple_Types (_, level) =>
-        homogenized_type ctxt nonmono_Ts level 0
+        homogenized_type ctxt mono level 0
         #> ho_type_from_typ format type_enc false 0 #> SOME
       | _ => K NONE
     fun do_out_of_bound_type pos phi universal (name, T) =
-      if should_predicate_on_type ctxt nonmono_Ts type_enc
-             (fn () => should_predicate_on_var pos phi universal name) T then
+      if should_guard_type ctxt mono type_enc
+             (fn () => should_guard_var pos phi universal name) T then
         IVar (name, T)
         |> type_guard_iterm ctxt format type_enc T
         |> do_term pos |> AAtom |> SOME
@@ -1663,13 +1663,13 @@
 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
    of monomorphization). The TPTP explicitly forbids name clashes, and some of
    the remote provers might care. *)
-fun formula_line_for_fact ctxt format prefix encode freshen pos nonmono_Ts
-        type_enc (j, {name, locality, kind, iformula, atomic_types}) =
+fun formula_line_for_fact ctxt format prefix encode freshen pos mono type_enc
+                          (j, {name, locality, kind, iformula, atomic_types}) =
   (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind,
    iformula
    |> close_iformula_universally
-   |> formula_from_iformula ctxt format nonmono_Ts type_enc
-                            should_predicate_on_var_in_formula
+   |> formula_from_iformula ctxt format mono type_enc
+                            should_guard_var_in_formula
                             (if pos then SOME true else NONE)
    |> bound_tvars type_enc atomic_types
    |> close_formula_universally,
@@ -1704,11 +1704,11 @@
                          (fo_literal_from_arity_literal concl_lits))
            |> close_formula_universally, isabelle_info introN, NONE)
 
-fun formula_line_for_conjecture ctxt format nonmono_Ts type_enc
+fun formula_line_for_conjecture ctxt format mono type_enc
         ({name, kind, iformula, atomic_types, ...} : translated_formula) =
   Formula (conjecture_prefix ^ name, kind,
-           formula_from_iformula ctxt format nonmono_Ts type_enc
-               should_predicate_on_var_in_formula (SOME false)
+           formula_from_iformula ctxt format mono type_enc
+               should_guard_var_in_formula (SOME false)
                (close_iformula_universally iformula)
            |> bound_tvars type_enc atomic_types
            |> close_formula_universally, NONE, NONE)
@@ -1785,48 +1785,80 @@
               | _ => fold add_undefined_const (var_types ())))
   end
 
+(* We add "bool" in case the helper "True_or_False" is included later. *)
+val default_mono =
+  {maybe_finite_Ts = [@{typ bool}],
+   surely_finite_Ts = [@{typ bool}],
+   maybe_infinite_Ts = known_infinite_types,
+   surely_infinite_Ts = known_infinite_types,
+   maybe_nonmono_Ts = [@{typ bool}]}
+
 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
    out with monotonicity" paper presented at CADE 2011. *)
-fun add_iterm_nonmonotonic_types _ _ _ (SOME false) _ = I
-  | add_iterm_nonmonotonic_types ctxt level locality _
-        (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) =
-    (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
-     (case level of
+fun add_iterm_mononotonicity_info _ _ (SOME false) _ mono = mono
+  | add_iterm_mononotonicity_info ctxt level _
+        (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2))
+        (mono as {maybe_finite_Ts, surely_finite_Ts, maybe_infinite_Ts,
+                  surely_infinite_Ts, maybe_nonmono_Ts}) =
+    if is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] then
+      case level of
         Noninf_Nonmono_Types soundness =>
-        (* The second conjunct about globality is not strictly necessary, but it
-           helps prevent finding proofs that are only sound "modulo
-           infiniteness". For example, if the conjecture is
-           "EX x y::nat. x ~= y", its untyped negation "ALL x y. x = y" would
-           lead to a nonsensical proof that we can't replay. *)
-        not (is_type_infinite ctxt soundness locality T
-             (* andalso is_locality_global locality *))
-      | Fin_Nonmono_Types => is_type_surely_finite ctxt T
-      | _ => true)) ? insert_type ctxt I T
-  | add_iterm_nonmonotonic_types _ _ _ _ _ = I
-fun add_fact_nonmonotonic_types ctxt level
-        ({kind, locality, iformula, ...} : translated_formula) =
+        if exists (type_instance ctxt T) surely_infinite_Ts orelse
+           member (type_aconv ctxt) maybe_finite_Ts T then
+          mono
+        else if is_type_surely_infinite' ctxt soundness surely_infinite_Ts
+                                         T then
+          {maybe_finite_Ts = maybe_finite_Ts,
+           surely_finite_Ts = surely_finite_Ts,
+           maybe_infinite_Ts = maybe_infinite_Ts,
+           surely_infinite_Ts = surely_infinite_Ts |> insert_type ctxt I T,
+           maybe_nonmono_Ts = maybe_nonmono_Ts}
+        else
+          {maybe_finite_Ts = maybe_finite_Ts |> insert (type_aconv ctxt) T,
+           surely_finite_Ts = surely_finite_Ts,
+           maybe_infinite_Ts = maybe_infinite_Ts,
+           surely_infinite_Ts = surely_infinite_Ts,
+           maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
+      | Fin_Nonmono_Types =>
+        if exists (type_instance ctxt T) surely_finite_Ts orelse
+           member (type_aconv ctxt) maybe_infinite_Ts T then
+          mono
+        else if is_type_surely_finite ctxt T then
+          {maybe_finite_Ts = maybe_finite_Ts,
+           surely_finite_Ts = surely_finite_Ts |> insert_type ctxt I T,
+           maybe_infinite_Ts = maybe_infinite_Ts,
+           surely_infinite_Ts = surely_infinite_Ts,
+           maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
+        else
+          {maybe_finite_Ts = maybe_finite_Ts,
+           surely_finite_Ts = surely_finite_Ts,
+           maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_aconv ctxt) T,
+           surely_infinite_Ts = surely_infinite_Ts,
+           maybe_nonmono_Ts = maybe_nonmono_Ts}
+      | _ => mono
+    else
+      mono
+  | add_iterm_mononotonicity_info _ _ _ _ mono = mono
+fun add_fact_mononotonicity_info ctxt level
+        ({kind, iformula, ...} : translated_formula) =
   formula_fold (SOME (kind <> Conjecture))
-               (add_iterm_nonmonotonic_types ctxt level locality) iformula
-fun nonmonotonic_types_for_facts ctxt type_enc facts =
+               (add_iterm_mononotonicity_info ctxt level) iformula
+fun mononotonicity_info_for_facts ctxt type_enc facts =
   let val level = level_of_type_enc type_enc in
-    if is_type_level_monotonicity_based level then
-      [] |> fold (add_fact_nonmonotonic_types ctxt level) facts
-         (* We must add "bool" in case the helper "True_or_False" is added
-            later. *)
-         |> insert_type ctxt I @{typ bool}
-    else
-      []
+    default_mono
+    |> is_type_level_monotonicity_based level
+       ? fold (add_fact_mononotonicity_info ctxt level) facts
   end
 
 (* FIXME: do the right thing for existentials! *)
-fun formula_line_for_guards_mono_type ctxt format nonmono_Ts type_enc T =
+fun formula_line_for_guards_mono_type ctxt format mono type_enc T =
   Formula (guards_sym_formula_prefix ^
            ascii_of (mangled_type format type_enc T),
            Axiom,
            IConst (`make_bound_var "X", T, [])
            |> type_guard_iterm ctxt format type_enc T
            |> AAtom
-           |> formula_from_iformula ctxt format nonmono_Ts type_enc
+           |> formula_from_iformula ctxt format mono type_enc
                                     (K (K (K (K true)))) (SOME true)
            |> bound_tvars type_enc (atyps_of T)
            |> close_formula_universally,
@@ -1838,27 +1870,25 @@
   |> bound_tvars type_enc atomic_Ts
   |> close_formula_universally
 
-fun formula_line_for_tags_mono_type ctxt format nonmono_Ts type_enc T =
+fun formula_line_for_tags_mono_type ctxt format mono type_enc T =
   let val x_var = ATerm (`make_bound_var "X", []) in
     Formula (tags_sym_formula_prefix ^
              ascii_of (mangled_type format type_enc T),
              Axiom,
              eq_formula type_enc (atyps_of T) false
-                        (tag_with_type ctxt format nonmono_Ts type_enc NONE T
-                                       x_var)
+                        (tag_with_type ctxt format mono type_enc NONE T x_var)
                         x_var,
              isabelle_info simpN, NONE)
   end
 
-fun problem_lines_for_mono_types ctxt format nonmono_Ts type_enc Ts =
+fun problem_lines_for_mono_types ctxt format mono type_enc Ts =
   case type_enc of
     Simple_Types _ => []
   | Guards _ =>
-    map (formula_line_for_guards_mono_type ctxt format nonmono_Ts type_enc) Ts
-  | Tags _ =>
-    map (formula_line_for_tags_mono_type ctxt format nonmono_Ts type_enc) Ts
+    map (formula_line_for_guards_mono_type ctxt format mono type_enc) Ts
+  | Tags _ => map (formula_line_for_tags_mono_type ctxt format mono type_enc) Ts
 
-fun decl_line_for_sym ctxt format nonmono_Ts type_enc s
+fun decl_line_for_sym ctxt format mono type_enc s
                       (s', T_args, T, pred_sym, ary, _) =
   let
     val (T_arg_Ts, level) =
@@ -1867,12 +1897,12 @@
       | _ => (replicate (length T_args) homo_infinite_type, No_Types)
   in
     Decl (sym_decl_prefix ^ s, (s, s'),
-          (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
+          (T_arg_Ts ---> (T |> homogenized_type ctxt mono level ary))
           |> ho_type_from_typ format type_enc pred_sym (length T_arg_Ts + ary))
   end
 
-fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind nonmono_Ts
-        type_enc n s j (s', T_args, T, _, ary, in_conj) =
+fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono type_enc n s
+                                     j (s', T_args, T, _, ary, in_conj) =
   let
     val (kind, maybe_negate) =
       if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
@@ -1886,7 +1916,7 @@
     val sym_needs_arg_types = exists (curry (op =) dummyT) T_args
     fun should_keep_arg_type T =
       sym_needs_arg_types andalso
-      should_predicate_on_type ctxt nonmono_Ts type_enc (K true) T
+      should_guard_type ctxt mono type_enc (K true) T
     val bound_Ts =
       arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE)
   in
@@ -1896,7 +1926,7 @@
              |> fold (curry (IApp o swap)) bounds
              |> type_guard_iterm ctxt format type_enc res_T
              |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
-             |> formula_from_iformula ctxt format nonmono_Ts type_enc
+             |> formula_from_iformula ctxt format mono type_enc
                                       (K (K (K (K true)))) (SOME true)
              |> n > 1 ? bound_tvars type_enc (atyps_of T)
              |> close_formula_universally
@@ -1904,8 +1934,8 @@
              isabelle_info introN, NONE)
   end
 
-fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind
-        nonmono_Ts type_enc n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
+fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind mono
+        type_enc n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
   let
     val ident_base =
       tags_sym_formula_prefix ^ s ^
@@ -1920,8 +1950,8 @@
     val cst = mk_aterm format type_enc (s, s') T_args
     val eq = maybe_negate oo eq_formula type_enc (atyps_of T) pred_sym
     val should_encode =
-      should_encode_type ctxt nonmono_Ts (level_of_type_enc type_enc)
-    val tag_with = tag_with_type ctxt format nonmono_Ts type_enc NONE
+      should_encode_type ctxt mono (level_of_type_enc type_enc)
+    val tag_with = tag_with_type ctxt format mono type_enc NONE
     val add_formula_for_res =
       if should_encode res_T then
         cons (Formula (ident_base ^ "_res", kind,
@@ -1949,19 +1979,19 @@
 
 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
 
-fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts type_enc
+fun problem_lines_for_sym_decls ctxt format conj_sym_kind mono type_enc
                                 (s, decls) =
   case type_enc of
     Simple_Types _ =>
-    decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_enc s)
+    decls |> map (decl_line_for_sym ctxt format mono type_enc s)
   | Guards (_, level, _) =>
     let
       val decls =
         case decls of
           decl :: (decls' as _ :: _) =>
           let val T = result_type_of_decl decl in
-            if forall (curry (type_instance ctxt o swap) T
-                       o result_type_of_decl) decls' then
+            if forall (type_generalization ctxt T o result_type_of_decl)
+                      decls' then
               [decl]
             else
               decls
@@ -1969,12 +1999,12 @@
         | _ => decls
       val n = length decls
       val decls =
-        decls |> filter (should_encode_type ctxt nonmono_Ts level
+        decls |> filter (should_encode_type ctxt mono level
                          o result_type_of_decl)
     in
       (0 upto length decls - 1, decls)
-      |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind
-                                                 nonmono_Ts type_enc n s)
+      |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono
+                                                 type_enc n s)
     end
   | Tags (_, _, heaviness) =>
     (case heaviness of
@@ -1983,26 +2013,26 @@
        let val n = length decls in
          (0 upto n - 1 ~~ decls)
          |> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format
-                      conj_sym_kind nonmono_Ts type_enc n s)
+                      conj_sym_kind mono type_enc n s)
        end)
 
-fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
-                                     type_enc sym_decl_tab =
+fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc
+                                     sym_decl_tab =
   let
     val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
     val mono_Ts =
       if polymorphism_of_type_enc type_enc = Polymorphic then
         syms |> maps (map result_type_of_decl o snd)
-             |> filter_out (should_encode_type ctxt nonmono_Ts
+             |> filter_out (should_encode_type ctxt mono
                                 (level_of_type_enc type_enc))
              |> rpair [] |-> fold (insert_type ctxt I)
       else
         []
     val mono_lines =
-      problem_lines_for_mono_types ctxt format nonmono_Ts type_enc mono_Ts
+      problem_lines_for_mono_types ctxt format mono type_enc mono_Ts
     val decl_lines =
       fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
-                                                     nonmono_Ts type_enc)
+                                                     mono type_enc)
                syms []
   in mono_lines @ decl_lines end
 
@@ -2063,7 +2093,7 @@
       translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
                          hyp_ts concl_t facts
     val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
-    val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_enc
+    val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
     val repair = repair_fact ctxt format type_enc sym_tab
     val (conjs, facts) = (conjs, facts) |> pairself (map repair)
     val repaired_sym_tab =
@@ -2074,12 +2104,12 @@
     val sym_decl_lines =
       (conjs, helpers @ facts)
       |> sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
-      |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
+      |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
                                                type_enc
     val helper_lines =
       0 upto length helpers - 1 ~~ helpers
-      |> map (formula_line_for_fact ctxt format helper_prefix I false true
-                                    nonmono_Ts type_enc)
+      |> map (formula_line_for_fact ctxt format helper_prefix I false true mono
+                                    type_enc)
       |> (if needs_type_tag_idempotence type_enc then
             cons (type_tag_idempotence_fact ())
           else
@@ -2090,15 +2120,14 @@
       [(explicit_declsN, sym_decl_lines),
        (factsN,
         map (formula_line_for_fact ctxt format fact_prefix ascii_of
-                                   (not exporter) (not exporter) nonmono_Ts
+                                   (not exporter) (not exporter) mono
                                    type_enc)
             (0 upto length facts - 1 ~~ facts)),
        (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
        (aritiesN, map formula_line_for_arity_clause arity_clauses),
        (helpersN, helper_lines),
        (conjsN,
-        map (formula_line_for_conjecture ctxt format nonmono_Ts type_enc)
-            conjs),
+        map (formula_line_for_conjecture ctxt format mono type_enc) conjs),
        (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs))]
     val problem =
       problem