# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1488215846 0
# Node ID 799bbbb3a39515af96461fb25deb37e3dc584dbb
# Parent  002b4c8c366ebbb75db83b7890560c7a77c263b3
Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.

diff -r 002b4c8c366e -r 799bbbb3a395 NEWS
--- a/NEWS	Mon Feb 27 00:00:28 2017 +0100
+++ b/NEWS	Mon Feb 27 17:17:26 2017 +0000
@@ -106,7 +106,7 @@
 
 * Session HOL-Analysis: more material involving arcs, paths, covering
 spaces, innessential maps, retracts. Major results include the Jordan
-Curve Theorem.
+Curve Theorem and the Great Picard Theorem.
 
 * The theorem in Permutations has been renamed:
   bij_swap_ompose_bij ~> bij_swap_compose_bij
diff -r 002b4c8c366e -r 799bbbb3a395 src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Feb 27 00:00:28 2017 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Feb 27 17:17:26 2017 +0000
@@ -8030,6 +8030,37 @@
 
 definition "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"
 
+lemma betweenI:
+  assumes "0 \<le> u" "u \<le> 1" "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
+  shows "between (a, b) x"
+using assms unfolding between_def closed_segment_def by auto
+
+lemma betweenE:
+  assumes "between (a, b) x"
+  obtains u where "0 \<le> u" "u \<le> 1" "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
+using assms unfolding between_def closed_segment_def by auto
+
+lemma between_implies_scaled_diff:
+  assumes "between (S, T) X" "between (S, T) Y" "S \<noteq> Y"
+  obtains c where "(X - Y) = c *\<^sub>R (S - Y)"
+proof -
+  from \<open>between (S, T) X\<close> obtain u\<^sub>X where X: "X = u\<^sub>X *\<^sub>R S + (1 - u\<^sub>X) *\<^sub>R T"
+    by (metis add.commute betweenE eq_diff_eq)
+  from \<open>between (S, T) Y\<close> obtain u\<^sub>Y where Y: "Y = u\<^sub>Y *\<^sub>R S + (1 - u\<^sub>Y) *\<^sub>R T"
+    by (metis add.commute betweenE eq_diff_eq)
+  have "X - Y = (u\<^sub>X - u\<^sub>Y) *\<^sub>R (S - T)"
+  proof -
+    from X Y have "X - Y =  u\<^sub>X *\<^sub>R S - u\<^sub>Y *\<^sub>R S + ((1 - u\<^sub>X) *\<^sub>R T - (1 - u\<^sub>Y) *\<^sub>R T)" by simp
+    also have "\<dots> = (u\<^sub>X - u\<^sub>Y) *\<^sub>R S - (u\<^sub>X - u\<^sub>Y) *\<^sub>R T" by (simp add: scaleR_left.diff)
+    finally show ?thesis by (simp add: real_vector.scale_right_diff_distrib)
+  qed
+  moreover from Y have "S - Y = (1 - u\<^sub>Y) *\<^sub>R (S - T)"
+    by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib)
+  moreover note \<open>S \<noteq> Y\<close>
+  ultimately have "(X - Y) = ((u\<^sub>X - u\<^sub>Y) / (1 - u\<^sub>Y)) *\<^sub>R (S - Y)" by auto
+  from this that show thesis by blast
+qed
+
 lemma between_mem_segment: "between (a,b) x \<longleftrightarrow> x \<in> closed_segment a b"
   unfolding between_def by auto
 
@@ -8142,6 +8173,13 @@
     shows "between (a,b) x \<longleftrightarrow> norm(x - a) *\<^sub>R (b - x) = norm(b - x) *\<^sub>R (x - a)"
   by (auto simp: between dist_triangle_eq norm_minus_commute algebra_simps)
 
+lemma between_swap:
+  fixes A B X Y :: "'a::euclidean_space"
+  assumes "between (A, B) X"
+  assumes "between (A, B) Y"
+  shows "between (X, B) Y \<longleftrightarrow> between (A, Y) X"
+using assms by (auto simp add: between)
+
 
 subsection \<open>Shrinking towards the interior of a convex set\<close>
 
diff -r 002b4c8c366e -r 799bbbb3a395 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Mon Feb 27 00:00:28 2017 +0100
+++ b/src/HOL/Fields.thy	Mon Feb 27 17:17:26 2017 +0000
@@ -494,6 +494,10 @@
   "1 = a / b \<longleftrightarrow> b \<noteq> 0 \<and> a = b"
   by (simp add: eq_commute [of 1])
 
+lemma divide_eq_minus_1_iff:
+   "(a / b = - 1) \<longleftrightarrow> b \<noteq> 0 \<and> a = - b"
+using divide_eq_1_iff by fastforce
+
 lemma times_divide_times_eq:
   "(x / y) * (z / w) = (x * z) / (y * w)"
   by simp
diff -r 002b4c8c366e -r 799bbbb3a395 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Mon Feb 27 00:00:28 2017 +0100
+++ b/src/HOL/Power.thy	Mon Feb 27 17:17:26 2017 +0000
@@ -563,6 +563,11 @@
 lemma power_Suc_le_self: "0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ Suc n \<le> a"
   using power_decreasing [of 1 "Suc n" a] by simp
 
+lemma power2_eq_iff_nonneg [simp]:
+  assumes "0 \<le> x" "0 \<le> y"
+  shows "(x ^ 2 = y ^ 2) \<longleftrightarrow> x = y"
+using assms power2_eq_imp_eq by blast
+
 end
 
 context linordered_ring_strict
diff -r 002b4c8c366e -r 799bbbb3a395 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Mon Feb 27 00:00:28 2017 +0100
+++ b/src/HOL/Transcendental.thy	Mon Feb 27 17:17:26 2017 +0000
@@ -4926,7 +4926,12 @@
   by (metis arccos_cos arccos_cos2 cos_minus_pi cos_total diff_le_0_iff_le le_add_same_cancel1
       minus_diff_eq uminus_add_conv_diff)
 
-lemma sin_arccos_nonzero: "- 1 < x \<Longrightarrow> x < 1 \<Longrightarrow> \<not> sin (arccos x) = 0"
+corollary arccos_minus_abs:
+  assumes "\<bar>x\<bar> \<le> 1"
+  shows "arccos (- x) = pi - arccos x"
+using assms by (simp add: arccos_minus)
+
+lemma sin_arccos_nonzero: "- 1 < x \<Longrightarrow> x < 1 \<Longrightarrow> sin (arccos x) \<noteq> 0"
   using arccos_lt_bounded sin_gt_zero by force
 
 lemma arctan: "- (pi/2) < arctan y \<and> arctan y < pi/2 \<and> tan (arctan y) = y"
@@ -4958,11 +4963,7 @@
   by (rule arctan_unique) simp_all
 
 lemma arctan_minus: "arctan (- x) = - arctan x"
-  apply (rule arctan_unique)
-    apply (simp only: neg_less_iff_less arctan_ubound)
-   apply (metis minus_less_iff arctan_lbound)
-  apply (simp add: arctan)
-  done
+  using arctan [of "x"] by (auto simp: arctan_unique)
 
 lemma cos_arctan_not_zero [simp]: "cos (arctan x) \<noteq> 0"
   by (intro less_imp_neq [symmetric] cos_gt_zero_pi arctan_lbound arctan_ubound)