# HG changeset patch # User blanchet # Date 1275047361 -7200 # Node ID fc1e20373e6aa47a6f565822ca4858865d3dfc9b # Parent 38ba15040455f9fe56570295cbf323020e1cfa3b make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work diff -r 38ba15040455 -r fc1e20373e6a src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Thu May 27 17:22:16 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri May 28 13:49:21 2010 +0200 @@ -121,9 +121,8 @@ : problem) = let (* get clauses and prepare them for writing *) - val (ctxt, (chain_ths, th)) = goal; + val (ctxt, (chained_ths, th)) = goal; val thy = ProofContext.theory_of ctxt; - val chain_ths = map (Thm.put_name_hint chained_hint) chain_ths; val goal_clss = #1 (neg_conjecture_clauses ctxt th subgoal) val goal_cls = List.concat goal_clss val the_filtered_clauses = @@ -135,7 +134,7 @@ NONE => the_filtered_clauses | SOME axcls => axcls); val (internal_thm_names, clauses) = - prepare goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy; + prepare goal_cls chained_ths the_axiom_clauses the_filtered_clauses thy; (* path to unique problem file *) val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER" diff -r 38ba15040455 -r fc1e20373e6a src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu May 27 17:22:16 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri May 28 13:49:21 2010 +0200 @@ -352,7 +352,7 @@ fun subtract_cls ax_clauses = filter_out (Termtab.defined (mk_clause_table ax_clauses) o prop_of) -fun all_valid_thms respect_no_atp ctxt chain_ths = +fun all_valid_thms respect_no_atp ctxt chained_ths = let val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt); val local_facts = ProofContext.facts_of ctxt; @@ -372,12 +372,13 @@ val ths = filter_out bad_for_atp ths0; in if Facts.is_concealed facts name orelse - forall (member Thm.eq_thm chain_ths) ths orelse (respect_no_atp andalso is_package_def name) then I else case find_first check_thms [name1, name2, name] of NONE => I - | SOME a => cons (a, ths) + | SOME name' => + cons (name' |> forall (member Thm.eq_thm chained_ths) ths + ? prefix chained_prefix, ths) end); in valid_facts global_facts @ valid_facts local_facts end; @@ -397,10 +398,10 @@ (* The single-name theorems go after the multiple-name ones, so that single names are preferred when both are available. *) -fun name_thm_pairs respect_no_atp ctxt chain_ths = +fun name_thm_pairs respect_no_atp ctxt chained_ths = let val (mults, singles) = - List.partition is_multi (all_valid_thms respect_no_atp ctxt chain_ths) + List.partition is_multi (all_valid_thms respect_no_atp ctxt chained_ths) val ps = [] |> fold add_single_names singles |> fold add_multi_names mults in ps |> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end; @@ -409,11 +410,11 @@ (warning ("No name for theorem " ^ Display.string_of_thm_without_context th); false) | check_named _ = true; -fun get_all_lemmas respect_no_atp ctxt chain_ths = +fun get_all_lemmas respect_no_atp ctxt chained_ths = let val included_thms = tap (fn ths => trace_msg (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems"))) - (name_thm_pairs respect_no_atp ctxt chain_ths) + (name_thm_pairs respect_no_atp ctxt chained_ths) in filter check_named included_thms end; @@ -510,14 +511,14 @@ fun get_relevant_facts respect_no_atp relevance_threshold relevance_convergence defs_relevant max_new theory_relevant (relevance_override as {add, only, ...}) - (ctxt, (chain_ths, _)) goal_cls = + (ctxt, (chained_ths, _)) goal_cls = if (only andalso null add) orelse relevance_threshold > 1.0 then [] else let val thy = ProofContext.theory_of ctxt val is_FO = is_first_order thy goal_cls - val included_cls = get_all_lemmas respect_no_atp ctxt chain_ths + val included_cls = get_all_lemmas respect_no_atp ctxt chained_ths |> cnf_rules_pairs thy |> make_unique |> restrict_to_logic thy is_FO |> remove_unwanted_clauses @@ -529,14 +530,8 @@ (* prepare for passing to writer, create additional clauses based on the information from extra_cls *) -fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy = +fun prepare_clauses dfg goal_cls chained_ths axcls extra_cls thy = let - (* add chain thms *) - val chain_cls = - cnf_rules_pairs thy (filter check_named - (map (`Thm.get_name_hint) chain_ths)) - val axcls = chain_cls @ axcls - val extra_cls = chain_cls @ extra_cls val is_FO = is_first_order thy goal_cls val ccls = subtract_cls extra_cls goal_cls val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls diff -r 38ba15040455 -r fc1e20373e6a src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Thu May 27 17:22:16 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri May 28 13:49:21 2010 +0200 @@ -7,6 +7,7 @@ signature SLEDGEHAMMER_FACT_PREPROCESSOR = sig + val chained_prefix: string val trace: bool Unsynchronized.ref val trace_msg: (unit -> string) -> unit val skolem_prefix: string @@ -31,6 +32,9 @@ open Sledgehammer_FOL_Clause +(* Used to label theorems chained into the goal. *) +val chained_prefix = "Sledgehammer.chained_" + val trace = Unsynchronized.ref false; fun trace_msg msg = if !trace then tracing (msg ()) else (); diff -r 38ba15040455 -r fc1e20373e6a src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu May 27 17:22:16 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 28 13:49:21 2010 +0200 @@ -233,13 +233,19 @@ state) atps in () end -fun minimize override_params i fact_refs state = +fun minimize override_params i frefs state = let val thy = Proof.theory_of state val ctxt = Proof.context_of state - val theorems_from_refs = - map o pairf Facts.string_of_ref o ProofContext.get_fact - val name_thms_pairs = theorems_from_refs ctxt fact_refs + val chained_ths = #facts (Proof.goal state) + fun theorems_from_ref ctxt fref = + let + val ths = ProofContext.get_fact ctxt fref + val name = Facts.string_of_ref fref + |> forall (member Thm.eq_thm chained_ths) ths + ? prefix chained_prefix + in (name, ths) end + val name_thms_pairs = map (theorems_from_ref ctxt) frefs in case subgoal_count state of 0 => priority "No subgoal!" @@ -267,11 +273,11 @@ fun string_for_raw_param (key, values) = key ^ (case space_implode " " values of "" => "" | value => " = " ^ value) -fun minimize_command override_params i atp_name facts = +fun minimize_command override_params i atp_name fact_names = sledgehammerN ^ " " ^ minimizeN ^ " [atp = " ^ atp_name ^ (override_params |> filter is_raw_param_relevant_for_minimize |> implode o map (prefix ", " o string_for_raw_param)) ^ - "] (" ^ space_implode " " facts ^ ")" ^ + "] (" ^ space_implode " " fact_names ^ ")" ^ (if i = 1 then "" else " " ^ string_of_int i) fun hammer_away override_params subcommand opt_i relevance_override state = diff -r 38ba15040455 -r fc1e20373e6a src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu May 27 17:22:16 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri May 28 13:49:21 2010 +0200 @@ -10,7 +10,6 @@ type minimize_command = string list -> string type name_pool = Sledgehammer_FOL_Clause.name_pool - val chained_hint: string val invert_const: string -> string val invert_type_const: string -> string val num_type_args: theory -> string -> int @@ -582,9 +581,6 @@ | extract_num _ = NONE in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end -(* Used to label theorems chained into the goal. *) -val chained_hint = "sledgehammer_chained" - fun apply_command _ 1 = "by " | apply_command 1 _ = "apply " | apply_command i _ = "prefer " ^ string_of_int i ^ " apply " @@ -602,16 +598,24 @@ "To minimize the number of lemmas, try this command: " ^ Markup.markup Markup.sendback command ^ ".\n" +val unprefix_chained = perhaps (try (unprefix chained_prefix)) + fun metis_proof_text (minimize_command, atp_proof, thm_names, goal, i) = let - val lemmas = + val raw_lemmas = atp_proof |> extract_clause_numbers_in_atp_proof |> filter (is_axiom_clause_number thm_names) |> map (fn i => Vector.sub (thm_names, i - 1)) - |> filter_out (fn s => s = "??.unknown" orelse s = chained_hint) - |> sort_distinct string_ord + val (chained_lemmas, other_lemmas) = + raw_lemmas |> List.partition (String.isPrefix chained_prefix) + |>> map (unprefix chained_prefix) + |> pairself (sort_distinct string_ord) + val lemmas = other_lemmas @ chained_lemmas val n = Logic.count_prems (prop_of goal) - in (metis_line i n lemmas ^ minimize_line minimize_command lemmas, lemmas) end + in + (metis_line i n other_lemmas ^ minimize_line minimize_command lemmas, + lemmas) + end (** Isar proof construction and manipulation **) @@ -929,7 +933,7 @@ fun do_facts (ls, ss) = let val ls = ls |> sort_distinct (prod_ord string_ord int_ord) - val ss = ss |> sort_distinct string_ord + val ss = ss |> map unprefix_chained |> sort_distinct string_ord in metis_command 1 1 (map string_for_label ls @ ss) end and do_step ind (Fix xs) = do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"