removed Nat_Numeral.thy, moving all theorems elsewhere
authorhuffman
Sun Apr 01 16:09:58 2012 +0200 (2012-04-01)
changeset 4725530a1692557b0
parent 47244 a7f85074c169
child 47256 aabdd7765b64
removed Nat_Numeral.thy, moving all theorems elsewhere
src/HOL/Code_Numeral.thy
src/HOL/Divides.thy
src/HOL/Int.thy
src/HOL/IsaMakefile
src/HOL/Nat.thy
src/HOL/Nat_Numeral.thy
src/HOL/Nat_Transfer.thy
src/HOL/Num.thy
src/HOL/Numeral_Simprocs.thy
src/HOL/Power.thy
     1.1 --- a/src/HOL/Code_Numeral.thy	Sun Apr 01 09:12:03 2012 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Sun Apr 01 16:09:58 2012 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4  header {* Type of target language numerals *}
     1.5  
     1.6  theory Code_Numeral
     1.7 -imports Nat_Numeral Nat_Transfer Divides
     1.8 +imports Nat_Transfer Divides
     1.9  begin
    1.10  
    1.11  text {*
     2.1 --- a/src/HOL/Divides.thy	Sun Apr 01 09:12:03 2012 +0200
     2.2 +++ b/src/HOL/Divides.thy	Sun Apr 01 16:09:58 2012 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  header {* The division operators div and mod *}
     2.5  
     2.6  theory Divides
     2.7 -imports Nat_Numeral Nat_Transfer
     2.8 +imports Nat_Transfer
     2.9  uses "~~/src/Provers/Arith/cancel_div_mod.ML"
    2.10  begin
    2.11  
     3.1 --- a/src/HOL/Int.thy	Sun Apr 01 09:12:03 2012 +0200
     3.2 +++ b/src/HOL/Int.thy	Sun Apr 01 16:09:58 2012 +0200
     3.3 @@ -990,6 +990,8 @@
     3.4    "numeral v - (1::nat) = nat (numeral v - 1)"
     3.5    using diff_nat_numeral [of v Num.One] by simp
     3.6  
     3.7 +lemmas nat_arith = diff_nat_numeral
     3.8 +
     3.9  
    3.10  subsection "Induction principles for int"
    3.11  
    3.12 @@ -1756,6 +1758,8 @@
    3.13  lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m"] for m
    3.14  lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
    3.15  lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
    3.16 +lemmas zpower_numeral_even = power_numeral_even [where 'a=int]
    3.17 +lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int]
    3.18  
    3.19  lemma zpower_zpower:
    3.20    "(x ^ y) ^ z = (x ^ (y * z)::int)"
     4.1 --- a/src/HOL/IsaMakefile	Sun Apr 01 09:12:03 2012 +0200
     4.2 +++ b/src/HOL/IsaMakefile	Sun Apr 01 16:09:58 2012 +0200
     4.3 @@ -290,7 +290,6 @@
     4.4    List.thy \
     4.5    Main.thy \
     4.6    Map.thy \
     4.7 -  Nat_Numeral.thy \
     4.8    Nat_Transfer.thy \
     4.9    New_DSequence.thy \
    4.10    New_Random_Sequence.thy \
     5.1 --- a/src/HOL/Nat.thy	Sun Apr 01 09:12:03 2012 +0200
     5.2 +++ b/src/HOL/Nat.thy	Sun Apr 01 16:09:58 2012 +0200
     5.3 @@ -1112,6 +1112,24 @@
     5.4      -- {* elimination of @{text -} on @{text nat} in assumptions *}
     5.5  by (auto split: nat_diff_split)
     5.6  
     5.7 +lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
     5.8 +  by simp
     5.9 +
    5.10 +lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))"
    5.11 +  unfolding One_nat_def by (cases m) simp_all
    5.12 +
    5.13 +lemma mult_eq_if: "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))"
    5.14 +  unfolding One_nat_def by (cases m) simp_all
    5.15 +
    5.16 +lemma Suc_diff_eq_diff_pred: "0 < n ==> Suc m - n = m - (n - 1)"
    5.17 +  unfolding One_nat_def by (cases n) simp_all
    5.18 +
    5.19 +lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
    5.20 +  unfolding One_nat_def by (cases m) simp_all
    5.21 +
    5.22 +lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
    5.23 +  by (fact Let_def)
    5.24 +
    5.25  
    5.26  subsubsection {* Monotonicity of Multiplication *}
    5.27  
     6.1 --- a/src/HOL/Nat_Numeral.thy	Sun Apr 01 09:12:03 2012 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,121 +0,0 @@
     6.4 -(*  Title:      HOL/Nat_Numeral.thy
     6.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.6 -    Copyright   1999  University of Cambridge
     6.7 -*)
     6.8 -
     6.9 -header {* Binary numerals for the natural numbers *}
    6.10 -
    6.11 -theory Nat_Numeral
    6.12 -imports Int
    6.13 -begin
    6.14 -
    6.15 -subsection{*Comparisons*}
    6.16 -
    6.17 -text{*Simprules for comparisons where common factors can be cancelled.*}
    6.18 -lemmas zero_compare_simps =
    6.19 -    add_strict_increasing add_strict_increasing2 add_increasing
    6.20 -    zero_le_mult_iff zero_le_divide_iff 
    6.21 -    zero_less_mult_iff zero_less_divide_iff 
    6.22 -    mult_le_0_iff divide_le_0_iff 
    6.23 -    mult_less_0_iff divide_less_0_iff 
    6.24 -    zero_le_power2 power2_less_0
    6.25 -
    6.26 -subsubsection{*Nat *}
    6.27 -
    6.28 -lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
    6.29 -by simp
    6.30 -
    6.31 -(*Expresses a natural number constant as the Suc of another one.
    6.32 -  NOT suitable for rewriting because n recurs on the right-hand side.*)
    6.33 -lemmas expand_Suc = Suc_pred' [of "numeral v", OF zero_less_numeral] for v
    6.34 -
    6.35 -subsubsection{*Arith *}
    6.36 -
    6.37 -(* These two can be useful when m = numeral... *)
    6.38 -
    6.39 -lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))"
    6.40 -  unfolding One_nat_def by (cases m) simp_all
    6.41 -
    6.42 -lemma mult_eq_if: "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))"
    6.43 -  unfolding One_nat_def by (cases m) simp_all
    6.44 -
    6.45 -lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))"
    6.46 -  unfolding One_nat_def by (cases m) simp_all
    6.47 -
    6.48 - 
    6.49 -subsection{*Literal arithmetic involving powers*}
    6.50 -
    6.51 -text{*For arbitrary rings*}
    6.52 -
    6.53 -lemma power_numeral_even:
    6.54 -  fixes z :: "'a::monoid_mult"
    6.55 -  shows "z ^ numeral (Num.Bit0 w) = (let w = z ^ (numeral w) in w * w)"
    6.56 -  unfolding numeral_Bit0 power_add Let_def ..
    6.57 -
    6.58 -lemma power_numeral_odd:
    6.59 -  fixes z :: "'a::monoid_mult"
    6.60 -  shows "z ^ numeral (Num.Bit1 w) = (let w = z ^ (numeral w) in z * w * w)"
    6.61 -  unfolding numeral_Bit1 One_nat_def add_Suc_right add_0_right
    6.62 -  unfolding power_Suc power_add Let_def mult_assoc ..
    6.63 -
    6.64 -lemmas zpower_numeral_even = power_numeral_even [where 'a=int]
    6.65 -lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int]
    6.66 -
    6.67 -lemmas nat_arith =
    6.68 -  diff_nat_numeral
    6.69 -
    6.70 -lemmas semiring_norm =
    6.71 -  Let_def arith_simps nat_arith rel_simps
    6.72 -  if_False if_True
    6.73 -  add_0 add_Suc add_numeral_left
    6.74 -  add_neg_numeral_left mult_numeral_left
    6.75 -  numeral_1_eq_1 [symmetric] Suc_eq_plus1
    6.76 -  eq_numeral_iff_iszero not_iszero_Numeral1
    6.77 -
    6.78 -lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
    6.79 -  by (fact Let_def)
    6.80 -
    6.81 -
    6.82 -subsection{*Literal arithmetic and @{term of_nat}*}
    6.83 -
    6.84 -lemma of_nat_double:
    6.85 -     "0 \<le> x ==> of_nat (nat (2 * x)) = of_nat (nat x) + of_nat (nat x)"
    6.86 -by (simp only: mult_2 nat_add_distrib of_nat_add) 
    6.87 -
    6.88 -
    6.89 -subsubsection{*For simplifying @{term "Suc m - K"} and  @{term "K - Suc m"}*}
    6.90 -
    6.91 -text{*Where K above is a literal*}
    6.92 -
    6.93 -lemma Suc_diff_eq_diff_pred: "0 < n ==> Suc m - n = m - (n - Numeral1)"
    6.94 -by (simp split: nat_diff_split)
    6.95 -
    6.96 -lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
    6.97 -by (simp split: nat_diff_split)
    6.98 -
    6.99 -
   6.100 -subsubsection{*Various Other Lemmas*}
   6.101 -
   6.102 -text {*Evens and Odds, for Mutilated Chess Board*}
   6.103 -
   6.104 -text{*Case analysis on @{term "n<2"}*}
   6.105 -lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
   6.106 -by (auto simp add: numeral_2_eq_2)
   6.107 -
   6.108 -text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
   6.109 -
   6.110 -lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
   6.111 -by simp
   6.112 -
   6.113 -lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
   6.114 -by simp
   6.115 -
   6.116 -text{*Can be used to eliminate long strings of Sucs, but not by default*}
   6.117 -lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
   6.118 -by simp
   6.119 -
   6.120 -text{*Legacy theorems*}
   6.121 -
   6.122 -lemmas nat_1_add_1 = one_add_one [where 'a=nat]
   6.123 -
   6.124 -end
     7.1 --- a/src/HOL/Nat_Transfer.thy	Sun Apr 01 09:12:03 2012 +0200
     7.2 +++ b/src/HOL/Nat_Transfer.thy	Sun Apr 01 16:09:58 2012 +0200
     7.3 @@ -4,7 +4,7 @@
     7.4  header {* Generic transfer machinery;  specific transfer from nats to ints and back. *}
     7.5  
     7.6  theory Nat_Transfer
     7.7 -imports Nat_Numeral
     7.8 +imports Int
     7.9  uses ("Tools/transfer.ML")
    7.10  begin
    7.11  
     8.1 --- a/src/HOL/Num.thy	Sun Apr 01 09:12:03 2012 +0200
     8.2 +++ b/src/HOL/Num.thy	Sun Apr 01 16:09:58 2012 +0200
     8.3 @@ -965,6 +965,27 @@
     8.4      (let pv = pred_numeral v in f (pv + n) (nat_rec a f (pv + n)))"
     8.5    by (simp add: numeral_eq_Suc Let_def)
     8.6  
     8.7 +text {* Case analysis on @{term "n < 2"} *}
     8.8 +
     8.9 +lemma less_2_cases: "n < 2 \<Longrightarrow> n = 0 \<or> n = Suc 0"
    8.10 +  by (auto simp add: numeral_2_eq_2)
    8.11 +
    8.12 +text {* Removal of Small Numerals: 0, 1 and (in additive positions) 2 *}
    8.13 +text {* bh: Are these rules really a good idea? *}
    8.14 +
    8.15 +lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
    8.16 +  by simp
    8.17 +
    8.18 +lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
    8.19 +  by simp
    8.20 +
    8.21 +text {* Can be used to eliminate long strings of Sucs, but not by default. *}
    8.22 +
    8.23 +lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
    8.24 +  by simp
    8.25 +
    8.26 +lemmas nat_1_add_1 = one_add_one [where 'a=nat] (* legacy *)
    8.27 +
    8.28  
    8.29  subsection {* Numeral equations as default simplification rules *}
    8.30  
     9.1 --- a/src/HOL/Numeral_Simprocs.thy	Sun Apr 01 09:12:03 2012 +0200
     9.2 +++ b/src/HOL/Numeral_Simprocs.thy	Sun Apr 01 16:09:58 2012 +0200
     9.3 @@ -14,6 +14,14 @@
     9.4    ("Tools/nat_numeral_simprocs.ML")
     9.5  begin
     9.6  
     9.7 +lemmas semiring_norm =
     9.8 +  Let_def arith_simps nat_arith rel_simps
     9.9 +  if_False if_True
    9.10 +  add_0 add_Suc add_numeral_left
    9.11 +  add_neg_numeral_left mult_numeral_left
    9.12 +  numeral_1_eq_1 [symmetric] Suc_eq_plus1
    9.13 +  eq_numeral_iff_iszero not_iszero_Numeral1
    9.14 +
    9.15  declare split_div [of _ _ "numeral k", arith_split] for k
    9.16  declare split_mod [of _ _ "numeral k", arith_split] for k
    9.17  
    10.1 --- a/src/HOL/Power.thy	Sun Apr 01 09:12:03 2012 +0200
    10.2 +++ b/src/HOL/Power.thy	Sun Apr 01 16:09:58 2012 +0200
    10.3 @@ -81,6 +81,15 @@
    10.4    "a ^ Suc (2*n) = a * (a ^ n) ^ 2"
    10.5    by (simp add: power_even_eq)
    10.6  
    10.7 +lemma power_numeral_even:
    10.8 +  "z ^ numeral (Num.Bit0 w) = (let w = z ^ (numeral w) in w * w)"
    10.9 +  unfolding numeral_Bit0 power_add Let_def ..
   10.10 +
   10.11 +lemma power_numeral_odd:
   10.12 +  "z ^ numeral (Num.Bit1 w) = (let w = z ^ (numeral w) in z * w * w)"
   10.13 +  unfolding numeral_Bit1 One_nat_def add_Suc_right add_0_right
   10.14 +  unfolding power_Suc power_add Let_def mult_assoc ..
   10.15 +
   10.16  end
   10.17  
   10.18  context comm_monoid_mult
   10.19 @@ -596,6 +605,9 @@
   10.20  
   10.21  subsection {* Miscellaneous rules *}
   10.22  
   10.23 +lemma power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))"
   10.24 +  unfolding One_nat_def by (cases m) simp_all
   10.25 +
   10.26  lemma power2_sum:
   10.27    fixes x y :: "'a::comm_semiring_1"
   10.28    shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
   10.29 @@ -647,6 +659,16 @@
   10.30  apply assumption
   10.31  done
   10.32  
   10.33 +text {* Simprules for comparisons where common factors can be cancelled. *}
   10.34 +
   10.35 +lemmas zero_compare_simps =
   10.36 +    add_strict_increasing add_strict_increasing2 add_increasing
   10.37 +    zero_le_mult_iff zero_le_divide_iff 
   10.38 +    zero_less_mult_iff zero_less_divide_iff 
   10.39 +    mult_le_0_iff divide_le_0_iff 
   10.40 +    mult_less_0_iff divide_less_0_iff 
   10.41 +    zero_le_power2 power2_less_0
   10.42 +
   10.43  
   10.44  subsection {* Exponentiation for the Natural Numbers *}
   10.45