Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.
authorpaulson <lp15@cam.ac.uk>
Mon Feb 27 17:17:26 2017 +0000 (2017-02-27)
changeset 65057799bbbb3a395
parent 65056 002b4c8c366e
child 65061 1803a9787eca
Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.
NEWS
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Fields.thy
src/HOL/Power.thy
src/HOL/Transcendental.thy
     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.5        minus_diff_eq uminus_add_conv_diff)
     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)