improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu May 12 15:29:19 2011 +0200
@@ -477,80 +477,6 @@
proofs. On the other hand, all HOL infinite types can be given the same
models in first-order logic (via Löwenheim-Skolem). *)
-fun datatype_constrs thy (T as Type (s, Ts)) =
- (case Datatype.get_info thy s of
- SOME {index, descr, ...} =>
- let val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the in
- map (apsnd (fn Us => map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
- constrs
- end
- | NONE => [])
- | datatype_constrs _ _ = []
-
-(* 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
- cardinality of the type can't be determined. *)
-fun tiny_card_of_type ctxt default_card T =
- 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 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)
- in Int.min (max, aux false [] T) end
-
-fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 T <> 0
-fun is_type_surely_infinite ctxt T = tiny_card_of_type ctxt 1 T = 0
-
fun should_encode_type _ _ All_Types _ = true
| should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T
| should_encode_type _ nonmono_Ts Nonmonotonic_Types T =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu May 12 15:29:19 2011 +0200
@@ -49,7 +49,6 @@
val const_names_in_fact :
theory -> (string * typ -> term list -> bool * term list) -> term
-> string list
- val is_dangerous_term : term -> bool
val relevant_facts :
Proof.context -> real * real -> int
-> (string * typ -> term list -> bool * term list) -> relevance_fudge
@@ -737,62 +736,6 @@
(**** Predicates to detect unwanted facts (prolific or likely to cause
unsoundness) ****)
-(* Too general means, positive equality literal with a variable X as one
- operand, when X does not occur properly in the other operand. This rules out
- clearly inconsistent facts such as X = a | X = b, though it by no means
- guarantees soundness. *)
-
-(* Unwanted equalities are those between a (bound or schematic) variable that
- does not properly occur in the second operand. *)
-val is_exhaustive_finite =
- let
- fun is_bad_equal (Var z) t =
- not (exists_subterm (fn Var z' => z = z' | _ => false) t)
- | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j))
- | is_bad_equal _ _ = false
- fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1
- fun do_formula pos t =
- case (pos, t) of
- (_, @{const Trueprop} $ t1) => do_formula pos t1
- | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) =>
- do_formula pos t'
- | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) =>
- do_formula pos t'
- | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) =>
- do_formula pos t'
- | (_, @{const "==>"} $ t1 $ t2) =>
- do_formula (not pos) t1 andalso
- (t2 = @{prop False} orelse do_formula pos t2)
- | (_, @{const HOL.implies} $ t1 $ t2) =>
- do_formula (not pos) t1 andalso
- (t2 = @{const False} orelse do_formula pos t2)
- | (_, @{const Not} $ t1) => do_formula (not pos) t1
- | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
- | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
- | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2
- | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
- | _ => false
- in do_formula true end
-
-fun has_bound_or_var_of_type tycons =
- exists_subterm (fn Var (_, Type (s, _)) => member (op =) tycons s
- | Abs (_, Type (s, _), _) => member (op =) tycons s
- | _ => false)
-
-(* Facts are forbidden to contain variables of these types. The typical reason
- is that they lead to unsoundness. Note that "unit" satisfies numerous
- equations like "?x = ()". The resulting clauses will have no type constraint,
- yielding false proofs. Even "bool" leads to many unsound proofs, though only
- for higher-order problems. *)
-val dangerous_types = [@{type_name unit}, @{type_name bool}, @{type_name prop}]
-
-(* Facts containing variables of type "unit" or "bool" or of the form
- "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types
- are omitted. *)
-val is_dangerous_term =
- transform_elim_term
- #> (has_bound_or_var_of_type dangerous_types orf is_exhaustive_finite)
-
fun is_theorem_bad_for_atps thm =
let val t = prop_of thm in
is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu May 12 15:29:19 2011 +0200
@@ -339,6 +339,62 @@
(* generic TPTP-based ATPs *)
+(* Too general means, positive equality literal with a variable X as one
+ operand, when X does not occur properly in the other operand. This rules out
+ clearly inconsistent facts such as X = a | X = b, though it by no means
+ guarantees soundness. *)
+
+(* Unwanted equalities are those between a (bound or schematic) variable that
+ does not properly occur in the second operand. *)
+val is_exhaustive_finite =
+ let
+ fun is_bad_equal (Var z) t =
+ not (exists_subterm (fn Var z' => z = z' | _ => false) t)
+ | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j))
+ | is_bad_equal _ _ = false
+ fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1
+ fun do_formula pos t =
+ case (pos, t) of
+ (_, @{const Trueprop} $ t1) => do_formula pos t1
+ | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) =>
+ do_formula pos t'
+ | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) =>
+ do_formula pos t'
+ | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) =>
+ do_formula pos t'
+ | (_, @{const "==>"} $ t1 $ t2) =>
+ do_formula (not pos) t1 andalso
+ (t2 = @{prop False} orelse do_formula pos t2)
+ | (_, @{const HOL.implies} $ t1 $ t2) =>
+ do_formula (not pos) t1 andalso
+ (t2 = @{const False} orelse do_formula pos t2)
+ | (_, @{const Not} $ t1) => do_formula (not pos) t1
+ | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
+ | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
+ | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2
+ | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
+ | _ => false
+ in do_formula true end
+
+fun has_bound_or_var_of_type pred =
+ exists_subterm (fn Var (_, T as Type _) => pred T
+ | Abs (_, T as Type _, _) => pred T
+ | _ => false)
+
+(* Facts are forbidden to contain variables of these types. The typical reason
+ is that they lead to unsoundness. Note that "unit" satisfies numerous
+ equations like "?x = ()". The resulting clauses will have no type constraint,
+ yielding false proofs. Even "bool" leads to many unsound proofs, though only
+ for higher-order problems. *)
+
+(* Facts containing variables of type "unit" or "bool" or of the form
+ "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types
+ are omitted. *)
+fun is_dangerous_term ctxt =
+ transform_elim_term
+ #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf
+ is_exhaustive_finite)
+
fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
| int_opt_add _ _ = NONE
@@ -448,7 +504,7 @@
val fairly_sound = is_type_sys_fairly_sound type_sys
val facts =
facts |> not fairly_sound
- ? filter_out (is_dangerous_term o prop_of o snd
+ ? filter_out (is_dangerous_term ctxt o prop_of o snd
o untranslated_fact)
|> take num_facts
|> not (null blacklist)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu May 12 15:29:19 2011 +0200
@@ -21,6 +21,8 @@
val varify_type : Proof.context -> typ -> typ
val instantiate_type : theory -> typ -> typ -> typ -> typ
val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
+ val is_type_surely_finite : Proof.context -> typ -> bool
+ val is_type_surely_infinite : Proof.context -> typ -> bool
val monomorphic_term : Type.tyenv -> term -> term
val eta_expand : typ list -> term -> int -> term
val transform_elim_term : term -> term
@@ -110,6 +112,81 @@
instantiate_type thy (varify_type ctxt T1) T1' (varify_type ctxt T2)
end
+fun datatype_constrs thy (T as Type (s, Ts)) =
+ (case Datatype.get_info thy s of
+ SOME {index, descr, ...} =>
+ let val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the in
+ map (apsnd (fn Us => map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
+ constrs
+ end
+ | NONE => [])
+ | datatype_constrs _ _ = []
+
+(* 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
+ cardinality of the type can't be determined. *)
+fun tiny_card_of_type ctxt default_card T =
+ 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)
+ in Int.min (max, aux false [] T) end
+
+fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 T <> 0
+fun is_type_surely_infinite ctxt T = tiny_card_of_type ctxt 1 T = 0
+
fun monomorphic_term subst t =
map_types (map_type_tvar (fn v =>
case Type.lookup subst v of