author paulson Mon, 27 Feb 2017 17:17:26 +0000 changeset 65057 799bbbb3a395 parent 65056 002b4c8c366e child 65061 1803a9787eca
Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.
 NEWS file | annotate | diff | comparison | revisions src/HOL/Analysis/Convex_Euclidean_Space.thy file | annotate | diff | comparison | revisions src/HOL/Fields.thy file | annotate | diff | comparison | revisions src/HOL/Power.thy file | annotate | diff | comparison | revisions src/HOL/Transcendental.thy file | annotate | diff | comparison | revisions
```--- 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

-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)