--- a/NEWS Tue Feb 08 17:36:21 2011 +0100
+++ b/NEWS Tue Feb 08 17:38:43 2011 +0100
@@ -14,6 +14,13 @@
without proper multithreading and TimeLimit implementation.
+*** HOL ***
+
+* Sledgehammer:
+ sledgehammer available_provers ~> sledgehammer supported_provers
+ INCOMPATIBILITY.
+
+
*** Document preparation ***
* New term style "isub" as ad-hoc conversion of variables x1, y23 into
--- a/doc-src/IsarRef/IsaMakefile Tue Feb 08 17:36:21 2011 +0100
+++ b/doc-src/IsarRef/IsaMakefile Tue Feb 08 17:38:43 2011 +0100
@@ -31,8 +31,10 @@
@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
Thy/document/pdfsetup.sty Thy/document/session.tex
+HOLCF:
+ @cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOLCF
-HOLCF-IsarRef: $(LOG)/HOLCF-IsarRef.gz
+HOLCF-IsarRef: HOLCF $(LOG)/HOLCF-IsarRef.gz
$(LOG)/HOLCF-IsarRef.gz: Thy/ROOT-HOLCF.ML ../antiquote_setup.ML \
Thy/HOLCF_Specific.thy
@@ -40,8 +42,10 @@
@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
Thy/document/pdfsetup.sty Thy/document/session.tex
+ZF:
+ @cd $(SRC)/ZF; $(ISABELLE_TOOL) make ZF
-ZF-IsarRef: $(LOG)/ZF-IsarRef.gz
+ZF-IsarRef: ZF $(LOG)/ZF-IsarRef.gz
$(LOG)/ZF-IsarRef.gz: Thy/ROOT-ZF.ML ../antiquote_setup.ML \
Thy/ZF_Specific.thy
--- a/doc-src/Sledgehammer/sledgehammer.tex Tue Feb 08 17:36:21 2011 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Feb 08 17:38:43 2011 +0100
@@ -303,9 +303,10 @@
due to Sledgehammer's asynchronous nature. The \textit{num} argument specifies a
limit on the number of messages to display (5 by default).
-\item[$\bullet$] \textbf{\textit{available\_provers}:} Prints the list of
-installed provers. See \S\ref{installation} and \S\ref{mode-of-operation} for
-more information on how to install automatic provers.
+\item[$\bullet$] \textbf{\textit{supported\_provers}:} Prints the list of
+automatic provers supported by Sledgehammer. See \S\ref{installation} and
+\S\ref{mode-of-operation} for more information on how to install automatic
+provers.
\item[$\bullet$] \textbf{\textit{running\_provers}:} Prints information about
currently running automatic provers, including elapsed runtime and remaining
--- a/src/HOL/Library/While_Combinator.thy Tue Feb 08 17:36:21 2011 +0100
+++ b/src/HOL/Library/While_Combinator.thy Tue Feb 08 17:38:43 2011 +0100
@@ -127,5 +127,21 @@
apply blast
done
+text{* Proving termination: *}
+
+theorem wf_while_option_Some:
+ assumes wf: "wf {(t, s). b s \<and> t = c s}"
+ shows "EX t. while_option b c s = Some t"
+using wf
+apply (induct s)
+apply simp
+apply (subst while_option_unfold)
+apply simp
+done
+
+theorem measure_while_option_Some: fixes f :: "'s \<Rightarrow> nat"
+shows "(!!s. b s \<Longrightarrow> f(c s) < f s) \<Longrightarrow> EX t. while_option b c s = Some t"
+by(erule wf_while_option_Some[OF wf_if_measure])
+
end
--- a/src/HOL/Smallcheck.thy Tue Feb 08 17:36:21 2011 +0100
+++ b/src/HOL/Smallcheck.thy Tue Feb 08 17:38:43 2011 +0100
@@ -113,7 +113,12 @@
definition
"full_small f d = full_small (%(x, t1). full_small (%(y, t2). f ((x, y),
- %u. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))) d) d"
+ %u. let T1 = (Typerep.typerep (TYPE('a)));
+ T2 = (Typerep.typerep (TYPE('b)))
+ in Code_Evaluation.App (Code_Evaluation.App (
+ Code_Evaluation.Const (STR ''Product_Type.Pair'')
+ (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]]))
+ (t1 ())) (t2 ()))) d) d"
instance ..
@@ -229,11 +234,23 @@
begin
definition
- "check_all f = check_all (%(x, t1). check_all (%(y, t2). f ((x, y), %_. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))))"
+ "check_all f = check_all (%(x, t1). check_all (%(y, t2). f ((x, y),
+ %u. let T1 = (Typerep.typerep (TYPE('a)));
+ T2 = (Typerep.typerep (TYPE('b)))
+ in Code_Evaluation.App (Code_Evaluation.App (
+ Code_Evaluation.Const (STR ''Product_Type.Pair'')
+ (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]]))
+ (t1 ())) (t2 ()))))"
definition enum_term_of_prod :: "('a * 'b) itself => unit => term list"
where
- "enum_term_of_prod = (%_ _. map (%(x, y). Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) x) y) (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))"
+ "enum_term_of_prod = (%_ _. map (%(x, y).
+ let T1 = (Typerep.typerep (TYPE('a)));
+ T2 = (Typerep.typerep (TYPE('b)))
+ in Code_Evaluation.App (Code_Evaluation.App (
+ Code_Evaluation.Const (STR ''Product_Type.Pair'')
+ (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]])) x) y)
+ (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ()))) "
instance ..
@@ -244,13 +261,30 @@
begin
definition
- "check_all f = (case check_all (%(a, t). f (Inl a, %_. Code_Evaluation.App (Code_Evaluation.term_of (Inl :: 'a => 'a + 'b)) (t ()))) of Some x' => Some x'
- | None => check_all (%(b, t). f (Inr b, %_. Code_Evaluation.App (Code_Evaluation.term_of (Inr :: 'b => 'a + 'b)) (t ()))))"
+ "check_all f = (case check_all (%(a, t). f (Inl a, %_.
+ let T1 = (Typerep.typerep (TYPE('a)));
+ T2 = (Typerep.typerep (TYPE('b)))
+ in Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'')
+ (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])) (t ()))) of Some x' => Some x'
+ | None => check_all (%(b, t). f (Inr b, %_. let
+ T1 = (Typerep.typerep (TYPE('a)));
+ T2 = (Typerep.typerep (TYPE('b)))
+ in Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'')
+ (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])) (t ()))))"
definition enum_term_of_sum :: "('a + 'b) itself => unit => term list"
where
- "enum_term_of_sum = (%_ _. map (Code_Evaluation.App (Code_Evaluation.term_of (Inl :: 'a => ('a + 'b)))) (enum_term_of (TYPE('a)) ()) @
- map (Code_Evaluation.App (Code_Evaluation.term_of (Inr :: 'b => ('a + 'b)))) (enum_term_of (TYPE('b)) ()))"
+ "enum_term_of_sum = (%_ _.
+ let
+ T1 = (Typerep.typerep (TYPE('a)));
+ T2 = (Typerep.typerep (TYPE('b)))
+ in
+ map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'')
+ (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
+ (enum_term_of (TYPE('a)) ()) @
+ map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'')
+ (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
+ (enum_term_of (TYPE('b)) ()))"
instance ..
@@ -312,7 +346,8 @@
definition enum_term_of_option :: "'a option itself => unit => term list"
where
- "enum_term_of_option = (% _ _. (Code_Evaluation.term_of (None :: 'a option)) # (map (Code_Evaluation.App (Code_Evaluation.term_of (Some :: 'a => 'a option))) (enum_term_of (TYPE('a)) ())))"
+ "enum_term_of_option = (% _ _. (Code_Evaluation.term_of (None :: 'a option)) # (map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Option.option.Some'')
+ (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a), Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]]))) (enum_term_of (TYPE('a)) ())))"
instance ..
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Feb 08 17:36:21 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Feb 08 17:38:43 2011 +0100
@@ -20,10 +20,16 @@
explicit_forall: bool,
use_conjecture_for_hypotheses: bool}
+ datatype e_weight_method = E_Auto | E_Fun_Weight | E_Sym_Offset_Weight
+
(* for experimentation purposes -- do not use in production code *)
- val e_weights : bool Unsynchronized.ref
- val e_weight_factor : real Unsynchronized.ref
- val e_default_weight : real Unsynchronized.ref
+ val e_weight_method : e_weight_method Unsynchronized.ref
+ val e_default_fun_weight : real Unsynchronized.ref
+ val e_fun_weight_base : real Unsynchronized.ref
+ val e_fun_weight_factor : real Unsynchronized.ref
+ val e_default_sym_offs_weight : real Unsynchronized.ref
+ val e_sym_offs_weight_base : real Unsynchronized.ref
+ val e_sym_offs_weight_factor : real Unsynchronized.ref
val eN : string
val spassN : string
@@ -33,7 +39,7 @@
val remote_prefix : string
val add_atp : string * atp_config -> theory -> theory
val get_atp : theory -> string -> atp_config
- val available_atps : theory -> string list
+ val supported_atps : theory -> string list
val is_atp_installed : theory -> string -> bool
val refresh_systems_on_tptp : unit -> unit
val setup : theory -> theory
@@ -95,28 +101,46 @@
val tstp_proof_delims =
("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
-val e_weights = Unsynchronized.ref true
-val e_weight_factor = Unsynchronized.ref 40.0
-val e_default_weight = Unsynchronized.ref 0.5
+datatype e_weight_method = E_Auto | E_Fun_Weight | E_Sym_Offset_Weight
+
+val e_weight_method = Unsynchronized.ref E_Fun_Weight
+val e_default_fun_weight = Unsynchronized.ref 0.5
+val e_fun_weight_base = Unsynchronized.ref 0.0
+val e_fun_weight_factor = Unsynchronized.ref 40.0
+val e_default_sym_offs_weight = Unsynchronized.ref 0.0
+val e_sym_offs_weight_base = Unsynchronized.ref ~30.0
+val e_sym_offs_weight_factor = Unsynchronized.ref ~30.0
+
+fun e_weight_method_case fw sow =
+ case !e_weight_method of
+ E_Auto => raise Fail "Unexpected \"E_Auto\""
+ | E_Fun_Weight => fw
+ | E_Sym_Offset_Weight => sow
+
+fun scaled_e_weight w =
+ e_weight_method_case (!e_fun_weight_base) (!e_sym_offs_weight_base)
+ + w * e_weight_method_case (!e_fun_weight_factor) (!e_sym_offs_weight_factor)
+ |> Real.ceil |> signed_string_of_int
fun e_weight_arguments weights =
- if !e_weights andalso string_ord (getenv "E_VERSION", "1.2w") <> LESS then
+ if !e_weight_method = E_Auto orelse
+ string_ord (getenv "E_VERSION", "1.2w") = LESS then
+ "-xAutoDev"
+ else
"--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
\--destructive-er-aggressive --destructive-er --presat-simplify \
\--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
\--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \
- \-H'(4*FunWeight(SimulateSOS, " ^
- string_of_int (Real.ceil (!e_default_weight * !e_weight_factor)) ^
+ \-H'(4*" ^ e_weight_method_case "FunWeight" "SymOffsetWeight" ^
+ "(SimulateSOS, " ^
+ scaled_e_weight (e_weight_method_case (!e_default_fun_weight)
+ (!e_default_sym_offs_weight)) ^
",20,1.5,1.5,1" ^
- (weights ()
- |> map (fn (s, w) => "," ^ s ^ ":" ^
- string_of_int (Real.ceil (w * !e_weight_factor)))
- |> implode) ^
+ (weights () |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight w)
+ |> implode) ^
"),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
\1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
\FIFOWeight(PreferProcessed))'"
- else
- "-xAutoDev"
val e_config : atp_config =
{exec = ("E_HOME", "eproof"),
@@ -283,7 +307,7 @@
the (Symtab.lookup (Data.get thy) name) |> fst
handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
-val available_atps = Symtab.keys o Data.get
+val supported_atps = Symtab.keys o Data.get
fun is_atp_installed thy name =
let val {exec, required_execs, ...} = get_atp thy name in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Tue Feb 08 17:36:21 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Tue Feb 08 17:38:43 2011 +0100
@@ -681,5 +681,6 @@
|> add_conjectures_weights (these (AList.lookup (op =) problem conjsN))
|> add_facts_weights (these (AList.lookup (op =) problem factsN))
|> Symtab.dest
+ |> sort (prod_ord Real.compare string_ord o pairself swap)
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Feb 08 17:36:21 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Feb 08 17:38:43 2011 +0100
@@ -113,7 +113,7 @@
fun is_prover_list ctxt s =
case space_explode " " s of
- ss as _ :: _ => forall (is_prover_available ctxt) ss
+ ss as _ :: _ => forall (is_prover_supported ctxt) ss
| _ => false
fun check_and_repair_raw_param ctxt (name, value) =
@@ -141,23 +141,23 @@
fun merge data : T = AList.merge (op =) (K true) data
)
-fun remotify_prover_if_available_and_not_already_remote ctxt name =
+fun remotify_prover_if_supported_and_not_already_remote ctxt name =
if String.isPrefix remote_prefix name then
SOME name
else
let val remote_name = remote_prefix ^ name in
- if is_prover_available ctxt remote_name then SOME remote_name else NONE
+ if is_prover_supported ctxt remote_name then SOME remote_name else NONE
end
fun remotify_prover_if_not_installed ctxt name =
- if is_prover_available ctxt name andalso is_prover_installed ctxt name then
+ if is_prover_supported ctxt name andalso is_prover_installed ctxt name then
SOME name
else
- remotify_prover_if_available_and_not_already_remote ctxt name
+ remotify_prover_if_supported_and_not_already_remote ctxt name
fun avoid_too_many_local_threads _ _ [] = []
| avoid_too_many_local_threads ctxt 0 provers =
- map_filter (remotify_prover_if_available_and_not_already_remote ctxt)
+ map_filter (remotify_prover_if_supported_and_not_already_remote ctxt)
provers
| avoid_too_many_local_threads ctxt n (prover :: provers) =
let val n = if String.isPrefix remote_prefix prover then n else n - 1 in
@@ -270,7 +270,7 @@
val runN = "run"
val minimizeN = "minimize"
val messagesN = "messages"
-val available_proversN = "available_provers"
+val supported_proversN = "supported_provers"
val running_proversN = "running_provers"
val kill_proversN = "kill_provers"
val refresh_tptpN = "refresh_tptp"
@@ -305,8 +305,8 @@
(#add relevance_override) state
else if subcommand = messagesN then
messages opt_i
- else if subcommand = available_proversN then
- available_provers ctxt
+ else if subcommand = supported_proversN then
+ supported_provers ctxt
else if subcommand = running_proversN then
running_provers ()
else if subcommand = kill_proversN then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Feb 08 17:36:21 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Feb 08 17:38:43 2011 +0100
@@ -71,7 +71,7 @@
val das_Tool : string
val select_smt_solver : string -> Proof.context -> Proof.context
val is_smt_prover : Proof.context -> string -> bool
- val is_prover_available : Proof.context -> string -> bool
+ val is_prover_supported : Proof.context -> string -> bool
val is_prover_installed : Proof.context -> string -> bool
val default_max_relevant_for_prover : Proof.context -> string -> int
val is_built_in_const_for_prover :
@@ -89,7 +89,7 @@
val smt_weighted_fact :
theory -> int -> prover_fact * int
-> (string * locality) * (int option * thm)
- val available_provers : Proof.context -> unit
+ val supported_provers : Proof.context -> unit
val kill_provers : unit -> unit
val running_provers : unit -> unit
val messages : int option -> unit
@@ -121,16 +121,14 @@
fun is_smt_prover ctxt name =
member (op =) (SMT_Solver.available_solvers_of ctxt) name
-fun is_prover_available ctxt name =
+fun is_prover_supported ctxt name =
let val thy = ProofContext.theory_of ctxt in
- is_smt_prover ctxt name orelse member (op =) (available_atps thy) name
+ is_smt_prover ctxt name orelse member (op =) (supported_atps thy) name
end
fun is_prover_installed ctxt =
is_smt_prover ctxt orf is_atp_installed (ProofContext.theory_of ctxt)
-fun available_smt_solvers ctxt = SMT_Solver.available_solvers_of ctxt
-
fun default_max_relevant_for_prover ctxt name =
let val thy = ProofContext.theory_of ctxt in
if is_smt_prover ctxt name then
@@ -205,15 +203,15 @@
fun relevance_fudge_for_prover ctxt name =
if is_smt_prover ctxt name then smt_relevance_fudge else atp_relevance_fudge
-fun available_provers ctxt =
+fun supported_provers ctxt =
let
val thy = ProofContext.theory_of ctxt
val (remote_provers, local_provers) =
- sort_strings (available_atps thy) @
- sort_strings (available_smt_solvers ctxt)
+ sort_strings (supported_atps thy) @
+ sort_strings (SMT_Solver.available_solvers_of ctxt)
|> List.partition (String.isPrefix remote_prefix)
in
- Output.urgent_message ("Available provers: " ^
+ Output.urgent_message ("Supported provers: " ^
commas (local_provers @ remote_provers) ^ ".")
end
@@ -281,8 +279,8 @@
fun proof_banner auto =
if auto then "Auto Sledgehammer found a proof" else "Try this command"
-val smt_triggers = Unsynchronized.ref false
-val smt_weights = Unsynchronized.ref false
+val smt_triggers = Unsynchronized.ref true
+val smt_weights = Unsynchronized.ref true
val smt_weight_min_facts = Unsynchronized.ref 20
(* FUDGE *)
@@ -672,7 +670,7 @@
let val thy = ProofContext.theory_of ctxt in
if is_smt_prover ctxt name then
run_smt_solver auto name
- else if member (op =) (available_atps thy) name then
+ else if member (op =) (supported_atps thy) name then
run_atp auto name (get_atp thy name)
else
error ("No such prover: " ^ name ^ ".")
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Feb 08 17:36:21 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Feb 08 17:38:43 2011 +0100
@@ -183,7 +183,7 @@
val (_, hyp_ts, concl_t) = strip_subgoal goal i
val no_dangerous_types = types_dangerous_types type_sys
val _ = () |> not blocking ? kill_provers
- val _ = case find_first (not o is_prover_available ctxt) provers of
+ val _ = case find_first (not o is_prover_supported ctxt) provers of
SOME name => error ("No such prover: " ^ name ^ ".")
| NONE => ()
val _ = if auto then () else Output.urgent_message "Sledgehammering..."
--- a/src/HOL/Wellfounded.thy Tue Feb 08 17:36:21 2011 +0100
+++ b/src/HOL/Wellfounded.thy Tue Feb 08 17:38:43 2011 +0100
@@ -680,6 +680,15 @@
apply (rule wf_less_than [THEN wf_inv_image])
done
+lemma wf_if_measure: fixes f :: "'a \<Rightarrow> nat"
+shows "(!!x. P x \<Longrightarrow> f(g x) < f x) \<Longrightarrow> wf {(y,x). P x \<and> y = g x}"
+apply(insert wf_measure[of f])
+apply(simp only: measure_def inv_image_def less_than_def less_eq)
+apply(erule wf_subset)
+apply auto
+done
+
+
text{* Lexicographic combinations *}
definition lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" (infixr "<*lex*>" 80) where