# HG changeset patch
# User wenzelm
# Date 1363427423 -3600
# Node ID c22bd20b0d63f1ee99181de55ab52d61449eb67c
# Parent  d5c95b55f84941835fea7c0db721ac57dcdb48a6# Parent  e19a22974c7297da2f163f53f6eed2b0c7c70cbb
merged

diff -r e19a22974c72 -r c22bd20b0d63 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Thu Mar 14 16:49:36 2013 +0100
+++ b/Admin/components/components.sha1	Sat Mar 16 10:50:23 2013 +0100
@@ -38,6 +38,7 @@
 8ee375cfc38972f080dbc78f07b68dac03efe968  ProofGeneral-3.7.1.1.tar.gz
 847b52c0676b5eb0fbf0476f64fc08c2d72afd0c  ProofGeneral-4.1.tar.gz
 0885e1f1d8feaca78d2f204b6487e6eec6dfab4b  scala-2.10.0.tar.gz
+f7dc7a4e1aea46408fd6e44b8cfacb33af61afbc  scala-2.10.1.tar.gz
 b447017e81600cc5e30dd61b5d4962f6da01aa80  scala-2.8.1.final.tar.gz
 5659440f6b86db29f0c9c0de7249b7e24a647126  scala-2.9.2.tar.gz
 43b5afbcad575ab6817d2289756ca22fd2ef43a9  spass-3.8ds.tar.gz
diff -r e19a22974c72 -r c22bd20b0d63 Admin/components/main
--- a/Admin/components/main	Thu Mar 14 16:49:36 2013 +0100
+++ b/Admin/components/main	Sat Mar 16 10:50:23 2013 +0100
@@ -8,6 +8,6 @@
 jfreechart-1.0.14
 kodkodi-1.5.2
 polyml-5.5.0-3
-scala-2.10.0
+scala-2.10.1
 spass-3.8ds
 z3-3.2
diff -r e19a22974c72 -r c22bd20b0d63 src/Doc/ProgProve/Logic.thy
--- a/src/Doc/ProgProve/Logic.thy	Thu Mar 14 16:49:36 2013 +0100
+++ b/src/Doc/ProgProve/Logic.thy	Sat Mar 16 10:50:23 2013 +0100
@@ -428,7 +428,7 @@
 
 \subsubsection{Finding theorems}
 
-Command \isacom{find\_theorems} searches for specific theorems in the current
+Command \isacom{find{\isacharunderscorekeyword}theorems} searches for specific theorems in the current
 theory. Search criteria include pattern matching on terms and on names.
 For details see the Isabelle/Isar Reference Manual~\cite{IsarRef}.
 \bigskip
diff -r e19a22974c72 -r c22bd20b0d63 src/HOL/BNF/Examples/Stream.thy
--- a/src/HOL/BNF/Examples/Stream.thy	Thu Mar 14 16:49:36 2013 +0100
+++ b/src/HOL/BNF/Examples/Stream.thy	Sat Mar 16 10:50:23 2013 +0100
@@ -207,6 +207,29 @@
 lemma sdrop_add[simp]: "sdrop n (sdrop m s) = sdrop (m + n) s"
   by (induct m arbitrary: s) auto
 
+partial_function (tailrec) sdrop_while :: "('a \<Rightarrow> bool) \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where 
+  "sdrop_while P s = (if P (shd s) then sdrop_while P (stl s) else s)"
+
+lemma sdrop_while_Stream[code]:
+  "sdrop_while P (Stream a s) = (if P a then sdrop_while P s else Stream a s)"
+  by (subst sdrop_while.simps) simp
+
+lemma sdrop_while_sdrop_LEAST:
+  assumes "\<exists>n. P (s !! n)"
+  shows "sdrop_while (Not o P) s = sdrop (LEAST n. P (s !! n)) s"
+proof -
+  from assms obtain m where "P (s !! m)" "\<And>n. P (s !! n) \<Longrightarrow> m \<le> n"
+    and *: "(LEAST n. P (s !! n)) = m" by atomize_elim (auto intro: LeastI Least_le)
+  thus ?thesis unfolding *
+  proof (induct m arbitrary: s)
+    case (Suc m)
+    hence "sdrop_while (Not \<circ> P) (stl s) = sdrop m (stl s)"
+      by (metis (full_types) not_less_eq_eq snth.simps(2))
+    moreover from Suc(3) have "\<not> (P (s !! 0))" by blast
+    ultimately show ?case by (subst sdrop_while.simps) simp
+  qed (metis comp_apply sdrop.simps(1) sdrop_while.simps snth.simps(1))
+qed
+
 
 subsection {* unary predicates lifted to streams *}
 
diff -r e19a22974c72 -r c22bd20b0d63 src/HOL/IMP/Live.thy
--- a/src/HOL/IMP/Live.thy	Thu Mar 14 16:49:36 2013 +0100
+++ b/src/HOL/IMP/Live.thy	Sat Mar 16 10:50:23 2013 +0100
@@ -32,7 +32,7 @@
 "gen (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = vars b \<union> gen c\<^isub>1 \<union> gen c\<^isub>2" |
 "gen (WHILE b DO c) = vars b \<union> gen c"
 
