logrootScript.sml
1Theory logroot[bare]
2Ancestors
3 arithmetic pair combin
4Libs
5 HolKernel boolLib Parse BasicProvers metisLib simpLib
6 computeLib
7
8(* ----------------------------------------------------------------------- *)
9
10fun AC_THM term = CONV_RULE bool_EQ_CONV (AC_CONV (MULT_ASSOC, MULT_COMM) term)
11val arith_ss = srw_ss() ++ numSimps.old_ARITH_ss
12val ARITH_ss = numSimps.ARITH_ss
13
14fun DECIDE_TAC (g as (asl, _)) =
15 (MAP_EVERY UNDISCH_TAC (filter numSimps.is_arith_asm asl)
16 THEN CONV_TAC Arith.ARITH_CONV) g
17
18val decide_tac = DECIDE_TAC;
19val metis_tac = METIS_TAC;
20
21val DECIDE = EQT_ELIM o Arith.ARITH_CONV;
22val rw = SRW_TAC [ARITH_ss];
23val std_ss = arith_ss;
24val qabbrev_tac = Q.ABBREV_TAC;
25val qexists_tac = Q.EXISTS_TAC;
26fun simp l = ASM_SIMP_TAC (srw_ss() ++ ARITH_ss) l;
27fun fs l = FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) l;
28fun rfs l = REV_FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) l;
29
30(* ----------------------------------------------------------------------- *)
31
32Theorem lt_mult2[local]:
33 a < c /\ b < d ==> a * b < c * d:num
34Proof
35 STRIP_TAC
36 THEN `0 < d` by DECIDE_TAC
37 THEN METIS_TAC [LE_MULT_LCANCEL, LT_MULT_RCANCEL, LESS_EQ_LESS_TRANS,
38 LESS_OR_EQ]
39QED
40
41(* ------------------------------------------------------------------------- *)
42(* Exponential Theorems *)
43(* ------------------------------------------------------------------------- *)
44
45Theorem exp_lemma2[local]:
46 !a b r. 0 < r ==> a < b ==> a ** r < b ** r
47Proof
48 REPEAT STRIP_TAC
49 THEN Induct_on `r`
50 THEN RW_TAC arith_ss [EXP]
51 THEN Cases_on `r = 0`
52 THEN RW_TAC arith_ss [EXP]
53 THEN MATCH_MP_TAC lt_mult2
54 THEN RW_TAC arith_ss []
55QED
56
57val exp_lemma3 =
58 METIS_PROVE [LESS_OR_EQ, exp_lemma2]
59 ``!a b r. 0 < r ==> a <= b ==> a ** r <= b ** r``;
60
61Theorem lem[local]:
62 1 < a /\ 0 < b ==> 1n < a * b
63Proof
64 Induct_on `b`
65 THEN REWRITE_TAC [ADD1, LEFT_ADD_DISTRIB]
66 THEN DECIDE_TAC
67QED
68
69Theorem exp_lemma4[local]:
70 !e a b. 1n < e ==> a < b ==> e ** a < e ** b
71Proof
72 REPEAT STRIP_TAC
73 THEN `?p. b = SUC p + a`
74 by (IMP_RES_TAC LESS_ADD_1
75 THEN Q.EXISTS_TAC `p`
76 THEN DECIDE_TAC)
77 THEN ASM_REWRITE_TAC
78 [EXP_ADD, EXP,
79 REWRITE_RULE [MULT_CLAUSES] (SPEC ``1n`` LT_MULT_RCANCEL)]
80 THEN CONJ_TAC
81 THENL [ALL_TAC, MATCH_MP_TAC lem]
82 THEN Cases_on `e`
83 THEN REWRITE_TAC [ZERO_LESS_EXP]
84 THEN DECIDE_TAC
85QED
86
87val exp_lemma5 =
88 METIS_PROVE [LESS_OR_EQ, exp_lemma4]
89 ``!e a b. 1n < e ==> a <= b ==> e ** a <= e ** b``;
90
91Theorem LT_EXP_ISO:
92 !e a b. 1n < e ==> (a < b <=> e ** a < e ** b)
93Proof
94 PROVE_TAC [NOT_LESS, exp_lemma4, exp_lemma5]
95QED
96
97Theorem LE_EXP_ISO:
98 !e a b. 1n < e ==> (a <= b <=> e ** a <= e ** b)
99Proof
100 PROVE_TAC [exp_lemma4, exp_lemma5, LESS_OR_EQ, NOT_LESS]
101QED
102
103Theorem EXP_LT_ISO:
104 !a b r. 0 < r ==> (a < b <=> a ** r < b ** r)
105Proof
106 PROVE_TAC [NOT_LESS, exp_lemma3, exp_lemma2, LESS_OR_EQ, NOT_LESS]
107QED
108
109Theorem EXP_LE_ISO:
110 !a b r. 0 < r ==> (a <= b <=> a ** r <= b ** r)
111Proof
112 PROVE_TAC [NOT_LESS, exp_lemma3, exp_lemma2, LESS_OR_EQ, NOT_LESS]
113QED
114
115(* Theorem: 0 < m ==> ((n ** m = n) <=> ((m = 1) \/ (n = 0) \/ (n = 1))) *)
116(* Proof:
117 If part: n ** m = n ==> n = 0 \/ n = 1
118 By contradiction, assume n <> 0 /\ n <> 1.
119 Then ?k. m = SUC k by num_CASES, 0 < m
120 so n ** SUC k = n by n ** m = n
121 or n * n ** k = n by EXP
122 ==> n ** k = 1 by MULT_EQ_SELF, 0 < n
123 ==> n = 1 or k = 0 by EXP_EQ_1
124 ==> n = 1 or m = 1,
125 These contradict n <> 1 and m <> 1.
126 Only-if part: n ** 1 = n /\ 0 ** m = 0 /\ 1 ** m = 1
127 These are true by EXP_1, ZERO_EXP.
128*)
129Theorem EXP_EQ_SELF:
130 !n m. 0 < m ==> ((n ** m = n) <=> ((m = 1) \/ (n = 0) \/ (n = 1)))
131Proof
132 rw_tac std_ss[EQ_IMP_THM] >| [
133 spose_not_then strip_assume_tac >>
134 `m <> 0` by decide_tac >>
135 `?k. m = SUC k` by metis_tac[num_CASES] >>
136 `n * n ** k = n` by fs[EXP] >>
137 `n ** k = 1` by metis_tac[MULT_EQ_SELF, NOT_ZERO_LT_ZERO] >>
138 fs[EXP_EQ_1],
139 rw[],
140 rw[],
141 rw[]
142 ]
143QED
144
145(* Obtain a theorem *)
146Theorem EXP_LE = X_LE_X_EXP |> GEN ``x:num`` |> SPEC ``b:num`` |> GEN_ALL;
147(* val EXP_LE = |- !n b. 0 < n ==> b <= b ** n: thm *)
148
149(* Theorem: 1 < b /\ 1 < n ==> b < b ** n *)
150(* Proof:
151 By contradiction, assume ~(b < b ** n).
152 Then b ** n <= b by arithmetic
153 But b <= b ** n by EXP_LE, 0 < n
154 ==> b ** n = b by EQ_LESS_EQ
155 ==> b = 1 or n = 0 or n = 1.
156 All these contradict 1 < b and 1 < n.
157*)
158Theorem EXP_LT:
159 !n b. 1 < b /\ 1 < n ==> b < b ** n
160Proof
161 spose_not_then strip_assume_tac >>
162 `b <= b ** n` by rw[EXP_LE] >>
163 `b ** n = b` by decide_tac >>
164 rfs[EXP_EQ_SELF]
165QED
166
167(* Theorem: 0 < a /\ n < m /\ (a ** n * b = a ** m * c) ==>
168 ?d. 0 < d /\ (b = a ** d * c) *)
169(* Proof:
170 Let d = m - n.
171 Then 0 < d, and m = n + d by arithmetic
172 and 0 < a ==> a ** n <> 0 by EXP_EQ_0
173 a ** n * b
174 = a ** (n + d) * c by m = n + d
175 = (a ** n * a ** d) * c by EXP_ADD
176 = a ** n * (a ** d * c) by MULT_ASSOC
177 The result follows by MULT_LEFT_CANCEL
178*)
179Theorem EXP_LCANCEL:
180 !a b c n m. 0 < a /\ n < m /\ (a ** n * b = a ** m * c) ==>
181 ?d. 0 < d /\ (b = a ** d * c)
182Proof
183 rpt strip_tac >>
184 `0 < m - n /\ (m = n + (m - n))` by decide_tac >>
185 qabbrev_tac `d = m - n` >>
186 `a ** n <> 0` by metis_tac[EXP_EQ_0, NOT_ZERO_LT_ZERO] >>
187 metis_tac[EXP_ADD, MULT_ASSOC, MULT_LEFT_CANCEL]
188QED
189
190Theorem EXP_RCANCEL:
191 !a b c n m. 0 < a /\ n < m /\ (b * a ** n = c * a ** m) ==>
192 ?d. 0 < d /\ (b = c * a ** d)
193Proof
194 metis_tac[EXP_LCANCEL, MULT_COMM]
195QED
196
197(*
198EXP_POS |- !m n. 0 < m ==> 0 < m ** n
199ONE_LT_EXP |- !x y. 1 < x ** y <=> 1 < x /\ 0 < y
200ZERO_LT_EXP |- 0 < x ** y <=> 0 < x \/ (y = 0)
201*)
202
203(* Theorem: 0 < m ==> 1 <= m ** n *)
204(* Proof:
205 0 < m ==> 0 < m ** n by EXP_POS
206 or 1 <= m ** n by arithmetic
207*)
208Theorem ONE_LE_EXP:
209 !m n. 0 < m ==> 1 <= m ** n
210Proof
211 metis_tac[EXP_POS, DECIDE``!x. 0 < x <=> 1 <= x``]
212QED
213
214(* ------------------------------------------------------------------------- *)
215(* ROOT and LOG *)
216(* ------------------------------------------------------------------------- *)
217
218Theorem ROOT_exists:
219 !r n. 0 < r ==> ?rt. rt ** r <= n /\ n < SUC rt ** r
220Proof
221 Induct_on `n`
222 THEN RW_TAC arith_ss []
223 THEN REPEAT STRIP_TAC
224 THEN FIRST_X_ASSUM (Q.SPEC_THEN `r` MP_TAC)
225 THEN SRW_TAC [][]
226 THEN Cases_on `SUC n < SUC rt ** r`
227 THEN1 (Q.EXISTS_TAC `rt` THEN SRW_TAC [numSimps.ARITH_ss][])
228 THEN POP_ASSUM (ASSUME_TAC o SIMP_RULE (srw_ss()) [NOT_LESS])
229 THEN Q.EXISTS_TAC `SUC rt`
230 THEN SRW_TAC [][]
231 THEN `SUC n = SUC rt ** r` by RW_TAC arith_ss []
232 THEN RW_TAC arith_ss []
233QED
234
235val ROOT = new_specification("ROOT", ["ROOT"],
236 SIMP_RULE (srw_ss()) [SKOLEM_THM, GSYM RIGHT_EXISTS_IMP_THM] ROOT_exists);
237
238Theorem ROOT_UNIQUE:
239 !r n p. (p ** r <= n /\ n < SUC p ** r) ==> (ROOT r n = p)
240Proof
241 REPEAT STRIP_TAC
242 THEN Cases_on `r = 0`
243 THEN FULL_SIMP_TAC arith_ss [EXP, DECIDE ``~(r = 0n) <=> 0 < r``]
244 THEN RW_TAC arith_ss []
245 THEN CCONTR_TAC
246 THEN `ROOT r n < p \/ p < ROOT r n` by DECIDE_TAC
247 THEN METIS_TAC [DECIDE ``a < b ==> SUC a <= b``, exp_lemma3, LESS_EQ_TRANS,
248 DECIDE ``a <= b ==> ~(b < a:num)``, ROOT]
249QED
250
251Theorem ROOT_EXP :
252 !n r. 0 < r ==> ROOT r (n ** r) = n
253Proof
254 rpt STRIP_TAC
255 >> MATCH_MP_TAC ROOT_UNIQUE
256 >> RW_TAC arith_ss []
257QED
258
259Theorem log_exists[local]:
260 !a n. 1 < a /\ 0 < n ==> ?log. a ** log <= n /\ n < a ** SUC log
261Proof
262 REPEAT STRIP_TAC
263 THEN Q.EXISTS_TAC `LEAST x. n < a ** SUC x`
264 THEN CONV_TAC (UNBETA_CONV ``LEAST x. n < a ** SUC x``)
265 THEN MATCH_MP_TAC WhileTheory.LEAST_ELIM
266 THEN CONJ_TAC
267 THENL [
268 SRW_TAC [][EXP]
269 THEN `?m. n <= a ** m` by METIS_TAC [EXP_ALWAYS_BIG_ENOUGH]
270 THEN Q.EXISTS_TAC `m`
271 THEN MATCH_MP_TAC LESS_EQ_LESS_TRANS
272 THEN Q.EXISTS_TAC `a ** m`
273 THEN SRW_TAC [] []
274 THEN METIS_TAC
275 [MULT_CLAUSES, LT_MULT_RCANCEL, EXP_EQ_0,
276 DECIDE ``1 < x ==> ~(x = 0)``, DECIDE ``~(x = 0) <=> 0 < x``],
277 Q.X_GEN_TAC `m`
278 THEN SRW_TAC [][]
279 THEN `(m = 0) \/ ?k. m = SUC k`
280 by METIS_TAC [TypeBase.nchotomy_of ``:num``]
281 THEN1 RW_TAC arith_ss [EXP]
282 THEN FIRST_X_ASSUM (Q.SPEC_THEN `k` MP_TAC)
283 THEN SRW_TAC [][EXP, NOT_LESS]
284 ]
285QED
286
287Theorem LOG_exists =
288 SIMP_RULE bool_ss [SKOLEM_THM, GSYM RIGHT_EXISTS_IMP_THM] log_exists;
289
290val LOG = new_specification("LOG", ["LOG"], LOG_exists);
291
292Theorem LOG_UNIQUE:
293 !a n:num p. (a ** p <= n /\ n < a ** SUC p) ==> (LOG a n = p)
294Proof
295 REPEAT STRIP_TAC
296 THEN Cases_on `~(n = 0)`
297 THEN Cases_on `~(a = 0)`
298 THEN RW_TAC arith_ss []
299 THEN Cases_on `a = 1`
300 THEN FULL_SIMP_TAC arith_ss [EXP]
301 THEN ((`0 < n /\ 1 < a` by DECIDE_TAC
302 THEN REPEAT (PAT_X_ASSUM ``~(a = b:num)`` (K (ALL_TAC))))
303 ORELSE
304 (Cases_on `a`
305 THEN FULL_SIMP_TAC arith_ss [EXP, ZERO_LESS_EXP]))
306 THEN CCONTR_TAC
307 THEN `LOG a n < p \/ p < LOG a n` by DECIDE_TAC
308 THEN METIS_TAC [exp_lemma5, DECIDE ``a < b <=> SUC a <= b``, LESS_EQ_TRANS,
309 NOT_LESS, LOG, EXP]
310QED
311
312Theorem LOG_POW:
313 !b n. 1n < b ==> (LOG b (b ** n) = n)
314Proof
315 REPEAT STRIP_TAC
316 THEN irule LOG_UNIQUE
317 THEN SRW_TAC [ARITH_ss] [EXP]
318QED
319
320Theorem LOG_ADD1:
321 !n a b. 0n < n /\ 1n < a /\ 0 < b ==>
322 (LOG a (a ** SUC n * b) = SUC (LOG a (a ** n * b)))
323Proof
324 RW_TAC arith_ss []
325 THEN MATCH_MP_TAC LOG_UNIQUE
326 THEN `~(a = 0) /\ 0 < a /\ ~(b = 0)` by DECIDE_TAC
327 THEN ASM_SIMP_TAC arith_ss [EXP]
328 THEN ASM_REWRITE_TAC [GSYM MULT_ASSOC, LT_MULT_LCANCEL, LE_MULT_LCANCEL]
329 THEN REWRITE_TAC [GSYM EXP]
330 THEN MATCH_MP_TAC LOG
331 THEN ASM_SIMP_TAC arith_ss [DECIDE ``0 < x <=> ~(x = 0)``, EXP_EQ_0]
332QED
333
334Theorem square[local]:
335 a:num ** 2 = a * a
336Proof REWRITE_TAC [EXP, EXP_1, TWO]
337QED
338
339Theorem LOG_BASE:
340 !a. 1n < a ==> (LOG a a = 1)
341Proof
342 RW_TAC arith_ss []
343 THEN MATCH_MP_TAC LOG_UNIQUE
344 THEN Induct_on `a`
345 THEN RW_TAC arith_ss [LEFT_ADD_DISTRIB, RIGHT_ADD_DISTRIB, EXP_ADD, ADD1,
346 EXP_1, square]
347QED
348
349Theorem LOG_EXP:
350 !n a b. 1n < a /\ 0 < b ==> (LOG a (a ** n * b) = n + LOG a b)
351Proof
352 REPEAT STRIP_TAC
353 THEN MATCH_MP_TAC LOG_UNIQUE
354 THEN RW_TAC arith_ss [EXP, EXP_ADD, EXP_EQ_0]
355 THEN1 METIS_TAC [LOG]
356 THEN Q_TAC SUFF_TAC `a ** n * b < a ** n * (a * a ** LOG a b)`
357 THEN1 SIMP_TAC bool_ss [AC MULT_COMM MULT_ASSOC]
358 THEN SRW_TAC [ARITH_ss][GSYM NOT_ZERO_LT_ZERO, EXP_EQ_0]
359 THEN METIS_TAC [EXP, LOG]
360QED
361
362Theorem LOG_1:
363 !a. 1n < a ==> (LOG a 1 = 0)
364Proof
365 REPEAT STRIP_TAC
366 THEN MATCH_MP_TAC LOG_UNIQUE
367 THEN REWRITE_TAC [EXP]
368 THEN DECIDE_TAC
369QED
370
371Theorem LOG_DIV:
372 !a x. 1n < a /\ a <= x ==> (LOG a x = 1 + LOG a (x DIV a))
373Proof
374 REPEAT STRIP_TAC
375 THEN MATCH_MP_TAC LOG_UNIQUE
376 THEN REWRITE_TAC [EXP_ADD, DECIDE ``SUC (1 + a) = 1 + SUC a``, EXP_1]
377 THEN RW_TAC bool_ss [GSYM (SPEC ``a:num ** b`` MULT_COMM), GSYM X_LE_DIV,
378 GSYM DIV_LT_X, DECIDE ``1 < a ==> 0n < a``, LOG]
379 THEN PROVE_TAC [X_LE_DIV, MULT_CLAUSES, DECIDE ``1 < a ==> 0n < a``,
380 DECIDE ``1 <= a ==> 0n < a``, LOG]
381QED
382
383Theorem LOG_ADD:
384 !a b c. 1 < a /\ b < a ** c ==> (LOG a (b + a ** c) = c)
385Proof
386 REPEAT STRIP_TAC
387 THEN MATCH_MP_TAC LOG_UNIQUE
388 THEN CONJ_TAC
389 THEN1 DECIDE_TAC
390 THEN REWRITE_TAC [EXP]
391 THEN MATCH_MP_TAC (DECIDE ``!a b c. a < b /\ b <= c ==> a < c:num``)
392 THEN Q.EXISTS_TAC `2 * a ** c`
393 THEN CONJ_TAC
394 THENL [REWRITE_TAC [TIMES2, LT_ADD_RCANCEL],
395 REWRITE_TAC [LE_MULT_RCANCEL]]
396 THEN DECIDE_TAC
397QED
398
399Theorem LOG_LE_MONO:
400 !a x y. 1 < a /\ 0 < x ==> x <= y ==> LOG a x <= LOG a y
401Proof
402 REPEAT STRIP_TAC
403 THEN REWRITE_TAC
404 [UNDISCH (SPECL [``a:num``,``LOG a x``,``SUC (LOG a y)``] LT_EXP_ISO),
405 DECIDE ``a <= b <=> a < SUC b``]
406 THEN MATCH_MP_TAC
407 (DECIDE ``!a b c d. a <= b /\ b <= c /\ c < d ==> a < d:num``)
408 THEN Q.EXISTS_TAC `x`
409 THEN Q.EXISTS_TAC `y`
410 THEN METIS_TAC [LOG, LESS_TRANS, LESS_OR_EQ]
411QED
412
413Theorem LOG_RWT:
414 !m n. 1 < m /\ 0 < n ==>
415 (LOG m n = if n < m then 0 else SUC (LOG m (n DIV m)))
416Proof
417 SRW_TAC [ARITH_ss] [LOG_DIV, ADD1, LOG_UNIQUE, EXP]
418QED
419
420Theorem LOG_EQ_0:
421 !a b. 1 < a /\ 0 < b ==> ((LOG a b = 0) <=> b < a)
422Proof
423 SRW_TAC[][LOG_RWT]
424QED
425
426Theorem LOG_MULT:
427 !b x. 1 < b /\ 0 < x ==> (LOG b (b * x) = SUC (LOG b x))
428Proof
429 SRW_TAC[][] THEN
430 `0 < b /\ x <> 0` by DECIDE_TAC THEN
431 `0 < b * x` by (
432 Cases_on`b` THEN FULL_SIMP_TAC(srw_ss())[ADD1,RIGHT_ADD_DISTRIB] THEN
433 DECIDE_TAC ) THEN
434 ASM_SIMP_TAC(srw_ss())[LOG_RWT,boolSimps.SimpLHS] THEN
435 REWRITE_TAC[Once MULT_COMM] THEN
436 ASM_SIMP_TAC(srw_ss())[MULT_DIV]
437QED
438
439Theorem LOG_add_digit:
440 !b x y. 1 < b /\ 0 < y /\ x < b ==> (LOG b (b * y + x) = SUC (LOG b y))
441Proof
442 SRW_TAC[][] THEN
443 `0 < b * y + x` by (
444 Cases_on`x` THEN ASM_SIMP_TAC(srw_ss()++ARITH_ss)[] THEN
445 Cases_on`b` THEN FULL_SIMP_TAC(srw_ss()++ARITH_ss)[MULT] THEN
446 DECIDE_TAC ) THEN
447 ASM_SIMP_TAC(srw_ss()++ARITH_ss)[LOG_RWT,boolSimps.SimpLHS] THEN
448 SRW_TAC[][] THEN1 (
449 `b <= b * y` by ASM_SIMP_TAC(srw_ss()++ARITH_ss)[] THEN
450 DECIDE_TAC ) THEN
451 `x + b * y = y * b + x` by SIMP_TAC(srw_ss()++ARITH_ss)[] THEN
452 POP_ASSUM SUBST1_TAC THEN
453 ASM_SIMP_TAC(srw_ss()++ARITH_ss)[ADD_DIV_ADD_DIV] THEN
454 IMP_RES_TAC LESS_DIV_EQ_ZERO THEN
455 ASM_SIMP_TAC(srw_ss()++ARITH_ss)[]
456QED
457
458Theorem LT_EXP_LOG:
459 x < b ** e <=> b = 0 /\ e = 0 /\ x = 0 \/ b = 1 /\ x = 0 \/
460 2 <= b /\ (LOG b x < e \/ x = 0)
461Proof
462 Cases_on ‘b = 0’
463 >- (Cases_on ‘e = 0’ >> simp[ZERO_EXP]) >>
464 simp[] >> Cases_on ‘b = 1’ >> simp[] >> iff_tac >>
465 simp[DISJ_IMP_THM]
466 >- (Cases_on ‘x = 0’ >> simp[] >>
467 CCONTR_TAC >> FULL_SIMP_TAC (srw_ss()) [NOT_LESS]>>
468 ‘0 < b /\ 1 < b’ by simp[] >>
469 drule_all_then assume_tac EXP_BASE_LEQ_MONO_IMP >>
470 ‘b ** LOG b x <= x’ by simp[LOG] >>
471 DECIDE_TAC) >>
472 strip_tac >> Cases_on ‘x = 0’ >> simp[] >>
473 CCONTR_TAC >> full_simp_tac (srw_ss()) [NOT_LESS]>>
474 ‘x < b ** (SUC (LOG b x))’ by simp[LOG] >>
475 ‘b ** e < b ** (SUC (LOG b x))’ by DECIDE_TAC >>
476 pop_assum mp_tac >> ‘1 < b’ by simp[] >>
477 pop_assum mp_tac >>
478 simp_tac (srw_ss()) [] >> simp[]
479QED
480
481Theorem NB12_NEQ0[local]:
482 NUMERAL (BIT1 n) <> 0 /\ NUMERAL (BIT2 n) <> 0 /\
483 0 < NUMERAL (BIT1 n) /\ 0 < NUMERAL (BIT2 n) /\
484 (NUMERAL (BIT2 n) <= 1 <=> F) /\ (NUMERAL (BIT2 n) <> 1) /\
485 (NUMERAL (BIT1 n) <= 1 <=> NUMERAL (BIT1 n) = 1) /\
486 NUMERAL (BIT1 (BIT1 n)) <> 1 /\ NUMERAL (BIT1 (BIT2 n)) <> 1
487Proof
488 REWRITE_TAC[NUMERAL_DEF, BIT1, BIT2, ADD_CLAUSES, numTheory.NOT_SUC,
489 GSYM NOT_ZERO_LT_ZERO, LESS_EQ_MONO] >>
490 REWRITE_TAC[ALT_ZERO, ADD_CLAUSES, NOT_SUC_LESS_EQ_0,
491 prim_recTheory.INV_SUC_EQ, numTheory.NOT_SUC] >>
492 REWRITE_TAC [LESS_OR_EQ, LT]
493QED
494
495Theorem LT_EXP_LOG_SIMP[simp] =
496 CONJ
497 (LT_EXP_LOG |> Q.INST [‘x’ |-> ‘NUMERAL $ BIT1 x’, ‘b’ |-> ‘NUMERAL b’])
498 (LT_EXP_LOG |> Q.INST [‘x’ |-> ‘NUMERAL $ BIT2 x’, ‘b’ |-> ‘NUMERAL b’])
499 |> REWRITE_RULE[NB12_NEQ0]
500
501Theorem EXP_LE_LOG_SIMP[simp] =
502 LT_EXP_LOG_SIMP
503 |> ONCE_REWRITE_RULE [tautLib.TAUT_PROVE “(x <=> y) <=> (~x <=> ~y)”]
504 |> REWRITE_RULE [NOT_LESS, DE_MORGAN_THM, NOT_LESS_EQUAL]
505
506fun trip f g h x = (f x, g x, h x)
507fun conj3 (x,y,z) = CONJ x (CONJ y z)
508
509Theorem LE_EXP_LOG_SIMP[simp] =
510 LT_EXP_LOG
511 |> Q.INST [‘x’ |-> ‘x - 1’, ‘b’ |-> ‘NUMERAL b’]
512 |> SIMP_RULE bool_ss
513 [DECIDE “0 < x ==> (x - 1 < y <=> x <= y)”, ASSUME “0 < x”]
514 |> DISCH_ALL
515 |> trip (Q.INST [‘x’ |-> ‘NUMERAL (BIT1 (BIT1 x))’])
516 (Q.INST [‘x’ |-> ‘NUMERAL (BIT1 (BIT2 x))’])
517 (Q.INST [‘x’ |-> ‘NUMERAL (BIT2 x)’])
518 |> conj3
519 |> REWRITE_RULE[NB12_NEQ0,SUB_RIGHT_EQ, ADD_CLAUSES, LESS_EQ_REFL,
520 DECIDE “x = y \/ x <= y <=> x <= y”]
521
522Theorem EXP_LT_LOG_SIMP[simp] =
523 LE_EXP_LOG_SIMP
524 |> ONCE_REWRITE_RULE [tautLib.TAUT_PROVE “(x <=> y) <=> (~x <=> ~y)”]
525 |> REWRITE_RULE [NOT_LESS, DE_MORGAN_THM, NOT_LESS_EQUAL]
526
527Theorem less_lemma1[local]:
528 a <= c /\ b <= d ==> a * b <= c * d:num
529Proof
530 REPEAT STRIP_TAC
531 THEN MATCH_MP_TAC LESS_EQ_TRANS
532 THEN Q.EXISTS_TAC `c * b`
533 THEN REWRITE_TAC [LE_MULT_LCANCEL, LE_MULT_RCANCEL]
534 THEN DECIDE_TAC
535QED
536
537Theorem div_lemma1[local]:
538 !a b c. 0 < b /\ 0 < c ==> (a DIV b) ** c <= a ** c DIV b ** c
539Proof
540 REPEAT STRIP_TAC
541 THEN Induct_on `c`
542 THEN1 DECIDE_TAC
543 THEN STRIP_TAC
544 THEN Cases_on `0 < c`
545 THENL [FULL_SIMP_TAC bool_ss [EXP], `c = 0` by DECIDE_TAC]
546 THEN ASM_REWRITE_TAC [EXP, LESS_EQ_REFL, MULT_CLAUSES]
547 THEN MATCH_MP_TAC LESS_EQ_TRANS
548 THEN Q.EXISTS_TAC `(a DIV b) * (a ** c DIV b ** c)`
549 THEN RW_TAC bool_ss [LE_MULT_LCANCEL]
550 THEN `0 < b ** c`
551 by (Cases_on `b`
552 THEN REWRITE_TAC [ZERO_LESS_EXP]
553 THEN DECIDE_TAC)
554 THEN RW_TAC bool_ss
555 [GSYM (CONV_RULE
556 (ONCE_DEPTH_CONV (REWR_CONV MULT_COMM)) DIV_DIV_DIV_MULT),
557 X_LE_DIV]
558 THEN ONCE_REWRITE_TAC [AC_THM ``a * b * c * d = (a * c) * (b * d:num)``]
559 THEN MATCH_MP_TAC less_lemma1
560 THEN METIS_TAC [DIVISION, DECIDE ``(a = b + c) ==> b <= a:num``]
561QED
562
563Theorem square_add_lemma[local]:
564 a ** e * b ** e = (a * b:num) ** e
565Proof
566 Induct_on `e`
567 THEN RW_TAC arith_ss [EXP]
568 THEN METIS_TAC [MULT_COMM, MULT_ASSOC]
569QED
570
571Theorem ROOT_DIV:
572 !r x y. 0 < r /\ 0 < y ==> (ROOT r x DIV y = ROOT r (x DIV (y ** r)))
573Proof
574 REPEAT STRIP_TAC
575 THEN MATCH_MP_TAC (GSYM ROOT_UNIQUE)
576 THEN `0 < y ** r`
577 by (Cases_on `y`
578 THEN REWRITE_TAC [ZERO_LESS_EXP]
579 THEN DECIDE_TAC)
580 THEN CONJ_TAC
581 THENL [
582 MATCH_MP_TAC LESS_EQ_TRANS
583 THEN EXISTS_TAC ``(ROOT r x) ** r DIV y ** r``
584 THEN RW_TAC bool_ss [div_lemma1]
585 THEN METIS_TAC [DIV_LE_MONOTONE, ROOT],
586 RW_TAC bool_ss [DIV_LT_X]
587 THEN MATCH_MP_TAC (DECIDE ``!a b c. a < b /\ b <= c ==> a < c:num``)
588 THEN EXISTS_TAC ``SUC (ROOT r x) ** r``
589 THEN RW_TAC bool_ss [ROOT]
590 THEN REWRITE_TAC [square_add_lemma]
591 THEN MATCH_MP_TAC (UNDISCH (SPEC_ALL exp_lemma3))
592 THEN REWRITE_TAC [ADD1, RIGHT_ADD_DISTRIB, MULT_CLAUSES]
593 THEN GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) bool_rewrites
594 [SPEC ``ROOT r x`` (UNDISCH (SPEC ``y:num`` DIVISION))]
595 THEN REWRITE_TAC [GSYM ADD_ASSOC, LE_ADD_LCANCEL]
596 THEN METIS_TAC [DECIDE ``a < b ==> a + 1n <= b``, DIVISION]]
597QED
598
599Theorem ROOT_LE_MONO:
600 !r x y. 0 < r ==> x <= y ==> ROOT r x <= ROOT r y
601Proof
602 REPEAT STRIP_TAC
603 THEN REWRITE_TAC [DECIDE ``a <= b <=> a < SUC b``]
604 THEN ONCE_REWRITE_TAC [UNDISCH (SPEC_ALL EXP_LT_ISO)]
605 THEN MATCH_MP_TAC
606 (DECIDE ``!a b c d. a <= b /\ b <= c /\ c < d ==> a < d:num``)
607 THEN Q.EXISTS_TAC `x`
608 THEN Q.EXISTS_TAC `y`
609 THEN RW_TAC bool_ss [ROOT]
610QED
611
612Theorem EXP_MUL:
613 !a b c. (a ** b) ** c = a ** (b * c)
614Proof
615 Induct_on `c`
616 THEN REWRITE_TAC [MULT_CLAUSES, EXP_ADD, ADD1, LEFT_ADD_DISTRIB, EXP, EXP_1]
617 THEN PROVE_TAC []
618QED
619
620Theorem LOG_ROOT:
621 !a x r. 1 < a /\ 0 < x /\ 0 < r ==> (LOG a (ROOT r x) = (LOG a x) DIV r)
622Proof
623 REPEAT STRIP_TAC
624 THEN MATCH_MP_TAC LOG_UNIQUE
625 THEN CONJ_TAC
626 THENL [
627 REWRITE_TAC [DECIDE ``a <= b <=> a < SUC b``]
628 THEN ONCE_REWRITE_TAC [UNDISCH (SPEC_ALL EXP_LT_ISO)]
629 THEN MATCH_MP_TAC (DECIDE ``!a b c. a <= b /\ b < c ==> a < c:num``)
630 THEN Q.EXISTS_TAC `x`
631 THEN RW_TAC bool_ss [ROOT, EXP_MUL]
632 THEN MATCH_MP_TAC LESS_EQ_TRANS
633 THEN Q.EXISTS_TAC `a ** (LOG a x)`
634 THEN RW_TAC bool_ss [LOG, GSYM LE_EXP_ISO],
635 ONCE_REWRITE_TAC [UNDISCH (SPEC_ALL EXP_LT_ISO)]
636 THEN MATCH_MP_TAC (DECIDE ``!a b c d. a <= b /\ b < c ==> a < c:num``)
637 THEN Q.EXISTS_TAC `x`
638 THEN RW_TAC bool_ss [ROOT, EXP_MUL]
639 THEN MATCH_MP_TAC (DECIDE ``!a b c. a < b /\ b <= c ==> a < c:num``)
640 THEN Q.EXISTS_TAC `a ** SUC (LOG a x)`
641 THEN RW_TAC bool_ss [LOG, GSYM LE_EXP_ISO]
642 THEN RW_TAC bool_ss [ADD1, RIGHT_ADD_DISTRIB, MULT_CLAUSES]
643 THEN GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) bool_rewrites
644 [SPEC ``LOG a x`` (UNDISCH (SPEC ``r:num`` DIVISION))]
645 THEN REWRITE_TAC [LT_ADD_LCANCEL, DECIDE ``a + 1 <= b <=> a < b:num``]]
646 THEN METIS_TAC [DIVISION, DECIDE ``(a = b + c) ==> (b <= a:num)``]
647QED
648
649Theorem zero_lt_twoexp[local]:
650 !n. 0 < 2 ** n
651Proof
652 Induct
653 THEN REWRITE_TAC [EXP]
654 THEN TRY (MATCH_MP_TAC LESS_MULT2)
655 THEN DECIDE_TAC
656QED
657
658Theorem LOG_MOD:
659 !n. 0 < n ==> (n = 2 ** LOG 2 n + n MOD 2 ** LOG 2 n)
660Proof
661 REPEAT STRIP_TAC
662 THEN Cases_on `?b c. (n = b + 2 ** c) /\ b < 2 ** c`
663 THEN RW_TAC bool_ss []
664 THEN1 (RW_TAC bool_ss [LOG_ADD, DECIDE ``1 < 2n``]
665 THEN METIS_TAC [ADD_MODULUS_LEFT, ADD_COMM, LESS_MOD, zero_lt_twoexp,
666 DECIDE ``b < a ==> 0n < a``])
667 THEN POP_ASSUM (fn th => CCONTR_TAC THEN MP_TAC th)
668 THEN RW_TAC arith_ss []
669 THEN POP_ASSUM (K ALL_TAC)
670 THEN Induct_on `n`
671 THEN RW_TAC arith_ss []
672 THEN Cases_on `n`
673 THEN FULL_SIMP_TAC arith_ss []
674 THENL [
675 Q.EXISTS_TAC `0`
676 THEN Q.EXISTS_TAC `0`
677 THEN RW_TAC arith_ss [EXP],
678 Cases_on `SUC b < 2 ** c`
679 THENL [
680 Q.EXISTS_TAC `SUC b`
681 THEN Q.EXISTS_TAC `c`
682 THEN RW_TAC arith_ss [],
683 FULL_SIMP_TAC arith_ss [NOT_LESS]
684 THEN `SUC b = 2 ** c` by DECIDE_TAC
685 THEN ASM_REWRITE_TAC [DECIDE ``SUC (a + b) = SUC a + b``]]]
686 THEN Q.EXISTS_TAC `0`
687 THEN Q.EXISTS_TAC `SUC c`
688 THEN RW_TAC arith_ss [EXP]
689QED
690
691local
692val numtac = REWRITE_TAC[NUMERAL_DEF, BIT1, BIT2, ALT_ZERO, ADD_CLAUSES,
693 prim_recTheory.LESS_0, prim_recTheory.LESS_MONO_EQ]
694fun numpr t = prove(t,numtac)
695val one_lt_ths = map numpr [“1 < NUMERAL (BIT1 (BIT1 b))”,
696 “1 < NUMERAL (BIT1 (BIT2 b))”,
697 “1 < NUMERAL (BIT2 b)”]
698val zero_lt_ths = map numpr [“0 < NUMERAL (BIT1 n)”,
699 “0 < NUMERAL (BIT2 n)”]
700val allths = List.concat $ map (fn lt1 => map (CONJ lt1) zero_lt_ths) one_lt_ths
701in
702Theorem LOG_NUMERAL[compute,simp] =
703 map (MATCH_MP LOG_RWT) allths |> LIST_CONJ |> REWRITE_RULE [ADD1];
704end (* local *)
705
706
707Theorem lem[local]:
708 0 < r ==> (0 ** r = 0)
709Proof RW_TAC arith_ss [EXP_EQ_0]
710QED
711
712Theorem ROOT_COMPUTE:
713 !r n.
714 0 < r ==>
715 (ROOT r 0 = 0) /\
716 (ROOT r n = let x = 2 * ROOT r (n DIV 2 ** r) in
717 if n < SUC x ** r then x else SUC x)
718Proof
719 RW_TAC (arith_ss ++ boolSimps.LET_ss) []
720 THEN MATCH_MP_TAC ROOT_UNIQUE
721 THEN CONJ_TAC
722 THEN FULL_SIMP_TAC arith_ss [NOT_LESS, EXP_1, lem]
723 THEN MAP_FIRST MATCH_MP_TAC
724 [LESS_EQ_TRANS, DECIDE ``!a b c. a < b /\ b <= c ==> a < c``]
725 THENL [
726 Q.EXISTS_TAC `ROOT r n ** r`,
727 Q.EXISTS_TAC `SUC (ROOT r n) ** r`]
728 THEN RW_TAC arith_ss
729 [ROOT, GSYM EXP_LE_ISO, GSYM ROOT_DIV, DECIDE ``0 < 2n``]
730 THEN METIS_TAC
731 [DIVISION, MULT_COMM, DECIDE ``0 < 2n``,
732 DECIDE ``(a = b + c) ==> b <= a:num``, ADD1, LE_ADD_LCANCEL,
733 DECIDE ``a <= 1 <=> a < 2n``]
734QED
735
736(* For evaluation of ROOT r n in HOL4 interactive session. *)
737Theorem ROOT_EVAL[compute]:
738 !r n. ROOT r n =
739 if r = 0 then ROOT 0 n else
740 if n = 0 then 0 else
741 let m = 2 * (ROOT r (n DIV 2 ** r)) in
742 m + if (SUC m) ** r <= n then 1 else 0
743Proof
744 rpt strip_tac >>
745 (Cases_on `r = 0` >> asm_simp_tac arith_ss[LET_THM]) >>
746 `0 < r` by asm_simp_tac arith_ss[] >>
747 (Cases_on `n = 0` >> asm_simp_tac arith_ss[Once ROOT_COMPUTE, LET_THM]) >>
748 `0 DIV 2 ** r = 0` by RW_TAC arith_ss[ZERO_DIV] >>
749 METIS_TAC[ROOT_COMPUTE]
750QED
751
752
753Definition SQRTd_def[nocompute]: SQRTd n = (ROOT 2 n, n - (ROOT 2 n * ROOT 2 n))
754End
755
756Definition iSQRTd_def[nocompute]:
757 iSQRTd (x,n) =
758 let p = SQRTd n in
759 let next = 4 * SND p + x in
760 let ndiff = 4 * FST p + 1 in
761 if next < ndiff then (2 * FST p,next)
762 else (2 * FST p + 1,next - ndiff)
763End
764
765Theorem sqrt_zero[local]:
766 ROOT 2 0 = 0
767Proof RW_TAC arith_ss [ROOT_COMPUTE]
768QED
769val sqrt_compute = SIMP_RULE arith_ss [] (SPEC ``2n`` ROOT_COMPUTE);
770
771val mult_eq_lemma =
772 METIS_PROVE [MULT_COMM, MULT_ASSOC, DECIDE ``2 * 2 = 4n``]
773 ``2 * a * (2 * a) = 4n * (a * a)``
774
775Theorem iSQRT_lemma[local]:
776 SQRTd m = iSQRTd (m MOD 4,m DIV 4)
777Proof
778 REWRITE_TAC [SQRTd_def]
779 THEN REWRITE_TAC [iSQRTd_def, FST, SND]
780 THEN REWRITE_TAC [SQRTd_def]
781 THEN RW_TAC (bool_ss ++ boolSimps.LET_ss) [FST, SND]
782 THEN (SUBGOAL_THEN ``(4 * (ROOT 2 (m DIV 4) * ROOT 2 (m DIV 4)) <= m /\
783 ROOT 2 (m DIV 4) * ROOT 2 (m DIV 4) <= m DIV 4) /\
784 ROOT 2 m * ROOT 2 m <= m``
785 (fn th =>
786 RW_TAC bool_ss []
787 THEN FULL_SIMP_TAC bool_ss
788 [SIMP_RULE arith_ss [] (SPEC ``4n`` (GSYM DIVISION)), th,
789 DECIDE ``a <= b ==> (4 * (b - a) + c =
790 (b * 4 + c) - (4 * a))``,
791 SUB_CANCEL,
792 DECIDE ``a <= b ==> (b - a <= c <=> b < a + (c + 1n))``]
793 THEN ASSUME_TAC (CONJUNCT2 th))
794 THEN1 METIS_TAC [EXP, DECIDE ``2 = SUC 1``, EXP_1, ROOT, DECIDE ``0 < 2n``,
795 DECIDE ``0 < 4n``, MULT_COMM, X_LE_DIV]
796 THEN Cases_on `m = 0`
797 THEN RW_TAC arith_ss [sqrt_zero]
798 THEN RW_TAC arith_ss
799 [SUB_CANCEL,
800 DECIDE ``~(m < 4 * a + (4 * b + 1)) ==> 4 * a + (2 * b + 1) <= m``]
801 THEN GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) bool_rewrites
802 [CONJUNCT2 (SPEC_ALL sqrt_compute)]
803 THEN RW_TAC (arith_ss ++ boolSimps.LET_ss)
804 [mult_eq_lemma, ADD1, LEFT_ADD_DISTRIB, RIGHT_ADD_DISTRIB]
805 THEN PAT_X_ASSUM ``~(a < b:num)`` MP_TAC
806 THEN FULL_SIMP_TAC arith_ss
807 [ADD1, LEFT_ADD_DISTRIB, RIGHT_ADD_DISTRIB, mult_eq_lemma,
808 METIS_PROVE [DECIDE ``SUC 1 = 2``, EXP, EXP_1]
809 ``a ** 2 = a * a:num``])
810QED
811
812Theorem numeral_sqrt0[local]:
813 (SQRTd ZERO = (0,0)) /\
814 (SQRTd (BIT1 ZERO)= (1,0)) /\
815 (SQRTd (BIT2 ZERO)= (1,1)) /\
816 (SQRTd (BIT1 (BIT1 n)) = iSQRTd (3,n)) /\
817 (SQRTd (BIT2 (BIT1 n)) = iSQRTd (0,SUC n)) /\
818 (SQRTd (BIT1 (BIT2 n)) = iSQRTd (1,SUC n)) /\
819 (SQRTd (BIT2 (BIT2 n)) = iSQRTd (2,SUC n)) /\
820 (SQRTd (SUC (BIT1 (BIT1 n))) = iSQRTd (0,SUC n)) /\
821 (SQRTd (SUC (BIT2 (BIT1 n))) = iSQRTd (1,SUC n)) /\
822 (SQRTd (SUC (BIT1 (BIT2 n))) = iSQRTd (2,SUC n)) /\
823 (SQRTd (SUC (BIT2 (BIT2 n))) = iSQRTd (3,SUC n))
824Proof
825 REWRITE_TAC [BIT1, BIT2, ALT_ZERO, ADD_CLAUSES, NUMERAL_DEF]
826 THEN RW_TAC arith_ss [iSQRT_lemma, ADD1]
827 THEN RW_TAC (arith_ss ++ boolSimps.LET_ss) [iSQRTd_def, SQRTd_def, sqrt_zero]
828QED
829
830Definition iSQRT0_def:
831 iSQRT0 n =
832 let p = SQRTd n in
833 let d = SND p - FST p in
834 if d = 0 then (2 * FST p,4 * SND p) else (SUC (2 * FST p),4 * d - 1)
835End
836
837Definition iSQRT1_def:
838 iSQRT1 n =
839 let p = SQRTd n in
840 let d = (SUC (SND p) - FST p) in
841 if d = 0 then (2 * FST p, SUC (4 * SND p))
842 else (SUC (2 * FST p),4 * (d - 1))
843End
844
845Definition iSQRT2_def:
846 iSQRT2 n =
847 let p = SQRTd n in
848 let d = 2 * FST p in
849 let c = SUC (2 * SND p) in
850 let e = c - d in
851 if e = 0 then (d,2 * c) else (SUC d, 2 * e - 1)
852End
853
854Definition iSQRT3_def:
855 iSQRT3 n =
856 let p = SQRTd n in
857 let d = 2 * FST p in
858 let c = SUC (2 * (SND p)) in
859 let e = SUC c - d in
860 if e = 0 then (d,SUC (2 * c)) else (SUC d, 2 * (e - 1))
861End
862
863Theorem numeral_sqrt[compute]:
864 (SQRTd ZERO = (0,0)) /\
865 (SQRTd (BIT1 ZERO) = (1,0)) /\
866 (SQRTd (BIT2 ZERO) = (1,1)) /\
867 (SQRTd (BIT1 (BIT1 n)) = iSQRT3 n) /\
868 (SQRTd (BIT2 (BIT1 n)) = iSQRT0 (SUC n)) /\
869 (SQRTd (BIT1 (BIT2 n)) = iSQRT1 (SUC n)) /\
870 (SQRTd (BIT2 (BIT2 n)) = iSQRT2 (SUC n)) /\
871 (SQRTd (SUC (BIT1 (BIT1 n))) = iSQRT0 (SUC n)) /\
872 (SQRTd (SUC (BIT2 (BIT1 n))) = iSQRT1 (SUC n)) /\
873 (SQRTd (SUC (BIT1 (BIT2 n))) = iSQRT2 (SUC n)) /\
874 (SQRTd (SUC (BIT2 (BIT2 n))) = iSQRT3 (SUC n))
875Proof
876 RW_TAC(arith_ss ++ boolSimps.LET_ss) [numeral_sqrt0]
877 THEN REWRITE_TAC [iSQRT0_def, iSQRT1_def, iSQRT2_def, iSQRT3_def]
878 THEN RW_TAC (arith_ss ++ boolSimps.LET_ss) [iSQRTd_def, ADD1]
879QED
880
881Theorem numeral_root2[compute]:
882 ROOT 2 (NUMERAL n) = FST (SQRTd n)
883Proof REWRITE_TAC [FST, SQRTd_def, NUMERAL_DEF]
884QED
885
886val () = Theory.delete_const "iSQRTd"
887
888(* ------------------------------------------------------------------------- *)
889(* ROOT Computation *)
890(* ------------------------------------------------------------------------- *)
891
892(* Theorem: ROOT n (a ** n) = a *)
893(* Proof:
894 Since a < SUC a by LESS_SUC
895 a ** n < (SUC a) ** n by EXP_BASE_LT_MONO
896 Let b = a ** n,
897 Then a ** n <= b by LESS_EQ_REFL
898 and b < (SUC a) ** n by above
899 Hence a = ROOT n b by ROOT_UNIQUE
900*)
901Theorem ROOT_POWER:
902 !a n. 1 < a /\ 0 < n ==> (ROOT n (a ** n) = a)
903Proof
904 rw[EXP_BASE_LT_MONO, ROOT_UNIQUE]
905QED
906
907(* Theorem: 0 < m /\ (b ** m = n) ==> (b = ROOT m n) *)
908(* Proof:
909 Note n <= n by LESS_EQ_REFL
910 so b ** m <= n by b ** m = n
911 Also b < SUC b by LESS_SUC
912 so b ** m < (SUC b) ** m by EXP_EXP_LT_MONO, 0 < m
913 so n < (SUC b) ** m by b ** m = n
914 Thus b = ROOT m n by ROOT_UNIQUE
915*)
916Theorem ROOT_FROM_POWER:
917 !m n b. 0 < m /\ (b ** m = n) ==> (b = ROOT m n)
918Proof
919 rpt strip_tac >>
920 rw[ROOT_UNIQUE]
921QED
922
923(* Theorem: 0 < m ==> (ROOT m 0 = 0) *)
924(* Proof:
925 Note 0 ** m = 0 by EXP_0
926 Thus 0 = ROOT m 0 by ROOT_FROM_POWER
927*)
928Theorem ROOT_OF_0[simp]:
929 !m. 0 < m ==> (ROOT m 0 = 0)
930Proof
931 rw[ROOT_FROM_POWER]
932QED
933
934(* Theorem: 0 < m ==> (ROOT m 1 = 1) *)
935(* Proof:
936 Note 1 ** m = 1 by EXP_1
937 Thus 1 = ROOT m 1 by ROOT_FROM_POWER
938*)
939Theorem ROOT_OF_1[simp]:
940 !m. 0 < m ==> (ROOT m 1 = 1)
941Proof
942 rw[ROOT_FROM_POWER]
943QED
944
945(* Proof:
946 If part: 0 < r ==> ROOT r n ** r <= n /\ n < SUC (ROOT r n) ** r
947 This is true by ROOT, 0 < r
948 Only-if part: p ** r <= n /\ n < SUC p ** r ==> ROOT r n = p
949 This is true by ROOT_UNIQUE
950*)
951Theorem ROOT_THM:
952 !r. 0 < r ==> !n p. (ROOT r n = p) <=> (p ** r <= n /\ n < SUC p ** r)
953Proof
954 metis_tac[ROOT, ROOT_UNIQUE]
955QED
956
957(* Theorem: 0 < m ==> !n. (ROOT m n = 0) <=> (n = 0) *)
958(* Proof:
959 If part: ROOT m n = 0 ==> n = 0
960 Note n < SUC (ROOT m n) ** r by ROOT
961 or n < SUC 0 ** m by ROOT m n = 0
962 so n < 1 by ONE, EXP_1
963 or n = 0 by arithmetic
964 Only-if part: ROOT m 0 = 0, true by ROOT_OF_0
965*)
966Theorem ROOT_EQ_0:
967 !m. 0 < m ==> !n. (ROOT m n = 0) <=> (n = 0)
968Proof
969 rw[EQ_IMP_THM] >>
970 `n < 1` by metis_tac[ROOT, EXP_1, ONE] >>
971 decide_tac
972QED
973
974(* Theorem: ROOT 1 n = n *)
975(* Proof:
976 Note n ** 1 = n by EXP_1
977 so n ** 1 <= n
978 Also n < SUC n by LESS_SUC
979 so n < SUC n ** 1 by EXP_1
980 Thus ROOT 1 n = n by ROOT_UNIQUE
981*)
982Theorem ROOT_1[simp]:
983 !n. ROOT 1 n = n
984Proof
985 rw[ROOT_UNIQUE]
986QED
987
988(* Proof:
989 Let x = ROOT r n, y = ROOT r (SUC n). x <= y.
990 Note n < (SUC x) ** r /\ x ** r <= n by ROOT_THM
991 and SUC n < (SUC y) ** r /\ y ** r <= SUC n by ROOT_THM
992 Since n < (SUC x) ** r,
993 SUC n <= (SUC x) ** r.
994 If SUC n = (SUC x) ** r,
995 Then y = ROOT r (SUC n)
996 = ROOT r ((SUC x) ** r)
997 = SUC x by ROOT_POWER
998 If SUC n < (SUC x) ** r,
999 Then x ** r <= n < SUC n by LESS_SUC
1000 Thus x = y by ROOT_THM
1001*)
1002Theorem ROOT_SUC:
1003 !r n. 0 < r ==>
1004 (ROOT r (SUC n) = ROOT r n + if SUC n = (SUC (ROOT r n)) ** r then 1 else 0)
1005Proof
1006 rpt strip_tac >>
1007 qabbrev_tac `x = ROOT r n` >>
1008 qabbrev_tac `y = ROOT r (SUC n)` >>
1009 Cases_on `n = 0` >| [
1010 `x = 0` by rw[ROOT_OF_0, Abbr`x`] >>
1011 `y = 1` by rw[ROOT_OF_1, Abbr`y`] >>
1012 simp[],
1013 `x <> 0` by rw[ROOT_EQ_0, Abbr`x`] >>
1014 `n < (SUC x) ** r /\ x ** r <= n` by metis_tac[ROOT_THM] >>
1015 `SUC n < (SUC y) ** r /\ y ** r <= SUC n` by metis_tac[ROOT_THM] >>
1016 `(SUC n = (SUC x) ** r) \/ SUC n < (SUC x) ** r` by decide_tac >| [
1017 `1 < SUC x` by decide_tac >>
1018 `y = SUC x` by metis_tac[ROOT_POWER] >>
1019 simp[],
1020 `x ** r <= SUC n` by decide_tac >>
1021 `x = y` by metis_tac[ROOT_THM] >>
1022 simp[]
1023 ]
1024 ]
1025QED
1026
1027(* Proof:
1028 ROOT m n = 1
1029 <=> 1 ** m <= n /\ n < (SUC 1) ** m by ROOT_THM, 0 < m
1030 <=> 1 <= n /\ n < 2 ** m by TWO, EXP_1
1031 <=> 0 < n /\ n < 2 ** m by arithmetic
1032*)
1033Theorem ROOT_EQ_1:
1034 !m. 0 < m ==> !n. (ROOT m n = 1) <=> (0 < n /\ n < 2 ** m)
1035Proof
1036 rpt strip_tac >>
1037 `!n. 0 < n <=> 1 <= n` by decide_tac >>
1038 metis_tac[ROOT_THM, TWO, EXP_1]
1039QED
1040
1041(* Theorem: 0 < m ==> ROOT m n <= n *)
1042(* Proof:
1043 Let r = ROOT m n.
1044 Note r <= r ** m by X_LE_X_EXP, 0 < m
1045 <= n by ROOT
1046*)
1047Theorem ROOT_LE_SELF:
1048 !m n. 0 < m ==> ROOT m n <= n
1049Proof
1050 metis_tac[X_LE_X_EXP, ROOT, LESS_EQ_TRANS]
1051QED
1052
1053(* Theorem: 0 < m ==> ((ROOT m n = n) <=> ((m = 1) \/ (n = 0) \/ (n = 1))) *)
1054(* Proof:
1055 If part: ROOT m n = n ==> m = 1 \/ n = 0 \/ n = 1
1056 Note n ** m <= n by ROOT, 0 < r
1057 But n <= n ** m by X_LE_X_EXP, 0 < m
1058 so n ** m = n by EQ_LESS_EQ
1059 ==> m = 1 or n = 0 or n = 1 by EXP_EQ_SELF
1060 Only-if part: ROOT 1 n = n /\ ROOT m 0 = 0 /\ ROOT m 1 = 1
1061 True by ROOT_1, ROOT_OF_0, ROOT_OF_1.
1062*)
1063Theorem ROOT_EQ_SELF:
1064 !m n. 0 < m ==> (ROOT m n = n <=> m = 1 \/ n = 0 \/ n = 1)
1065Proof
1066 rw_tac std_ss[EQ_IMP_THM] >> rw[] >>
1067 `n ** m <= n` by metis_tac[ROOT] >>
1068 `n <= n ** m` by rw[X_LE_X_EXP] >>
1069 `n ** m = n` by decide_tac >>
1070 fs[]
1071QED
1072
1073(* Theorem: 0 < m ==> (n <= ROOT m n <=> ((m = 1) \/ (n = 0) \/ (n = 1))) *)
1074(* Proof:
1075 Note ROOT m n <= n by ROOT_LE_SELF
1076 Thus n <= ROOT m n <=> ROOT m n = n by EQ_LESS_EQ
1077 The result follows by ROOT_EQ_SELF
1078*)
1079Theorem ROOT_GE_SELF:
1080 !m n. 0 < m ==> (n <= ROOT m n <=> ((m = 1) \/ (n = 0) \/ (n = 1)))
1081Proof
1082 metis_tac[ROOT_LE_SELF, ROOT_EQ_SELF, EQ_LESS_EQ]
1083QED
1084
1085(*
1086EVAL “MAP (\k. ROOT k 100) [1 .. 10]”;
1087 |- ... = [100; 10; 4; 3; 2; 2; 1; 1; 1; 1]: thm
1088
1089This shows (ROOT k) is a decreasing function of k,
1090but this is very hard to prove without some real number theory.
1091Even this is hard to prove: ROOT 3 n <= ROOT 2 n
1092
1093No! -- this can be proved, see below.
1094*)
1095
1096(* Theorem: 0 < a /\ a <= b ==> ROOT b n <= ROOT a n *)
1097(* Proof:
1098 Let x = ROOT a n, y = ROOT b n. To show: y <= x.
1099 By contradiction, suppose x < y.
1100 Then SUC x <= y.
1101 Note x ** a <= n /\ n < (SUC x) ** a by ROOT
1102 and y ** b <= n /\ n < (SUC y) ** b by ROOT
1103 But a <= b
1104 (SUC x) ** a
1105 <= (SUC x) ** b by EXP_BASE_LEQ_MONO_IMP, 0 < SUC x, a <= b
1106 <= y ** b by EXP_EXP_LE_MONO, 0 < b
1107 This leads to n < (SUC x) ** a <= y ** b <= n, a contradiction.
1108*)
1109Theorem ROOT_LE_REVERSE:
1110 !a b n. 0 < a /\ a <= b ==> ROOT b n <= ROOT a n
1111Proof
1112 rpt strip_tac >>
1113 qabbrev_tac `x = ROOT a n` >>
1114 qabbrev_tac `y = ROOT b n` >>
1115 spose_not_then strip_assume_tac >>
1116 `0 < b /\ SUC x <= y` by decide_tac >>
1117 `x ** a <= n /\ n < (SUC x) ** a` by rw[ROOT, Abbr`x`] >>
1118 `y ** b <= n /\ n < (SUC y) ** b` by rw[ROOT, Abbr`y`] >>
1119 `(SUC x) ** a <= (SUC x) ** b` by rw[EXP_BASE_LEQ_MONO_IMP] >>
1120 `(SUC x) ** b <= y ** b` by rw[EXP_EXP_LE_MONO] >>
1121 decide_tac
1122QED
1123
1124(* ------------------------------------------------------------------------- *)
1125(* Square Root *)
1126(* ------------------------------------------------------------------------- *)
1127
1128(* Use overload for SQRT *)
1129Overload SQRT = ``\n. ROOT 2 n``
1130
1131(* Theorem: 0 < n ==> (SQRT n) ** 2 <= n /\ n < SUC (SQRT n) ** 2 *)
1132(* Proof: by ROOT:
1133 |- !r n. 0 < r ==> ROOT r n ** r <= n /\ n < SUC (ROOT r n) ** r
1134*)
1135Theorem SQRT_PROPERTY:
1136 !n. (SQRT n) ** 2 <= n /\ n < SUC (SQRT n) ** 2
1137Proof
1138 rw[ROOT]
1139QED
1140
1141(* Get a useful theorem *)
1142(* |- !n p. p ** 2 <= n /\ n < SUC p ** 2 ==> SQRT n = p *)
1143Theorem SQRT_UNIQUE = ROOT_UNIQUE |> SPEC ``2``;
1144
1145(* |- !n p. (SQRT n = p) <=> p ** 2 <= n /\ n < SUC p ** 2 *)
1146Theorem SQRT_THM =
1147 ROOT_THM |> SPEC ``2`` |> SIMP_RULE (srw_ss())[];
1148
1149(* Theorem: n <= m ==> SQRT n <= SQRT m *)
1150(* Proof: by ROOT_LE_MONO *)
1151Theorem SQRT_LE:
1152 !n m. n <= m ==> SQRT n <= SQRT m
1153Proof
1154 rw[ROOT_LE_MONO]
1155QED
1156
1157(* Theorem: n < m ==> SQRT n <= SQRT m *)
1158(* Proof:
1159 Since n < m ==> n <= m by LESS_IMP_LESS_OR_EQ
1160 This is true by ROOT_LE_MONO
1161*)
1162Theorem SQRT_LT:
1163 !n m. n < m ==> SQRT n <= SQRT m
1164Proof
1165 rw[ROOT_LE_MONO, LESS_IMP_LESS_OR_EQ]
1166QED
1167
1168(* Theorem: SQRT 0 = 0 *)
1169(* Proof: by ROOT_OF_0 *)
1170Theorem SQRT_0[simp]:
1171 SQRT 0 = 0
1172Proof
1173 rw[]
1174QED
1175
1176(* Theorem: SQRT 1 = 1 *)
1177(* Proof: by ROOT_OF_1 *)
1178Theorem SQRT_1[simp]:
1179 SQRT 1 = 1
1180Proof
1181 rw[]
1182QED
1183
1184(* Theorem: SQRT n = 0 <=> n = 0 *)
1185(* Proof:
1186 If part: SQRT n = 0 ==> n = 0.
1187 By contradiction, suppose n <> 0.
1188 This means 1 <= n
1189 Hence SQRT 1 <= SQRT n by SQRT_LE
1190 so 1 <= SQRT n by SQRT_1
1191 This contradicts SQRT n = 0.
1192 Only-if part: n = 0 ==> SQRT n = 0
1193 True since SQRT 0 = 0 by SQRT_0
1194*)
1195Theorem SQRT_EQ_0:
1196 !n. (SQRT n = 0) <=> (n = 0)
1197Proof
1198 rw[EQ_IMP_THM] >>
1199 spose_not_then strip_assume_tac >>
1200 `1 <= n` by decide_tac >>
1201 `SQRT 1 <= SQRT n` by rw[SQRT_LE] >>
1202 `SQRT 1 = 1` by rw[] >>
1203 decide_tac
1204QED
1205
1206(* Theorem: SQRT n = 1 <=> n = 1 \/ n = 2 \/ n = 3 *)
1207(* Proof:
1208 If part: SQRT n = 1 ==> (n = 1) \/ (n = 2) \/ (n = 3).
1209 By contradiction, suppose n <> 1 /\ n <> 2 /\ n <> 3.
1210 Note n <> 0 by SQRT_EQ_0
1211 This means 4 <= n
1212 Hence SQRT 4 <= SQRT n by SQRT_LE
1213 so 2 <= SQRT n by EVAL_TAC, SQRT 4 = 2
1214 This contradicts SQRT n = 1.
1215 Only-if part: n = 1 \/ n = 2 \/ n = 3 ==> SQRT n = 1
1216 All these are true by EVAL_TAC
1217*)
1218Theorem SQRT_EQ_1:
1219 !n. (SQRT n = 1) <=> ((n = 1) \/ (n = 2) \/ (n = 3))
1220Proof
1221 rw[EQ_IMP_THM] >| [
1222 spose_not_then strip_assume_tac >>
1223 `n <> 0` by metis_tac[SQRT_EQ_0] >>
1224 `4 <= n` by decide_tac >>
1225 `SQRT 4 <= SQRT n` by rw[SQRT_LE] >>
1226 `SQRT 4 = 2` by EVAL_TAC >>
1227 decide_tac,
1228 EVAL_TAC,
1229 EVAL_TAC,
1230 EVAL_TAC
1231 ]
1232QED
1233
1234(* Theorem: SQRT (n ** 2) = n *)
1235(* Proof:
1236 If 1 < n, true by ROOT_POWER, 0 < 2
1237 Otherwise, n = 0 or n = 1.
1238 When n = 0,
1239 SQRT (0 ** 2) = SQRT 0 = 0 by SQRT_0
1240 When n = 1,
1241 SQRT (1 ** 2) = SQRT 1 = 1 by SQRT_1
1242*)
1243Theorem SQRT_EXP_2:
1244 !n. SQRT (n ** 2) = n
1245Proof
1246 rpt strip_tac >>
1247 Cases_on `1 < n` >-
1248 fs[ROOT_POWER] >>
1249 `(n = 0) \/ (n = 1)` by decide_tac >>
1250 rw[]
1251QED
1252
1253(* Theorem alias *)
1254Theorem SQRT_OF_SQ = SQRT_EXP_2;
1255(* val SQRT_OF_SQ = |- !n. SQRT (n ** 2) = n: thm *)
1256
1257(* Theorem: (n <= SQRT n) <=> ((n = 0) \/ (n = 1)) *)
1258(* Proof:
1259 If part: (n <= SQRT n) ==> ((n = 0) \/ (n = 1))
1260 By contradiction, suppose n <> 0 /\ n <> 1.
1261 Then 1 < n, implying n ** 2 <= SQRT n ** 2 by EXP_BASE_LE_MONO
1262 but SQRT n ** 2 <= n by SQRT_PROPERTY
1263 so n ** 2 <= n by LESS_EQ_TRANS
1264 or n * n <= n * 1 by EXP_2
1265 or n <= 1 by LE_MULT_LCANCEL, n <> 0.
1266 This contradicts 1 < n.
1267 Only-if part: ((n = 0) \/ (n = 1)) ==> (n <= SQRT n)
1268 This is to show:
1269 (1) 0 <= SQRT 0, true by SQRT 0 = 0 by SQRT_0
1270 (2) 1 <= SQRT 1, true by SQRT 1 = 1 by SQRT_1
1271*)
1272Theorem SQRT_GE_SELF:
1273 !n. (n <= SQRT n) <=> ((n = 0) \/ (n = 1))
1274Proof
1275 rw[EQ_IMP_THM] >| [
1276 spose_not_then strip_assume_tac >>
1277 `1 < n` by decide_tac >>
1278 `n ** 2 <= SQRT n ** 2` by rw[EXP_BASE_LE_MONO] >>
1279 `SQRT n ** 2 <= n` by rw[SQRT_PROPERTY] >>
1280 `n ** 2 <= n` by metis_tac[LESS_EQ_TRANS] >>
1281 `n * n <= n * 1` by metis_tac[EXP_2, MULT_RIGHT_1] >>
1282 `n <= 1` by metis_tac[LE_MULT_LCANCEL] >>
1283 decide_tac,
1284 rw[],
1285 rw[]
1286 ]
1287QED
1288
1289(* Theorem: (SQRT n = n) <=> ((n = 0) \/ (n = 1)) *)
1290(* Proof: by ROOT_EQ_SELF, 0 < 2 *)
1291Theorem SQRT_EQ_SELF:
1292 !n. (SQRT n = n) <=> ((n = 0) \/ (n = 1))
1293Proof
1294 rw[ROOT_EQ_SELF]
1295QED
1296
1297(* Theorem: SQRT n < m ==> n < m ** 2 *)
1298(* Proof:
1299 SQRT n < m
1300 ==> SUC (SQRT n) <= m by arithmetic
1301 ==> (SUC (SQRT m)) ** 2 <= m ** 2 by EXP_EXP_LE_MONO
1302 But n < (SUC (SQRT n)) ** 2 by SQRT_PROPERTY
1303 Thus n < m ** 2 by inequality
1304*)
1305Theorem SQRT_LT_IMP:
1306 !n m. SQRT n < m ==> n < m ** 2
1307Proof
1308 rpt strip_tac >>
1309 `SUC (SQRT n) <= m` by decide_tac >>
1310 `SUC (SQRT n) ** 2 <= m ** 2` by simp[EXP_EXP_LE_MONO] >>
1311 `n < SUC (SQRT n) ** 2` by simp[SQRT_PROPERTY] >>
1312 decide_tac
1313QED
1314
1315(* Theorem: n < SQRT m ==> n ** 2 < m *)
1316(* Proof:
1317 n < SQRT m
1318 ==> n ** 2 < (SQRT m) ** 2 by EXP_EXP_LT_MONO
1319 But (SQRT m) ** 2 <= m by SQRT_PROPERTY
1320 Thus n ** 2 < m by inequality
1321*)
1322Theorem LT_SQRT_IMP:
1323 !n m. n < SQRT m ==> n ** 2 < m
1324Proof
1325 rpt strip_tac >>
1326 `n ** 2 < (SQRT m) ** 2` by simp[EXP_EXP_LT_MONO] >>
1327 `(SQRT m) ** 2 <= m` by simp[SQRT_PROPERTY] >>
1328 decide_tac
1329QED
1330
1331(* Theorem: SQRT n < SQRT m ==> n < m *)
1332(* Proof:
1333 SQRT n < SQRT m
1334 ==> n < (SQRT m) ** 2 by SQRT_LT_IMP
1335 and (SQRT m) ** 2 <= m by SQRT_PROPERTY
1336 so n < m by inequality
1337*)
1338Theorem SQRT_LT_SQRT:
1339 !n m. SQRT n < SQRT m ==> n < m
1340Proof
1341 rpt strip_tac >>
1342 imp_res_tac SQRT_LT_IMP >>
1343 `(SQRT m) ** 2 <= m` by simp[SQRT_PROPERTY] >>
1344 decide_tac
1345QED
1346
1347(* Non-theorems:
1348 SQRT n <= SQRT m ==> n <= m
1349 counter-example: SQRT 5 = 2 = SQRT 4, but 5 > 4.
1350
1351 n < m ==> SQRT n < SQRT m
1352 counter-example: 4 < 5, but SQRT 4 = 2 = SQRT 5.
1353*)
1354
1355(* ------------------------------------------------------------------------- *)
1356(* Logarithm *)
1357(* ------------------------------------------------------------------------- *)
1358
1359(* Theorem: 1 < a ==> LOG a (a ** n) = n *)
1360(* Proof:
1361 LOG a (a ** n)
1362 = LOG a ((a ** n) * 1) by MULT_RIGHT_1
1363 = n + LOG a 1 by LOG_EXP
1364 = n + 0 by LOG_1
1365 = n by ADD_0
1366*)
1367Theorem LOG_EXACT_EXP:
1368 !a. 1 < a ==> !n. LOG a (a ** n) = n
1369Proof
1370 metis_tac[MULT_RIGHT_1, LOG_EXP, LOG_1, ADD_0, DECIDE``0 < 1``]
1371QED
1372
1373(* Theorem: 1 < a /\ 0 < b /\ b <= a ** n ==> LOG a b <= n *)
1374(* Proof:
1375 Given b <= a ** n
1376 LOG a b <= LOG a (a ** n) by LOG_LE_MONO
1377 = n by LOG_EXACT_EXP
1378*)
1379Theorem EXP_TO_LOG:
1380 !a b n. 1 < a /\ 0 < b /\ b <= a ** n ==> LOG a b <= n
1381Proof
1382 metis_tac[LOG_LE_MONO, LOG_EXACT_EXP]
1383QED
1384
1385(* Proof:
1386 If part: 1 < a /\ 0 < n ==> a ** LOG a n <= n /\ n < a ** SUC (LOG a n)
1387 This is true by LOG.
1388 Only-if part: a ** p <= n /\ n < a ** SUC p ==> LOG a n = p
1389 This is true by LOG_UNIQUE
1390*)
1391Theorem LOG_THM:
1392 !a n. 1 < a /\ 0 < n ==> !p. (LOG a n = p) <=> a ** p <= n /\ n < a ** SUC p
1393Proof
1394 metis_tac[LOG, LOG_UNIQUE]
1395QED
1396
1397(* Theorem: LOG m n = if m <= 1 \/ (n = 0) then LOG m n
1398 else if n < m then 0 else SUC (LOG m (n DIV m)) *)
1399(* Proof: by LOG_RWT *)
1400Theorem LOG_EVAL: (* was: "LOG_EVAL[compute]" *)
1401 !m n. LOG m n = if m <= 1 \/ (n = 0) then LOG m n
1402 else if n < m then 0 else SUC (LOG m (n DIV m))
1403Proof
1404 rw[LOG_RWT]
1405QED
1406(* Put to computeLib for LOG evaluation of any base *)
1407
1408(*
1409> EVAL ``MAP (LOG 3) [1 .. 20]``; =
1410 [0; 0; 1; 1; 1; 1; 1; 1; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2]: thm
1411> EVAL ``MAP (LOG 3) [1 .. 30]``; =
1412 [0; 0; 1; 1; 1; 1; 1; 1; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2;
1413 2; 2; 3; 3; 3; 3]: thm
1414*)
1415
1416(* Theorem: 1 < a /\ 0 < n ==>
1417 !p. (LOG a n = p) <=> SUC n <= a ** SUC p /\ a ** SUC p <= a * n *)
1418(* Proof:
1419 Note !p. LOG a n = p
1420 <=> n < a ** SUC p /\ a ** p <= n by LOG_THM
1421 <=> n < a ** SUC p /\ a * a ** p <= a * n by LE_MULT_LCANCEL
1422 <=> n < a ** SUC p /\ a ** SUC p <= a * n by EXP
1423 <=> SUC n <= a ** SUC p /\ a ** SUC p <= a * n by arithmetic
1424*)
1425Theorem LOG_TEST:
1426 !a n. 1 < a /\ 0 < n ==>
1427 !p. (LOG a n = p) <=> SUC n <= a ** SUC p /\ a ** SUC p <= a * n
1428Proof
1429 rw[EQ_IMP_THM] >| [
1430 `n < a ** SUC (LOG a n)` by metis_tac[LOG_THM] >>
1431 decide_tac,
1432 `a ** (LOG a n) <= n` by metis_tac[LOG_THM] >>
1433 rw[EXP],
1434 `a * a ** p <= a * n` by fs[EXP] >>
1435 `a ** p <= n` by fs[] >>
1436 `n < a ** SUC p` by decide_tac >>
1437 metis_tac[LOG_THM]
1438 ]
1439QED
1440
1441(* For continuous functions, log_b (x ** y) = y * log_b x. *)
1442
1443(* Proof:
1444 Note:
1445
1446> LOG_THM |> SPEC ``b:num`` |> SPEC ``x:num``;
1447val it = |- 1 < b /\ 0 < x ==> !p. LOG b x = p <=> b ** p <= x /\ x < b ** SUC p
1448> LOG_THM |> SPEC ``b:num`` |> SPEC ``(x:num) ** n``;
1449val it = |- 1 < b /\ 0 < x ** n ==>
1450 !p. LOG b (x ** n) = p <=> b ** p <= x ** n /\ x ** n < b ** SUC p
1451
1452 Let y = LOG b x, z = LOG b (x ** n).
1453 Then b ** y <= x /\ x < b ** SUC y by LOG_THM, (1)
1454 and b ** z <= x ** n /\ x ** n < b ** SUC z by LOG_THM, (2)
1455 From (1),
1456 b ** (n * y) <= x ** n /\ by EXP_EXP_LE_MONO,
1457 EXP_EXP_MULT
1458 x ** n < b ** (n * SUC y) by EXP_EXP_LT_MONO,
1459 EXP_EXP_MULT, 0 < n
1460 Cross combine with (2),
1461 b ** (n * y) <= x ** n < b ** SUC z
1462 and b ** z <= x ** n < b ** (n * y)
1463 ==> n * y < SUC z /\ z < n * SUC y by EXP_BASE_LT_MONO
1464 or n * y <= z /\ z < n * SUC y
1465*)
1466Theorem LOG_POWER:
1467 !b x n. 1 < b /\ 0 < x /\ 0 < n ==>
1468 n * LOG b x <= LOG b (x ** n) /\ LOG b (x ** n) < n * SUC (LOG b x)
1469Proof
1470 ntac 4 strip_tac >>
1471 `0 < x ** n` by rw[] >>
1472 qabbrev_tac `y = LOG b x` >>
1473 qabbrev_tac `z = LOG b (x ** n)` >>
1474 `b ** y <= x /\ x < b ** SUC y` by metis_tac[LOG_THM] >>
1475 `b ** z <= x ** n /\ x ** n < b ** SUC z` by metis_tac[LOG_THM] >>
1476 `b ** (y * n) <= x ** n` by rw[EXP_EXP_MULT] >>
1477 `x ** n < b ** ((SUC y) * n)` by rw[EXP_EXP_MULT] >>
1478 `b ** (y * n) < b ** SUC z` by decide_tac >>
1479 `b ** z < b ** (SUC y * n)` by decide_tac >>
1480 `y * n < SUC z` by metis_tac[EXP_BASE_LT_MONO] >>
1481 `z < SUC y * n` by metis_tac[EXP_BASE_LT_MONO] >>
1482 decide_tac
1483QED
1484
1485(* Theorem: 1 < a /\ 0 < n /\ a <= b ==> LOG b n <= LOG a n *)
1486(* Proof:
1487 Let x = LOG a n, y = LOG b n. To show: y <= x.
1488 By contradiction, suppose x < y.
1489 Then SUC x <= y.
1490 Note a ** x <= n /\ n < a ** SUC x by LOG_THM
1491 and b ** y <= n /\ n < b ** SUC y by LOG_THM
1492 But a <= b
1493 a ** SUC x
1494 <= b ** SUC x by EXP_EXP_LE_MONO, 0 < SUC x
1495 <= b ** y by EXP_BASE_LEQ_MONO_IMP, SUC x <= y
1496 This leads to n < a ** SUC x <= b ** y <= n, a contradiction.
1497*)
1498Theorem LOG_LE_REVERSE:
1499 !a b n. 1 < a /\ 0 < n /\ a <= b ==> LOG b n <= LOG a n
1500Proof
1501 rpt strip_tac >>
1502 qabbrev_tac `x = LOG a n` >>
1503 qabbrev_tac `y = LOG b n` >>
1504 spose_not_then strip_assume_tac >>
1505 `1 < b /\ SUC x <= y` by decide_tac >>
1506 `a ** x <= n /\ n < a ** SUC x` by metis_tac[LOG_THM] >>
1507 `b ** y <= n /\ n < b ** SUC y` by metis_tac[LOG_THM] >>
1508 `a ** SUC x <= b ** SUC x` by rw[EXP_EXP_LE_MONO] >>
1509 `b ** SUC x <= b ** y` by rw[EXP_BASE_LEQ_MONO_IMP] >>
1510 decide_tac
1511QED
1512
1513(* ----------------------------------------------------------------------- *)
1514
1515(*
1516
1517Testing:
1518
1519open reduceLib computeLib;
1520
1521val compset1 = num_compset;
1522
1523val _ = add_thms [numeral_root2,numeral_sqrt2,FST,SND,iSQRT0_def,iSQRT1_def,
1524 iSQRT2_def,iSQRT3_def] compset1;
1525
1526val _ = time (CBV_CONV compset2) ``SQRT 123456789123456789123456789``;
1527val _ = time (CBV_CONV compset1) ``ROOT 2 123456789123456789123456789``;
1528
1529
1530val list = map (rand o concl)
1531 (map (fn x => REDUCE_CONV (mk_mult(``12345678912345678912345678n``,
1532 term_of_int x))) (for 0 60 I));
1533
1534time (map (fn x => CBV_CONV compset1 (mk_comb(``ROOT 2``,x)))) list;
1535time (map (fn x => CBV_CONV compset2 (mk_comb(``SQRT``,x)))) list;
1536
1537
1538val compset2 = num_compset;
1539
1540val SQRT_def = Define `SQRT x = ROOT 2 x`;
1541
1542val sqrt_thm = prove(
1543 ``!x p. SQRT x = let q = p * p in
1544 if (q <= x /\ x < q + 2 * p + 1) then p else SQRT x``,
1545 RW_TAC (arith_ss ++ boolSimps.LET_ss) [SQRT_def] THEN
1546 MATCH_MP_TAC ROOT_UNIQUE THEN
1547 RW_TAC bool_ss [ADD1,EXP_ADD,EXP_1,DECIDE ``2 = SUC 1``,
1548 LEFT_ADD_DISTRIB,RIGHT_ADD_DISTRIB] THEN
1549 DECIDE_TAC);
1550
1551
1552val dest_sqrt = dest_monop ``$SQRT`` (mk_HOL_ERR "bitsLib" "dest_log2" "");
1553
1554fun cbv_SQRT_CONV tm =
1555 let open Arbnum numSyntax
1556 val x = dest_sqrt tm
1557 val n = dest_numeral x
1558 fun sqrt a n = if (a * a <= n andalso n < (a + one) * (a + one)) then a
1559 else sqrt (div2 (Arbnum.div (a * a + n,a))) n;
1560 val p = sqrt one n
1561 in Drule.SPECL [x, mk_numeral p] sqrt_thm
1562 end
1563 handle HOL_ERR _ => raise (mk_HOL_ERR "ieeeLib" "cbv_SQRT" "")
1564 | Domain => raise (mk_HOL_ERR "ieeeLib" "cbv_SQRT" "");
1565
1566val _ = add_conv (``$SQRT``, 1, cbv_SQRT_CONV) compset2;
1567
1568time (CBV_CONV compset2) ``SQRT 123456789123456789123456789``;
1569time (CBV_CONV compset1) ``ROOT 2 123456789123456789123456789``;
1570*)
1571
1572
1573(* Overload LOG base 2 *)
1574Overload LOG2 = ``\n. LOG 2 n``
1575
1576(* Theorem: LOG2 1 = 0 *)
1577(* Proof:
1578 LOG_1 |> SPEC ``2``;
1579 val it = |- 1 < 2 ==> LOG2 1 = 0: thm
1580*)
1581Theorem LOG2_1[simp]:
1582 LOG2 1 = 0
1583Proof
1584 rw[LOG_1]
1585QED
1586
1587(* Theorem: LOG2 2 = 1 *)
1588(* Proof:
1589 LOG_BASE |> SPEC ``2``;
1590 val it = |- 1 < 2 ==> LOG2 2 = 1: thm
1591*)
1592Theorem LOG2_2[simp]:
1593 LOG2 2 = 1
1594Proof
1595 rw[LOG_BASE]
1596QED
1597
1598Theorem LOG2_THM =
1599 LOG_THM |> SPEC ``2`` |> SIMP_RULE (srw_ss())[];
1600(* = |- !n. 0 < n ==> !p. (LOG2 n = p) <=> 2 ** p <= n /\ n < 2 ** SUC p *)
1601
1602Theorem LOG2_PROPERTY = LOG |> SPEC ``2`` |> SIMP_RULE (srw_ss())[];
1603(* = |- !n. 0 < n ==> 2 ** LOG2 n <= n /\ n < 2 ** SUC (LOG2 n) *)
1604
1605(* Theorem: 0 < n ==> 2 ** LOG2 n <= n) *)
1606(* Proof: by LOG2_PROPERTY *)
1607Theorem TWO_EXP_LOG2_LE:
1608 !n. 0 < n ==> 2 ** LOG2 n <= n
1609Proof
1610 rw[LOG2_PROPERTY]
1611QED
1612
1613Theorem LOG2_UNIQUE =
1614 LOG_UNIQUE |> SPEC ``2`` |> SPEC ``n:num`` |> SPEC ``m:num`` |> GEN_ALL;
1615(* = |- !n m. 2 ** m <= n /\ n < 2 ** SUC m ==> LOG2 n = m *)
1616
1617(* Theorem: 0 < n ==> ((LOG2 n = 0) <=> (n = 1)) *)
1618(* Proof:
1619 LOG_EQ_0 |> SPEC ``2``;
1620 |- !b. 1 < 2 /\ 0 < b ==> (LOG2 b = 0 <=> b < 2)
1621*)
1622Theorem LOG2_EQ_0:
1623 !n. 0 < n ==> ((LOG2 n = 0) <=> (n = 1))
1624Proof
1625 rw[LOG_EQ_0]
1626QED
1627
1628(* Theorem: 0 < n ==> LOG2 n = 1 <=> (n = 2) \/ (n = 3) *)
1629(* Proof:
1630 If part: LOG2 n = 1 ==> n = 2 \/ n = 3
1631 Note 2 ** 1 <= n /\ n < 2 ** SUC 1 by LOG2_PROPERTY
1632 or 2 <= n /\ n < 4 by arithmetic
1633 Thus n = 2 or n = 3.
1634 Only-if part: LOG2 2 = 1 /\ LOG2 3 = 1
1635 Note LOG2 2 = 1 by LOG2_2
1636 and LOG2 3 = 1 by LOG2_UNIQUE
1637 since 2 ** 1 <= 3 /\ 3 < 2 ** SUC 1 ==> (LOG2 3 = 1)
1638*)
1639Theorem LOG2_EQ_1:
1640 !n. 0 < n ==> ((LOG2 n = 1) <=> ((n = 2) \/ (n = 3)))
1641Proof
1642 rw_tac std_ss[EQ_IMP_THM] >| [
1643 imp_res_tac LOG2_PROPERTY >>
1644 rfs[],
1645 rw[],
1646 irule LOG2_UNIQUE >>
1647 simp[]
1648 ]
1649QED
1650
1651(* Obtain theorem *)
1652Theorem LOG2_LE_MONO =
1653 LOG_LE_MONO |> SPEC ``2`` |> SPEC ``n:num`` |> SPEC ``m:num``
1654 |> SIMP_RULE (srw_ss())[] |> GEN_ALL;
1655(* val LOG2_LE_MONO = |- !n m. 0 < n ==> n <= m ==> LOG2 n <= LOG2 m: thm *)
1656
1657(* Theorem: 0 < n /\ n <= m ==> LOG2 n <= LOG2 m *)
1658(* Proof: by LOG_LE_MONO *)
1659Theorem LOG2_LE:
1660 !n m. 0 < n /\ n <= m ==> LOG2 n <= LOG2 m
1661Proof
1662 rw[LOG_LE_MONO, DECIDE``1 < 2``]
1663QED
1664
1665(* Note: next is not LOG2_LT_MONO! *)
1666
1667(* Theorem: 0 < n /\ n < m ==> LOG2 n <= LOG2 m *)
1668(* Proof:
1669 Since n < m ==> n <= m by LESS_IMP_LESS_OR_EQ
1670 This is true by LOG_LE_MONO
1671*)
1672Theorem LOG2_LT:
1673 !n m. 0 < n /\ n < m ==> LOG2 n <= LOG2 m
1674Proof
1675 rw[LOG_LE_MONO, LESS_IMP_LESS_OR_EQ, DECIDE``1 < 2``]
1676QED
1677
1678(* Theorem: 0 < n ==> LOG2 n < n *)
1679(* Proof:
1680 LOG2 n
1681 < 2 ** (LOG2 n) by X_LT_EXP_X, 1 < 2
1682 <= n by LOG2_PROPERTY, 0 < n
1683*)
1684Theorem LOG2_LT_SELF:
1685 !n. 0 < n ==> LOG2 n < n
1686Proof
1687 rpt strip_tac >>
1688 `LOG2 n < 2 ** (LOG2 n)` by rw[X_LT_EXP_X] >>
1689 `2 ** LOG2 n <= n` by rw[LOG2_PROPERTY] >>
1690 decide_tac
1691QED
1692
1693(* Theorem: 0 < n ==> LOG2 n <> n *)
1694(* Proof:
1695 Note n < LOG2 n by LOG2_LT_SELF
1696 Thus n <> LOG2 n by arithmetic
1697*)
1698Theorem LOG2_NEQ_SELF:
1699 !n. 0 < n ==> LOG2 n <> n
1700Proof
1701 rpt strip_tac >>
1702 `LOG2 n < n` by rw[LOG2_LT_SELF] >>
1703 decide_tac
1704QED
1705
1706(* Theorem: LOG2 n = n ==> n = 0 *)
1707(* Proof: by LOG2_NEQ_SELF *)
1708Theorem LOG2_EQ_SELF:
1709 !n. (LOG2 n = n) ==> (n = 0)
1710Proof
1711 metis_tac[LOG2_NEQ_SELF, DECIDE``~(0 < n) <=> (n = 0)``]
1712QED
1713
1714(* Theorem: 1 < n ==> 0 < LOG2 n *)
1715(* Proof:
1716 1 < n
1717 ==> 2 <= n
1718 ==> LOG2 2 <= LOG2 n by LOG2_LE
1719 ==> 1 <= LOG2 n by LOG_BASE, LOG2 2 = 1
1720 or 0 < LOG2 n
1721*)
1722Theorem LOG2_POS[simp]:
1723 !n. 1 < n ==> 0 < LOG2 n
1724Proof
1725 rpt strip_tac >>
1726 `LOG2 2 = 1` by rw[LOG_BASE, DECIDE``1 < 2``] >>
1727 `2 <= n` by decide_tac >>
1728 `LOG2 2 <= LOG2 n` by rw[LOG2_LE] >>
1729 decide_tac
1730QED
1731
1732(* Theorem: 1 < n ==> 1 < 2 * LOG2 n *)
1733(* Proof:
1734 1 < n
1735 ==> 2 <= n
1736 ==> LOG2 2 <= LOG2 n by LOG2_LE
1737 ==> 1 <= LOG2 n by LOG_BASE, LOG2 2 = 1
1738 ==> 2 * 1 <= 2 * LOG2 n by LE_MULT_LCANCEL
1739 or 1 < 2 * LOG2 n
1740*)
1741Theorem LOG2_TWICE_LT:
1742 !n. 1 < n ==> 1 < 2 * (LOG2 n)
1743Proof
1744 rpt strip_tac >>
1745 `LOG2 2 = 1` by rw[LOG_BASE, DECIDE``1 < 2``] >>
1746 `2 <= n` by decide_tac >>
1747 `LOG2 2 <= LOG2 n` by rw[LOG2_LE] >>
1748 `1 <= LOG2 n` by decide_tac >>
1749 `2 <= 2 * LOG2 n` by rw_tac arith_ss[LE_MULT_LCANCEL, DECIDE``0 < 2``] >>
1750 decide_tac
1751QED
1752
1753(* Theorem: 1 < n ==> 4 <= (2 * (LOG2 n)) ** 2 *)
1754(* Proof:
1755 1 < n
1756 ==> 2 <= n
1757 ==> LOG2 2 <= LOG2 n by LOG2_LE
1758 ==> 1 <= LOG2 n by LOG2_2, or LOG_BASE, LOG2 2 = 1
1759 ==> 2 * 1 <= 2 * LOG2 n by LE_MULT_LCANCEL
1760 ==> 2 ** 2 <= (2 * LOG2 n) ** 2 by EXP_EXP_LE_MONO
1761 ==> 4 <= (2 * LOG2 n) ** 2
1762*)
1763Theorem LOG2_TWICE_SQ:
1764 !n. 1 < n ==> 4 <= (2 * (LOG2 n)) ** 2
1765Proof
1766 rpt strip_tac >>
1767 `LOG2 2 = 1` by rw[] >>
1768 `2 <= n` by decide_tac >>
1769 `LOG2 2 <= LOG2 n` by rw[LOG2_LE] >>
1770 `1 <= LOG2 n` by decide_tac >>
1771 `2 <= 2 * LOG2 n` by rw_tac arith_ss[LE_MULT_LCANCEL, DECIDE``0 < 2``] >>
1772 `2 ** 2 <= (2 * LOG2 n) ** 2` by rw[EXP_EXP_LE_MONO, DECIDE``0 < 2``] >>
1773 `2 ** 2 = 4` by rw_tac arith_ss[] >>
1774 decide_tac
1775QED
1776
1777(* Theorem: 0 < n ==> 4 <= (2 * SUC (LOG2 n)) ** 2 *)
1778(* Proof:
1779 0 < n
1780 ==> 1 <= n
1781 ==> LOG2 1 <= LOG2 n by LOG2_LE
1782 ==> 0 <= LOG2 n by LOG2_1, or LOG_BASE, LOG2 1 = 0
1783 ==> 1 <= SUC (LOG2 n) by LESS_EQ_MONO
1784 ==> 2 * 1 <= 2 * SUC (LOG2 n) by LE_MULT_LCANCEL
1785 ==> 2 ** 2 <= (2 * SUC (LOG2 n)) ** 2 by EXP_EXP_LE_MONO
1786 ==> 4 <= (2 * SUC (LOG2 n)) ** 2
1787*)
1788Theorem LOG2_SUC_TWICE_SQ:
1789 !n. 0 < n ==> 4 <= (2 * SUC (LOG2 n)) ** 2
1790Proof
1791 rpt strip_tac >>
1792 `LOG2 1 = 0` by rw[] >>
1793 `1 ≤ n` by decide_tac >>
1794 `LOG2 1 <= LOG2 n` by rw[LOG2_LE] >>
1795 `1 ≤ SUC (LOG2 n)` by decide_tac >>
1796 `2 ≤ 2 * SUC (LOG2 n)` by rw_tac arith_ss[LE_MULT_LCANCEL, DECIDE``0 < 2``] >>
1797 `2 ** 2 ≤ (2 * SUC (LOG2 n)) ** 2` by rw[EXP_EXP_LE_MONO, DECIDE``0 < 2``] >>
1798 `2 ** 2 = 4` by rw_tac arith_ss[] >>
1799 decide_tac
1800QED
1801
1802(* Theorem: 1 < n ==> 1 < (SUC (LOG2 n)) ** 2 *)
1803(* Proof:
1804 Note 0 < LOG2 n by LOG2_POS, 1 < n
1805 so 1 < SUC (LOG2 n) by arithmetic
1806 ==> 1 < (SUC (LOG2 n)) ** 2 by ONE_LT_EXP, 0 < 2
1807*)
1808Theorem LOG2_SUC_SQ:
1809 !n. 1 < n ==> 1 < (SUC (LOG2 n)) ** 2
1810Proof
1811 rpt strip_tac >>
1812 `0 < LOG2 n` by rw[] >>
1813 `1 < SUC (LOG2 n)` by decide_tac >>
1814 rw[ONE_LT_EXP]
1815QED
1816
1817(* Theorem: LOG2 (2 ** n) = n *)
1818(* Proof: by LOG_EXACT_EXP *)
1819Theorem LOG2_2_EXP:
1820 !n. LOG2 (2 ** n) = n
1821Proof
1822 rw[LOG_EXACT_EXP]
1823QED
1824
1825(* Theorem: (2 ** (LOG2 n) = n) <=> ?k. n = 2 ** k *)
1826(* Proof:
1827 If part: 2 ** LOG2 n = n ==> ?k. n = 2 ** k
1828 True by taking k = LOG2 n.
1829 Only-if part: 2 ** LOG2 (2 ** k) = 2 ** k
1830 Note LOG2 n = k by LOG_EXACT_EXP, 1 < 2
1831 or n = 2 ** k = 2 ** LOG2 n.
1832*)
1833Theorem LOG2_EXACT_EXP:
1834 !n. (2 ** (LOG2 n) = n) <=> ?k. n = 2 ** k
1835Proof
1836 metis_tac[LOG2_2_EXP]
1837QED
1838
1839(* Theorem: 0 < n ==> LOG2 (n * 2 ** m) = (LOG2 n) + m *)
1840(* Proof:
1841 LOG_EXP |> SPEC ``m:num`` |> SPEC ``2`` |> SPEC ``n:num``;
1842 val it = |- 1 < 2 /\ 0 < n ==> LOG2 (2 ** m * n) = m + LOG2 n: thm
1843*)
1844Theorem LOG2_MULT_EXP:
1845 !n m. 0 < n ==> (LOG2 (n * 2 ** m) = (LOG2 n) + m)
1846Proof
1847 rw[GSYM LOG_EXP]
1848QED
1849
1850(* Theorem: 0 < n ==> (LOG2 (2 * n) = 1 + LOG2 n) *)
1851(* Proof:
1852 LOG_MULT |> SPEC ``2`` |> SPEC ``n:num``;
1853 val it = |- 1 < 2 /\ 0 < n ==> LOG2 (TWICE n) = SUC (LOG2 n): thm
1854*)
1855Theorem LOG2_TWICE:
1856 !n. 0 < n ==> (LOG2 (2 * n) = 1 + LOG2 n)
1857Proof
1858 rw[LOG_MULT]
1859QED
1860
1861(* ----------------------------------------------------------------------- *)