author paulson Mon Feb 27 17:17:26 2017 +0000 (2017-02-27) changeset 65057 799bbbb3a395 parent 65056 002b4c8c366e child 65061 1803a9787eca
Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.
 NEWS file | annotate | diff | revisions src/HOL/Analysis/Convex_Euclidean_Space.thy file | annotate | diff | revisions src/HOL/Fields.thy file | annotate | diff | revisions src/HOL/Power.thy file | annotate | diff | revisions src/HOL/Transcendental.thy file | annotate | diff | revisions
```     1.1 --- a/NEWS	Mon Feb 27 00:00:28 2017 +0100
1.2 +++ b/NEWS	Mon Feb 27 17:17:26 2017 +0000
1.3 @@ -106,7 +106,7 @@
1.4
1.5  * Session HOL-Analysis: more material involving arcs, paths, covering
1.6  spaces, innessential maps, retracts. Major results include the Jordan
1.7 -Curve Theorem.
1.8 +Curve Theorem and the Great Picard Theorem.
1.9
1.10  * The theorem in Permutations has been renamed:
1.11    bij_swap_ompose_bij ~> bij_swap_compose_bij
```
```     2.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Feb 27 00:00:28 2017 +0100
2.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Feb 27 17:17:26 2017 +0000
2.3 @@ -8030,6 +8030,37 @@
2.4
2.5  definition "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"
2.6
2.7 +lemma betweenI:
2.8 +  assumes "0 \<le> u" "u \<le> 1" "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
2.9 +  shows "between (a, b) x"
2.10 +using assms unfolding between_def closed_segment_def by auto
2.11 +
2.12 +lemma betweenE:
2.13 +  assumes "between (a, b) x"
2.14 +  obtains u where "0 \<le> u" "u \<le> 1" "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
2.15 +using assms unfolding between_def closed_segment_def by auto
2.16 +
2.17 +lemma between_implies_scaled_diff:
2.18 +  assumes "between (S, T) X" "between (S, T) Y" "S \<noteq> Y"
2.19 +  obtains c where "(X - Y) = c *\<^sub>R (S - Y)"
2.20 +proof -
2.21 +  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"
2.22 +    by (metis add.commute betweenE eq_diff_eq)
2.23 +  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"
2.24 +    by (metis add.commute betweenE eq_diff_eq)
2.25 +  have "X - Y = (u\<^sub>X - u\<^sub>Y) *\<^sub>R (S - T)"
2.26 +  proof -
2.27 +    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
2.28 +    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)
2.29 +    finally show ?thesis by (simp add: real_vector.scale_right_diff_distrib)
2.30 +  qed
2.31 +  moreover from Y have "S - Y = (1 - u\<^sub>Y) *\<^sub>R (S - T)"
2.32 +    by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib)
2.33 +  moreover note \<open>S \<noteq> Y\<close>
2.34 +  ultimately have "(X - Y) = ((u\<^sub>X - u\<^sub>Y) / (1 - u\<^sub>Y)) *\<^sub>R (S - Y)" by auto
2.35 +  from this that show thesis by blast
2.36 +qed
2.37 +
2.38  lemma between_mem_segment: "between (a,b) x \<longleftrightarrow> x \<in> closed_segment a b"
2.39    unfolding between_def by auto
2.40
2.41 @@ -8142,6 +8173,13 @@
2.42      shows "between (a,b) x \<longleftrightarrow> norm(x - a) *\<^sub>R (b - x) = norm(b - x) *\<^sub>R (x - a)"
2.43    by (auto simp: between dist_triangle_eq norm_minus_commute algebra_simps)
2.44
2.45 +lemma between_swap:
2.46 +  fixes A B X Y :: "'a::euclidean_space"
2.47 +  assumes "between (A, B) X"
2.48 +  assumes "between (A, B) Y"
2.49 +  shows "between (X, B) Y \<longleftrightarrow> between (A, Y) X"
2.50 +using assms by (auto simp add: between)
2.51 +
2.52
2.53  subsection \<open>Shrinking towards the interior of a convex set\<close>
2.54
```
```     3.1 --- a/src/HOL/Fields.thy	Mon Feb 27 00:00:28 2017 +0100
3.2 +++ b/src/HOL/Fields.thy	Mon Feb 27 17:17:26 2017 +0000
3.3 @@ -494,6 +494,10 @@
3.4    "1 = a / b \<longleftrightarrow> b \<noteq> 0 \<and> a = b"
3.5    by (simp add: eq_commute [of 1])
3.6
3.7 +lemma divide_eq_minus_1_iff:
3.8 +   "(a / b = - 1) \<longleftrightarrow> b \<noteq> 0 \<and> a = - b"
3.9 +using divide_eq_1_iff by fastforce
3.10 +
3.11  lemma times_divide_times_eq:
3.12    "(x / y) * (z / w) = (x * z) / (y * w)"
3.13    by simp
```
```     4.1 --- a/src/HOL/Power.thy	Mon Feb 27 00:00:28 2017 +0100
4.2 +++ b/src/HOL/Power.thy	Mon Feb 27 17:17:26 2017 +0000
4.3 @@ -563,6 +563,11 @@
4.4  lemma power_Suc_le_self: "0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ Suc n \<le> a"
4.5    using power_decreasing [of 1 "Suc n" a] by simp
4.6
4.7 +lemma power2_eq_iff_nonneg [simp]:
4.8 +  assumes "0 \<le> x" "0 \<le> y"
4.9 +  shows "(x ^ 2 = y ^ 2) \<longleftrightarrow> x = y"
4.10 +using assms power2_eq_imp_eq by blast
4.11 +
4.12  end
4.13
4.14  context linordered_ring_strict
```
```     5.1 --- a/src/HOL/Transcendental.thy	Mon Feb 27 00:00:28 2017 +0100
5.2 +++ b/src/HOL/Transcendental.thy	Mon Feb 27 17:17:26 2017 +0000
5.3 @@ -4926,7 +4926,12 @@
5.4    by (metis arccos_cos arccos_cos2 cos_minus_pi cos_total diff_le_0_iff_le le_add_same_cancel1
5.6
5.7 -lemma sin_arccos_nonzero: "- 1 < x \<Longrightarrow> x < 1 \<Longrightarrow> \<not> sin (arccos x) = 0"
5.8 +corollary arccos_minus_abs:
5.9 +  assumes "\<bar>x\<bar> \<le> 1"
5.10 +  shows "arccos (- x) = pi - arccos x"
5.11 +using assms by (simp add: arccos_minus)
5.12 +
5.13 +lemma sin_arccos_nonzero: "- 1 < x \<Longrightarrow> x < 1 \<Longrightarrow> sin (arccos x) \<noteq> 0"
5.14    using arccos_lt_bounded sin_gt_zero by force
5.15
5.16  lemma arctan: "- (pi/2) < arctan y \<and> arctan y < pi/2 \<and> tan (arctan y) = y"
5.17 @@ -4958,11 +4963,7 @@
5.18    by (rule arctan_unique) simp_all
5.19
5.20  lemma arctan_minus: "arctan (- x) = - arctan x"
5.21 -  apply (rule arctan_unique)
5.22 -    apply (simp only: neg_less_iff_less arctan_ubound)
5.23 -   apply (metis minus_less_iff arctan_lbound)
5.24 -  apply (simp add: arctan)
5.25 -  done
5.26 +  using arctan [of "x"] by (auto simp: arctan_unique)
5.27
5.28  lemma cos_arctan_not_zero [simp]: "cos (arctan x) \<noteq> 0"
5.29    by (intro less_imp_neq [symmetric] cos_gt_zero_pi arctan_lbound arctan_ubound)
```