# HG changeset patch # User blanchet # Date 1308669459 -7200 # Node ID bdb11c68f1421f81614f0b7e260835a699ef71bf # Parent 43326cadc31a08132ae0577659404b0e18979c2b generate type predicates for existentials/skolems, otherwise some problems might not be provable diff -r 43326cadc31a -r bdb11c68f142 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Tue Jun 21 17:17:38 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Jun 21 17:17:39 2011 +0200 @@ -1474,9 +1474,9 @@ 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 = +fun should_predicate_on_var_in_formula pos phi (SOME true) name = formula_fold pos (is_var_positively_naked_in_term name) phi false + | should_predicate_on_var_in_formula _ _ _ _ = true 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) @@ -1548,34 +1548,33 @@ end | do_formula pos (AConn conn) = aconn_map pos do_formula conn | do_formula pos (AAtom tm) = AAtom (do_term pos tm) - in do_formula o SOME end + in do_formula end fun bound_tvars type_sys Ts = mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal) (type_literals_for_types type_sys add_sorts_on_tvar Ts)) -fun formula_for_fact ctxt format nonmono_Ts type_sys - ({combformula, atomic_types, ...} : translated_formula) = - combformula - |> close_combformula_universally - |> formula_from_combformula ctxt format nonmono_Ts type_sys - is_var_nonmonotonic_in_formula true - |> bound_tvars type_sys atomic_types - |> close_formula_universally - (* Each fact is given a unique fact number to avoid name clashes (e.g., because of monomorphization). The TPTP explicitly forbids name clashes, and some of the remote provers might care. *) -fun formula_line_for_fact ctxt format prefix encode freshen nonmono_Ts type_sys - (j, formula as {name, locality, kind, ...}) = - Formula (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ - encode name, - kind, formula_for_fact ctxt format nonmono_Ts type_sys formula, NONE, - case locality of - Intro => intro_info - | Elim => elim_info - | Simp => simp_info - | _ => NONE) +fun formula_line_for_fact ctxt format prefix encode exporter nonmono_Ts type_sys + (j, {name, locality, kind, combformula, atomic_types}) = + (prefix ^ (if exporter then "" else string_of_int j ^ "_") ^ encode name, + kind, + combformula + |> close_combformula_universally + |> formula_from_combformula ctxt format nonmono_Ts type_sys + should_predicate_on_var_in_formula + (if exporter then NONE else SOME true) + |> bound_tvars type_sys atomic_types + |> close_formula_universally, + NONE, + case locality of + Intro => intro_info + | Elim => elim_info + | Simp => simp_info + | _ => NONE) + |> Formula fun formula_line_for_class_rel_clause ({name, subclass, superclass, ...} : class_rel_clause) = @@ -1604,7 +1603,7 @@ ({name, kind, combformula, atomic_types, ...} : translated_formula) = Formula (conjecture_prefix ^ name, kind, formula_from_combformula ctxt format nonmono_Ts type_sys - is_var_nonmonotonic_in_formula false + should_predicate_on_var_in_formula (SOME false) (close_combformula_universally combformula) |> bound_tvars type_sys atomic_types |> close_formula_universally, NONE, NONE) @@ -1725,7 +1724,7 @@ |> type_pred_combterm ctxt format type_sys res_T |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts) |> formula_from_combformula ctxt format poly_nonmono_Ts type_sys - (K (K (K (K true)))) true + (K (K (K (K true)))) (SOME true) |> n > 1 ? bound_tvars type_sys (atyps_of T) |> close_formula_universally |> maybe_negate, @@ -1859,7 +1858,7 @@ val explicit_apply = NONE (* for experimental purposes *) fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys - freshen_facts readable_names preproc hyp_ts concl_t facts = + exporter readable_names preproc hyp_ts concl_t facts = let val (format, type_sys) = choose_format [format] type_sys val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) = @@ -1887,7 +1886,7 @@ poly_nonmono_Ts type_sys val helper_lines = 0 upto length helpers - 1 ~~ helpers - |> map (formula_line_for_fact ctxt format helper_prefix I false + |> map (formula_line_for_fact ctxt format helper_prefix I exporter poly_nonmono_Ts type_sys) |> (if needs_type_tag_idempotence type_sys then cons (type_tag_idempotence_fact ()) @@ -1898,8 +1897,8 @@ val problem = [(explicit_declsN, sym_decl_lines), (factsN, - map (formula_line_for_fact ctxt format fact_prefix ascii_of - freshen_facts nonmono_Ts type_sys) + map (formula_line_for_fact ctxt format fact_prefix ascii_of exporter + nonmono_Ts type_sys) (0 upto length facts - 1 ~~ facts)), (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses), (aritiesN, map formula_line_for_arity_clause arity_clauses), diff -r 43326cadc31a -r bdb11c68f142 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 21 17:17:38 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 21 17:17:39 2011 +0200 @@ -646,7 +646,7 @@ val (atp_problem, pool, conjecture_offset, facts_offset, fact_names, typed_helpers, sym_tab) = prepare_atp_problem ctxt format conj_sym_kind prem_kind - type_sys true (Config.get ctxt atp_readable_names) true + type_sys false (Config.get ctxt atp_readable_names) true hyp_ts concl_t facts fun weights () = atp_problem_weights atp_problem val full_proof = debug orelse isar_proof