# HG changeset patch
# User blanchet
# Date 1356093234 -3600
# Node ID 1d8dae3257f047b19e337d305c46d4b55f7d336e
# Parent  5977de2993ac43e0496ed028348edb01443c7c88# Parent  b1b9119503b8ecaa9b7574c8a892917e6820cab3
merge

diff -r b1b9119503b8 -r 1d8dae3257f0 src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Fri Dec 21 11:05:44 2012 +0100
+++ b/src/Doc/Main/Main_Doc.thy	Fri Dec 21 13:33:54 2012 +0100
@@ -590,30 +590,38 @@
 \section*{Infix operators in Main} % @{theory Main}
 
 \begin{center}
-\begin{tabular}{lll}
-Operator & precedence & associativity \\
-@{text"="}, @{text"\<noteq>"} & 50 & left\\
-@{text"\<le>"}, @{text"<"}, @{text"\<ge>"}, @{text">"} & 50 \\
-@{text"\<and>"} & 35 & right \\
-@{text"\<or>"} & 30 & right \\
-@{text"\<longrightarrow>"}, @{text"\<longleftrightarrow>"} & 25 & right\\
-@{text"\<subseteq>"}, @{text"\<subset>"}, @{text"\<supseteq>"}, @{text"\<supset>"} & 50 \\
-@{text"\<in>"}, @{text"\<notin>"} & 50 \\
-@{text"\<inter>"} & 70 & left \\
-@{text"\<union>"} & 65 & left \\
-@{text"\<circ>"} & 55 & left\\
-@{text"`"} & 90 & right\\
-@{text"O"} & 75 & right\\
-@{text"``"} & 90 & right\\
-@{text"+"}, @{text"-"} & 65 & left \\
-@{text"*"}, @{text"/"} & 70 & left \\
-@{text"div"}, @{text"mod"} & 70 & left\\
-@{text"^"} & 80 & right\\
-@{text"^^"} & 80 & right\\
-@{text"dvd"} & 50 \\
-@{text"#"}, @{text"@"} & 65 & right\\
-@{text"!"} & 100 & left\\
-@{text"++"} & 100 & left\\
+\begin{tabular}{llll}
+ & Operator & precedence & associativity \\
+\hline
+Meta-logic & @{text"\<Longrightarrow>"} & 1 & right \\
+& @{text"\<equiv>"} & 2 \\
+\hline
+Logic & @{text"\<and>"} & 35 & right \\
+&@{text"\<or>"} & 30 & right \\
+&@{text"\<longrightarrow>"}, @{text"\<longleftrightarrow>"} & 25 & right\\
+&@{text"="}, @{text"\<noteq>"} & 50 & left\\
+\hline
+Orderings & @{text"\<le>"}, @{text"<"}, @{text"\<ge>"}, @{text">"} & 50 \\
+\hline
+Sets & @{text"\<subseteq>"}, @{text"\<subset>"}, @{text"\<supseteq>"}, @{text"\<supset>"} & 50 \\
+&@{text"\<in>"}, @{text"\<notin>"} & 50 \\
+&@{text"\<inter>"} & 70 & left \\
+&@{text"\<union>"} & 65 & left \\
+\hline
+Functions and Relations & @{text"\<circ>"} & 55 & left\\
+&@{text"`"} & 90 & right\\
+&@{text"O"} & 75 & right\\
+&@{text"``"} & 90 & right\\
+\hline
+Numbers & @{text"+"}, @{text"-"} & 65 & left \\
+&@{text"*"}, @{text"/"} & 70 & left \\
+&@{text"div"}, @{text"mod"} & 70 & left\\
+&@{text"^"} & 80 & right\\
+&@{text"^^"} & 80 & right\\
+&@{text"dvd"} & 50 \\
+\hline
+Lists & @{text"#"}, @{text"@"} & 65 & right\\
+&@{text"!"} & 100 & left
 \end{tabular}
 \end{center}
 *}
diff -r b1b9119503b8 -r 1d8dae3257f0 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Dec 21 11:05:44 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Dec 21 13:33:54 2012 +0100
@@ -364,7 +364,7 @@
     (if i = 1 then "" else " " ^ string_of_int i)
   end
 
-val default_learn_prover_timeout = 0.5
+val default_learn_prover_timeout = 2.0
 
 fun hammer_away override_params subcommand opt_i fact_override state =
   let
