moved root and sqrt lemmas from Transcendental.thy to NthRoot.thy
authorhuffman
Tue Apr 17 00:55:00 2007 +0200 (2007-04-17)
changeset 22721d9be18bd7a28
parent 22720 296813d7d306
child 22722 704de05715b4
moved root and sqrt lemmas from Transcendental.thy to NthRoot.thy
src/HOL/Hyperreal/NthRoot.thy
src/HOL/Hyperreal/Transcendental.thy
     1.1 --- a/src/HOL/Hyperreal/NthRoot.thy	Tue Apr 17 00:37:14 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/NthRoot.thy	Tue Apr 17 00:55:00 2007 +0200
     1.3 @@ -239,6 +239,80 @@
     1.4  apply (auto)
     1.5  done
     1.6  
     1.7 +lemma real_root_less_mono:
     1.8 +     "[| 0 \<le> x; x < y |] ==> root(Suc n) x < root(Suc n) y"
     1.9 +apply (frule order_le_less_trans, assumption)
    1.10 +apply (frule_tac n1 = n in real_root_pow_pos2 [THEN ssubst])
    1.11 +apply (rotate_tac 1, assumption)
    1.12 +apply (frule_tac n1 = n in real_root_pow_pos [THEN ssubst])
    1.13 +apply (rotate_tac 3, assumption)
    1.14 +apply (drule_tac y = "root (Suc n) y ^ Suc n" in order_less_imp_le)
    1.15 +apply (frule_tac n = n in real_root_pos_pos_le)
    1.16 +apply (frule_tac n = n in real_root_pos_pos)
    1.17 +apply (drule_tac x = "root (Suc n) x" and y = "root (Suc n) y" in realpow_increasing)
    1.18 +apply (assumption, assumption)
    1.19 +apply (drule_tac x = "root (Suc n) x" in order_le_imp_less_or_eq)
    1.20 +apply auto
    1.21 +apply (drule_tac f = "%x. x ^ (Suc n)" in arg_cong)
    1.22 +apply (auto simp add: real_root_pow_pos2 simp del: realpow_Suc)
    1.23 +done
    1.24 +
    1.25 +lemma real_root_le_mono:
    1.26 +     "[| 0 \<le> x; x \<le> y |] ==> root(Suc n) x \<le> root(Suc n) y"
    1.27 +apply (drule_tac y = y in order_le_imp_less_or_eq)
    1.28 +apply (auto dest: real_root_less_mono intro: order_less_imp_le)
    1.29 +done
    1.30 +
    1.31 +lemma real_root_less_iff [simp]:
    1.32 +     "[| 0 \<le> x; 0 \<le> y |] ==> (root(Suc n) x < root(Suc n) y) = (x < y)"
    1.33 +apply (auto intro: real_root_less_mono)
    1.34 +apply (rule ccontr, drule linorder_not_less [THEN iffD1])
    1.35 +apply (drule_tac x = y and n = n in real_root_le_mono, auto)
    1.36 +done
    1.37 +
    1.38 +lemma real_root_le_iff [simp]:
    1.39 +     "[| 0 \<le> x; 0 \<le> y |] ==> (root(Suc n) x \<le> root(Suc n) y) = (x \<le> y)"
    1.40 +apply (auto intro: real_root_le_mono)
    1.41 +apply (simp (no_asm) add: linorder_not_less [symmetric])
    1.42 +apply auto
    1.43 +apply (drule_tac x = y and n = n in real_root_less_mono, auto)
    1.44 +done
    1.45 +
    1.46 +lemma real_root_eq_iff [simp]:
    1.47 +     "[| 0 \<le> x; 0 \<le> y |] ==> (root(Suc n) x = root(Suc n) y) = (x = y)"
    1.48 +apply (auto intro!: order_antisym [where 'a = real])
    1.49 +apply (rule_tac n1 = n in real_root_le_iff [THEN iffD1])
    1.50 +apply (rule_tac [4] n1 = n in real_root_le_iff [THEN iffD1], auto)
    1.51 +done
    1.52 +
    1.53 +lemma real_root_pos_unique:
    1.54 +     "[| 0 \<le> x; 0 \<le> y; y ^ (Suc n) = x |] ==> root (Suc n) x = y"
    1.55 +by (auto dest: real_root_pos2 simp del: realpow_Suc)
    1.56 +
    1.57 +lemma real_root_mult:
    1.58 +     "[| 0 \<le> x; 0 \<le> y |] 
    1.59 +      ==> root(Suc n) (x * y) = root(Suc n) x * root(Suc n) y"
    1.60 +apply (rule real_root_pos_unique)
    1.61 +apply (auto intro!: real_root_pos_pos_le 
    1.62 +            simp add: power_mult_distrib zero_le_mult_iff real_root_pow_pos2 
    1.63 +            simp del: realpow_Suc)
    1.64 +done
    1.65 +
    1.66 +lemma real_root_inverse:
    1.67 +     "0 \<le> x ==> (root(Suc n) (inverse x) = inverse(root(Suc n) x))"
    1.68 +apply (rule real_root_pos_unique)
    1.69 +apply (auto intro: real_root_pos_pos_le 
    1.70 +            simp add: power_inverse [symmetric] real_root_pow_pos2 
    1.71 +            simp del: realpow_Suc)
    1.72 +done
    1.73 +
    1.74 +lemma real_root_divide: 
    1.75 +     "[| 0 \<le> x; 0 \<le> y |]  
    1.76 +      ==> (root(Suc n) (x / y) = root(Suc n) x / root(Suc n) y)"
    1.77 +apply (simp add: divide_inverse)
    1.78 +apply (auto simp add: real_root_mult real_root_inverse)
    1.79 +done
    1.80 +
    1.81  
    1.82  subsection{*Square Root*}
    1.83  
    1.84 @@ -407,4 +481,41 @@
    1.85    qed
    1.86  qed
    1.87  
    1.88 +
    1.89 +lemma real_sqrt_less_mono: "[| 0 \<le> x; x < y |] ==> sqrt(x) < sqrt(y)"
    1.90 +by (simp add: sqrt_def)
    1.91 +
    1.92 +lemma real_sqrt_le_mono: "[| 0 \<le> x; x \<le> y |] ==> sqrt(x) \<le> sqrt(y)"
    1.93 +by (simp add: sqrt_def)
    1.94 +
    1.95 +lemma real_sqrt_less_iff [simp]:
    1.96 +     "[| 0 \<le> x; 0 \<le> y |] ==> (sqrt(x) < sqrt(y)) = (x < y)"
    1.97 +by (simp add: sqrt_def)
    1.98 +
    1.99 +lemma real_sqrt_le_iff [simp]:
   1.100 +     "[| 0 \<le> x; 0 \<le> y |] ==> (sqrt(x) \<le> sqrt(y)) = (x \<le> y)"
   1.101 +by (simp add: sqrt_def)
   1.102 +
   1.103 +lemma real_sqrt_eq_iff [simp]:
   1.104 +     "[| 0 \<le> x; 0 \<le> y |] ==> (sqrt(x) = sqrt(y)) = (x = y)"
   1.105 +by (simp add: sqrt_def)
   1.106 +
   1.107 +lemma real_sqrt_sos_less_one_iff [simp]: "(sqrt(x\<twosuperior> + y\<twosuperior>) < 1) = (x\<twosuperior> + y\<twosuperior> < 1)"
   1.108 +apply (rule real_sqrt_one [THEN subst], safe)
   1.109 +apply (rule_tac [2] real_sqrt_less_mono)
   1.110 +apply (drule real_sqrt_less_iff [THEN [2] rev_iffD1], auto)
   1.111 +done
   1.112 +
   1.113 +lemma real_sqrt_sos_eq_one_iff [simp]: "(sqrt(x\<twosuperior> + y\<twosuperior>) = 1) = (x\<twosuperior> + y\<twosuperior> = 1)"
   1.114 +apply (rule real_sqrt_one [THEN subst], safe)
   1.115 +apply (drule real_sqrt_eq_iff [THEN [2] rev_iffD1], auto)
   1.116 +done
   1.117 +
   1.118 +lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r"
   1.119 +apply (simp add: divide_inverse)
   1.120 +apply (case_tac "r=0")
   1.121 +apply (auto simp add: mult_ac)
   1.122 +done
   1.123 +
   1.124 +
   1.125  end
     2.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Tue Apr 17 00:37:14 2007 +0200
     2.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Tue Apr 17 00:55:00 2007 +0200
     2.3 @@ -1911,116 +1911,6 @@
     2.4  by (cut_tac x = x in sin_cos_squared_add3, auto)
     2.5  
     2.6  
     2.7 -lemma real_root_less_mono:
     2.8 -     "[| 0 \<le> x; x < y |] ==> root(Suc n) x < root(Suc n) y"
     2.9 -apply (frule order_le_less_trans, assumption)
    2.10 -apply (frule_tac n1 = n in real_root_pow_pos2 [THEN ssubst])
    2.11 -apply (rotate_tac 1, assumption)
    2.12 -apply (frule_tac n1 = n in real_root_pow_pos [THEN ssubst])
    2.13 -apply (rotate_tac 3, assumption)
    2.14 -apply (drule_tac y = "root (Suc n) y ^ Suc n" in order_less_imp_le)
    2.15 -apply (frule_tac n = n in real_root_pos_pos_le)
    2.16 -apply (frule_tac n = n in real_root_pos_pos)
    2.17 -apply (drule_tac x = "root (Suc n) x" and y = "root (Suc n) y" in realpow_increasing)
    2.18 -apply (assumption, assumption)
    2.19 -apply (drule_tac x = "root (Suc n) x" in order_le_imp_less_or_eq)
    2.20 -apply auto
    2.21 -apply (drule_tac f = "%x. x ^ (Suc n)" in arg_cong)
    2.22 -apply (auto simp add: real_root_pow_pos2 simp del: realpow_Suc)
    2.23 -done
    2.24 -
    2.25 -lemma real_root_le_mono:
    2.26 -     "[| 0 \<le> x; x \<le> y |] ==> root(Suc n) x \<le> root(Suc n) y"
    2.27 -apply (drule_tac y = y in order_le_imp_less_or_eq)
    2.28 -apply (auto dest: real_root_less_mono intro: order_less_imp_le)
    2.29 -done
    2.30 -
    2.31 -lemma real_root_less_iff [simp]:
    2.32 -     "[| 0 \<le> x; 0 \<le> y |] ==> (root(Suc n) x < root(Suc n) y) = (x < y)"
    2.33 -apply (auto intro: real_root_less_mono)
    2.34 -apply (rule ccontr, drule linorder_not_less [THEN iffD1])
    2.35 -apply (drule_tac x = y and n = n in real_root_le_mono, auto)
    2.36 -done
    2.37 -
    2.38 -lemma real_root_le_iff [simp]:
    2.39 -     "[| 0 \<le> x; 0 \<le> y |] ==> (root(Suc n) x \<le> root(Suc n) y) = (x \<le> y)"
    2.40 -apply (auto intro: real_root_le_mono)
    2.41 -apply (simp (no_asm) add: linorder_not_less [symmetric])
    2.42 -apply auto
    2.43 -apply (drule_tac x = y and n = n in real_root_less_mono, auto)
    2.44 -done
    2.45 -
    2.46 -lemma real_root_eq_iff [simp]:
    2.47 -     "[| 0 \<le> x; 0 \<le> y |] ==> (root(Suc n) x = root(Suc n) y) = (x = y)"
    2.48 -apply (auto intro!: order_antisym [where 'a = real])
    2.49 -apply (rule_tac n1 = n in real_root_le_iff [THEN iffD1])
    2.50 -apply (rule_tac [4] n1 = n in real_root_le_iff [THEN iffD1], auto)
    2.51 -done
    2.52 -
    2.53 -lemma real_root_pos_unique:
    2.54 -     "[| 0 \<le> x; 0 \<le> y; y ^ (Suc n) = x |] ==> root (Suc n) x = y"
    2.55 -by (auto dest: real_root_pos2 simp del: realpow_Suc)
    2.56 -
    2.57 -lemma real_root_mult:
    2.58 -     "[| 0 \<le> x; 0 \<le> y |] 
    2.59 -      ==> root(Suc n) (x * y) = root(Suc n) x * root(Suc n) y"
    2.60 -apply (rule real_root_pos_unique)
    2.61 -apply (auto intro!: real_root_pos_pos_le 
    2.62 -            simp add: power_mult_distrib zero_le_mult_iff real_root_pow_pos2 
    2.63 -            simp del: realpow_Suc)
    2.64 -done
    2.65 -
    2.66 -lemma real_root_inverse:
    2.67 -     "0 \<le> x ==> (root(Suc n) (inverse x) = inverse(root(Suc n) x))"
    2.68 -apply (rule real_root_pos_unique)
    2.69 -apply (auto intro: real_root_pos_pos_le 
    2.70 -            simp add: power_inverse [symmetric] real_root_pow_pos2 
    2.71 -            simp del: realpow_Suc)
    2.72 -done
    2.73 -
    2.74 -lemma real_root_divide: 
    2.75 -     "[| 0 \<le> x; 0 \<le> y |]  
    2.76 -      ==> (root(Suc n) (x / y) = root(Suc n) x / root(Suc n) y)"
    2.77 -apply (simp add: divide_inverse)
    2.78 -apply (auto simp add: real_root_mult real_root_inverse)
    2.79 -done
    2.80 -
    2.81 -lemma real_sqrt_less_mono: "[| 0 \<le> x; x < y |] ==> sqrt(x) < sqrt(y)"
    2.82 -by (simp add: sqrt_def)
    2.83 -
    2.84 -lemma real_sqrt_le_mono: "[| 0 \<le> x; x \<le> y |] ==> sqrt(x) \<le> sqrt(y)"
    2.85 -by (simp add: sqrt_def)
    2.86 -
    2.87 -lemma real_sqrt_less_iff [simp]:
    2.88 -     "[| 0 \<le> x; 0 \<le> y |] ==> (sqrt(x) < sqrt(y)) = (x < y)"
    2.89 -by (simp add: sqrt_def)
    2.90 -
    2.91 -lemma real_sqrt_le_iff [simp]:
    2.92 -     "[| 0 \<le> x; 0 \<le> y |] ==> (sqrt(x) \<le> sqrt(y)) = (x \<le> y)"
    2.93 -by (simp add: sqrt_def)
    2.94 -
    2.95 -lemma real_sqrt_eq_iff [simp]:
    2.96 -     "[| 0 \<le> x; 0 \<le> y |] ==> (sqrt(x) = sqrt(y)) = (x = y)"
    2.97 -by (simp add: sqrt_def)
    2.98 -
    2.99 -lemma real_sqrt_sos_less_one_iff [simp]: "(sqrt(x\<twosuperior> + y\<twosuperior>) < 1) = (x\<twosuperior> + y\<twosuperior> < 1)"
   2.100 -apply (rule real_sqrt_one [THEN subst], safe)
   2.101 -apply (rule_tac [2] real_sqrt_less_mono)
   2.102 -apply (drule real_sqrt_less_iff [THEN [2] rev_iffD1], auto)
   2.103 -done
   2.104 -
   2.105 -lemma real_sqrt_sos_eq_one_iff [simp]: "(sqrt(x\<twosuperior> + y\<twosuperior>) = 1) = (x\<twosuperior> + y\<twosuperior> = 1)"
   2.106 -apply (rule real_sqrt_one [THEN subst], safe)
   2.107 -apply (drule real_sqrt_eq_iff [THEN [2] rev_iffD1], auto)
   2.108 -done
   2.109 -
   2.110 -lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r"
   2.111 -apply (simp add: divide_inverse)
   2.112 -apply (case_tac "r=0")
   2.113 -apply (auto simp add: mult_ac)
   2.114 -done
   2.115 -
   2.116 -
   2.117  subsection{*Theorems About Sqrt, Transcendental Functions for Complex*}
   2.118  
   2.119  lemma le_real_sqrt_sumsq [simp]: "x \<le> sqrt (x * x + y * y)"