# HG changeset patch # User wenzelm # Date 1308314124 -7200 # Node ID eeba70379f1a35d5a4ff0945c76f2d5791d428f9 # Parent 717880e98e6b550129548fb0c896afde62aa0e50# Parent a26e514c92b29c1c9e9a77c2051f1aa09f3446ba merged diff -r a26e514c92b2 -r eeba70379f1a src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Fri Jun 17 14:31:13 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Fri Jun 17 14:35:24 2011 +0200 @@ -317,6 +317,7 @@ AConn (c, [opn pos1 phi1, opn pos2 phi2]) end | opn _ (AAtom t) = AAtom (t |> conj ? open_conjecture_term) + | opn _ phi = phi in opn (SOME (not conj)) end fun open_formula_line (Formula (ident, kind, phi, source, info)) = Formula (ident, kind, open_formula (kind = Conjecture) phi, source, info) diff -r a26e514c92b2 -r eeba70379f1a src/HOL/Tools/ATP/atp_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_reconstruct.ML Fri Jun 17 14:31:13 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Fri Jun 17 14:35:24 2011 +0200 @@ -215,7 +215,7 @@ union (op =) (resolve_fact facts_offset fact_names name) | add_fact ctxt _ _ (Inference (_, _, deps)) = if AList.defined (op =) deps leo2_ext then - insert (op =) (ext_name ctxt, General (* or Chained... *)) + insert (op =) (ext_name ctxt, Extensionality) else I | add_fact _ _ _ _ = I diff -r a26e514c92b2 -r eeba70379f1a src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Fri Jun 17 14:31:13 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Fri Jun 17 14:35:24 2011 +0200 @@ -40,7 +40,9 @@ CombVar of name * typ | CombApp of combterm * combterm - datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained + datatype locality = + General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum | + Chained datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic datatype type_level = @@ -534,7 +536,9 @@ |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T)) | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs" -datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained +datatype locality = + General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum | + Chained (* (quasi-)underapproximation of the truth *) fun is_locality_global Local = false @@ -1357,7 +1361,7 @@ (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^ (if needs_fairly_sound then typed_helper_suffix else untyped_helper_suffix), - General), + Helper), let val t = th |> prop_of in t |> should_specialize_helper type_sys t ? (case types of @@ -1467,12 +1471,12 @@ CombApp (CombConst (type_pred, T --> @{typ bool}, [T]) |> enforce_type_arg_policy_in_combterm ctxt format type_sys, tm) -fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum - | var_occurs_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum = +fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum + | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum = accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, []))) fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false | is_var_nonmonotonic_in_formula pos phi _ name = - formula_fold pos (var_occurs_positively_naked_in_term name) phi false + formula_fold pos (is_var_positively_naked_in_term name) phi false fun mk_const_aterm format type_sys x T_args args = ATerm (x, map_filter (fo_term_for_type_arg format type_sys) T_args @ args) @@ -1652,11 +1656,6 @@ ? (fold (add_fact true) conjs #> fold (add_fact false) facts) end -(* These types witness that the type classes they belong to allow infinite - models and hence that any types with these type classes is monotonic. *) -val known_infinite_types = - [@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}] - (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it out with monotonicity" paper presented at CADE 2011. *) fun add_combterm_nonmonotonic_types _ _ _ (SOME false) _ = I @@ -1667,7 +1666,7 @@ (case level of Noninf_Nonmono_Types => not (is_locality_global locality) orelse - not (is_type_surely_infinite ctxt known_infinite_types T) + not (is_type_surely_infinite ctxt T) | Fin_Nonmono_Types => is_type_surely_finite ctxt T | _ => true)) ? insert_type ctxt I (deep_freeze_type T) | add_combterm_nonmonotonic_types _ _ _ _ _ = I diff -r a26e514c92b2 -r eeba70379f1a src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Fri Jun 17 14:31:13 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_util.ML Fri Jun 17 14:35:24 2011 +0200 @@ -22,7 +22,7 @@ Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp -> typ val is_type_surely_finite : Proof.context -> typ -> bool - val is_type_surely_infinite : Proof.context -> typ list -> 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_prop : term -> term @@ -136,70 +136,64 @@ 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 assigns T = +fun tiny_card_of_type ctxt 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 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 - (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 *) - | Type ("Int.int", []) => 0 (* optimization *) - | Type (s, _) => - (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) - (* 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 _ => default_card + 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 *) + | Type ("Int.int", []) => 0 (* optimization *) + | Type (s, _) => + (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) + (* 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 + | TVar _ => 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 infinite_Ts T = - tiny_card_of_type ctxt 1 (map (rpair 0) infinite_Ts) T = 0 +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 = map_types (map_type_tvar (fn v => diff -r a26e514c92b2 -r eeba70379f1a src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Fri Jun 17 14:31:13 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Fri Jun 17 14:35:24 2011 +0200 @@ -141,9 +141,11 @@ in (ths, (0, [])) |-> fold (fn th => fn (j, rest) => - (j + 1, ((nth_name j, - if member Thm.eq_thm_prop chained_ths th then Chained - else General), th) :: rest)) + (j + 1, + ((nth_name j, + if member Thm.eq_thm_prop chained_ths th then Chained + else if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality + else General), th) :: rest)) |> snd end @@ -479,13 +481,13 @@ chained_const_irrel_weight (irrel_weight_for fudge) swap const_tab chained_const_tab -fun locality_bonus (_ : relevance_fudge) General = 0.0 - | locality_bonus {intro_bonus, ...} Intro = intro_bonus +fun locality_bonus ({intro_bonus, ...} : relevance_fudge) Intro = intro_bonus | locality_bonus {elim_bonus, ...} Elim = elim_bonus | locality_bonus {simp_bonus, ...} Simp = simp_bonus | locality_bonus {local_bonus, ...} Local = local_bonus | locality_bonus {assum_bonus, ...} Assum = assum_bonus | locality_bonus {chained_bonus, ...} Chained = chained_bonus + | locality_bonus _ _ = 0.0 fun is_odd_const_name s = s = abs_name orelse String.isPrefix skolem_prefix s orelse @@ -827,7 +829,10 @@ if is_chained th then Chained else if global then - Termtab.lookup clasimpset_table (prop_of th) |> the_default General + case Termtab.lookup clasimpset_table (prop_of th) of + SOME loc => loc + | NONE => if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality + else General else if is_assum th then Assum else Local fun is_good_unnamed_local th =