# HG changeset patch # User huffman # Date 1179079542 -7200 # Node ID 617140080e6aca23cd5a0f9616e039380190147f # Parent 48dc37776d1eea04b721d97ea728a49cc32f2b90 define roots of negative reals so that many lemmas no longer require side conditions; simplification solves more goals than previously diff -r 48dc37776d1e -r 617140080e6a src/HOL/Complex/Complex.thy --- a/src/HOL/Complex/Complex.thy Sun May 13 19:15:36 2007 +0200 +++ b/src/HOL/Complex/Complex.thy Sun May 13 20:05:42 2007 +0200 @@ -394,7 +394,6 @@ lemma complex_mod_mult: "cmod (x * y) = cmod x * cmod y" apply (induct x, induct y) apply (simp add: real_sqrt_mult_distrib [symmetric]) -apply (rule_tac f=sqrt in arg_cong) apply (simp add: power2_sum power2_diff power_mult_distrib ring_distrib) done @@ -618,9 +617,7 @@ lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))" apply (simp add: cmod_def) -apply (rule real_sqrt_eq_iff [THEN iffD2]) -apply (auto simp add: complex_mult_cnj - simp del: of_real_add) +apply (simp add: complex_mult_cnj del: of_real_add) done lemma complex_Re_cnj [simp]: "Re(cnj z) = Re z" diff -r 48dc37776d1e -r 617140080e6a src/HOL/Complex/NSCA.thy --- a/src/HOL/Complex/NSCA.thy Sun May 13 19:15:36 2007 +0200 +++ b/src/HOL/Complex/NSCA.thy Sun May 13 20:05:42 2007 +0200 @@ -269,11 +269,12 @@ apply (erule (1) InfinitesimalD2) done -lemma real_sqrt_lessI: "\0 \ x; 0 < u; x < u\\ \ sqrt x < u" -by (frule (1) real_sqrt_less_mono) simp +lemma real_sqrt_lessI: "\0 < u; x < u\\ \ sqrt x < u" +(* TODO: this belongs somewhere else *) +by (frule real_sqrt_less_mono) simp lemma hypreal_sqrt_lessI: - "\x u. \0 \ x; 0 < u; x < u\\ \ ( *f* sqrt) x < u" + "\x u. \0 < u; x < u\\ \ ( *f* sqrt) x < u" by transfer (rule real_sqrt_lessI) lemma hypreal_sqrt_ge_zero: "\x. 0 \ x \ 0 \ ( *f* sqrt) x" diff -r 48dc37776d1e -r 617140080e6a src/HOL/Hyperreal/NthRoot.thy --- a/src/HOL/Hyperreal/NthRoot.thy Sun May 13 19:15:36 2007 +0200 +++ b/src/HOL/Hyperreal/NthRoot.thy Sun May 13 20:05:42 2007 +0200 @@ -4,20 +4,13 @@ Conversion to Isar and new proofs by Lawrence C Paulson, 2004 *) -header{*Existence of Nth Root*} +header {* Nth Roots of Real Numbers *} theory NthRoot imports SEQ Parity begin -definition - root :: "[nat, real] \ real" where - "root n x = (THE u. (0 < x \ 0 < u) \ (u ^ n = x))" - -definition - sqrt :: "real \ real" where - "sqrt x = root 2 x" - +subsection {* Existence of Nth Root *} text {* Various lemmas needed for this result. We follow the proof given by @@ -65,7 +58,7 @@ by (blast intro: lemma_nth_realpow_isUb_ex lemma_nth_realpow_non_empty reals_complete) -subsection{*First Half -- Lemmas First*} +subsubsection {* First Half -- Lemmas First *} lemma lemma_nth_realpow_seq: "isLub (UNIV::real set) {x. x ^ n <= a & (0::real) < x} u @@ -104,7 +97,7 @@ apply (auto simp add: real_of_nat_def) done -subsection{*Second Half*} +subsubsection {* Second Half *} lemma less_isLub_not_isUb: "[| isLub (UNIV::real set) S u; x < u |] @@ -165,7 +158,7 @@ apply (auto intro: realpow_nth_le realpow_nth_ge order_antisym) done -(* positive only *) +text {* positive only *} lemma realpow_pos_nth: "[| (0::real) < a; 0 < n |] ==> \r. 0 < r & r ^ n = a" apply (frule nth_realpow_isLub_ex, auto) apply (auto intro: realpow_nth_le realpow_nth_ge order_antisym lemma_nth_realpow_isLub_gt_zero) @@ -174,7 +167,7 @@ lemma realpow_pos_nth2: "(0::real) < a ==> \r. 0 < r & r ^ Suc n = a" by (blast intro: realpow_pos_nth) -(* uniqueness of nth positive root *) +text {* uniqueness of nth positive root *} lemma realpow_pos_nth_unique: "[| (0::real) < a; 0 < n |] ==> EX! r. 0 < r & r ^ n = a" apply (auto intro!: realpow_pos_nth) @@ -185,159 +178,250 @@ subsection {* Nth Root *} -lemma real_root_zero [simp]: "root (Suc n) 0 = 0" -apply (simp add: root_def) -apply (safe intro!: the_equality power_0_Suc elim!: realpow_zero_zero) -done +text {* We define roots of negative reals such that + @{term "root n (- x) = - root n x"}. This allows + us to omit side conditions from many theorems. *} -lemma real_root_pow_pos: - "0 < x ==> (root (Suc n) x) ^ (Suc n) = x" -apply (simp add: root_def del: realpow_Suc) -apply (drule_tac n="Suc n" in realpow_pos_nth_unique, simp) -apply (erule theI' [THEN conjunct2]) -done - -lemma real_root_pow_pos2: "0 \ x ==> (root (Suc n) x) ^ (Suc n) = x" -by (auto dest!: real_le_imp_less_or_eq dest: real_root_pow_pos) +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 real_root_pos: - "0 < x ==> root(Suc n) (x ^ (Suc n)) = x" +lemma real_root_zero [simp]: "root n 0 = 0" +unfolding root_def by simp + +lemma real_root_minus: "0 < n \ root n (- x) = - root n x" +unfolding root_def by simp + +lemma real_root_gt_zero: "\0 < n; 0 < x\ \ 0 < root n x" apply (simp add: root_def) -apply (rule the_equality) -apply (frule_tac [2] n = n in zero_less_power) -apply (auto simp add: zero_less_mult_iff) -apply (rule_tac x = u and y = x in linorder_cases) -apply (drule_tac n1 = n and x = u in zero_less_Suc [THEN [3] realpow_less]) -apply (drule_tac [4] n1 = n and x = x in zero_less_Suc [THEN [3] realpow_less]) -apply (auto) -done - -lemma real_root_pos2: "0 \ x ==> root(Suc n) (x ^ (Suc n)) = x" -by (auto dest!: real_le_imp_less_or_eq real_root_pos) - -lemma real_root_gt_zero: - "0 < x ==> 0 < root (Suc n) x" -apply (simp add: root_def del: realpow_Suc) -apply (drule_tac n="Suc n" in realpow_pos_nth_unique, simp) +apply (drule (1) realpow_pos_nth_unique) apply (erule theI' [THEN conjunct1]) done -lemma real_root_pos_pos: - "0 < x ==> 0 \ root(Suc n) x" -by (rule real_root_gt_zero [THEN order_less_imp_le]) +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 -lemma real_root_pos_pos_le: "0 \ x ==> 0 \ root(Suc n) x" +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 real_root_ge_zero: "\0 < n; 0 \ x\ \ 0 \ root n x" by (auto simp add: order_le_less real_root_gt_zero) -lemma real_root_one [simp]: "root (Suc n) 1 = 1" -apply (simp add: root_def) -apply (rule the_equality, auto) -apply (rule ccontr) -apply (rule_tac x = u and y = 1 in linorder_cases) -apply (drule_tac n = n in realpow_Suc_less_one) -apply (drule_tac [4] n = n in power_gt1_lemma) -apply (auto) +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 -lemma real_root_less_mono: - "[| 0 \ x; x < y |] ==> root(Suc n) x < root(Suc n) y" +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_one [simp]: "0 < n \ root n 1 = 1" +by (simp add: real_root_pos_unique) + +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 (rule_tac n="Suc n" in power_less_imp_less_base) -apply (simp only: real_root_pow_pos2) -apply (erule real_root_pos_pos_le) -apply (erule order_trans) -apply (erule order_less_imp_le) +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_le_mono: - "[| 0 \ x; x \ y |] ==> root(Suc n) x \ root(Suc n) y" -apply (drule_tac y = y in order_le_imp_less_or_eq) -apply (auto dest: real_root_less_mono intro: order_less_imp_le) +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) + lemma real_root_less_iff [simp]: - "[| 0 \ x; 0 \ y |] ==> (root(Suc n) x < root(Suc n) y) = (x < y)" -apply (auto intro: real_root_less_mono) -apply (rule ccontr, drule linorder_not_less [THEN iffD1]) -apply (drule_tac x = y and n = n in real_root_le_mono, auto) + "0 < n \ (root n x < root n y) = (x < y)" +apply (cases "x < y") +apply (simp add: real_root_less_mono) +apply (simp add: linorder_not_less real_root_le_mono) done lemma real_root_le_iff [simp]: - "[| 0 \ x; 0 \ y |] ==> (root(Suc n) x \ root(Suc n) y) = (x \ y)" -apply (auto intro: real_root_le_mono) -apply (simp (no_asm) add: linorder_not_less [symmetric]) -apply auto -apply (drule_tac x = y and n = n in real_root_less_mono, auto) + "0 < n \ (root n x \ root n y) = (x \ y)" +apply (cases "x \ y") +apply (simp add: real_root_le_mono) +apply (simp add: linorder_not_le real_root_less_mono) done lemma real_root_eq_iff [simp]: - "[| 0 \ x; 0 \ y |] ==> (root(Suc n) x = root(Suc n) y) = (x = y)" -apply (auto intro!: order_antisym [where 'a = real]) -apply (rule_tac n1 = n in real_root_le_iff [THEN iffD1]) -apply (rule_tac [4] n1 = n in real_root_le_iff [THEN iffD1], auto) -done + "0 < n \ (root n x = root n y) = (x = y)" +by (simp add: order_eq_iff) + +lemmas real_root_gt_0_iff [simp] = real_root_less_iff [where x=0, simplified] +lemmas real_root_lt_0_iff [simp] = real_root_less_iff [where y=0, simplified] +lemmas real_root_ge_0_iff [simp] = real_root_le_iff [where x=0, simplified] +lemmas real_root_le_0_iff [simp] = real_root_le_iff [where y=0, simplified] +lemmas real_root_eq_0_iff [simp] = real_root_eq_iff [where y=0, simplified] -lemma real_root_pos_unique: - "[| 0 \ x; 0 \ y; y ^ (Suc n) = x |] ==> root (Suc n) x = y" -by (auto dest: real_root_pos2 simp del: realpow_Suc) +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: - "[| 0 \ x; 0 \ y |] - ==> root(Suc n) (x * y) = root(Suc n) x * root(Suc n) y" -apply (rule real_root_pos_unique) -apply (auto intro!: real_root_pos_pos_le - simp add: power_mult_distrib zero_le_mult_iff real_root_pow_pos2 - simp del: realpow_Suc) -done + 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: - "0 \ x ==> (root(Suc n) (inverse x) = inverse(root(Suc n) x))" -apply (rule real_root_pos_unique) -apply (auto intro: real_root_pos_pos_le - simp add: power_inverse [symmetric] real_root_pow_pos2 - simp del: realpow_Suc) -done + 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 \ x; 0 \ y |] - ==> (root(Suc n) (x / y) = root(Suc n) x / root(Suc n) y)" -apply (simp add: divide_inverse) -apply (auto simp add: real_root_mult real_root_inverse) -done +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) -subsection{*Square Root*} +subsection {* Square Root *} -text{*needed because 2 is a binary numeral!*} -lemma root_2_eq [simp]: "root 2 = root (Suc (Suc 0))" -by (simp only: numeral_2_eq_2) +definition + sqrt :: "real \ real" where + "sqrt = root 2" -lemma real_sqrt_zero [simp]: "sqrt 0 = 0" -by (simp add: sqrt_def) +lemma pos2: "0 < (2::nat)" by simp + +lemma real_sqrt_unique: "\y\ = x; 0 \ y\ \ sqrt x = y" +unfolding sqrt_def by (rule real_root_pos_unique [OF pos2]) -lemma real_sqrt_one [simp]: "sqrt 1 = 1" -by (simp add: sqrt_def) +lemma real_sqrt_abs [simp]: "sqrt (x\) = \x\" +apply (rule real_sqrt_unique) +apply (rule power2_abs) +apply (rule abs_ge_zero) +done -lemma real_sqrt_pow2 [simp]: "0 \ x ==> (sqrt x)\ = x" -unfolding sqrt_def numeral_2_eq_2 -by (rule real_root_pow_pos2) +lemma real_sqrt_pow2 [simp]: "0 \ x \ (sqrt x)\ = x" +unfolding sqrt_def by (rule real_root_pow_pos2 [OF pos2]) -lemma real_sqrt_pow2_iff [iff]: "((sqrt x)\ = x) = (0 \ x)" +lemma real_sqrt_pow2_iff [simp]: "((sqrt x)\ = x) = (0 \ x)" apply (rule iffI) apply (erule subst) apply (rule zero_le_power2) apply (erule real_sqrt_pow2) done -lemma sqrt_eqI: "\r\ = a; 0 \ r\ \ sqrt a = r" -unfolding sqrt_def numeral_2_eq_2 -by (erule subst, erule real_root_pos2) +lemma real_sqrt_zero [simp]: "sqrt 0 = 0" +unfolding sqrt_def by (rule real_root_zero) + +lemma real_sqrt_one [simp]: "sqrt 1 = 1" +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]) + +lemma real_sqrt_mult: "sqrt (x * y) = sqrt x * sqrt y" +unfolding sqrt_def by (rule real_root_mult [OF pos2]) + +lemma real_sqrt_inverse: "sqrt (inverse x) = inverse (sqrt x)" +unfolding sqrt_def by (rule real_root_inverse [OF pos2]) + +lemma real_sqrt_divide: "sqrt (x / y) = sqrt x / sqrt y" +unfolding sqrt_def by (rule real_root_divide [OF pos2]) + +lemma real_sqrt_power: "sqrt (x ^ k) = sqrt x ^ k" +unfolding sqrt_def by (rule real_root_power [OF pos2]) + +lemma real_sqrt_gt_zero: "0 < x \ 0 < sqrt x" +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]) -lemma real_sqrt_abs [simp]: "sqrt (x\) = \x\" -apply (rule sqrt_eqI) -apply (rule power2_abs) -apply (rule abs_ge_zero) -done +lemma real_sqrt_less_mono: "x < y \ sqrt x < sqrt y" +unfolding sqrt_def by (rule real_root_less_mono [OF pos2]) + +lemma real_sqrt_le_mono: "x \ y \ sqrt x \ sqrt y" +unfolding sqrt_def by (rule real_root_le_mono [OF pos2]) + +lemma real_sqrt_less_iff [simp]: "(sqrt x < sqrt y) = (x < y)" +unfolding sqrt_def by (rule real_root_less_iff [OF pos2]) + +lemma real_sqrt_le_iff [simp]: "(sqrt x \ sqrt y) = (x \ y)" +unfolding sqrt_def by (rule real_root_le_iff [OF pos2]) + +lemma real_sqrt_eq_iff [simp]: "(sqrt x = sqrt y) = (x = y)" +unfolding sqrt_def by (rule real_root_eq_iff [OF pos2]) + +lemmas real_sqrt_gt_0_iff [simp] = real_sqrt_less_iff [where x=0, simplified] +lemmas real_sqrt_lt_0_iff [simp] = real_sqrt_less_iff [where y=0, simplified] +lemmas real_sqrt_ge_0_iff [simp] = real_sqrt_le_iff [where x=0, simplified] +lemmas real_sqrt_le_0_iff [simp] = real_sqrt_le_iff [where y=0, simplified] +lemmas real_sqrt_eq_0_iff [simp] = real_sqrt_eq_iff [where y=0, simplified] + +lemmas real_sqrt_gt_1_iff [simp] = real_sqrt_less_iff [where x=1, simplified] +lemmas real_sqrt_lt_1_iff [simp] = real_sqrt_less_iff [where y=1, simplified] +lemmas real_sqrt_ge_1_iff [simp] = real_sqrt_le_iff [where x=1, simplified] +lemmas real_sqrt_le_1_iff [simp] = real_sqrt_le_iff [where y=1, simplified] +lemmas real_sqrt_eq_1_iff [simp] = real_sqrt_eq_iff [where y=1, simplified] lemma not_real_square_gt_zero [simp]: "(~ (0::real) < x*x) = (x = 0)" apply auto @@ -345,56 +429,25 @@ apply (simp add: zero_less_mult_iff) done -lemma real_sqrt_gt_zero: "0 < x ==> 0 < sqrt(x)" -by (simp add: sqrt_def real_root_gt_zero) - -lemma real_sqrt_ge_zero: "0 \ x ==> 0 \ sqrt(x)" -by (auto intro: real_sqrt_gt_zero simp add: order_le_less) - - -(*we need to prove something like this: -lemma "[|r ^ n = a; 0 0 < r|] ==> root n a = r" -apply (case_tac n, simp) -apply (simp add: root_def) -apply (rule someI2 [of _ r], safe) -apply (auto simp del: realpow_Suc dest: power_inject_base) -*) - -lemma real_sqrt_mult_distrib: - "[| 0 \ x; 0 \ y |] ==> sqrt(x*y) = sqrt(x) * sqrt(y)" -unfolding sqrt_def numeral_2_eq_2 -by (rule real_root_mult) - -lemmas real_sqrt_mult_distrib2 = real_sqrt_mult_distrib - lemma real_sqrt_abs2 [simp]: "sqrt(x*x) = \x\" apply (subst power2_eq_square [symmetric]) apply (rule real_sqrt_abs) done lemma real_sqrt_pow2_gt_zero: "0 < x ==> 0 < (sqrt x)\" -by simp +by simp (* TODO: delete *) lemma real_sqrt_not_eq_zero: "0 < x ==> sqrt x \ 0" -apply (frule real_sqrt_pow2_gt_zero) -apply (auto simp add: numeral_2_eq_2) -done +by simp (* TODO: delete *) lemma real_inv_sqrt_pow2: "0 < x ==> inverse (sqrt(x)) ^ 2 = inverse x" by (simp add: power_inverse [symmetric]) lemma real_sqrt_eq_zero_cancel: "[| 0 \ x; sqrt(x) = 0|] ==> x = 0" -apply (drule real_le_imp_less_or_eq) -apply (auto dest: real_sqrt_not_eq_zero) -done - -lemma real_sqrt_eq_zero_cancel_iff [simp]: "0 \ x ==> ((sqrt x = 0) = (x=0))" -by (auto simp add: real_sqrt_eq_zero_cancel) +by simp lemma real_sqrt_ge_one: "1 \ x ==> 1 \ sqrt x" -apply (rule power2_le_imp_le, simp) -apply (simp add: real_sqrt_ge_zero) -done +by simp lemma sqrt_divide_self_eq: assumes nneg: "0 \ x" @@ -413,25 +466,6 @@ qed qed - -lemma real_sqrt_less_mono: "[| 0 \ x; x < y |] ==> sqrt(x) < sqrt(y)" -by (simp add: sqrt_def) - -lemma real_sqrt_le_mono: "[| 0 \ x; x \ y |] ==> sqrt(x) \ sqrt(y)" -by (simp add: sqrt_def) - -lemma real_sqrt_less_iff [simp]: - "[| 0 \ x; 0 \ y |] ==> (sqrt(x) < sqrt(y)) = (x < y)" -by (simp add: sqrt_def) - -lemma real_sqrt_le_iff [simp]: - "[| 0 \ x; 0 \ y |] ==> (sqrt(x) \ sqrt(y)) = (x \ y)" -by (simp add: sqrt_def) - -lemma real_sqrt_eq_iff [simp]: - "[| 0 \ x; 0 \ y |] ==> (sqrt(x) = sqrt(y)) = (x = y)" -by (simp add: sqrt_def) - lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r" apply (simp add: divide_inverse) apply (case_tac "r=0") @@ -441,7 +475,7 @@ subsection {* Square Root of Sum of Squares *} lemma "(sqrt (x\ + y\))\ = x\ + y\" -by (rule realpow_two_le_add_order [THEN real_sqrt_pow2_iff [THEN iffD2]]) +by simp lemma real_sqrt_mult_self_sum_ge_zero [simp]: "0 \ sqrt(x*x + y*y)" by (rule real_sqrt_ge_zero [OF real_mult_self_sum_ge_zero]) @@ -455,7 +489,7 @@ lemma real_sqrt_sum_squares_mult_squared_eq [simp]: "sqrt ((x\ + y\) * (xa\ + ya\)) ^ 2 = (x\ + y\) * (xa\ + ya\)" -by (auto simp add: zero_le_mult_iff simp del: realpow_Suc) +by (auto simp add: zero_le_mult_iff) lemma real_sqrt_sum_squares_ge1 [simp]: "x \ sqrt(x\ + y\)" by (rule power2_le_imp_le, simp_all) @@ -463,15 +497,11 @@ lemma real_sqrt_sum_squares_ge2 [simp]: "y \ sqrt(x\ + y\)" by (rule power2_le_imp_le, simp_all) -lemma real_sqrt_sos_less_one_iff [simp]: "(sqrt(x\ + y\) < 1) = (x\ + y\ < 1)" -apply (subst real_sqrt_one [symmetric]) -apply (rule real_sqrt_less_iff, auto) -done +lemma real_sqrt_sos_less_one_iff: "(sqrt (x\ + y\) < 1) = (x\ + y\ < 1)" +by (rule real_sqrt_lt_1_iff) -lemma real_sqrt_sos_eq_one_iff [simp]: "(sqrt(x\ + y\) = 1) = (x\ + y\ = 1)" -apply (subst real_sqrt_one [symmetric]) -apply (rule real_sqrt_eq_iff, auto) -done +lemma real_sqrt_sos_eq_one_iff: "(sqrt (x\ + y\) = 1) = (x\ + y\ = 1)" +by (rule real_sqrt_eq_1_iff) lemma power2_sum: fixes x y :: "'a::{number_ring,recpower}" @@ -501,4 +531,24 @@ apply (simp add: add_increasing) done +text "Legacy theorem names:" +lemmas real_root_pos2 = real_root_power_cancel +lemmas real_root_pos_pos = real_root_gt_zero [THEN order_less_imp_le] +lemmas real_root_pos_pos_le = real_root_ge_zero +lemmas real_sqrt_mult_distrib = real_sqrt_mult +lemmas real_sqrt_mult_distrib2 = real_sqrt_mult +lemmas real_sqrt_eq_zero_cancel_iff = real_sqrt_eq_0_iff + +(* needed for CauchysMeanTheorem.het_base from AFP *) +lemma real_root_pos: "0 < x \ root (Suc n) (x ^ (Suc n)) = x" +by (rule real_root_power_cancel [OF zero_less_Suc order_less_imp_le]) + +(* FIXME: the stronger version of real_root_less_iff + breaks CauchysMeanTheorem.list_gmean_gt_iff from AFP. *) + +declare real_root_less_iff [simp del] +lemma real_root_less_iff_nonneg [simp]: + "\0 < n; 0 \ x; 0 \ y\ \ (root n x < root n y) = (x < y)" +by (rule real_root_less_iff) + end diff -r 48dc37776d1e -r 617140080e6a src/HOL/Hyperreal/Transcendental.thy --- a/src/HOL/Hyperreal/Transcendental.thy Sun May 13 19:15:36 2007 +0200 +++ b/src/HOL/Hyperreal/Transcendental.thy Sun May 13 20:05:42 2007 +0200 @@ -1928,7 +1928,8 @@ lemma lemma_real_divide_sqrt_ge_minus_one: "0 < x ==> -1 \ x/(sqrt (x * x + y * y))" -by (simp add: divide_const_simps linorder_not_le [symmetric]) +by (simp add: divide_const_simps linorder_not_le [symmetric] + del: real_sqrt_le_0_iff real_sqrt_ge_0_iff) lemma real_sqrt_sum_squares_gt_zero1: "x < 0 ==> 0 < sqrt (x * x + y * y)" apply (rule real_sqrt_gt_zero) @@ -1943,14 +1944,10 @@ done lemma real_sqrt_sum_squares_gt_zero3: "x \ 0 ==> 0 < sqrt(x\ + y\)" -apply (cut_tac x = x and y = 0 in linorder_less_linear) -apply (auto intro: real_sqrt_sum_squares_gt_zero2 real_sqrt_sum_squares_gt_zero1 simp add: numeral_2_eq_2) -done +by (simp add: add_pos_nonneg) lemma real_sqrt_sum_squares_gt_zero3a: "y \ 0 ==> 0 < sqrt(x\ + y\)" -apply (drule_tac y = x in real_sqrt_sum_squares_gt_zero3) -apply (auto simp add: real_add_commute) -done +by (simp add: add_nonneg_pos) lemma real_sqrt_sum_squares_eq_cancel: "sqrt(x\ + y\) = x ==> y = 0" by (drule_tac f = "%x. x\" in arg_cong, auto) @@ -1965,7 +1962,8 @@ lemma lemma_real_divide_sqrt_ge_minus_one2: "x < 0 ==> -1 \ x/(sqrt (x * x + y * y))" -apply (simp add: divide_const_simps) +apply (simp add: divide_const_simps + del: real_sqrt_gt_0_iff real_sqrt_lt_0_iff) apply (insert minus_le_real_sqrt_sumsq [of x y], arith) done @@ -1979,10 +1977,12 @@ by (subst add_commute, simp add: minus_sqrt_le) lemma not_neg_sqrt_sumsq: "~ sqrt (x * x + y * y) < 0" -by (simp add: linorder_not_less) +by (simp add: linorder_not_less + del: real_sqrt_lt_0_iff real_sqrt_ge_0_iff) lemma cos_x_y_ge_minus_one: "-1 \ x / sqrt (x * x + y * y)" -by (simp add: minus_sqrt_le not_neg_sqrt_sumsq divide_const_simps) +by (simp add: minus_sqrt_le not_neg_sqrt_sumsq divide_const_simps + del: real_sqrt_gt_0_iff real_sqrt_lt_0_iff) lemma cos_x_y_ge_minus_one1a [simp]: "-1 \ y / sqrt (x * x + y * y)" by (subst add_commute, simp add: cos_x_y_ge_minus_one) @@ -2006,11 +2006,13 @@ lemma cos_abs_x_y_ge_minus_one [simp]: "-1 \ \x\ / sqrt (x * x + y * y)" -by (auto simp add: divide_const_simps abs_if linorder_not_le [symmetric]) +by (auto simp add: divide_const_simps abs_if linorder_not_le [symmetric] + simp del: real_sqrt_ge_0_iff real_sqrt_le_0_iff) lemma cos_abs_x_y_le_one [simp]: "\x\ / sqrt (x * x + y * y) \ 1" -apply (insert minus_le_real_sqrt_sumsq [of x y] le_real_sqrt_sumsq [of x y]) -apply (auto simp add: divide_const_simps abs_if linorder_neq_iff) +apply (insert minus_le_real_sqrt_sumsq [of x y] le_real_sqrt_sumsq [of x y]) +apply (auto simp add: divide_const_simps abs_if linorder_neq_iff + simp del: real_sqrt_gt_0_iff real_sqrt_eq_0_iff) done declare cos_arcos [OF cos_abs_x_y_ge_minus_one cos_abs_x_y_le_one, simp] @@ -2165,20 +2167,15 @@ apply (rule real_add_commute [THEN subst]) apply (rule real_sqrt_ge_abs1) done -declare real_sqrt_ge_abs1 [simp] real_sqrt_ge_abs2 [simp] lemma real_sqrt_two_gt_zero [simp]: "0 < sqrt 2" -by (auto intro: real_sqrt_gt_zero) +by simp lemma real_sqrt_two_ge_zero [simp]: "0 \ sqrt 2" -by (auto intro: real_sqrt_ge_zero) +by simp lemma real_sqrt_two_gt_one [simp]: "1 < sqrt 2" -apply (rule order_less_le_trans [of _ "7/5"], simp) -apply (rule_tac n = 1 in realpow_increasing) - prefer 3 apply (simp add: numeral_2_eq_2 [symmetric] del: realpow_Suc) -apply (simp_all add: numeral_2_eq_2) -done +by simp lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u" by (simp add: divide_less_eq mult_compare_simps)