10 |
10 |
11 subsection {* The Integers *} |
11 subsection {* The Integers *} |
12 |
12 |
13 text {* Addition *} |
13 text {* Addition *} |
14 |
14 |
15 lemma "(#13::int) + #19 = #32" |
15 lemma "(# 13::int) + # 19 = # 32" |
16 by simp |
16 by simp |
17 |
17 |
18 lemma "(#1234::int) + #5678 = #6912" |
18 lemma "(# 1234::int) + # 5678 = # 6912" |
19 by simp |
19 by simp |
20 |
20 |
21 lemma "(#1359::int) + #-2468 = #-1109" |
21 lemma "(# 1359::int) + # -2468 = # -1109" |
22 by simp |
22 by simp |
23 |
23 |
24 lemma "(#93746::int) + #-46375 = #47371" |
24 lemma "(# 93746::int) + # -46375 = # 47371" |
25 by simp |
25 by simp |
26 |
26 |
27 |
27 |
28 text {* \medskip Negation *} |
28 text {* \medskip Negation *} |
29 |
29 |
30 lemma "- (#65745::int) = #-65745" |
30 lemma "- (# 65745::int) = # -65745" |
31 by simp |
31 by simp |
32 |
32 |
33 lemma "- (#-54321::int) = #54321" |
33 lemma "- (# -54321::int) = # 54321" |
34 by simp |
34 by simp |
35 |
35 |
36 |
36 |
37 text {* \medskip Multiplication *} |
37 text {* \medskip Multiplication *} |
38 |
38 |
39 lemma "(#13::int) * #19 = #247" |
39 lemma "(# 13::int) * # 19 = # 247" |
40 by simp |
40 by simp |
41 |
41 |
42 lemma "(#-84::int) * #51 = #-4284" |
42 lemma "(# -84::int) * # 51 = # -4284" |
43 by simp |
43 by simp |
44 |
44 |
45 lemma "(#255::int) * #255 = #65025" |
45 lemma "(# 255::int) * # 255 = # 65025" |
46 by simp |
46 by simp |
47 |
47 |
48 lemma "(#1359::int) * #-2468 = #-3354012" |
48 lemma "(# 1359::int) * # -2468 = # -3354012" |
49 by simp |
49 by simp |
50 |
50 |
51 lemma "(#89::int) * #10 \<noteq> #889" |
51 lemma "(# 89::int) * # 10 \<noteq> # 889" |
52 by simp |
52 by simp |
53 |
53 |
54 lemma "(#13::int) < #18 - #4" |
54 lemma "(# 13::int) < # 18 - # 4" |
55 by simp |
55 by simp |
56 |
56 |
57 lemma "(#-345::int) < #-242 + #-100" |
57 lemma "(# -345::int) < # -242 + # -100" |
58 by simp |
58 by simp |
59 |
59 |
60 lemma "(#13557456::int) < #18678654" |
60 lemma "(# 13557456::int) < # 18678654" |
61 by simp |
61 by simp |
62 |
62 |
63 lemma "(#999999::int) \<le> (#1000001 + #1) - #2" |
63 lemma "(# 999999::int) \<le> (# 1000001 + Numeral1) - # 2" |
64 by simp |
64 by simp |
65 |
65 |
66 lemma "(#1234567::int) \<le> #1234567" |
66 lemma "(# 1234567::int) \<le> # 1234567" |
67 by simp |
67 by simp |
68 |
68 |
69 |
69 |
70 text {* \medskip Quotient and Remainder *} |
70 text {* \medskip Quotient and Remainder *} |
71 |
71 |
72 lemma "(#10::int) div #3 = #3" |
72 lemma "(# 10::int) div # 3 = # 3" |
73 by simp |
73 by simp |
74 |
74 |
75 lemma "(#10::int) mod #3 = #1" |
75 lemma "(# 10::int) mod # 3 = Numeral1" |
76 by simp |
76 by simp |
77 |
77 |
78 text {* A negative divisor *} |
78 text {* A negative divisor *} |
79 |
79 |
80 lemma "(#10::int) div #-3 = #-4" |
80 lemma "(# 10::int) div # -3 = # -4" |
81 by simp |
81 by simp |
82 |
82 |
83 lemma "(#10::int) mod #-3 = #-2" |
83 lemma "(# 10::int) mod # -3 = # -2" |
84 by simp |
84 by simp |
85 |
85 |
86 text {* |
86 text {* |
87 A negative dividend\footnote{The definition agrees with mathematical |
87 A negative dividend\footnote{The definition agrees with mathematical |
88 convention but not with the hardware of most computers} |
88 convention but not with the hardware of most computers} |
89 *} |
89 *} |
90 |
90 |
91 lemma "(#-10::int) div #3 = #-4" |
91 lemma "(# -10::int) div # 3 = # -4" |
92 by simp |
92 by simp |
93 |
93 |
94 lemma "(#-10::int) mod #3 = #2" |
94 lemma "(# -10::int) mod # 3 = # 2" |
95 by simp |
95 by simp |
96 |
96 |
97 text {* A negative dividend \emph{and} divisor *} |
97 text {* A negative dividend \emph{and} divisor *} |
98 |
98 |
99 lemma "(#-10::int) div #-3 = #3" |
99 lemma "(# -10::int) div # -3 = # 3" |
100 by simp |
100 by simp |
101 |
101 |
102 lemma "(#-10::int) mod #-3 = #-1" |
102 lemma "(# -10::int) mod # -3 = # -1" |
103 by simp |
103 by simp |
104 |
104 |
105 text {* A few bigger examples *} |
105 text {* A few bigger examples *} |
106 |
106 |
107 lemma "(#8452::int) mod #3 = #1" |
107 lemma "(# 8452::int) mod # 3 = Numeral1" |
108 by simp |
108 by simp |
109 |
109 |
110 lemma "(#59485::int) div #434 = #137" |
110 lemma "(# 59485::int) div # 434 = # 137" |
111 by simp |
111 by simp |
112 |
112 |
113 lemma "(#1000006::int) mod #10 = #6" |
113 lemma "(# 1000006::int) mod # 10 = # 6" |
114 by simp |
114 by simp |
115 |
115 |
116 |
116 |
117 text {* \medskip Division by shifting *} |
117 text {* \medskip Division by shifting *} |
118 |
118 |
119 lemma "#10000000 div #2 = (#5000000::int)" |
119 lemma "# 10000000 div # 2 = (# 5000000::int)" |
120 by simp |
120 by simp |
121 |
121 |
122 lemma "#10000001 mod #2 = (#1::int)" |
122 lemma "# 10000001 mod # 2 = (Numeral1::int)" |
123 by simp |
123 by simp |
124 |
124 |
125 lemma "#10000055 div #32 = (#312501::int)" |
125 lemma "# 10000055 div # 32 = (# 312501::int)" |
126 by simp |
126 by simp |
127 |
127 |
128 lemma "#10000055 mod #32 = (#23::int)" |
128 lemma "# 10000055 mod # 32 = (# 23::int)" |
129 by simp |
129 by simp |
130 |
130 |
131 lemma "#100094 div #144 = (#695::int)" |
131 lemma "# 100094 div # 144 = (# 695::int)" |
132 by simp |
132 by simp |
133 |
133 |
134 lemma "#100094 mod #144 = (#14::int)" |
134 lemma "# 100094 mod # 144 = (# 14::int)" |
135 by simp |
135 by simp |
136 |
136 |
137 |
137 |
138 subsection {* The Natural Numbers *} |
138 subsection {* The Natural Numbers *} |
139 |
139 |
140 text {* Successor *} |
140 text {* Successor *} |
141 |
141 |
142 lemma "Suc #99999 = #100000" |
142 lemma "Suc # 99999 = # 100000" |
143 by (simp add: Suc_nat_number_of) |
143 by (simp add: Suc_nat_number_of) |
144 -- {* not a default rewrite since sometimes we want to have @{text "Suc #nnn"} *} |
144 -- {* not a default rewrite since sometimes we want to have @{text "Suc #nnn"} *} |
145 |
145 |
146 |
146 |
147 text {* \medskip Addition *} |
147 text {* \medskip Addition *} |
148 |
148 |
149 lemma "(#13::nat) + #19 = #32" |
149 lemma "(# 13::nat) + # 19 = # 32" |
150 by simp |
150 by simp |
151 |
151 |
152 lemma "(#1234::nat) + #5678 = #6912" |
152 lemma "(# 1234::nat) + # 5678 = # 6912" |
153 by simp |
153 by simp |
154 |
154 |
155 lemma "(#973646::nat) + #6475 = #980121" |
155 lemma "(# 973646::nat) + # 6475 = # 980121" |
156 by simp |
156 by simp |
157 |
157 |
158 |
158 |
159 text {* \medskip Subtraction *} |
159 text {* \medskip Subtraction *} |
160 |
160 |
161 lemma "(#32::nat) - #14 = #18" |
161 lemma "(# 32::nat) - # 14 = # 18" |
162 by simp |
162 by simp |
163 |
163 |
164 lemma "(#14::nat) - #15 = #0" |
164 lemma "(# 14::nat) - # 15 = Numeral0" |
165 by simp |
165 by simp |
166 |
166 |
167 lemma "(#14::nat) - #1576644 = #0" |
167 lemma "(# 14::nat) - # 1576644 = Numeral0" |
168 by simp |
168 by simp |
169 |
169 |
170 lemma "(#48273776::nat) - #3873737 = #44400039" |
170 lemma "(# 48273776::nat) - # 3873737 = # 44400039" |
171 by simp |
171 by simp |
172 |
172 |
173 |
173 |
174 text {* \medskip Multiplication *} |
174 text {* \medskip Multiplication *} |
175 |
175 |
176 lemma "(#12::nat) * #11 = #132" |
176 lemma "(# 12::nat) * # 11 = # 132" |
177 by simp |
177 by simp |
178 |
178 |
179 lemma "(#647::nat) * #3643 = #2357021" |
179 lemma "(# 647::nat) * # 3643 = # 2357021" |
180 by simp |
180 by simp |
181 |
181 |
182 |
182 |
183 text {* \medskip Quotient and Remainder *} |
183 text {* \medskip Quotient and Remainder *} |
184 |
184 |
185 lemma "(#10::nat) div #3 = #3" |
185 lemma "(# 10::nat) div # 3 = # 3" |
186 by simp |
186 by simp |
187 |
187 |
188 lemma "(#10::nat) mod #3 = #1" |
188 lemma "(# 10::nat) mod # 3 = Numeral1" |
189 by simp |
189 by simp |
190 |
190 |
191 lemma "(#10000::nat) div #9 = #1111" |
191 lemma "(# 10000::nat) div # 9 = # 1111" |
192 by simp |
192 by simp |
193 |
193 |
194 lemma "(#10000::nat) mod #9 = #1" |
194 lemma "(# 10000::nat) mod # 9 = Numeral1" |
195 by simp |
195 by simp |
196 |
196 |
197 lemma "(#10000::nat) div #16 = #625" |
197 lemma "(# 10000::nat) div # 16 = # 625" |
198 by simp |
198 by simp |
199 |
199 |
200 lemma "(#10000::nat) mod #16 = #0" |
200 lemma "(# 10000::nat) mod # 16 = Numeral0" |
201 by simp |
201 by simp |
202 |
202 |
203 |
203 |
204 text {* \medskip Testing the cancellation of complementary terms *} |
204 text {* \medskip Testing the cancellation of complementary terms *} |
205 |
205 |
206 lemma "y + (x + -x) = (#0::int) + y" |
206 lemma "y + (x + -x) = (Numeral0::int) + y" |
207 by simp |
207 by simp |
208 |
208 |
209 lemma "y + (-x + (- y + x)) = (#0::int)" |
209 lemma "y + (-x + (- y + x)) = (Numeral0::int)" |
210 by simp |
210 by simp |
211 |
211 |
212 lemma "-x + (y + (- y + x)) = (#0::int)" |
212 lemma "-x + (y + (- y + x)) = (Numeral0::int)" |
213 by simp |
213 by simp |
214 |
214 |
215 lemma "x + (x + (- x + (- x + (- y + - z)))) = (#0::int) - y - z" |
215 lemma "x + (x + (- x + (- x + (- y + - z)))) = (Numeral0::int) - y - z" |
216 by simp |
216 by simp |
217 |
217 |
218 lemma "x + x - x - x - y - z = (#0::int) - y - z" |
218 lemma "x + x - x - x - y - z = (Numeral0::int) - y - z" |
219 by simp |
219 by simp |
220 |
220 |
221 lemma "x + y + z - (x + z) = y - (#0::int)" |
221 lemma "x + y + z - (x + z) = y - (Numeral0::int)" |
222 by simp |
222 by simp |
223 |
223 |
224 lemma "x + (y + (y + (y + (-x + -x)))) = (#0::int) + y - x + y + y" |
224 lemma "x + (y + (y + (y + (-x + -x)))) = (Numeral0::int) + y - x + y + y" |
225 by simp |
225 by simp |
226 |
226 |
227 lemma "x + (y + (y + (y + (-y + -x)))) = y + (#0::int) + y" |
227 lemma "x + (y + (y + (y + (-y + -x)))) = y + (Numeral0::int) + y" |
228 by simp |
228 by simp |
229 |
229 |
230 lemma "x + y - x + z - x - y - z + x < (#1::int)" |
230 lemma "x + y - x + z - x - y - z + x < (Numeral1::int)" |
231 by simp |
231 by simp |
232 |
232 |
233 |
233 |
234 subsection {* Normal form of bit strings *} |
234 subsection {* Normal form of bit strings *} |
235 |
235 |