# HG changeset patch # User wenzelm # Date 1297183123 -3600 # Node ID 2837df4d1c7a9434d4109c3e4febe1fa89f04920 # Parent ab3f6d76fb236da90f6f650364fd508f56289ac8# Parent 05514b09bb4b03c8c4376f7bc3aad6522a3efcc9 merged diff -r 05514b09bb4b -r 2837df4d1c7a NEWS --- 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 diff -r 05514b09bb4b -r 2837df4d1c7a doc-src/IsarRef/IsaMakefile --- 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 diff -r 05514b09bb4b -r 2837df4d1c7a doc-src/Sledgehammer/sledgehammer.tex --- 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 diff -r 05514b09bb4b -r 2837df4d1c7a src/HOL/Library/While_Combinator.thy --- 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 \ 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 \ nat" +shows "(!!s. b s \ f(c s) < f s) \ EX t. while_option b c s = Some t" +by(erule wf_while_option_Some[OF wf_if_measure]) + end diff -r 05514b09bb4b -r 2837df4d1c7a src/HOL/Smallcheck.thy --- 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 .. diff -r 05514b09bb4b -r 2837df4d1c7a src/HOL/Tools/ATP/atp_systems.ML --- 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 diff -r 05514b09bb4b -r 2837df4d1c7a src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- 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; diff -r 05514b09bb4b -r 2837df4d1c7a src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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 diff -r 05514b09bb4b -r 2837df4d1c7a src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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 ^ ".") diff -r 05514b09bb4b -r 2837df4d1c7a src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- 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..." diff -r 05514b09bb4b -r 2837df4d1c7a src/HOL/Wellfounded.thy --- 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 \ nat" +shows "(!!x. P x \ f(g x) < f x) \ wf {(y,x). P x \ 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 \'a) set \ ('b \ 'b) set \ (('a \ 'b) \ ('a \ 'b)) set" (infixr "<*lex*>" 80) where