src/HOL/Tools/ATP/atp_translate.ML
changeset 44500 dbd98b549597
parent 44499 8870232a87ad
child 44501 5bde887b4785
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 22:05:18 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 22:06:25 2011 +0200
     1.3 @@ -1095,12 +1095,9 @@
     1.4  val known_infinite_types =
     1.5    [@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}]
     1.6  
     1.7 -fun is_type_surely_infinite' ctxt soundness cached_Ts T =
     1.8 -  (* Unlike virtually any other polymorphic fact whose type variables can be
     1.9 -     instantiated by a known infinite type, extensionality actually encodes a
    1.10 -     cardinality constraints. *)
    1.11 +fun is_type_kind_of_surely_infinite ctxt soundness cached_Ts T =
    1.12    soundness <> Sound andalso
    1.13 -  is_type_surely_infinite ctxt (soundness = Unsound) cached_Ts T
    1.14 +  is_type_surely_infinite ctxt (soundness <> Unsound) cached_Ts T
    1.15  
    1.16  (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
    1.17     dangerous because their "exhaust" properties can easily lead to unsound ATP
    1.18 @@ -1114,7 +1111,7 @@
    1.19      exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
    1.20      not (exists (type_instance ctxt T) surely_infinite_Ts orelse
    1.21           (not (member (type_aconv ctxt) maybe_finite_Ts T) andalso
    1.22 -          is_type_surely_infinite' ctxt soundness surely_infinite_Ts T))
    1.23 +          is_type_kind_of_surely_infinite ctxt soundness surely_infinite_Ts T))
    1.24    | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
    1.25                               maybe_nonmono_Ts, ...}
    1.26                         Fin_Nonmono_Types T =
    1.27 @@ -1844,8 +1841,8 @@
    1.28          if exists (type_instance ctxt T) surely_infinite_Ts orelse
    1.29             member (type_aconv ctxt) maybe_finite_Ts T then
    1.30            mono
    1.31 -        else if is_type_surely_infinite' ctxt soundness surely_infinite_Ts
    1.32 -                                         T then
    1.33 +        else if is_type_kind_of_surely_infinite ctxt soundness
    1.34 +                                                surely_infinite_Ts T then
    1.35            {maybe_finite_Ts = maybe_finite_Ts,
    1.36             surely_finite_Ts = surely_finite_Ts,
    1.37             maybe_infinite_Ts = maybe_infinite_Ts,