# HG changeset patch
# User paulson
# Date 1530268780 -3600
# Node ID 7da59435126a007305f45729ce479d1a4d7e4ae0
# Parent  7c6f812afdc45fac7d8481fec6dcd80ad0cc26a2# Parent  f8b98d31ad4535d4a550c597d9c0e677c94ec646
merged

diff -r f8b98d31ad45 -r 7da59435126a CONTRIBUTORS
--- 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
 
diff -r f8b98d31ad45 -r 7da59435126a NEWS
--- 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.
diff -r f8b98d31ad45 -r 7da59435126a src/HOL/Rat.thy
--- 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
 
diff -r f8b98d31ad45 -r 7da59435126a src/HOL/Real.thy
--- 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"
diff -r f8b98d31ad45 -r 7da59435126a src/Pure/Admin/isabelle_cronjob.scala
--- 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")) }
diff -r f8b98d31ad45 -r 7da59435126a src/Pure/Tools/server.scala
--- 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)) =>