src/HOL/Tools/ATP/atp_util.ML
changeset 44500 dbd98b549597
parent 44491 ba22ed224b20
child 44784 c9a081ef441d
     1.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Thu Aug 25 22:05:18 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Thu Aug 25 22:06:25 2011 +0200
     1.3 @@ -161,16 +161,14 @@
     1.4     0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means
     1.5     cardinality 2 or more. The specified default cardinality is returned if the
     1.6     cardinality of the type can't be determined. *)
     1.7 -fun tiny_card_of_type ctxt inst_tvars assigns default_card T =
     1.8 +fun tiny_card_of_type ctxt sound assigns default_card T =
     1.9    let
    1.10      val thy = Proof_Context.theory_of ctxt
    1.11      val max = 2 (* 1 would be too small for the "fun" case *)
    1.12 -    val type_cmp =
    1.13 -      if inst_tvars then uncurry (type_generalization ctxt) else type_aconv ctxt
    1.14      fun aux slack avoid T =
    1.15        if member (op =) avoid T then
    1.16          0
    1.17 -      else case AList.lookup type_cmp assigns T of
    1.18 +      else case AList.lookup (type_aconv ctxt) assigns T of
    1.19          SOME k => k
    1.20        | NONE =>
    1.21          case T of
    1.22 @@ -218,13 +216,14 @@
    1.23            (* Very slightly unsound: Type variables are assumed not to be
    1.24               constrained to cardinality 1. (In practice, the user would most
    1.25               likely have used "unit" directly anyway.) *)
    1.26 -        | TFree _ => if default_card = 1 then 2 else default_card
    1.27 +        | TFree _ =>
    1.28 +          if not sound andalso default_card = 1 then 2 else default_card
    1.29          | TVar _ => default_card
    1.30    in Int.min (max, aux false [] T) end
    1.31  
    1.32 -fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt false [] 0 T <> 0
    1.33 -fun is_type_surely_infinite ctxt inst_tvars infinite_Ts T =
    1.34 -  tiny_card_of_type ctxt inst_tvars (map (rpair 0) infinite_Ts) 1 T = 0
    1.35 +fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt true [] 0 T <> 0
    1.36 +fun is_type_surely_infinite ctxt sound infinite_Ts T =
    1.37 +  tiny_card_of_type ctxt sound (map (rpair 0) infinite_Ts) 1 T = 0
    1.38  
    1.39  (* Simple simplifications to ensure that sort annotations don't leave a trail of
    1.40     spurious "True"s. *)