# HG changeset patch # User blanchet # Date 1292408788 -3600 # Node ID 9c68004b8c9df1c7b6bdf00f76b50f074f27a2af # Parent cb1cbae54dbf48cee208eb387d04ab52345381fa added Sledgehammer support for higher-order propositional reasoning diff -r cb1cbae54dbf -r 9c68004b8c9d src/HOL/Metis.thy --- a/src/HOL/Metis.thy Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Metis.thy Wed Dec 15 11:26:28 2010 +0100 @@ -15,17 +15,26 @@ ("Tools/try.ML") begin -definition fequal :: "'a \ 'a \ bool" where [no_atp]: -"fequal X Y \ (X = Y)" +definition fFalse :: bool where [no_atp]: +"fFalse \ False" -lemma fequal_imp_equal [no_atp]: "\ fequal X Y \ X = Y" -by (simp add: fequal_def) +definition fTrue :: bool where [no_atp]: +"fTrue \ True" + +definition fNot :: "bool \ bool" where [no_atp]: +"fNot P \ \ P" -lemma equal_imp_fequal [no_atp]: "\ X = Y \ fequal X Y" -by (simp add: fequal_def) +definition fconj :: "bool \ bool \ bool" where [no_atp]: +"fconj P Q \ P \ Q" + +definition fdisj :: "bool \ bool \ bool" where [no_atp]: +"fdisj P Q \ P \ Q" -lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y" -by auto +definition fimplies :: "bool \ bool \ bool" where [no_atp]: +"fimplies P Q \ (P \ Q)" + +definition fequal :: "'a \ 'a \ bool" where [no_atp]: +"fequal x y \ (x = y)" use "Tools/Metis/metis_translate.ML" use "Tools/Metis/metis_reconstruct.ML" @@ -36,8 +45,9 @@ #> Metis_Tactics.setup *} -hide_const (open) fequal -hide_fact (open) fequal_def fequal_imp_equal equal_imp_fequal equal_imp_equal +hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal +hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def + fequal_def subsection {* Try *} diff -r cb1cbae54dbf -r 9c68004b8c9d src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Dec 15 11:26:28 2010 +0100 @@ -81,22 +81,13 @@ fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS) -fun smart_invert_const "fFalse" = @{const_name False} - | smart_invert_const "fTrue" = @{const_name True} - | smart_invert_const "fNot" = @{const_name Not} - | smart_invert_const "fconj" = @{const_name conj} - | smart_invert_const "fdisj" = @{const_name disj} - | smart_invert_const "fimplies" = @{const_name implies} - | smart_invert_const "fequal" = @{const_name HOL.eq} - | smart_invert_const s = invert_const s - fun hol_type_from_metis_term _ (Metis_Term.Var v) = (case strip_prefix_and_unascii tvar_prefix v of SOME w => make_tvar w | NONE => make_tvar v) | hol_type_from_metis_term ctxt (Metis_Term.Fn(x, tys)) = (case strip_prefix_and_unascii type_const_prefix x of - SOME tc => Type (smart_invert_const tc, + SOME tc => Type (invert_const tc, map (hol_type_from_metis_term ctxt) tys) | NONE => case strip_prefix_and_unascii tfree_prefix x of @@ -132,7 +123,7 @@ case strip_prefix_and_unascii const_prefix a of SOME b => let - val c = smart_invert_const b + val c = invert_const b val ntypes = num_type_args thy c val nterms = length ts - ntypes val tts = map tm_to_tt ts @@ -158,7 +149,7 @@ | NONE => (*Not a constant. Is it a type constructor?*) case strip_prefix_and_unascii type_const_prefix a of SOME b => - SomeType (Type (smart_invert_const b, types_of (map tm_to_tt ts))) + SomeType (Type (invert_const b, types_of (map tm_to_tt ts))) | NONE => (*Maybe a TFree. Should then check that ts=[].*) case strip_prefix_and_unascii tfree_prefix a of SOME b => SomeType (mk_tfree ctxt b) @@ -186,7 +177,7 @@ Const (@{const_name HOL.eq}, HOLogic.typeT) | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (x,[]), ty])) = (case strip_prefix_and_unascii const_prefix x of - SOME c => Const (smart_invert_const c, dummyT) + SOME c => Const (invert_const c, dummyT) | NONE => (*Not a constant. Is it a fixed variable??*) case strip_prefix_and_unascii fixed_var_prefix x of SOME v => Free (v, hol_type_from_metis_term ctxt ty) @@ -200,7 +191,7 @@ list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2]) | cvt (t as Metis_Term.Fn (x, [])) = (case strip_prefix_and_unascii const_prefix x of - SOME c => Const (smart_invert_const c, dummyT) + SOME c => Const (invert_const c, dummyT) | NONE => (*Not a constant. Is it a fixed variable??*) case strip_prefix_and_unascii fixed_var_prefix x of SOME v => Free (v, dummyT) diff -r cb1cbae54dbf -r 9c68004b8c9d src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Tools/Metis/metis_translate.ML Wed Dec 15 11:26:28 2010 +0100 @@ -74,6 +74,7 @@ val tvar_classes_of_terms : term list -> string list val type_consts_of_terms : theory -> term list -> string list val string_of_mode : mode -> string + val metis_helpers : (string * (bool * thm list)) list val prepare_metis_problem : mode -> Proof.context -> bool -> thm list -> thm list list -> mode * metis_problem @@ -130,8 +131,14 @@ (* Invert the table of translations between Isabelle and ATPs. *) val const_trans_table_inv = - Symtab.update ("fequal", @{const_name HOL.eq}) - (Symtab.make (map swap (Symtab.dest const_trans_table))) + const_trans_table |> Symtab.dest |> map swap |> Symtab.make + |> fold Symtab.update [("fFalse", @{const_name False}), + ("fTrue", @{const_name True}), + ("fNot", @{const_name Not}), + ("fconj", @{const_name conj}), + ("fdisj", @{const_name disj}), + ("fimplies", @{const_name implies}), + ("fequal", @{const_name HOL.eq})] val invert_const = perhaps (Symtab.lookup const_trans_table_inv) @@ -660,7 +667,7 @@ end end; -val helpers = +val metis_helpers = [("c_COMBI", (false, @{thms Meson.COMBI_def})), ("c_COMBK", (false, @{thms Meson.COMBK_def})), ("c_COMBB", (false, @{thms Meson.COMBB_def})), @@ -670,26 +677,20 @@ (false, @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1] fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]})), ("c_fFalse", (true, [@{lemma "x = fTrue | x = fFalse" - by (unfold Metis.fFalse_def Metis.fTrue_def) fast}])), - ("c_fFalse", (false, [@{lemma "~ fFalse" - by (unfold Metis.fFalse_def) fast}])), + by (unfold fFalse_def fTrue_def) fast}])), + ("c_fFalse", (false, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])), ("c_fTrue", (true, [@{lemma "x = fTrue | x = fFalse" - by (unfold Metis.fFalse_def Metis.fTrue_def) fast}])), - ("c_fTrue", (false, [@{lemma "fTrue" - by (unfold Metis.fTrue_def) fast}])), + by (unfold fFalse_def fTrue_def) fast}])), + ("c_fTrue", (false, [@{lemma "fTrue" by (unfold fTrue_def) fast}])), ("c_fNot", (false, @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1] fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]})), ("c_fconj", - (false, @{lemma "~ P | ~ Q | Metis.fconj P Q" - "~ Metis.fconj P Q | P" - "~ Metis.fconj P Q | Q" - by (unfold Metis.fconj_def) fast+})), + (false, @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q" + by (unfold fconj_def) fast+})), ("c_fdisj", - (false, @{lemma "~ P | Metis.fdisj P Q" - "~ Q | Metis.fdisj P Q" - "~ Metis.fdisj P Q | P | Q" - by (unfold Metis.fdisj_def) fast+})), + (false, @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q" + by (unfold fdisj_def) fast+})), ("c_fimplies", (false, @{lemma "P | Metis.fimplies P Q" "~ Q | Metis.fimplies P Q" @@ -801,10 +802,11 @@ #> `(Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq fdefs)) val helper_ths = - helpers |> filter (is_used o fst) - |> maps (fn (c, (needs_full_types, thms)) => - if needs_full_types andalso mode <> FT then [] - else map prepare_helper thms) + metis_helpers + |> filter (is_used o fst) + |> maps (fn (c, (needs_full_types, thms)) => + if needs_full_types andalso mode <> FT then [] + else map prepare_helper thms) in lmap |> fold (add_thm false) helper_ths end in (mode, add_type_thm (type_ext thy (maps (map prop_of) (cls :: thss))) lmap) diff -r cb1cbae54dbf -r 9c68004b8c9d src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Wed Dec 15 11:26:28 2010 +0100 @@ -126,7 +126,8 @@ fun using_labels [] = "" | using_labels ls = "using " ^ space_implode " " (map string_for_label ls) ^ " " -fun metis_name type_sys = if is_fully_typed type_sys then "metisFT" else "metis" +fun metis_name type_sys = + if types_dangerous_types type_sys then "metisFT" else "metis" fun metis_call type_sys ss = command_call (metis_name type_sys) ss fun metis_command type_sys i n (ls, ss) = using_labels ls ^ apply_on_subgoal i n ^ metis_call type_sys ss @@ -335,19 +336,14 @@ val term_ts = map (aux NONE []) term_us val extra_ts = map (aux NONE []) extra_us val t = - Const (c, if is_fully_typed type_sys then - case opt_T of - SOME T => map fastype_of term_ts ---> T - | NONE => - if num_type_args thy c = 0 then - Sign.const_instance thy (c, []) - else - raise Fail ("no type information for " ^ quote c) - else if num_type_args thy c = length type_us then - Sign.const_instance thy (c, - map (type_from_fo_term tfrees) type_us) - else - HOLogic.typeT) + Const (c, case opt_T of + SOME T => map fastype_of term_ts ---> T + | NONE => + if num_type_args thy c = length type_us then + Sign.const_instance thy (c, + map (type_from_fo_term tfrees) type_us) + else + HOLogic.typeT) in list_comb (t, term_ts @ extra_ts) end | NONE => (* a free or schematic variable *) let diff -r cb1cbae54dbf -r 9c68004b8c9d src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Wed Dec 15 11:26:28 2010 +0100 @@ -20,7 +20,6 @@ val precise_overloaded_args : bool Unsynchronized.ref val fact_prefix : string val conjecture_prefix : string - val is_fully_typed : type_system -> bool val types_dangerous_types : type_system -> bool val num_atp_type_args : theory -> type_system -> string -> int val translate_atp_fact : @@ -32,7 +31,7 @@ -> string problem * string Symtab.table * int * (string * 'a) list vector end; -structure Sledgehammer_ATP_Translate (*### : SLEDGEHAMMER_ATP_TRANSLATE *) = +structure Sledgehammer_ATP_Translate : SLEDGEHAMMER_ATP_TRANSLATE = struct open ATP_Problem @@ -65,10 +64,6 @@ Const_Args | No_Types -fun is_fully_typed (Tags full_types) = full_types - | is_fully_typed (Preds full_types) = full_types - | is_fully_typed _ = false - fun types_dangerous_types (Tags _) = true | types_dangerous_types (Preds _) = true | types_dangerous_types _ = false @@ -84,7 +79,7 @@ fun needs_type_args thy type_sys s = case type_sys of Tags full_types => not full_types andalso is_overloaded thy s - | Preds full_types => is_overloaded thy s (* FIXME: could be more precise *) + | Preds _ => is_overloaded thy s (* FIXME: could be more precise *) | Const_Args => is_overloaded thy s | No_Types => false @@ -100,9 +95,11 @@ | mk_ahorn (phi :: phis) psi = AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi]) -fun combformula_for_prop thy = +fun combformula_for_prop thy eq_as_iff = let - val do_term = combterm_from_term thy + fun do_term bs t ts = + combterm_from_term thy bs (Envir.eta_contract t) + |>> AAtom ||> union (op =) ts fun do_quant bs q s T t' = let val s = Name.variant (map fst bs) s in do_formula ((s, T) :: bs) t' @@ -123,9 +120,8 @@ | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2 | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2 | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 => - do_conn bs AIff t1 t2 - | _ => (fn ts => do_term bs (Envir.eta_contract t) - |>> AAtom ||> union (op =) ts) + if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t + | _ => do_term bs t in do_formula [] end val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm @@ -224,7 +220,7 @@ in perhaps (try aux) end (* making fact and conjecture formulas *) -fun make_formula ctxt presimp name kind t = +fun make_formula ctxt eq_as_iff presimp name kind t = let val thy = ProofContext.theory_of ctxt val t = t |> Envir.beta_eta_contract @@ -237,66 +233,59 @@ |> perhaps (try (HOLogic.dest_Trueprop)) |> introduce_combinators_in_term ctxt kind |> kind <> Axiom ? freeze_term - val (combformula, ctypes_sorts) = combformula_for_prop thy t [] + val (combformula, ctypes_sorts) = combformula_for_prop thy eq_as_iff t [] in {name = name, combformula = combformula, kind = kind, ctypes_sorts = ctypes_sorts} end -fun make_fact ctxt presimp ((name, _), th) = - case make_formula ctxt presimp name Axiom (prop_of th) of +fun make_fact ctxt eq_as_iff presimp ((name, _), th) = + case make_formula ctxt eq_as_iff presimp name Axiom (prop_of th) of {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE | formula => SOME formula fun make_conjecture ctxt ts = let val last = length ts - 1 in - map2 (fn j => make_formula ctxt true (Int.toString j) + map2 (fn j => make_formula ctxt true true (Int.toString j) (if j = last then Conjecture else Hypothesis)) (0 upto last) ts end (** Helper facts **) -fun count_combterm (CombConst ((s, _), _, _)) = - Symtab.map_entry s (Integer.add 1) - | count_combterm (CombVar _) = I - | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2] -fun count_combformula (AQuant (_, _, phi)) = count_combformula phi - | count_combformula (AConn (_, phis)) = fold count_combformula phis - | count_combformula (AAtom tm) = count_combterm tm -fun count_translated_formula ({combformula, ...} : translated_formula) = - count_combformula combformula - -val optional_helpers = - [(["c_COMBI"], @{thms Meson.COMBI_def}), - (["c_COMBK"], @{thms Meson.COMBK_def}), - (["c_COMBB"], @{thms Meson.COMBB_def}), - (["c_COMBC"], @{thms Meson.COMBC_def}), - (["c_COMBS"], @{thms Meson.COMBS_def})] -val optional_fully_typed_helpers = - [(["c_True", "c_False", "c_If"], @{thms True_or_False}), - (["c_If"], @{thms if_True if_False})] -val mandatory_helpers = @{thms Metis.fequal_def} +fun count_term (ATerm ((s, _), tms)) = + (if is_atp_variable s then I + else Symtab.map_entry s (Integer.add 1)) + #> fold count_term tms +fun count_formula (AQuant (_, _, phi)) = count_formula phi + | count_formula (AConn (_, phis)) = fold count_formula phis + | count_formula (AAtom tm) = count_term tm val init_counters = - [optional_helpers, optional_fully_typed_helpers] |> maps (maps fst) - |> sort_distinct string_ord |> map (rpair 0) |> Symtab.make + metis_helpers |> map fst |> sort_distinct string_ord |> map (rpair 0) + |> Symtab.make -fun get_helper_facts ctxt is_FO type_sys conjectures facts = +fun get_helper_facts ctxt type_sys formulas = let - val ct = - fold (fold count_translated_formula) [conjectures, facts] init_counters - fun is_needed c = the (Symtab.lookup ct c) > 0 - fun baptize th = ((Thm.get_name_hint th, false), th) + val no_dangerous_types = types_dangerous_types type_sys + val ct = init_counters |> fold count_formula formulas + fun is_used s = the (Symtab.lookup ct s) > 0 + fun dub c needs_full_types (th, j) = + ((c ^ "_" ^ string_of_int j ^ (if needs_full_types then "ft" else ""), + false), th) + fun make_facts eq_as_iff = map_filter (make_fact ctxt eq_as_iff false) in - (optional_helpers - |> is_fully_typed type_sys ? append optional_fully_typed_helpers - |> maps (fn (ss, ths) => - if exists is_needed ss then map baptize ths else [])) @ - (if is_FO then [] else map baptize mandatory_helpers) - |> map_filter (make_fact ctxt false) + metis_helpers + |> filter (is_used o fst) + |> maps (fn (c, (needs_full_types, ths)) => + if needs_full_types andalso not no_dangerous_types then + [] + else + ths ~~ (1 upto length ths) + |> map (dub c needs_full_types) + |> make_facts (not needs_full_types)) end -fun translate_atp_fact ctxt = `(make_fact ctxt true) +fun translate_atp_fact ctxt = `(make_fact ctxt true true) fun translate_formulas ctxt type_sys hyp_ts concl_t rich_facts = let @@ -311,20 +300,18 @@ boost an ATP's performance (for some reason). *) val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts) val goal_t = Logic.list_implies (hyp_ts, concl_t) - val is_FO = Meson.is_fol_term thy goal_t val subs = tfree_classes_of_terms [goal_t] val supers = tvar_classes_of_terms fact_ts val tycons = type_consts_of_terms thy (goal_t :: fact_ts) (* TFrees in the conjecture; TVars in the facts *) val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t]) - val helper_facts = get_helper_facts ctxt is_FO type_sys conjectures facts val (supers', arity_clauses) = if type_sys = No_Types then ([], []) else make_arity_clauses thy tycons supers val class_rel_clauses = make_class_rel_clauses thy subs supers' in (fact_names |> map single |> Vector.fromList, - (conjectures, facts, helper_facts, class_rel_clauses, arity_clauses)) + (conjectures, facts, class_rel_clauses, arity_clauses)) end fun tag_with_type ty t = ATerm (`I type_tag_name, [ty, t]) @@ -352,7 +339,7 @@ | is_dtyp_dangerous _ (Datatype_Aux.DtRec _) = false and is_type_dangerous ctxt (Type (s, Ts)) = is_type_constr_dangerous ctxt s andalso forall (is_type_dangerous ctxt) Ts - | is_type_dangerous ctxt _ = false + | is_type_dangerous _ _ = false and is_type_constr_dangerous ctxt s = let val thy = ProofContext.theory_of ctxt in case Datatype_Data.get_info thy s of @@ -376,6 +363,15 @@ full_types orelse is_combtyp_dangerous ctxt ty | should_tag_with_type _ _ _ = false +val fname_table = + [("c_False", (0, ("c_fFalse", @{const_name Metis.fFalse}))), + ("c_True", (0, ("c_fTrue", @{const_name Metis.fTrue}))), + ("c_Not", (1, ("c_fNot", @{const_name Metis.fNot}))), + ("c_conj", (2, ("c_fconj", @{const_name Metis.fconj}))), + ("c_disj", (2, ("c_fdisj", @{const_name Metis.fdisj}))), + ("c_implies", (2, ("c_fimplies", @{const_name Metis.fimplies}))), + ("equal", (2, ("c_fequal", @{const_name Metis.fequal})))] + fun fo_term_for_combterm ctxt type_sys = let val thy = ProofContext.theory_of ctxt @@ -385,27 +381,27 @@ val (x, ty_args) = case head of CombConst (name as (s, s'), _, ty_args) => - (case strip_prefix_and_unascii const_prefix s of - NONE => - if s = "equal" then - if top_level andalso length args = 2 then (name, []) - else (("c_fequal", @{const_name Metis.fequal}), ty_args) - else - (name, ty_args) - | SOME s'' => - let - val s'' = invert_const s'' - val ty_args = - if needs_type_args thy type_sys s'' then ty_args else [] - in - if top_level then - case s of - "c_False" => (("$false", s'), []) - | "c_True" => (("$true", s'), []) - | _ => (name, ty_args) - else - (name, ty_args) - end) + (case AList.lookup (op =) fname_table s of + SOME (n, fname) => + if top_level andalso length args = n then (name, []) + else (fname, ty_args) + | NONE => + case strip_prefix_and_unascii const_prefix s of + NONE => (name, ty_args) + | SOME s'' => + let + val s'' = invert_const s'' + val ty_args = + if needs_type_args thy type_sys s'' then ty_args else [] + in + if top_level then + case s of + "c_False" => (("$false", s'), []) + | "c_True" => (("$true", s'), []) + | _ => (name, ty_args) + else + (name, ty_args) + end) | CombVar (name, _) => (name, []) | CombApp _ => raise Fail "impossible \"CombApp\"" val t = @@ -498,9 +494,14 @@ fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi fun consider_problem problem = fold (fold consider_problem_line o snd) problem +(* needed for helper facts if the problem otherwise does not involve equality *) +val equal_entry = ("equal", {min_arity = 2, max_arity = 2, sub_level = false}) + fun const_table_for_problem explicit_apply problem = - if explicit_apply then NONE - else SOME (Symtab.empty |> consider_problem problem) + if explicit_apply then + NONE + else + SOME (Symtab.empty |> Symtab.update equal_entry |> consider_problem problem) fun min_arity_of thy type_sys NONE s = (if s = "equal" orelse s = type_tag_name orelse @@ -561,14 +562,14 @@ not sub_level andalso min_arity = max_arity | NONE => false -fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) = +fun repair_predicates_in_term pred_const_tab (t as ATerm ((s, _), ts)) = if s = type_tag_name then case ts of [_, t' as ATerm ((s', _), _)] => - if is_predicate const_tab s' then t' else boolify t + if is_predicate pred_const_tab s' then t' else boolify t | _ => raise Fail "malformed type tag" else - t |> not (is_predicate const_tab s) ? boolify + t |> not (is_predicate pred_const_tab s) ? boolify fun close_universally phi = let @@ -586,33 +587,28 @@ fun repair_formula thy explicit_forall type_sys const_tab = let + val pred_const_tab = case type_sys of Tags _ => NONE | _ => const_tab fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) | aux (AConn (c, phis)) = AConn (c, map aux phis) | aux (AAtom tm) = AAtom (tm |> repair_applications_in_term thy type_sys const_tab - |> repair_predicates_in_term const_tab) + |> repair_predicates_in_term pred_const_tab) in aux #> explicit_forall ? close_universally end fun repair_problem_line thy explicit_forall type_sys const_tab (Fof (ident, kind, phi)) = Fof (ident, kind, repair_formula thy explicit_forall type_sys const_tab phi) -fun repair_problem_with_const_table thy = - map o apsnd o map ooo repair_problem_line thy +fun repair_problem thy = map o apsnd o map ooo repair_problem_line thy -fun repair_problem thy explicit_forall type_sys explicit_apply problem = - repair_problem_with_const_table thy explicit_forall type_sys - (const_table_for_problem explicit_apply problem) problem +fun dest_Fof (Fof z) = z fun prepare_atp_problem ctxt readable_names explicit_forall type_sys explicit_apply hyp_ts concl_t facts = let val thy = ProofContext.theory_of ctxt - val (fact_names, (conjectures, facts, helper_facts, class_rel_clauses, - arity_clauses)) = + val (fact_names, (conjectures, facts, class_rel_clauses, arity_clauses)) = translate_formulas ctxt type_sys hyp_ts concl_t facts val fact_lines = map (problem_line_for_fact ctxt fact_prefix type_sys) facts - val helper_lines = - map (problem_line_for_fact ctxt helper_prefix type_sys) helper_facts val conjecture_lines = map (problem_line_for_conjecture ctxt type_sys) conjectures val tfree_lines = problem_lines_for_free_types type_sys conjectures @@ -625,11 +621,21 @@ [("Relevant facts", fact_lines), ("Class relationships", class_rel_lines), ("Arity declarations", arity_lines), - ("Helper facts", helper_lines), + ("Helper facts", []), ("Conjectures", conjecture_lines), ("Type variables", tfree_lines)] - |> repair_problem thy explicit_forall type_sys explicit_apply - val (problem, pool) = nice_atp_problem readable_names problem + val const_tab = const_table_for_problem explicit_apply problem + val problem = + problem |> repair_problem thy explicit_forall type_sys const_tab + val helper_facts = + get_helper_facts ctxt type_sys (maps (map (#3 o dest_Fof) o snd) problem) + val helper_lines = + helper_facts + |> map (problem_line_for_fact ctxt helper_prefix type_sys + #> repair_problem_line thy explicit_forall type_sys const_tab) + val (problem, pool) = + problem |> AList.update (op =) ("Helper facts", helper_lines) + |> nice_atp_problem readable_names val conjecture_offset = length fact_lines + length class_rel_lines + length arity_lines + length helper_lines diff -r cb1cbae54dbf -r 9c68004b8c9d src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Dec 15 11:26:28 2010 +0100 @@ -233,6 +233,8 @@ | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 => fold (do_term_or_formula T) [t1, t2] | @{const Trueprop} $ t1 => do_formula pos t1 + | @{const False} => I + | @{const True} => I | @{const Not} $ t1 => do_formula (flip pos) t1 | Const (@{const_name All}, _) $ Abs (_, T, t') => do_quantifier (pos = SOME false) T t' diff -r cb1cbae54dbf -r 9c68004b8c9d src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Dec 15 11:26:28 2010 +0100 @@ -127,11 +127,12 @@ #default_max_relevant (get_atp thy name) end -(* These are typically simplified away by "Meson.presimplify". Equality is - handled specially via "fequal". *) +(* These are either simplified away by "Meson.presimplify" (most of the time) or + handled specially via "fFalse", "fTrue", ..., "fequal". *) val atp_irrelevant_consts = - [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}, - @{const_name HOL.eq}] + [@{const_name False}, @{const_name True}, @{const_name Not}, + @{const_name conj}, @{const_name disj}, @{const_name implies}, + @{const_name HOL.eq}, @{const_name If}, @{const_name Let}] fun is_built_in_const_for_prover ctxt name (s, T) args = if is_smt_prover ctxt name then SMT_Builtin.is_builtin_ext ctxt (s, T) args