make default unsound mode less unsound
authorblanchet
Thu Aug 25 22:06:25 2011 +0200 (2011-08-25)
changeset 44500dbd98b549597
parent 44499 8870232a87ad
child 44501 5bde887b4785
make default unsound mode less unsound
src/HOL/Tools/ATP/atp_translate.ML
src/HOL/Tools/ATP/atp_util.ML
     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,
     2.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Thu Aug 25 22:05:18 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Thu Aug 25 22:06:25 2011 +0200
     2.3 @@ -161,16 +161,14 @@
     2.4     0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means
     2.5     cardinality 2 or more. The specified default cardinality is returned if the
     2.6     cardinality of the type can't be determined. *)
     2.7 -fun tiny_card_of_type ctxt inst_tvars assigns default_card T =
     2.8 +fun tiny_card_of_type ctxt sound assigns default_card T =
     2.9    let
    2.10      val thy = Proof_Context.theory_of ctxt
    2.11      val max = 2 (* 1 would be too small for the "fun" case *)
    2.12 -    val type_cmp =
    2.13 -      if inst_tvars then uncurry (type_generalization ctxt) else type_aconv ctxt
    2.14      fun aux slack avoid T =
    2.15        if member (op =) avoid T then
    2.16          0
    2.17 -      else case AList.lookup type_cmp assigns T of
    2.18 +      else case AList.lookup (type_aconv ctxt) assigns T of
    2.19          SOME k => k
    2.20        | NONE =>
    2.21          case T of
    2.22 @@ -218,13 +216,14 @@
    2.23            (* Very slightly unsound: Type variables are assumed not to be
    2.24               constrained to cardinality 1. (In practice, the user would most
    2.25               likely have used "unit" directly anyway.) *)
    2.26 -        | TFree _ => if default_card = 1 then 2 else default_card
    2.27 +        | TFree _ =>
    2.28 +          if not sound andalso default_card = 1 then 2 else default_card
    2.29          | TVar _ => default_card
    2.30    in Int.min (max, aux false [] T) end
    2.31  
    2.32 -fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt false [] 0 T <> 0
    2.33 -fun is_type_surely_infinite ctxt inst_tvars infinite_Ts T =
    2.34 -  tiny_card_of_type ctxt inst_tvars (map (rpair 0) infinite_Ts) 1 T = 0
    2.35 +fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt true [] 0 T <> 0
    2.36 +fun is_type_surely_infinite ctxt sound infinite_Ts T =
    2.37 +  tiny_card_of_type ctxt sound (map (rpair 0) infinite_Ts) 1 T = 0
    2.38  
    2.39  (* Simple simplifications to ensure that sort annotations don't leave a trail of
    2.40     spurious "True"s. *)