# HG changeset patch # User blanchet # Date 1319886958 -7200 # Node ID ee584ff987c328c7bd7c49d9d33a08bf57112a2c # Parent aa35859c87410566973cf38d6010b83ede789725 check "sound" flag before doing something unsound... diff -r aa35859c8741 -r ee584ff987c3 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Sat Oct 29 12:57:43 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Sat Oct 29 13:15:58 2011 +0200 @@ -19,7 +19,7 @@ General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic - datatype soundness = Sound_Modulo_Infiniteness | Sound + datatype soundness = Sound_Modulo_Infinity | Sound datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars datatype type_level = All_Types | @@ -529,7 +529,7 @@ datatype order = First_Order | Higher_Order datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic -datatype soundness = Sound_Modulo_Infiniteness | Sound +datatype soundness = Sound_Modulo_Infinity | Sound datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars datatype type_level = All_Types | diff -r aa35859c8741 -r ee584ff987c3 src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Sat Oct 29 12:57:43 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_util.ML Sat Oct 29 13:15:58 2011 +0200 @@ -208,20 +208,23 @@ | [] => 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) + if not sound then + (* 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. *) + (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) + else + default_card | [] => default_card) (* Very slightly unsound: Type variables are assumed not to be constrained to cardinality 1. (In practice, the user would most diff -r aa35859c8741 -r ee584ff987c3 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Oct 29 12:57:43 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Oct 29 13:15:58 2011 +0200 @@ -615,8 +615,7 @@ val num_facts = length facts |> is_none max_relevant ? Integer.min best_max_relevant - val soundness = - if sound then Sound else Sound_Modulo_Infiniteness + val soundness = if sound then Sound else Sound_Modulo_Infinity val type_enc = type_enc |> choose_type_enc soundness best_type_enc format val fairly_sound = is_type_enc_fairly_sound type_enc