# HG changeset patch # User wenzelm # Date 1376844585 -7200 # Node ID 47c9aff07725b6efe5c55cbdd8cbeb6240c77059 # Parent 98fc4753334252b6fae498dc23d199e778e0688e more symbols; diff -r 98fc47533342 -r 47c9aff07725 src/HOL/NthRoot.thy --- a/src/HOL/NthRoot.thy Sun Aug 18 17:00:10 2013 +0200 +++ b/src/HOL/NthRoot.thy Sun Aug 18 18:49:45 2013 +0200 @@ -464,7 +464,7 @@ apply (rule real_sqrt_abs) done -lemma real_inv_sqrt_pow2: "0 < x ==> inverse (sqrt(x)) ^ 2 = inverse x" +lemma real_inv_sqrt_pow2: "0 < x ==> (inverse (sqrt x))\<^sup>2 = inverse x" by (simp add: power_inverse [symmetric]) lemma real_sqrt_eq_zero_cancel: "[| 0 \ x; sqrt(x) = 0|] ==> x = 0" @@ -516,7 +516,7 @@ by (simp add: zero_le_mult_iff) lemma real_sqrt_sum_squares_mult_squared_eq [simp]: - "sqrt ((x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2)) ^ 2 = (x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2)" + "(sqrt ((x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2)))\<^sup>2 = (x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2)" by (simp add: zero_le_mult_iff) lemma real_sqrt_sum_squares_eq_cancel: "sqrt (x\<^sup>2 + y\<^sup>2) = x \ y = 0" diff -r 98fc47533342 -r 47c9aff07725 src/HOL/Power.thy --- a/src/HOL/Power.thy Sun Aug 18 17:00:10 2013 +0200 +++ b/src/HOL/Power.thy Sun Aug 18 18:49:45 2013 +0200 @@ -74,11 +74,11 @@ by (simp add: numeral_3_eq_3 mult_assoc) lemma power_even_eq: - "a ^ (2*n) = (a ^ n) ^ 2" + "a ^ (2 * n) = (a ^ n)\<^sup>2" by (subst mult_commute) (simp add: power_mult) lemma power_odd_eq: - "a ^ Suc (2*n) = a * (a ^ n) ^ 2" + "a ^ Suc (2*n) = a * (a ^ n)\<^sup>2" by (simp add: power_even_eq) lemma power_numeral_even: diff -r 98fc47533342 -r 47c9aff07725 src/HOL/Real.thy --- a/src/HOL/Real.thy Sun Aug 18 17:00:10 2013 +0200 +++ b/src/HOL/Real.thy Sun Aug 18 18:49:45 2013 +0200 @@ -1559,13 +1559,13 @@ text {* FIXME: declare this [simp] for all types, or not at all *} lemma realpow_two_sum_zero_iff [simp]: - "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)" + "(x\<^sup>2 + y\<^sup>2 = (0::real)) = (x = 0 & y = 0)" by (rule sum_power2_eq_zero_iff) lemma real_minus_mult_self_le [simp]: "-(u * u) \ (x * (x::real))" by (rule_tac y = 0 in order_trans, auto) -lemma realpow_square_minus_le [simp]: "-(u ^ 2) \ (x::real) ^ 2" +lemma realpow_square_minus_le [simp]: "- u\<^sup>2 \ (x::real)\<^sup>2" by (auto simp add: power2_eq_square) diff -r 98fc47533342 -r 47c9aff07725 src/HOL/Semiring_Normalization.thy --- a/src/HOL/Semiring_Normalization.thy Sun Aug 18 17:00:10 2013 +0200 +++ b/src/HOL/Semiring_Normalization.thy Sun Aug 18 18:49:45 2013 +0200 @@ -107,7 +107,7 @@ "(x ^ p) * (x ^ q) = x ^ (p + q)" "x * (x ^ q) = x ^ (Suc q)" "(x ^ q) * x = x ^ (Suc q)" - "x * x = x ^ 2" + "x * x = x\<^sup>2" "(x * y) ^ q = (x ^ q) * (y ^ q)" "(x ^ p) ^ q = x ^ (p * q)" "x ^ 0 = 1" diff -r 98fc47533342 -r 47c9aff07725 src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Sun Aug 18 17:00:10 2013 +0200 +++ b/src/HOL/Transcendental.thy Sun Aug 18 18:49:45 2013 +0200 @@ -1251,7 +1251,7 @@ finally show ?thesis . qed -lemma exp_bound: "0 <= (x::real) ==> x <= 1 ==> exp x <= 1 + x + x^2" +lemma exp_bound: "0 <= (x::real) ==> x <= 1 ==> exp x <= 1 + x + x\<^sup>2" proof - assume a: "0 <= x" assume b: "x <= 1" @@ -1274,17 +1274,17 @@ note aux1 = this have "(\n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))" by (intro sums_mult geometric_sums, simp) - hence aux2: "(\n. (x::real) ^ 2 / 2 * (1 / 2) ^ n) sums x^2" + hence aux2: "(\n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums x\<^sup>2" by simp - have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <= x^2" + have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <= x\<^sup>2" proof - have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <= - suminf (%n. (x^2/2) * ((1/2)^n))" + suminf (%n. (x\<^sup>2/2) * ((1/2)^n))" apply (rule summable_le) apply (rule allI, rule aux1) apply (rule summable_exp [THEN summable_ignore_initial_segment]) by (rule sums_summable, rule aux2) - also have "... = x^2" + also have "... = x\<^sup>2" by (rule sums_unique [THEN sym], rule aux2) finally show ?thesis . qed @@ -1294,14 +1294,14 @@ lemma ln_one_minus_pos_upper_bound: "0 <= x ==> x < 1 ==> ln (1 - x) <= - x" proof - assume a: "0 <= (x::real)" and b: "x < 1" - have "(1 - x) * (1 + x + x^2) = (1 - x^3)" + have "(1 - x) * (1 + x + x\<^sup>2) = (1 - x^3)" by (simp add: algebra_simps power2_eq_square power3_eq_cube) also have "... <= 1" by (auto simp add: a) - finally have "(1 - x) * (1 + x + x ^ 2) <= 1" . + finally have "(1 - x) * (1 + x + x\<^sup>2) <= 1" . moreover have c: "0 < 1 + x + x\<^sup>2" by (simp add: add_pos_nonneg a) - ultimately have "1 - x <= 1 / (1 + x + x^2)" + ultimately have "1 - x <= 1 / (1 + x + x\<^sup>2)" by (elim mult_imp_le_div_pos) also have "... <= 1 / exp x" apply (rule divide_left_mono) @@ -1343,18 +1343,18 @@ apply auto done -lemma ln_one_plus_pos_lower_bound: "0 <= x ==> x <= 1 ==> x - x^2 <= ln (1 + x)" +lemma ln_one_plus_pos_lower_bound: "0 <= x ==> x <= 1 ==> x - x\<^sup>2 <= ln (1 + x)" proof - assume a: "0 <= x" and b: "x <= 1" - have "exp (x - x^2) = exp x / exp (x^2)" + have "exp (x - x\<^sup>2) = exp x / exp (x\<^sup>2)" by (rule exp_diff) - also have "... <= (1 + x + x^2) / exp (x ^2)" + also have "... <= (1 + x + x\<^sup>2) / exp (x \<^sup>2)" apply (rule divide_right_mono) apply (rule exp_bound) apply (rule a, rule b) apply simp done - also have "... <= (1 + x + x^2) / (1 + x^2)" + also have "... <= (1 + x + x\<^sup>2) / (1 + x\<^sup>2)" apply (rule divide_left_mono) apply (simp add: exp_ge_add_one_self_aux) apply (simp add: a) @@ -1362,14 +1362,14 @@ done also from a have "... <= 1 + x" by (simp add: field_simps add_strict_increasing zero_le_mult_iff) - finally have "exp (x - x^2) <= 1 + x" . + finally have "exp (x - x\<^sup>2) <= 1 + x" . also have "... = exp (ln (1 + x))" proof - from a have "0 < 1 + x" by auto thus ?thesis by (auto simp only: exp_ln_iff [THEN sym]) qed - finally have "exp (x - x ^ 2) <= exp (ln (1 + x))" . + finally have "exp (x - x\<^sup>2) <= exp (ln (1 + x))" . thus ?thesis by (auto simp only: exp_le_cancel_iff) qed @@ -1392,7 +1392,7 @@ qed lemma ln_one_minus_pos_lower_bound: "0 <= x ==> x <= (1 / 2) ==> - - x - 2 * x^2 <= ln (1 - x)" + - x - 2 * x\<^sup>2 <= ln (1 - x)" proof - assume a: "0 <= x" and b: "x <= (1 / 2)" from b have c: "x < 1" @@ -1412,10 +1412,10 @@ by auto finally have d: "- x / (1 - x) <= ln (1 - x)" . have "0 < 1 - x" using a b by simp - hence e: "-x - 2 * x^2 <= - x / (1 - x)" + hence e: "-x - 2 * x\<^sup>2 <= - x / (1 - x)" using mult_right_le_one_le[of "x*x" "2*x"] a b by (simp add:field_simps power2_eq_square) - from e d show "- x - 2 * x^2 <= ln (1 - x)" + from e d show "- x - 2 * x\<^sup>2 <= ln (1 - x)" by (rule order_trans) qed @@ -1426,7 +1426,7 @@ done lemma abs_ln_one_plus_x_minus_x_bound_nonneg: - "0 <= x ==> x <= 1 ==> abs(ln (1 + x) - x) <= x^2" + "0 <= x ==> x <= 1 ==> abs(ln (1 + x) - x) <= x\<^sup>2" proof - assume x: "0 <= x" assume x1: "x <= 1" @@ -1438,9 +1438,9 @@ by (rule abs_of_nonpos) also have "... = x - ln (1 + x)" by simp - also have "... <= x^2" + also have "... <= x\<^sup>2" proof - - from x x1 have "x - x^2 <= ln (1 + x)" + from x x1 have "x - x\<^sup>2 <= ln (1 + x)" by (intro ln_one_plus_pos_lower_bound) thus ?thesis by simp @@ -1449,7 +1449,7 @@ qed lemma abs_ln_one_plus_x_minus_x_bound_nonpos: - "-(1 / 2) <= x ==> x <= 0 ==> abs(ln (1 + x) - x) <= 2 * x^2" + "-(1 / 2) <= x ==> x <= 0 ==> abs(ln (1 + x) - x) <= 2 * x\<^sup>2" proof - assume a: "-(1 / 2) <= x" assume b: "x <= 0" @@ -1459,8 +1459,8 @@ apply (rule ln_add_one_self_le_self2) using a apply auto done - also have "... <= 2 * x^2" - apply (subgoal_tac "- (-x) - 2 * (-x)^2 <= ln (1 - (-x))") + also have "... <= 2 * x\<^sup>2" + apply (subgoal_tac "- (-x) - 2 * (-x)\<^sup>2 <= ln (1 - (-x))") apply (simp add: algebra_simps) apply (rule ln_one_minus_pos_lower_bound) using a b apply auto @@ -1469,7 +1469,7 @@ qed lemma abs_ln_one_plus_x_minus_x_bound: - "abs x <= 1 / 2 ==> abs(ln (1 + x) - x) <= 2 * x^2" + "abs x <= 1 / 2 ==> abs(ln (1 + x) - x) <= 2 * x\<^sup>2" apply (case_tac "0 <= x") apply (rule order_trans) apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg) @@ -2190,8 +2190,8 @@ by (auto intro!: DERIV_intros) lemma sin_cos_add_lemma: - "(sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 + - (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2 = 0" + "(sin (x + y) - (sin x * cos y + cos x * sin y))\<^sup>2 + + (cos (x + y) - (cos x * cos y - sin x * sin y))\<^sup>2 = 0" (is "?f x = 0") proof - have "\x. DERIV (\x. ?f x) x :> 0" @@ -2715,7 +2715,7 @@ lemma tan_double: "[| cos x \ 0; cos (2 * x) \ 0 |] - ==> tan (2 * x) = (2 * tan x)/(1 - (tan(x) ^ 2))" + ==> tan (2 * x) = (2 * tan x) / (1 - (tan x)\<^sup>2)" using tan_add [of x x] by (simp add: power2_eq_square) lemma tan_gt_zero: "[| 0 < x; x < pi/2 |] ==> 0 < tan x" @@ -2818,13 +2818,13 @@ lemma tan_monotone: assumes "- (pi / 2) < y" and "y < x" and "x < pi / 2" shows "tan y < tan x" proof - - have "\ x'. y \ x' \ x' \ x \ DERIV tan x' :> inverse (cos x'^2)" + have "\ x'. y \ x' \ x' \ x \ DERIV tan x' :> inverse ((cos x')\<^sup>2)" proof (rule allI, rule impI) fix x' :: real assume "y \ x' \ x' \ x" hence "-(pi/2) < x'" and "x' < pi/2" using assms by auto from cos_gt_zero_pi[OF this] have "cos x' \ 0" by auto - thus "DERIV tan x' :> inverse (cos x'^2)" by (rule DERIV_tan) + thus "DERIV tan x' :> inverse ((cos x')\<^sup>2)" by (rule DERIV_tan) qed from MVT2[OF `y < x` this] obtain z where "y < z" and "z < x" and tan_diff: "tan x - tan y = (x - y) * inverse ((cos z)\<^sup>2)" by auto @@ -3058,7 +3058,7 @@ using tan_arctan [of x] unfolding tan_def cos_arctan by (simp add: eq_divide_eq) -lemma tan_sec: "cos x \ 0 ==> 1 + tan(x) ^ 2 = inverse(cos x) ^ 2" +lemma tan_sec: "cos x \ 0 ==> 1 + (tan x)\<^sup>2 = (inverse (cos x))\<^sup>2" apply (rule power_inverse [THEN subst]) apply (rule_tac c1 = "(cos x)\<^sup>2" in real_mult_right_cancel [THEN iffD1]) apply (auto dest: field_power_not_zero @@ -3427,10 +3427,10 @@ assumes "\x\ \ 1" shows "summable (\ k. (-1)^k * (1 / real (k*2+1) * x ^ (k*2+1)))" (is "summable (?c x)") by (rule summable_Leibniz(1), rule zeroseq_arctan_series[OF assms], rule monoseq_arctan_series[OF assms]) -lemma less_one_imp_sqr_less_one: fixes x :: real assumes "\x\ < 1" shows "x^2 < 1" +lemma less_one_imp_sqr_less_one: fixes x :: real assumes "\x\ < 1" shows "x\<^sup>2 < 1" proof - from mult_left_mono[OF less_imp_le[OF `\x\ < 1`] abs_ge_zero[of x]] - have "\ x^2 \ < 1" using `\ x \ < 1` unfolding numeral_2_eq_2 power_Suc2 by auto + have "\x\<^sup>2\ < 1" using `\x\ < 1` unfolding numeral_2_eq_2 power_Suc2 by auto thus ?thesis using zero_le_power2 by auto qed @@ -3442,9 +3442,9 @@ { fix n :: nat assume "even n" hence "2 * (n div 2) = n" by presburger } note n_even=this have if_eq: "\ n x'. ?f n * real (Suc n) * x'^n = (if even n then (-1)^(n div 2) * x'^(2 * (n div 2)) else 0)" using n_even by auto - { fix x :: real assume "\x\ < 1" hence "x^2 < 1" by (rule less_one_imp_sqr_less_one) - have "summable (\ n. -1 ^ n * (x^2) ^n)" - by (rule summable_Leibniz(1), auto intro!: LIMSEQ_realpow_zero monoseq_realpow `x^2 < 1` order_less_imp_le[OF `x^2 < 1`]) + { fix x :: real assume "\x\ < 1" hence "x\<^sup>2 < 1" by (rule less_one_imp_sqr_less_one) + have "summable (\ n. -1 ^ n * (x\<^sup>2) ^n)" + by (rule summable_Leibniz(1), auto intro!: LIMSEQ_realpow_zero monoseq_realpow `x\<^sup>2 < 1` order_less_imp_le[OF `x\<^sup>2 < 1`]) hence "summable (\ n. -1 ^ n * x^(2*n))" unfolding power_mult . } note summable_Integral = this @@ -3518,11 +3518,11 @@ proof (rule allI, rule impI) fix x assume "-r < x \ x < r" hence "\x\ < r" by auto hence "\x\ < 1" using `r < 1` by auto - have "\ - (x^2) \ < 1" using less_one_imp_sqr_less_one[OF `\x\ < 1`] by auto - hence "(\ n. (- (x^2)) ^ n) sums (1 / (1 - (- (x^2))))" unfolding real_norm_def[symmetric] by (rule geometric_sums) - hence "(?c' x) sums (1 / (1 - (- (x^2))))" unfolding power_mult_distrib[symmetric] power_mult nat_mult_commute[of _ 2] by auto - hence suminf_c'_eq_geom: "inverse (1 + x^2) = suminf (?c' x)" using sums_unique unfolding inverse_eq_divide by auto - have "DERIV (\ x. suminf (?c x)) x :> (inverse (1 + x^2))" unfolding suminf_c'_eq_geom + have "\ - (x\<^sup>2) \ < 1" using less_one_imp_sqr_less_one[OF `\x\ < 1`] by auto + hence "(\ n. (- (x\<^sup>2)) ^ n) sums (1 / (1 - (- (x\<^sup>2))))" unfolding real_norm_def[symmetric] by (rule geometric_sums) + hence "(?c' x) sums (1 / (1 - (- (x\<^sup>2))))" unfolding power_mult_distrib[symmetric] power_mult nat_mult_commute[of _ 2] by auto + hence suminf_c'_eq_geom: "inverse (1 + x\<^sup>2) = suminf (?c' x)" using sums_unique unfolding inverse_eq_divide by auto + have "DERIV (\ x. suminf (?c x)) x :> (inverse (1 + x\<^sup>2))" unfolding suminf_c'_eq_geom by (rule DERIV_arctan_suminf[OF `0 < r` `r < 1` `\x\ < r`]) from DERIV_add_minus[OF this DERIV_arctan] show "DERIV (\ x. suminf (?c x) - arctan x) x :> 0" unfolding diff_minus by auto @@ -3632,7 +3632,7 @@ qed lemma arctan_half: fixes x :: real - shows "arctan x = 2 * arctan (x / (1 + sqrt(1 + x^2)))" + shows "arctan x = 2 * arctan (x / (1 + sqrt(1 + x\<^sup>2)))" proof - obtain y where low: "- (pi / 2) < y" and high: "y < pi / 2" and y_eq: "tan y = x" using tan_total by blast hence low2: "- (pi / 2) < y / 2" and high2: "y / 2 < pi / 2" by auto @@ -3640,18 +3640,18 @@ have divide_nonzero_divide: "\ A B C :: real. C \ 0 \ A / B = (A / C) / (B / C)" by auto have "0 < cos y" using cos_gt_zero_pi[OF low high] . - hence "cos y \ 0" and cos_sqrt: "sqrt ((cos y) ^ 2) = cos y" by auto - - have "1 + (tan y)^2 = 1 + sin y^2 / cos y^2" unfolding tan_def power_divide .. - also have "\ = cos y^2 / cos y^2 + sin y^2 / cos y^2" using `cos y \ 0` by auto - also have "\ = 1 / cos y^2" unfolding add_divide_distrib[symmetric] sin_cos_squared_add2 .. - finally have "1 + (tan y)^2 = 1 / cos y^2" . + hence "cos y \ 0" and cos_sqrt: "sqrt ((cos y)\<^sup>2) = cos y" by auto + + have "1 + (tan y)\<^sup>2 = 1 + (sin y)\<^sup>2 / (cos y)\<^sup>2" unfolding tan_def power_divide .. + also have "\ = (cos y)\<^sup>2 / (cos y)\<^sup>2 + (sin y)\<^sup>2 / (cos y)\<^sup>2" using `cos y \ 0` by auto + also have "\ = 1 / (cos y)\<^sup>2" unfolding add_divide_distrib[symmetric] sin_cos_squared_add2 .. + finally have "1 + (tan y)\<^sup>2 = 1 / (cos y)\<^sup>2" . have "sin y / (cos y + 1) = tan y / ((cos y + 1) / cos y)" unfolding tan_def divide_nonzero_divide[OF `cos y \ 0`, symmetric] .. also have "\ = tan y / (1 + 1 / cos y)" using `cos y \ 0` unfolding add_divide_distrib by auto - also have "\ = tan y / (1 + 1 / sqrt(cos y^2))" unfolding cos_sqrt .. - also have "\ = tan y / (1 + sqrt(1 / cos y^2))" unfolding real_sqrt_divide by auto - finally have eq: "sin y / (cos y + 1) = tan y / (1 + sqrt(1 + (tan y)^2))" unfolding `1 + (tan y)^2 = 1 / cos y^2` . + also have "\ = tan y / (1 + 1 / sqrt ((cos y)\<^sup>2))" unfolding cos_sqrt .. + also have "\ = tan y / (1 + sqrt (1 / (cos y)\<^sup>2))" unfolding real_sqrt_divide by auto + finally have eq: "sin y / (cos y + 1) = tan y / (1 + sqrt(1 + (tan y)\<^sup>2))" unfolding `1 + (tan y)\<^sup>2 = 1 / (cos y)\<^sup>2` . have "arctan x = y" using arctan_tan low high y_eq by auto also have "\ = 2 * (arctan (tan (y/2)))" using arctan_tan[OF low2 high2] by auto