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.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.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.29  abbreviation (xsymbols)
1.30 @@ -43,6 +54,205 @@
1.32  end
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.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.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.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.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.124 +end
1.126 +context ordered_semidom
1.127 +begin
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.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.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.141 +end
1.143 +context ordered_idom
1.144 +begin
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.150 +lemma zero_le_power2 [simp]:
1.151 +  "0 \<le> a\<twosuperior>"
1.152 +  by (simp add: power2_eq_square)
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.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.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.166 +lemma power2_abs [simp]:
1.167 +  "(abs a)\<twosuperior> = a\<twosuperior>"
1.168 +  by (simp add: power2_eq_square abs_mult_self)
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.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.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.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.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.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.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.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.221 +end
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.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.234  subsection {* Predicate for negative binary numbers *}
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.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.246  subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
1.248 @@ -314,128 +519,10 @@
1.250  subsection{*Powers with Numeric Exponents*}
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.256 -lemma power2_eq_square: "(a::'a::recpower)\<twosuperior> = a * a"
1.257 -  by (simp add: numeral_2_eq_2 Power.power_Suc)
1.259 -lemma zero_power2 [simp]: "(0::'a::{semiring_1,recpower})\<twosuperior> = 0"
1.260 -  by (simp add: power2_eq_square)
1.262 -lemma one_power2 [simp]: "(1::'a::{semiring_1,recpower})\<twosuperior> = 1"
1.263 -  by (simp add: power2_eq_square)
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.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.281 -lemma zero_le_power2[simp]: "0 \<le> (a\<twosuperior>::'a::{ordered_idom,recpower})"
1.282 -  by (simp add: power2_eq_square)
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.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.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.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.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.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.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.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.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.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.331 -lemma power_minus1_odd: "(- 1) ^ Suc(2*n) = -(1::'a::{comm_ring_1,recpower})"
1.332 -  by (simp add: power_Suc)
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.337 -lemma power_odd_eq: "(a::int) ^ Suc(2*n) = a * (a^n)^2"
1.338 -  by (simp add: power_even_eq)
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.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.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.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.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.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.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.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.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.411  subsection{*Literal arithmetic and @{term of_nat}*}