diff -r b1b9119503b8 -r 1d8dae3257f0 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Dec 21 11:05:44 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Dec 21 13:33:54 2012 +0100
@@ -58,7 +58,7 @@
   val prover_dependencies_of :
     Proof.context -> params -> string -> int -> fact list -> string Symtab.table
     -> thm -> bool * string list option
-  val weight_mash_facts : ('a * thm) list -> (('a * thm) * real) list
+  val weight_mash_facts : 'a list -> ('a * real) list
   val find_mash_suggestions :
     int -> (Symtab.key * 'a) list -> ('b * thm) list -> ('b * thm) list
     -> ('b * thm) list -> ('b * thm) list * ('b * thm) list
@@ -727,7 +727,6 @@
 fun is_fact_in_graph fact_G (_, th) =
   can (Graph.get_node fact_G) (nickname_of th)
 
-(* use MePo weights for now *)
 val weight_raw_mash_facts = weight_mepo_facts
 val weight_mash_facts = weight_raw_mash_facts
 
diff -r b1b9119503b8 -r 1d8dae3257f0 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Dec 21 11:05:44 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Dec 21 13:33:54 2012 +0100
@@ -18,7 +18,7 @@
   val const_names_in_fact :
     theory -> (string * typ -> term list -> bool * term list) -> term
     -> string list
-  val weight_mepo_facts : ('a * thm) list -> (('a * thm) * real) list
+  val weight_mepo_facts : 'a list -> ('a * real) list
   val mepo_suggested_facts :
     Proof.context -> params -> string -> int -> relevance_fudge option
     -> term list -> term -> fact list -> fact list
@@ -28,6 +28,7 @@
 struct
 
 open ATP_Problem_Generate
+open Sledgehammer_Util
 open Sledgehammer_Fact
 open Sledgehammer_Provers
 
@@ -509,10 +510,9 @@
                       "Total relevant: " ^ string_of_int (length accepts)))
   end
 
-(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
 (* FUDGE *)
 fun weight_of_mepo_fact rank =
-  Math.pow (1.5, 15.5 - 0.05 * Real.fromInt rank) + 15.0
+  Math.pow (0.62, log2 (Real.fromInt (rank + 1)))
 
 fun weight_mepo_facts facts =
   facts ~~ map weight_of_mepo_fact (0 upto length facts - 1)
diff -r b1b9119503b8 -r 1d8dae3257f0 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Dec 21 11:05:44 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Dec 21 13:33:54 2012 +0100
@@ -7,6 +7,7 @@
 signature SLEDGEHAMMER_UTIL =
 sig
   val sledgehammerN : string
+  val log2 : real -> real
   val plural_s : int -> string
   val serial_commas : string -> string list -> string list
   val simplify_spaces : string -> string
@@ -32,6 +33,10 @@
 
 val sledgehammerN = "sledgehammer"
 
+val log10_2 = Math.log10 2.0
+
+fun log2 n = Math.log10 n / log10_2
+
 fun plural_s n = if n = 1 then "" else "s"
 
 val serial_commas = Try.serial_commas
diff -r b1b9119503b8 -r 1d8dae3257f0 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Fri Dec 21 11:05:44 2012 +0100
+++ b/src/Pure/Pure.thy	Fri Dec 21 13:33:54 2012 +0100
@@ -146,7 +146,7 @@
 qed
 
 lemma imp_conjunction:
-  "(PROP A ==> PROP B &&& PROP C) == (PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
+  "(PROP A ==> PROP B &&& PROP C) == ((PROP A ==> PROP B) &&& (PROP A ==> PROP C))"
 proof
   assume conj: "PROP A ==> PROP B &&& PROP C"
   show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
diff -r b1b9119503b8 -r 1d8dae3257f0 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Dec 21 11:05:44 2012 +0100
+++ b/src/Pure/pure_thy.ML	Fri Dec 21 13:33:54 2012 +0100
@@ -177,7 +177,7 @@
   #> Sign.add_modesyntax_i ("HTML", false)
    [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
   #> Sign.add_consts_i
-   [(Binding.name "==", typ "'a => 'a => prop", Infixr ("==", 2)),
+   [(Binding.name "==", typ "'a => 'a => prop", Infix ("==", 2)),
     (Binding.name "==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
     (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
     (Binding.name "prop", typ "prop => prop", NoSyn),