1900 |
1900 |
1901 lemma cos_one_sin_zero: "cos x = 1 ==> sin x = 0" |
1901 lemma cos_one_sin_zero: "cos x = 1 ==> sin x = 0" |
1902 by (cut_tac x = x in sin_cos_squared_add3, auto) |
1902 by (cut_tac x = x in sin_cos_squared_add3, auto) |
1903 |
1903 |
1904 |
1904 |
1905 subsection{*Theorems About Sqrt, Transcendental Functions for Complex*} |
1905 subsection {* Existence of Polar Coordinates *} |
1906 |
1906 |
1907 lemma le_real_sqrt_sumsq [simp]: "x \<le> sqrt (x * x + y * y)" |
1907 lemma cos_x_y_le_one: "\<bar>x / sqrt (x\<twosuperior> + y\<twosuperior>)\<bar> \<le> 1" |
1908 by (simp add: power2_eq_square [symmetric]) |
1908 apply (rule power2_le_imp_le [OF _ zero_le_one]) |
1909 |
1909 apply (simp add: abs_divide power_divide divide_le_eq not_sum_power2_lt_zero) |
1910 lemma minus_le_real_sqrt_sumsq [simp]: "-x \<le> sqrt (x * x + y * y)" |
1910 done |
1911 apply (simp add: power2_eq_square [symmetric]) |
1911 |
1912 apply (rule power2_le_imp_le, simp_all) |
1912 lemma cos_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> cos (arccos y) = y" |
1913 done |
1913 by (simp add: abs_le_iff) |
1914 |
1914 |
1915 lemma lemma_real_divide_sqrt_ge_minus_one: |
1915 lemma cos_total_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> \<exists>!x. 0 \<le> x \<and> x \<le> pi \<and> cos x = y" |
1916 "0 < x ==> -1 \<le> x/(sqrt (x * x + y * y))" |
1916 by (simp add: abs_le_iff cos_total) |
1917 by (simp add: divide_const_simps linorder_not_le [symmetric] |
1917 |
1918 del: real_sqrt_le_0_iff real_sqrt_ge_0_iff) |
1918 lemmas cos_arccos_lemma1 = cos_arccos_abs [OF cos_x_y_le_one] |
1919 |
1919 |
1920 lemma real_sqrt_sum_squares_gt_zero1: "x < 0 ==> 0 < sqrt (x * x + y * y)" |
1920 lemmas cos_total_lemma1 = cos_total_abs [OF cos_x_y_le_one] |
1921 by (simp add: sum_squares_gt_zero_iff) |
|
1922 |
|
1923 lemma real_sqrt_sum_squares_gt_zero2: "0 < x ==> 0 < sqrt (x * x + y * y)" |
|
1924 by (simp add: sum_squares_gt_zero_iff) |
|
1925 |
|
1926 lemma real_sqrt_sum_squares_gt_zero3: "x \<noteq> 0 ==> 0 < sqrt(x\<twosuperior> + y\<twosuperior>)" |
|
1927 by (simp add: add_pos_nonneg) |
|
1928 |
|
1929 lemma real_sqrt_sum_squares_gt_zero3a: "y \<noteq> 0 ==> 0 < sqrt(x\<twosuperior> + y\<twosuperior>)" |
|
1930 by (simp add: add_nonneg_pos) |
|
1931 |
|
1932 lemma real_sqrt_sum_squares_eq_cancel: "sqrt(x\<twosuperior> + y\<twosuperior>) = x ==> y = 0" |
|
1933 by (drule_tac f = "%x. x\<twosuperior>" in arg_cong, simp) |
|
1934 |
|
1935 lemma real_sqrt_sum_squares_eq_cancel2: "sqrt(x\<twosuperior> + y\<twosuperior>) = y ==> x = 0" |
|
1936 by (drule_tac f = "%x. x\<twosuperior>" in arg_cong, simp) |
|
1937 |
|
1938 lemma lemma_real_divide_sqrt_le_one: "x < 0 ==> x/(sqrt (x * x + y * y)) \<le> 1" |
|
1939 by (simp add: divide_le_eq not_sum_squares_lt_zero) |
|
1940 |
|
1941 lemma lemma_real_divide_sqrt_ge_minus_one2: |
|
1942 "x < 0 ==> -1 \<le> x/(sqrt (x * x + y * y))" |
|
1943 apply (simp add: divide_const_simps |
|
1944 del: real_sqrt_gt_0_iff real_sqrt_lt_0_iff) |
|
1945 apply (insert minus_le_real_sqrt_sumsq [of x y], arith) |
|
1946 done |
|
1947 |
|
1948 lemma lemma_real_divide_sqrt_le_one2: "0 < x ==> x/(sqrt (x * x + y * y)) \<le> 1" |
|
1949 by (simp add: divide_le_eq not_sum_squares_lt_zero) |
|
1950 |
|
1951 lemma minus_sqrt_le: "- sqrt (x * x + y * y) \<le> x" |
|
1952 by (insert minus_le_real_sqrt_sumsq [of x y], arith) |
|
1953 |
|
1954 lemma minus_sqrt_le2: "- sqrt (x * x + y * y) \<le> y" |
|
1955 by (subst add_commute, simp add: minus_sqrt_le) |
|
1956 |
|
1957 lemma not_neg_sqrt_sumsq: "~ sqrt (x * x + y * y) < 0" |
|
1958 by (simp add: not_sum_squares_lt_zero) |
|
1959 |
|
1960 lemma cos_x_y_ge_minus_one: "-1 \<le> x / sqrt (x * x + y * y)" |
|
1961 by (simp add: minus_sqrt_le not_neg_sqrt_sumsq divide_const_simps |
|
1962 del: real_sqrt_gt_0_iff real_sqrt_lt_0_iff) |
|
1963 |
|
1964 lemma cos_x_y_ge_minus_one1a (*[simp]*): "-1 \<le> y / sqrt (x * x + y * y)" |
|
1965 by (subst add_commute, simp add: cos_x_y_ge_minus_one) |
|
1966 |
|
1967 lemma cos_x_y_le_one (*[simp]*): "x / sqrt (x * x + y * y) \<le> 1" |
|
1968 by (simp add: divide_le_eq not_sum_squares_lt_zero) |
|
1969 |
|
1970 lemma cos_x_y_le_one2 (*[simp]*): "y / sqrt (x * x + y * y) \<le> 1" |
|
1971 apply (cut_tac x = y and y = x in cos_x_y_le_one) |
|
1972 apply (simp add: real_add_commute) |
|
1973 done |
|
1974 |
|
1975 lemmas cos_arccos_lemma1 = (* used by polar_ex1 *) |
|
1976 cos_arccos [OF cos_x_y_ge_minus_one cos_x_y_le_one] |
|
1977 |
|
1978 lemmas arccos_bounded_lemma1 = |
|
1979 arccos_bounded [OF cos_x_y_ge_minus_one cos_x_y_le_one] |
|
1980 |
|
1981 lemmas cos_arccos_lemma2 = |
|
1982 cos_arccos [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2] |
|
1983 |
|
1984 lemmas arccos_bounded_lemma2 = |
|
1985 arccos_bounded [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2] |
|
1986 |
|
1987 lemma cos_abs_x_y_ge_minus_one (*[simp]*): |
|
1988 "-1 \<le> \<bar>x\<bar> / sqrt (x * x + y * y)" |
|
1989 by (auto simp add: divide_const_simps abs_if linorder_not_le [symmetric] |
|
1990 simp del: real_sqrt_ge_0_iff real_sqrt_le_0_iff) |
|
1991 |
|
1992 lemma cos_abs_x_y_le_one (*[simp]*): "\<bar>x\<bar> / sqrt (x * x + y * y) \<le> 1" |
|
1993 apply (insert minus_le_real_sqrt_sumsq [of x y] le_real_sqrt_sumsq [of x y]) |
|
1994 apply (auto simp add: divide_const_simps abs_if linorder_neq_iff |
|
1995 simp del: real_sqrt_gt_0_iff real_sqrt_eq_0_iff) |
|
1996 done |
|
1997 |
|
1998 lemmas cos_arccos_lemma3 = |
|
1999 cos_arccos [OF cos_abs_x_y_ge_minus_one cos_abs_x_y_le_one] |
|
2000 |
|
2001 lemmas arccos_bounded_lemma3 = |
|
2002 arccos_bounded [OF cos_abs_x_y_ge_minus_one cos_abs_x_y_le_one] |
|
2003 |
|
2004 lemma minus_pi_less_zero (*[simp]*): "-pi < 0" |
|
2005 by simp |
|
2006 |
|
2007 lemma minus_pi_le_zero (*[simp]*): "-pi \<le> 0" |
|
2008 by simp |
|
2009 |
|
2010 lemma arccos_ge_minus_pi: "[| -1 \<le> y; y \<le> 1 |] ==> -pi \<le> arccos y" |
|
2011 apply (rule real_le_trans) |
|
2012 apply (rule_tac [2] arccos_lbound, auto) |
|
2013 done |
|
2014 |
|
2015 lemmas arccos_ge_minus_pi_lemma = |
|
2016 arccos_ge_minus_pi [OF cos_x_y_ge_minus_one cos_x_y_le_one, simp] |
|
2017 |
1921 |
2018 (* How tedious! *) |
1922 (* How tedious! *) |
2019 lemma lemma_divide_rearrange: |
1923 lemma lemma_divide_rearrange: |
2020 "[| x + (y::real) \<noteq> 0; 1 - z = x/(x + y) |] ==> z = y/(x + y)" |
1924 "[| x + (y::real) \<noteq> 0; 1 - z = x/(x + y) |] ==> z = y/(x + y)" |
2021 apply (rule_tac c1 = "x + y" in real_mult_right_cancel [THEN iffD1]) |
1925 apply (rule_tac c1 = "x + y" in real_mult_right_cancel [THEN iffD1]) |
2031 apply (auto simp add: mult_assoc) |
1935 apply (auto simp add: mult_assoc) |
2032 apply (auto simp add: right_distrib left_diff_distrib) |
1936 apply (auto simp add: right_distrib left_diff_distrib) |
2033 done |
1937 done |
2034 |
1938 |
2035 lemma lemma_cos_sin_eq: |
1939 lemma lemma_cos_sin_eq: |
2036 "[| 0 < x * x + y * y; |
1940 "[| 0 < x\<twosuperior> + y\<twosuperior>; |
2037 1 - (sin xa)\<twosuperior> = (x / sqrt (x * x + y * y)) ^ 2 |] |
1941 1 - (sin xa)\<twosuperior> = (x / sqrt (x\<twosuperior> + y\<twosuperior>))\<twosuperior> |] |
2038 ==> (sin xa)\<twosuperior> = (y / sqrt (x * x + y * y)) ^ 2" |
1942 ==> (sin xa)\<twosuperior> = (y / sqrt (x\<twosuperior> + y\<twosuperior>))\<twosuperior>" |
2039 by (auto intro: lemma_divide_rearrange |
1943 by (auto intro: lemma_divide_rearrange simp add: power_divide) |
2040 simp add: power_divide power2_eq_square [symmetric]) |
|
2041 |
|
2042 |
|
2043 lemma lemma_sin_cos_eq: |
|
2044 "[| 0 < x * x + y * y; |
|
2045 1 - (cos xa)\<twosuperior> = (y / sqrt (x * x + y * y)) ^ 2 |] |
|
2046 ==> (cos xa)\<twosuperior> = (x / sqrt (x * x + y * y)) ^ 2" |
|
2047 apply (auto simp add: power_divide power2_eq_square [symmetric]) |
|
2048 apply (subst add_commute) |
|
2049 apply (rule lemma_divide_rearrange, simp add: real_add_eq_0_iff) |
|
2050 apply (simp add: add_commute) |
|
2051 done |
|
2052 |
1944 |
2053 lemma sin_x_y_disj: |
1945 lemma sin_x_y_disj: |
2054 "[| x \<noteq> 0; |
1946 "[| 0 < y; |
2055 cos xa = x / sqrt (x * x + y * y) |
1947 cos xa = x / sqrt (x\<twosuperior> + y\<twosuperior>) |
2056 |] ==> sin xa = y / sqrt (x * x + y * y) | |
1948 |] ==> sin xa = y / sqrt (x\<twosuperior> + y\<twosuperior>) | |
2057 sin xa = - y / sqrt (x * x + y * y)" |
1949 sin xa = - y / sqrt (x\<twosuperior> + y\<twosuperior>)" |
2058 apply (drule_tac f = "%x. x\<twosuperior>" in arg_cong) |
1950 apply (drule_tac f = "%x. x\<twosuperior>" in arg_cong) |
2059 apply (subgoal_tac "0 < x * x + y * y") |
1951 apply (subgoal_tac "0 < x\<twosuperior> + y\<twosuperior>") |
2060 apply (simp add: cos_squared_eq) |
1952 apply (simp add: cos_squared_eq) |
2061 apply (subgoal_tac "(sin xa)\<twosuperior> = (y / sqrt (x * x + y * y)) ^ 2") |
1953 apply (subgoal_tac "(sin xa)\<twosuperior> = (y / sqrt (x\<twosuperior> + y\<twosuperior>))\<twosuperior>") |
2062 apply (rule_tac [2] lemma_cos_sin_eq) |
1954 apply (rule_tac [2] lemma_cos_sin_eq) |
2063 apply (auto simp add: realpow_two_disj numeral_2_eq_2 simp del: realpow_Suc) |
1955 apply (auto simp add: realpow_two_disj numeral_2_eq_2 simp del: realpow_Suc) |
2064 apply (auto simp add: sum_squares_gt_zero_iff) |
1956 apply (auto simp add: sum_squares_gt_zero_iff) |
2065 done |
1957 done |
2066 |
1958 |
2067 lemma lemma_cos_not_eq_zero: "x \<noteq> 0 ==> x / sqrt (x * x + y * y) \<noteq> 0" |
1959 lemma real_sqrt_divide_less_zero: "0 < y ==> - y / sqrt (x\<twosuperior> + y\<twosuperior>) < 0" |
2068 by (simp add: divide_inverse sum_squares_eq_zero_iff) |
1960 by (simp add: divide_pos_pos sum_power2_gt_zero_iff) |
2069 |
|
2070 lemma cos_x_y_disj: |
|
2071 "[| x \<noteq> 0; |
|
2072 sin xa = y / sqrt (x * x + y * y) |
|
2073 |] ==> cos xa = x / sqrt (x * x + y * y) | |
|
2074 cos xa = - x / sqrt (x * x + y * y)" |
|
2075 apply (drule_tac f = "%x. x\<twosuperior>" in arg_cong) |
|
2076 apply (subgoal_tac "0 < x * x + y * y") |
|
2077 apply (simp add: sin_squared_eq del: realpow_Suc) |
|
2078 apply (subgoal_tac "(cos xa)\<twosuperior> = (x / sqrt (x * x + y * y)) ^ 2") |
|
2079 apply (rule_tac [2] lemma_sin_cos_eq) |
|
2080 apply (auto simp add: realpow_two_disj numeral_2_eq_2 simp del: realpow_Suc) |
|
2081 apply (auto simp add: sum_squares_gt_zero_iff) |
|
2082 done |
|
2083 |
|
2084 lemma real_sqrt_divide_less_zero: "0 < y ==> - y / sqrt (x * x + y * y) < 0" |
|
2085 by (simp add: divide_pos_pos sum_squares_gt_zero_iff) |
|
2086 |
1961 |
2087 lemma polar_ex1: |
1962 lemma polar_ex1: |
2088 "[| x \<noteq> 0; 0 < y |] ==> \<exists>r a. x = r * cos a & y = r * sin a" |
1963 "0 < y ==> \<exists>r a. x = r * cos a & y = r * sin a" |
2089 apply (rule_tac x = "sqrt (x\<twosuperior> + y\<twosuperior>)" in exI) |
1964 apply (rule_tac x = "sqrt (x\<twosuperior> + y\<twosuperior>)" in exI) |
2090 apply (rule_tac x = "arccos (x / sqrt (x * x + y * y))" in exI) |
1965 apply (rule_tac x = "arccos (x / sqrt (x\<twosuperior> + y\<twosuperior>))" in exI) |
2091 apply auto |
1966 apply (simp add: cos_arccos_lemma1) |
2092 apply (drule_tac y2 = y in real_sqrt_sum_squares_gt_zero3 [THEN real_not_refl2, THEN not_sym]) |
|
2093 apply (auto simp add: power2_eq_square cos_arccos_lemma1) |
|
2094 apply (simp add: arccos_def) |
1967 apply (simp add: arccos_def) |
2095 apply (cut_tac x1 = x and y1 = y |
1968 apply (cut_tac x1 = x and y1 = y in cos_total_lemma1) |
2096 in cos_total [OF cos_x_y_ge_minus_one cos_x_y_le_one]) |
|
2097 apply (rule someI2_ex, blast) |
1969 apply (rule someI2_ex, blast) |
2098 apply (erule_tac V = "EX! xa. 0 \<le> xa & xa \<le> pi & cos xa = x / sqrt (x * x + y * y)" in thin_rl) |
1970 apply (erule_tac V = "Ex1 ?P" in thin_rl) |
2099 apply (frule sin_x_y_disj, blast) |
1971 apply (frule sin_x_y_disj, blast) |
2100 apply (drule_tac y2 = y in real_sqrt_sum_squares_gt_zero3 [THEN real_not_refl2, THEN not_sym]) |
1972 apply (auto) |
2101 apply (auto simp add: power2_eq_square) |
|
2102 apply (drule sin_ge_zero, assumption) |
1973 apply (drule sin_ge_zero, assumption) |
2103 apply (drule_tac x = x in real_sqrt_divide_less_zero, auto) |
1974 apply (drule_tac x = x in real_sqrt_divide_less_zero, auto) |
2104 done |
1975 done |
2105 |
1976 |
2106 lemma real_sum_squares_cancel2a: "x * x = -(y * y) ==> y = (0::real)" |
|
2107 by (simp add: real_add_eq_0_iff [symmetric] sum_squares_eq_zero_iff) |
|
2108 |
|
2109 lemma polar_ex2: |
1977 lemma polar_ex2: |
2110 "[| x \<noteq> 0; y < 0 |] ==> \<exists>r a. x = r * cos a & y = r * sin a" |
1978 "y < 0 ==> \<exists>r a. x = r * cos a & y = r * sin a" |
2111 apply (cut_tac x = 0 and y = x in linorder_less_linear, auto) |
1979 apply (insert polar_ex1 [where x=x and y="-y"], simp, clarify) |
2112 apply (rule_tac x = "sqrt (x\<twosuperior> + y\<twosuperior>)" in exI) |
|
2113 apply (rule_tac x = "arcsin (y / sqrt (x * x + y * y))" in exI) |
|
2114 apply (subst sin_arcsin [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2]) |
|
2115 apply (auto dest: real_sum_squares_cancel2a |
|
2116 simp add: power2_eq_square real_0_le_add_iff real_add_eq_0_iff) |
|
2117 apply (unfold arcsin_def) |
|
2118 apply (cut_tac x1 = x and y1 = y |
|
2119 in sin_total [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2]) |
|
2120 apply (rule someI2_ex, blast) |
|
2121 apply (erule_tac V = "EX! v. ?P v" in thin_rl) |
|
2122 apply (cut_tac x=x and y=y in cos_x_y_disj, simp, blast) |
|
2123 apply (auto simp add: real_0_le_add_iff real_add_eq_0_iff) |
|
2124 apply (drule cos_ge_zero, force) |
|
2125 apply (drule_tac x = y in real_sqrt_divide_less_zero) |
|
2126 apply (auto simp add: add_commute) |
|
2127 apply (insert polar_ex1 [of x "-y"], simp, clarify) |
|
2128 apply (rule_tac x = r in exI) |
1980 apply (rule_tac x = r in exI) |
2129 apply (rule_tac x = "-a" in exI, simp) |
1981 apply (rule_tac x = "-a" in exI, simp) |
2130 done |
1982 done |
2131 |
1983 |
2132 lemma polar_Ex: "\<exists>r a. x = r * cos a & y = r * sin a" |
1984 lemma polar_Ex: "\<exists>r a. x = r * cos a & y = r * sin a" |
2133 apply (case_tac "x = 0", auto) |
1985 apply (rule_tac x=0 and y=y in linorder_cases) |
2134 apply (rule_tac x = y in exI) |
1986 apply (erule polar_ex1) |
2135 apply (rule_tac x = "pi/2" in exI, auto) |
1987 apply (rule_tac x=x in exI, rule_tac x=0 in exI, simp) |
2136 apply (cut_tac x = 0 and y = y in linorder_less_linear, auto) |
1988 apply (erule polar_ex2) |
2137 apply (rule_tac [2] x = x in exI) |
1989 done |
2138 apply (rule_tac [2] x = 0 in exI, auto) |
1990 |
2139 apply (blast intro: polar_ex1 polar_ex2)+ |
1991 subsection {* Theorems About Sqrt *} |
2140 done |
1992 |
|
1993 lemma le_real_sqrt_sumsq [simp]: "x \<le> sqrt (x * x + y * y)" |
|
1994 by (simp add: power2_eq_square [symmetric]) |
|
1995 |
|
1996 lemma real_sqrt_sum_squares_eq_cancel: "sqrt(x\<twosuperior> + y\<twosuperior>) = x ==> y = 0" |
|
1997 by (drule_tac f = "%x. x\<twosuperior>" in arg_cong, simp) |
|
1998 |
|
1999 lemma real_sqrt_sum_squares_eq_cancel2: "sqrt(x\<twosuperior> + y\<twosuperior>) = y ==> x = 0" |
|
2000 by (drule_tac f = "%x. x\<twosuperior>" in arg_cong, simp) |
2141 |
2001 |
2142 lemma real_sqrt_ge_abs1 [simp]: "\<bar>x\<bar> \<le> sqrt (x\<twosuperior> + y\<twosuperior>)" |
2002 lemma real_sqrt_ge_abs1 [simp]: "\<bar>x\<bar> \<le> sqrt (x\<twosuperior> + y\<twosuperior>)" |
2143 by (rule power2_le_imp_le, simp_all) |
2003 by (rule power2_le_imp_le, simp_all) |
2144 |
2004 |
2145 lemma real_sqrt_ge_abs2 [simp]: "\<bar>y\<bar> \<le> sqrt (x\<twosuperior> + y\<twosuperior>)" |
2005 lemma real_sqrt_ge_abs2 [simp]: "\<bar>y\<bar> \<le> sqrt (x\<twosuperior> + y\<twosuperior>)" |