# HG changeset patch # User blanchet # Date 1314018165 -7200 # Node ID 23adec5984f1927f6406c4d39047b4f6993b8a9f # Parent 6750b4297691f018fe5a1cbd14cda5dc42f7afcc make sound mode more sound (and clean up code) diff -r 6750b4297691 -r 23adec5984f1 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Mon Aug 22 15:02:45 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Mon Aug 22 15:02:45 2011 +0200 @@ -1077,7 +1077,7 @@ exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts | should_encode_type _ _ All_Types _ = true | should_encode_type ctxt _ Fin_Nonmono_Types T = - is_type_surely_finite ctxt false T + is_type_surely_finite ctxt T | should_encode_type _ _ _ _ = false fun should_predicate_on_type ctxt nonmono_Ts (Guards (_, level, heaviness)) @@ -1779,10 +1779,11 @@ (* Unlike virtually any other polymorphic fact whose type variables can be instantiated by a known infinite type, extensionality actually encodes a cardinality constraints. *) - not (is_type_surely_infinite ctxt sound + not (not sound andalso + is_type_surely_infinite ctxt (if locality = Extensionality then [] else known_infinite_types) T) - | Fin_Nonmono_Types => is_type_surely_finite ctxt false T + | Fin_Nonmono_Types => is_type_surely_finite ctxt T | _ => true)) ? insert_type ctxt I (deep_freeze_type T) | add_iterm_nonmonotonic_types _ _ _ _ _ _ = I fun add_fact_nonmonotonic_types ctxt level sound @@ -1829,8 +1830,8 @@ bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, [])) val sym_needs_arg_types = exists (curry (op =) dummyT) T_args fun should_keep_arg_type T = - sym_needs_arg_types orelse - not (should_predicate_on_type ctxt nonmono_Ts type_enc (K false) T) + sym_needs_arg_types andalso + should_predicate_on_type ctxt nonmono_Ts type_enc (K true) T val bound_Ts = arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE) in diff -r 6750b4297691 -r 23adec5984f1 src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Mon Aug 22 15:02:45 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_util.ML Mon Aug 22 15:02:45 2011 +0200 @@ -21,8 +21,8 @@ val typ_of_dtyp : Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp -> typ - val is_type_surely_finite : Proof.context -> bool -> typ -> bool - val is_type_surely_infinite : Proof.context -> bool -> typ list -> typ -> bool + val is_type_surely_finite : Proof.context -> typ -> bool + val is_type_surely_infinite : Proof.context -> typ list -> typ -> bool val s_not : term -> term val s_conj : term * term -> term val s_disj : term * term -> term @@ -149,17 +149,16 @@ 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 sound unsound_assigns default_card T = +fun tiny_card_of_type ctxt assigns default_card T = let val thy = Proof_Context.theory_of ctxt 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 (sound, AList.lookup (Sign.typ_instance thy o swap) - unsound_assigns T) of - (false, SOME k) => k - | _ => + else case AList.lookup (Sign.typ_instance thy o swap) assigns T of + SOME k => k + | NONE => case T of Type (@{type_name fun}, [T1, T2]) => (case (aux slack avoid T1, aux slack avoid T2) of @@ -198,22 +197,20 @@ (Logic.varifyT_global abs_type) T (Logic.varifyT_global rep_type) |> aux true avoid of - 0 => if sound then default_card else 0 + 0 => 0 | 1 => 1 | _ => default_card) | [] => default_card) (* 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 andalso not sound then 2 else default_card + | TFree _ => if default_card = 1 then 2 else default_card | TVar _ => default_card in Int.min (max, aux false [] T) end -fun is_type_surely_finite ctxt sound T = - tiny_card_of_type ctxt sound [] 0 T <> 0 -fun is_type_surely_infinite ctxt sound infinite_Ts T = - tiny_card_of_type ctxt sound (map (rpair 0) infinite_Ts) 1 T = 0 +fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt [] 0 T <> 0 +fun is_type_surely_infinite ctxt infinite_Ts T = + tiny_card_of_type ctxt (map (rpair 0) infinite_Ts) 1 T = 0 (* Simple simplifications to ensure that sort annotations don't leave a trail of spurious "True"s. *) diff -r 6750b4297691 -r 23adec5984f1 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Aug 22 15:02:45 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Aug 22 15:02:45 2011 +0200 @@ -498,7 +498,7 @@ are omitted. *) fun is_dangerous_prop ctxt = transform_elim_prop - #> (has_bound_or_var_of_type (is_type_surely_finite ctxt false) orf + #> (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)