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.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.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.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.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.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.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])