-lemma L_gen_kill: "L c X = (X - kill c) \<union> gen c"
+lemma L_gen_kill: "L c X = gen c \<union> (X - kill c)"
 by(induct c arbitrary:X) auto
 
 lemma L_While_pfp: "L c (L (WHILE b DO c) X) \<subseteq> L (WHILE b DO c) X"
@@ -250,7 +250,7 @@
 using bury_sound2[of c UNIV]
 by (auto simp: fun_eq_iff[symmetric])
 
-corollary bury_iff: "(bury c UNIV,s) \<Rightarrow> s' \<longleftrightarrow> (c,s) \<Rightarrow> s'"
+corollary bury_sim: "bury c UNIV \<sim> c"
 by(metis final_bury_sound final_bury_sound2)
 
 end
diff -r e19a22974c72 -r c22bd20b0d63 src/Pure/ML/ml_statistics_polyml-5.5.0.ML
--- a/src/Pure/ML/ml_statistics_polyml-5.5.0.ML	Thu Mar 14 16:49:36 2013 +0100
+++ b/src/Pure/ML/ml_statistics_polyml-5.5.0.ML	Sat Mar 16 10:50:23 2013 +0100
@@ -51,10 +51,8 @@
      ("threads_wait_IO", Markup.print_int threadsWaitIO),
      ("threads_wait_mutex", Markup.print_int threadsWaitMutex),
      ("threads_wait_signal", Markup.print_int threadsWaitSignal),
-     ("time_GC_system", signed_string_of_real (Time.toReal timeGCSystem)),
-     ("time_GC_user", signed_string_of_real (Time.toReal timeGCUser)),
-     ("time_non_GC_system", signed_string_of_real (Time.toReal timeNonGCSystem)),
-     ("time_non_GC_user", signed_string_of_real (Time.toReal timeNonGCUser))] @
+     ("time_CPU", signed_string_of_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
+     ("time_GC", signed_string_of_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @
     user_counters
   end;
 
diff -r e19a22974c72 -r c22bd20b0d63 src/Pure/Tools/ml_statistics.scala
--- a/src/Pure/Tools/ml_statistics.scala	Thu Mar 14 16:49:36 2013 +0100
+++ b/src/Pure/Tools/ml_statistics.scala	Sat Mar 16 10:50:23 2013 +0100
@@ -7,6 +7,7 @@
 package isabelle
 
 
+import scala.collection.mutable
 import scala.collection.immutable.{SortedSet, SortedMap}
 import scala.swing.{Frame, Component}
 
@@ -42,8 +43,9 @@
     ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar",
       "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal"))
 
-  val time_fields =
-    ("Time", List("time_GC_system", "time_GC_user", "time_non_GC_system", "time_non_GC_user"))
+  val time_fields = ("Time", List("time_CPU", "time_GC"))
+
+  val speed_fields = ("Speed", List("speed_CPU", "speed_GC"))
 
   val tasks_fields =
     ("Future tasks",
@@ -53,7 +55,8 @@
     ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
 
   val standard_fields =
-    List(GC_fields, heap_fields, threads_fields, time_fields, tasks_fields, workers_fields)
+    List(GC_fields, heap_fields, threads_fields, time_fields, speed_fields,
+      tasks_fields, workers_fields)
 }
 
 final class ML_Statistics private(val name: String, val stats: List[Properties.T])
@@ -72,15 +75,34 @@
         yield x)
 
   val content: List[ML_Statistics.Entry] =
-    stats.map(props => {
+  {
+    var last_edge = Map.empty[String, (Double, Double, Double)]
+    val result = new mutable.ListBuffer[ML_Statistics.Entry]
+    for (props <- stats) {
       val time = now(props) - time_start
       require(time >= 0.0)
+
+      // rising edges -- relative speed
+      val speeds =
+        for ((key, value) <- props; a <- Library.try_unprefix("time", key)) yield {
+          val (x0, y0, s0) = last_edge.get(a) getOrElse (0.0, 0.0, 0.0)
+
+          val x1 = time
+          val y1 = java.lang.Double.parseDouble(value)
+          val s1 = if (x1 == x0) 0.0 else (y1 - y0) / (x1 - x0)
+
+          val b = ("speed" + a).intern
+          if (y1 > y0) { last_edge += (a -> (x1, y1, s1)); (b, s1) } else (b, s0)
+        }
+
       val data =
-        SortedMap.empty[String, Double] ++
+        SortedMap.empty[String, Double] ++ speeds ++
           (for ((x, y) <- props.iterator if x != Now.name)
             yield (x, java.lang.Double.parseDouble(y)))
-      ML_Statistics.Entry(time, data)
-    })
+      result += ML_Statistics.Entry(time, data)
+    }
+    result.toList
+  }
 
 
   /* charts */