--- a/src/HOL/Nat_Numeral.thy Thu Mar 29 11:47:30 2012 +0200
+++ b/src/HOL/Nat_Numeral.thy Thu Mar 29 14:09:10 2012 +0200
@@ -9,245 +9,6 @@
imports Int
begin
-subsection {* Numerals for natural numbers *}
-
-text {*
- Arithmetic for naturals is reduced to that for the non-negative integers.
-*}
-
-subsection {* Special case: squares and cubes *}
-
-lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
- by (simp add: nat_number(2-4))
-
-lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))"
- by (simp add: nat_number(2-4))
-
-context power
-begin
-
-abbreviation (xsymbols)
- power2 :: "'a \<Rightarrow> 'a" ("(_\<twosuperior>)" [1000] 999) where
- "x\<twosuperior> \<equiv> x ^ 2"
-
-notation (latex output)
- power2 ("(_\<twosuperior>)" [1000] 999)
-
-notation (HTML output)
- power2 ("(_\<twosuperior>)" [1000] 999)
-
-end
-
-context monoid_mult
-begin
-
-lemma power2_eq_square: "a\<twosuperior> = a * a"
- by (simp add: numeral_2_eq_2)
-
-lemma power3_eq_cube: "a ^ 3 = a * a * a"
- by (simp add: numeral_3_eq_3 mult_assoc)
-
-lemma power_even_eq:
- "a ^ (2*n) = (a ^ n) ^ 2"
- by (subst mult_commute) (simp add: power_mult)
-
-lemma power_odd_eq:
- "a ^ Suc (2*n) = a * (a ^ n) ^ 2"
- by (simp add: power_even_eq)
-
-end
-
-context semiring_1
-begin
-
-lemma zero_power2 [simp]: "0\<twosuperior> = 0"
- by (simp add: power2_eq_square)
-
-lemma one_power2 [simp]: "1\<twosuperior> = 1"
- by (simp add: power2_eq_square)
-
-end
-
-context ring_1
-begin
-
-lemma power2_minus [simp]:
- "(- a)\<twosuperior> = a\<twosuperior>"
- by (simp add: power2_eq_square)
-
-lemma power_minus1_even [simp]:
- "-1 ^ (2*n) = 1"
-proof (induct n)
- case 0 show ?case by simp
-next
- case (Suc n) then show ?case by (simp add: power_add power2_eq_square)
-qed
-
-lemma power_minus1_odd:
- "-1 ^ Suc (2*n) = -1"
- by simp
-
-lemma power_minus_even [simp]:
- "(-a) ^ (2*n) = a ^ (2*n)"
- by (simp add: power_minus [of a])
-
-end
-
-context ring_1_no_zero_divisors
-begin
-
-lemma zero_eq_power2 [simp]:
- "a\<twosuperior> = 0 \<longleftrightarrow> a = 0"
- unfolding power2_eq_square by simp
-
-lemma power2_eq_1_iff:
- "a\<twosuperior> = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"
- unfolding power2_eq_square by (rule square_eq_1_iff)
-
-end
-
-context idom
-begin
-
-lemma power2_eq_iff: "x\<twosuperior> = y\<twosuperior> \<longleftrightarrow> x = y \<or> x = - y"
- unfolding power2_eq_square by (rule square_eq_iff)
-
-end
-
-context linordered_ring
-begin
-
-lemma sum_squares_ge_zero:
- "0 \<le> x * x + y * y"
- by (intro add_nonneg_nonneg zero_le_square)
-
-lemma not_sum_squares_lt_zero:
- "\<not> x * x + y * y < 0"
- by (simp add: not_less sum_squares_ge_zero)
-
-end
-
-context linordered_ring_strict
-begin
-
-lemma sum_squares_eq_zero_iff:
- "x * x + y * y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
- by (simp add: add_nonneg_eq_0_iff)
-
-lemma sum_squares_le_zero_iff:
- "x * x + y * y \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
- by (simp add: le_less not_sum_squares_lt_zero sum_squares_eq_zero_iff)
-
-lemma sum_squares_gt_zero_iff:
- "0 < x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
- by (simp add: not_le [symmetric] sum_squares_le_zero_iff)
-
-end
-
-context linordered_semidom
-begin
-
-lemma power2_le_imp_le:
- "x\<twosuperior> \<le> y\<twosuperior> \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y"
- unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
-
-lemma power2_less_imp_less:
- "x\<twosuperior> < y\<twosuperior> \<Longrightarrow> 0 \<le> y \<Longrightarrow> x < y"
- by (rule power_less_imp_less_base)
-
-lemma power2_eq_imp_eq:
- "x\<twosuperior> = y\<twosuperior> \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x = y"
- unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base) simp
-
-end
-
-context linordered_idom
-begin
-
-lemma zero_le_power2 [simp]:
- "0 \<le> a\<twosuperior>"
- by (simp add: power2_eq_square)
-
-lemma zero_less_power2 [simp]:
- "0 < a\<twosuperior> \<longleftrightarrow> a \<noteq> 0"
- by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
-
-lemma power2_less_0 [simp]:
- "\<not> a\<twosuperior> < 0"
- by (force simp add: power2_eq_square mult_less_0_iff)
-
-lemma abs_power2 [simp]:
- "abs (a\<twosuperior>) = a\<twosuperior>"
- by (simp add: power2_eq_square abs_mult abs_mult_self)
-
-lemma power2_abs [simp]:
- "(abs a)\<twosuperior> = a\<twosuperior>"
- by (simp add: power2_eq_square abs_mult_self)
-
-lemma odd_power_less_zero:
- "a < 0 \<Longrightarrow> a ^ Suc (2*n) < 0"
-proof (induct n)
- case 0
- then show ?case by simp
-next
- case (Suc n)
- have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
- by (simp add: mult_ac power_add power2_eq_square)
- thus ?case
- by (simp del: power_Suc add: Suc mult_less_0_iff mult_neg_neg)
-qed
-
-lemma odd_0_le_power_imp_0_le:
- "0 \<le> a ^ Suc (2*n) \<Longrightarrow> 0 \<le> a"
- using odd_power_less_zero [of a n]
- by (force simp add: linorder_not_less [symmetric])
-
-lemma zero_le_even_power'[simp]:
- "0 \<le> a ^ (2*n)"
-proof (induct n)
- case 0
- show ?case by simp
-next
- case (Suc n)
- have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)"
- by (simp add: mult_ac power_add power2_eq_square)
- thus ?case
- by (simp add: Suc zero_le_mult_iff)
-qed
-
-lemma sum_power2_ge_zero:
- "0 \<le> x\<twosuperior> + y\<twosuperior>"
- unfolding power2_eq_square by (rule sum_squares_ge_zero)
-
-lemma not_sum_power2_lt_zero:
- "\<not> x\<twosuperior> + y\<twosuperior> < 0"
- unfolding power2_eq_square by (rule not_sum_squares_lt_zero)
-
-lemma sum_power2_eq_zero_iff:
- "x\<twosuperior> + y\<twosuperior> = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
- unfolding power2_eq_square by (rule sum_squares_eq_zero_iff)
-
-lemma sum_power2_le_zero_iff:
- "x\<twosuperior> + y\<twosuperior> \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
- unfolding power2_eq_square by (rule sum_squares_le_zero_iff)
-
-lemma sum_power2_gt_zero_iff:
- "0 < x\<twosuperior> + y\<twosuperior> \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
- unfolding power2_eq_square by (rule sum_squares_gt_zero_iff)
-
-end
-
-lemma power2_sum:
- fixes x y :: "'a::comm_semiring_1"
- shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
- by (simp add: algebra_simps power2_eq_square mult_2_right)
-
-lemma power2_diff:
- fixes x y :: "'a::comm_ring_1"
- shows "(x - y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> - 2 * x * y"
- by (simp add: ring_distribs power2_eq_square mult_2) (rule mult_commute)
-
-
subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
declare nat_1 [simp]