reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false

--- 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
@@ -1762,6 +1762,11 @@
               | _ => fold add_undefined_const (var_types ())))
   end
 
+(* 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"}]
+
 (* 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
@@ -1771,7 +1776,12 @@
      (case level of
         Noninf_Nonmono_Types =>
         not (is_locality_global locality) orelse
-        not (is_type_surely_infinite ctxt sound T)
+        (* Unlike virtually any other polymorphic fact whose type variables can
+           be instantiated by a known infinite type, extensionality actually
+           encodes a cardinality constraints. *)
+        not (is_type_surely_infinite ctxt sound
+                 (if locality = Extensionality then []
+                  else known_infinite_types) T)
       | Fin_Nonmono_Types => is_type_surely_finite ctxt false T
       | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
   | add_iterm_nonmonotonic_types _ _ _ _ _ _ = I

--- a/src/HOL/Tools/ATP/atp_util.ML	Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Mon Aug 22 15:02:45 2011 +0200
@@ -22,7 +22,7 @@
     Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
     -> typ
   val is_type_surely_finite : Proof.context -> bool -> typ -> bool
-  val is_type_surely_infinite : Proof.context -> bool -> typ -> bool
+  val is_type_surely_infinite : Proof.context -> bool -> typ list -> typ -> bool
   val s_not : term -> term
   val s_conj : term * term -> term
   val s_disj : term * term -> term
@@ -149,65 +149,71 @@
    0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means
    cardinality 2 or more. The specified default cardinality is returned if the
    cardinality of the type can't be determined. *)
-fun tiny_card_of_type ctxt sound default_card T =
+fun tiny_card_of_type ctxt sound unsound_assigns default_card T =
   let
     val thy = Proof_Context.theory_of ctxt
     val max = 2 (* 1 would be too small for the "fun" case *)
     fun aux slack avoid T =
       if member (op =) avoid T then
         0
-      else case T of
-        Type (@{type_name fun}, [T1, T2]) =>
-        (case (aux slack avoid T1, aux slack avoid T2) of
-           (k, 1) => if slack andalso k = 0 then 0 else 1
-         | (0, _) => 0
-         | (_, 0) => 0
-         | (k1, k2) =>
-           if k1 >= max orelse k2 >= max then max
-           else Int.min (max, Integer.pow k2 k1))
-      | @{typ prop} => 2
-      | @{typ bool} => 2 (* optimization *)
-      | @{typ nat} => 0 (* optimization *)
-      | Type ("Int.int", []) => 0 (* optimization *)
-      | Type (s, _) =>
-        (case datatype_constrs thy T of
-           constrs as _ :: _ =>
-           let
-             val constr_cards =
-               map (Integer.prod o map (aux slack (T :: avoid)) o binder_types
-                    o snd) constrs
-           in
-             if exists (curry (op =) 0) constr_cards then 0
-             else Int.min (max, Integer.sum constr_cards)
-           end
-         | [] =>
-           case Typedef.get_info ctxt s of
-             ({abs_type, rep_type, ...}, _) :: _ =>
-             (* We cheat here by assuming that typedef types are infinite if
-                their underlying type is infinite. This is unsound in general
-                but it's hard to think of a realistic example where this would
-                not be the case. We are also slack with representation types:
-                If a representation type has the form "sigma => tau", we
-                consider it enough to check "sigma" for infiniteness. (Look
-                for "slack" in this function.) *)
-             (case varify_and_instantiate_type ctxt
-                       (Logic.varifyT_global abs_type) T
-                       (Logic.varifyT_global rep_type)
-                   |> aux true avoid of
-                0 => if sound then default_card else 0
-              | 1 => 1
-              | _ => default_card)
-           | [] => default_card)
-        (* Very slightly unsound: Type variables are assumed not to be
-           constrained to cardinality 1. (In practice, the user would most
-           likely have used "unit" directly anyway.) *)
-      | TFree _ =>
-        if default_card = 1 andalso not sound then 2 else default_card
-      | TVar _ => default_card
+      else case (sound, AList.lookup (Sign.typ_instance thy o swap)
+                                     unsound_assigns T) of
+        (false, SOME k) => k
+      | _ =>
+        case T of
+          Type (@{type_name fun}, [T1, T2]) =>
+          (case (aux slack avoid T1, aux slack avoid T2) of
+             (k, 1) => if slack andalso k = 0 then 0 else 1
+           | (0, _) => 0
+           | (_, 0) => 0
+           | (k1, k2) =>
+             if k1 >= max orelse k2 >= max then max
+             else Int.min (max, Integer.pow k2 k1))
+        | @{typ prop} => 2
+        | @{typ bool} => 2 (* optimization *)
+        | @{typ nat} => 0 (* optimization *)
+        | Type ("Int.int", []) => 0 (* optimization *)
+        | Type (s, _) =>
+          (case datatype_constrs thy T of
+             constrs as _ :: _ =>
+             let
+               val constr_cards =
+                 map (Integer.prod o map (aux slack (T :: avoid)) o binder_types
+                      o snd) constrs
+             in
+               if exists (curry (op =) 0) constr_cards then 0
+               else Int.min (max, Integer.sum constr_cards)
+             end
+           | [] =>
+             case Typedef.get_info ctxt s of
+               ({abs_type, rep_type, ...}, _) :: _ =>
+               (* We cheat here by assuming that typedef types are infinite if
+                  their underlying type is infinite. This is unsound in general
+                  but it's hard to think of a realistic example where this would
+                  not be the case. We are also slack with representation types:
+                  If a representation type has the form "sigma => tau", we
+                  consider it enough to check "sigma" for infiniteness. (Look
+                  for "slack" in this function.) *)
+               (case varify_and_instantiate_type ctxt
+                         (Logic.varifyT_global abs_type) T
+                         (Logic.varifyT_global rep_type)
+                     |> aux true avoid of
+                  0 => if sound then default_card else 0
+                | 1 => 1
+                | _ => default_card)
+             | [] => default_card)
+          (* Very slightly unsound: Type variables are assumed not to be
+             constrained to cardinality 1. (In practice, the user would most
+             likely have used "unit" directly anyway.) *)
+        | TFree _ =>
+          if default_card = 1 andalso not sound then 2 else default_card
+        | TVar _ => default_card
   in Int.min (max, aux false [] T) end
 
-fun is_type_surely_finite ctxt sound T = tiny_card_of_type ctxt sound 0 T <> 0
-fun is_type_surely_infinite ctxt sound T = tiny_card_of_type ctxt sound 1 T = 0
+fun is_type_surely_finite ctxt sound T =
+  tiny_card_of_type ctxt sound [] 0 T <> 0
+fun is_type_surely_infinite ctxt sound infinite_Ts T =
+  tiny_card_of_type ctxt sound (map (rpair 0) infinite_Ts) 1 T = 0
 
 (* Simple simplifications to ensure that sort annotations don't leave a trail of
    spurious "True"s. *)