--- a/src/HOL/Decision_Procs/Approximation.thy Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Sun Aug 18 19:59:19 2013 +0200
@@ -234,10 +234,10 @@
assumes "sqrt x < b" and "0 < b" and "0 < x"
shows "sqrt x < (b + x / b)/2"
proof -
- from assms have "0 < (b - sqrt x) ^ 2 " by simp
- also have "\<dots> = b ^ 2 - 2 * b * sqrt x + (sqrt x) ^ 2" by algebra
- also have "\<dots> = b ^ 2 - 2 * b * sqrt x + x" using assms by simp
- finally have "0 < b ^ 2 - 2 * b * sqrt x + x" by assumption
+ from assms have "0 < (b - sqrt x)\<^sup>2 " by simp
+ also have "\<dots> = b\<^sup>2 - 2 * b * sqrt x + (sqrt x)\<^sup>2" by algebra
+ also have "\<dots> = b\<^sup>2 - 2 * b * sqrt x + x" using assms by simp
+ finally have "0 < b\<^sup>2 - 2 * b * sqrt x + x" .
hence "0 < b / 2 - sqrt x + x / (2 * b)" using assms
by (simp add: field_simps power2_eq_square)
thus ?thesis by (simp add: field_simps)
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Sun Aug 18 19:59:19 2013 +0200
@@ -287,7 +287,7 @@
by (simp only: numerals even_nat_div_two_times_two [OF `even w`])
have "Ipol ls P * Ipol ls P = Ipol ls P ^ Suc (Suc 0)"
by simp
- then have "Ipol ls P * Ipol ls P = Ipol ls P ^ 2"
+ then have "Ipol ls P * Ipol ls P = (Ipol ls P)\<^sup>2"
by (simp add: numerals)
with Suc show ?thesis
by (auto simp add: power_mult [symmetric, of _ 2 _] two_times mul_ci sqr_ci
--- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Sun Aug 18 19:59:19 2013 +0200
@@ -72,7 +72,7 @@
shows "g / v * tan (35 * d) \<in> { 3 * d .. 3.1 * d }"
using assms by (approximation 20)
-lemma "x \<in> { 0 .. 1 :: real } \<longrightarrow> x ^ 2 \<le> x"
+lemma "x \<in> { 0 .. 1 :: real } \<longrightarrow> x\<^sup>2 \<le> x"
by (approximation 30 splitting: x=1 taylor: x = 3)
value [approximate] "10"
--- a/src/HOL/Library/Formal_Power_Series.thy Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Sun Aug 18 19:59:19 2013 +0200
@@ -1173,22 +1173,22 @@
lemma fps_inverse_deriv:
fixes a:: "('a :: field) fps"
assumes a0: "a$0 \<noteq> 0"
- shows "fps_deriv (inverse a) = - fps_deriv a * inverse a ^ 2"
+ shows "fps_deriv (inverse a) = - fps_deriv a * (inverse a)\<^sup>2"
proof-
from inverse_mult_eq_1[OF a0]
have "fps_deriv (inverse a * a) = 0" by simp
hence "inverse a * fps_deriv a + fps_deriv (inverse a) * a = 0" by simp
hence "inverse a * (inverse a * fps_deriv a + fps_deriv (inverse a) * a) = 0" by simp
with inverse_mult_eq_1[OF a0]
- have "inverse a ^ 2 * fps_deriv a + fps_deriv (inverse a) = 0"
+ have "(inverse a)\<^sup>2 * fps_deriv a + fps_deriv (inverse a) = 0"
unfolding power2_eq_square
apply (simp add: field_simps)
apply (simp add: mult_assoc[symmetric])
done
- then have "inverse a ^ 2 * fps_deriv a + fps_deriv (inverse a) - fps_deriv a * inverse a ^ 2 =
- 0 - fps_deriv a * inverse a ^ 2"
+ then have "(inverse a)\<^sup>2 * fps_deriv a + fps_deriv (inverse a) - fps_deriv a * (inverse a)\<^sup>2 =
+ 0 - fps_deriv a * (inverse a)\<^sup>2"
by simp
- then show "fps_deriv (inverse a) = - fps_deriv a * inverse a ^ 2"
+ then show "fps_deriv (inverse a) = - fps_deriv a * (inverse a)\<^sup>2"
by (simp add: field_simps)
qed
@@ -1223,7 +1223,7 @@
lemma fps_inverse_deriv':
fixes a:: "('a :: field) fps"
assumes a0: "a$0 \<noteq> 0"
- shows "fps_deriv (inverse a) = - fps_deriv a / a ^ 2"
+ shows "fps_deriv (inverse a) = - fps_deriv a / a\<^sup>2"
using fps_inverse_deriv[OF a0]
unfolding power2_eq_square fps_divide_def fps_inverse_mult
by simp
@@ -1236,7 +1236,7 @@
lemma fps_divide_deriv:
fixes a:: "('a :: field) fps"
assumes a0: "b$0 \<noteq> 0"
- shows "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b ^ 2"
+ shows "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b\<^sup>2"
using fps_inverse_deriv[OF a0]
by (simp add: fps_divide_def field_simps
power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0])
@@ -3210,7 +3210,7 @@
apply (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric] of_nat_add[symmetric])
by simp
-lemma binomial_Vandermonde_same: "setsum (\<lambda>k. (n choose k)^2) {0..n} = (2*n) choose n"
+lemma binomial_Vandermonde_same: "setsum (\<lambda>k. (n choose k)\<^sup>2) {0..n} = (2*n) choose n"
using binomial_Vandermonde[of n n n,symmetric]
unfolding mult_2 apply (simp add: power2_eq_square)
apply (rule setsum_cong2)
@@ -3425,8 +3425,8 @@
qed
lemma fps_sin_cos_sum_of_squares:
- "fps_cos c ^ 2 + fps_sin c ^ 2 = 1" (is "?lhs = 1")
-proof-
+ "(fps_cos c)\<^sup>2 + (fps_sin c)\<^sup>2 = 1" (is "?lhs = 1")
+proof -
have "fps_deriv ?lhs = 0"
apply (simp add: fps_deriv_power fps_sin_deriv fps_cos_deriv)
apply (simp add: field_simps fps_const_neg[symmetric] del: fps_const_neg)
@@ -3546,7 +3546,7 @@
definition "fps_tan c = fps_sin c / fps_cos c"
-lemma fps_tan_deriv: "fps_deriv(fps_tan c) = fps_const c/ (fps_cos c ^ 2)"
+lemma fps_tan_deriv: "fps_deriv (fps_tan c) = fps_const c / (fps_cos c)\<^sup>2"
proof -
have th0: "fps_cos c $ 0 \<noteq> 0" by (simp add: fps_cos_def)
show ?thesis
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Sun Aug 18 19:59:19 2013 +0200
@@ -14,7 +14,7 @@
else Complex (sqrt((cmod z + Re z) /2))
((Im z / abs(Im z)) * sqrt((cmod z - Re z) /2)))"
-lemma csqrt[algebra]: "csqrt z ^ 2 = z"
+lemma csqrt[algebra]: "(csqrt z)\<^sup>2 = z"
proof-
obtain x y where xy: "z = Complex x y" by (cases z)
{assume y0: "y = 0"
@@ -34,13 +34,15 @@
hence "cmod ?z - x \<ge> 0" "cmod ?z + x \<ge> 0" by arith+
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) }
note th = this
- have sq4: "\<And>x::real. x^2 / 4 = (x / 2) ^ 2"
+ have sq4: "\<And>x::real. x\<^sup>2 / 4 = (x / 2)\<^sup>2"
by (simp add: power2_eq_square)
from th[of x y]
- 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
+ have sq4': "sqrt (((sqrt (x * x + y * y) + x)\<^sup>2 / 4)) = (sqrt (x * x + y * y) + x) / 2"
+ "sqrt (((sqrt (x * x + y * y) - x)\<^sup>2 / 4)) = (sqrt (x * x + y * y) - x) / 2"
+ unfolding sq4 by simp_all
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"
unfolding power2_eq_square by simp
- have "sqrt 4 = sqrt (2^2)" by simp
+ have "sqrt 4 = sqrt (2\<^sup>2)" by simp
hence sqrt4: "sqrt 4 = 2" by (simp only: real_sqrt_abs)
have th2: "2 *(y * sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) + x) / 4)) / \<bar>y\<bar> = y"
using iffD2[OF real_sqrt_pow2_iff sum_power2_ge_zero[of x y]] y0
@@ -184,14 +186,14 @@
shows "cmod (z + 1) < 1 \<or> cmod (z - 1) < 1 \<or> cmod (z + ii) < 1 \<or> cmod (z - ii) < 1"
proof-
obtain x y where z: "z = Complex x y " by (cases z, auto)
- from md z have xy: "x^2 + y^2 = 1" by (simp add: cmod_def)
+ from md z have xy: "x\<^sup>2 + y\<^sup>2 = 1" by (simp add: cmod_def)
{assume C: "cmod (z + 1) \<ge> 1" "cmod (z - 1) \<ge> 1" "cmod (z + ii) \<ge> 1" "cmod (z - ii) \<ge> 1"
from C z xy have "2*x \<le> 1" "2*x \<ge> -1" "2*y \<le> 1" "2*y \<ge> -1"
by (simp_all add: cmod_def power2_eq_square algebra_simps)
hence "abs (2*x) \<le> 1" "abs (2*y) \<le> 1" by simp_all
- hence "(abs (2 * x))^2 <= 1^2" "(abs (2 * y)) ^2 <= 1^2"
+ hence "(abs (2 * x))\<^sup>2 <= 1\<^sup>2" "(abs (2 * y))\<^sup>2 <= 1\<^sup>2"
by - (rule power_mono, simp, simp)+
- hence th0: "4*x^2 \<le> 1" "4*y^2 \<le> 1"
+ hence th0: "4*x\<^sup>2 \<le> 1" "4*y\<^sup>2 \<le> 1"
by (simp_all add: power_mult_distrib)
from add_mono[OF th0] xy have False by simp }
thus ?thesis unfolding linorder_not_le[symmetric] by blast
@@ -454,7 +456,7 @@
ultimately show ?thesis by blast
qed
-lemma "(rcis (sqrt (abs r)) (a/2)) ^ 2 = rcis (abs r) a"
+lemma "(rcis (sqrt (abs r)) (a/2))\<^sup>2 = rcis (abs r) a"
unfolding power2_eq_square
apply (simp add: rcis_mult)
apply (simp add: power2_eq_square[symmetric])
@@ -464,7 +466,7 @@
unfolding cis_def
by simp
-lemma "(rcis (sqrt (abs r)) ((pi + a)/2)) ^ 2 = rcis (- abs r) a"
+lemma "(rcis (sqrt (abs r)) ((pi + a)/2))\<^sup>2 = rcis (- abs r) a"
unfolding power2_eq_square
apply (simp add: rcis_mult add_divide_distrib)
apply (simp add: power2_eq_square[symmetric] rcis_def cispi cis_mult[symmetric])
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sun Aug 18 19:59:19 2013 +0200
@@ -3361,7 +3361,7 @@
thus False using y[THEN bspec[where x="y + u *\<^sub>R (x - y)"]]
using assms(1)[unfolded convex_alt, THEN bspec[where x=y]]
using `x\<in>s` `y\<in>s` by (auto simp add: dist_commute algebra_simps) qed
- moreover have "0 < norm (y - z) ^ 2" using `y\<in>s` `z\<notin>s` by auto
+ moreover have "0 < (norm (y - z))\<^sup>2" using `y\<in>s` `z\<notin>s` by auto
hence "0 < inner (y - z) (y - z)" unfolding power2_norm_eq_inner by simp
ultimately show "inner (y - z) z + (norm (y - z))\<^sup>2 / 2 < inner (y - z) x"
unfolding power2_norm_eq_inner and not_less by (auto simp add: field_simps inner_commute inner_diff)
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Sun Aug 18 19:59:19 2013 +0200
@@ -629,7 +629,7 @@
then guess x .. note x=this
show ?thesis proof(cases "f a = f b")
case False
- have "norm (f b - f a) * norm (f b - f a) = norm (f b - f a)^2"
+ have "norm (f b - f a) * norm (f b - f a) = (norm (f b - f a))\<^sup>2"
by (simp add: power2_eq_square)
also have "\<dots> = (f b - f a) \<bullet> (f b - f a)" unfolding power2_norm_eq_inner ..
also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)"
--- a/src/HOL/Multivariate_Analysis/Determinants.thy Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy Sun Aug 18 19:59:19 2013 +0200
@@ -917,7 +917,7 @@
{fix v w
{fix x note fd[rule_format, of x 0, unfolded dist_norm f0 diff_0_right] }
note th0 = this
- have "f v \<bullet> f w = c^2 * (v \<bullet> w)"
+ have "f v \<bullet> f w = c\<^sup>2 * (v \<bullet> w)"
unfolding dot_norm_neg dist_norm[symmetric]
unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)}
note fc = this
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Sun Aug 18 19:59:19 2013 +0200
@@ -17,7 +17,7 @@
lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)"
proof -
- have "(x + 1/2)^2 + 3/4 > 0" using zero_le_power2[of "x+1/2"] by arith
+ have "(x + 1/2)\<^sup>2 + 3/4 > 0" using zero_le_power2[of "x+1/2"] by arith
then show ?thesis by (simp add: field_simps power2_eq_square)
qed
@@ -30,21 +30,21 @@
apply auto
done
-lemma real_le_lsqrt: "0 <= x \<Longrightarrow> 0 <= y \<Longrightarrow> x <= y^2 ==> sqrt x <= y"
- using real_sqrt_le_iff[of x "y^2"] by simp
-
-lemma real_le_rsqrt: "x^2 \<le> y \<Longrightarrow> x \<le> sqrt y"
- using real_sqrt_le_mono[of "x^2" y] by simp
-
-lemma real_less_rsqrt: "x^2 < y \<Longrightarrow> x < sqrt y"
- using real_sqrt_less_mono[of "x^2" y] by simp
+lemma real_le_lsqrt: "0 <= x \<Longrightarrow> 0 <= y \<Longrightarrow> x <= y\<^sup>2 ==> sqrt x <= y"
+ using real_sqrt_le_iff[of x "y\<^sup>2"] by simp
+
+lemma real_le_rsqrt: "x\<^sup>2 \<le> y \<Longrightarrow> x \<le> sqrt y"
+ using real_sqrt_le_mono[of "x\<^sup>2" y] by simp
+
+lemma real_less_rsqrt: "x\<^sup>2 < y \<Longrightarrow> x < sqrt y"
+ using real_sqrt_less_mono[of "x\<^sup>2" y] by simp
lemma sqrt_even_pow2:
assumes n: "even n"
shows "sqrt(2 ^ n) = 2 ^ (n div 2)"
proof -
from n obtain m where m: "n = 2*m" unfolding even_mult_two_ex ..
- from m have "sqrt(2 ^ n) = sqrt ((2 ^ m) ^ 2)"
+ from m have "sqrt(2 ^ n) = sqrt ((2 ^ m)\<^sup>2)"
by (simp only: power_mult[symmetric] mult_commute)
then show ?thesis using m by simp
qed
@@ -85,13 +85,13 @@
text{* Squaring equations and inequalities involving norms. *}
-lemma dot_square_norm: "x \<bullet> x = norm(x)^2"
+lemma dot_square_norm: "x \<bullet> x = (norm x)\<^sup>2"
by (simp only: power2_norm_eq_inner) (* TODO: move? *)
-lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a^2"
+lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a\<^sup>2"
by (auto simp add: norm_eq_sqrt_inner)
-lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)^2 \<le> y^2"
+lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)\<^sup>2 \<le> y\<^sup>2"
proof
assume "\<bar>x\<bar> \<le> \<bar>y\<bar>"
then have "\<bar>x\<bar>\<^sup>2 \<le> \<bar>y\<bar>\<^sup>2" by (rule power_mono, simp)
@@ -102,21 +102,21 @@
then show "\<bar>x\<bar> \<le> \<bar>y\<bar>" by simp
qed
-lemma norm_le_square: "norm(x) <= a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x <= a^2"
+lemma norm_le_square: "norm(x) <= a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x <= a\<^sup>2"
apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
using norm_ge_zero[of x]
apply arith
done
-lemma norm_ge_square: "norm(x) >= a \<longleftrightarrow> a <= 0 \<or> x \<bullet> x >= a ^ 2"
+lemma norm_ge_square: "norm(x) >= a \<longleftrightarrow> a <= 0 \<or> x \<bullet> x >= a\<^sup>2"
apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
using norm_ge_zero[of x]
apply arith
done
-lemma norm_lt_square: "norm(x) < a \<longleftrightarrow> 0 < a \<and> x \<bullet> x < a^2"
+lemma norm_lt_square: "norm(x) < a \<longleftrightarrow> 0 < a \<and> x \<bullet> x < a\<^sup>2"
by (metis not_le norm_ge_square)
-lemma norm_gt_square: "norm(x) > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a^2"
+lemma norm_gt_square: "norm(x) > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a\<^sup>2"
by (metis norm_le_square not_less)
text{* Dot product in terms of the norm rather than conversely. *}
@@ -124,10 +124,10 @@
lemmas inner_simps = inner_add_left inner_add_right inner_diff_right inner_diff_left
inner_scaleR_left inner_scaleR_right
-lemma dot_norm: "x \<bullet> y = (norm(x + y) ^2 - norm x ^ 2 - norm y ^ 2) / 2"
+lemma dot_norm: "x \<bullet> y = ((norm (x + y))\<^sup>2 - (norm x)\<^sup>2 - (norm y)\<^sup>2) / 2"
unfolding power2_norm_eq_inner inner_simps inner_commute by auto
-lemma dot_norm_neg: "x \<bullet> y = ((norm x ^ 2 + norm y ^ 2) - norm(x - y) ^ 2) / 2"
+lemma dot_norm_neg: "x \<bullet> y = (((norm x)\<^sup>2 + (norm y)\<^sup>2) - (norm (x - y))\<^sup>2) / 2"
unfolding power2_norm_eq_inner inner_simps inner_commute
by (auto simp add: algebra_simps)
@@ -469,11 +469,11 @@
lemma triangle_lemma:
- assumes x: "0 <= (x::real)" and y:"0 <= y" and z: "0 <= z" and xy: "x^2 <= y^2 + z^2"
+ assumes x: "0 <= (x::real)" and y:"0 <= y" and z: "0 <= z" and xy: "x\<^sup>2 <= y\<^sup>2 + z\<^sup>2"
shows "x <= y + z"
proof -
- have "y^2 + z^2 \<le> y^2 + 2*y*z + z^2" using z y by (simp add: mult_nonneg_nonneg)
- with xy have th: "x ^2 \<le> (y+z)^2" by (simp add: power2_eq_square field_simps)
+ 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)
+ with xy have th: "x\<^sup>2 \<le> (y+z)\<^sup>2" by (simp add: power2_eq_square field_simps)
from y z have yz: "y + z \<ge> 0" by arith
from power2_le_imp_le[OF th yz] show ?thesis .
qed
@@ -2592,11 +2592,11 @@
proof -
let ?d = "DIM('a)"
have "real ?d \<ge> 0" by simp
- then have d2: "(sqrt (real ?d))^2 = real ?d"
+ then have d2: "(sqrt (real ?d))\<^sup>2 = real ?d"
by (auto intro: real_sqrt_pow2)
have th: "sqrt (real ?d) * infnorm x \<ge> 0"
by (simp add: zero_le_mult_iff infnorm_pos_le)
- have th1: "x \<bullet> x \<le> (sqrt (real ?d) * infnorm x)^2"
+ have th1: "x \<bullet> x \<le> (sqrt (real ?d) * infnorm x)\<^sup>2"
unfolding power_mult_distrib d2
unfolding real_of_nat_def
apply(subst euclidean_inner)
@@ -2680,9 +2680,9 @@
by simp_all
then have n: "norm x > 0" "norm y > 0"
using norm_ge_zero[of x] norm_ge_zero[of y] by arith+
- have th: "\<And>(a::real) b c. a + b + c \<noteq> 0 ==> (a = b + c \<longleftrightarrow> a^2 = (b + c)^2)"
+ have th: "\<And>(a::real) b c. a + b + c \<noteq> 0 ==> (a = b + c \<longleftrightarrow> a\<^sup>2 = (b + c)\<^sup>2)"
by algebra
- have "norm(x + y) = norm x + norm y \<longleftrightarrow> norm(x + y)^ 2 = (norm x + norm y) ^2"
+ have "norm (x + y) = norm x + norm y \<longleftrightarrow> (norm (x + y))\<^sup>2 = (norm x + norm y)\<^sup>2"
apply (rule th) using n norm_ge_zero[of "x + y"]
apply arith
done
--- a/src/HOL/NSA/CLim.thy Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/NSA/CLim.thy Sun Aug 18 19:59:19 2013 +0200
@@ -15,7 +15,7 @@
(*??generalize*)
lemma lemma_complex_mult_inverse_squared [simp]:
- "x \<noteq> (0::complex) \<Longrightarrow> (x * inverse(x) ^ 2) = inverse x"
+ "x \<noteq> (0::complex) \<Longrightarrow> x * (inverse x)\<^sup>2 = inverse x"
by (simp add: numeral_2_eq_2)
text{*Changing the quantified variable. Install earlier?*}
@@ -152,12 +152,12 @@
text{*Can't relax the premise @{term "x \<noteq> 0"}: it isn't continuous at zero*}
lemma NSCDERIV_inverse:
- "(x::complex) \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))"
+ "(x::complex) \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- ((inverse x)\<^sup>2))"
unfolding numeral_2_eq_2
by (rule NSDERIV_inverse)
lemma CDERIV_inverse:
- "(x::complex) \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))"
+ "(x::complex) \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (- ((inverse x)\<^sup>2))"
unfolding numeral_2_eq_2
by (rule DERIV_inverse)
@@ -166,13 +166,13 @@
lemma CDERIV_inverse_fun:
"[| DERIV f x :> d; f(x) \<noteq> (0::complex) |]
- ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"
+ ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse ((f x)\<^sup>2)))"
unfolding numeral_2_eq_2
by (rule DERIV_inverse_fun)
lemma NSCDERIV_inverse_fun:
"[| NSDERIV f x :> d; f(x) \<noteq> (0::complex) |]
- ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"
+ ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse ((f x)\<^sup>2)))"
unfolding numeral_2_eq_2
by (rule NSDERIV_inverse_fun)
@@ -181,13 +181,13 @@
lemma CDERIV_quotient:
"[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> (0::complex) |]
- ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)"
+ ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / ((g x)\<^sup>2)"
unfolding numeral_2_eq_2
by (rule DERIV_quotient)
lemma NSCDERIV_quotient:
"[| NSDERIV f x :> d; NSDERIV g x :> e; g(x) \<noteq> (0::complex) |]
- ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)"
+ ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / ((g x)\<^sup>2)"
unfolding numeral_2_eq_2
by (rule NSDERIV_quotient)
--- a/src/HOL/NSA/HTranscendental.thy Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/NSA/HTranscendental.thy Sun Aug 18 19:59:19 2013 +0200
@@ -103,7 +103,7 @@
lemma hypreal_sqrt_ge_zero: "0 \<le> x ==> 0 \<le> ( *f* sqrt)(x)"
by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less)
-lemma hypreal_sqrt_hrabs [simp]: "!!x. ( *f* sqrt)(x ^ 2) = abs(x)"
+lemma hypreal_sqrt_hrabs [simp]: "!!x. ( *f* sqrt)(x\<^sup>2) = abs(x)"
by (transfer, simp)
lemma hypreal_sqrt_hrabs2 [simp]: "!!x. ( *f* sqrt)(x*x) = abs(x)"
@@ -128,7 +128,7 @@
apply (auto simp add: st_hrabs st_zero_le star_sqrt_HFinite)
done
-lemma hypreal_sqrt_sum_squares_ge1 [simp]: "!!x y. x \<le> ( *f* sqrt)(x ^ 2 + y ^ 2)"
+lemma hypreal_sqrt_sum_squares_ge1 [simp]: "!!x y. x \<le> ( *f* sqrt)(x\<^sup>2 + y\<^sup>2)"
by transfer (rule real_sqrt_sum_squares_ge1)
lemma HFinite_hypreal_sqrt:
@@ -584,14 +584,14 @@
text{*A familiar approximation to @{term "cos x"} when @{term x} is small*}
lemma STAR_cos_Infinitesimal_approx:
- "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - x ^ 2"
+ "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - x\<^sup>2"
apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
apply (auto simp add: Infinitesimal_approx_minus [symmetric]
diff_minus add_assoc [symmetric] numeral_2_eq_2)
done
lemma STAR_cos_Infinitesimal_approx2:
- "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - (x ^ 2)/2"
+ "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - (x\<^sup>2)/2"
apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
apply (auto intro: Infinitesimal_SReal_divide
simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2)
--- a/src/HOL/NSA/NSComplex.thy Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/NSA/NSComplex.thy Sun Aug 18 19:59:19 2013 +0200
@@ -325,7 +325,7 @@
by transfer (rule complex_cnj_zero_iff)
lemma hcomplex_mult_hcnj:
- "!!z. z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)"
+ "!!z. z * hcnj z = hcomplex_of_hypreal ((hRe z)\<^sup>2 + (hIm z)\<^sup>2)"
by transfer (rule complex_mult_cnj)
@@ -339,7 +339,7 @@
"hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n"
by simp
-lemma hcmod_mult_hcnj: "!!z. hcmod(z * hcnj(z)) = hcmod(z) ^ 2"
+lemma hcmod_mult_hcnj: "!!z. hcmod(z * hcnj(z)) = (hcmod z)\<^sup>2"
by transfer (rule complex_mod_mult_cnj)
lemma hcmod_triangle_ineq2 [simp]:
@@ -358,7 +358,7 @@
lemma hcomplexpow_Suc [simp]: "z ^ (Suc n) = (z::hcomplex) * (z ^ n)"
by (rule power_Suc)
-lemma hcomplexpow_i_squared [simp]: "iii ^ 2 = -1"
+lemma hcomplexpow_i_squared [simp]: "iii\<^sup>2 = -1"
by transfer (rule power2_i)
lemma hcomplex_of_hypreal_pow:
@@ -405,7 +405,7 @@
lemma hsgn_eq: "!!z. hsgn z = z / hcomplex_of_hypreal (hcmod z)"
by transfer (rule sgn_eq)
-lemma hcmod_i: "!!x y. hcmod (HComplex x y) = ( *f* sqrt) (x ^ 2 + y ^ 2)"
+lemma hcmod_i: "!!x y. hcmod (HComplex x y) = ( *f* sqrt) (x\<^sup>2 + y\<^sup>2)"
by transfer (rule complex_norm)
lemma hcomplex_eq_cancel_iff1 [simp]:
@@ -435,8 +435,7 @@
by transfer (rule Im_sgn)
lemma HComplex_inverse:
- "!!x y. inverse (HComplex x y) =
- HComplex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"
+ "!!x y. inverse (HComplex x y) = HComplex (x/(x\<^sup>2 + y\<^sup>2)) (-y/(x\<^sup>2 + y\<^sup>2))"
by transfer (rule complex_inverse)
lemma hRe_mult_i_eq[simp]:
--- a/src/HOL/Number_Theory/Fib.thy Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Number_Theory/Fib.thy Sun Aug 18 19:59:19 2013 +0200
@@ -169,24 +169,24 @@
*}
lemma fib_Cassini_aux_int: "fib (int n + 2) * fib (int n) -
- (fib (int n + 1))^2 = (-1)^(n + 1)"
+ (fib (int n + 1))\<^sup>2 = (-1)^(n + 1)"
apply (induct n)
apply (auto simp add: field_simps power2_eq_square fib_reduce_int power_add)
done
lemma fib_Cassini_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n -
- (fib (n + 1))^2 = (-1)^(nat n + 1)"
+ (fib (n + 1))\<^sup>2 = (-1)^(nat n + 1)"
by (insert fib_Cassini_aux_int [of "nat n"], auto)
(*
lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n =
- (fib (n + 1))^2 + (-1)^(nat n + 1)"
+ (fib (n + 1))\<^sup>2 + (-1)^(nat n + 1)"
by (frule fib_Cassini_int, simp)
*)
lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib ((n::int) + 2) * fib n =
- (if even n then tsub ((fib (n + 1))^2) 1
- else (fib (n + 1))^2 + 1)"
+ (if even n then tsub ((fib (n + 1))\<^sup>2) 1
+ else (fib (n + 1))\<^sup>2 + 1)"
apply (frule fib_Cassini_int, auto simp add: pos_int_even_equiv_nat_even)
apply (subst tsub_eq)
apply (insert fib_gr_0_int [of "n + 1"], force)
@@ -194,8 +194,8 @@
done
lemma fib_Cassini_nat: "fib ((n::nat) + 2) * fib n =
- (if even n then (fib (n + 1))^2 - 1
- else (fib (n + 1))^2 + 1)"
+ (if even n then (fib (n + 1))\<^sup>2 - 1
+ else (fib (n + 1))\<^sup>2 + 1)"
by (rule fib_Cassini'_int [transferred, of n], auto)
--- a/src/HOL/Old_Number_Theory/Euler.thy Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Old_Number_Theory/Euler.thy Sun Aug 18 19:59:19 2013 +0200
@@ -75,7 +75,7 @@
from this and a show ?thesis
by (auto simp add: zcong_zmult_prop2)
qed
- then have "[j^2 = a] (mod p)" by (simp add: power2_eq_square)
+ then have "[j\<^sup>2 = a] (mod p)" by (simp add: power2_eq_square)
with assms show False by (simp add: QuadRes_def)
qed
@@ -269,7 +269,7 @@
text {* \medskip Prove the final part of Euler's Criterion: *}
-lemma aux__1: "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> ~(p dvd y)"
+lemma aux__1: "[| ~([x = 0] (mod p)); [y\<^sup>2 = x] (mod p)|] ==> ~(p dvd y)"
by (metis dvdI power2_eq_square zcong_sym zcong_trans zcong_zero_equiv_div dvd_trans)
lemma aux__2: "2 * nat((p - 1) div 2) = nat (2 * ((p - 1) div 2))"
--- a/src/HOL/Old_Number_Theory/EvenOdd.thy Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Old_Number_Theory/EvenOdd.thy Sun Aug 18 19:59:19 2013 +0200
@@ -175,9 +175,9 @@
by (simp add: nat_mult_distrib)
finally have "(-1::int)^nat x = (-1)^(2 * nat a)"
by simp
- also have "... = ((-1::int)^2)^ (nat a)"
+ also have "... = (-1::int)\<^sup>2 ^ nat a"
by (simp add: zpower_zpower [symmetric])
- also have "(-1::int)^2 = 1"
+ also have "(-1::int)\<^sup>2 = 1"
by simp
finally show ?thesis
by simp
@@ -192,11 +192,11 @@
by simp
also from a have "nat (2 * a + 1) = 2 * nat a + 1"
by (auto simp add: nat_mult_distrib nat_add_distrib)
- finally have "(-1::int)^nat x = (-1)^(2 * nat a + 1)"
+ finally have "(-1::int) ^ nat x = (-1)^(2 * nat a + 1)"
by simp
- also have "... = ((-1::int)^2)^ (nat a) * (-1)^1"
+ also have "... = ((-1::int)\<^sup>2) ^ nat a * (-1)^1"
by (auto simp add: power_mult power_add)
- also have "(-1::int)^2 = 1"
+ also have "(-1::int)\<^sup>2 = 1"
by simp
finally show ?thesis
by simp
--- a/src/HOL/Old_Number_Theory/Pocklington.thy Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy Sun Aug 18 19:59:19 2013 +0200
@@ -940,32 +940,32 @@
qed
lemma prime_divisor_sqrt:
- "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d^2 \<le> n \<longrightarrow> d = 1)"
+ "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d\<^sup>2 \<le> n \<longrightarrow> d = 1)"
proof-
{assume "n=0 \<or> n=1" hence ?thesis using prime_0 prime_1
by (auto simp add: nat_power_eq_0_iff)}
moreover
{assume n: "n\<noteq>0" "n\<noteq>1"
hence np: "n > 1" by arith
- {fix d assume d: "d dvd n" "d^2 \<le> n" and H: "\<forall>m. m dvd n \<longrightarrow> m=1 \<or> m=n"
+ {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"
from H d have d1n: "d = 1 \<or> d=n" by blast
{assume dn: "d=n"
- have "n^2 > n*1" using n by (simp add: power2_eq_square)
+ have "n\<^sup>2 > n*1" using n by (simp add: power2_eq_square)
with dn d(2) have "d=1" by simp}
with d1n have "d = 1" by blast }
moreover
- {fix d assume d: "d dvd n" and H: "\<forall>d'. d' dvd n \<and> d'^2 \<le> n \<longrightarrow> d' = 1"
+ {fix d assume d: "d dvd n" and H: "\<forall>d'. d' dvd n \<and> d'\<^sup>2 \<le> n \<longrightarrow> d' = 1"
from d n have "d \<noteq> 0" apply - apply (rule ccontr) by simp
hence dp: "d > 0" by simp
from d[unfolded dvd_def] obtain e where e: "n= d*e" by blast
from n dp e have ep:"e > 0" by simp
- have "d^2 \<le> n \<or> e^2 \<le> n" using dp ep
+ have "d\<^sup>2 \<le> n \<or> e\<^sup>2 \<le> n" using dp ep
by (auto simp add: e power2_eq_square mult_le_cancel_left)
moreover
- {assume h: "d^2 \<le> n"
+ {assume h: "d\<^sup>2 \<le> n"
from H[rule_format, of d] h d have "d = 1" by blast}
moreover
- {assume h: "e^2 \<le> n"
+ {assume h: "e\<^sup>2 \<le> n"
from e have "e dvd n" unfolding dvd_def by (simp add: mult_commute)
with H[rule_format, of e] h have "e=1" by simp
with e have "d = n" by simp}
@@ -974,7 +974,7 @@
ultimately show ?thesis by auto
qed
lemma prime_prime_factor_sqrt:
- "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)"
+ "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)"
(is "?lhs \<longleftrightarrow>?rhs")
proof-
{assume "n=0 \<or> n=1" hence ?thesis using prime_0 prime_1 by auto}
@@ -990,14 +990,14 @@
}
moreover
{assume H: ?rhs
- {fix d assume d: "d dvd n" "d^2 \<le> n" "d\<noteq>1"
+ {fix d assume d: "d dvd n" "d\<^sup>2 \<le> n" "d\<noteq>1"
from prime_factor[OF d(3)]
obtain p where p: "prime p" "p dvd d" by blast
from n have np: "n > 0" by arith
from d(1) n have "d \<noteq> 0" by - (rule ccontr, auto)
hence dp: "d > 0" by arith
from mult_mono[OF dvd_imp_le[OF p(2) dp] dvd_imp_le[OF p(2) dp]] d(2)
- have "p^2 \<le> n" unfolding power2_eq_square by arith
+ have "p\<^sup>2 \<le> n" unfolding power2_eq_square by arith
with H n p(1) dvd_trans[OF p(2) d(1)] have False by blast}
with n prime_divisor_sqrt have ?lhs by auto}
ultimately have ?thesis by blast }
@@ -1073,7 +1073,7 @@
qed
lemma pocklington:
- assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q^2"
+ assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q\<^sup>2"
and an: "[a^ (n - 1) = 1] (mod n)"
and aq:"\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n - 1) div p) - 1) n"
shows "prime n"
@@ -1081,7 +1081,7 @@
proof-
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)"
from n have n01: "n\<noteq>0" "n\<noteq>1" by arith+
- {fix p assume p: "prime p" "p dvd n" "p^2 \<le> n"
+ {fix p assume p: "prime p" "p dvd n" "p\<^sup>2 \<le> n"
from p(3) sqr have "p^(Suc 1) \<le> q^(Suc 1)" by (simp add: power2_eq_square)
hence pq: "p \<le> q" unfolding exp_mono_le .
from pocklington_lemma[OF n nqr an aq p(1,2)] cong_1_divides
@@ -1093,7 +1093,7 @@
(* Variant for application, to separate the exponentiation. *)
lemma pocklington_alt:
- assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q^2"
+ assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q\<^sup>2"
and an: "[a^ (n - 1) = 1] (mod n)"
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)"
shows "prime n"
@@ -1205,7 +1205,7 @@
lemma pocklington_primefact:
- assumes n: "n \<ge> 2" and qrn: "q*r = n - 1" and nq2: "n \<le> q^2"
+ assumes n: "n \<ge> 2" and qrn: "q*r = n - 1" and nq2: "n \<le> q\<^sup>2"
and arnb: "(a^r) mod n = b" and psq: "foldr op * ps 1 = q"
and bqn: "(b^q) mod n = 1"
and psp: "list_all (\<lambda>p. prime p \<and> coprime ((b^(q div p)) mod n - 1) n) ps"
--- a/src/HOL/Old_Number_Theory/Primes.thy Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Old_Number_Theory/Primes.thy Sun Aug 18 19:59:19 2013 +0200
@@ -56,39 +56,39 @@
using power_inject_base[of x n y] by auto
-lemma even_square: assumes e: "even (n::nat)" shows "\<exists>x. n ^ 2 = 4*x"
+lemma even_square: assumes e: "even (n::nat)" shows "\<exists>x. n\<^sup>2 = 4*x"
proof-
from e have "2 dvd n" by presburger
then obtain k where k: "n = 2*k" using dvd_def by auto
- hence "n^2 = 4* (k^2)" by (simp add: power2_eq_square)
+ hence "n\<^sup>2 = 4 * k\<^sup>2" by (simp add: power2_eq_square)
thus ?thesis by blast
qed
-lemma odd_square: assumes e: "odd (n::nat)" shows "\<exists>x. n ^ 2 = 4*x + 1"
+lemma odd_square: assumes e: "odd (n::nat)" shows "\<exists>x. n\<^sup>2 = 4*x + 1"
proof-
from e have np: "n > 0" by presburger
from e have "2 dvd (n - 1)" by presburger
then obtain k where "n - 1 = 2*k" using dvd_def by auto
hence k: "n = 2*k + 1" using e by presburger
- hence "n^2 = 4* (k^2 + k) + 1" by algebra
+ hence "n\<^sup>2 = 4* (k\<^sup>2 + k) + 1" by algebra
thus ?thesis by blast
qed
-lemma diff_square: "(x::nat)^2 - y^2 = (x+y)*(x - y)"
+lemma diff_square: "(x::nat)\<^sup>2 - y\<^sup>2 = (x+y)*(x - y)"
proof-
have "x \<le> y \<or> y \<le> x" by (rule nat_le_linear)
moreover
{assume le: "x \<le> y"
- hence "x ^2 \<le> y^2" by (simp only: numeral_2_eq_2 exp_mono_le Let_def)
+ hence "x\<^sup>2 \<le> y\<^sup>2" by (simp only: numeral_2_eq_2 exp_mono_le Let_def)
with le have ?thesis by simp }
moreover
{assume le: "y \<le> x"
- hence le2: "y ^2 \<le> x^2" by (simp only: numeral_2_eq_2 exp_mono_le Let_def)
+ hence le2: "y\<^sup>2 \<le> x\<^sup>2" by (simp only: numeral_2_eq_2 exp_mono_le Let_def)
from le have "\<exists>z. y + z = x" by presburger
then obtain z where z: "x = y + z" by blast
- from le2 have "\<exists>z. x^2 = y^2 + z" by presburger
- then obtain z2 where z2: "x^2 = y^2 + z2" by blast
- from z z2 have ?thesis apply simp by algebra }
+ from le2 have "\<exists>z. x\<^sup>2 = y\<^sup>2 + z" by presburger
+ then obtain z2 where z2: "x\<^sup>2 = y\<^sup>2 + z2" by blast
+ from z z2 have ?thesis by simp algebra }
ultimately show ?thesis by blast
qed
@@ -544,29 +544,29 @@
from g(2,3) dvd_trans[OF p(2)] p(1) show ?thesis by auto
qed
lemma coprime_sos: assumes xy: "coprime x y"
- shows "coprime (x * y) (x^2 + y^2)"
+ shows "coprime (x * y) (x\<^sup>2 + y\<^sup>2)"
proof-
- {assume c: "\<not> coprime (x * y) (x^2 + y^2)"
+ {assume c: "\<not> coprime (x * y) (x\<^sup>2 + y\<^sup>2)"
from coprime_prime_dvd_ex[OF c] obtain p
- where p: "prime p" "p dvd x*y" "p dvd x^2 + y^2" by blast
+ where p: "prime p" "p dvd x*y" "p dvd x\<^sup>2 + y\<^sup>2" by blast
{assume px: "p dvd x"
from dvd_mult[OF px, of x] p(3)
- obtain r s where "x * x = p * r" and "x^2 + y^2 = p * s"
+ obtain r s where "x * x = p * r" and "x\<^sup>2 + y\<^sup>2 = p * s"
by (auto elim!: dvdE)
- then have "y^2 = p * (s - r)"
+ then have "y\<^sup>2 = p * (s - r)"
by (auto simp add: power2_eq_square diff_mult_distrib2)
- then have "p dvd y^2" ..
+ then have "p dvd y\<^sup>2" ..
with prime_divexp[OF p(1), of y 2] have py: "p dvd y" .
from p(1) px py xy[unfolded coprime, rule_format, of p] prime_1
have False by simp }
moreover
{assume py: "p dvd y"
from dvd_mult[OF py, of y] p(3)
- obtain r s where "y * y = p * r" and "x^2 + y^2 = p * s"
+ obtain r s where "y * y = p * r" and "x\<^sup>2 + y\<^sup>2 = p * s"
by (auto elim!: dvdE)
- then have "x^2 = p * (s - r)"
+ then have "x\<^sup>2 = p * (s - r)"
by (auto simp add: power2_eq_square diff_mult_distrib2)
- then have "p dvd x^2" ..
+ then have "p dvd x\<^sup>2" ..
with prime_divexp[OF p(1), of x 2] have px: "p dvd x" .
from p(1) px py xy[unfolded coprime, rule_format, of p] prime_1
have False by simp }
--- a/src/HOL/Old_Number_Theory/Residues.thy Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Old_Number_Theory/Residues.thy Sun Aug 18 19:59:19 2013 +0200
@@ -19,7 +19,7 @@
where "StandardRes m x = x mod m"
definition QuadRes :: "int => int => bool"
- where "QuadRes m x = (\<exists>y. ([(y ^ 2) = x] (mod m)))"
+ where "QuadRes m x = (\<exists>y. ([y\<^sup>2 = x] (mod m)))"
definition Legendre :: "int => int => int" where
"Legendre a p = (if ([a = 0] (mod p)) then 0
--- a/src/HOL/Probability/Distributions.thy Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Probability/Distributions.thy Sun Aug 18 19:59:19 2013 +0200
@@ -372,7 +372,7 @@
also have "(\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel) = (a + b) / 2"
proof (subst integral_FTC_atLeastAtMost)
fix x
- show "DERIV (\<lambda>x. x ^ 2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}"
+ show "DERIV (\<lambda>x. x\<^sup>2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}"
using uniform_distributed_params[OF D]
by (auto intro!: DERIV_intros)
show "isCont (\<lambda>x. x / Sigma_Algebra.measure lborel {a..b}) x"
--- a/src/HOL/ex/Groebner_Examples.thy Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/ex/Groebner_Examples.thy Sun Aug 18 19:59:19 2013 +0200
@@ -47,8 +47,8 @@
by simp
lemma
- assumes "a * x^2 + b * x + c = (0::int)" and "d * x^2 + e * x + f = 0"
- 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"
+ assumes "a * x\<^sup>2 + b * x + c = (0::int)" and "d * x\<^sup>2 + e * x + f = 0"
+ 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"
using assms by algebra
lemma "(x::int)^3 - x^2 - 5*x - 3 = 0 \<longleftrightarrow> (x = 3 \<or> x = -1)"
@@ -58,8 +58,8 @@
by algebra
lemma
- fixes x::"'a::{idom}"
- shows "x^2*y = x^2 & x*y^2 = y^2 \<longleftrightarrow> x=1 & y=1 | x=0 & y=0"
+ fixes x::"'a::idom"
+ shows "x\<^sup>2*y = x\<^sup>2 & x*y\<^sup>2 = y\<^sup>2 \<longleftrightarrow> x = 1 & y = 1 | x = 0 & y = 0"
by algebra
subsection {* Lemmas for Lagrange's theorem *}