reintroduced type encodings "poly_preds_{bang,query}", but this time being more liberal about type variables of known safe sorts
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 20 12:47:59 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 20 12:47:59 2011 +0200
@@ -141,13 +141,12 @@
case (core, (poly, level, heaviness)) of
("simple", (NONE, _, Light)) => Simple_Types level
| ("preds", (SOME Polymorphic, _, _)) =>
- if level = All_Types then Preds (Polymorphic, level, heaviness)
- else raise Same.SAME
+ Preds (Polymorphic, level, heaviness)
| ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
| ("tags", (SOME Polymorphic, All_Types, _)) =>
Tags (Polymorphic, All_Types, heaviness)
| ("tags", (SOME Polymorphic, Finite_Types, _)) =>
- (* The light encoding yields too many unsound proofs. *)
+ (* The actual light encoding yields too many unsound proofs. *)
Tags (Polymorphic, Finite_Types, Heavy)
| ("tags", (SOME Polymorphic, _, _)) => raise Same.SAME
| ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri May 20 12:47:59 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri May 20 12:47:59 2011 +0200
@@ -122,6 +122,12 @@
| NONE => [])
| datatype_constrs _ _ = []
+(* Feel free to extend this list with any sorts that don't have finiteness
+ axioms. *)
+val safe_sorts =
+ @{sort type} @ @{sort "{default,zero,one,plus,minus,uminus,times,inverse}"} @
+ @{sort "{abs,sgn,ord,equal,number}"}
+
(* Similar to "Nitpick_HOL.bounded_exact_card_of_type".
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
@@ -130,58 +136,61 @@
let
val max = 2 (* 1 would be too small for the "fun" case *)
fun aux slack avoid T =
- (if member (op =) avoid T then
- 0
- else case T of
- Type (@{type_name fun}, [T1, T2]) =>
- (case (aux slack avoid T1, aux slack avoid T2) of
- (k, 1) => if slack andalso k = 0 then 0 else 1
- | (0, _) => 0
- | (_, 0) => 0
- | (k1, k2) =>
- if k1 >= max orelse k2 >= max then max
- else Int.min (max, Integer.pow k2 k1))
- | @{typ prop} => 2
- | @{typ bool} => 2 (* optimization *)
- | @{typ nat} => 0 (* optimization *)
- | @{typ int} => 0 (* optimization *)
- | Type (s, _) =>
- let val thy = Proof_Context.theory_of ctxt in
- case datatype_constrs thy T of
- constrs as _ :: _ =>
- let
- val constr_cards =
- map (Integer.prod o map (aux slack (T :: avoid)) o binder_types
- o snd) constrs
- in
- if exists (curry (op =) 0) constr_cards then 0
- else Int.min (max, Integer.sum constr_cards)
- end
- | [] =>
- case Typedef.get_info ctxt s of
- ({abs_type, rep_type, ...}, _) :: _ =>
- (* We cheat here by assuming that typedef types are infinite if
- their underlying type is infinite. This is unsound in general
- but it's hard to think of a realistic example where this would
- not be the case. We are also slack with representation types:
- If a representation type has the form "sigma => tau", we
- consider it enough to check "sigma" for infiniteness. (Look
- for "slack" in this function.) *)
- (case varify_and_instantiate_type ctxt
- (Logic.varifyT_global abs_type) T
- (Logic.varifyT_global rep_type)
- |> aux true avoid of
- 0 => 0
- | 1 => 1
- | _ => default_card)
- | [] => default_card
- end
- | TFree _ =>
- (* 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.) *)
- if default_card = 1 then 2 else default_card
- | _ => default_card)
+ if member (op =) avoid T then
+ 0
+ else case T of
+ Type (@{type_name fun}, [T1, T2]) =>
+ (case (aux slack avoid T1, aux slack avoid T2) of
+ (k, 1) => if slack andalso k = 0 then 0 else 1
+ | (0, _) => 0
+ | (_, 0) => 0
+ | (k1, k2) =>
+ if k1 >= max orelse k2 >= max then max
+ else Int.min (max, Integer.pow k2 k1))
+ | @{typ prop} => 2
+ | @{typ bool} => 2 (* optimization *)
+ | @{typ nat} => 0 (* optimization *)
+ | @{typ int} => 0 (* optimization *)
+ | Type (s, _) =>
+ let val thy = Proof_Context.theory_of ctxt in
+ case datatype_constrs thy T of
+ constrs as _ :: _ =>
+ let
+ val constr_cards =
+ map (Integer.prod o map (aux slack (T :: avoid)) o binder_types
+ o snd) constrs
+ in
+ if exists (curry (op =) 0) constr_cards then 0
+ else Int.min (max, Integer.sum constr_cards)
+ end
+ | [] =>
+ case Typedef.get_info ctxt s of
+ ({abs_type, rep_type, ...}, _) :: _ =>
+ (* We cheat here by assuming that typedef types are infinite if
+ their underlying type is infinite. This is unsound in general
+ but it's hard to think of a realistic example where this would
+ not be the case. We are also slack with representation types:
+ If a representation type has the form "sigma => tau", we
+ consider it enough to check "sigma" for infiniteness. (Look for
+ "slack" in this function.) *)
+ (case varify_and_instantiate_type ctxt
+ (Logic.varifyT_global abs_type) T
+ (Logic.varifyT_global rep_type)
+ |> aux true avoid of
+ 0 => 0
+ | 1 => 1
+ | _ => default_card)
+ | [] => default_card
+ end
+ (* 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
+ (* Schematic type variables that contain only unproblematic sorts
+ (with no finiteness axiom) can safely be considered infinite. *)
+ | TVar (_, S) =>
+ if default_card = 0 orelse subset (op =) (S, safe_sorts) then 0
+ else default_card
in Int.min (max, aux false [] T) end
fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 T <> 0