Some new lemmas thanks to Lukas Bulwahn. Also, 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
--- 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>
--- 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
--- 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
--- 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)