--- a/CONTRIBUTORS Thu Jun 28 17:14:40 2018 +0100
+++ b/CONTRIBUTORS Fri Jun 29 11:39:40 2018 +0100
@@ -37,6 +37,9 @@
* March 2018: Viorel Preoteasa
Generalisation of complete_distrib_lattice
+* February 2018: Wenda Li
+ A unified definition for the order of zeros and poles. Improved reasoning around non-essential singularities.
+
* January 2018: Sebastien Gouezel
Various small additions to HOL-Analysis
--- a/NEWS Thu Jun 28 17:14:40 2018 +0100
+++ b/NEWS Fri Jun 29 11:39:40 2018 +0100
@@ -390,6 +390,10 @@
Ln, namely (-pi,pi]; the old Arg function has been renamed Arg2pi.
INCOMPATIBILITY.
+* Session HOL-Analysis: the functions zorder, zer_poly, porder and pol_poly have been redefined.
+All related lemmas have been reworked.
+INCOMPATIBILITY.
+
* Session HOL-Analysis: infinite products, Moebius functions, the
Riemann mapping theorem, the Vitali covering theorem,
change-of-variables results for integration and measures.
--- a/src/HOL/Rat.thy Thu Jun 28 17:14:40 2018 +0100
+++ b/src/HOL/Rat.thy Fri Jun 29 11:39:40 2018 +0100
@@ -821,6 +821,16 @@
end
+lemma Rats_cases [cases set: Rats]:
+ assumes "q \<in> \<rat>"
+ obtains (of_rat) r where "q = of_rat r"
+proof -
+ from \<open>q \<in> \<rat>\<close> have "q \<in> range of_rat"
+ by (simp only: Rats_def)
+ then obtain r where "q = of_rat r" ..
+ then show thesis ..
+qed
+
lemma Rats_of_rat [simp]: "of_rat r \<in> \<rat>"
by (simp add: Rats_def)
@@ -851,11 +861,8 @@
apply (rule of_rat_add [symmetric])
done
-lemma Rats_minus [simp]: "a \<in> \<rat> \<Longrightarrow> - a \<in> \<rat>"
- apply (auto simp add: Rats_def)
- apply (rule range_eqI)
- apply (rule of_rat_minus [symmetric])
- done
+lemma Rats_minus_iff [simp]: "- a \<in> \<rat> \<longleftrightarrow> a \<in> \<rat>"
+by (metis Rats_cases Rats_of_rat add.inverse_inverse of_rat_minus)
lemma Rats_diff [simp]: "a \<in> \<rat> \<Longrightarrow> b \<in> \<rat> \<Longrightarrow> a - b \<in> \<rat>"
apply (auto simp add: Rats_def)
@@ -890,16 +897,6 @@
apply (rule of_rat_power [symmetric])
done
-lemma Rats_cases [cases set: Rats]:
- assumes "q \<in> \<rat>"
- obtains (of_rat) r where "q = of_rat r"
-proof -
- from \<open>q \<in> \<rat>\<close> have "q \<in> range of_rat"
- by (simp only: Rats_def)
- then obtain r where "q = of_rat r" ..
- then show thesis ..
-qed
-
lemma Rats_induct [case_names of_rat, induct set: Rats]: "q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q"
by (rule Rats_cases) auto
--- a/src/HOL/Real.thy Thu Jun 28 17:14:40 2018 +0100
+++ b/src/HOL/Real.thy Fri Jun 29 11:39:40 2018 +0100
@@ -1192,6 +1192,10 @@
subsection \<open>Rationals\<close>
+lemma Rats_abs_iff[simp]:
+ "\<bar>(x::real)\<bar> \<in> \<rat> \<longleftrightarrow> x \<in> \<rat>"
+by(simp add: abs_real_def split: if_splits)
+
lemma Rats_eq_int_div_int: "\<rat> = {real_of_int i / real_of_int j | i j. j \<noteq> 0}" (is "_ = ?S")
proof
show "\<rat> \<subseteq> ?S"
--- a/src/Pure/Admin/isabelle_cronjob.scala Thu Jun 28 17:14:40 2018 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Fri Jun 29 11:39:40 2018 +0100
@@ -299,7 +299,7 @@
" -e ISABELLE_GHC=/usr/local/ghc-8.0.2/bin/ghc" +
" -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
args = "-a",
- detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows"))),
+ detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows")))
) :::
{
for { (n, hosts) <- List(1 -> List("lxbroy6"), 2 -> List("lxbroy8", "lxbroy5")) }
--- a/src/Pure/Tools/server.scala Thu Jun 28 17:14:40 2018 +0100
+++ b/src/Pure/Tools/server.scala Fri Jun 29 11:39:40 2018 +0100
@@ -102,7 +102,7 @@
val session = context.server.the_session(args.session_id)
Server_Commands.Use_Theories.command(
args, session, id = task.id, progress = task.progress)._1
- }),
+ })
},
"purge_theories" ->
{ case (context, Server_Commands.Purge_Theories(args)) =>