numeralScript.sml
1(*---------------------------------------------------------------------------
2
3 Development of a theory of numerals, including rewrite theorems for
4 the basic arithmetic operations and relations.
5
6 Michael Norrish, December 1998
7
8 Inspired by a similar development done by John Harrison for his
9 HOL Light theorem prover.
10
11 ---------------------------------------------------------------------------*)
12
13
14(* for interactive development of this theory; evaluate the following
15 commands before trying to evaluate the ML that follows.
16
17 fun mload s = (print ("Loading "^s^"\n"); load s);
18 app mload ["simpLib", "boolSimps", "arithmeticTheory", "Q",
19 "mesonLib", "metisLib", "WhileTheory",
20 "pairSyntax", "combinSyntax"];
21*)
22Theory numeral[bare]
23Ancestors
24 arithmetic
25Libs
26 HolKernel boolLib simpLib Parse Prim_rec metisLib BasicProvers
27
28
29val bool_ss = boolSimps.bool_ss;
30
31val INV_SUC_EQ = prim_recTheory.INV_SUC_EQ
32and LESS_REFL = prim_recTheory.LESS_REFL
33and SUC_LESS = prim_recTheory.SUC_LESS
34and NOT_LESS_0 = prim_recTheory.NOT_LESS_0
35and LESS_MONO = prim_recTheory.LESS_MONO
36and LESS_SUC_REFL = prim_recTheory.LESS_SUC_REFL
37and LESS_SUC = prim_recTheory.LESS_SUC
38and LESS_THM = prim_recTheory.LESS_THM
39and LESS_SUC_IMP = prim_recTheory.LESS_SUC_IMP
40and LESS_0 = prim_recTheory.LESS_0
41and EQ_LESS = prim_recTheory.EQ_LESS
42and SUC_ID = prim_recTheory.SUC_ID
43and NOT_LESS_EQ = prim_recTheory.NOT_LESS_EQ
44and LESS_NOT_EQ = prim_recTheory.LESS_NOT_EQ
45and LESS_SUC_SUC = prim_recTheory.LESS_SUC_SUC
46and PRE = prim_recTheory.PRE
47and WF_LESS = prim_recTheory.WF_LESS;
48
49val NOT_SUC = numTheory.NOT_SUC
50and INV_SUC = numTheory.INV_SUC
51and INDUCTION = numTheory.INDUCTION
52and NUMERAL_DEF = arithmeticTheory.NUMERAL_DEF;
53
54val INDUCT_TAC = INDUCT_THEN INDUCTION ASSUME_TAC
55
56val _ = print "Developing rewrites for numeral addition\n"
57
58Theorem PRE_ADD[local]:
59 !n m. PRE (n + SUC m) = n + m
60Proof
61 INDUCT_TAC THEN SIMP_TAC bool_ss [ADD_CLAUSES, PRE]
62QED
63
64Theorem numeral_suc:
65 (SUC ZERO = BIT1 ZERO) /\
66 (!n. SUC (BIT1 n) = BIT2 n) /\
67 (!n. SUC (BIT2 n) = BIT1 (SUC n))
68Proof
69 SIMP_TAC bool_ss [BIT1, BIT2, ALT_ZERO, ADD_CLAUSES]
70QED
71
72
73(*---------------------------------------------------------------------------*)
74(* Internal markers. Throughout this theory, we will be using various *)
75(* internal markers that represent some intermediate result within an *)
76(* algorithm. All such markers are constants with names that have *)
77(* leading i's *)
78(*---------------------------------------------------------------------------*)
79
80val iZ = new_definition("iZ", ``iZ (x:num) = x``);
81
82val iiSUC = new_definition("iiSUC", ``iiSUC n = SUC (SUC n)``);
83
84local open OpenTheoryMap in
85val _ = OpenTheory_const_name
86 {const={Thy="numeral",Name="iZ"},name=(["Unwanted"],"id")}
87fun OpenTheory_add s = OpenTheory_const_name
88 {const={Thy="numeral",Name=s},name=(["HOL4","Numeral"],s)}
89val _ = OpenTheory_add "iiSUC"
90end
91
92Theorem numeral_distrib: (!n. 0 + n = n) /\ (!n. n + 0 = n) /\
93 (!n m. NUMERAL n + NUMERAL m = NUMERAL (iZ (n + m))) /\
94 (!n. 0 * n = 0) /\ (!n. n * 0 = 0) /\
95 (!n m. NUMERAL n * NUMERAL m = NUMERAL (n * m)) /\
96 (!n. 0 - n = 0) /\ (!n. n - 0 = n) /\
97 (!n m. NUMERAL n - NUMERAL m = NUMERAL (n - m)) /\
98 (!n. 0 EXP (NUMERAL (BIT1 n)) = 0) /\
99 (!n. 0 EXP (NUMERAL (BIT2 n)) = 0) /\
100 (!n. n EXP 0 = 1) /\
101 (!n m. (NUMERAL n) EXP (NUMERAL m) = NUMERAL (n EXP m)) /\
102 (SUC 0 = 1) /\
103 (!n. SUC(NUMERAL n) = NUMERAL (SUC n)) /\
104 (PRE 0 = 0) /\
105 (!n. PRE(NUMERAL n) = NUMERAL (PRE n)) /\
106 (!n. (NUMERAL n = 0) = (n = ZERO)) /\
107 (!n. (0 = NUMERAL n) = (n = ZERO)) /\
108 (!n m. (NUMERAL n = NUMERAL m) = (n=m)) /\
109 (!n. n < 0 <=> F) /\ (!n. 0 < NUMERAL n <=> ZERO < n) /\
110 (!n m. NUMERAL n < NUMERAL m <=> n<m) /\
111 (!n. 0 > n <=> F) /\ (!n. NUMERAL n > 0 <=> ZERO < n) /\
112 (!n m. NUMERAL n > NUMERAL m <=> m<n) /\
113 (!n. 0 <= n <=> T) /\ (!n. NUMERAL n <= 0 <=> n <= ZERO) /\
114 (!n m. NUMERAL n <= NUMERAL m <=> n<=m) /\
115 (!n. n >= 0 <=> T) /\ (!n. 0 >= n <=> (n = 0)) /\
116 (!n m. NUMERAL n >= NUMERAL m <=> m <= n) /\
117 (!n. ODD (NUMERAL n) = ODD n) /\ (!n. EVEN (NUMERAL n) = EVEN n) /\
118 ~ODD 0 /\ EVEN 0
119Proof
120 SIMP_TAC bool_ss [NUMERAL_DEF, GREATER_DEF, iZ, GREATER_OR_EQ,
121 LESS_OR_EQ, EQ_IMP_THM, DISJ_IMP_THM, ADD_CLAUSES,
122 ALT_ZERO, MULT_CLAUSES, EXP, PRE, NOT_LESS_0, SUB_0,
123 BIT1, BIT2, ODD, EVEN] THEN
124 mesonLib.MESON_TAC [LESS_0_CASES]
125QED
126
127Theorem numeral_iisuc: (iiSUC ZERO = BIT2 ZERO) /\
128 (iiSUC (BIT1 n) = BIT1 (SUC n)) /\
129 (iiSUC (BIT2 n) = BIT2 (SUC n))
130Proof
131 SIMP_TAC bool_ss [BIT1, BIT2, iiSUC, ALT_ZERO, ADD_CLAUSES]
132QED
133
134
135(*---------------------------------------------------------------------------*)
136(* The following addition algorithm makes use of internal markers iZ and *)
137(* iiSUC. *)
138(* *)
139(* iZ is used to mark the place where the algorithm is currently working. *)
140(* Without a rule such as the fourth below would give the rewriter a chance *)
141(* to rewrite away an addition under a SUC, which we don't want. *)
142(* *)
143(* SUC is used as an internal marker to represent carrying one, while *)
144(* iiSUC is used to represent carrying two (necessary with our *)
145(* formulation of numerals). *)
146(*---------------------------------------------------------------------------*)
147
148Theorem numeral_add: !n m.
149 (iZ (ZERO + n) = n) /\
150 (iZ (n + ZERO) = n) /\
151 (iZ (BIT1 n + BIT1 m) = BIT2 (iZ (n + m))) /\
152 (iZ (BIT1 n + BIT2 m) = BIT1 (SUC (n + m))) /\
153 (iZ (BIT2 n + BIT1 m) = BIT1 (SUC (n + m))) /\
154 (iZ (BIT2 n + BIT2 m) = BIT2 (SUC (n + m))) /\
155 (SUC (ZERO + n) = SUC n) /\
156 (SUC (n + ZERO) = SUC n) /\
157 (SUC (BIT1 n + BIT1 m) = BIT1 (SUC (n + m))) /\
158 (SUC (BIT1 n + BIT2 m) = BIT2 (SUC (n + m))) /\
159 (SUC (BIT2 n + BIT1 m) = BIT2 (SUC (n + m))) /\
160 (SUC (BIT2 n + BIT2 m) = BIT1 (iiSUC (n + m))) /\
161 (iiSUC (ZERO + n) = iiSUC n) /\
162 (iiSUC (n + ZERO) = iiSUC n) /\
163 (iiSUC (BIT1 n + BIT1 m) = BIT2 (SUC (n + m))) /\
164 (iiSUC (BIT1 n + BIT2 m) = BIT1 (iiSUC (n + m))) /\
165 (iiSUC (BIT2 n + BIT1 m) = BIT1 (iiSUC (n + m))) /\
166 (iiSUC (BIT2 n + BIT2 m) = BIT2 (iiSUC (n + m)))
167Proof
168 SIMP_TAC bool_ss [BIT1, BIT2, iZ, iiSUC,ADD_CLAUSES, INV_SUC_EQ, ALT_ZERO] >>
169 REPEAT GEN_TAC >> CONV_TAC (AC_CONV(ADD_ASSOC, ADD_SYM))
170QED
171
172(*---------------------------------------------------------------------------*)
173(* rewrites needed for addition *)
174(*---------------------------------------------------------------------------*)
175
176val add_rwts = [numeral_distrib, numeral_add, numeral_suc, numeral_iisuc]
177
178val numeral_proof_rwts = [BIT1, BIT2, INV_SUC_EQ,
179 NUMERAL_DEF, iZ, iiSUC, ADD_CLAUSES, NOT_SUC,
180 SUC_NOT, LESS_0, NOT_LESS_0, ALT_ZERO]
181
182Theorem double_add_not_SUC[local]:
183 !n m.
184 ~(SUC (n + n) = m + m) /\ ~(m + m = SUC (n + n))
185Proof
186 INDUCT_TAC THEN SIMP_TAC bool_ss numeral_proof_rwts THEN
187 INDUCT_TAC THEN ASM_SIMP_TAC bool_ss numeral_proof_rwts
188QED
189
190
191val _ = print "Developing numeral rewrites for relations\n"
192
193Theorem numeral_eq:
194 !n m.
195 ((ZERO = BIT1 n) = F) /\
196 ((BIT1 n = ZERO) = F) /\
197 ((ZERO = BIT2 n) = F) /\
198 ((BIT2 n = ZERO) = F) /\
199 ((BIT1 n = BIT2 m) = F) /\
200 ((BIT2 n = BIT1 m) = F) /\
201 ((BIT1 n = BIT1 m) = (n = m)) /\
202 ((BIT2 n = BIT2 m) = (n = m))
203Proof
204 SIMP_TAC bool_ss numeral_proof_rwts THEN
205 INDUCT_TAC THEN
206 SIMP_TAC bool_ss (double_add_not_SUC::numeral_proof_rwts) THEN
207 INDUCT_TAC THEN ASM_SIMP_TAC bool_ss numeral_proof_rwts
208QED
209
210
211fun ncases str n0 =
212 DISJ_CASES_THEN2 SUBST_ALL_TAC
213 (X_CHOOSE_THEN (mk_var(n0, (==`:num`==))) SUBST_ALL_TAC)
214 (SPEC (mk_var(str, (==`:num`==))) num_CASES)
215
216Theorem double_less[local]:
217 !n m. (n + n < m + m <=> n < m) /\ (n + n <= m + m <=> n <= m)
218Proof
219 INDUCT_TAC THEN GEN_TAC THEN ncases "m" "m0" THEN
220 ASM_SIMP_TAC bool_ss [ADD_CLAUSES, NOT_LESS_0, LESS_0, LESS_MONO_EQ,
221 ZERO_LESS_EQ, NOT_SUC_LESS_EQ_0, LESS_EQ_MONO]
222QED
223
224
225Theorem double_1suc_less[local]:
226 !x y. (SUC(x + x) < y + y <=> x < y) /\
227 (SUC(x + x) <= y + y <=> x < y) /\
228 (x + x < SUC(y + y) <=> ~(y < x)) /\
229 (x + x <= SUC(y + y) <=> ~(y < x))
230Proof
231 INDUCT_TAC THEN GEN_TAC THEN ncases "y" "y0" THEN
232 ASM_SIMP_TAC bool_ss [ADD_CLAUSES, LESS_EQ_MONO, NOT_LESS_0,
233 ZERO_LESS_EQ, NOT_SUC_LESS_EQ_0, LESS_0,
234 LESS_MONO_EQ]
235QED
236
237Theorem double_2suc_less[local]:
238 !n m. (n + n < SUC (SUC (m + m)) <=> n < SUC m) /\
239 (SUC (SUC (m + m)) < n + n <=> SUC m < n) /\
240 (n + n <= SUC (SUC (m + m)) <=> n <= SUC m) /\
241 (SUC (SUC (m + m)) <= n + n <=> SUC m <= n)
242Proof
243ONCE_REWRITE_TAC [GSYM (el 4 (CONJUNCTS ADD_CLAUSES))] THEN
244ONCE_REWRITE_TAC [GSYM (el 3 (CONJUNCTS ADD_CLAUSES))] THEN
245REWRITE_TAC [double_less]
246QED
247
248val DOUBLE_FACTS = LIST_CONJ [double_less, double_1suc_less, double_2suc_less]
249
250Theorem numeral_lt: !n m.
251 (ZERO < BIT1 n <=> T) /\
252 (ZERO < BIT2 n <=> T) /\
253 (n < ZERO <=> F) /\
254 (BIT1 n < BIT1 m <=> n < m) /\
255 (BIT2 n < BIT2 m <=> n < m) /\
256 (BIT1 n < BIT2 m <=> ~(m < n)) /\
257 (BIT2 n < BIT1 m <=> n < m)
258Proof
259 SIMP_TAC bool_ss (DOUBLE_FACTS::LESS_MONO_EQ::numeral_proof_rwts)
260QED
261
262(*---------------------------------------------------------------------------*)
263(* I've kept this rewrite entirely independent of the above. I don't if *)
264(* this is a good idea or not. *)
265(*---------------------------------------------------------------------------*)
266
267Theorem numeral_lte: !n m. (ZERO <= n <=> T) /\
268 (BIT1 n <= ZERO <=> F) /\
269 (BIT2 n <= ZERO <=> F) /\
270 (BIT1 n <= BIT1 m <=> n <= m) /\
271 (BIT1 n <= BIT2 m <=> n <= m) /\
272 (BIT2 n <= BIT1 m <=> ~(m <= n)) /\
273 (BIT2 n <= BIT2 m <=> n <= m)
274Proof
275 SIMP_TAC bool_ss ([DOUBLE_FACTS, LESS_MONO_EQ, LESS_EQ_MONO] @
276 (map (REWRITE_RULE [NUMERAL_DEF])
277 [ZERO_LESS_EQ, NOT_SUC_LESS_EQ_0, NOT_LESS]) @
278 numeral_proof_rwts) THEN
279 SIMP_TAC bool_ss [GSYM NOT_LESS]
280QED
281
282val _ = print "Developing numeral rewrites for subtraction\n";
283val _ = print " (includes initiality theorem for bit functions)\n";
284
285Theorem numeral_pre:
286 (PRE ZERO = ZERO) /\
287 (PRE (BIT1 ZERO) = ZERO) /\
288 (!n. PRE (BIT1 (BIT1 n)) = BIT2 (PRE (BIT1 n))) /\
289 (!n. PRE (BIT1 (BIT2 n)) = BIT2 (BIT1 n)) /\
290 (!n. PRE (BIT2 n) = BIT1 n)
291Proof
292 SIMP_TAC bool_ss [BIT1, BIT2, PRE, PRE_ADD,
293 ADD_CLAUSES, ADD_ASSOC, PRE, ALT_ZERO]
294QED
295
296(*---------------------------------------------------------------------------*)
297(* We could just go on and prove similar rewrites for subtraction, but *)
298(* they get a bit inefficient because every iteration of the rewriting *)
299(* ends up checking whether or not x < y. To get around this, we prove *)
300(* initiality for our BIT functions and ZERO, and then define a function *)
301(* which implements bitwise subtraction for x and y, assuming that x is *)
302(* at least as big as y. *)
303(*---------------------------------------------------------------------------*)
304
305(* Measure function for WF recursion construction *)
306val our_M = Term
307 `\f a. if a = ZERO then (zf:'a) else
308 if (?n. (a = BIT1 n))
309 then (b1f:num->'a->'a)
310 (@n. a = BIT1 n) (f (@n. a = BIT1 n))
311 else b2f (@n. a = BIT2 n) (f (@n. a = BIT2 n))`;
312
313
314fun AP_TAC (asl, g) =
315 let val _ = is_eq g orelse raise Fail "Goal not an equality"
316 val (lhs, rhs) = dest_eq g
317 val (lf, la) = dest_comb lhs handle _ =>
318 raise Fail "lhs must be an application"
319 val (rf, ra) = dest_comb rhs handle _ =>
320 raise Fail "rhs must be an application"
321 in
322 if (term_eq lf rf) then AP_TERM_TAC (asl, g) else
323 if (term_eq la ra) then AP_THM_TAC (asl, g) else
324 raise Fail "One of function or argument must be equal"
325 end
326
327val APn_TAC = REPEAT AP_TAC;
328
329
330Theorem bit_initiality: !zf b1f b2f.
331 ?f.
332 (f ZERO = zf) /\
333 (!n. f (BIT1 n) = b1f n (f n)) /\
334 (!n. f (BIT2 n) = b2f n (f n))
335Proof
336 REPEAT STRIP_TAC THEN
337 ASSUME_TAC
338 (MP (INST_TYPE [Type.beta |-> Type.alpha]
339 (ISPEC “$<” relationTheory.WF_RECURSION_THM))
340 WF_LESS) THEN
341 POP_ASSUM (STRIP_ASSUME_TAC o CONJUNCT1 o
342 SIMP_RULE bool_ss [EXISTS_UNIQUE_DEF] o
343 ISPEC our_M) THEN
344 Q.EXISTS_TAC `f` THEN REPEAT CONJ_TAC THENL [
345 ASM_SIMP_TAC bool_ss [],
346 GEN_TAC THEN
347 FIRST_ASSUM (fn th => CONV_TAC (LHS_CONV (REWR_CONV th))) THEN
348 SIMP_TAC bool_ss [numeral_eq] THEN AP_TAC THEN
349 SIMP_TAC bool_ss [relationTheory.RESTRICT_DEF, BIT1] THEN
350 ONCE_REWRITE_TAC [ADD_CLAUSES] THEN REWRITE_TAC [LESS_ADD_SUC],
351 GEN_TAC THEN
352 FIRST_ASSUM (fn th => CONV_TAC (LHS_CONV (REWR_CONV th))) THEN
353 SIMP_TAC bool_ss [numeral_eq] THEN AP_TAC THEN
354 SIMP_TAC bool_ss [relationTheory.RESTRICT_DEF, BIT2] THEN
355 ONCE_REWRITE_TAC [ADD_CLAUSES] THEN REWRITE_TAC [LESS_ADD_SUC]
356 ]
357QED
358
359Theorem bit_cases[local]:
360 !n. (n = ZERO) \/ (?b1. n = BIT1 b1) \/ (?b2. n = BIT2 b2)
361Proof
362INDUCT_TAC THENL [
363 SIMP_TAC bool_ss [ALT_ZERO],
364 POP_ASSUM (STRIP_ASSUME_TAC) THEN POP_ASSUM SUBST_ALL_TAC THENL [
365 DISJ2_TAC THEN DISJ1_TAC THEN EXISTS_TAC (Term`ZERO`) THEN
366 REWRITE_TAC [numeral_suc],
367 DISJ2_TAC THEN DISJ2_TAC THEN Q.EXISTS_TAC `b1` THEN
368 SIMP_TAC bool_ss [BIT1, BIT2, ADD_CLAUSES],
369 DISJ2_TAC THEN DISJ1_TAC THEN Q.EXISTS_TAC `SUC b2` THEN
370 SIMP_TAC bool_ss [BIT1, BIT2, ADD_CLAUSES]
371 ]
372]
373QED
374
375Theorem old_style_bit_initiality[local]:
376 !zf b1f b2f.
377 ?!f.
378 (f ZERO = zf) /\
379 (!n. f (BIT1 n) = b1f (f n) n) /\
380 (!n. f (BIT2 n) = b2f (f n) n)
381Proof
382 REPEAT GEN_TAC THEN CONV_TAC EXISTS_UNIQUE_CONV THEN CONJ_TAC THENL [
383 STRIP_ASSUME_TAC
384 (Q.SPECL [`zf`, `\n a. b1f a n`, `\n a. b2f a n`] bit_initiality) THEN
385 RULE_ASSUM_TAC BETA_RULE THEN mesonLib.ASM_MESON_TAC [],
386 REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN
387 INDUCT_THEN (MATCH_MP relationTheory.WF_INDUCTION_THM WF_LESS)
388 STRIP_ASSUME_TAC THEN
389 (* now do numeral cases on n *)
390 STRIP_ALL_THEN SUBST_ALL_TAC (SPEC_ALL bit_cases) THENL [
391 ASM_SIMP_TAC bool_ss [],
392 ASM_SIMP_TAC bool_ss [] THEN AP_TAC THEN AP_TAC THEN
393 FIRST_ASSUM MATCH_MP_TAC THEN SIMP_TAC bool_ss [BIT1] THEN
394 ONCE_REWRITE_TAC [ADD_CLAUSES] THEN REWRITE_TAC [LESS_ADD_SUC],
395 ASM_SIMP_TAC bool_ss [] THEN AP_TAC THEN AP_TAC THEN
396 FIRST_ASSUM MATCH_MP_TAC THEN SIMP_TAC bool_ss [BIT2] THEN
397 ONCE_REWRITE_TAC [ADD_CLAUSES] THEN REWRITE_TAC [LESS_ADD_SUC]
398 ]
399 ]
400QED
401
402
403(*---------------------------------------------------------------------------*)
404(* Now with bit initiality we can define our subtraction helper *)
405(* function. However, before doing this it's nice to have a cases *)
406(* function for the bit structure. *)
407(*---------------------------------------------------------------------------*)
408
409val iBIT_cases = new_recursive_definition {
410 def = Term`(iBIT_cases ZERO zf bf1 bf2 = zf) /\
411 (iBIT_cases (BIT1 n) zf bf1 bf2 = bf1 n) /\
412 (iBIT_cases (BIT2 n) zf bf1 bf2 = bf2 n)`,
413 name = "iBIT_cases",
414 rec_axiom = bit_initiality};
415val _ = OpenTheory_add"iBIT_cases"
416
417(*---------------------------------------------------------------------------*)
418(* Another internal marker, this one represents a zero digit. We can't *)
419(* avoid using this with subtraction because of the fact that when you *)
420(* subtract two big numbers that are close together, you will end up *)
421(* with a result that has a whole pile of leading zeroes. (The *)
422(* alternative is to construct an algorithm that stops whenever it *)
423(* notices that the two arguments are equal. This "looking ahead" would *)
424(* require a conditional rewrite, and this is not very appealing.) *)
425(*---------------------------------------------------------------------------*)
426
427val iDUB = new_definition("iDUB", “iDUB x = x + x”);
428val _ = OpenTheory_add "iDUB"
429
430(*---------------------------------------------------------------------------*)
431(* iSUB implements subtraction. When the first argument (a boolean) is *)
432(* true, it corresponds to simple subtraction, when it's false, it *)
433(* corresponds to subtraction and then less another one (i.e., with a *)
434(* one being carried. Note that iSUB's results include iDUB "zero *)
435(* digits"; these will be eliminated in a final phase of rewriting.) *)
436(*---------------------------------------------------------------------------*)
437
438val iSUB_DEF = new_recursive_definition {
439 def = Term`
440 (iSUB b ZERO x = ZERO) /\
441 (iSUB b (BIT1 n) x =
442 if b
443 then iBIT_cases x (BIT1 n)
444 (* BIT1 m *) (\m. iDUB (iSUB T n m))
445 (* BIT2 m *) (\m. BIT1 (iSUB F n m))
446 else iBIT_cases x (iDUB n)
447 (* BIT1 m *) (\m. BIT1 (iSUB F n m))
448 (* BIT2 m *) (\m. iDUB (iSUB F n m))) /\
449 (iSUB b (BIT2 n) x =
450 if b
451 then iBIT_cases x (BIT2 n)
452 (* BIT1 m *) (\m. BIT1 (iSUB T n m))
453 (* BIT2 m *) (\m. iDUB (iSUB T n m))
454 else iBIT_cases x (BIT1 n)
455 (* BIT1 m *) (\m. iDUB (iSUB T n m))
456 (* BIT2 m *) (\m. BIT1 (iSUB F n m)))`,
457 name = "iSUB_DEF",
458 rec_axiom = bit_initiality};
459val _ = OpenTheory_add"iSUB"
460
461Theorem bit_induction =
462 Prim_rec.prove_induction_thm old_style_bit_initiality;
463
464Theorem iSUB_ZERO[local]:
465 (!n b. iSUB b ZERO n = ZERO) /\
466 (!n. iSUB T n ZERO = n)
467Proof
468 SIMP_TAC bool_ss [iSUB_DEF] THEN GEN_TAC THEN
469 STRUCT_CASES_TAC (Q.SPEC `n` bit_cases) THEN
470 SIMP_TAC bool_ss [iSUB_DEF, iBIT_cases]
471QED
472
473(*---------------------------------------------------------------------------*)
474(* An equivalent form to the definition that doesn't need the cases theorem, *)
475(* and can thus be used by REWRITE_TAC. To get the other to work you need *)
476(* the simplifier because it needs to do beta-reduction of the arguments to *)
477(* iBIT_cases. Alternatively, the form of the arguments in iSUB_THM could *)
478(* be simply expressed as function composition without a lambda x present *)
479(* at all. *)
480(*---------------------------------------------------------------------------*)
481
482Theorem iSUB_THM: !b n m. (iSUB b ZERO x = ZERO) /\
483 (iSUB T n ZERO = n) /\
484 (iSUB F (BIT1 n) ZERO = iDUB n) /\
485 (iSUB T (BIT1 n) (BIT1 m) = iDUB (iSUB T n m)) /\
486 (iSUB F (BIT1 n) (BIT1 m) = BIT1 (iSUB F n m)) /\
487 (iSUB T (BIT1 n) (BIT2 m) = BIT1 (iSUB F n m)) /\
488 (iSUB F (BIT1 n) (BIT2 m) = iDUB (iSUB F n m)) /\
489
490 (iSUB F (BIT2 n) ZERO = BIT1 n) /\
491 (iSUB T (BIT2 n) (BIT1 m) = BIT1 (iSUB T n m)) /\
492 (iSUB F (BIT2 n) (BIT1 m) = iDUB (iSUB T n m)) /\
493 (iSUB T (BIT2 n) (BIT2 m) = iDUB (iSUB T n m)) /\
494 (iSUB F (BIT2 n) (BIT2 m) = BIT1 (iSUB F n m))
495Proof
496 SIMP_TAC bool_ss [iSUB_DEF, iBIT_cases, iSUB_ZERO]
497QED
498
499(*---------------------------------------------------------------------------*)
500(* Rewrites for relational expressions that can be used under the guards of *)
501(* conditional operators. *)
502(*---------------------------------------------------------------------------*)
503
504Theorem less_less_eqs[local]:
505 !n m. (n < m ==> ~(m <= n) /\ (m <= SUC n <=> (m = SUC n)) /\
506 ~(m + m <= n)) /\
507 (n <= m ==> ~(m < n) /\ (m <= n <=> (m = n)) /\
508 ~(SUC m <= n))
509Proof
510 REPEAT GEN_TAC THEN CONJ_TAC THEN STRIP_TAC THEN REPEAT CONJ_TAC THENL [
511 STRIP_TAC THEN MAP_EVERY IMP_RES_TAC [LESS_LESS_EQ_TRANS, LESS_REFL],
512 EQ_TAC THEN SIMP_TAC bool_ss [LESS_OR_EQ] THEN STRIP_TAC THEN
513 IMP_RES_TAC LESS_LESS_SUC,
514 POP_ASSUM MP_TAC THEN Q.SPEC_TAC (`m:num`, `m`) THEN INDUCT_TAC THENL [
515 SIMP_TAC bool_ss [NOT_LESS_0],
516 SIMP_TAC bool_ss [GSYM NOT_LESS] THEN REPEAT STRIP_TAC THEN
517 MATCH_MP_TAC LESS_TRANS THEN Q.EXISTS_TAC `SUC m` THEN
518 ASM_SIMP_TAC bool_ss [LESS_ADD_SUC]
519 ],
520 STRIP_TAC THEN MAP_EVERY IMP_RES_TAC [LESS_LESS_EQ_TRANS, LESS_REFL],
521 EQ_TAC THEN SIMP_TAC bool_ss [LESS_EQ_REFL] THEN STRIP_TAC THEN
522 IMP_RES_TAC LESS_EQUAL_ANTISYM,
523 SIMP_TAC bool_ss [GSYM NOT_LESS] THEN
524 ASM_SIMP_TAC bool_ss [LESS_EQ, LESS_EQ_MONO]
525 ]
526QED
527
528
529Theorem sub_facts[local]:
530 !m. (SUC (SUC m) - m = SUC (SUC 0)) /\
531 (SUC m - m = SUC 0) /\
532 (m - m = 0)
533Proof
534INDUCT_TAC THEN ASM_SIMP_TAC bool_ss [SUB_MONO_EQ, SUB_0, SUB_EQUAL_0]
535QED
536
537val COND_OUT_THMS = CONJ COND_RAND COND_RATOR
538
539Theorem SUB_elim[local]:
540 !n m. (n + m) - m = n
541Proof
542 GEN_TAC THEN INDUCT_THEN numTheory.INDUCTION ASSUME_TAC THEN
543 ASM_SIMP_TAC bool_ss [ADD_CLAUSES, SUB_0, SUB_MONO_EQ]
544QED
545
546(*---------------------------------------------------------------------------*)
547(* Induction over the bit structure to demonstrate that the iSUB function *)
548(* does actually implement subtraction, if the arguments are the *)
549(* "right way round" *)
550(*---------------------------------------------------------------------------*)
551
552Theorem iSUB_correct[local]:
553 !n m. (m <= n ==> (iSUB T n m = n - m)) /\
554 (m < n ==> (iSUB F n m = n - SUC m))
555Proof
556 INDUCT_THEN bit_induction ASSUME_TAC THENL [
557 SIMP_TAC bool_ss [SUB, iSUB_ZERO, ALT_ZERO],
558 SIMP_TAC bool_ss [iSUB_DEF] THEN GEN_TAC THEN
559 STRUCT_CASES_TAC (Q.SPEC `m` bit_cases) THENL [
560 SIMP_TAC bool_ss [SUB_0, iBIT_cases, iDUB, BIT1, ALT_ZERO] THEN
561 SIMP_TAC bool_ss [ADD_ASSOC, SUB_elim],
562 SIMP_TAC bool_ss [iBIT_cases, numeral_lt, numeral_lte] THEN
563 ASM_SIMP_TAC bool_ss [BIT2, BIT1, PRE_SUB,
564 SUB_LEFT_SUC, SUB_MONO_EQ, SUB_LEFT_ADD, SUB_RIGHT_ADD, SUB_RIGHT_SUB,
565 ADD_CLAUSES, less_less_eqs, LESS_MONO_EQ, GSYM LESS_OR_EQ, iDUB,
566 DOUBLE_FACTS] THEN CONJ_TAC THEN
567 SIMP_TAC bool_ss [COND_OUT_THMS, ADD_CLAUSES, sub_facts],
568 ASM_SIMP_TAC bool_ss [iBIT_cases, numeral_lt, BIT1,
569 BIT2, PRE_SUB, SUB_LEFT_SUC, SUB_MONO_EQ, SUB_LEFT_ADD,
570 SUB_RIGHT_ADD, SUB_RIGHT_SUB, ADD_CLAUSES, less_less_eqs, iDUB,
571 DOUBLE_FACTS, LESS_EQ_MONO] THEN
572 CONJ_TAC THEN
573 SIMP_TAC bool_ss [ADD_CLAUSES, sub_facts, COND_OUT_THMS]
574 ],
575 GEN_TAC THEN STRUCT_CASES_TAC (Q.SPEC `m` bit_cases) THEN
576 ASM_SIMP_TAC bool_ss [iBIT_cases, numeral_lte, numeral_lt, ALT_ZERO,
577 iSUB_DEF, SUB_0] THENL [
578 SIMP_TAC bool_ss [sub_facts, BIT2, BIT1, ADD_CLAUSES,
579 SUB_MONO_EQ, SUB_0],
580 ASM_SIMP_TAC bool_ss [NOT_LESS, BIT1, BIT2, iDUB,
581 ADD_CLAUSES, SUB_MONO_EQ, INV_SUC_EQ, SUB_LEFT_SUC, SUB_RIGHT_SUB,
582 SUB_LEFT_SUB, SUB_LEFT_ADD, SUB_RIGHT_ADD, less_less_eqs] THEN
583 CONJ_TAC THEN
584 SIMP_TAC bool_ss [COND_OUT_THMS, ADD_CLAUSES, sub_facts, NUMERAL_DEF],
585 ASM_SIMP_TAC bool_ss [NOT_LESS, BIT1, BIT2, iDUB,
586 ADD_CLAUSES, SUB_MONO_EQ, INV_SUC_EQ, SUB_LEFT_SUC, SUB_RIGHT_SUB,
587 SUB_LEFT_SUB, SUB_LEFT_ADD, SUB_RIGHT_ADD, less_less_eqs] THEN
588 CONJ_TAC THEN
589 SIMP_TAC bool_ss [COND_OUT_THMS, ADD_CLAUSES, sub_facts, NUMERAL_DEF]
590 ]
591 ]
592QED
593
594Theorem numeral_sub:
595 !n m. NUMERAL (n - m) = if m < n then NUMERAL (iSUB T n m) else 0
596Proof
597 SIMP_TAC bool_ss [iSUB_correct, COND_OUT_THMS,
598 REWRITE_RULE [NUMERAL_DEF] SUB_EQ_0, LESS_EQ_CASES,
599 NUMERAL_DEF, LESS_IMP_LESS_OR_EQ, GSYM NOT_LESS]
600QED
601
602val NOT_ZERO = arithmeticTheory.NOT_ZERO_LT_ZERO;
603
604Theorem iDUB_removal:
605 !n. (iDUB (BIT1 n) = BIT2 (iDUB n)) /\
606 (iDUB (BIT2 n) = BIT2 (BIT1 n)) /\
607 (iDUB ZERO = ZERO)
608Proof
609 SIMP_TAC bool_ss [iDUB, BIT2, BIT1, PRE_SUB1,
610 ADD_CLAUSES, ALT_ZERO]
611QED
612
613val _ = print "Developing numeral rewrites for multiplication\n"
614
615Theorem numeral_mult: !n m.
616 (ZERO * n = ZERO) /\
617 (n * ZERO = ZERO) /\
618 (BIT1 n * m = iZ (iDUB (n * m) + m)) /\
619 (BIT2 n * m = iDUB (iZ (n * m + m)))
620Proof
621 SIMP_TAC bool_ss [BIT1, BIT2, iDUB, RIGHT_ADD_DISTRIB, iZ,
622 MULT_CLAUSES, ADD_CLAUSES, ALT_ZERO] THEN
623 REPEAT GEN_TAC THEN CONV_TAC (AC_CONV (ADD_ASSOC, ADD_SYM))
624QED
625
626
627val _ = print "Developing numeral treatment of exponentiation\n";
628
629(*---------------------------------------------------------------------------*)
630(* In order to do efficient exponentiation, we need to define the operation *)
631(* of squaring. (We can't just rewrite to n * n, because simple rewriting *)
632(* would then rewrite both arms of the multiplication independently, thereby *)
633(* doing twice as much work as necessary.) *)
634(*---------------------------------------------------------------------------*)
635
636val iSQR = new_definition("iSQR", “iSQR x = x * x”);
637val _ = OpenTheory_add"iSQR"
638
639Theorem numeral_exp: (!n. n EXP ZERO = BIT1 ZERO) /\
640 (!n m. n EXP (BIT1 m) = n * iSQR (n EXP m)) /\
641 (!n m. n EXP (BIT2 m) = iSQR n * iSQR (n EXP m))
642Proof
643 SIMP_TAC bool_ss [BIT1, iSQR, BIT2, EXP_ADD, EXP,
644 ADD_CLAUSES, ALT_ZERO, NUMERAL_DEF] THEN
645 REPEAT STRIP_TAC THEN CONV_TAC (AC_CONV(MULT_ASSOC, MULT_SYM))
646QED
647
648val _ = print "Even-ness and odd-ness of numerals\n"
649
650Theorem numeral_evenodd:
651 !n. EVEN ZERO /\ EVEN (BIT2 n) /\ ~EVEN (BIT1 n) /\
652 ~ODD ZERO /\ ~ODD (BIT2 n) /\ ODD (BIT1 n)
653Proof
654 SIMP_TAC bool_ss [BIT1, ALT_ZERO, BIT2, ADD_CLAUSES,
655 EVEN, ODD, EVEN_ADD, ODD_ADD]
656QED
657
658val _ = print "Factorial for numerals\n"
659
660Theorem numeral_fact:
661 (FACT 0 = 1) /\
662 (!n. FACT (NUMERAL (BIT1 n)) =
663 NUMERAL (BIT1 n) * FACT (PRE(NUMERAL(BIT1 n)))) /\
664 (!n. FACT (NUMERAL (BIT2 n)) = NUMERAL (BIT2 n) * FACT (NUMERAL (BIT1 n)))
665Proof
666 REPEAT STRIP_TAC THEN REWRITE_TAC [FACT] THEN
667 (STRIP_ASSUME_TAC (SPEC (Term`n:num`) num_CASES) THENL [
668 ALL_TAC,
669 POP_ASSUM SUBST_ALL_TAC
670 ] THEN ASM_REWRITE_TAC[FACT,PRE,NOT_SUC, NUMERAL_DEF,
671 BIT1, BIT2, ADD_CLAUSES])
672QED
673
674val _ = print "funpow for numerals\n"
675
676Theorem numeral_funpow:
677 (FUNPOW f 0 x = x) /\
678 (FUNPOW f (NUMERAL (BIT1 n)) x = FUNPOW f (PRE (NUMERAL (BIT1 n))) (f x)) /\
679 (FUNPOW f (NUMERAL (BIT2 n)) x = FUNPOW f (NUMERAL (BIT1 n)) (f x))
680Proof
681 REPEAT STRIP_TAC THEN REWRITE_TAC [FUNPOW] THEN
682 (STRIP_ASSUME_TAC (SPEC (Term`n:num`) num_CASES) THENL [
683 ALL_TAC,
684 POP_ASSUM SUBST_ALL_TAC
685 ] THEN ASM_REWRITE_TAC[FUNPOW,PRE,ADD_CLAUSES, NUMERAL_DEF,
686 BIT1, BIT2])
687QED
688
689val _ = print "min and max for numerals\n"
690
691Theorem numeral_MIN:
692 (MIN 0 x = 0) /\
693 (MIN x 0 = 0) /\
694 (MIN (NUMERAL x) (NUMERAL y) = NUMERAL (if x < y then x else y))
695Proof
696 REWRITE_TAC [MIN_0] THEN
697 REWRITE_TAC [MIN_DEF, NUMERAL_DEF]
698QED
699
700Theorem numeral_MAX:
701 (MAX 0 x = x) /\
702 (MAX x 0 = x) /\
703 (MAX (NUMERAL x) (NUMERAL y) = NUMERAL (if x < y then y else x))
704Proof
705 REWRITE_TAC [MAX_0] THEN
706 REWRITE_TAC [MAX_DEF, NUMERAL_DEF]
707QED
708
709
710val _ = print "DIVMOD for numerals\n"
711
712(*---------------------------------------------------------------------------*)
713(* For calculation *)
714(*---------------------------------------------------------------------------*)
715
716Theorem divmod_POS:
717 !n. 0<n ==>
718 (DIVMOD (a,m,n) =
719 if m < n then
720 (a,m)
721 else
722 (let q = findq (1,m,n) in DIVMOD (a + q,m - n * q,n)))
723Proof
724 RW_TAC bool_ss [Once DIVMOD_THM,NOT_ZERO_LT_ZERO,prim_recTheory.LESS_REFL]
725QED
726
727Theorem DIVMOD_NUMERAL_CALC:
728 (!m n. m DIV (BIT1 n) = FST(DIVMOD (ZERO,m,BIT1 n))) /\
729 (!m n. m DIV (BIT2 n) = FST(DIVMOD (ZERO,m,BIT2 n))) /\
730 (!m n. m MOD (BIT1 n) = SND(DIVMOD (ZERO,m,BIT1 n))) /\
731 (!m n. m MOD (BIT2 n) = SND(DIVMOD (ZERO,m,BIT2 n)))
732Proof
733 METIS_TAC [DIVMOD_CALC,numeral_lt,ALT_ZERO]
734QED
735
736Theorem numeral_div2:
737 (DIV2 0 = 0) /\
738 (!n. DIV2 (NUMERAL (BIT1 n)) = NUMERAL n) /\
739 (!n. DIV2 (NUMERAL (BIT2 n)) = NUMERAL (SUC n))
740Proof
741 RW_TAC bool_ss [ALT_ZERO, NUMERAL_DEF, BIT1, BIT2]
742 THEN REWRITE_TAC [DIV2_def, ADD_ASSOC, GSYM TIMES2]
743 THEN METIS_TAC [ZERO_DIV, ALT_ZERO, NUMERAL_DEF, DIVMOD_ID, ADD_CLAUSES,
744 MULT_COMM, ADD_DIV_ADD_DIV, LESS_DIV_EQ_ZERO,
745 numeral_lt, numeral_suc]
746QED
747
748(* ----------------------------------------------------------------------
749 Rewrites to optimise calculations with powers of 2
750 ---------------------------------------------------------------------- *)
751
752val texp_help_def = new_recursive_definition {
753 name = "texp_help_def",
754 def = ``(texp_help 0 acc = BIT2 acc) /\
755 (texp_help (SUC n) acc = texp_help n (BIT1 acc))``,
756 rec_axiom = TypeBase.axiom_of ``:num``};
757val _ = OpenTheory_add"texp_help"
758
759Theorem texp_help_thm:
760 !n a. texp_help n a = (a + 1) * 2 EXP (n + 1)
761Proof
762 INDUCT_TAC THEN SRW_TAC [][texp_help_def] THENL [
763 SRW_TAC [][EXP, MULT_CLAUSES, ONE, TWO, ADD_CLAUSES, BIT2],
764 SRW_TAC [][EXP, ADD_CLAUSES] THEN
765 Q.SUBGOAL_THEN `BIT1 a = 2 * a + 1` ASSUME_TAC THEN1
766 SRW_TAC [][BIT1, TWO, ONE, MULT_CLAUSES, ADD_CLAUSES] THEN
767 SRW_TAC [][RIGHT_ADD_DISTRIB, MULT_CLAUSES, TIMES2, LEFT_ADD_DISTRIB,
768 AC ADD_ASSOC ADD_COMM, AC MULT_ASSOC MULT_COMM]
769 ]
770QED
771
772Theorem texp_help0:
773 texp_help n 0 = 2 ** (n + 1)
774Proof
775 SRW_TAC [][texp_help_thm, ADD_CLAUSES, MULT_CLAUSES, EXP_ADD, EXP_1,
776 MULT_COMM]
777QED
778
779Theorem numeral_texp_help:
780 (texp_help ZERO acc = BIT2 acc) /\
781 (texp_help (BIT1 n) acc = texp_help (PRE (BIT1 n)) (BIT1 acc)) /\
782 (texp_help (BIT2 n) acc = texp_help (BIT1 n) (BIT1 acc))
783Proof
784 SRW_TAC [][texp_help_def, BIT1, BIT2, ADD_CLAUSES, PRE, ALT_ZERO]
785QED
786
787Theorem TWO_EXP_THM:
788 (2 EXP 0 = 1) /\
789 (2 EXP (NUMERAL (BIT1 n)) = NUMERAL (texp_help (PRE (BIT1 n)) ZERO)) /\
790 (2 EXP (NUMERAL (BIT2 n)) = NUMERAL (texp_help (BIT1 n) ZERO))
791Proof
792 SRW_TAC [][texp_help0, EXP, ALT_ZERO] THEN
793 SRW_TAC [][NUMERAL_DEF, EXP_BASE_INJECTIVE, numeral_lt] THEN
794 SRW_TAC [][BIT1, BIT2, PRE, ADD_CLAUSES, ALT_ZERO]
795QED
796
797val onecount_def = new_specification(
798 "onecount_def", ["onecount"],
799 (BETA_RULE o
800 ONCE_REWRITE_RULE [FUN_EQ_THM] o
801 Q.SPECL [`\a. a:num`,
802 `\ (n:num) (rf:num->num) (a:num). rf (SUC a)`,
803 `\ (n:num) (rf:num->num) (a:num). ZERO`] o
804 INST_TYPE [alpha |-> ``:num -> num``]) bit_initiality)
805val onecount0 = SIMP_RULE (srw_ss()) [ALT_ZERO] (CONJUNCT1 onecount_def)
806val _ = OpenTheory_add"onecount"
807
808val exactlog_def = new_specification(
809 "exactlog_def", ["exactlog"],
810 (BETA_RULE o
811 Q.SPECL [`ZERO`,
812 `\ (n:num) (r:num). ZERO`,
813 `\ (n:num) (r:num). let x = onecount n ZERO
814 in
815 if x = ZERO then ZERO
816 else BIT1 x`] o
817 INST_TYPE [alpha |-> ``:num``]) bit_initiality)
818val _ = OpenTheory_add"exactlog"
819
820val onecount_lemma1 = prove(
821 ``!n a. 0 < onecount n a ==> a <= onecount n a``,
822 HO_MATCH_MP_TAC bit_induction THEN
823 SRW_TAC [][onecount_def, LESS_EQ_REFL, ALT_ZERO, LESS_REFL] THEN
824 MATCH_MP_TAC LESS_EQ_TRANS THEN Q.EXISTS_TAC `SUC a` THEN
825 SRW_TAC [][LESS_EQ_SUC_REFL]);
826
827val onecount_lemma2 = prove(
828 ``!n. 0 < n ==> !a b. (onecount n a = 0) = (onecount n b = 0)``,
829 HO_MATCH_MP_TAC bit_induction THEN
830 SRW_TAC [][ALT_ZERO, LESS_REFL, onecount_def] THEN
831 Q.SPEC_THEN `n` FULL_STRUCT_CASES_TAC num_CASES THENL [
832 SRW_TAC [][onecount0, NOT_SUC, ALT_ZERO],
833 SRW_TAC [][LESS_0]
834 ]);
835
836val sub_eq' = prove(
837 ``(m - n = p) = if n <= m then m = p + n else (p = 0)``,
838 SRW_TAC [][SUB_RIGHT_EQ, EQ_IMP_THM, ADD_COMM, LESS_EQ_REFL, ADD_CLAUSES]
839 THENL [
840 FULL_SIMP_TAC (srw_ss()) [LESS_EQ_0, LESS_EQUAL_ANTISYM, ADD_CLAUSES],
841 FULL_SIMP_TAC (srw_ss()) [LESS_EQ_ADD],
842 FULL_SIMP_TAC (srw_ss()) [LESS_EQ_0],
843 FULL_SIMP_TAC (srw_ss()) [NOT_LESS_EQUAL, LESS_OR_EQ]
844 ]);
845
846val sub_add' = prove(
847 ``m - n + p = if n <= m then m + p - n else p``,
848 SRW_TAC [][SUB_RIGHT_ADD] THENL [
849 Q.SUBGOAL_THEN `m = n` SUBST_ALL_TAC
850 THEN1 SRW_TAC [][LESS_EQUAL_ANTISYM] THEN
851 METIS_TAC [ADD_SUB, ADD_COMM],
852 METIS_TAC [NOT_LESS_EQUAL, LESS_ANTISYM]
853 ]);
854
855val onecount_lemma3 = prove(
856 ``!n a. 0 < onecount n (SUC a) ==>
857 (onecount n (SUC a) = SUC (onecount n a))``,
858 HO_MATCH_MP_TAC bit_induction THEN
859 SRW_TAC [][onecount_def, ALT_ZERO, LESS_REFL]);
860
861Theorem onecount_characterisation:
862 !n a. 0 < onecount n a /\ 0 < n ==> (n = 2 EXP (onecount n a - a) - 1)
863Proof
864 HO_MATCH_MP_TAC bit_induction THEN
865 SRW_TAC [][onecount_def] THENL [
866 FULL_SIMP_TAC (srw_ss()) [ALT_ZERO, LESS_REFL],
867 SRW_TAC [][onecount_lemma3, SUB, EXP] THENL [
868 Q.SUBGOAL_THEN `0 < n` STRIP_ASSUME_TAC
869 THEN1 (CCONTR_TAC THEN
870 FULL_SIMP_TAC (srw_ss()) [NOT_LESS, LESS_EQ_0, onecount0,
871 LESS_REFL]) THEN
872 Q.SUBGOAL_THEN `0 < onecount n a` STRIP_ASSUME_TAC
873 THEN1 METIS_TAC [onecount_lemma2, NOT_ZERO_LT_ZERO] THEN
874 METIS_TAC [onecount_lemma1, LESS_EQ_ANTISYM],
875 FULL_SIMP_TAC (srw_ss()) [NOT_LESS] THEN
876 ASM_CASES_TAC ``0 < n`` THENL [
877 Q.SUBGOAL_THEN `0 < onecount n a` STRIP_ASSUME_TAC
878 THEN1 METIS_TAC [onecount_lemma2, NOT_ZERO_LT_ZERO] THEN
879 Q.ABBREV_TAC `X = onecount n a - a` THEN
880 Q_TAC SUFF_TAC `n = 2 ** X - 1` THENL [
881 DISCH_THEN SUBST1_TAC THEN
882 SRW_TAC [][Once BIT1, sub_add', EXP0] THEN
883 SIMP_TAC bool_ss [EXP0, GSYM ONE, ADD_SUB, TIMES2]
884 >- FULL_SIMP_TAC bool_ss [LESS_REFL] >>
885 FULL_SIMP_TAC bool_ss [TWO, ONE, LESS_0],
886
887 Q.UNABBREV_TAC `X` THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
888 SRW_TAC [][]
889 ],
890 FULL_SIMP_TAC (srw_ss()) [NOT_LESS, LESS_EQ_0, onecount0, SUB_EQUAL_0,
891 EXP, MULT_CLAUSES] THEN
892 SRW_TAC [][TWO, ONE, BIT1, SUB, ADD_CLAUSES, LESS_REFL, LESS_SUC_REFL]
893 ]
894 ],
895 FULL_SIMP_TAC (srw_ss()) [ALT_ZERO, LESS_REFL]
896 ]
897QED
898
899val onecount_thm = SIMP_RULE (srw_ss()) [SUB_0]
900 (Q.SPECL [`n`, `0`] onecount_characterisation)
901
902val bit_cases = hd (Prim_rec.prove_cases_thm bit_induction)
903
904Theorem SUC_LE1[local,simp]:
905 SUC x <= 1 <=> x = 0
906Proof
907 iff_tac >- REWRITE_TAC[ONE,LESS_EQ_MONO,LESS_EQ_0] >>
908 SIMP_TAC bool_ss [ONE, LESS_EQ_REFL]
909QED
910
911Theorem SUC_SUB1[simp,local]:
912 SUC x - 1 = x
913Proof
914 REWRITE_TAC[ONE,SUB_MONO_EQ,SUB_0]
915QED
916
917Theorem TWO_NE0[simp,local]:
918 2 <> 0
919Proof
920 REWRITE_TAC[TWO,NOT_SUC]
921QED
922
923Theorem exactlog_characterisation:
924 !n m. (exactlog n = BIT1 m) ==> (n = 2 ** (m + 1))
925Proof
926 REPEAT GEN_TAC THEN
927 Q.SPEC_THEN `n` STRUCT_CASES_TAC bit_cases THEN
928 SRW_TAC [][exactlog_def, numeral_eq, LET_THM] THEN
929 RULE_ASSUM_TAC (REWRITE_RULE [ALT_ZERO, NOT_ZERO_LT_ZERO]) THEN
930 ASM_CASES_TAC ``0 < n'`` THENL [
931 SIMP_TAC (srw_ss()) [Once BIT2] THEN
932 POP_ASSUM (fn zln =>
933 POP_ASSUM
934 (fn zloc => ASSUME_TAC (MATCH_MP (GEN_ALL onecount_thm)
935 (CONJ zloc zln)))) THEN
936 POP_ASSUM (fn th => CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [th]))) THEN
937 Q.ABBREV_TAC `X = onecount n' 0` THEN
938 Q.SUBGOAL_THEN `onecount n' ZERO = X` SUBST_ALL_TAC THEN1
939 SRW_TAC [][ALT_ZERO] THEN
940 SRW_TAC [][sub_add', SUB_LEFT_ADD] THEN
941 FULL_SIMP_TAC (srw_ss()) [LESS_REFL, ADD_CLAUSES]
942 >- REWRITE_TAC[GSYM ADD1, EXP, TIMES2] >>
943 REWRITE_TAC[ADD_CLAUSES,TWO,ONE],
944
945 FULL_SIMP_TAC (srw_ss()) [onecount0, NOT_LESS, LESS_EQ_0, LESS_REFL]
946 ]
947QED
948
949val internal_mult_def = new_definition(
950 "internal_mult_def",
951 ``internal_mult = $*``);
952val _ = OpenTheory_add "internal_mult"
953
954Theorem DIV2_BIT1:
955 DIV2 (BIT1 x) = x
956Proof
957 SRW_TAC [][REWRITE_RULE [NUMERAL_DEF] numeral_div2]
958QED
959
960val odd_lemma = prove(
961 ``!n. ODD n ==> ?m. n = BIT1 m``,
962 HO_MATCH_MP_TAC bit_induction THEN SRW_TAC [][numeral_evenodd, numeral_eq]);
963
964val enhanced_numeral_mult = prove(
965 ``x * y = if y = ZERO then ZERO
966 else if x = ZERO then ZERO
967 else
968 let m = exactlog x in
969 let n = exactlog y
970 in
971 if ODD m then texp_help (DIV2 m) (PRE y)
972 else if ODD n then texp_help (DIV2 n) (PRE x)
973 else internal_mult x y``,
974 SRW_TAC [][internal_mult_def, MULT_CLAUSES, ALT_ZERO] THEN
975 SRW_TAC [][] THENL [
976 IMP_RES_TAC odd_lemma THEN markerLib.UNABBREV_ALL_TAC THEN
977 SRW_TAC [][DIV2_BIT1, texp_help_thm] THEN
978 Q.SPEC_THEN `y` FULL_STRUCT_CASES_TAC num_CASES THEN1
979 FULL_SIMP_TAC (srw_ss()) [] THEN
980 SRW_TAC [][PRE, ADD1] THEN IMP_RES_TAC exactlog_characterisation THEN
981 SRW_TAC [][AC MULT_ASSOC MULT_COMM],
982
983 IMP_RES_TAC odd_lemma THEN markerLib.UNABBREV_ALL_TAC THEN
984 SRW_TAC [][DIV2_BIT1, texp_help_thm] THEN
985 Q.SPEC_THEN `x` FULL_STRUCT_CASES_TAC num_CASES THEN1
986 FULL_SIMP_TAC (srw_ss()) [] THEN
987 SRW_TAC [][PRE, ADD1] THEN IMP_RES_TAC exactlog_characterisation THEN
988 SRW_TAC [][AC MULT_ASSOC MULT_COMM]
989 ]);
990
991val sillylet = prove(``LET f ZERO = f ZERO``, REWRITE_TAC [LET_THM])
992val silly_exactlog =
993 prove(``exactlog (BIT1 x) = ZERO``, REWRITE_TAC [exactlog_def])
994
995fun gen_case x y =
996 SIMP_RULE bool_ss [numeral_eq, silly_exactlog, sillylet, numeral_evenodd]
997 (Q.INST [`x` |-> x, `y` |-> y] enhanced_numeral_mult)
998
999
1000Theorem enumeral_mult =
1001 LIST_CONJ (List.take(CONJUNCTS (SPEC_ALL numeral_mult), 2) @
1002 [gen_case `BIT1 x` `BIT1 y`,
1003 gen_case `BIT1 x` `BIT2 y`,
1004 gen_case `BIT2 x` `BIT1 y`,
1005 gen_case `BIT2 x` `BIT2 y`])
1006
1007Theorem internal_mult_characterisation =
1008 REWRITE_RULE [SYM internal_mult_def] numeral_mult;
1009
1010(* ----------------------------------------------------------------------
1011 hide the internal constants from this theory so that later name-
1012 spaces are not contaminated. Constants can still be found by using
1013 numeral$cname syntax.
1014 ---------------------------------------------------------------------- *)
1015
1016val _ = app
1017 (fn s => remove_ovl_mapping s {Name = s, Thy = "numeral"})
1018 ["iZ", "iiSUC", "iDUB", "iSUB", "iSQR", "texp_help",
1019 "onecount", "exactlog"]