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
```