# HG changeset patch
# User huffman
# Date 1333022950 -7200
# Node ID 0c0501cb6da6fd5d1bd2dd8de969fe42dd8ef783
# Parent  ebd8c46d156b21d58d2ce8c3b22c0c8e41de0d8c
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy

diff -r ebd8c46d156b -r 0c0501cb6da6 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu Mar 29 11:47:30 2012 +0200
+++ b/src/HOL/Int.thy	Thu Mar 29 14:09:10 2012 +0200
@@ -857,14 +857,6 @@
   "abs(-1 ^ n) = (1::'a::linordered_idom)"
 by (simp add: power_abs)
 
-text{*Lemmas for specialist use, NOT as default simprules*}
-(* TODO: see if semiring duplication can be removed without breaking proofs *)
-lemma mult_2: "2 * z = (z+z::'a::semiring_1)"
-unfolding one_add_one [symmetric] left_distrib by simp
-
-lemma mult_2_right: "z * 2 = (z+z::'a::semiring_1)"
-unfolding one_add_one [symmetric] right_distrib by simp
-
 
 subsection{*More Inequality Reasoning*}
 
diff -r ebd8c46d156b -r 0c0501cb6da6 src/HOL/Nat_Numeral.thy
--- 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]
diff -r ebd8c46d156b -r 0c0501cb6da6 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Thu Mar 29 11:47:30 2012 +0200
+++ b/src/HOL/Num.thy	Thu Mar 29 14:09:10 2012 +0200
@@ -528,6 +528,12 @@
   by (induct n,
     simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1)
 
+lemma mult_2: "2 * z = z + z"
+  unfolding one_add_one [symmetric] left_distrib by simp
+
+lemma mult_2_right: "z * 2 = z + z"
+  unfolding one_add_one [symmetric] right_distrib by simp
+
 end
 
 lemma nat_of_num_numeral: "nat_of_num = numeral"
@@ -864,6 +870,12 @@
   "numeral (Bit1 n) = Suc (numeral (Bit0 n))"
   by (simp_all add: numeral.simps BitM_plus_one)
 
+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))
+
 
 subsection {* Numeral equations as default simplification rules *}
 
diff -r ebd8c46d156b -r 0c0501cb6da6 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Thu Mar 29 11:47:30 2012 +0200
+++ b/src/HOL/Power.thy	Thu Mar 29 14:09:10 2012 +0200
@@ -24,6 +24,18 @@
 notation (HTML output)
   power ("(_\<^bsup>_\<^esup>)" [1000] 1000)
 
+text {* Special syntax for squares. *}
+
+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
@@ -55,6 +67,20 @@
   "a ^ (m * n) = (a ^ m) ^ n"
   by (induct n) (simp_all add: power_add)
 
+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 comm_monoid_mult
@@ -91,6 +117,12 @@
 lemma power_zero_numeral [simp]: "(0::'a) ^ numeral k = 0"
   by (cases "numeral k :: nat", simp_all)
 
+lemma zero_power2: "0\<twosuperior> = 0" (* delete? *)
+  by (rule power_zero_numeral)
+
+lemma one_power2: "1\<twosuperior> = 1" (* delete? *)
+  by (rule power_one)
+
 end
 
 context comm_semiring_1
@@ -163,6 +195,87 @@
   "neg_numeral k ^ numeral (Num.Bit1 l) = neg_numeral (Num.pow k (Num.Bit1 l))"
   by (simp only: neg_numeral_def power_minus_Bit1 power_numeral pow.simps)
 
+lemma power2_minus [simp]:
+  "(- a)\<twosuperior> = a\<twosuperior>"
+  by (rule power_minus_Bit0)
+
+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 field_power_not_zero:
+  "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
+  by (induct n) auto
+
+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 division_ring
+begin
+
+text {* FIXME reorient or rename to @{text nonzero_inverse_power} *}
+lemma nonzero_power_inverse:
+  "a \<noteq> 0 \<Longrightarrow> inverse (a ^ n) = (inverse a) ^ n"
+  by (induct n)
+    (simp_all add: nonzero_inverse_mult_distrib power_commutes field_power_not_zero)
+
+end
+
+context field
+begin
+
+lemma nonzero_power_divide:
+  "b \<noteq> 0 \<Longrightarrow> (a / b) ^ n = a ^ n / b ^ n"
+  by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
+
+end
+
+
+subsection {* Exponentiation on ordered types *}
+
+context linordered_ring (* TODO: move *)
+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_semidom
@@ -356,6 +469,35 @@
   "a ^ n = b ^ n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 < n \<Longrightarrow> a = b"
   by (cases n) (simp_all del: power_Suc, rule power_inject_base)
 
+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_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_idom
@@ -381,36 +523,91 @@
   "0 \<le> abs a ^ n"
   by (rule zero_le_power [OF abs_ge_zero])
 
-end
+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
 
-context ring_1_no_zero_divisors
-begin
+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 field_power_not_zero:
-  "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
-  by (induct n) auto
+lemma sum_power2_ge_zero:
+  "0 \<le> x\<twosuperior> + y\<twosuperior>"
+  by (intro add_nonneg_nonneg zero_le_power2)
+
+lemma not_sum_power2_lt_zero:
+  "\<not> x\<twosuperior> + y\<twosuperior> < 0"
+  unfolding not_less by (rule sum_power2_ge_zero)
+
+lemma sum_power2_eq_zero_iff:
+  "x\<twosuperior> + y\<twosuperior> = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
+  unfolding power2_eq_square by (simp add: add_nonneg_eq_0_iff)
+
+lemma sum_power2_le_zero_iff:
+  "x\<twosuperior> + y\<twosuperior> \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
+  by (simp add: le_less sum_power2_eq_zero_iff not_sum_power2_lt_zero)
+
+lemma sum_power2_gt_zero_iff:
+  "0 < x\<twosuperior> + y\<twosuperior> \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
+  unfolding not_le [symmetric] by (simp add: sum_power2_le_zero_iff)
 
 end
 
-context division_ring
-begin
 
-text {* FIXME reorient or rename to @{text nonzero_inverse_power} *}
-lemma nonzero_power_inverse:
-  "a \<noteq> 0 \<Longrightarrow> inverse (a ^ n) = (inverse a) ^ n"
-  by (induct n)
-    (simp_all add: nonzero_inverse_mult_distrib power_commutes field_power_not_zero)
+subsection {* Miscellaneous rules *}
 
-end
-
-context field
-begin
+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 nonzero_power_divide:
-  "b \<noteq> 0 \<Longrightarrow> (a / b) ^ n = a ^ n / b ^ n"
-  by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
-
-end
+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)
 
 lemma power_0_Suc [simp]:
   "(0::'a::{power, semiring_0}) ^ Suc n = 0"