# HG changeset patch # User blanchet # Date 1275058838 -7200 # Node ID 365f2296ae5bb2a09ff4a7b9bcfb8a2951f589be # Parent 5610d9097caea2f273666f55e94833496eae28db# Parent fc1e20373e6aa47a6f565822ca4858865d3dfc9b merged diff -r 5610d9097cae -r 365f2296ae5b doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Fri May 28 13:37:47 2010 +0200 +++ b/doc-src/Nitpick/nitpick.tex Fri May 28 17:00:38 2010 +0200 @@ -2226,9 +2226,8 @@ sometimes helpful when investigating why a counterexample is genuine, but they can clutter the output. -\opfalse{show\_all}{dont\_show\_all} -Enabling this option effectively enables \textit{show\_datatypes} and -\textit{show\_consts}. +\opnodefault{show\_all}{bool} +Abbreviation for \textit{show\_datatypes} and \textit{show\_consts}. \opdefault{max\_potential}{int}{$\mathbf{1}$} Specifies the maximum number of potential counterexamples to display. Setting diff -r 5610d9097cae -r 365f2296ae5b src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Fri May 28 13:37:47 2010 +0200 +++ b/src/HOL/Library/Multiset.thy Fri May 28 17:00:38 2010 +0200 @@ -1699,7 +1699,6 @@ by (fact multiset_order.less_asym) ML {* -(* Proof.context -> string -> (typ -> term list) -> typ -> term -> term *) fun multiset_postproc _ maybe_name all_values (T as Type (_, [elem_T])) (Const _ $ t') = let @@ -1727,4 +1726,4 @@ Nitpick.register_term_postprocessor @{typ "'a multiset"} multiset_postproc *} -end \ No newline at end of file +end diff -r 5610d9097cae -r 365f2296ae5b src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri May 28 13:37:47 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri May 28 17:00:38 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 5610d9097cae -r 365f2296ae5b src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri May 28 13:37:47 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri May 28 17:00:38 2010 +0200 @@ -62,7 +62,6 @@ ("debug", "false"), ("verbose", "false"), ("overlord", "false"), - ("show_all", "false"), ("show_datatypes", "false"), ("show_consts", "false"), ("format", "1"), @@ -91,7 +90,6 @@ ("no_debug", "debug"), ("quiet", "verbose"), ("no_overlord", "overlord"), - ("dont_show_all", "show_all"), ("hide_datatypes", "show_datatypes"), ("hide_consts", "show_consts"), ("trust_potential", "check_potential"), @@ -100,7 +98,7 @@ fun is_known_raw_param s = AList.defined (op =) default_default_params s orelse AList.defined (op =) negated_params s orelse - s = "max" orelse s = "eval" orelse s = "expect" orelse + s = "max" orelse s = "show_all" orelse s = "eval" orelse s = "expect" orelse exists (fn p => String.isPrefix (p ^ " ") s) ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize", "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format"] @@ -115,14 +113,17 @@ else if String.isPrefix "non_" name then SOME (unprefix "non_" name) else NONE | some_name => some_name -fun unnegate_raw_param (name, value) = +fun normalize_raw_param (name, value) = case unnegate_param_name name of - SOME name' => (name', case value of - ["false"] => ["true"] - | ["true"] => ["false"] - | [] => ["false"] - | _ => value) - | NONE => (name, value) + SOME name' => [(name', case value of + ["false"] => ["true"] + | ["true"] => ["false"] + | [] => ["false"] + | _ => value)] + | NONE => if name = "show_all" then + [("show_datatypes", value), ("show_consts", value)] + else + [(name, value)] structure Data = Theory_Data( type T = raw_param list @@ -130,7 +131,8 @@ val extend = I fun merge (x, y) = AList.merge (op =) (K true) (x, y)) -val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param +val set_default_raw_param = + Data.map o fold (AList.update (op =)) o normalize_raw_param val default_raw_params = Data.get fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\") @@ -145,7 +147,7 @@ fun extract_params ctxt auto default_params override_params = let - val override_params = map unnegate_raw_param override_params + val override_params = maps normalize_raw_param override_params val raw_params = rev override_params @ rev default_params val lookup = Option.map stringify_raw_param_value o AList.lookup (op =) raw_params @@ -250,9 +252,8 @@ val timeout = if auto then NONE else lookup_time "timeout" val tac_timeout = lookup_time "tac_timeout" val max_threads = Int.max (0, lookup_int "max_threads") - val show_all = debug orelse lookup_bool "show_all" - val show_datatypes = show_all orelse lookup_bool "show_datatypes" - val show_consts = show_all orelse lookup_bool "show_consts" + val show_datatypes = debug orelse lookup_bool "show_datatypes" + val show_consts = debug orelse lookup_bool "show_consts" val formats = lookup_ints_assigns read_term_polymorphic "format" 0 val evals = lookup_term_list "eval" val max_potential = diff -r 5610d9097cae -r 365f2296ae5b src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Fri May 28 13:37:47 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Fri May 28 17:00:38 2010 +0200 @@ -587,7 +587,7 @@ | term_for_rep _ seen (Type (@{type_name fun}, [T1, T2])) T' (Vect (k, R')) [js] = term_for_vect seen k R' T1 T2 T' js - | term_for_rep _ seen (Type (@{type_name fun}, [T1, T2])) T' + | term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T' (Func (R1, Formula Neut)) jss = let val jss1 = all_combinations_for_rep R1 @@ -596,7 +596,7 @@ map (fn js => term_for_rep true seen T2 T2 (Atom (2, 0)) [[int_from_bool (member (op =) jss js)]]) jss1 - in make_fun false T1 T2 T' ts1 ts2 end + in make_fun maybe_opt T1 T2 T' ts1 ts2 end | term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T' (Func (R1, R2)) jss = let diff -r 5610d9097cae -r 365f2296ae5b src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri May 28 13:37:47 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri May 28 17:00:38 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 5610d9097cae -r 365f2296ae5b src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri May 28 13:37:47 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri May 28 17:00:38 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 5610d9097cae -r 365f2296ae5b src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 28 13:37:47 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 28 17:00:38 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 5610d9097cae -r 365f2296ae5b src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri May 28 13:37:47 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri May 28 17:00:38 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"