--- a/Admin/jenkins/build/ci_build_benchmark.scala Fri Sep 16 17:12:39 2016 +0200
+++ b/Admin/jenkins/build/ci_build_benchmark.scala Fri Sep 16 18:01:31 2016 +0200
@@ -3,7 +3,8 @@
import isabelle._
- def threads = 8
+ override def documents = false
+ def threads = 6
def jobs = 1
def include = Nil
def select = List(Path.explode("$ISABELLE_HOME/src/Benchmarks"))
--- a/NEWS Fri Sep 16 17:12:39 2016 +0200
+++ b/NEWS Fri Sep 16 18:01:31 2016 +0200
@@ -332,6 +332,11 @@
- The MaSh relevance filter has been sped up.
- Produce syntactically correct Vampire 4.0 problem files.
+* The 'coinductive' command produces a proper coinduction rule for
+mutual coinductive predicates. This new rule replaces the old rule,
+which exposed details of the internal fixpoint construction and was
+hard to use. INCOMPATIBILITY.
+
* (Co)datatype package:
- New commands for defining corecursive functions and reasoning about
them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive',
--- a/src/HOL/Library/Liminf_Limsup.thy Fri Sep 16 17:12:39 2016 +0200
+++ b/src/HOL/Library/Liminf_Limsup.thy Fri Sep 16 18:01:31 2016 +0200
@@ -159,6 +159,14 @@
shows "Limsup net f = Limsup net g"
by (intro antisym Limsup_mono eventually_mono[OF assms]) auto
+lemma Liminf_bot[simp]: "Liminf bot f = top"
+ unfolding Liminf_def top_unique[symmetric]
+ by (rule SUP_upper2[where i="\<lambda>x. False"]) simp_all
+
+lemma Limsup_bot[simp]: "Limsup bot f = bot"
+ unfolding Limsup_def bot_unique[symmetric]
+ by (rule INF_lower2[where i="\<lambda>x. False"]) simp_all
+
lemma Liminf_le_Limsup:
assumes ntriv: "\<not> trivial_limit F"
shows "Liminf F f \<le> Limsup F f"
@@ -180,27 +188,26 @@
qed
lemma Liminf_bounded:
- assumes ntriv: "\<not> trivial_limit F"
assumes le: "eventually (\<lambda>n. C \<le> X n) F"
shows "C \<le> Liminf F X"
- using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp
+ using Liminf_mono[OF le] Liminf_const[of F C]
+ by (cases "F = bot") simp_all
lemma Limsup_bounded:
- assumes ntriv: "\<not> trivial_limit F"
assumes le: "eventually (\<lambda>n. X n \<le> C) F"
shows "Limsup F X \<le> C"
- using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
+ using Limsup_mono[OF le] Limsup_const[of F C]
+ by (cases "F = bot") simp_all
lemma le_Limsup:
assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. l \<le> f x"
shows "l \<le> Limsup F f"
-proof -
- have "l = Limsup F (\<lambda>x. l)"
- using F by (simp add: Limsup_const)
- also have "\<dots> \<le> Limsup F f"
- by (intro Limsup_mono x)
- finally show ?thesis .
-qed
+ using F Liminf_bounded Liminf_le_Limsup order.trans x by blast
+
+lemma Liminf_le:
+ assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. f x \<le> l"
+ shows "Liminf F f \<le> l"
+ using F Liminf_le_Limsup Limsup_bounded order.trans x by blast
lemma le_Liminf_iff:
fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
@@ -505,6 +512,46 @@
by (auto simp: Limsup_def)
qed
+lemma Liminf_filtermap_le: "Liminf (filtermap f F) g \<le> Liminf F (\<lambda>x. g (f x))"
+ apply (cases "F = bot", simp)
+ by (subst Liminf_def)
+ (auto simp add: INF_lower Liminf_bounded eventually_filtermap eventually_mono intro!: SUP_least)
+
+lemma Limsup_filtermap_ge: "Limsup (filtermap f F) g \<ge> Limsup F (\<lambda>x. g (f x))"
+ apply (cases "F = bot", simp)
+ by (subst Limsup_def)
+ (auto simp add: SUP_upper Limsup_bounded eventually_filtermap eventually_mono intro!: INF_greatest)
+
+lemma Liminf_least: "(\<And>P. eventually P F \<Longrightarrow> (INF x:Collect P. f x) \<le> x) \<Longrightarrow> Liminf F f \<le> x"
+ by (auto intro!: SUP_least simp: Liminf_def)
+
+lemma Limsup_greatest: "(\<And>P. eventually P F \<Longrightarrow> x \<le> (SUP x:Collect P. f x)) \<Longrightarrow> Limsup F f \<ge> x"
+ by (auto intro!: INF_greatest simp: Limsup_def)
+
+lemma Liminf_filtermap_ge: "inj f \<Longrightarrow> Liminf (filtermap f F) g \<ge> Liminf F (\<lambda>x. g (f x))"
+ apply (cases "F = bot", simp)
+ apply (rule Liminf_least)
+ subgoal for P
+ by (auto simp: eventually_filtermap the_inv_f_f
+ intro!: Liminf_bounded INF_lower2 eventually_mono[of P])
+ done
+
+lemma Limsup_filtermap_le: "inj f \<Longrightarrow> Limsup (filtermap f F) g \<le> Limsup F (\<lambda>x. g (f x))"
+ apply (cases "F = bot", simp)
+ apply (rule Limsup_greatest)
+ subgoal for P
+ by (auto simp: eventually_filtermap the_inv_f_f
+ intro!: Limsup_bounded SUP_upper2 eventually_mono[of P])
+ done
+
+lemma Liminf_filtermap_eq: "inj f \<Longrightarrow> Liminf (filtermap f F) g = Liminf F (\<lambda>x. g (f x))"
+ using Liminf_filtermap_le[of f F g] Liminf_filtermap_ge[of f F g]
+ by simp
+
+lemma Limsup_filtermap_eq: "inj f \<Longrightarrow> Limsup (filtermap f F) g = Limsup F (\<lambda>x. g (f x))"
+ using Limsup_filtermap_le[of f F g] Limsup_filtermap_ge[of F g f]
+ by simp
+
subsection \<open>More Limits\<close>
--- a/src/Pure/Tools/ci_profile.scala Fri Sep 16 17:12:39 2016 +0200
+++ b/src/Pure/Tools/ci_profile.scala Fri Sep 16 18:01:31 2016 +0200
@@ -59,6 +59,17 @@
(Timing.zero /: timings)(_ + _)
}
+ private def with_documents(options: Options): Options =
+ {
+ if (documents)
+ options
+ .bool.update("browser_info", true)
+ .string.update("document", "pdf")
+ .string.update("document_variants", "document:outline=/proof,/ML")
+ else
+ options
+ }
+
final def hg_id(path: Path): String =
Isabelle_System.hg("id -i", path.file).out
@@ -80,10 +91,7 @@
System.getProperties().putAll(props)
val options =
- Options.init()
- .bool.update("browser_info", true)
- .string.update("document", "pdf")
- .string.update("document_variants", "document:outline=/proof,/ML")
+ with_documents(Options.init())
.int.update("parallel_proofs", 2)
.int.update("threads", threads)
@@ -127,6 +135,8 @@
/* profile */
+ def documents: Boolean = true
+
def threads: Int
def jobs: Int
def include: List[Path]