author wenzelm Sun Aug 18 19:59:19 2013 +0200 (2013-08-18) changeset 53077 a1b3784f8129 parent 53076 47c9aff07725 child 53078 cc06f17d8057
more symbols;
```     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Sun Aug 18 18:49:45 2013 +0200
1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Aug 18 19:59:19 2013 +0200
1.3 @@ -234,10 +234,10 @@
1.4    assumes "sqrt x < b" and "0 < b" and "0 < x"
1.5    shows "sqrt x < (b + x / b)/2"
1.6  proof -
1.7 -  from assms have "0 < (b - sqrt x) ^ 2 " by simp
1.8 -  also have "\<dots> = b ^ 2 - 2 * b * sqrt x + (sqrt x) ^ 2" by algebra
1.9 -  also have "\<dots> = b ^ 2 - 2 * b * sqrt x + x" using assms by simp
1.10 -  finally have "0 < b ^ 2 - 2 * b * sqrt x + x" by assumption
1.11 +  from assms have "0 < (b - sqrt x)\<^sup>2 " by simp
1.12 +  also have "\<dots> = b\<^sup>2 - 2 * b * sqrt x + (sqrt x)\<^sup>2" by algebra
1.13 +  also have "\<dots> = b\<^sup>2 - 2 * b * sqrt x + x" using assms by simp
1.14 +  finally have "0 < b\<^sup>2 - 2 * b * sqrt x + x" .
1.15    hence "0 < b / 2 - sqrt x + x / (2 * b)" using assms
1.16      by (simp add: field_simps power2_eq_square)
1.17    thus ?thesis by (simp add: field_simps)
```
```     2.1 --- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Sun Aug 18 18:49:45 2013 +0200
2.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Sun Aug 18 19:59:19 2013 +0200
2.3 @@ -287,7 +287,7 @@
2.4              by (simp only: numerals even_nat_div_two_times_two [OF `even w`])
2.5            have "Ipol ls P * Ipol ls P = Ipol ls P ^ Suc (Suc 0)"
2.6              by simp
2.7 -          then have "Ipol ls P * Ipol ls P = Ipol ls P ^ 2"
2.8 +          then have "Ipol ls P * Ipol ls P = (Ipol ls P)\<^sup>2"
2.10            with Suc show ?thesis
2.11              by (auto simp add: power_mult [symmetric, of _ 2 _] two_times mul_ci sqr_ci
```
```     3.1 --- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Sun Aug 18 18:49:45 2013 +0200
3.2 +++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Sun Aug 18 19:59:19 2013 +0200
3.3 @@ -72,7 +72,7 @@
3.4    shows "g / v * tan (35 * d) \<in> { 3 * d .. 3.1 * d }"
3.5    using assms by (approximation 20)
3.6
3.7 -lemma "x \<in> { 0 .. 1 :: real } \<longrightarrow> x ^ 2 \<le> x"
3.8 +lemma "x \<in> { 0 .. 1 :: real } \<longrightarrow> x\<^sup>2 \<le> x"
3.9    by (approximation 30 splitting: x=1 taylor: x = 3)
3.10
3.11  value [approximate] "10"
```
```     4.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Sun Aug 18 18:49:45 2013 +0200
4.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Sun Aug 18 19:59:19 2013 +0200
4.3 @@ -1173,22 +1173,22 @@
4.4  lemma fps_inverse_deriv:
4.5    fixes a:: "('a :: field) fps"
4.6    assumes a0: "a\$0 \<noteq> 0"
4.7 -  shows "fps_deriv (inverse a) = - fps_deriv a * inverse a ^ 2"
4.8 +  shows "fps_deriv (inverse a) = - fps_deriv a * (inverse a)\<^sup>2"
4.9  proof-
4.10    from inverse_mult_eq_1[OF a0]
4.11    have "fps_deriv (inverse a * a) = 0" by simp
4.12    hence "inverse a * fps_deriv a + fps_deriv (inverse a) * a = 0" by simp
4.13    hence "inverse a * (inverse a * fps_deriv a + fps_deriv (inverse a) * a) = 0"  by simp
4.14    with inverse_mult_eq_1[OF a0]
4.15 -  have "inverse a ^ 2 * fps_deriv a + fps_deriv (inverse a) = 0"
4.16 +  have "(inverse a)\<^sup>2 * fps_deriv a + fps_deriv (inverse a) = 0"
4.17      unfolding power2_eq_square
4.20      done
4.21 -  then have "inverse a ^ 2 * fps_deriv a + fps_deriv (inverse a) - fps_deriv a * inverse a ^ 2 =
4.22 -      0 - fps_deriv a * inverse a ^ 2"
4.23 +  then have "(inverse a)\<^sup>2 * fps_deriv a + fps_deriv (inverse a) - fps_deriv a * (inverse a)\<^sup>2 =
4.24 +      0 - fps_deriv a * (inverse a)\<^sup>2"
4.25      by simp
4.26 -  then show "fps_deriv (inverse a) = - fps_deriv a * inverse a ^ 2"
4.27 +  then show "fps_deriv (inverse a) = - fps_deriv a * (inverse a)\<^sup>2"
4.29  qed
4.30
4.31 @@ -1223,7 +1223,7 @@
4.32  lemma fps_inverse_deriv':
4.33    fixes a:: "('a :: field) fps"
4.34    assumes a0: "a\$0 \<noteq> 0"
4.35 -  shows "fps_deriv (inverse a) = - fps_deriv a / a ^ 2"
4.36 +  shows "fps_deriv (inverse a) = - fps_deriv a / a\<^sup>2"
4.37    using fps_inverse_deriv[OF a0]
4.38    unfolding power2_eq_square fps_divide_def fps_inverse_mult
4.39    by simp
4.40 @@ -1236,7 +1236,7 @@
4.41  lemma fps_divide_deriv:
4.42    fixes a:: "('a :: field) fps"
4.43    assumes a0: "b\$0 \<noteq> 0"
4.44 -  shows "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b ^ 2"
4.45 +  shows "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b\<^sup>2"
4.46    using fps_inverse_deriv[OF a0]
4.47    by (simp add: fps_divide_def field_simps
4.48      power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0])
4.49 @@ -3210,7 +3210,7 @@
4.50    apply (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric] of_nat_add[symmetric])
4.51    by simp
4.52
4.53 -lemma binomial_Vandermonde_same: "setsum (\<lambda>k. (n choose k)^2) {0..n} = (2*n) choose n"
4.54 +lemma binomial_Vandermonde_same: "setsum (\<lambda>k. (n choose k)\<^sup>2) {0..n} = (2*n) choose n"
4.55    using binomial_Vandermonde[of n n n,symmetric]
4.56    unfolding mult_2 apply (simp add: power2_eq_square)
4.57    apply (rule setsum_cong2)
4.58 @@ -3425,8 +3425,8 @@
4.59  qed
4.60
4.61  lemma fps_sin_cos_sum_of_squares:
4.62 -  "fps_cos c ^ 2 + fps_sin c ^ 2 = 1" (is "?lhs = 1")
4.63 -proof-
4.64 +  "(fps_cos c)\<^sup>2 + (fps_sin c)\<^sup>2 = 1" (is "?lhs = 1")
4.65 +proof -
4.66    have "fps_deriv ?lhs = 0"
4.67      apply (simp add:  fps_deriv_power fps_sin_deriv fps_cos_deriv)
4.68      apply (simp add: field_simps fps_const_neg[symmetric] del: fps_const_neg)
4.69 @@ -3546,7 +3546,7 @@
4.70
4.71  definition "fps_tan c = fps_sin c / fps_cos c"
4.72
4.73 -lemma fps_tan_deriv: "fps_deriv(fps_tan c) = fps_const c/ (fps_cos c ^ 2)"
4.74 +lemma fps_tan_deriv: "fps_deriv (fps_tan c) = fps_const c / (fps_cos c)\<^sup>2"
4.75  proof -
4.76    have th0: "fps_cos c \$ 0 \<noteq> 0" by (simp add: fps_cos_def)
4.77    show ?thesis
```
```     5.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sun Aug 18 18:49:45 2013 +0200
5.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sun Aug 18 19:59:19 2013 +0200
5.3 @@ -14,7 +14,7 @@
5.4             else Complex (sqrt((cmod z + Re z) /2))
5.5                          ((Im z / abs(Im z)) * sqrt((cmod z - Re z) /2)))"
5.6
5.7 -lemma csqrt[algebra]: "csqrt z ^ 2 = z"
5.8 +lemma csqrt[algebra]: "(csqrt z)\<^sup>2 = z"
5.9  proof-
5.10    obtain x y where xy: "z = Complex x y" by (cases z)
5.11    {assume y0: "y = 0"
5.12 @@ -34,13 +34,15 @@
5.13        hence "cmod ?z - x \<ge> 0" "cmod ?z + x \<ge> 0" by arith+
5.14        hence "(sqrt (x * x + y * y) + x) / 2 \<ge> 0" "(sqrt (x * x + y * y) - x) / 2 \<ge> 0" by (simp_all add: power2_eq_square) }
5.15      note th = this
5.16 -    have sq4: "\<And>x::real. x^2 / 4 = (x / 2) ^ 2"
5.17 +    have sq4: "\<And>x::real. x\<^sup>2 / 4 = (x / 2)\<^sup>2"
5.19      from th[of x y]
5.20 -    have sq4': "sqrt (((sqrt (x * x + y * y) + x)^2 / 4)) = (sqrt (x * x + y * y) + x) / 2" "sqrt (((sqrt (x * x + y * y) - x)^2 / 4)) = (sqrt (x * x + y * y) - x) / 2" unfolding sq4 by simp_all
5.21 +    have sq4': "sqrt (((sqrt (x * x + y * y) + x)\<^sup>2 / 4)) = (sqrt (x * x + y * y) + x) / 2"
5.22 +      "sqrt (((sqrt (x * x + y * y) - x)\<^sup>2 / 4)) = (sqrt (x * x + y * y) - x) / 2"
5.23 +      unfolding sq4 by simp_all
5.24      then have th1: "sqrt ((sqrt (x * x + y * y) + x) * (sqrt (x * x + y * y) + x) / 4) - sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) - x) / 4) = x"
5.25        unfolding power2_eq_square by simp
5.26 -    have "sqrt 4 = sqrt (2^2)" by simp
5.27 +    have "sqrt 4 = sqrt (2\<^sup>2)" by simp
5.28      hence sqrt4: "sqrt 4 = 2" by (simp only: real_sqrt_abs)
5.29      have th2: "2 *(y * sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) + x) / 4)) / \<bar>y\<bar> = y"
5.30        using iffD2[OF real_sqrt_pow2_iff sum_power2_ge_zero[of x y]] y0
5.31 @@ -184,14 +186,14 @@
5.32    shows "cmod (z + 1) < 1 \<or> cmod (z - 1) < 1 \<or> cmod (z + ii) < 1 \<or> cmod (z - ii) < 1"
5.33  proof-
5.34    obtain x y where z: "z = Complex x y " by (cases z, auto)
5.35 -  from md z have xy: "x^2 + y^2 = 1" by (simp add: cmod_def)
5.36 +  from md z have xy: "x\<^sup>2 + y\<^sup>2 = 1" by (simp add: cmod_def)
5.37    {assume C: "cmod (z + 1) \<ge> 1" "cmod (z - 1) \<ge> 1" "cmod (z + ii) \<ge> 1" "cmod (z - ii) \<ge> 1"
5.38      from C z xy have "2*x \<le> 1" "2*x \<ge> -1" "2*y \<le> 1" "2*y \<ge> -1"
5.39        by (simp_all add: cmod_def power2_eq_square algebra_simps)
5.40      hence "abs (2*x) \<le> 1" "abs (2*y) \<le> 1" by simp_all
5.41 -    hence "(abs (2 * x))^2 <= 1^2" "(abs (2 * y)) ^2 <= 1^2"
5.42 +    hence "(abs (2 * x))\<^sup>2 <= 1\<^sup>2" "(abs (2 * y))\<^sup>2 <= 1\<^sup>2"
5.43        by - (rule power_mono, simp, simp)+
5.44 -    hence th0: "4*x^2 \<le> 1" "4*y^2 \<le> 1"
5.45 +    hence th0: "4*x\<^sup>2 \<le> 1" "4*y\<^sup>2 \<le> 1"
5.47      from add_mono[OF th0] xy have False by simp }
5.48    thus ?thesis unfolding linorder_not_le[symmetric] by blast
5.49 @@ -454,7 +456,7 @@
5.50    ultimately show ?thesis by blast
5.51  qed
5.52
5.53 -lemma "(rcis (sqrt (abs r)) (a/2)) ^ 2 = rcis (abs r) a"
5.54 +lemma "(rcis (sqrt (abs r)) (a/2))\<^sup>2 = rcis (abs r) a"
5.55    unfolding power2_eq_square
5.58 @@ -464,7 +466,7 @@
5.59    unfolding cis_def
5.60    by simp
5.61
5.62 -lemma "(rcis (sqrt (abs r)) ((pi + a)/2)) ^ 2 = rcis (- abs r) a"
5.63 +lemma "(rcis (sqrt (abs r)) ((pi + a)/2))\<^sup>2 = rcis (- abs r) a"
5.64    unfolding power2_eq_square
5.66    apply (simp add: power2_eq_square[symmetric] rcis_def cispi cis_mult[symmetric])
```
```     6.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Aug 18 18:49:45 2013 +0200
6.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Aug 18 19:59:19 2013 +0200
6.3 @@ -3361,7 +3361,7 @@
6.4        thus False using y[THEN bspec[where x="y + u *\<^sub>R (x - y)"]]
6.5          using assms(1)[unfolded convex_alt, THEN bspec[where x=y]]
6.6          using `x\<in>s` `y\<in>s` by (auto simp add: dist_commute algebra_simps) qed
6.7 -    moreover have "0 < norm (y - z) ^ 2" using `y\<in>s` `z\<notin>s` by auto
6.8 +    moreover have "0 < (norm (y - z))\<^sup>2" using `y\<in>s` `z\<notin>s` by auto
6.9      hence "0 < inner (y - z) (y - z)" unfolding power2_norm_eq_inner by simp
6.10      ultimately show "inner (y - z) z + (norm (y - z))\<^sup>2 / 2 < inner (y - z) x"
6.11        unfolding power2_norm_eq_inner and not_less by (auto simp add: field_simps inner_commute inner_diff)
```
```     7.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Aug 18 18:49:45 2013 +0200
7.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Aug 18 19:59:19 2013 +0200
7.3 @@ -629,7 +629,7 @@
7.4    then guess x .. note x=this
7.5    show ?thesis proof(cases "f a = f b")
7.6      case False
7.7 -    have "norm (f b - f a) * norm (f b - f a) = norm (f b - f a)^2"
7.8 +    have "norm (f b - f a) * norm (f b - f a) = (norm (f b - f a))\<^sup>2"
7.10      also have "\<dots> = (f b - f a) \<bullet> (f b - f a)" unfolding power2_norm_eq_inner ..
7.11      also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)"
```
```     8.1 --- a/src/HOL/Multivariate_Analysis/Determinants.thy	Sun Aug 18 18:49:45 2013 +0200
8.2 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Sun Aug 18 19:59:19 2013 +0200
8.3 @@ -917,7 +917,7 @@
8.4    {fix v w
8.5      {fix x note fd[rule_format, of x 0, unfolded dist_norm f0 diff_0_right] }
8.6      note th0 = this
8.7 -    have "f v \<bullet> f w = c^2 * (v \<bullet> w)"
8.8 +    have "f v \<bullet> f w = c\<^sup>2 * (v \<bullet> w)"
8.9        unfolding dot_norm_neg dist_norm[symmetric]
8.10        unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)}
8.11    note fc = this
```
```     9.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sun Aug 18 18:49:45 2013 +0200
9.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sun Aug 18 19:59:19 2013 +0200
9.3 @@ -17,7 +17,7 @@
9.4
9.5  lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)"
9.6  proof -
9.7 -  have "(x + 1/2)^2 + 3/4 > 0" using zero_le_power2[of "x+1/2"] by arith
9.8 +  have "(x + 1/2)\<^sup>2 + 3/4 > 0" using zero_le_power2[of "x+1/2"] by arith
9.9    then show ?thesis by (simp add: field_simps power2_eq_square)
9.10  qed
9.11
9.12 @@ -30,21 +30,21 @@
9.13    apply auto
9.14    done
9.15
9.16 -lemma real_le_lsqrt: "0 <= x \<Longrightarrow> 0 <= y \<Longrightarrow> x <= y^2 ==> sqrt x <= y"
9.17 -  using real_sqrt_le_iff[of x "y^2"] by simp
9.18 -
9.19 -lemma real_le_rsqrt: "x^2 \<le> y \<Longrightarrow> x \<le> sqrt y"
9.20 -  using real_sqrt_le_mono[of "x^2" y] by simp
9.21 -
9.22 -lemma real_less_rsqrt: "x^2 < y \<Longrightarrow> x < sqrt y"
9.23 -  using real_sqrt_less_mono[of "x^2" y] by simp
9.24 +lemma real_le_lsqrt: "0 <= x \<Longrightarrow> 0 <= y \<Longrightarrow> x <= y\<^sup>2 ==> sqrt x <= y"
9.25 +  using real_sqrt_le_iff[of x "y\<^sup>2"] by simp
9.26 +
9.27 +lemma real_le_rsqrt: "x\<^sup>2 \<le> y \<Longrightarrow> x \<le> sqrt y"
9.28 +  using real_sqrt_le_mono[of "x\<^sup>2" y] by simp
9.29 +
9.30 +lemma real_less_rsqrt: "x\<^sup>2 < y \<Longrightarrow> x < sqrt y"
9.31 +  using real_sqrt_less_mono[of "x\<^sup>2" y] by simp
9.32
9.33  lemma sqrt_even_pow2:
9.34    assumes n: "even n"
9.35    shows "sqrt(2 ^ n) = 2 ^ (n div 2)"
9.36  proof -
9.37    from n obtain m where m: "n = 2*m" unfolding even_mult_two_ex ..
9.38 -  from m  have "sqrt(2 ^ n) = sqrt ((2 ^ m) ^ 2)"
9.39 +  from m  have "sqrt(2 ^ n) = sqrt ((2 ^ m)\<^sup>2)"
9.40      by (simp only: power_mult[symmetric] mult_commute)
9.41    then show ?thesis  using m by simp
9.42  qed
9.43 @@ -85,13 +85,13 @@
9.44
9.45  text{* Squaring equations and inequalities involving norms.  *}
9.46
9.47 -lemma dot_square_norm: "x \<bullet> x = norm(x)^2"
9.48 +lemma dot_square_norm: "x \<bullet> x = (norm x)\<^sup>2"
9.49    by (simp only: power2_norm_eq_inner) (* TODO: move? *)
9.50
9.51 -lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a^2"
9.52 +lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a\<^sup>2"
9.53    by (auto simp add: norm_eq_sqrt_inner)
9.54
9.55 -lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)^2 \<le> y^2"
9.56 +lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)\<^sup>2 \<le> y\<^sup>2"
9.57  proof
9.58    assume "\<bar>x\<bar> \<le> \<bar>y\<bar>"
9.59    then have "\<bar>x\<bar>\<^sup>2 \<le> \<bar>y\<bar>\<^sup>2" by (rule power_mono, simp)
9.60 @@ -102,21 +102,21 @@
9.61    then show "\<bar>x\<bar> \<le> \<bar>y\<bar>" by simp
9.62  qed
9.63
9.64 -lemma norm_le_square: "norm(x) <= a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x <= a^2"
9.65 +lemma norm_le_square: "norm(x) <= a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x <= a\<^sup>2"
9.66    apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
9.67    using norm_ge_zero[of x]
9.68    apply arith
9.69    done
9.70
9.71 -lemma norm_ge_square: "norm(x) >= a \<longleftrightarrow> a <= 0 \<or> x \<bullet> x >= a ^ 2"
9.72 +lemma norm_ge_square: "norm(x) >= a \<longleftrightarrow> a <= 0 \<or> x \<bullet> x >= a\<^sup>2"
9.73    apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
9.74    using norm_ge_zero[of x]
9.75    apply arith
9.76    done
9.77
9.78 -lemma norm_lt_square: "norm(x) < a \<longleftrightarrow> 0 < a \<and> x \<bullet> x < a^2"
9.79 +lemma norm_lt_square: "norm(x) < a \<longleftrightarrow> 0 < a \<and> x \<bullet> x < a\<^sup>2"
9.80    by (metis not_le norm_ge_square)
9.81 -lemma norm_gt_square: "norm(x) > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a^2"
9.82 +lemma norm_gt_square: "norm(x) > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a\<^sup>2"
9.83    by (metis norm_le_square not_less)
9.84
9.85  text{* Dot product in terms of the norm rather than conversely. *}
9.86 @@ -124,10 +124,10 @@
9.88    inner_scaleR_left inner_scaleR_right
9.89
9.90 -lemma dot_norm: "x \<bullet> y = (norm(x + y) ^2 - norm x ^ 2 - norm y ^ 2) / 2"
9.91 +lemma dot_norm: "x \<bullet> y = ((norm (x + y))\<^sup>2 - (norm x)\<^sup>2 - (norm y)\<^sup>2) / 2"
9.92    unfolding power2_norm_eq_inner inner_simps inner_commute by auto
9.93
9.94 -lemma dot_norm_neg: "x \<bullet> y = ((norm x ^ 2 + norm y ^ 2) - norm(x - y) ^ 2) / 2"
9.95 +lemma dot_norm_neg: "x \<bullet> y = (((norm x)\<^sup>2 + (norm y)\<^sup>2) - (norm (x - y))\<^sup>2) / 2"
9.96    unfolding power2_norm_eq_inner inner_simps inner_commute
9.97    by (auto simp add: algebra_simps)
9.98
9.99 @@ -469,11 +469,11 @@
9.100
9.101
9.102  lemma triangle_lemma:
9.103 -  assumes x: "0 <= (x::real)" and y:"0 <= y" and z: "0 <= z" and xy: "x^2 <= y^2 + z^2"
9.104 +  assumes x: "0 <= (x::real)" and y:"0 <= y" and z: "0 <= z" and xy: "x\<^sup>2 <= y\<^sup>2 + z\<^sup>2"
9.105    shows "x <= y + z"
9.106  proof -
9.107 -  have "y^2 + z^2 \<le> y^2 + 2*y*z + z^2" using z y by (simp add: mult_nonneg_nonneg)
9.108 -  with xy have th: "x ^2 \<le> (y+z)^2" by (simp add: power2_eq_square field_simps)
9.109 +  have "y\<^sup>2 + z\<^sup>2 \<le> y\<^sup>2 + 2*y*z + z\<^sup>2" using z y by (simp add: mult_nonneg_nonneg)
9.110 +  with xy have th: "x\<^sup>2 \<le> (y+z)\<^sup>2" by (simp add: power2_eq_square field_simps)
9.111    from y z have yz: "y + z \<ge> 0" by arith
9.112    from power2_le_imp_le[OF th yz] show ?thesis .
9.113  qed
9.114 @@ -2592,11 +2592,11 @@
9.115  proof -
9.116    let ?d = "DIM('a)"
9.117    have "real ?d \<ge> 0" by simp
9.118 -  then have d2: "(sqrt (real ?d))^2 = real ?d"
9.119 +  then have d2: "(sqrt (real ?d))\<^sup>2 = real ?d"
9.120      by (auto intro: real_sqrt_pow2)
9.121    have th: "sqrt (real ?d) * infnorm x \<ge> 0"
9.122      by (simp add: zero_le_mult_iff infnorm_pos_le)
9.123 -  have th1: "x \<bullet> x \<le> (sqrt (real ?d) * infnorm x)^2"
9.124 +  have th1: "x \<bullet> x \<le> (sqrt (real ?d) * infnorm x)\<^sup>2"
9.125      unfolding power_mult_distrib d2
9.126      unfolding real_of_nat_def
9.127      apply(subst euclidean_inner)
9.128 @@ -2680,9 +2680,9 @@
9.129        by simp_all
9.130      then have n: "norm x > 0" "norm y > 0"
9.131        using norm_ge_zero[of x] norm_ge_zero[of y] by arith+
9.132 -    have th: "\<And>(a::real) b c. a + b + c \<noteq> 0 ==> (a = b + c \<longleftrightarrow> a^2 = (b + c)^2)"
9.133 +    have th: "\<And>(a::real) b c. a + b + c \<noteq> 0 ==> (a = b + c \<longleftrightarrow> a\<^sup>2 = (b + c)\<^sup>2)"
9.134        by algebra
9.135 -    have "norm(x + y) = norm x + norm y \<longleftrightarrow> norm(x + y)^ 2 = (norm x + norm y) ^2"
9.136 +    have "norm (x + y) = norm x + norm y \<longleftrightarrow> (norm (x + y))\<^sup>2 = (norm x + norm y)\<^sup>2"
9.137        apply (rule th) using n norm_ge_zero[of "x + y"]
9.138        apply arith
9.139        done
```
```    10.1 --- a/src/HOL/NSA/CLim.thy	Sun Aug 18 18:49:45 2013 +0200
10.2 +++ b/src/HOL/NSA/CLim.thy	Sun Aug 18 19:59:19 2013 +0200
10.3 @@ -15,7 +15,7 @@
10.4
10.5  (*??generalize*)
10.6  lemma lemma_complex_mult_inverse_squared [simp]:
10.7 -     "x \<noteq> (0::complex) \<Longrightarrow> (x * inverse(x) ^ 2) = inverse x"
10.8 +     "x \<noteq> (0::complex) \<Longrightarrow> x * (inverse x)\<^sup>2 = inverse x"
10.10
10.11  text{*Changing the quantified variable. Install earlier?*}
10.12 @@ -152,12 +152,12 @@
10.13
10.14  text{*Can't relax the premise @{term "x \<noteq> 0"}: it isn't continuous at zero*}
10.15  lemma NSCDERIV_inverse:
10.16 -     "(x::complex) \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))"
10.17 +     "(x::complex) \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- ((inverse x)\<^sup>2))"
10.18  unfolding numeral_2_eq_2
10.19  by (rule NSDERIV_inverse)
10.20
10.21  lemma CDERIV_inverse:
10.22 -     "(x::complex) \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))"
10.23 +     "(x::complex) \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (- ((inverse x)\<^sup>2))"
10.24  unfolding numeral_2_eq_2
10.25  by (rule DERIV_inverse)
10.26
10.27 @@ -166,13 +166,13 @@
10.28
10.29  lemma CDERIV_inverse_fun:
10.30       "[| DERIV f x :> d; f(x) \<noteq> (0::complex) |]
10.31 -      ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"
10.32 +      ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse ((f x)\<^sup>2)))"
10.33  unfolding numeral_2_eq_2
10.34  by (rule DERIV_inverse_fun)
10.35
10.36  lemma NSCDERIV_inverse_fun:
10.37       "[| NSDERIV f x :> d; f(x) \<noteq> (0::complex) |]
10.38 -      ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"
10.39 +      ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse ((f x)\<^sup>2)))"
10.40  unfolding numeral_2_eq_2
10.41  by (rule NSDERIV_inverse_fun)
10.42
10.43 @@ -181,13 +181,13 @@
10.44
10.45  lemma CDERIV_quotient:
10.46       "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> (0::complex) |]
10.47 -       ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)"
10.48 +       ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / ((g x)\<^sup>2)"
10.49  unfolding numeral_2_eq_2
10.50  by (rule DERIV_quotient)
10.51
10.52  lemma NSCDERIV_quotient:
10.53       "[| NSDERIV f x :> d; NSDERIV g x :> e; g(x) \<noteq> (0::complex) |]
10.54 -       ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)"
10.55 +       ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / ((g x)\<^sup>2)"
10.56  unfolding numeral_2_eq_2
10.57  by (rule NSDERIV_quotient)
10.58
```
```    11.1 --- a/src/HOL/NSA/HTranscendental.thy	Sun Aug 18 18:49:45 2013 +0200
11.2 +++ b/src/HOL/NSA/HTranscendental.thy	Sun Aug 18 19:59:19 2013 +0200
11.3 @@ -103,7 +103,7 @@
11.4  lemma hypreal_sqrt_ge_zero: "0 \<le> x ==> 0 \<le> ( *f* sqrt)(x)"
11.5  by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less)
11.6
11.7 -lemma hypreal_sqrt_hrabs [simp]: "!!x. ( *f* sqrt)(x ^ 2) = abs(x)"
11.8 +lemma hypreal_sqrt_hrabs [simp]: "!!x. ( *f* sqrt)(x\<^sup>2) = abs(x)"
11.9  by (transfer, simp)
11.10
11.11  lemma hypreal_sqrt_hrabs2 [simp]: "!!x. ( *f* sqrt)(x*x) = abs(x)"
11.12 @@ -128,7 +128,7 @@
11.13  apply (auto simp add: st_hrabs st_zero_le star_sqrt_HFinite)
11.14  done
11.15
11.16 -lemma hypreal_sqrt_sum_squares_ge1 [simp]: "!!x y. x \<le> ( *f* sqrt)(x ^ 2 + y ^ 2)"
11.17 +lemma hypreal_sqrt_sum_squares_ge1 [simp]: "!!x y. x \<le> ( *f* sqrt)(x\<^sup>2 + y\<^sup>2)"
11.18  by transfer (rule real_sqrt_sum_squares_ge1)
11.19
11.20  lemma HFinite_hypreal_sqrt:
11.21 @@ -584,14 +584,14 @@
11.22  text{*A familiar approximation to @{term "cos x"} when @{term x} is small*}
11.23
11.24  lemma STAR_cos_Infinitesimal_approx:
11.25 -     "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - x ^ 2"
11.26 +     "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - x\<^sup>2"
11.27  apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
11.28  apply (auto simp add: Infinitesimal_approx_minus [symmetric]
11.30  done
11.31
11.32  lemma STAR_cos_Infinitesimal_approx2:
11.33 -     "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - (x ^ 2)/2"
11.34 +     "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - (x\<^sup>2)/2"
11.35  apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
11.36  apply (auto intro: Infinitesimal_SReal_divide
11.37              simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2)
```
```    12.1 --- a/src/HOL/NSA/NSComplex.thy	Sun Aug 18 18:49:45 2013 +0200
12.2 +++ b/src/HOL/NSA/NSComplex.thy	Sun Aug 18 19:59:19 2013 +0200
12.3 @@ -325,7 +325,7 @@
12.4  by transfer (rule complex_cnj_zero_iff)
12.5
12.6  lemma hcomplex_mult_hcnj:
12.7 -     "!!z. z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)"
12.8 +     "!!z. z * hcnj z = hcomplex_of_hypreal ((hRe z)\<^sup>2 + (hIm z)\<^sup>2)"
12.9  by transfer (rule complex_mult_cnj)
12.10
12.11
12.12 @@ -339,7 +339,7 @@
12.13       "hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n"
12.14  by simp
12.15
12.16 -lemma hcmod_mult_hcnj: "!!z. hcmod(z * hcnj(z)) = hcmod(z) ^ 2"
12.17 +lemma hcmod_mult_hcnj: "!!z. hcmod(z * hcnj(z)) = (hcmod z)\<^sup>2"
12.18  by transfer (rule complex_mod_mult_cnj)
12.19
12.20  lemma hcmod_triangle_ineq2 [simp]:
12.21 @@ -358,7 +358,7 @@
12.22  lemma hcomplexpow_Suc [simp]: "z ^ (Suc n) = (z::hcomplex) * (z ^ n)"
12.23  by (rule power_Suc)
12.24
12.25 -lemma hcomplexpow_i_squared [simp]: "iii ^ 2 = -1"
12.26 +lemma hcomplexpow_i_squared [simp]: "iii\<^sup>2 = -1"
12.27  by transfer (rule power2_i)
12.28
12.29  lemma hcomplex_of_hypreal_pow:
12.30 @@ -405,7 +405,7 @@
12.31  lemma hsgn_eq: "!!z. hsgn z = z / hcomplex_of_hypreal (hcmod z)"
12.32  by transfer (rule sgn_eq)
12.33
12.34 -lemma hcmod_i: "!!x y. hcmod (HComplex x y) = ( *f* sqrt) (x ^ 2 + y ^ 2)"
12.35 +lemma hcmod_i: "!!x y. hcmod (HComplex x y) = ( *f* sqrt) (x\<^sup>2 + y\<^sup>2)"
12.36  by transfer (rule complex_norm)
12.37
12.38  lemma hcomplex_eq_cancel_iff1 [simp]:
12.39 @@ -435,8 +435,7 @@
12.40  by transfer (rule Im_sgn)
12.41
12.42  lemma HComplex_inverse:
12.43 -     "!!x y. inverse (HComplex x y) =
12.44 -      HComplex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"
12.45 +     "!!x y. inverse (HComplex x y) = HComplex (x/(x\<^sup>2 + y\<^sup>2)) (-y/(x\<^sup>2 + y\<^sup>2))"
12.46  by transfer (rule complex_inverse)
12.47
12.48  lemma hRe_mult_i_eq[simp]:
```
```    13.1 --- a/src/HOL/Number_Theory/Fib.thy	Sun Aug 18 18:49:45 2013 +0200
13.2 +++ b/src/HOL/Number_Theory/Fib.thy	Sun Aug 18 19:59:19 2013 +0200
13.3 @@ -169,24 +169,24 @@
13.4  *}
13.5
13.6  lemma fib_Cassini_aux_int: "fib (int n + 2) * fib (int n) -
13.7 -    (fib (int n + 1))^2 = (-1)^(n + 1)"
13.8 +    (fib (int n + 1))\<^sup>2 = (-1)^(n + 1)"
13.9    apply (induct n)
13.11    done
13.12
13.13  lemma fib_Cassini_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n -
13.14 -    (fib (n + 1))^2 = (-1)^(nat n + 1)"
13.15 +    (fib (n + 1))\<^sup>2 = (-1)^(nat n + 1)"
13.16    by (insert fib_Cassini_aux_int [of "nat n"], auto)
13.17
13.18  (*
13.19  lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n =
13.20 -    (fib (n + 1))^2 + (-1)^(nat n + 1)"
13.21 +    (fib (n + 1))\<^sup>2 + (-1)^(nat n + 1)"
13.22    by (frule fib_Cassini_int, simp)
13.23  *)
13.24
13.25  lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib ((n::int) + 2) * fib n =
13.26 -  (if even n then tsub ((fib (n + 1))^2) 1
13.27 -   else (fib (n + 1))^2 + 1)"
13.28 +  (if even n then tsub ((fib (n + 1))\<^sup>2) 1
13.29 +   else (fib (n + 1))\<^sup>2 + 1)"
13.30    apply (frule fib_Cassini_int, auto simp add: pos_int_even_equiv_nat_even)
13.31    apply (subst tsub_eq)
13.32    apply (insert fib_gr_0_int [of "n + 1"], force)
13.33 @@ -194,8 +194,8 @@
13.34    done
13.35
13.36  lemma fib_Cassini_nat: "fib ((n::nat) + 2) * fib n =
13.37 -    (if even n then (fib (n + 1))^2 - 1
13.38 -     else (fib (n + 1))^2 + 1)"
13.39 +    (if even n then (fib (n + 1))\<^sup>2 - 1
13.40 +     else (fib (n + 1))\<^sup>2 + 1)"
13.41    by (rule fib_Cassini'_int [transferred, of n], auto)
13.42
13.43
```
```    14.1 --- a/src/HOL/Old_Number_Theory/Euler.thy	Sun Aug 18 18:49:45 2013 +0200
14.2 +++ b/src/HOL/Old_Number_Theory/Euler.thy	Sun Aug 18 19:59:19 2013 +0200
14.3 @@ -75,7 +75,7 @@
14.4      from this and a show ?thesis
14.5        by (auto simp add: zcong_zmult_prop2)
14.6    qed
14.7 -  then have "[j^2 = a] (mod p)" by (simp add: power2_eq_square)
14.8 +  then have "[j\<^sup>2 = a] (mod p)" by (simp add: power2_eq_square)
14.10  qed
14.11
14.12 @@ -269,7 +269,7 @@
14.13
14.14  text {* \medskip Prove the final part of Euler's Criterion: *}
14.15
14.16 -lemma aux__1: "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> ~(p dvd y)"
14.17 +lemma aux__1: "[| ~([x = 0] (mod p)); [y\<^sup>2 = x] (mod p)|] ==> ~(p dvd y)"
14.18    by (metis dvdI power2_eq_square zcong_sym zcong_trans zcong_zero_equiv_div dvd_trans)
14.19
14.20  lemma aux__2: "2 * nat((p - 1) div 2) =  nat (2 * ((p - 1) div 2))"
```
```    15.1 --- a/src/HOL/Old_Number_Theory/EvenOdd.thy	Sun Aug 18 18:49:45 2013 +0200
15.2 +++ b/src/HOL/Old_Number_Theory/EvenOdd.thy	Sun Aug 18 19:59:19 2013 +0200
15.3 @@ -175,9 +175,9 @@
15.5    finally have "(-1::int)^nat x = (-1)^(2 * nat a)"
15.6      by simp
15.7 -  also have "... = ((-1::int)^2)^ (nat a)"
15.8 +  also have "... = (-1::int)\<^sup>2 ^ nat a"
15.9      by (simp add: zpower_zpower [symmetric])
15.10 -  also have "(-1::int)^2 = 1"
15.11 +  also have "(-1::int)\<^sup>2 = 1"
15.12      by simp
15.13    finally show ?thesis
15.14      by simp
15.15 @@ -192,11 +192,11 @@
15.16      by simp
15.17    also from a have "nat (2 * a + 1) = 2 * nat a + 1"
15.19 -  finally have "(-1::int)^nat x = (-1)^(2 * nat a + 1)"
15.20 +  finally have "(-1::int) ^ nat x = (-1)^(2 * nat a + 1)"
15.21      by simp
15.22 -  also have "... = ((-1::int)^2)^ (nat a) * (-1)^1"
15.23 +  also have "... = ((-1::int)\<^sup>2) ^ nat a * (-1)^1"
15.25 -  also have "(-1::int)^2 = 1"
15.26 +  also have "(-1::int)\<^sup>2 = 1"
15.27      by simp
15.28    finally show ?thesis
15.29      by simp
```
```    16.1 --- a/src/HOL/Old_Number_Theory/Pocklington.thy	Sun Aug 18 18:49:45 2013 +0200
16.2 +++ b/src/HOL/Old_Number_Theory/Pocklington.thy	Sun Aug 18 19:59:19 2013 +0200
16.3 @@ -940,32 +940,32 @@
16.4  qed
16.5
16.6  lemma prime_divisor_sqrt:
16.7 -  "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d^2 \<le> n \<longrightarrow> d = 1)"
16.8 +  "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d\<^sup>2 \<le> n \<longrightarrow> d = 1)"
16.9  proof-
16.10    {assume "n=0 \<or> n=1" hence ?thesis using prime_0 prime_1
16.11      by (auto simp add: nat_power_eq_0_iff)}
16.12    moreover
16.13    {assume n: "n\<noteq>0" "n\<noteq>1"
16.14      hence np: "n > 1" by arith
16.15 -    {fix d assume d: "d dvd n" "d^2 \<le> n" and H: "\<forall>m. m dvd n \<longrightarrow> m=1 \<or> m=n"
16.16 +    {fix d assume d: "d dvd n" "d\<^sup>2 \<le> n" and H: "\<forall>m. m dvd n \<longrightarrow> m=1 \<or> m=n"
16.17        from H d have d1n: "d = 1 \<or> d=n" by blast
16.18        {assume dn: "d=n"
16.19 -        have "n^2 > n*1" using n by (simp add: power2_eq_square)
16.20 +        have "n\<^sup>2 > n*1" using n by (simp add: power2_eq_square)
16.21          with dn d(2) have "d=1" by simp}
16.22        with d1n have "d = 1" by blast  }
16.23      moreover
16.24 -    {fix d assume d: "d dvd n" and H: "\<forall>d'. d' dvd n \<and> d'^2 \<le> n \<longrightarrow> d' = 1"
16.25 +    {fix d assume d: "d dvd n" and H: "\<forall>d'. d' dvd n \<and> d'\<^sup>2 \<le> n \<longrightarrow> d' = 1"
16.26        from d n have "d \<noteq> 0" apply - apply (rule ccontr) by simp
16.27        hence dp: "d > 0" by simp
16.28        from d[unfolded dvd_def] obtain e where e: "n= d*e" by blast
16.29        from n dp e have ep:"e > 0" by simp
16.30 -      have "d^2 \<le> n \<or> e^2 \<le> n" using dp ep
16.31 +      have "d\<^sup>2 \<le> n \<or> e\<^sup>2 \<le> n" using dp ep
16.32          by (auto simp add: e power2_eq_square mult_le_cancel_left)
16.33        moreover
16.34 -      {assume h: "d^2 \<le> n"
16.35 +      {assume h: "d\<^sup>2 \<le> n"
16.36          from H[rule_format, of d] h d have "d = 1" by blast}
16.37        moreover
16.38 -      {assume h: "e^2 \<le> n"
16.39 +      {assume h: "e\<^sup>2 \<le> n"
16.40          from e have "e dvd n" unfolding dvd_def by (simp add: mult_commute)
16.41          with H[rule_format, of e] h have "e=1" by simp
16.42          with e have "d = n" by simp}
16.43 @@ -974,7 +974,7 @@
16.44    ultimately show ?thesis by auto
16.45  qed
16.46  lemma prime_prime_factor_sqrt:
16.47 -  "prime n \<longleftrightarrow> n \<noteq> 0 \<and> n \<noteq> 1 \<and> \<not> (\<exists>p. prime p \<and> p dvd n \<and> p^2 \<le> n)"
16.48 +  "prime n \<longleftrightarrow> n \<noteq> 0 \<and> n \<noteq> 1 \<and> \<not> (\<exists>p. prime p \<and> p dvd n \<and> p\<^sup>2 \<le> n)"
16.49    (is "?lhs \<longleftrightarrow>?rhs")
16.50  proof-
16.51    {assume "n=0 \<or> n=1" hence ?thesis using prime_0 prime_1 by auto}
16.52 @@ -990,14 +990,14 @@
16.53      }
16.54      moreover
16.55      {assume H: ?rhs
16.56 -      {fix d assume d: "d dvd n" "d^2 \<le> n" "d\<noteq>1"
16.57 +      {fix d assume d: "d dvd n" "d\<^sup>2 \<le> n" "d\<noteq>1"
16.58          from prime_factor[OF d(3)]
16.59          obtain p where p: "prime p" "p dvd d" by blast
16.60          from n have np: "n > 0" by arith
16.61          from d(1) n have "d \<noteq> 0" by - (rule ccontr, auto)
16.62          hence dp: "d > 0" by arith
16.63          from mult_mono[OF dvd_imp_le[OF p(2) dp] dvd_imp_le[OF p(2) dp]] d(2)
16.64 -        have "p^2 \<le> n" unfolding power2_eq_square by arith
16.65 +        have "p\<^sup>2 \<le> n" unfolding power2_eq_square by arith
16.66          with H n p(1) dvd_trans[OF p(2) d(1)] have False  by blast}
16.67        with n prime_divisor_sqrt  have ?lhs by auto}
16.68      ultimately have ?thesis by blast }
16.69 @@ -1073,7 +1073,7 @@
16.70  qed
16.71
16.72  lemma pocklington:
16.73 -  assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q^2"
16.74 +  assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q\<^sup>2"
16.75    and an: "[a^ (n - 1) = 1] (mod n)"
16.76    and aq:"\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n - 1) div p) - 1) n"
16.77    shows "prime n"
16.78 @@ -1081,7 +1081,7 @@
16.79  proof-
16.80    let ?ths = "n \<noteq> 0 \<and> n \<noteq> 1 \<and> \<not> (\<exists>p. prime p \<and> p dvd n \<and> p\<^sup>2 \<le> n)"
16.81    from n have n01: "n\<noteq>0" "n\<noteq>1" by arith+
16.82 -  {fix p assume p: "prime p" "p dvd n" "p^2 \<le> n"
16.83 +  {fix p assume p: "prime p" "p dvd n" "p\<^sup>2 \<le> n"
16.84      from p(3) sqr have "p^(Suc 1) \<le> q^(Suc 1)" by (simp add: power2_eq_square)
16.85      hence pq: "p \<le> q" unfolding exp_mono_le .
16.86      from pocklington_lemma[OF n nqr an aq p(1,2)]  cong_1_divides
16.87 @@ -1093,7 +1093,7 @@
16.88
16.89  (* Variant for application, to separate the exponentiation.                  *)
16.90  lemma pocklington_alt:
16.91 -  assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q^2"
16.92 +  assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q\<^sup>2"
16.93    and an: "[a^ (n - 1) = 1] (mod n)"
16.94    and aq:"\<forall>p. prime p \<and> p dvd q \<longrightarrow> (\<exists>b. [a^((n - 1) div p) = b] (mod n) \<and> coprime (b - 1) n)"
16.95    shows "prime n"
16.96 @@ -1205,7 +1205,7 @@
16.97
16.98
16.99  lemma pocklington_primefact:
16.100 -  assumes n: "n \<ge> 2" and qrn: "q*r = n - 1" and nq2: "n \<le> q^2"
16.101 +  assumes n: "n \<ge> 2" and qrn: "q*r = n - 1" and nq2: "n \<le> q\<^sup>2"
16.102    and arnb: "(a^r) mod n = b" and psq: "foldr op * ps 1 = q"
16.103    and bqn: "(b^q) mod n = 1"
16.104    and psp: "list_all (\<lambda>p. prime p \<and> coprime ((b^(q div p)) mod n - 1) n) ps"
```
```    17.1 --- a/src/HOL/Old_Number_Theory/Primes.thy	Sun Aug 18 18:49:45 2013 +0200
17.2 +++ b/src/HOL/Old_Number_Theory/Primes.thy	Sun Aug 18 19:59:19 2013 +0200
17.3 @@ -56,39 +56,39 @@
17.4  using power_inject_base[of x n y] by auto
17.5
17.6
17.7 -lemma even_square: assumes e: "even (n::nat)" shows "\<exists>x. n ^ 2 = 4*x"
17.8 +lemma even_square: assumes e: "even (n::nat)" shows "\<exists>x. n\<^sup>2 = 4*x"
17.9  proof-
17.10    from e have "2 dvd n" by presburger
17.11    then obtain k where k: "n = 2*k" using dvd_def by auto
17.12 -  hence "n^2 = 4* (k^2)" by (simp add: power2_eq_square)
17.13 +  hence "n\<^sup>2 = 4 * k\<^sup>2" by (simp add: power2_eq_square)
17.14    thus ?thesis by blast
17.15  qed
17.16
17.17 -lemma odd_square: assumes e: "odd (n::nat)" shows "\<exists>x. n ^ 2 = 4*x + 1"
17.18 +lemma odd_square: assumes e: "odd (n::nat)" shows "\<exists>x. n\<^sup>2 = 4*x + 1"
17.19  proof-
17.20    from e have np: "n > 0" by presburger
17.21    from e have "2 dvd (n - 1)" by presburger
17.22    then obtain k where "n - 1 = 2*k" using dvd_def by auto
17.23    hence k: "n = 2*k + 1"  using e by presburger
17.24 -  hence "n^2 = 4* (k^2 + k) + 1" by algebra
17.25 +  hence "n\<^sup>2 = 4* (k\<^sup>2 + k) + 1" by algebra
17.26    thus ?thesis by blast
17.27  qed
17.28
17.29 -lemma diff_square: "(x::nat)^2 - y^2 = (x+y)*(x - y)"
17.30 +lemma diff_square: "(x::nat)\<^sup>2 - y\<^sup>2 = (x+y)*(x - y)"
17.31  proof-
17.32    have "x \<le> y \<or> y \<le> x" by (rule nat_le_linear)
17.33    moreover
17.34    {assume le: "x \<le> y"
17.35 -    hence "x ^2 \<le> y^2" by (simp only: numeral_2_eq_2 exp_mono_le Let_def)
17.36 +    hence "x\<^sup>2 \<le> y\<^sup>2" by (simp only: numeral_2_eq_2 exp_mono_le Let_def)
17.37      with le have ?thesis by simp }
17.38    moreover
17.39    {assume le: "y \<le> x"
17.40 -    hence le2: "y ^2 \<le> x^2" by (simp only: numeral_2_eq_2 exp_mono_le Let_def)
17.41 +    hence le2: "y\<^sup>2 \<le> x\<^sup>2" by (simp only: numeral_2_eq_2 exp_mono_le Let_def)
17.42      from le have "\<exists>z. y + z = x" by presburger
17.43      then obtain z where z: "x = y + z" by blast
17.44 -    from le2 have "\<exists>z. x^2 = y^2 + z" by presburger
17.45 -    then obtain z2 where z2: "x^2 = y^2 + z2"  by blast
17.46 -    from z z2 have ?thesis apply simp by algebra }
17.47 +    from le2 have "\<exists>z. x\<^sup>2 = y\<^sup>2 + z" by presburger
17.48 +    then obtain z2 where z2: "x\<^sup>2 = y\<^sup>2 + z2" by blast
17.49 +    from z z2 have ?thesis by simp algebra }
17.50    ultimately show ?thesis by blast
17.51  qed
17.52
17.53 @@ -544,29 +544,29 @@
17.54    from g(2,3) dvd_trans[OF p(2)] p(1) show ?thesis by auto
17.55  qed
17.56  lemma coprime_sos: assumes xy: "coprime x y"
17.57 -  shows "coprime (x * y) (x^2 + y^2)"
17.58 +  shows "coprime (x * y) (x\<^sup>2 + y\<^sup>2)"
17.59  proof-
17.60 -  {assume c: "\<not> coprime (x * y) (x^2 + y^2)"
17.61 +  {assume c: "\<not> coprime (x * y) (x\<^sup>2 + y\<^sup>2)"
17.62      from coprime_prime_dvd_ex[OF c] obtain p
17.63 -      where p: "prime p" "p dvd x*y" "p dvd x^2 + y^2" by blast
17.64 +      where p: "prime p" "p dvd x*y" "p dvd x\<^sup>2 + y\<^sup>2" by blast
17.65      {assume px: "p dvd x"
17.66        from dvd_mult[OF px, of x] p(3)
17.67 -        obtain r s where "x * x = p * r" and "x^2 + y^2 = p * s"
17.68 +        obtain r s where "x * x = p * r" and "x\<^sup>2 + y\<^sup>2 = p * s"
17.69            by (auto elim!: dvdE)
17.70 -        then have "y^2 = p * (s - r)"
17.71 +        then have "y\<^sup>2 = p * (s - r)"
17.72            by (auto simp add: power2_eq_square diff_mult_distrib2)
17.73 -        then have "p dvd y^2" ..
17.74 +        then have "p dvd y\<^sup>2" ..
17.75        with prime_divexp[OF p(1), of y 2] have py: "p dvd y" .
17.76        from p(1) px py xy[unfolded coprime, rule_format, of p] prime_1
17.77        have False by simp }
17.78      moreover
17.79      {assume py: "p dvd y"
17.80        from dvd_mult[OF py, of y] p(3)
17.81 -        obtain r s where "y * y = p * r" and "x^2 + y^2 = p * s"
17.82 +        obtain r s where "y * y = p * r" and "x\<^sup>2 + y\<^sup>2 = p * s"
17.83            by (auto elim!: dvdE)
17.84 -        then have "x^2 = p * (s - r)"
17.85 +        then have "x\<^sup>2 = p * (s - r)"
17.86            by (auto simp add: power2_eq_square diff_mult_distrib2)
17.87 -        then have "p dvd x^2" ..
17.88 +        then have "p dvd x\<^sup>2" ..
17.89        with prime_divexp[OF p(1), of x 2] have px: "p dvd x" .
17.90        from p(1) px py xy[unfolded coprime, rule_format, of p] prime_1
17.91        have False by simp }
```
```    18.1 --- a/src/HOL/Old_Number_Theory/Residues.thy	Sun Aug 18 18:49:45 2013 +0200
18.2 +++ b/src/HOL/Old_Number_Theory/Residues.thy	Sun Aug 18 19:59:19 2013 +0200
18.3 @@ -19,7 +19,7 @@
18.4    where "StandardRes m x = x mod m"
18.5
18.6  definition QuadRes :: "int => int => bool"
18.7 -  where "QuadRes m x = (\<exists>y. ([(y ^ 2) = x] (mod m)))"
18.8 +  where "QuadRes m x = (\<exists>y. ([y\<^sup>2 = x] (mod m)))"
18.9
18.10  definition Legendre :: "int => int => int" where
18.11    "Legendre a p = (if ([a = 0] (mod p)) then 0
```
```    19.1 --- a/src/HOL/Probability/Distributions.thy	Sun Aug 18 18:49:45 2013 +0200
19.2 +++ b/src/HOL/Probability/Distributions.thy	Sun Aug 18 19:59:19 2013 +0200
19.3 @@ -372,7 +372,7 @@
19.4    also have "(\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel) = (a + b) / 2"
19.5    proof (subst integral_FTC_atLeastAtMost)
19.6      fix x
19.7 -    show "DERIV (\<lambda>x. x ^ 2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}"
19.8 +    show "DERIV (\<lambda>x. x\<^sup>2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}"
19.9        using uniform_distributed_params[OF D]
19.10        by (auto intro!: DERIV_intros)
19.11      show "isCont (\<lambda>x. x / Sigma_Algebra.measure lborel {a..b}) x"
```
```    20.1 --- a/src/HOL/ex/Groebner_Examples.thy	Sun Aug 18 18:49:45 2013 +0200
20.2 +++ b/src/HOL/ex/Groebner_Examples.thy	Sun Aug 18 19:59:19 2013 +0200
20.3 @@ -47,8 +47,8 @@
20.4    by simp
20.5
20.6  lemma
20.7 -  assumes "a * x^2 + b * x + c = (0::int)" and "d * x^2 + e * x + f = 0"
20.8 -  shows "d^2*c^2 - 2*d*c*a*f + a^2*f^2 - e*d*b*c - e*b*a*f + a*e^2*c + f*d*b^2 = 0"
20.9 +  assumes "a * x\<^sup>2 + b * x + c = (0::int)" and "d * x\<^sup>2 + e * x + f = 0"
20.10 +  shows "d\<^sup>2*c\<^sup>2 - 2*d*c*a*f + a\<^sup>2 * f\<^sup>2 - e*d*b*c - e*b*a*f + a*e\<^sup>2*c + f*d*b\<^sup>2 = 0"
20.11    using assms by algebra
20.12
20.13  lemma "(x::int)^3  - x^2  - 5*x - 3 = 0 \<longleftrightarrow> (x = 3 \<or> x = -1)"
20.14 @@ -58,8 +58,8 @@
20.15    by algebra
20.16
20.17  lemma
20.18 -  fixes x::"'a::{idom}"
20.19 -  shows "x^2*y = x^2 & x*y^2 = y^2 \<longleftrightarrow>  x=1 & y=1 | x=0 & y=0"
20.20 +  fixes x::"'a::idom"
20.21 +  shows "x\<^sup>2*y = x\<^sup>2 & x*y\<^sup>2 = y\<^sup>2 \<longleftrightarrow>  x = 1 & y = 1 | x = 0 & y = 0"
20.22    by algebra
20.23
20.24  subsection {* Lemmas for Lagrange's theorem *}
```