src/HOL/Nat_Numeral.thy
changeset 31014 79f0858d9d49
parent 31002 bc4117fe72ab
child 31034 736f521ad036
     1.1 --- a/src/HOL/Nat_Numeral.thy	Tue Apr 28 13:34:48 2009 +0200
     1.2 +++ b/src/HOL/Nat_Numeral.thy	Tue Apr 28 15:50:29 2009 +0200
     1.3 @@ -10,6 +10,8 @@
     1.4  uses ("Tools/nat_simprocs.ML")
     1.5  begin
     1.6  
     1.7 +subsection {* Numerals for natural numbers *}
     1.8 +
     1.9  text {*
    1.10    Arithmetic for naturals is reduced to that for the non-negative integers.
    1.11  *}
    1.12 @@ -28,7 +30,16 @@
    1.13    "nat (number_of v) = number_of v"
    1.14    unfolding nat_number_of_def ..
    1.15  
    1.16 -context recpower
    1.17 +
    1.18 +subsection {* Special case: squares and cubes *}
    1.19 +
    1.20 +lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
    1.21 +  by (simp add: nat_number_of_def)
    1.22 +
    1.23 +lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))"
    1.24 +  by (simp add: nat_number_of_def)
    1.25 +
    1.26 +context power
    1.27  begin
    1.28  
    1.29  abbreviation (xsymbols)
    1.30 @@ -43,6 +54,205 @@
    1.31  
    1.32  end
    1.33  
    1.34 +context monoid_mult
    1.35 +begin
    1.36 +
    1.37 +lemma power2_eq_square: "a\<twosuperior> = a * a"
    1.38 +  by (simp add: numeral_2_eq_2)
    1.39 +
    1.40 +lemma power3_eq_cube: "a ^ 3 = a * a * a"
    1.41 +  by (simp add: numeral_3_eq_3 mult_assoc)
    1.42 +
    1.43 +lemma power_even_eq:
    1.44 +  "a ^ (2*n) = (a ^ n) ^ 2"
    1.45 +  by (subst OrderedGroup.mult_commute) (simp add: power_mult)
    1.46 +
    1.47 +lemma power_odd_eq:
    1.48 +  "a ^ Suc (2*n) = a * (a ^ n) ^ 2"
    1.49 +  by (simp add: power_even_eq)
    1.50 +
    1.51 +end
    1.52 +
    1.53 +context semiring_1
    1.54 +begin
    1.55 +
    1.56 +lemma zero_power2 [simp]: "0\<twosuperior> = 0"
    1.57 +  by (simp add: power2_eq_square)
    1.58 +
    1.59 +lemma one_power2 [simp]: "1\<twosuperior> = 1"
    1.60 +  by (simp add: power2_eq_square)
    1.61 +
    1.62 +end
    1.63 +
    1.64 +context comm_ring_1
    1.65 +begin
    1.66 +
    1.67 +lemma power2_minus [simp]:
    1.68 +  "(- a)\<twosuperior> = a\<twosuperior>"
    1.69 +  by (simp add: power2_eq_square)
    1.70 +
    1.71 +text{*
    1.72 +  We cannot prove general results about the numeral @{term "-1"},
    1.73 +  so we have to use @{term "- 1"} instead.
    1.74 +*}
    1.75 +
    1.76 +lemma power_minus1_even [simp]:
    1.77 +  "(- 1) ^ (2*n) = 1"
    1.78 +proof (induct n)
    1.79 +  case 0 show ?case by simp
    1.80 +next
    1.81 +  case (Suc n) then show ?case by (simp add: power_add)
    1.82 +qed
    1.83 +
    1.84 +lemma power_minus1_odd:
    1.85 +  "(- 1) ^ Suc (2*n) = - 1"
    1.86 +  by simp
    1.87 +
    1.88 +lemma power_minus_even [simp]:
    1.89 +  "(-a) ^ (2*n) = a ^ (2*n)"
    1.90 +  by (simp add: power_minus [of a]) 
    1.91 +
    1.92 +end
    1.93 +
    1.94 +context ordered_ring_strict
    1.95 +begin
    1.96 +
    1.97 +lemma sum_squares_ge_zero:
    1.98 +  "0 \<le> x * x + y * y"
    1.99 +  by (intro add_nonneg_nonneg zero_le_square)
   1.100 +
   1.101 +lemma not_sum_squares_lt_zero:
   1.102 +  "\<not> x * x + y * y < 0"
   1.103 +  by (simp add: not_less sum_squares_ge_zero)
   1.104 +
   1.105 +lemma sum_squares_eq_zero_iff:
   1.106 +  "x * x + y * y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   1.107 +  by (simp add: sum_nonneg_eq_zero_iff)
   1.108 +
   1.109 +lemma sum_squares_le_zero_iff:
   1.110 +  "x * x + y * y \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   1.111 +  by (simp add: le_less not_sum_squares_lt_zero sum_squares_eq_zero_iff)
   1.112 +
   1.113 +lemma sum_squares_gt_zero_iff:
   1.114 +  "0 < x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
   1.115 +proof -
   1.116 +  have "x * x + y * y \<noteq> 0 \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
   1.117 +    by (simp add: sum_squares_eq_zero_iff)
   1.118 +  then have "0 \<noteq> x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
   1.119 +    by auto
   1.120 +  then show ?thesis
   1.121 +    by (simp add: less_le sum_squares_ge_zero)
   1.122 +qed
   1.123 +
   1.124 +end
   1.125 +
   1.126 +context ordered_semidom
   1.127 +begin
   1.128 +
   1.129 +lemma power2_le_imp_le:
   1.130 +  "x\<twosuperior> \<le> y\<twosuperior> \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y"
   1.131 +  unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
   1.132 +
   1.133 +lemma power2_less_imp_less:
   1.134 +  "x\<twosuperior> < y\<twosuperior> \<Longrightarrow> 0 \<le> y \<Longrightarrow> x < y"
   1.135 +  by (rule power_less_imp_less_base)
   1.136 +
   1.137 +lemma power2_eq_imp_eq:
   1.138 +  "x\<twosuperior> = y\<twosuperior> \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x = y"
   1.139 +  unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base) simp
   1.140 +
   1.141 +end
   1.142 +
   1.143 +context ordered_idom
   1.144 +begin
   1.145 +
   1.146 +lemma zero_eq_power2 [simp]:
   1.147 +  "a\<twosuperior> = 0 \<longleftrightarrow> a = 0"
   1.148 +  by (force simp add: power2_eq_square)
   1.149 +
   1.150 +lemma zero_le_power2 [simp]:
   1.151 +  "0 \<le> a\<twosuperior>"
   1.152 +  by (simp add: power2_eq_square)
   1.153 +
   1.154 +lemma zero_less_power2 [simp]:
   1.155 +  "0 < a\<twosuperior> \<longleftrightarrow> a \<noteq> 0"
   1.156 +  by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
   1.157 +
   1.158 +lemma power2_less_0 [simp]:
   1.159 +  "\<not> a\<twosuperior> < 0"
   1.160 +  by (force simp add: power2_eq_square mult_less_0_iff) 
   1.161 +
   1.162 +lemma abs_power2 [simp]:
   1.163 +  "abs (a\<twosuperior>) = a\<twosuperior>"
   1.164 +  by (simp add: power2_eq_square abs_mult abs_mult_self)
   1.165 +
   1.166 +lemma power2_abs [simp]:
   1.167 +  "(abs a)\<twosuperior> = a\<twosuperior>"
   1.168 +  by (simp add: power2_eq_square abs_mult_self)
   1.169 +
   1.170 +lemma odd_power_less_zero:
   1.171 +  "a < 0 \<Longrightarrow> a ^ Suc (2*n) < 0"
   1.172 +proof (induct n)
   1.173 +  case 0
   1.174 +  then show ?case by simp
   1.175 +next
   1.176 +  case (Suc n)
   1.177 +  have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
   1.178 +    by (simp add: mult_ac power_add power2_eq_square)
   1.179 +  thus ?case
   1.180 +    by (simp del: power_Suc add: Suc mult_less_0_iff mult_neg_neg)
   1.181 +qed
   1.182 +
   1.183 +lemma odd_0_le_power_imp_0_le:
   1.184 +  "0 \<le> a ^ Suc (2*n) \<Longrightarrow> 0 \<le> a"
   1.185 +  using odd_power_less_zero [of a n]
   1.186 +    by (force simp add: linorder_not_less [symmetric]) 
   1.187 +
   1.188 +lemma zero_le_even_power'[simp]:
   1.189 +  "0 \<le> a ^ (2*n)"
   1.190 +proof (induct n)
   1.191 +  case 0
   1.192 +    show ?case by (simp add: zero_le_one)
   1.193 +next
   1.194 +  case (Suc n)
   1.195 +    have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" 
   1.196 +      by (simp add: mult_ac power_add power2_eq_square)
   1.197 +    thus ?case
   1.198 +      by (simp add: Suc zero_le_mult_iff)
   1.199 +qed
   1.200 +
   1.201 +lemma sum_power2_ge_zero:
   1.202 +  "0 \<le> x\<twosuperior> + y\<twosuperior>"
   1.203 +  unfolding power2_eq_square by (rule sum_squares_ge_zero)
   1.204 +
   1.205 +lemma not_sum_power2_lt_zero:
   1.206 +  "\<not> x\<twosuperior> + y\<twosuperior> < 0"
   1.207 +  unfolding power2_eq_square by (rule not_sum_squares_lt_zero)
   1.208 +
   1.209 +lemma sum_power2_eq_zero_iff:
   1.210 +  "x\<twosuperior> + y\<twosuperior> = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   1.211 +  unfolding power2_eq_square by (rule sum_squares_eq_zero_iff)
   1.212 +
   1.213 +lemma sum_power2_le_zero_iff:
   1.214 +  "x\<twosuperior> + y\<twosuperior> \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   1.215 +  unfolding power2_eq_square by (rule sum_squares_le_zero_iff)
   1.216 +
   1.217 +lemma sum_power2_gt_zero_iff:
   1.218 +  "0 < x\<twosuperior> + y\<twosuperior> \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
   1.219 +  unfolding power2_eq_square by (rule sum_squares_gt_zero_iff)
   1.220 +
   1.221 +end
   1.222 +
   1.223 +lemma power2_sum:
   1.224 +  fixes x y :: "'a::number_ring"
   1.225 +  shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
   1.226 +  by (simp add: ring_distribs power2_eq_square)
   1.227 +
   1.228 +lemma power2_diff:
   1.229 +  fixes x y :: "'a::number_ring"
   1.230 +  shows "(x - y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> - 2 * x * y"
   1.231 +  by (simp add: ring_distribs power2_eq_square)
   1.232 +
   1.233  
   1.234  subsection {* Predicate for negative binary numbers *}
   1.235  
   1.236 @@ -115,11 +325,6 @@
   1.237  lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
   1.238  by (simp add: nat_numeral_1_eq_1)
   1.239  
   1.240 -lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
   1.241 -apply (unfold nat_number_of_def)
   1.242 -apply (rule nat_2)
   1.243 -done
   1.244 -
   1.245  
   1.246  subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
   1.247  
   1.248 @@ -314,128 +519,10 @@
   1.249  
   1.250  subsection{*Powers with Numeric Exponents*}
   1.251  
   1.252 -text{*We cannot refer to the number @{term 2} in @{text Ring_and_Field.thy}.
   1.253 -We cannot prove general results about the numeral @{term "-1"}, so we have to
   1.254 -use @{term "- 1"} instead.*}
   1.255 -
   1.256 -lemma power2_eq_square: "(a::'a::recpower)\<twosuperior> = a * a"
   1.257 -  by (simp add: numeral_2_eq_2 Power.power_Suc)
   1.258 -
   1.259 -lemma zero_power2 [simp]: "(0::'a::{semiring_1,recpower})\<twosuperior> = 0"
   1.260 -  by (simp add: power2_eq_square)
   1.261 -
   1.262 -lemma one_power2 [simp]: "(1::'a::{semiring_1,recpower})\<twosuperior> = 1"
   1.263 -  by (simp add: power2_eq_square)
   1.264 -
   1.265 -lemma power3_eq_cube: "(x::'a::recpower) ^ 3 = x * x * x"
   1.266 -  apply (subgoal_tac "3 = Suc (Suc (Suc 0))")
   1.267 -  apply (erule ssubst)
   1.268 -  apply (simp add: power_Suc mult_ac)
   1.269 -  apply (unfold nat_number_of_def)
   1.270 -  apply (subst nat_eq_iff)
   1.271 -  apply simp
   1.272 -done
   1.273 -
   1.274  text{*Squares of literal numerals will be evaluated.*}
   1.275 -lemmas power2_eq_square_number_of =
   1.276 +lemmas power2_eq_square_number_of [simp] =
   1.277      power2_eq_square [of "number_of w", standard]
   1.278 -declare power2_eq_square_number_of [simp]
   1.279 -
   1.280 -
   1.281 -lemma zero_le_power2[simp]: "0 \<le> (a\<twosuperior>::'a::{ordered_idom,recpower})"
   1.282 -  by (simp add: power2_eq_square)
   1.283 -
   1.284 -lemma zero_less_power2[simp]:
   1.285 -     "(0 < a\<twosuperior>) = (a \<noteq> (0::'a::{ordered_idom,recpower}))"
   1.286 -  by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
   1.287 -
   1.288 -lemma power2_less_0[simp]:
   1.289 -  fixes a :: "'a::{ordered_idom,recpower}"
   1.290 -  shows "~ (a\<twosuperior> < 0)"
   1.291 -by (force simp add: power2_eq_square mult_less_0_iff) 
   1.292 -
   1.293 -lemma zero_eq_power2[simp]:
   1.294 -     "(a\<twosuperior> = 0) = (a = (0::'a::{ordered_idom,recpower}))"
   1.295 -  by (force simp add: power2_eq_square mult_eq_0_iff)
   1.296 -
   1.297 -lemma abs_power2[simp]:
   1.298 -     "abs(a\<twosuperior>) = (a\<twosuperior>::'a::{ordered_idom,recpower})"
   1.299 -  by (simp add: power2_eq_square abs_mult abs_mult_self)
   1.300 -
   1.301 -lemma power2_abs[simp]:
   1.302 -     "(abs a)\<twosuperior> = (a\<twosuperior>::'a::{ordered_idom,recpower})"
   1.303 -  by (simp add: power2_eq_square abs_mult_self)
   1.304 -
   1.305 -lemma power2_minus[simp]:
   1.306 -     "(- a)\<twosuperior> = (a\<twosuperior>::'a::{comm_ring_1,recpower})"
   1.307 -  by (simp add: power2_eq_square)
   1.308 -
   1.309 -lemma power2_le_imp_le:
   1.310 -  fixes x y :: "'a::{ordered_semidom,recpower}"
   1.311 -  shows "\<lbrakk>x\<twosuperior> \<le> y\<twosuperior>; 0 \<le> y\<rbrakk> \<Longrightarrow> x \<le> y"
   1.312 -unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
   1.313  
   1.314 -lemma power2_less_imp_less:
   1.315 -  fixes x y :: "'a::{ordered_semidom,recpower}"
   1.316 -  shows "\<lbrakk>x\<twosuperior> < y\<twosuperior>; 0 \<le> y\<rbrakk> \<Longrightarrow> x < y"
   1.317 -by (rule power_less_imp_less_base)
   1.318 -
   1.319 -lemma power2_eq_imp_eq:
   1.320 -  fixes x y :: "'a::{ordered_semidom,recpower}"
   1.321 -  shows "\<lbrakk>x\<twosuperior> = y\<twosuperior>; 0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> x = y"
   1.322 -unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base, simp)
   1.323 -
   1.324 -lemma power_minus1_even[simp]: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})"
   1.325 -proof (induct n)
   1.326 -  case 0 show ?case by simp
   1.327 -next
   1.328 -  case (Suc n) then show ?case by (simp add: power_Suc power_add)
   1.329 -qed
   1.330 -
   1.331 -lemma power_minus1_odd: "(- 1) ^ Suc(2*n) = -(1::'a::{comm_ring_1,recpower})"
   1.332 -  by (simp add: power_Suc) 
   1.333 -
   1.334 -lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2"
   1.335 -  by (subst mult_commute) (simp add: power_mult)
   1.336 -
   1.337 -lemma power_odd_eq: "(a::int) ^ Suc(2*n) = a * (a^n)^2"
   1.338 -  by (simp add: power_even_eq)
   1.339 -
   1.340 -lemma power_minus_even [simp]:
   1.341 -  "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"
   1.342 -  by (simp add: power_minus [of a]) 
   1.343 -
   1.344 -lemma zero_le_even_power'[simp]:
   1.345 -     "0 \<le> (a::'a::{ordered_idom,recpower}) ^ (2*n)"
   1.346 -proof (induct "n")
   1.347 -  case 0
   1.348 -    show ?case by (simp add: zero_le_one)
   1.349 -next
   1.350 -  case (Suc n)
   1.351 -    have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" 
   1.352 -      by (simp add: mult_ac power_add power2_eq_square)
   1.353 -    thus ?case
   1.354 -      by (simp add: prems zero_le_mult_iff)
   1.355 -qed
   1.356 -
   1.357 -lemma odd_power_less_zero:
   1.358 -     "(a::'a::{ordered_idom,recpower}) < 0 ==> a ^ Suc(2*n) < 0"
   1.359 -proof (induct "n")
   1.360 -  case 0
   1.361 -  then show ?case by simp
   1.362 -next
   1.363 -  case (Suc n)
   1.364 -  have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
   1.365 -    by (simp add: mult_ac power_add power2_eq_square)
   1.366 -  thus ?case
   1.367 -    by (simp del: power_Suc add: prems mult_less_0_iff mult_neg_neg)
   1.368 -qed
   1.369 -
   1.370 -lemma odd_0_le_power_imp_0_le:
   1.371 -     "0 \<le> a  ^ Suc(2*n) ==> 0 \<le> (a::'a::{ordered_idom,recpower})"
   1.372 -apply (insert odd_power_less_zero [of a n]) 
   1.373 -apply (force simp add: linorder_not_less [symmetric]) 
   1.374 -done
   1.375  
   1.376  text{*Simprules for comparisons where common factors can be cancelled.*}
   1.377  lemmas zero_compare_simps =
   1.378 @@ -621,7 +708,7 @@
   1.379  text{*For arbitrary rings*}
   1.380  
   1.381  lemma power_number_of_even:
   1.382 -  fixes z :: "'a::{number_ring,recpower}"
   1.383 +  fixes z :: "'a::number_ring"
   1.384    shows "z ^ number_of (Int.Bit0 w) = (let w = z ^ (number_of w) in w * w)"
   1.385  unfolding Let_def nat_number_of_def number_of_Bit0
   1.386  apply (rule_tac x = "number_of w" in spec, clarify)
   1.387 @@ -630,7 +717,7 @@
   1.388  done
   1.389  
   1.390  lemma power_number_of_odd:
   1.391 -  fixes z :: "'a::{number_ring,recpower}"
   1.392 +  fixes z :: "'a::number_ring"
   1.393    shows "z ^ number_of (Int.Bit1 w) = (if (0::int) <= number_of w
   1.394       then (let w = z ^ (number_of w) in z * w * w) else 1)"
   1.395  unfolding Let_def nat_number_of_def number_of_Bit1
   1.396 @@ -697,11 +784,11 @@
   1.397  lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
   1.398    by (simp add: Let_def)
   1.399  
   1.400 -lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring,recpower})"
   1.401 -by (simp add: power_mult power_Suc); 
   1.402 +lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring})"
   1.403 +  by (simp only: number_of_Min power_minus1_even)
   1.404  
   1.405 -lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring,recpower})"
   1.406 -by (simp add: power_mult power_Suc); 
   1.407 +lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring})"
   1.408 +  by (simp only: number_of_Min power_minus1_odd)
   1.409  
   1.410  
   1.411  subsection{*Literal arithmetic and @{term of_nat}*}