# HG changeset patch # User wenzelm # Date 1474041691 -7200 # Node ID 8a4b41a8afb8f0e98f0fb126ccd0d575f558d4fa # Parent 19979c2f0d4ab8734661d1b83f237f56f72f9ef8# Parent 85c83757788c431d59bd6e0b7a39d514c32a5294 merged diff -r 85c83757788c -r 8a4b41a8afb8 Admin/jenkins/build/ci_build_benchmark.scala --- 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")) diff -r 85c83757788c -r 8a4b41a8afb8 NEWS --- 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', diff -r 85c83757788c -r 8a4b41a8afb8 src/HOL/Library/Liminf_Limsup.thy --- 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="\x. False"]) simp_all + +lemma Limsup_bot[simp]: "Limsup bot f = bot" + unfolding Limsup_def bot_unique[symmetric] + by (rule INF_lower2[where i="\x. False"]) simp_all + lemma Liminf_le_Limsup: assumes ntriv: "\ trivial_limit F" shows "Liminf F f \ Limsup F f" @@ -180,27 +188,26 @@ qed lemma Liminf_bounded: - assumes ntriv: "\ trivial_limit F" assumes le: "eventually (\n. C \ X n) F" shows "C \ 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: "\ trivial_limit F" assumes le: "eventually (\n. X n \ C) F" shows "Limsup F X \ 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 \ bot" and x: "\\<^sub>F x in F. l \ f x" shows "l \ Limsup F f" -proof - - have "l = Limsup F (\x. l)" - using F by (simp add: Limsup_const) - also have "\ \ 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 \ bot" and x: "\\<^sub>F x in F. f x \ l" + shows "Liminf F f \ l" + using F Liminf_le_Limsup Limsup_bounded order.trans x by blast lemma le_Liminf_iff: fixes X :: "_ \ _ :: complete_linorder" @@ -505,6 +512,46 @@ by (auto simp: Limsup_def) qed +lemma Liminf_filtermap_le: "Liminf (filtermap f F) g \ Liminf F (\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 \ Limsup F (\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: "(\P. eventually P F \ (INF x:Collect P. f x) \ x) \ Liminf F f \ x" + by (auto intro!: SUP_least simp: Liminf_def) + +lemma Limsup_greatest: "(\P. eventually P F \ x \ (SUP x:Collect P. f x)) \ Limsup F f \ x" + by (auto intro!: INF_greatest simp: Limsup_def) + +lemma Liminf_filtermap_ge: "inj f \ Liminf (filtermap f F) g \ Liminf F (\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 \ Limsup (filtermap f F) g \ Limsup F (\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 \ Liminf (filtermap f F) g = Liminf F (\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 \ Limsup (filtermap f F) g = Limsup F (\x. g (f x))" + using Limsup_filtermap_le[of f F g] Limsup_filtermap_ge[of F g f] + by simp + subsection \More Limits\ diff -r 85c83757788c -r 8a4b41a8afb8 src/Pure/Tools/ci_profile.scala --- 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]