src/HOL/Nat_Numeral.thy
author huffman
Fri Mar 30 11:52:26 2012 +0200 (2012-03-30)
changeset 47218 2b652cbadde1
parent 47217 501b9bbd0d6e
child 47220 52426c62b5d0
permissions -rw-r--r--
new lemmas for simplifying subtraction on nat numerals
     1 (*  Title:      HOL/Nat_Numeral.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1999  University of Cambridge
     4 *)
     5 
     6 header {* Binary numerals for the natural numbers *}
     7 
     8 theory Nat_Numeral
     9 imports Int
    10 begin
    11 
    12 subsection{*Comparisons*}
    13 
    14 text{*Simprules for comparisons where common factors can be cancelled.*}
    15 lemmas zero_compare_simps =
    16     add_strict_increasing add_strict_increasing2 add_increasing
    17     zero_le_mult_iff zero_le_divide_iff 
    18     zero_less_mult_iff zero_less_divide_iff 
    19     mult_le_0_iff divide_le_0_iff 
    20     mult_less_0_iff divide_less_0_iff 
    21     zero_le_power2 power2_less_0
    22 
    23 subsubsection{*Nat *}
    24 
    25 lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
    26 by simp
    27 
    28 (*Expresses a natural number constant as the Suc of another one.
    29   NOT suitable for rewriting because n recurs on the right-hand side.*)
    30 lemmas expand_Suc = Suc_pred' [of "numeral v", OF zero_less_numeral] for v
    31 
    32 subsubsection{*Arith *}
    33 
    34 (* These two can be useful when m = numeral... *)
    35 
    36 lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))"
    37   unfolding One_nat_def by (cases m) simp_all
    38 
    39 lemma mult_eq_if: "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))"
    40   unfolding One_nat_def by (cases m) simp_all
    41 
    42 lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))"
    43   unfolding One_nat_def by (cases m) simp_all
    44 
    45  
    46 subsection{*Literal arithmetic involving powers*}
    47 
    48 text{*For arbitrary rings*}
    49 
    50 lemma power_numeral_even:
    51   fixes z :: "'a::monoid_mult"
    52   shows "z ^ numeral (Num.Bit0 w) = (let w = z ^ (numeral w) in w * w)"
    53   unfolding numeral_Bit0 power_add Let_def ..
    54 
    55 lemma power_numeral_odd:
    56   fixes z :: "'a::monoid_mult"
    57   shows "z ^ numeral (Num.Bit1 w) = (let w = z ^ (numeral w) in z * w * w)"
    58   unfolding numeral_Bit1 One_nat_def add_Suc_right add_0_right
    59   unfolding power_Suc power_add Let_def mult_assoc ..
    60 
    61 lemmas zpower_numeral_even = power_numeral_even [where 'a=int]
    62 lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int]
    63 
    64 lemma nat_numeral_Bit0:
    65   "numeral (Num.Bit0 w) = (let n::nat = numeral w in n + n)"
    66   unfolding numeral_Bit0 Let_def ..
    67 
    68 lemma nat_numeral_Bit1:
    69   "numeral (Num.Bit1 w) = (let n = numeral w in Suc (n + n))"
    70   unfolding numeral_Bit1 Let_def by simp
    71 
    72 lemmas eval_nat_numeral =
    73   nat_numeral_Bit0 nat_numeral_Bit1
    74 
    75 lemmas nat_arith =
    76   diff_nat_numeral
    77 
    78 lemmas semiring_norm =
    79   Let_def arith_simps nat_arith rel_simps
    80   if_False if_True
    81   add_0 add_Suc add_numeral_left
    82   add_neg_numeral_left mult_numeral_left
    83   numeral_1_eq_1 [symmetric] Suc_eq_plus1
    84   eq_numeral_iff_iszero not_iszero_Numeral1
    85 
    86 lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
    87   by (fact Let_def)
    88 
    89 
    90 subsection{*Literal arithmetic and @{term of_nat}*}
    91 
    92 lemma of_nat_double:
    93      "0 \<le> x ==> of_nat (nat (2 * x)) = of_nat (nat x) + of_nat (nat x)"
    94 by (simp only: mult_2 nat_add_distrib of_nat_add) 
    95 
    96 
    97 subsubsection{*For simplifying @{term "Suc m - K"} and  @{term "K - Suc m"}*}
    98 
    99 text{*Where K above is a literal*}
   100 
   101 lemma Suc_diff_eq_diff_pred: "0 < n ==> Suc m - n = m - (n - Numeral1)"
   102 by (simp split: nat_diff_split)
   103 
   104 lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
   105 by (simp split: nat_diff_split)
   106 
   107 
   108 subsubsection{*Various Other Lemmas*}
   109 
   110 text {*Evens and Odds, for Mutilated Chess Board*}
   111 
   112 text{*Case analysis on @{term "n<2"}*}
   113 lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
   114 by (auto simp add: numeral_2_eq_2)
   115 
   116 text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
   117 
   118 lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
   119 by simp
   120 
   121 lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
   122 by simp
   123 
   124 text{*Can be used to eliminate long strings of Sucs, but not by default*}
   125 lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
   126 by simp
   127 
   128 text{*Legacy theorems*}
   129 
   130 lemmas nat_1_add_1 = one_add_one [where 'a=nat]
   131 
   132 end