merged
authorwenzelm
Tue, 08 Feb 2011 17:38:43 +0100
changeset 41728 2837df4d1c7a
parent 41727 ab3f6d76fb23 (diff)
parent 41718 05514b09bb4b (current diff)
child 41729 ae1a46cdb9cb
merged
NEWS
src/Pure/Concurrent/time_limit_dummy.ML
src/Pure/ML-Systems/polyml-5.2.ML
--- 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