# HG changeset patch # User huffman # Date 1176764100 -7200 # Node ID d9be18bd7a28332e9b9aefbb33fbbe68f5660f09 # Parent 296813d7d3069fe428827c81a332db5e1c799fbf moved root and sqrt lemmas from Transcendental.thy to NthRoot.thy diff -r 296813d7d306 -r d9be18bd7a28 src/HOL/Hyperreal/NthRoot.thy --- a/src/HOL/Hyperreal/NthRoot.thy Tue Apr 17 00:37:14 2007 +0200 +++ b/src/HOL/Hyperreal/NthRoot.thy Tue Apr 17 00:55:00 2007 +0200 @@ -239,6 +239,80 @@ apply (auto) done +lemma real_root_less_mono: + "[| 0 \ x; x < y |] ==> root(Suc n) x < root(Suc n) y" +apply (frule order_le_less_trans, assumption) +apply (frule_tac n1 = n in real_root_pow_pos2 [THEN ssubst]) +apply (rotate_tac 1, assumption) +apply (frule_tac n1 = n in real_root_pow_pos [THEN ssubst]) +apply (rotate_tac 3, assumption) +apply (drule_tac y = "root (Suc n) y ^ Suc n" in order_less_imp_le) +apply (frule_tac n = n in real_root_pos_pos_le) +apply (frule_tac n = n in real_root_pos_pos) +apply (drule_tac x = "root (Suc n) x" and y = "root (Suc n) y" in realpow_increasing) +apply (assumption, assumption) +apply (drule_tac x = "root (Suc n) x" in order_le_imp_less_or_eq) +apply auto +apply (drule_tac f = "%x. x ^ (Suc n)" in arg_cong) +apply (auto simp add: real_root_pow_pos2 simp del: realpow_Suc) +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) +done + +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) +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) +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 + +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) + +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 + +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 + +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 + subsection{*Square Root*} @@ -407,4 +481,41 @@ 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_sqrt_sos_less_one_iff [simp]: "(sqrt(x\ + y\) < 1) = (x\ + y\ < 1)" +apply (rule real_sqrt_one [THEN subst], safe) +apply (rule_tac [2] real_sqrt_less_mono) +apply (drule real_sqrt_less_iff [THEN [2] rev_iffD1], auto) +done + +lemma real_sqrt_sos_eq_one_iff [simp]: "(sqrt(x\ + y\) = 1) = (x\ + y\ = 1)" +apply (rule real_sqrt_one [THEN subst], safe) +apply (drule real_sqrt_eq_iff [THEN [2] rev_iffD1], auto) +done + +lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r" +apply (simp add: divide_inverse) +apply (case_tac "r=0") +apply (auto simp add: mult_ac) +done + + end diff -r 296813d7d306 -r d9be18bd7a28 src/HOL/Hyperreal/Transcendental.thy --- a/src/HOL/Hyperreal/Transcendental.thy Tue Apr 17 00:37:14 2007 +0200 +++ b/src/HOL/Hyperreal/Transcendental.thy Tue Apr 17 00:55:00 2007 +0200 @@ -1911,116 +1911,6 @@ by (cut_tac x = x in sin_cos_squared_add3, auto) -lemma real_root_less_mono: - "[| 0 \ x; x < y |] ==> root(Suc n) x < root(Suc n) y" -apply (frule order_le_less_trans, assumption) -apply (frule_tac n1 = n in real_root_pow_pos2 [THEN ssubst]) -apply (rotate_tac 1, assumption) -apply (frule_tac n1 = n in real_root_pow_pos [THEN ssubst]) -apply (rotate_tac 3, assumption) -apply (drule_tac y = "root (Suc n) y ^ Suc n" in order_less_imp_le) -apply (frule_tac n = n in real_root_pos_pos_le) -apply (frule_tac n = n in real_root_pos_pos) -apply (drule_tac x = "root (Suc n) x" and y = "root (Suc n) y" in realpow_increasing) -apply (assumption, assumption) -apply (drule_tac x = "root (Suc n) x" in order_le_imp_less_or_eq) -apply auto -apply (drule_tac f = "%x. x ^ (Suc n)" in arg_cong) -apply (auto simp add: real_root_pow_pos2 simp del: realpow_Suc) -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) -done - -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) -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) -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 - -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) - -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 - -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 - -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_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_sqrt_sos_less_one_iff [simp]: "(sqrt(x\ + y\) < 1) = (x\ + y\ < 1)" -apply (rule real_sqrt_one [THEN subst], safe) -apply (rule_tac [2] real_sqrt_less_mono) -apply (drule real_sqrt_less_iff [THEN [2] rev_iffD1], auto) -done - -lemma real_sqrt_sos_eq_one_iff [simp]: "(sqrt(x\ + y\) = 1) = (x\ + y\ = 1)" -apply (rule real_sqrt_one [THEN subst], safe) -apply (drule real_sqrt_eq_iff [THEN [2] rev_iffD1], auto) -done - -lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r" -apply (simp add: divide_inverse) -apply (case_tac "r=0") -apply (auto simp add: mult_ac) -done - - subsection{*Theorems About Sqrt, Transcendental Functions for Complex*} lemma le_real_sqrt_sumsq [simp]: "x \ sqrt (x * x + y * y)"