author | wenzelm |
Fri, 30 Mar 2012 17:22:17 +0200 | |
changeset 47230 | 6584098d5378 |
parent 47210 | b1dd32b2a505 |
child 47216 | 4d0878d54ca5 |
permissions | -rw-r--r-- |
30925 | 1 |
(* Title: HOL/Nat_Numeral.thy |
23164 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 |
Copyright 1999 University of Cambridge |
|
4 |
*) |
|
5 |
||
30925 | 6 |
header {* Binary numerals for the natural numbers *} |
23164 | 7 |
|
30925 | 8 |
theory Nat_Numeral |
33296
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset
|
9 |
imports Int |
23164 | 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)" |
|
35216 | 26 |
by simp |
23164 | 27 |
|
28 |
(*Expresses a natural number constant as the Suc of another one. |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
29 |
NOT suitable for rewriting because n recurs on the right-hand side.*) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
30 |
lemmas expand_Suc = Suc_pred' [of "numeral v", OF zero_less_numeral] for v |
23164 | 31 |
|
32 |
subsubsection{*Arith *} |
|
33 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
34 |
(* These two can be useful when m = numeral... *) |
23164 | 35 |
|
36 |
lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))" |
|
30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
29958
diff
changeset
|
37 |
unfolding One_nat_def by (cases m) simp_all |
23164 | 38 |
|
39 |
lemma mult_eq_if: "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))" |
|
30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
29958
diff
changeset
|
40 |
unfolding One_nat_def by (cases m) simp_all |
23164 | 41 |
|
42 |
lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))" |
|
30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
29958
diff
changeset
|
43 |
unfolding One_nat_def by (cases m) simp_all |
23164 | 44 |
|
45 |
||
46 |
subsection{*Literal arithmetic involving powers*} |
|
47 |
||
23294 | 48 |
text{*For arbitrary rings*} |
23164 | 49 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
50 |
lemma power_numeral_even: |
43526
2b92a6943915
generalize lemmas power_number_of_even and power_number_of_odd
huffman
parents:
40690
diff
changeset
|
51 |
fixes z :: "'a::monoid_mult" |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
52 |
shows "z ^ numeral (Num.Bit0 w) = (let w = z ^ (numeral w) in w * w)" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
53 |
unfolding numeral_Bit0 power_add Let_def .. |
23164 | 54 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
55 |
lemma power_numeral_odd: |
43526
2b92a6943915
generalize lemmas power_number_of_even and power_number_of_odd
huffman
parents:
40690
diff
changeset
|
56 |
fixes z :: "'a::monoid_mult" |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
57 |
shows "z ^ numeral (Num.Bit1 w) = (let w = z ^ (numeral w) in z * w * w)" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
58 |
unfolding numeral_Bit1 One_nat_def add_Suc_right add_0_right |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
59 |
unfolding power_Suc power_add Let_def mult_assoc .. |
23164 | 60 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
61 |
lemmas zpower_numeral_even = power_numeral_even [where 'a=int] |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
62 |
lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int] |
23164 | 63 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
64 |
lemma nat_numeral_Bit0: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
65 |
"numeral (Num.Bit0 w) = (let n::nat = numeral w in n + n)" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
66 |
unfolding numeral_Bit0 Let_def .. |
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25965
diff
changeset
|
67 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
68 |
lemma nat_numeral_Bit1: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
69 |
"numeral (Num.Bit1 w) = (let n = numeral w in Suc (n + n))" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
70 |
unfolding numeral_Bit1 Let_def by simp |
23164 | 71 |
|
40077 | 72 |
lemmas eval_nat_numeral = |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
73 |
nat_numeral_Bit0 nat_numeral_Bit1 |
35216 | 74 |
|
36699
816da1023508
moved nat_arith ot Nat_Numeral: clarified normalizer setup
haftmann
parents:
35815
diff
changeset
|
75 |
lemmas nat_arith = |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
76 |
diff_nat_numeral |
36699
816da1023508
moved nat_arith ot Nat_Numeral: clarified normalizer setup
haftmann
parents:
35815
diff
changeset
|
77 |
|
36716 | 78 |
lemmas semiring_norm = |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
79 |
Let_def arith_simps nat_arith rel_simps |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
80 |
if_False if_True |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
81 |
add_0 add_Suc add_numeral_left |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
82 |
add_neg_numeral_left mult_numeral_left |
36716 | 83 |
numeral_1_eq_1 [symmetric] Suc_eq_plus1 |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
84 |
eq_numeral_iff_iszero not_iszero_Numeral1 |
36716 | 85 |
|
23164 | 86 |
lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)" |
33296
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset
|
87 |
by (fact Let_def) |
23164 | 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 |
||
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
97 |
subsubsection{*For simplifying @{term "Suc m - K"} and @{term "K - Suc m"}*} |
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
98 |
|
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
99 |
text{*Where K above is a literal*} |
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
100 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
101 |
lemma Suc_diff_eq_diff_pred: "0 < n ==> Suc m - n = m - (n - Numeral1)" |
35216 | 102 |
by (simp split: nat_diff_split) |
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
103 |
|
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
104 |
text{*No longer required as a simprule because of the @{text inverse_fold} |
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
105 |
simproc*} |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
106 |
lemma Suc_diff_numeral: "Suc m - (numeral v) = m - (numeral v - 1)" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
107 |
by (subst expand_Suc, simp only: diff_Suc_Suc) |
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
108 |
|
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
109 |
lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n" |
35216 | 110 |
by (simp split: nat_diff_split) |
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
111 |
|
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
112 |
|
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
113 |
subsubsection{*For @{term nat_case} and @{term nat_rec}*} |
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
114 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
115 |
lemma nat_case_numeral [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
116 |
"nat_case a f (numeral v) = (let pv = nat (numeral v - 1) in f pv)" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
117 |
by (subst expand_Suc, simp only: nat.cases nat_numeral_diff_1 Let_def) |
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
118 |
|
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
119 |
lemma nat_case_add_eq_if [simp]: |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
120 |
"nat_case a f ((numeral v) + n) = (let pv = nat (numeral v - 1) in f (pv + n))" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
121 |
by (subst expand_Suc, simp only: nat.cases nat_numeral_diff_1 Let_def add_Suc) |
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
122 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
123 |
lemma nat_rec_numeral [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
124 |
"nat_rec a f (numeral v) = (let pv = nat (numeral v - 1) in f pv (nat_rec a f pv))" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
125 |
by (subst expand_Suc, simp only: nat_rec_Suc nat_numeral_diff_1 Let_def) |
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
126 |
|
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
127 |
lemma nat_rec_add_eq_if [simp]: |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
128 |
"nat_rec a f (numeral v + n) = |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
129 |
(let pv = nat (numeral v - 1) in f (pv + n) (nat_rec a f (pv + n)))" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
130 |
by (subst expand_Suc, simp only: nat_rec_Suc nat_numeral_diff_1 Let_def add_Suc) |
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
131 |
|
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
132 |
|
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
133 |
subsubsection{*Various Other Lemmas*} |
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
134 |
|
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
135 |
text {*Evens and Odds, for Mutilated Chess Board*} |
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
136 |
|
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
137 |
text{*Lemmas for specialist use, NOT as default simprules*} |
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
138 |
lemma nat_mult_2: "2 * z = (z+z::nat)" |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
139 |
by (rule mult_2) (* FIXME: duplicate *) |
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
140 |
|
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
141 |
lemma nat_mult_2_right: "z * 2 = (z+z::nat)" |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
142 |
by (rule mult_2_right) (* FIXME: duplicate *) |
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
143 |
|
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
144 |
text{*Case analysis on @{term "n<2"}*} |
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
145 |
lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0" |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
146 |
by (auto simp add: numeral_2_eq_2) |
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
147 |
|
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
148 |
text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*} |
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
149 |
|
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
150 |
lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)" |
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
151 |
by simp |
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
152 |
|
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
153 |
lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)" |
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
154 |
by simp |
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
155 |
|
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
156 |
text{*Can be used to eliminate long strings of Sucs, but not by default*} |
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
157 |
lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n" |
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
158 |
by simp |
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset
|
159 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
160 |
text{*Legacy theorems*} |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
161 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
162 |
lemmas nat_1_add_1 = one_add_one [where 'a=nat] |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46026
diff
changeset
|
163 |
|
31096 | 164 |
end |