--- 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,
--- 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. *)