src/HOL/Power.thy
changeset 53015 a1119cf551e8
parent 52435 6646bb548c6b
child 53076 47c9aff07725
     1.1 --- a/src/HOL/Power.thy	Tue Aug 13 14:20:22 2013 +0200
     1.2 +++ b/src/HOL/Power.thy	Tue Aug 13 16:25:47 2013 +0200
     1.3 @@ -27,14 +27,14 @@
     1.4  text {* Special syntax for squares. *}
     1.5  
     1.6  abbreviation (xsymbols)
     1.7 -  power2 :: "'a \<Rightarrow> 'a"  ("(_\<twosuperior>)" [1000] 999) where
     1.8 -  "x\<twosuperior> \<equiv> x ^ 2"
     1.9 +  power2 :: "'a \<Rightarrow> 'a"  ("(_\<^sup>2)" [1000] 999) where
    1.10 +  "x\<^sup>2 \<equiv> x ^ 2"
    1.11  
    1.12  notation (latex output)
    1.13 -  power2  ("(_\<twosuperior>)" [1000] 999)
    1.14 +  power2  ("(_\<^sup>2)" [1000] 999)
    1.15  
    1.16  notation (HTML output)
    1.17 -  power2  ("(_\<twosuperior>)" [1000] 999)
    1.18 +  power2  ("(_\<^sup>2)" [1000] 999)
    1.19  
    1.20  end
    1.21  
    1.22 @@ -67,7 +67,7 @@
    1.23    "a ^ (m * n) = (a ^ m) ^ n"
    1.24    by (induct n) (simp_all add: power_add)
    1.25  
    1.26 -lemma power2_eq_square: "a\<twosuperior> = a * a"
    1.27 +lemma power2_eq_square: "a\<^sup>2 = a * a"
    1.28    by (simp add: numeral_2_eq_2)
    1.29  
    1.30  lemma power3_eq_cube: "a ^ 3 = a * a * a"
    1.31 @@ -139,10 +139,10 @@
    1.32  lemma power_zero_numeral [simp]: "(0::'a) ^ numeral k = 0"
    1.33    by (simp add: numeral_eq_Suc)
    1.34  
    1.35 -lemma zero_power2: "0\<twosuperior> = 0" (* delete? *)
    1.36 +lemma zero_power2: "0\<^sup>2 = 0" (* delete? *)
    1.37    by (rule power_zero_numeral)
    1.38  
    1.39 -lemma one_power2: "1\<twosuperior> = 1" (* delete? *)
    1.40 +lemma one_power2: "1\<^sup>2 = 1" (* delete? *)
    1.41    by (rule power_one)
    1.42  
    1.43  end
    1.44 @@ -218,7 +218,7 @@
    1.45    by (simp only: neg_numeral_def power_minus_Bit1 power_numeral pow.simps)
    1.46  
    1.47  lemma power2_minus [simp]:
    1.48 -  "(- a)\<twosuperior> = a\<twosuperior>"
    1.49 +  "(- a)\<^sup>2 = a\<^sup>2"
    1.50    by (rule power_minus_Bit0)
    1.51  
    1.52  lemma power_minus1_even [simp]:
    1.53 @@ -247,11 +247,11 @@
    1.54    by (induct n) auto
    1.55  
    1.56  lemma zero_eq_power2 [simp]:
    1.57 -  "a\<twosuperior> = 0 \<longleftrightarrow> a = 0"
    1.58 +  "a\<^sup>2 = 0 \<longleftrightarrow> a = 0"
    1.59    unfolding power2_eq_square by simp
    1.60  
    1.61  lemma power2_eq_1_iff:
    1.62 -  "a\<twosuperior> = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"
    1.63 +  "a\<^sup>2 = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"
    1.64    unfolding power2_eq_square by (rule square_eq_1_iff)
    1.65  
    1.66  end
    1.67 @@ -259,7 +259,7 @@
    1.68  context idom
    1.69  begin
    1.70  
    1.71 -lemma power2_eq_iff: "x\<twosuperior> = y\<twosuperior> \<longleftrightarrow> x = y \<or> x = - y"
    1.72 +lemma power2_eq_iff: "x\<^sup>2 = y\<^sup>2 \<longleftrightarrow> x = y \<or> x = - y"
    1.73    unfolding power2_eq_square by (rule square_eq_iff)
    1.74  
    1.75  end
    1.76 @@ -489,15 +489,15 @@
    1.77    by (cases n) (simp_all del: power_Suc, rule power_inject_base)
    1.78  
    1.79  lemma power2_le_imp_le:
    1.80 -  "x\<twosuperior> \<le> y\<twosuperior> \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y"
    1.81 +  "x\<^sup>2 \<le> y\<^sup>2 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y"
    1.82    unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
    1.83  
    1.84  lemma power2_less_imp_less:
    1.85 -  "x\<twosuperior> < y\<twosuperior> \<Longrightarrow> 0 \<le> y \<Longrightarrow> x < y"
    1.86 +  "x\<^sup>2 < y\<^sup>2 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x < y"
    1.87    by (rule power_less_imp_less_base)
    1.88  
    1.89  lemma power2_eq_imp_eq:
    1.90 -  "x\<twosuperior> = y\<twosuperior> \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x = y"
    1.91 +  "x\<^sup>2 = y\<^sup>2 \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x = y"
    1.92    unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base) simp
    1.93  
    1.94  end
    1.95 @@ -543,23 +543,23 @@
    1.96    by (rule zero_le_power [OF abs_ge_zero])
    1.97  
    1.98  lemma zero_le_power2 [simp]:
    1.99 -  "0 \<le> a\<twosuperior>"
   1.100 +  "0 \<le> a\<^sup>2"
   1.101    by (simp add: power2_eq_square)
   1.102  
   1.103  lemma zero_less_power2 [simp]:
   1.104 -  "0 < a\<twosuperior> \<longleftrightarrow> a \<noteq> 0"
   1.105 +  "0 < a\<^sup>2 \<longleftrightarrow> a \<noteq> 0"
   1.106    by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
   1.107  
   1.108  lemma power2_less_0 [simp]:
   1.109 -  "\<not> a\<twosuperior> < 0"
   1.110 +  "\<not> a\<^sup>2 < 0"
   1.111    by (force simp add: power2_eq_square mult_less_0_iff)
   1.112  
   1.113  lemma abs_power2 [simp]:
   1.114 -  "abs (a\<twosuperior>) = a\<twosuperior>"
   1.115 +  "abs (a\<^sup>2) = a\<^sup>2"
   1.116    by (simp add: power2_eq_square abs_mult abs_mult_self)
   1.117  
   1.118  lemma power2_abs [simp]:
   1.119 -  "(abs a)\<twosuperior> = a\<twosuperior>"
   1.120 +  "(abs a)\<^sup>2 = a\<^sup>2"
   1.121    by (simp add: power2_eq_square abs_mult_self)
   1.122  
   1.123  lemma odd_power_less_zero:
   1.124 @@ -594,23 +594,23 @@
   1.125  qed
   1.126  
   1.127  lemma sum_power2_ge_zero:
   1.128 -  "0 \<le> x\<twosuperior> + y\<twosuperior>"
   1.129 +  "0 \<le> x\<^sup>2 + y\<^sup>2"
   1.130    by (intro add_nonneg_nonneg zero_le_power2)
   1.131  
   1.132  lemma not_sum_power2_lt_zero:
   1.133 -  "\<not> x\<twosuperior> + y\<twosuperior> < 0"
   1.134 +  "\<not> x\<^sup>2 + y\<^sup>2 < 0"
   1.135    unfolding not_less by (rule sum_power2_ge_zero)
   1.136  
   1.137  lemma sum_power2_eq_zero_iff:
   1.138 -  "x\<twosuperior> + y\<twosuperior> = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   1.139 +  "x\<^sup>2 + y\<^sup>2 = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   1.140    unfolding power2_eq_square by (simp add: add_nonneg_eq_0_iff)
   1.141  
   1.142  lemma sum_power2_le_zero_iff:
   1.143 -  "x\<twosuperior> + y\<twosuperior> \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   1.144 +  "x\<^sup>2 + y\<^sup>2 \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   1.145    by (simp add: le_less sum_power2_eq_zero_iff not_sum_power2_lt_zero)
   1.146  
   1.147  lemma sum_power2_gt_zero_iff:
   1.148 -  "0 < x\<twosuperior> + y\<twosuperior> \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
   1.149 +  "0 < x\<^sup>2 + y\<^sup>2 \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
   1.150    unfolding not_le [symmetric] by (simp add: sum_power2_le_zero_iff)
   1.151  
   1.152  end
   1.153 @@ -623,12 +623,12 @@
   1.154  
   1.155  lemma power2_sum:
   1.156    fixes x y :: "'a::comm_semiring_1"
   1.157 -  shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
   1.158 +  shows "(x + y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 + 2 * x * y"
   1.159    by (simp add: algebra_simps power2_eq_square mult_2_right)
   1.160  
   1.161  lemma power2_diff:
   1.162    fixes x y :: "'a::comm_ring_1"
   1.163 -  shows "(x - y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> - 2 * x * y"
   1.164 +  shows "(x - y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 - 2 * x * y"
   1.165    by (simp add: ring_distribs power2_eq_square mult_2) (rule mult_commute)
   1.166  
   1.167  lemma power_0_Suc [simp]:
   1.168 @@ -723,12 +723,12 @@
   1.169  
   1.170  lemma power2_nat_le_eq_le:
   1.171    fixes m n :: nat
   1.172 -  shows "m\<twosuperior> \<le> n\<twosuperior> \<longleftrightarrow> m \<le> n"
   1.173 +  shows "m\<^sup>2 \<le> n\<^sup>2 \<longleftrightarrow> m \<le> n"
   1.174    by (auto intro: power2_le_imp_le power_mono)
   1.175  
   1.176  lemma power2_nat_le_imp_le:
   1.177    fixes m n :: nat
   1.178 -  assumes "m\<twosuperior> \<le> n"
   1.179 +  assumes "m\<^sup>2 \<le> n"
   1.180    shows "m \<le> n"
   1.181    using assms by (cases m) (simp_all add: power2_eq_square)
   1.182