src/HOL/NthRoot.thy
changeset 53015 a1119cf551e8
parent 51483 dc39d69774bb
child 53076 47c9aff07725
     1.1 --- a/src/HOL/NthRoot.thy	Tue Aug 13 14:20:22 2013 +0200
     1.2 +++ b/src/HOL/NthRoot.thy	Tue Aug 13 16:25:47 2013 +0200
     1.3 @@ -349,19 +349,19 @@
     1.4  
     1.5  lemma pos2: "0 < (2::nat)" by simp
     1.6  
     1.7 -lemma real_sqrt_unique: "\<lbrakk>y\<twosuperior> = x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt x = y"
     1.8 +lemma real_sqrt_unique: "\<lbrakk>y\<^sup>2 = x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt x = y"
     1.9  unfolding sqrt_def by (rule real_root_pos_unique [OF pos2])
    1.10  
    1.11 -lemma real_sqrt_abs [simp]: "sqrt (x\<twosuperior>) = \<bar>x\<bar>"
    1.12 +lemma real_sqrt_abs [simp]: "sqrt (x\<^sup>2) = \<bar>x\<bar>"
    1.13  apply (rule real_sqrt_unique)
    1.14  apply (rule power2_abs)
    1.15  apply (rule abs_ge_zero)
    1.16  done
    1.17  
    1.18 -lemma real_sqrt_pow2 [simp]: "0 \<le> x \<Longrightarrow> (sqrt x)\<twosuperior> = x"
    1.19 +lemma real_sqrt_pow2 [simp]: "0 \<le> x \<Longrightarrow> (sqrt x)\<^sup>2 = x"
    1.20  unfolding sqrt_def by (rule real_root_pow_pos2 [OF pos2])
    1.21  
    1.22 -lemma real_sqrt_pow2_iff [simp]: "((sqrt x)\<twosuperior> = x) = (0 \<le> x)"
    1.23 +lemma real_sqrt_pow2_iff [simp]: "((sqrt x)\<^sup>2 = x) = (0 \<le> x)"
    1.24  apply (rule iffI)
    1.25  apply (erule subst)
    1.26  apply (rule zero_le_power2)
    1.27 @@ -501,47 +501,47 @@
    1.28  
    1.29  lemma four_x_squared: 
    1.30    fixes x::real
    1.31 -  shows "4 * x\<twosuperior> = (2 * x)\<twosuperior>"
    1.32 +  shows "4 * x\<^sup>2 = (2 * x)\<^sup>2"
    1.33  by (simp add: power2_eq_square)
    1.34  
    1.35  subsection {* Square Root of Sum of Squares *}
    1.36  
    1.37 -lemma real_sqrt_sum_squares_ge_zero: "0 \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
    1.38 +lemma real_sqrt_sum_squares_ge_zero: "0 \<le> sqrt (x\<^sup>2 + y\<^sup>2)"
    1.39    by simp (* TODO: delete *)
    1.40  
    1.41  declare real_sqrt_sum_squares_ge_zero [THEN abs_of_nonneg, simp]
    1.42  
    1.43  lemma real_sqrt_sum_squares_mult_ge_zero [simp]:
    1.44 -     "0 \<le> sqrt ((x\<twosuperior> + y\<twosuperior>)*(xa\<twosuperior> + ya\<twosuperior>))"
    1.45 +     "0 \<le> sqrt ((x\<^sup>2 + y\<^sup>2)*(xa\<^sup>2 + ya\<^sup>2))"
    1.46    by (simp add: zero_le_mult_iff)
    1.47  
    1.48  lemma real_sqrt_sum_squares_mult_squared_eq [simp]:
    1.49 -     "sqrt ((x\<twosuperior> + y\<twosuperior>) * (xa\<twosuperior> + ya\<twosuperior>)) ^ 2 = (x\<twosuperior> + y\<twosuperior>) * (xa\<twosuperior> + ya\<twosuperior>)"
    1.50 +     "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)"
    1.51    by (simp add: zero_le_mult_iff)
    1.52  
    1.53 -lemma real_sqrt_sum_squares_eq_cancel: "sqrt (x\<twosuperior> + y\<twosuperior>) = x \<Longrightarrow> y = 0"
    1.54 -by (drule_tac f = "%x. x\<twosuperior>" in arg_cong, simp)
    1.55 +lemma real_sqrt_sum_squares_eq_cancel: "sqrt (x\<^sup>2 + y\<^sup>2) = x \<Longrightarrow> y = 0"
    1.56 +by (drule_tac f = "%x. x\<^sup>2" in arg_cong, simp)
    1.57  
    1.58 -lemma real_sqrt_sum_squares_eq_cancel2: "sqrt (x\<twosuperior> + y\<twosuperior>) = y \<Longrightarrow> x = 0"
    1.59 -by (drule_tac f = "%x. x\<twosuperior>" in arg_cong, simp)
    1.60 +lemma real_sqrt_sum_squares_eq_cancel2: "sqrt (x\<^sup>2 + y\<^sup>2) = y \<Longrightarrow> x = 0"
    1.61 +by (drule_tac f = "%x. x\<^sup>2" in arg_cong, simp)
    1.62  
    1.63 -lemma real_sqrt_sum_squares_ge1 [simp]: "x \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
    1.64 +lemma real_sqrt_sum_squares_ge1 [simp]: "x \<le> sqrt (x\<^sup>2 + y\<^sup>2)"
    1.65  by (rule power2_le_imp_le, simp_all)
    1.66  
    1.67 -lemma real_sqrt_sum_squares_ge2 [simp]: "y \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
    1.68 +lemma real_sqrt_sum_squares_ge2 [simp]: "y \<le> sqrt (x\<^sup>2 + y\<^sup>2)"
    1.69  by (rule power2_le_imp_le, simp_all)
    1.70  
    1.71 -lemma real_sqrt_ge_abs1 [simp]: "\<bar>x\<bar> \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
    1.72 +lemma real_sqrt_ge_abs1 [simp]: "\<bar>x\<bar> \<le> sqrt (x\<^sup>2 + y\<^sup>2)"
    1.73  by (rule power2_le_imp_le, simp_all)
    1.74  
    1.75 -lemma real_sqrt_ge_abs2 [simp]: "\<bar>y\<bar> \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
    1.76 +lemma real_sqrt_ge_abs2 [simp]: "\<bar>y\<bar> \<le> sqrt (x\<^sup>2 + y\<^sup>2)"
    1.77  by (rule power2_le_imp_le, simp_all)
    1.78  
    1.79  lemma le_real_sqrt_sumsq [simp]: "x \<le> sqrt (x * x + y * y)"
    1.80  by (simp add: power2_eq_square [symmetric])
    1.81  
    1.82  lemma real_sqrt_sum_squares_triangle_ineq:
    1.83 -  "sqrt ((a + c)\<twosuperior> + (b + d)\<twosuperior>) \<le> sqrt (a\<twosuperior> + b\<twosuperior>) + sqrt (c\<twosuperior> + d\<twosuperior>)"
    1.84 +  "sqrt ((a + c)\<^sup>2 + (b + d)\<^sup>2) \<le> sqrt (a\<^sup>2 + b\<^sup>2) + sqrt (c\<^sup>2 + d\<^sup>2)"
    1.85  apply (rule power2_le_imp_le, simp)
    1.86  apply (simp add: power2_sum)
    1.87  apply (simp only: mult_assoc distrib_left [symmetric])
    1.88 @@ -549,8 +549,8 @@
    1.89  apply (rule power2_le_imp_le)
    1.90  apply (simp add: power2_sum power_mult_distrib)
    1.91  apply (simp add: ring_distribs)
    1.92 -apply (subgoal_tac "0 \<le> b\<twosuperior> * c\<twosuperior> + a\<twosuperior> * d\<twosuperior> - 2 * (a * c) * (b * d)", simp)
    1.93 -apply (rule_tac b="(a * d - b * c)\<twosuperior>" in ord_le_eq_trans)
    1.94 +apply (subgoal_tac "0 \<le> b\<^sup>2 * c\<^sup>2 + a\<^sup>2 * d\<^sup>2 - 2 * (a * c) * (b * d)", simp)
    1.95 +apply (rule_tac b="(a * d - b * c)\<^sup>2" in ord_le_eq_trans)
    1.96  apply (rule zero_le_power2)
    1.97  apply (simp add: power2_diff power_mult_distrib)
    1.98  apply (simp add: mult_nonneg_nonneg)
    1.99 @@ -559,7 +559,7 @@
   1.100  done
   1.101  
   1.102  lemma real_sqrt_sum_squares_less:
   1.103 -  "\<lbrakk>\<bar>x\<bar> < u / sqrt 2; \<bar>y\<bar> < u / sqrt 2\<rbrakk> \<Longrightarrow> sqrt (x\<twosuperior> + y\<twosuperior>) < u"
   1.104 +  "\<lbrakk>\<bar>x\<bar> < u / sqrt 2; \<bar>y\<bar> < u / sqrt 2\<rbrakk> \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) < u"
   1.105  apply (rule power2_less_imp_less, simp)
   1.106  apply (drule power_strict_mono [OF _ abs_ge_zero pos2])
   1.107  apply (drule power_strict_mono [OF _ abs_ge_zero pos2])
   1.108 @@ -571,12 +571,12 @@
   1.109  text{*Needed for the infinitely close relation over the nonstandard
   1.110      complex numbers*}
   1.111  lemma lemma_sqrt_hcomplex_capprox:
   1.112 -     "[| 0 < u; x < u/2; y < u/2; 0 \<le> x; 0 \<le> y |] ==> sqrt (x\<twosuperior> + y\<twosuperior>) < u"
   1.113 +     "[| 0 < u; x < u/2; y < u/2; 0 \<le> x; 0 \<le> y |] ==> sqrt (x\<^sup>2 + y\<^sup>2) < u"
   1.114  apply (rule_tac y = "u/sqrt 2" in order_le_less_trans)
   1.115  apply (erule_tac [2] lemma_real_divide_sqrt_less)
   1.116  apply (rule power2_le_imp_le)
   1.117  apply (auto simp add: zero_le_divide_iff power_divide)
   1.118 -apply (rule_tac t = "u\<twosuperior>" in real_sum_of_halves [THEN subst])
   1.119 +apply (rule_tac t = "u\<^sup>2" in real_sum_of_halves [THEN subst])
   1.120  apply (rule add_mono)
   1.121  apply (auto simp add: four_x_squared intro: power_mono)
   1.122  done