# HG changeset patch
# User blanchet
# Date 1314302785 -7200
# Node ID dbd98b5495978b8e35b0227f8ac2a1f48c640d55
# Parent  8870232a87ada5f6a93f3aa311ecad975b110e4d
make default unsound mode less unsound

diff -r 8870232a87ad -r dbd98b549597 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 22:05:18 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 22:06:25 2011 +0200
@@ -1095,12 +1095,9 @@
 val known_infinite_types =
   [@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}]
 
-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. *)
+fun is_type_kind_of_surely_infinite ctxt soundness cached_Ts T =
   soundness <> Sound andalso
-  is_type_surely_infinite ctxt (soundness = Unsound) cached_Ts 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
@@ -1114,7 +1111,7 @@
     exists (type_intersect 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))
+          is_type_kind_of_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 =
@@ -1844,8 +1841,8 @@
         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
+        else if is_type_kind_of_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,
diff -r 8870232a87ad -r dbd98b549597 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Thu Aug 25 22:05:18 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Thu Aug 25 22:06:25 2011 +0200
@@ -161,16 +161,14 @@
    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 inst_tvars assigns default_card T =
+fun tiny_card_of_type ctxt sound assigns default_card T =
   let
     val thy = Proof_Context.theory_of ctxt
     val max = 2 (* 1 would be too small for the "fun" case *)
-    val type_cmp =
-      if inst_tvars then uncurry (type_generalization ctxt) else type_aconv ctxt
     fun aux slack avoid T =
       if member (op =) avoid T then
         0
-      else case AList.lookup type_cmp assigns T of
+      else case AList.lookup (type_aconv ctxt) assigns T of
         SOME k => k
       | NONE =>
         case T of
@@ -218,13 +216,14 @@
           (* 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 then 2 else default_card
+        | TFree _ =>
+          if not sound andalso default_card = 1 then 2 else default_card
         | TVar _ => default_card
   in Int.min (max, aux false [] T) end
 
-fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt false [] 0 T <> 0
-fun is_type_surely_infinite ctxt inst_tvars infinite_Ts T =
-  tiny_card_of_type ctxt inst_tvars (map (rpair 0) infinite_Ts) 1 T = 0
+fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt true [] 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. *)