src/HOL/Power.thy
changeset 47192 0c0501cb6da6
parent 47191 ebd8c46d156b
child 47209 4893907fe872
     1.1 --- a/src/HOL/Power.thy	Thu Mar 29 11:47:30 2012 +0200
     1.2 +++ b/src/HOL/Power.thy	Thu Mar 29 14:09:10 2012 +0200
     1.3 @@ -24,6 +24,18 @@
     1.4  notation (HTML output)
     1.5    power ("(_\<^bsup>_\<^esup>)" [1000] 1000)
     1.6  
     1.7 +text {* Special syntax for squares. *}
     1.8 +
     1.9 +abbreviation (xsymbols)
    1.10 +  power2 :: "'a \<Rightarrow> 'a"  ("(_\<twosuperior>)" [1000] 999) where
    1.11 +  "x\<twosuperior> \<equiv> x ^ 2"
    1.12 +
    1.13 +notation (latex output)
    1.14 +  power2  ("(_\<twosuperior>)" [1000] 999)
    1.15 +
    1.16 +notation (HTML output)
    1.17 +  power2  ("(_\<twosuperior>)" [1000] 999)
    1.18 +
    1.19  end
    1.20  
    1.21  context monoid_mult
    1.22 @@ -55,6 +67,20 @@
    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 +  by (simp add: numeral_2_eq_2)
    1.28 +
    1.29 +lemma power3_eq_cube: "a ^ 3 = a * a * a"
    1.30 +  by (simp add: numeral_3_eq_3 mult_assoc)
    1.31 +
    1.32 +lemma power_even_eq:
    1.33 +  "a ^ (2*n) = (a ^ n) ^ 2"
    1.34 +  by (subst mult_commute) (simp add: power_mult)
    1.35 +
    1.36 +lemma power_odd_eq:
    1.37 +  "a ^ Suc (2*n) = a * (a ^ n) ^ 2"
    1.38 +  by (simp add: power_even_eq)
    1.39 +
    1.40  end
    1.41  
    1.42  context comm_monoid_mult
    1.43 @@ -91,6 +117,12 @@
    1.44  lemma power_zero_numeral [simp]: "(0::'a) ^ numeral k = 0"
    1.45    by (cases "numeral k :: nat", simp_all)
    1.46  
    1.47 +lemma zero_power2: "0\<twosuperior> = 0" (* delete? *)
    1.48 +  by (rule power_zero_numeral)
    1.49 +
    1.50 +lemma one_power2: "1\<twosuperior> = 1" (* delete? *)
    1.51 +  by (rule power_one)
    1.52 +
    1.53  end
    1.54  
    1.55  context comm_semiring_1
    1.56 @@ -163,6 +195,87 @@
    1.57    "neg_numeral k ^ numeral (Num.Bit1 l) = neg_numeral (Num.pow k (Num.Bit1 l))"
    1.58    by (simp only: neg_numeral_def power_minus_Bit1 power_numeral pow.simps)
    1.59  
    1.60 +lemma power2_minus [simp]:
    1.61 +  "(- a)\<twosuperior> = a\<twosuperior>"
    1.62 +  by (rule power_minus_Bit0)
    1.63 +
    1.64 +lemma power_minus1_even [simp]:
    1.65 +  "-1 ^ (2*n) = 1"
    1.66 +proof (induct n)
    1.67 +  case 0 show ?case by simp
    1.68 +next
    1.69 +  case (Suc n) then show ?case by (simp add: power_add power2_eq_square)
    1.70 +qed
    1.71 +
    1.72 +lemma power_minus1_odd:
    1.73 +  "-1 ^ Suc (2*n) = -1"
    1.74 +  by simp
    1.75 +
    1.76 +lemma power_minus_even [simp]:
    1.77 +  "(-a) ^ (2*n) = a ^ (2*n)"
    1.78 +  by (simp add: power_minus [of a])
    1.79 +
    1.80 +end
    1.81 +
    1.82 +context ring_1_no_zero_divisors
    1.83 +begin
    1.84 +
    1.85 +lemma field_power_not_zero:
    1.86 +  "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
    1.87 +  by (induct n) auto
    1.88 +
    1.89 +lemma zero_eq_power2 [simp]:
    1.90 +  "a\<twosuperior> = 0 \<longleftrightarrow> a = 0"
    1.91 +  unfolding power2_eq_square by simp
    1.92 +
    1.93 +lemma power2_eq_1_iff:
    1.94 +  "a\<twosuperior> = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"
    1.95 +  unfolding power2_eq_square by (rule square_eq_1_iff)
    1.96 +
    1.97 +end
    1.98 +
    1.99 +context idom
   1.100 +begin
   1.101 +
   1.102 +lemma power2_eq_iff: "x\<twosuperior> = y\<twosuperior> \<longleftrightarrow> x = y \<or> x = - y"
   1.103 +  unfolding power2_eq_square by (rule square_eq_iff)
   1.104 +
   1.105 +end
   1.106 +
   1.107 +context division_ring
   1.108 +begin
   1.109 +
   1.110 +text {* FIXME reorient or rename to @{text nonzero_inverse_power} *}
   1.111 +lemma nonzero_power_inverse:
   1.112 +  "a \<noteq> 0 \<Longrightarrow> inverse (a ^ n) = (inverse a) ^ n"
   1.113 +  by (induct n)
   1.114 +    (simp_all add: nonzero_inverse_mult_distrib power_commutes field_power_not_zero)
   1.115 +
   1.116 +end
   1.117 +
   1.118 +context field
   1.119 +begin
   1.120 +
   1.121 +lemma nonzero_power_divide:
   1.122 +  "b \<noteq> 0 \<Longrightarrow> (a / b) ^ n = a ^ n / b ^ n"
   1.123 +  by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
   1.124 +
   1.125 +end
   1.126 +
   1.127 +
   1.128 +subsection {* Exponentiation on ordered types *}
   1.129 +
   1.130 +context linordered_ring (* TODO: move *)
   1.131 +begin
   1.132 +
   1.133 +lemma sum_squares_ge_zero:
   1.134 +  "0 \<le> x * x + y * y"
   1.135 +  by (intro add_nonneg_nonneg zero_le_square)
   1.136 +
   1.137 +lemma not_sum_squares_lt_zero:
   1.138 +  "\<not> x * x + y * y < 0"
   1.139 +  by (simp add: not_less sum_squares_ge_zero)
   1.140 +
   1.141  end
   1.142  
   1.143  context linordered_semidom
   1.144 @@ -356,6 +469,35 @@
   1.145    "a ^ n = b ^ n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 < n \<Longrightarrow> a = b"
   1.146    by (cases n) (simp_all del: power_Suc, rule power_inject_base)
   1.147  
   1.148 +lemma power2_le_imp_le:
   1.149 +  "x\<twosuperior> \<le> y\<twosuperior> \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y"
   1.150 +  unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
   1.151 +
   1.152 +lemma power2_less_imp_less:
   1.153 +  "x\<twosuperior> < y\<twosuperior> \<Longrightarrow> 0 \<le> y \<Longrightarrow> x < y"
   1.154 +  by (rule power_less_imp_less_base)
   1.155 +
   1.156 +lemma power2_eq_imp_eq:
   1.157 +  "x\<twosuperior> = y\<twosuperior> \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x = y"
   1.158 +  unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base) simp
   1.159 +
   1.160 +end
   1.161 +
   1.162 +context linordered_ring_strict
   1.163 +begin
   1.164 +
   1.165 +lemma sum_squares_eq_zero_iff:
   1.166 +  "x * x + y * y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   1.167 +  by (simp add: add_nonneg_eq_0_iff)
   1.168 +
   1.169 +lemma sum_squares_le_zero_iff:
   1.170 +  "x * x + y * y \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   1.171 +  by (simp add: le_less not_sum_squares_lt_zero sum_squares_eq_zero_iff)
   1.172 +
   1.173 +lemma sum_squares_gt_zero_iff:
   1.174 +  "0 < x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
   1.175 +  by (simp add: not_le [symmetric] sum_squares_le_zero_iff)
   1.176 +
   1.177  end
   1.178  
   1.179  context linordered_idom
   1.180 @@ -381,36 +523,91 @@
   1.181    "0 \<le> abs a ^ n"
   1.182    by (rule zero_le_power [OF abs_ge_zero])
   1.183  
   1.184 -end
   1.185 +lemma zero_le_power2 [simp]:
   1.186 +  "0 \<le> a\<twosuperior>"
   1.187 +  by (simp add: power2_eq_square)
   1.188 +
   1.189 +lemma zero_less_power2 [simp]:
   1.190 +  "0 < a\<twosuperior> \<longleftrightarrow> a \<noteq> 0"
   1.191 +  by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
   1.192 +
   1.193 +lemma power2_less_0 [simp]:
   1.194 +  "\<not> a\<twosuperior> < 0"
   1.195 +  by (force simp add: power2_eq_square mult_less_0_iff)
   1.196 +
   1.197 +lemma abs_power2 [simp]:
   1.198 +  "abs (a\<twosuperior>) = a\<twosuperior>"
   1.199 +  by (simp add: power2_eq_square abs_mult abs_mult_self)
   1.200 +
   1.201 +lemma power2_abs [simp]:
   1.202 +  "(abs a)\<twosuperior> = a\<twosuperior>"
   1.203 +  by (simp add: power2_eq_square abs_mult_self)
   1.204 +
   1.205 +lemma odd_power_less_zero:
   1.206 +  "a < 0 \<Longrightarrow> a ^ Suc (2*n) < 0"
   1.207 +proof (induct n)
   1.208 +  case 0
   1.209 +  then show ?case by simp
   1.210 +next
   1.211 +  case (Suc n)
   1.212 +  have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
   1.213 +    by (simp add: mult_ac power_add power2_eq_square)
   1.214 +  thus ?case
   1.215 +    by (simp del: power_Suc add: Suc mult_less_0_iff mult_neg_neg)
   1.216 +qed
   1.217  
   1.218 -context ring_1_no_zero_divisors
   1.219 -begin
   1.220 +lemma odd_0_le_power_imp_0_le:
   1.221 +  "0 \<le> a ^ Suc (2*n) \<Longrightarrow> 0 \<le> a"
   1.222 +  using odd_power_less_zero [of a n]
   1.223 +    by (force simp add: linorder_not_less [symmetric]) 
   1.224 +
   1.225 +lemma zero_le_even_power'[simp]:
   1.226 +  "0 \<le> a ^ (2*n)"
   1.227 +proof (induct n)
   1.228 +  case 0
   1.229 +    show ?case by simp
   1.230 +next
   1.231 +  case (Suc n)
   1.232 +    have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" 
   1.233 +      by (simp add: mult_ac power_add power2_eq_square)
   1.234 +    thus ?case
   1.235 +      by (simp add: Suc zero_le_mult_iff)
   1.236 +qed
   1.237  
   1.238 -lemma field_power_not_zero:
   1.239 -  "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
   1.240 -  by (induct n) auto
   1.241 +lemma sum_power2_ge_zero:
   1.242 +  "0 \<le> x\<twosuperior> + y\<twosuperior>"
   1.243 +  by (intro add_nonneg_nonneg zero_le_power2)
   1.244 +
   1.245 +lemma not_sum_power2_lt_zero:
   1.246 +  "\<not> x\<twosuperior> + y\<twosuperior> < 0"
   1.247 +  unfolding not_less by (rule sum_power2_ge_zero)
   1.248 +
   1.249 +lemma sum_power2_eq_zero_iff:
   1.250 +  "x\<twosuperior> + y\<twosuperior> = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   1.251 +  unfolding power2_eq_square by (simp add: add_nonneg_eq_0_iff)
   1.252 +
   1.253 +lemma sum_power2_le_zero_iff:
   1.254 +  "x\<twosuperior> + y\<twosuperior> \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   1.255 +  by (simp add: le_less sum_power2_eq_zero_iff not_sum_power2_lt_zero)
   1.256 +
   1.257 +lemma sum_power2_gt_zero_iff:
   1.258 +  "0 < x\<twosuperior> + y\<twosuperior> \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
   1.259 +  unfolding not_le [symmetric] by (simp add: sum_power2_le_zero_iff)
   1.260  
   1.261  end
   1.262  
   1.263 -context division_ring
   1.264 -begin
   1.265  
   1.266 -text {* FIXME reorient or rename to @{text nonzero_inverse_power} *}
   1.267 -lemma nonzero_power_inverse:
   1.268 -  "a \<noteq> 0 \<Longrightarrow> inverse (a ^ n) = (inverse a) ^ n"
   1.269 -  by (induct n)
   1.270 -    (simp_all add: nonzero_inverse_mult_distrib power_commutes field_power_not_zero)
   1.271 +subsection {* Miscellaneous rules *}
   1.272  
   1.273 -end
   1.274 -
   1.275 -context field
   1.276 -begin
   1.277 +lemma power2_sum:
   1.278 +  fixes x y :: "'a::comm_semiring_1"
   1.279 +  shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
   1.280 +  by (simp add: algebra_simps power2_eq_square mult_2_right)
   1.281  
   1.282 -lemma nonzero_power_divide:
   1.283 -  "b \<noteq> 0 \<Longrightarrow> (a / b) ^ n = a ^ n / b ^ n"
   1.284 -  by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
   1.285 -
   1.286 -end
   1.287 +lemma power2_diff:
   1.288 +  fixes x y :: "'a::comm_ring_1"
   1.289 +  shows "(x - y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> - 2 * x * y"
   1.290 +  by (simp add: ring_distribs power2_eq_square mult_2) (rule mult_commute)
   1.291  
   1.292  lemma power_0_Suc [simp]:
   1.293    "(0::'a::{power, semiring_0}) ^ Suc n = 0"