--- 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
--- 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
--- 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"
--- 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 = "\<midarrow>")
@@ -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 =
--- 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
--- 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
--- 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 ();
--- 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 =
--- 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"