gave up an optimization that sometimes lead to unsound proofs -- in short, facts talking about a schematic type variable can encode a cardinality constraint and be consistent with HOL, e.g. "card (UNIV::?'a set) = 1 ==> ALL x y. x = y"
1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Thu Jun 16 13:50:35 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Thu Jun 16 13:50:35 2011 +0200
1.3 @@ -1656,11 +1656,6 @@
1.4 ? (fold (add_fact true) conjs #> fold (add_fact false) facts)
1.5 end
1.6
1.7 -(* These types witness that the type classes they belong to allow infinite
1.8 - models and hence that any types with these type classes is monotonic. *)
1.9 -val known_infinite_types =
1.10 - [@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}]
1.11 -
1.12 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
1.13 out with monotonicity" paper presented at CADE 2011. *)
1.14 fun add_combterm_nonmonotonic_types _ _ _ (SOME false) _ = I
1.15 @@ -1670,12 +1665,8 @@
1.16 (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
1.17 (case level of
1.18 Noninf_Nonmono_Types =>
1.19 - (* Unlike virtually any other polymorphic fact whose type variables can
1.20 - be instantiated by a known infinite type, extensionality actually
1.21 - encodes a cardinality constraints. *)
1.22 not (is_locality_global locality) orelse
1.23 - not (is_type_surely_infinite ctxt (if locality = Extensionality then []
1.24 - else known_infinite_types) T)
1.25 + not (is_type_surely_infinite ctxt T)
1.26 | Fin_Nonmono_Types => is_type_surely_finite ctxt T
1.27 | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
1.28 | add_combterm_nonmonotonic_types _ _ _ _ _ = I
2.1 --- a/src/HOL/Tools/ATP/atp_util.ML Thu Jun 16 13:50:35 2011 +0200
2.2 +++ b/src/HOL/Tools/ATP/atp_util.ML Thu Jun 16 13:50:35 2011 +0200
2.3 @@ -22,7 +22,7 @@
2.4 Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
2.5 -> typ
2.6 val is_type_surely_finite : Proof.context -> typ -> bool
2.7 - val is_type_surely_infinite : Proof.context -> typ list -> typ -> bool
2.8 + val is_type_surely_infinite : Proof.context -> typ -> bool
2.9 val monomorphic_term : Type.tyenv -> term -> term
2.10 val eta_expand : typ list -> term -> int -> term
2.11 val transform_elim_prop : term -> term
2.12 @@ -136,70 +136,64 @@
2.13 0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means
2.14 cardinality 2 or more. The specified default cardinality is returned if the
2.15 cardinality of the type can't be determined. *)
2.16 -fun tiny_card_of_type ctxt default_card assigns T =
2.17 +fun tiny_card_of_type ctxt default_card T =
2.18 let
2.19 val thy = Proof_Context.theory_of ctxt
2.20 val max = 2 (* 1 would be too small for the "fun" case *)
2.21 fun aux slack avoid T =
2.22 if member (op =) avoid T then
2.23 0
2.24 - else case AList.lookup (Sign.typ_instance thy o swap) assigns T of
2.25 - SOME k => k
2.26 - | NONE =>
2.27 - case T of
2.28 - Type (@{type_name fun}, [T1, T2]) =>
2.29 - (case (aux slack avoid T1, aux slack avoid T2) of
2.30 - (k, 1) => if slack andalso k = 0 then 0 else 1
2.31 - | (0, _) => 0
2.32 - | (_, 0) => 0
2.33 - | (k1, k2) =>
2.34 - if k1 >= max orelse k2 >= max then max
2.35 - else Int.min (max, Integer.pow k2 k1))
2.36 - | @{typ prop} => 2
2.37 - | @{typ bool} => 2 (* optimization *)
2.38 - | @{typ nat} => 0 (* optimization *)
2.39 - | Type ("Int.int", []) => 0 (* optimization *)
2.40 - | Type (s, _) =>
2.41 - (case datatype_constrs thy T of
2.42 - constrs as _ :: _ =>
2.43 - let
2.44 - val constr_cards =
2.45 - map (Integer.prod o map (aux slack (T :: avoid)) o binder_types
2.46 - o snd) constrs
2.47 - in
2.48 - if exists (curry (op =) 0) constr_cards then 0
2.49 - else Int.min (max, Integer.sum constr_cards)
2.50 - end
2.51 - | [] =>
2.52 - case Typedef.get_info ctxt s of
2.53 - ({abs_type, rep_type, ...}, _) :: _ =>
2.54 - (* We cheat here by assuming that typedef types are infinite if
2.55 - their underlying type is infinite. This is unsound in general
2.56 - but it's hard to think of a realistic example where this would
2.57 - not be the case. We are also slack with representation types:
2.58 - If a representation type has the form "sigma => tau", we
2.59 - consider it enough to check "sigma" for infiniteness. (Look
2.60 - for "slack" in this function.) *)
2.61 - (case varify_and_instantiate_type ctxt
2.62 - (Logic.varifyT_global abs_type) T
2.63 - (Logic.varifyT_global rep_type)
2.64 - |> aux true avoid of
2.65 - 0 => 0
2.66 - | 1 => 1
2.67 - | _ => default_card)
2.68 - | [] => default_card)
2.69 - (* Very slightly unsound: Type variables are assumed not to be
2.70 - constrained to cardinality 1. (In practice, the user would most
2.71 - likely have used "unit" directly anyway.) *)
2.72 - | TFree _ => if default_card = 1 then 2 else default_card
2.73 - (* Schematic type variables that contain only unproblematic sorts
2.74 - (with no finiteness axiom) can safely be considered infinite. *)
2.75 - | TVar _ => default_card
2.76 + else case T of
2.77 + Type (@{type_name fun}, [T1, T2]) =>
2.78 + (case (aux slack avoid T1, aux slack avoid T2) of
2.79 + (k, 1) => if slack andalso k = 0 then 0 else 1
2.80 + | (0, _) => 0
2.81 + | (_, 0) => 0
2.82 + | (k1, k2) =>
2.83 + if k1 >= max orelse k2 >= max then max
2.84 + else Int.min (max, Integer.pow k2 k1))
2.85 + | @{typ prop} => 2
2.86 + | @{typ bool} => 2 (* optimization *)
2.87 + | @{typ nat} => 0 (* optimization *)
2.88 + | Type ("Int.int", []) => 0 (* optimization *)
2.89 + | Type (s, _) =>
2.90 + (case datatype_constrs thy T of
2.91 + constrs as _ :: _ =>
2.92 + let
2.93 + val constr_cards =
2.94 + map (Integer.prod o map (aux slack (T :: avoid)) o binder_types
2.95 + o snd) constrs
2.96 + in
2.97 + if exists (curry (op =) 0) constr_cards then 0
2.98 + else Int.min (max, Integer.sum constr_cards)
2.99 + end
2.100 + | [] =>
2.101 + case Typedef.get_info ctxt s of
2.102 + ({abs_type, rep_type, ...}, _) :: _ =>
2.103 + (* We cheat here by assuming that typedef types are infinite if
2.104 + their underlying type is infinite. This is unsound in general
2.105 + but it's hard to think of a realistic example where this would
2.106 + not be the case. We are also slack with representation types:
2.107 + If a representation type has the form "sigma => tau", we
2.108 + consider it enough to check "sigma" for infiniteness. (Look
2.109 + for "slack" in this function.) *)
2.110 + (case varify_and_instantiate_type ctxt
2.111 + (Logic.varifyT_global abs_type) T
2.112 + (Logic.varifyT_global rep_type)
2.113 + |> aux true avoid of
2.114 + 0 => 0
2.115 + | 1 => 1
2.116 + | _ => default_card)
2.117 + | [] => default_card)
2.118 + (* Very slightly unsound: Type variables are assumed not to be
2.119 + constrained to cardinality 1. (In practice, the user would most
2.120 + likely have used "unit" directly anyway.) *)
2.121 + | TFree _ => if default_card = 1 then 2 else default_card
2.122 + | TVar _ => default_card
2.123 in Int.min (max, aux false [] T) end
2.124
2.125 -fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 [] T <> 0
2.126 -fun is_type_surely_infinite ctxt infinite_Ts T =
2.127 - tiny_card_of_type ctxt 1 (map (rpair 0) infinite_Ts) T = 0
2.128 +fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 T <> 0
2.129 +fun is_type_surely_infinite ctxt T = tiny_card_of_type ctxt 1 T = 0
2.130
2.131 fun monomorphic_term subst =
2.132 map_types (map_type_tvar (fn v =>