# HG changeset patch # User hoelzl # Date 1363945303 -3600 # Node ID dc39d69774bb9524dbd732a871c6ab320101af07 # Parent 80efd8c49f52d8446304530ec4351ee110e2993a modernized definition of root: use the_inv, handle positive and negative case uniformly, and 0-th root is constant 0 diff -r 80efd8c49f52 -r dc39d69774bb src/HOL/Log.thy --- a/src/HOL/Log.thy Fri Mar 22 10:41:43 2013 +0100 +++ b/src/HOL/Log.thy Fri Mar 22 10:41:43 2013 +0100 @@ -244,7 +244,7 @@ lemma root_powr_inverse: "0 < n \ 0 < x \ root n x = x powr (1/n)" -by (auto simp: root_def powr_realpow[symmetric] powr_powr) + by (rule real_root_pos_unique) (auto simp: powr_realpow[symmetric] powr_powr) lemma ln_powr: "0 < x ==> 0 < y ==> ln(x powr y) = y * ln x" by (unfold powr_def, simp) diff -r 80efd8c49f52 -r dc39d69774bb src/HOL/NthRoot.thy --- a/src/HOL/NthRoot.thy Fri Mar 22 10:41:43 2013 +0100 +++ b/src/HOL/NthRoot.thy Fri Mar 22 10:41:43 2013 +0100 @@ -10,6 +10,17 @@ imports Parity Deriv begin +lemma abs_sgn_eq: "abs (sgn x :: real) = (if x = 0 then 0 else 1)" + by (simp add: sgn_real_def) + +lemma inverse_sgn: "sgn (inverse a) = inverse (sgn a :: real)" + by (simp add: sgn_real_def) + +lemma power_eq_iff_eq_base: + fixes a b :: "_ :: linordered_semidom" + shows "0 < n \ 0 \ a \ 0 \ b \ a ^ n = b ^ n \ a = b" + using power_eq_imp_eq_base[of a n b] by auto + subsection {* Existence of Nth Root *} text {* Existence follows from the Intermediate Value Theorem *} @@ -43,11 +54,8 @@ text {* Uniqueness of nth positive root *} -lemma realpow_pos_nth_unique: - "\0 < n; 0 < a\ \ \!r. 0 < r \ r ^ n = (a::real)" -apply (auto intro!: realpow_pos_nth) -apply (rule_tac n=n in power_eq_imp_eq_base, simp_all) -done +lemma realpow_pos_nth_unique: "\0 < n; 0 < a\ \ \!r. 0 < r \ r ^ n = (a::real)" + by (auto intro!: realpow_pos_nth simp: power_eq_iff_eq_base) subsection {* Nth Root *} @@ -55,66 +63,86 @@ @{term "root n (- x) = - root n x"}. This allows us to omit side conditions from many theorems. *} -definition - root :: "[nat, real] \ real" where - "root n x = (if 0 < x then (THE u. 0 < u \ u ^ n = x) else - if x < 0 then - (THE u. 0 < u \ u ^ n = - x) else 0)" +lemma inj_sgn_power: assumes "0 < n" shows "inj (\y. sgn y * \y\^n :: real)" (is "inj ?f") +proof (rule injI) + have x: "\a b :: real. (0 < a \ b < 0) \ (a < 0 \ 0 < b) \ a \ b" by auto + fix x y assume "?f x = ?f y" with power_eq_iff_eq_base[of n "\x\" "\y\"] `0a\ ^ n = x \ x = sgn b * \b\ ^ n \ 0 < n \ a = (b::real)" + using inj_sgn_power[THEN injD, of n a b] by simp + +definition root :: "nat \ real \ real" where + "root n x = (if n = 0 then 0 else the_inv (\y. sgn y * \y\^n) x)" + +lemma root_0 [simp]: "root 0 x = 0" + by (simp add: root_def) + +lemma root_sgn_power: "0 < n \ root n (sgn y * \y\^n) = y" + using the_inv_f_f[OF inj_sgn_power] by (simp add: root_def) + +lemma sgn_power_root: + assumes "0 < n" shows "sgn (root n x) * \(root n x)\^n = x" (is "?f (root n x) = x") +proof cases + assume "x \ 0" + with realpow_pos_nth[OF `0 < n`, of "\x\"] obtain r where "0 < r" "r ^ n = \x\" by auto + with `x \ 0` have S: "x \ range ?f" + by (intro image_eqI[of _ _ "sgn x * r"]) + (auto simp: abs_mult sgn_mult power_mult_distrib abs_sgn_eq mult_sgn_abs) + from `0 < n` f_the_inv_into_f[OF inj_sgn_power[OF `0 < n`] this] show ?thesis + by (simp add: root_def) +qed (insert `0 < n` root_sgn_power[of n 0], simp) + +lemma split_root: "P (root n x) \ (n = 0 \ P 0) \ (0 < n \ (\y. sgn y * \y\^n = x \ P y))" + apply (cases "n = 0") + apply simp_all + apply (metis root_sgn_power sgn_power_root) + done lemma real_root_zero [simp]: "root n 0 = 0" -unfolding root_def by simp + by (simp split: split_root add: sgn_zero_iff) + +lemma real_root_minus: "root n (- x) = - root n x" + by (clarsimp split: split_root elim!: sgn_power_injE simp: sgn_minus) -lemma real_root_minus: "0 < n \ root n (- x) = - root n x" -unfolding root_def by simp +lemma real_root_less_mono: "\0 < n; x < y\ \ root n x < root n y" +proof (clarsimp split: split_root) + have x: "\a b :: real. (0 < b \ a < 0) \ \ a > b" by auto + fix a b :: real assume "0 < n" "sgn a * \a\ ^ n < sgn b * \b\ ^ n" then show "a < b" + using power_less_imp_less_base[of a n b] power_less_imp_less_base[of "-b" n "-a"] + by (simp add: sgn_real_def power_less_zero_eq x[of "a ^ n" "- ((- b) ^ n)"] split: split_if_asm) +qed lemma real_root_gt_zero: "\0 < n; 0 < x\ \ 0 < root n x" -apply (simp add: root_def) -apply (drule (1) realpow_pos_nth_unique) -apply (erule theI' [THEN conjunct1]) -done + using real_root_less_mono[of n 0 x] by simp + +lemma real_root_ge_zero: "0 \ x \ 0 \ root n x" + using real_root_gt_zero[of n x] by (cases "n = 0") (auto simp add: le_less) lemma real_root_pow_pos: (* TODO: rename *) "\0 < n; 0 < x\ \ root n x ^ n = x" -apply (simp add: root_def) -apply (drule (1) realpow_pos_nth_unique) -apply (erule theI' [THEN conjunct2]) -done + using sgn_power_root[of n x] real_root_gt_zero[of n x] by simp lemma real_root_pow_pos2 [simp]: (* TODO: rename *) "\0 < n; 0 \ x\ \ root n x ^ n = x" by (auto simp add: order_le_less real_root_pow_pos) +lemma sgn_root: "0 < n \ sgn (root n x) = sgn x" + by (auto split: split_root simp: sgn_real_def power_less_zero_eq) + lemma odd_real_root_pow: "odd n \ root n x ^ n = x" -apply (rule_tac x=0 and y=x in linorder_le_cases) -apply (erule (1) real_root_pow_pos2 [OF odd_pos]) -apply (subgoal_tac "root n (- x) ^ n = - x") -apply (simp add: real_root_minus odd_pos) -apply (simp add: odd_pos) -done - -lemma real_root_ge_zero: "\0 < n; 0 \ x\ \ 0 \ root n x" -by (auto simp add: order_le_less real_root_gt_zero) + using sgn_power_root[of n x] by (simp add: odd_pos sgn_real_def split: split_if_asm) lemma real_root_power_cancel: "\0 < n; 0 \ x\ \ root n (x ^ n) = x" -apply (subgoal_tac "0 \ x ^ n") -apply (subgoal_tac "0 \ root n (x ^ n)") -apply (subgoal_tac "root n (x ^ n) ^ n = x ^ n") -apply (erule (3) power_eq_imp_eq_base) -apply (erule (1) real_root_pow_pos2) -apply (erule (1) real_root_ge_zero) -apply (erule zero_le_power) -done + using root_sgn_power[of n x] by (auto simp add: le_less power_0_left) lemma odd_real_root_power_cancel: "odd n \ root n (x ^ n) = x" -apply (rule_tac x=0 and y=x in linorder_le_cases) -apply (erule (1) real_root_power_cancel [OF odd_pos]) -apply (subgoal_tac "root n ((- x) ^ n) = - x") -apply (simp add: real_root_minus odd_pos) -apply (erule real_root_power_cancel [OF odd_pos], simp) -done + using root_sgn_power[of n x] by (simp add: odd_pos sgn_real_def power_0_left split: split_if_asm) -lemma real_root_pos_unique: - "\0 < n; 0 \ y; y ^ n = x\ \ root n x = y" -by (erule subst, rule real_root_power_cancel) +lemma real_root_pos_unique: "\0 < n; 0 \ y; y ^ n = x\ \ root n x = y" + using root_sgn_power[of n y] by (auto simp add: le_less power_0_left) lemma odd_real_root_unique: "\odd n; y ^ n = x\ \ root n x = y" @@ -125,32 +153,8 @@ text {* Root function is strictly monotonic, hence injective *} -lemma real_root_less_mono_lemma: - "\0 < n; 0 \ x; x < y\ \ root n x < root n y" -apply (subgoal_tac "0 \ y") -apply (subgoal_tac "root n x ^ n < root n y ^ n") -apply (erule power_less_imp_less_base) -apply (erule (1) real_root_ge_zero) -apply simp -apply simp -done - -lemma real_root_less_mono: "\0 < n; x < y\ \ root n x < root n y" -apply (cases "0 \ x") -apply (erule (2) real_root_less_mono_lemma) -apply (cases "0 \ y") -apply (rule_tac y=0 in order_less_le_trans) -apply (subgoal_tac "0 < root n (- x)") -apply (simp add: real_root_minus) -apply (simp add: real_root_gt_zero) -apply (simp add: real_root_ge_zero) -apply (subgoal_tac "root n (- y) < root n (- x)") -apply (simp add: real_root_minus) -apply (simp add: real_root_less_mono_lemma) -done - lemma real_root_le_mono: "\0 < n; x \ y\ \ root n x \ root n y" -by (auto simp add: order_le_less real_root_less_mono) + by (auto simp add: order_le_less real_root_less_mono) lemma real_root_less_iff [simp]: "0 < n \ (root n x < root n y) = (x < y)" @@ -191,26 +195,34 @@ lemma real_root_eq_1_iff [simp]: "0 < n \ (root n x = 1) = (x = 1)" by (insert real_root_eq_iff [where y=1], simp) +text {* Roots of multiplication and division *} + +lemma real_root_mult: "root n (x * y) = root n x * root n y" + by (auto split: split_root elim!: sgn_power_injE simp: sgn_mult abs_mult power_mult_distrib) + +lemma real_root_inverse: "root n (inverse x) = inverse (root n x)" + by (auto split: split_root elim!: sgn_power_injE simp: inverse_sgn power_inverse) + +lemma real_root_divide: "root n (x / y) = root n x / root n y" + by (simp add: divide_inverse real_root_mult real_root_inverse) + +lemma real_root_abs: "0 < n \ root n \x\ = \root n x\" + by (simp add: abs_if real_root_minus) + +lemma real_root_power: "0 < n \ root n (x ^ k) = root n x ^ k" + by (induct k) (simp_all add: real_root_mult) + text {* Roots of roots *} lemma real_root_Suc_0 [simp]: "root (Suc 0) x = x" by (simp add: odd_real_root_unique) -lemma real_root_pos_mult_exp: - "\0 < m; 0 < n; 0 < x\ \ root (m * n) x = root m (root n x)" -by (rule real_root_pos_unique, simp_all add: power_mult) +lemma real_root_mult_exp: "root (m * n) x = root m (root n x)" + by (auto split: split_root elim!: sgn_power_injE + simp: sgn_zero_iff sgn_mult power_mult[symmetric] abs_mult power_mult_distrib abs_sgn_eq) -lemma real_root_mult_exp: - "\0 < m; 0 < n\ \ root (m * n) x = root m (root n x)" -apply (rule linorder_cases [where x=x and y=0]) -apply (subgoal_tac "root (m * n) (- x) = root m (root n (- x))") -apply (simp add: real_root_minus) -apply (simp_all add: real_root_pos_mult_exp) -done - -lemma real_root_commute: - "\0 < m; 0 < n\ \ root m (root n x) = root n (root m x)" -by (simp add: real_root_mult_exp [symmetric] mult_commute) +lemma real_root_commute: "root m (root n x) = root n (root m x)" + by (simp add: real_root_mult_exp [symmetric] mult_commute) text {* Monotonicity in first argument *} @@ -236,118 +248,35 @@ "\0 < n; n < N; 0 \ x; x \ 1\ \ root n x \ root N x" by (auto simp add: order_le_less real_root_strict_increasing) -text {* Roots of multiplication and division *} - -lemma real_root_mult_lemma: - "\0 < n; 0 \ x; 0 \ y\ \ root n (x * y) = root n x * root n y" -by (simp add: real_root_pos_unique mult_nonneg_nonneg power_mult_distrib) - -lemma real_root_inverse_lemma: - "\0 < n; 0 \ x\ \ root n (inverse x) = inverse (root n x)" -by (simp add: real_root_pos_unique power_inverse [symmetric]) - -lemma real_root_mult: - assumes n: "0 < n" - shows "root n (x * y) = root n x * root n y" -proof (rule linorder_le_cases, rule_tac [!] linorder_le_cases) - assume "0 \ x" and "0 \ y" - thus ?thesis by (rule real_root_mult_lemma [OF n]) -next - assume "0 \ x" and "y \ 0" - hence "0 \ x" and "0 \ - y" by simp_all - hence "root n (x * - y) = root n x * root n (- y)" - by (rule real_root_mult_lemma [OF n]) - thus ?thesis by (simp add: real_root_minus [OF n]) -next - assume "x \ 0" and "0 \ y" - hence "0 \ - x" and "0 \ y" by simp_all - hence "root n (- x * y) = root n (- x) * root n y" - by (rule real_root_mult_lemma [OF n]) - thus ?thesis by (simp add: real_root_minus [OF n]) -next - assume "x \ 0" and "y \ 0" - hence "0 \ - x" and "0 \ - y" by simp_all - hence "root n (- x * - y) = root n (- x) * root n (- y)" - by (rule real_root_mult_lemma [OF n]) - thus ?thesis by (simp add: real_root_minus [OF n]) -qed - -lemma real_root_inverse: - assumes n: "0 < n" - shows "root n (inverse x) = inverse (root n x)" -proof (rule linorder_le_cases) - assume "0 \ x" - thus ?thesis by (rule real_root_inverse_lemma [OF n]) -next - assume "x \ 0" - hence "0 \ - x" by simp - hence "root n (inverse (- x)) = inverse (root n (- x))" - by (rule real_root_inverse_lemma [OF n]) - thus ?thesis by (simp add: real_root_minus [OF n]) -qed - -lemma real_root_divide: - "0 < n \ root n (x / y) = root n x / root n y" -by (simp add: divide_inverse real_root_mult real_root_inverse) - -lemma real_root_power: - "0 < n \ root n (x ^ k) = root n x ^ k" -by (induct k, simp_all add: real_root_mult) - -lemma real_root_abs: "0 < n \ root n \x\ = \root n x\" -by (simp add: abs_if real_root_minus) - text {* Continuity and derivatives *} -lemma isCont_root_pos: - assumes n: "0 < n" - assumes x: "0 < x" - shows "isCont (root n) x" -proof - - have "isCont (root n) (root n x ^ n)" - proof (rule isCont_inverse_function [where f="\a. a ^ n"]) - show "0 < root n x" using n x by simp - show "\z. \z - root n x\ \ root n x \ root n (z ^ n) = z" - by (simp add: abs_le_iff real_root_power_cancel n) - show "\z. \z - root n x\ \ root n x \ isCont (\a. a ^ n) z" - by simp - qed - thus ?thesis using n x by simp -qed +lemma isCont_real_root: "isCont (root n) x" +proof cases + assume n: "0 < n" + let ?f = "\y::real. sgn y * \y\^n" + have "continuous_on ({0..} \ {.. 0}) (\x. if 0 < x then x ^ n else - ((-x) ^ n) :: real)" + using n by (intro continuous_on_If continuous_on_intros) auto + then have "continuous_on UNIV ?f" + by (rule continuous_on_cong[THEN iffD1, rotated 2]) (auto simp: not_less real_sgn_neg le_less n) + then have [simp]: "\x. isCont ?f x" + by (simp add: continuous_on_eq_continuous_at) -lemma isCont_root_neg: - "\0 < n; x < 0\ \ isCont (root n) x" -apply (subgoal_tac "isCont (\x. - root n (- x)) x") -apply (simp add: real_root_minus) -apply (rule isCont_o2 [OF isCont_minus [OF isCont_ident]]) -apply (simp add: isCont_root_pos) -done - -lemma isCont_root_zero: - "0 < n \ isCont (root n) 0" -unfolding isCont_def -apply (rule LIM_I) -apply (rule_tac x="r ^ n" in exI, safe) -apply (simp) -apply (simp add: real_root_abs [symmetric]) -apply (rule_tac n="n" in power_less_imp_less_base, simp_all) -done - -lemma isCont_real_root: "0 < n \ isCont (root n) x" -apply (rule_tac x=x and y=0 in linorder_cases) -apply (simp_all add: isCont_root_pos isCont_root_neg isCont_root_zero) -done + have "isCont (root n) (?f (root n x))" + by (rule isCont_inverse_function [where f="?f" and d=1]) (auto simp: root_sgn_power n) + then show ?thesis + by (simp add: sgn_power_root n) +qed (simp add: root_def[abs_def]) lemma tendsto_real_root[tendsto_intros]: - "(f ---> x) F \ 0 < n \ ((\x. root n (f x)) ---> root n x) F" - using isCont_tendsto_compose[OF isCont_real_root, of n f x F] . + "(f ---> x) F \ ((\x. root n (f x)) ---> root n x) F" + using isCont_tendsto_compose[OF isCont_real_root, of f x F] . lemma continuous_real_root[continuous_intros]: - "continuous F f \ 0 < n \ continuous F (\x. root n (f x))" + "continuous F f \ continuous F (\x. root n (f x))" unfolding continuous_def by (rule tendsto_real_root) lemma continuous_on_real_root[continuous_on_intros]: - "continuous_on s f \ 0 < n \ continuous_on s (\x. root n (f x))" + "continuous_on s f \ continuous_on s (\x. root n (f x))" unfolding continuous_on_def by (auto intro: tendsto_real_root) lemma DERIV_real_root: @@ -363,9 +292,7 @@ by (rule DERIV_pow) show "real n * root n x ^ (n - Suc 0) \ 0" using n x by simp - show "isCont (root n) x" - using n by (rule isCont_real_root) -qed +qed (rule isCont_real_root) lemma DERIV_odd_real_root: assumes n: "odd n" @@ -380,9 +307,7 @@ by (rule DERIV_pow) show "real n * root n x ^ (n - Suc 0) \ 0" using odd_pos [OF n] x by simp - show "isCont (root n) x" - using odd_pos [OF n] by (rule isCont_real_root) -qed +qed (rule isCont_real_root) lemma DERIV_even_real_root: assumes n: "0 < n" and "even n" @@ -396,7 +321,7 @@ proof (rule allI, rule impI, erule conjE) fix y assume "x - 1 < y" and "y < 0" hence "root n (-y) ^ n = -y" using `0 < n` by simp - with real_root_minus[OF `0 < n`] and `even n` + with real_root_minus and `even n` show "- (root n y ^ n) = y" by simp qed next @@ -404,9 +329,7 @@ by (auto intro!: DERIV_intros) show "- real n * root n x ^ (n - Suc 0) \ 0" using n x by simp - show "isCont (root n) x" - using n by (rule isCont_real_root) -qed +qed (rule isCont_real_root) lemma DERIV_real_root_generic: assumes "0 < n" and "x \ 0" @@ -421,8 +344,7 @@ subsection {* Square Root *} -definition - sqrt :: "real \ real" where +definition sqrt :: "real \ real" where "sqrt = root 2" lemma pos2: "0 < (2::nat)" by simp @@ -453,16 +375,16 @@ unfolding sqrt_def by (rule real_root_one [OF pos2]) lemma real_sqrt_minus: "sqrt (- x) = - sqrt x" -unfolding sqrt_def by (rule real_root_minus [OF pos2]) +unfolding sqrt_def by (rule real_root_minus) lemma real_sqrt_mult: "sqrt (x * y) = sqrt x * sqrt y" -unfolding sqrt_def by (rule real_root_mult [OF pos2]) +unfolding sqrt_def by (rule real_root_mult) lemma real_sqrt_inverse: "sqrt (inverse x) = inverse (sqrt x)" -unfolding sqrt_def by (rule real_root_inverse [OF pos2]) +unfolding sqrt_def by (rule real_root_inverse) lemma real_sqrt_divide: "sqrt (x / y) = sqrt x / sqrt y" -unfolding sqrt_def by (rule real_root_divide [OF pos2]) +unfolding sqrt_def by (rule real_root_divide) lemma real_sqrt_power: "sqrt (x ^ k) = sqrt x ^ k" unfolding sqrt_def by (rule real_root_power [OF pos2]) @@ -471,7 +393,7 @@ unfolding sqrt_def by (rule real_root_gt_zero [OF pos2]) lemma real_sqrt_ge_zero: "0 \ x \ 0 \ sqrt x" -unfolding sqrt_def by (rule real_root_ge_zero [OF pos2]) +unfolding sqrt_def by (rule real_root_ge_zero) lemma real_sqrt_less_mono: "x < y \ sqrt x < sqrt y" unfolding sqrt_def by (rule real_root_less_mono [OF pos2]) @@ -501,19 +423,19 @@ lemmas real_sqrt_eq_1_iff [simp] = real_sqrt_eq_iff [where y=1, simplified] lemma isCont_real_sqrt: "isCont sqrt x" -unfolding sqrt_def by (rule isCont_real_root [OF pos2]) +unfolding sqrt_def by (rule isCont_real_root) lemma tendsto_real_sqrt[tendsto_intros]: "(f ---> x) F \ ((\x. sqrt (f x)) ---> sqrt x) F" - unfolding sqrt_def by (rule tendsto_real_root [OF _ pos2]) + unfolding sqrt_def by (rule tendsto_real_root) lemma continuous_real_sqrt[continuous_intros]: "continuous F f \ continuous F (\x. sqrt (f x))" - unfolding sqrt_def by (rule continuous_real_root [OF _ pos2]) + unfolding sqrt_def by (rule continuous_real_root) lemma continuous_on_real_sqrt[continuous_on_intros]: "continuous_on s f \ 0 < n \ continuous_on s (\x. sqrt (f x))" - unfolding sqrt_def by (rule continuous_on_real_root [OF _ pos2]) + unfolding sqrt_def by (rule continuous_on_real_root) lemma DERIV_real_sqrt_generic: assumes "x \ 0"