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