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 lemmas nat_arith = |
|
65 diff_nat_numeral |
|
66 |
|
67 lemmas semiring_norm = |
|
68 Let_def arith_simps nat_arith rel_simps |
|
69 if_False if_True |
|
70 add_0 add_Suc add_numeral_left |
|
71 add_neg_numeral_left mult_numeral_left |
|
72 numeral_1_eq_1 [symmetric] Suc_eq_plus1 |
|
73 eq_numeral_iff_iszero not_iszero_Numeral1 |
|
74 |
|
75 lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)" |
|
76 by (fact Let_def) |
|
77 |
|
78 |
|
79 subsection{*Literal arithmetic and @{term of_nat}*} |
|
80 |
|
81 lemma of_nat_double: |
|
82 "0 \<le> x ==> of_nat (nat (2 * x)) = of_nat (nat x) + of_nat (nat x)" |
|
83 by (simp only: mult_2 nat_add_distrib of_nat_add) |
|
84 |
|
85 |
|
86 subsubsection{*For simplifying @{term "Suc m - K"} and @{term "K - Suc m"}*} |
|
87 |
|
88 text{*Where K above is a literal*} |
|
89 |
|
90 lemma Suc_diff_eq_diff_pred: "0 < n ==> Suc m - n = m - (n - Numeral1)" |
|
91 by (simp split: nat_diff_split) |
|
92 |
|
93 lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n" |
|
94 by (simp split: nat_diff_split) |
|
95 |
|
96 |
|
97 subsubsection{*Various Other Lemmas*} |
|
98 |
|
99 text {*Evens and Odds, for Mutilated Chess Board*} |
|
100 |
|
101 text{*Case analysis on @{term "n<2"}*} |
|
102 lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0" |
|
103 by (auto simp add: numeral_2_eq_2) |
|
104 |
|
105 text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*} |
|
106 |
|
107 lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)" |
|
108 by simp |
|
109 |
|
110 lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)" |
|
111 by simp |
|
112 |
|
113 text{*Can be used to eliminate long strings of Sucs, but not by default*} |
|
114 lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n" |
|
115 by simp |
|
116 |
|
117 text{*Legacy theorems*} |
|
118 |
|
119 lemmas nat_1_add_1 = one_add_one [where 'a=nat] |
|
120 |
|
121 end |
|