more symbols;
authorwenzelm
Sun Aug 18 19:59:19 2013 +0200 (2013-08-18)
changeset 53077a1b3784f8129
parent 53076 47c9aff07725
child 53078 cc06f17d8057
more symbols;
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Commutative_Ring.thy
src/HOL/Decision_Procs/ex/Approximation_Ex.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Fundamental_Theorem_Algebra.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Determinants.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/NSA/CLim.thy
src/HOL/NSA/HTranscendental.thy
src/HOL/NSA/NSComplex.thy
src/HOL/Number_Theory/Fib.thy
src/HOL/Old_Number_Theory/Euler.thy
src/HOL/Old_Number_Theory/EvenOdd.thy
src/HOL/Old_Number_Theory/Pocklington.thy
src/HOL/Old_Number_Theory/Primes.thy
src/HOL/Old_Number_Theory/Residues.thy
src/HOL/Probability/Distributions.thy
src/HOL/ex/Groebner_Examples.thy
     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.9              by (simp add: numerals)
    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.18      apply (simp add: field_simps)
    4.19      apply (simp add: mult_assoc[symmetric])
    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.28      by (simp add: field_simps)
    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.18        by (simp add: power2_eq_square)
    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.46        by (simp_all add: power_mult_distrib)
    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.56    apply (simp add: rcis_mult)
    5.57    apply (simp add: power2_eq_square[symmetric])
    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.65    apply (simp add: rcis_mult add_divide_distrib)
    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.9        by (simp add: power2_eq_square)
    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.87  lemmas inner_simps = inner_add_left inner_add_right inner_diff_right inner_diff_left 
    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.9  by (simp add: numeral_2_eq_2)
   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.29              diff_minus add_assoc [symmetric] numeral_2_eq_2)
   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.10    apply (auto simp add: field_simps power2_eq_square fib_reduce_int power_add)
   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.9    with assms show False by (simp add: QuadRes_def)
   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.4      by (simp add: nat_mult_distrib)
    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.18      by (auto simp add: nat_mult_distrib nat_add_distrib)
   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.24      by (auto simp add: power_mult power_add)
   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 *}