1structure wordsLib :> wordsLib = 2struct 3 4open HolKernel Parse boolLib bossLib computeLib 5open wordsTheory wordsSyntax 6open bitTheory numeral_bitTheory bitLib 7open numposrepTheory numposrepLib 8open ASCIInumbersTheory ASCIInumbersSyntax ASCIInumbersLib 9open stringSyntax 10 11structure Parse = struct 12 open Parse 13 val (Type, Term) = parse_from_grammars wordsTheory.words_grammars 14end 15open Parse 16 17val () = ignore (Lib.with_flag (Feedback.emit_MESG, false) bossLib.srw_ss ()) 18 19val ERR = mk_HOL_ERR "wordsLib" 20 21(* ------------------------------------------------------------------------- *) 22 23fun is_word_literal t = 24 case Lib.total wordsSyntax.dest_word_2comp t of 25 SOME n => wordsSyntax.is_word_literal n 26 | NONE => wordsSyntax.is_word_literal t 27 28(* Tell the function definition mechanism about words. *) 29val () = Literal.add_literal is_word_literal 30 31fun is_word_zero t = 32 case Lib.total (fst o wordsSyntax.dest_n2w) t of 33 SOME n => Term.term_eq numSyntax.zero_tm n 34 | NONE => false 35 36fun is_word_one t = 37 case Lib.total (fst o wordsSyntax.dest_n2w) t of 38 SOME n => Term.term_eq (numSyntax.term_of_int 1) n 39 | NONE => false 40 41fun is_uintmax t = 42 case Lib.total wordsSyntax.dest_word_2comp t of 43 SOME n => is_word_one n 44 | NONE => false 45 46fun is_word_lht t = 47 wordsSyntax.is_word_L t orelse 48 wordsSyntax.is_word_H t orelse 49 wordsSyntax.is_word_T t 50 51(* ------------------------------------------------------------------------- 52 Conversions, evaluation and simpsets 53 ------------------------------------------------------------------------- *) 54 55val Na = Term.mk_comb (numSyntax.numeral_tm, Term.mk_var ("a", numLib.num)) 56val n2w = wordsSyntax.n2w_tm 57 58val TIMES_2EXP1 = 59 (GSYM o REWRITE_RULE [arithmeticTheory.MULT_LEFT_1] o 60 Q.SPECL [`x`, `1`]) bitTheory.TIMES_2EXP_def 61 62local 63 val cnv = 64 computeLib.compset_conv (reduceLib.num_compset()) 65 [computeLib.Defs 66 [NUMERAL_SFUNPOW_FDUB, NUMERAL_SFUNPOW_iDUB, iDUB_NUMERAL, 67 FDUB_iDUB, FDUB_FDUB, NUMERAL_TIMES_2EXP]] 68 val thms = [TIMES_2EXP1, arithmeticTheory.TIMES2, GSYM numeralTheory.iDUB] 69 val rwts = List.map (REWRITE_RULE thms) 70 [INT_MIN_def, dimword_IS_TWICE_INT_MIN, 71 UINT_MAX_def, INT_MAX_def, INT_MIN_SUM] 72in 73 val PRIM_SIZES_CONV = PURE_REWRITE_CONV rwts THENC fcpLib.INDEX_CONV THENC cnv 74end 75 76local 77 fun intSuff (s, n) = 78 Option.isSome (Int.fromString (String.extract (s, n, NONE))) 79 fun is_fcp_thm s = 80 let 81 fun is_pref_int p = String.isPrefix p s andalso intSuff (s, String.size p) 82 in 83 Lib.exists is_pref_int ["finite_", "dimindex_", "dimword_", "INT_MIN_"] 84 andalso s <> "dimindex_1_cases" 85 end 86 fun get_fcp_thm (s, th) = 87 if is_fcp_thm s then 88 SOME (case Lib.total (fst o boolSyntax.dest_eq o Thm.concl) th of 89 SOME t => (t, th) 90 | NONE => (Thm.concl th, Drule.EQT_INTRO th)) 91 else NONE 92 val tree = DB.theorems "words" 93 |> List.mapPartial get_fcp_thm 94 |> Redblackmap.fromList Term.compare 95 val err = 96 ERR "SIZES_CONV" 97 "Term not dimword, dimindex, INT_MIN, INT_MAX, UINT_MAX or FINITE" 98 val is_numeric = 99 Lib.can (fcpSyntax.dest_numeric_type o boolSyntax.dest_itself) 100 val is_univ_numeric = 101 Lib.can (fcpSyntax.dest_numeric_type o fst o Type.dom_rng o 102 pred_setSyntax.dest_univ) 103 fun suitable t = 104 case Lib.total boolSyntax.dest_strip_comb t of 105 SOME ("pred_set$FINITE", [a]) => is_univ_numeric a 106 | SOME ("words$INT_MIN", [a]) => is_numeric a 107 | SOME ("words$INT_MAX", [a]) => is_numeric a 108 | SOME ("words$UINT_MAX", [a]) => is_numeric a 109 | SOME ("words$dimword", [a]) => is_numeric a 110 | SOME ("fcp$dimindex", [a]) => is_numeric a 111 | _ => false 112 fun dst t = if suitable t then SOME t else NONE 113in 114 val SIZES_CONV = Conv.memoize dst tree (Lib.K true) err PRIM_SIZES_CONV 115end 116 117val SIZES_ss = 118 simpLib.named_merge_ss "sizes" 119 [simpLib.rewrites [ONE_LT_dimword, DIMINDEX_GT_0], 120 simpLib.std_conv_ss 121 {name = "SIZES_CONV", 122 conv = SIZES_CONV, 123 pats = [``fcp$dimindex(:'a)``, 124 ``pred_set$FINITE (pred_set$UNIV:'a set)``, 125 ``words$INT_MIN(:'a)``, 126 ``words$INT_MAX(:'a)``, 127 ``words$UINT_MAX(:'a)``, 128 ``words$dimword(:'a)``]}] 129 130local 131 val thm = 132 LIST_CONJ 133 (List.drop (CONJUNCTS (SPEC_ALL numeralTheory.numeral_evenodd), 3)) 134 val odd_conv = 135 PURE_REWRITE_CONV 136 [arithmeticTheory.NUMERAL_DEF, thm, 137 PURE_REWRITE_RULE [arithmeticTheory.ALT_ZERO] (CONJUNCT1 thm)] 138 val div2_conv = 139 PURE_REWRITE_CONV 140 [arithmeticTheory.NORM_0, numeralTheory.numeral_suc, 141 numeralTheory.numeral_div2] 142 val bool_conv = REWRITE_CONV [] 143 val (mod_2exp_max0_conv, mod_2exp_max1_conv, mod_2exp_max2_conv) = 144 Lib.triple_of_list 145 (List.map Conv.REWR_CONV 146 (CONJUNCTS 147 (PURE_REWRITE_RULE [GSYM arithmeticTheory.PRE_SUB1] 148 (numLib.SUC_RULE numeral_bitTheory.MOD_2EXP_MAX)))) 149 val args_max_conv = 150 Conv.RAND_CONV div2_conv 151 THENC Conv.RATOR_CONV (Conv.RAND_CONV (Conv.TRY_CONV reduceLib.PRE_CONV)) 152 val err_max = ERR "mod_2exp_max_conv" "" 153 val (mod_2exp_eq0_conv, mod_2exp_eq1_conv, mod_2exp_eq2_conv, 154 mod_2exp_eq_eq_conv) = 155 Lib.quadruple_of_list 156 (List.map Conv.REWR_CONV 157 (CONJUNCTS 158 (PURE_REWRITE_RULE [GSYM arithmeticTheory.PRE_SUB1] 159 (numLib.SUC_RULE numeral_bitTheory.MOD_2EXP_EQ)))) 160 val args_conv = 161 Conv.RAND_CONV div2_conv 162 THENC Conv.RATOR_CONV (Conv.RAND_CONV div2_conv) 163 THENC Conv.RATOR_CONV 164 (Conv.RATOR_CONV 165 (Conv.RAND_CONV (Conv.TRY_CONV reduceLib.PRE_CONV))) 166 val err = ERR "mod_2exp_eq_conv" "" 167in 168 fun mod_2exp_max_conv tm = 169 let 170 val (n, a) = Lib.with_exn bitSyntax.dest_mod_2exp_max tm err_max 171 in 172 if n = numSyntax.zero_tm 173 then mod_2exp_max0_conv tm 174 else let 175 val m = Lib.with_exn Term.rand n err_max 176 val odd_thm = odd_conv (numSyntax.mk_odd a) 177 val odd_rhs = rhs (concl odd_thm) 178 val cnv1 = if numSyntax.is_bit1 m 179 then mod_2exp_max1_conv 180 else mod_2exp_max2_conv 181 val cnv2 = 182 if odd_rhs = boolSyntax.T 183 then Conv.FORK_CONV 184 (K odd_thm, args_max_conv THENC mod_2exp_max_conv) 185 else if odd_rhs = boolSyntax.F 186 then Conv.LAND_CONV (K odd_thm) 187 else raise err_max 188 in 189 (cnv1 THENC cnv2 THENC bool_conv) tm 190 end 191 end 192 fun mod_2exp_eq_conv tm = 193 let 194 val (n, a, b) = Lib.with_exn bitSyntax.dest_mod_2exp_eq tm err 195 in 196 if n = numSyntax.zero_tm 197 then mod_2exp_eq0_conv tm 198 else if a = b 199 then mod_2exp_eq_eq_conv tm 200 else let 201 val m = Lib.with_exn Term.rand n err 202 val odd_thm = (Conv.BINOP_CONV odd_conv THENC bool_conv) 203 (boolSyntax.mk_eq 204 (numSyntax.mk_odd a, 205 numSyntax.mk_odd b)) 206 val odd_rhs = rhs (concl odd_thm) 207 val cnv1 = if numSyntax.is_bit1 m 208 then mod_2exp_eq1_conv 209 else mod_2exp_eq2_conv 210 val cnv2 = 211 if odd_rhs = boolSyntax.T 212 then Conv.FORK_CONV 213 (K odd_thm, args_conv THENC mod_2exp_eq_conv) 214 else if odd_rhs = boolSyntax.F 215 then Conv.LAND_CONV (K odd_thm) 216 else raise err 217 in 218 (cnv1 THENC cnv2 THENC bool_conv) tm 219 end 220 end 221end 222 223local 224 val (n2w_n2w_conv, n2w_max_conv, max_n2w_conv) = 225 Lib.triple_of_list 226 (List.map Conv.REWR_CONV (CONJUNCTS wordsTheory.word_eq_n2w)) 227 val sizes_conv = Conv.RATOR_CONV (Conv.RAND_CONV SIZES_CONV) 228 val cnv1 = max_n2w_conv THENC sizes_conv THENC mod_2exp_max_conv 229 val cnv2 = n2w_max_conv THENC sizes_conv THENC mod_2exp_max_conv 230 val cnv3 = 231 n2w_n2w_conv THENC Conv.RATOR_CONV sizes_conv THENC mod_2exp_eq_conv 232 val err = ERR "word_EQ_CONV" "not a ground word equality" 233in 234 fun word_EQ_CONV tm = 235 let 236 val (l, r) = Lib.with_exn boolSyntax.dest_eq tm err 237 in 238 if l = r 239 then Drule.ISPEC l boolTheory.REFL_CLAUSE 240 else if is_uintmax l andalso wordsSyntax.is_word_literal r 241 then cnv1 tm 242 else if is_uintmax r andalso wordsSyntax.is_word_literal l 243 then cnv2 tm 244 else if wordsSyntax.is_word_literal l andalso 245 wordsSyntax.is_word_literal r 246 then cnv3 tm 247 else raise err 248 end 249end 250 251local 252 val DIV2_CONV = 253 PURE_REWRITE_CONV 254 [numeralTheory.numeral_div2, numeralTheory.numeral_suc, 255 arithmeticTheory.NORM_0] 256 257 val conv1 = 258 Conv.REWR_CONV 259 (REWRITE_RULE [GSYM arithmeticTheory.DIV2_def] wordsTheory.BIT_SET_def) 260 THENC RATOR_CONV (RATOR_CONV (RAND_CONV Arithconv.NEQ_CONV)) 261 THENC PURE_ONCE_REWRITE_CONV [boolTheory.COND_CLAUSES] 262 263 val conv2 = 264 RATOR_CONV (RATOR_CONV (RAND_CONV Arithconv.ODD_CONV)) 265 THENC PURE_ONCE_REWRITE_CONV [boolTheory.COND_CLAUSES] 266 267 val conv3 = 268 RAND_CONV DIV2_CONV 269 THENC RATOR_CONV (RAND_CONV Arithconv.SUC_CONV) 270in 271 fun BIT_SET_CONV tm = 272 let 273 val thm1 = conv1 tm 274 in 275 if boolSyntax.is_cond (rhs (concl thm1)) 276 then let 277 val thm2 = Conv.RIGHT_CONV_RULE conv2 thm1 278 in 279 Conv.RIGHT_CONV_RULE 280 ((if pred_setSyntax.is_insert (rhs (concl thm2)) 281 then RAND_CONV 282 else I) (conv3 THENC BIT_SET_CONV)) thm2 283 end 284 else thm1 285 end 286end 287 288val BIT_ss = 289 simpLib.named_merge_ss "bit" 290 [simpLib.rewrites [BIT_ZERO], 291 simpLib.std_conv_ss 292 {conv = Conv.REWR_CONV wordsTheory.BIT_SET 293 THENC Conv.RAND_CONV BIT_SET_CONV 294 THENC TRY_CONV (pred_setLib.IN_CONV Arithconv.NEQ_CONV), 295 name = "BITS_CONV", 296 pats = [``bit$BIT n ^Na``]}] 297 298local 299 fun NUM_RULE l n x = 300 let 301 val y = SPEC_ALL x 302 val N = Parse.Term n 303 in 304 CONJ ((GEN_ALL 305 o simpLib.SIMP_RULE (bossLib.arith_ss++boolSimps.LET_ss) l 306 o Q.INST [n |-> `0n`]) y) 307 ((GEN_ALL o Thm.INST [N |-> ``NUMERAL ^N``]) y) 308 end 309 310 val MOD_WL = 311 CONV_RULE (STRIP_QUANT_CONV (RHS_CONV (ONCE_REWRITE_CONV [GSYM n2w_mod]))) 312 313 val MOD_WL1 = 314 CONV_RULE 315 (STRIP_QUANT_CONV 316 (RHS_CONV (RATOR_CONV (ONCE_REWRITE_CONV [GSYM n2w_mod])))) 317 318 val w2n_n2w_compute = Q.prove( 319 `!n. w2n ((n2w n) : 'a word) = 320 if n < dimword(:'a) then n else n MOD dimword(:'a)`, 321 SRW_TAC [boolSimps.LET_ss] []) 322 323 val word_2comp_compute = Q.prove( 324 `!n. word_2comp (n2w n) : 'a word = 325 let x = n MOD dimword (:'a) in 326 if x = 0 then 0w else n2w (dimword (:'a) - x)`, 327 SRW_TAC [boolSimps.LET_ss] [word_2comp_n2w]) 328 329 val word_lsl_compute = Q.prove( 330 `!n m. (n2w m : 'a word) << n = 331 if dimindex(:'a) - 1 < n then 332 0w 333 else 334 n2w ((m * 2 ** n) MOD dimword(:'a))`, 335 REWRITE_TAC [word_lsl_n2w, n2w_mod]) 336 337 val word_lsr_compute = 338 (REWRITE_RULE [word_bits_n2w, arithmeticTheory.MIN_IDEM] o 339 Q.SPECL [`^n2w n`, `^Na`]) word_lsr_n2w 340 341 val word_asr_compute = 342 (REWRITE_RULE [word_bits_n2w, word_msb_n2w, word_or_n2w, 343 word_lsr_compute, arithmeticTheory.MIN_IDEM] o 344 Q.SPECL [`^Na`, `^n2w n`]) word_asr_n2w 345 346 val bit_update_compute = 347 BIT_UPDATE |> REWRITE_RULE [FUN_EQ_THM] 348 |> (fn th => CONJ (Q.SPECL [`^Na`, `F`, `^n2w n`] th) 349 (Q.SPECL [`^Na`, `T`, `^n2w n`] th)) 350 351 val thms = 352 [numLib.SUC_RULE sum_numTheory.SUM_def, bit_update_compute, 353 n2w_w2n, w2n_n2w_compute, MOD_WL1 w2w_n2w, Q.SPEC `^n2w n` sw2sw_def, 354 word_len_def, word_L_def, word_H_def, word_T_def, 355 word_abs_def, word_min_def, word_max_def, word_smin_def, word_smax_def, 356 bit_count_upto_def, bit_count_def, 357 saturate_w2w_n2w, saturate_n2w_def, 358 saturate_add_def, saturate_sub_def, saturate_mul_def, 359 word_join_def, Q.SPECL [`^n2w n`, `n2w m:'b word`] word_concat_def, 360 Q.SPEC `^Na` word_replicate_concat_word_list, concat_word_list_def, 361 word_reverse_n2w, word_modify_n2w, bit_field_insert_def, 362 Q.SPEC `^Na` word_log2_n2w, 363 word_1comp_n2w, word_or_n2w, word_xor_n2w, word_and_n2w, 364 word_2comp_compute, word_nor_n2w, word_xnor_n2w, word_nand_n2w, 365 word_sub_def, word_div_def, word_quot_def, word_mod_def, word_rem_def, 366 MOD_WL word_add_n2w, MOD_WL word_mul_n2w, 367 word_rol_bv_def, word_lsl_bv_def, word_lsr_bv_def, word_asr_bv_def, 368 word_ror_bv_def, word_asr_compute, word_lsr_compute, 369 Q.SPEC `^Na` word_lsl_compute, SHIFT_ZERO, Q.SPEC `^Na` word_ror_n2w, 370 Q.SPECL [`w:'a word`, `^Na`] word_rol_def, word_rrx_n2w, 371 word_lsb_n2w, word_msb_n2w, word_bit_n2w, fcp_n2w, fcpTheory.L2V_def, 372 NUM_RULE [DIMINDEX_GT_0] `i:num` word_index_n2w, 373 NUM_RULE [DIMINDEX_GT_0] `n:num` fcpTheory.index_comp, 374 NUM_RULE [DIMINDEX_GT_0] `b:num` fcpTheory.FCP_APPLY_UPDATE_THM, 375 word_bits_n2w, word_signed_bits_n2w, word_slice_n2w, word_extract_n2w, 376 word_reduce_n2w, word_compare_def, Q.SPEC `^n2w n` reduce_and, 377 Q.SPEC `^n2w n` reduce_or, reduce_xor_def, reduce_xnor_def, 378 reduce_nand_def, reduce_nor_def, 379 Q.SPECL [`^Na`, `^n2w n`] word_sign_extend_def, 380 word_ge_n2w, word_gt_n2w, word_hi_n2w, word_hs_n2w, 381 word_le_n2w, word_lo_n2w, word_ls_n2w, word_lt_n2w, 382 l2w_def, w2l_def, s2w_def, w2s_def, add_with_carry_def, 383 word_from_bin_list_def, word_from_oct_list_def, 384 word_from_dec_list_def, word_from_hex_list_def, 385 word_to_bin_list_def, word_to_oct_list_def, 386 word_to_dec_list_def, word_to_hex_list_def, 387 word_from_bin_string_def, word_from_oct_string_def, 388 word_from_dec_string_def, word_from_hex_string_def, 389 word_to_bin_string_def, word_to_oct_string_def, 390 word_to_dec_string_def, word_to_hex_string_def] 391 392 fun mrw th = map (REWRITE_RULE [th]) 393in 394 val thms = 395 (mrw TIMES_2EXP1 o mrw (GSYM bitTheory.TIMES_2EXP_def) o 396 mrw (GSYM bitTheory.MOD_2EXP_def)) thms 397end 398 399fun add_words_compset extras = 400 computeLib.extend_compset 401 (computeLib.Extenders 402 (if extras then 403 [listSimps.list_rws, bitLib.add_bit_compset, 404 numposrepLib.add_numposrep_compset, 405 ASCIInumbersLib.add_ASCIInumbers_compset] 406 else []) :: 407 [computeLib.Defs thms, 408 computeLib.Convs 409 ([(``words$BIT_SET : num -> num -> num set``, 2, BIT_SET_CONV), 410 (``min$= : 'a word -> 'a word -> bool``, 2, word_EQ_CONV)] @ 411 List.map (fn x => (x, 1, SIZES_CONV)) 412 [fcpSyntax.dimindex_tm, wordsSyntax.dimword_tm, 413 wordsSyntax.uint_max_tm, wordsSyntax.int_min_tm, 414 wordsSyntax.int_max_tm, pred_setSyntax.finite_tm])]) 415 416val () = add_words_compset false computeLib.the_compset 417 418fun words_compset () = 419 let 420 val cmp = reduceLib.num_compset () 421 in 422 add_words_compset true cmp; cmp 423 end 424 425val WORD_EVAL_CONV = computeLib.CBV_CONV (words_compset ()) 426val WORD_EVAL_RULE = CONV_RULE WORD_EVAL_CONV 427val WORD_EVAL_TAC = CONV_TAC WORD_EVAL_CONV 428 429(* ------------------------------------------------------------------------- *) 430 431local 432 fun name_thy t = 433 let val {Name, Thy, ...} = dest_thy_const t in (Thy, Name) end 434 435 val name_thy_compare = 436 Lib.pair_compare (String.compare, String.compare) o 437 (Lib.swap ## Lib.swap) 438 439 fun name_thy_set l = 440 (List.app 441 (fn (thy, c) => 442 General.ignore (Term.prim_mk_const {Thy = thy, Name = c})) l 443 ; Redblackset.addList (Redblackset.empty name_thy_compare, l)) 444 445 val l1 = 446 ["l2w", "w2l", "s2w", "w2s", "add_with_carry", 447 "bit_count", "bit_count_upto", "word_from_bin_list", 448 "word_from_oct_list", "word_from_dec_list", "word_from_hex_list", 449 "word_to_bin_list", "word_to_oct_list", "word_to_dec_list", 450 "word_to_hex_list", "word_from_bin_string", "word_from_oct_string", 451 "word_from_dec_string", "word_from_hex_string", "word_to_bin_string", 452 "word_to_oct_string", "word_to_dec_string", "word_to_hex_string", 453 "word_reduce", "word_compare", "reduce_and", "reduce_or", "reduce_xor", 454 "reduce_nand", "reduce_nor", "reduce_xnor", "word_replicate", 455 "concat_word_list", "bit_field_insert", "word_len", "w2w", "w2n", 456 "sw2sw", "word_log2", "word_reverse", "word_lsb", "word_msb", 457 "word_join", "word_concat", "word_bit", "word_bits", "word_signed_bits", 458 "word_slice", "word_extract", "word_asr", "word_lsr", "word_lsl", 459 "word_ror", "word_rol", "word_rrx", "word_lsl_bv", "word_lsr_bv", 460 "word_asr_bv", "word_ror_bv", "word_rol_bv", "word_lo", "word_ls", 461 "word_lt", "word_le", "saturate_n2w", "saturate_w2w", "saturate_add", 462 "saturate_sub", "saturate_mul", "word_min", "word_max", "word_smin", 463 "word_smax", "word_abs", "word_div", "word_quot", "word_mod", "word_rem", 464 "word_sign_extend"] 465 466 val l2 = 467 ["SBIT", "BIT", "BITS", "BITV", "SLICE", 468 "TIMES_2EXP", "DIV_2EXP", "DIVMOD_2EXP", "MOD_2EXP", 469 "LOG2", "BITWISE", "BIT_REVERSE", "SIGN_EXTEND"] 470 471 val l3 = 472 ["l2n", "n2l", "BOOLIFY", 473 "num_from_bin_list", "num_from_oct_list", "num_from_dec_list", 474 "num_from_hex_list", "num_to_bin_list", "num_to_oct_list", 475 "num_to_dec_list", "num_to_hex_list"] 476 477 val l4 = 478 ["s2n", "n2s", "HEX", "UNHEX", 479 "num_from_bin_string", "num_from_oct_string", "num_from_dec_string", 480 "num_from_hex_string", 481 "num_to_bin_string", "num_to_oct_string", "num_to_dec_string", 482 "num_to_hex_string"] 483 484 val l5 = ["fcp_index", ":+"] 485 486 val s = [("min", ["="]), 487 ("logroot", ["LOG"]), 488 ("words", l1), 489 ("bit", l2), 490 ("numposrep", l3), 491 ("ASCIInumbers", l4), 492 ("fcp", l5)] 493 |> List.map (fn (thy, l) => List.map (Lib.pair thy) l) 494 |> List.concat 495 |> name_thy_set 496 497 val s2 = 498 Redblackset.addList 499 (s, map (pair "words") 500 ["word_mul", "word_add", "word_sub", "word_1comp", "word_2comp", 501 "word_xor", "word_and", "word_or", 502 "word_xnor", "word_nand", "word_nor", 503 "word_ge", "word_gt", "word_hi", "word_hs"] @ 504 map (pair "arithmetic") 505 ["+", "-", "*", "DIV", "DIV2", "EXP", "ODD", "EVEN", 506 "<=", ">=", "<", ">"]) 507 508 fun is_hex_digit_literal t = 509 numSyntax.int_of_term t < 16 handle HOL_ERR _ => false 510 511 fun is_bool t = t = boolSyntax.T orelse t = boolSyntax.F 512 513 fun is_ground_list t = 514 let 515 val (l, ty) = listSyntax.dest_list t 516 in 517 if ty = numSyntax.num 518 then Lib.all is_hex_digit_literal l 519 else if ty = stringSyntax.char_ty 520 then Lib.all (Char.isHexDigit o stringSyntax.fromHOLchar) l 521 else if ty = Type.bool 522 then Lib.all is_bool l 523 else wordsSyntax.is_word_type ty 524 end 525 handle HOL_ERR _ => false 526 527 fun is_ground_arg t = 528 case Lib.total pairSyntax.dest_pair t of 529 SOME (l, r) => is_ground_arg l andalso is_ground_arg r 530 | NONE => numSyntax.is_numeral t 531 orelse wordsSyntax.is_word_literal t 532 orelse is_uintmax t 533 orelse List.exists (Term.same_const t) 534 [boolSyntax.T, boolSyntax.F, 535 boolSyntax.conjunction, boolSyntax.disjunction, 536 ASCIInumbersSyntax.hex_tm, 537 ASCIInumbersSyntax.unhex_tm] 538 orelse is_ground_list t 539 540 fun is_ground_fn s t = 541 case (name_thy ## Lib.I) (boolSyntax.strip_comb t) of 542 (_, []) => is_word_lht t 543 | (("words", "BIT_SET"), l as [_, _]) => Lib.all is_ground_arg l 544 | (tn as (thy, name), l) => 545 Redblackset.member (s, tn) andalso 546 let 547 val (tys, _) = 548 boolSyntax.strip_fun 549 (Term.type_of (Term.prim_mk_const {Name = name, Thy = thy})) 550 in 551 List.length tys = List.length l andalso Lib.all is_ground_arg l 552 end 553 554 val alpha_rws = 555 [word_lsb_n2w, word_lsb_word_T, word_msb_word_T, WORD_0_POS, WORD_L_NEG, 556 word_bit_0, word_bit_0_word_T, w2w_0, sw2sw_0, sw2sw_word_T, 557 word_0_n2w, word_1_n2w, 558 word_len_def, word_reverse_0, word_reverse_word_T, word_log2_1, word_div_1, 559 word_join_0, word_concat_0_0, word_concat_word_T, word_join_word_T, 560 WORD_BITS_ZERO2, WORD_EXTRACT_ZERO2, WORD_SLICE_ZERO2, BIT_ZERO, BITS_ZERO2] 561 562 val alpha_rws2 = 563 [WORD_ADD_0, WORD_SUB_RZERO, WORD_MULT_CLAUSES, WORD_XOR_CLAUSES, 564 WORD_AND_CLAUSES, WORD_OR_CLAUSES] 565in 566 (* The for_simpset = true variant is designed for simplification, where other 567 simpsets are used to simplify arithmetic and bitwise operations. 568 The for_simpset = false variant is designed for full ground term 569 evaluation of word expressions. 570 *) 571 fun WORD_GROUND_CONV for_simpset = 572 let 573 val (rws, set) = if for_simpset then ([], s) else (alpha_rws2, s2) 574 val cnv = PURE_REWRITE_CONV rws THENC WORD_EVAL_CONV 575 val is_ground = is_ground_fn set 576 in 577 fn t => 578 ( List.null (type_vars_in_term t) andalso is_ground t orelse 579 raise ERR "WORD_GROUND_CONV" 580 "Term not ground or contains type variables." 581 ; cnv t 582 ) 583 end 584 val WORD_GROUND_ss = 585 simpLib.named_merge_ss "word ground" 586 [simpLib.rewrites alpha_rws, 587 simpLib.conv_ss 588 {conv = K (K (Conv.CHANGED_CONV (WORD_GROUND_CONV true))), 589 trace = 3, 590 name = "WORD_GROUND_CONV", 591 key = NONE}] 592 val WORD_GROUND_CONV = WORD_GROUND_CONV false 593end 594 595val SYM_WORD_NEG_1 = SYM WORD_NEG_1 596 597local 598 val d = ref (Redblackmap.mkDict Arbnum.compare: 599 (Arbnum.num, thm) Redblackmap.dict) 600 val mk_th = Conv.RIGHT_CONV_RULE (Conv.REWR_CONV SYM_WORD_NEG_1) o GSYM o 601 (Conv.REWR_CONV word_T_def THENC Conv.RAND_CONV SIZES_CONV) o 602 wordsSyntax.mk_word_T o fcpSyntax.mk_numeric_type 603 fun PRIM_UINT_MAX_CONV n = 604 case Redblackmap.peek (!d, n) of 605 SOME th => Conv.REWR_CONV th 606 | NONE => 607 let 608 val th = mk_th n 609 in 610 d := Redblackmap.insert (!d, n, th) 611 ; Conv.REWR_CONV th 612 end 613 val err = ERR "UINT_MAX_CONV" "" 614in 615 (* convert 0b11...1w to -1w *) 616 fun UINT_MAX_CONV t = 617 if wordsSyntax.is_n2w t 618 then case Lib.total wordsSyntax.size_of t of 619 SOME n => if n = Arbnum.one then raise err 620 else PRIM_UINT_MAX_CONV n t 621 | NONE => raise err 622 else raise err 623 val WORD_UINT_MAX_ss = 624 simpLib.std_conv_ss 625 {conv = UINT_MAX_CONV, name = "uint_max", pats = [``n2w a : 'a word``]} 626end 627 628(* ------------------------------------------------------------------------- *) 629 630val ADD1 = arithmeticTheory.ADD1 631 632val WORD_LSL_NUMERAL = (GEN_ALL o Q.SPECL [`w: 'a word`, `^Na`]) WORD_MUL_LSL 633 634val WORD_NOT_NUMERAL = 635 (SIMP_RULE std_ss [GSYM ADD1, WORD_LITERAL_ADD, word_sub_def] o 636 Q.SPEC `^n2w n`) WORD_NOT 637 638val WORD_NOT_NEG_NUMERAL = 639 (numLib.SUC_RULE o GEN_ALL o 640 SIMP_RULE arith_ss 641 [GSYM ADD1, WORD_LITERAL_ADD, word_sub_def, WORD_NEG_NEG] o 642 Q.SPEC `words$word_2comp (^n2w (num$SUC n))`) WORD_NOT 643 644val WORD_NOT_NEG_0 = 645 SIMP_CONV std_ss [SYM_WORD_NEG_1, WORD_NOT_0, WORD_NEG_0] 646 ``words$word_1comp (words$word_2comp 0w) : 'a word`` 647 648val WORD_LITERAL_MULT_thms = 649 [word_mul_n2w, WORD_LITERAL_MULT, word_L_MULT, word_L_MULT_NEG, 650 GSYM word_L2_def, word_L2_MULT, 651 (ONCE_REWRITE_RULE [WORD_MULT_COMM] o CONJUNCT1) WORD_LITERAL_MULT] @ 652 (map (ONCE_REWRITE_RULE [WORD_MULT_COMM]) 653 [word_L_MULT, word_L_MULT_NEG, word_L2_MULT]) 654 655val WORD_LITERAL_ADD_thms = 656 [word_add_n2w, WORD_LITERAL_ADD, 657 (ONCE_REWRITE_RULE [WORD_ADD_COMM] o CONJUNCT2) WORD_LITERAL_ADD] 658 659val word_mult_clauses = 660 List.take ((map GEN_ALL o CONJUNCTS o SPEC_ALL) WORD_MULT_CLAUSES, 4) 661 662val WORD_MULT_LEFT_1 = List.nth (word_mult_clauses, 2) 663 664val NEG_EQ_0 = trace ("metis", 0) (METIS_PROVE [WORD_NEG_MUL, WORD_NEG_EQ_0]) 665 ``(!w:'a word. (-1w * w = 0w) = (w = 0w)) /\ 666 (!w:'a word. (0w = -1w * w) = (w = 0w))`` 667 668(* ------------------------------------------------------------------------- *) 669 670local 671 val SYM_WORD_DIV_LSR = GSYM WORD_DIV_LSR 672 val one_tm = numSyntax.term_of_int 1 673 val two_tm = numSyntax.term_of_int 2 674in 675 (* 676 e.g. WORD_DIV_LSR_CONV ``w // 8w : word16`` 677 |- w // 8w = w >>> 3 678 *) 679 680 fun WORD_DIV_LSR_CONV tm = 681 let 682 val (l, r) = wordsSyntax.dest_word_div tm 683 val (v, ty) = wordsSyntax.dest_n2w r 684 val p = fst (wordsSyntax.dest_mod_word_literal r) 685 val n = numSyntax.mk_numeral (Arbnum.log2 p) 686 val lt_thm = numSyntax.mk_less (n, wordsSyntax.mk_dimindex ty) 687 |> (Conv.RAND_CONV SIZES_CONV THENC numLib.REDUCE_CONV) 688 |> Drule.EQT_ELIM 689 val exp_thm = boolSyntax.mk_eq 690 (wordsSyntax.mk_n2w (v, ty), 691 wordsSyntax.mk_n2w (numSyntax.mk_exp (two_tm, n), ty)) 692 |> WORD_EVAL_CONV 693 |> Drule.EQT_ELIM 694 val thm1 = Rewrite.PURE_ONCE_REWRITE_CONV [exp_thm] tm 695 val thm2 = Thm.MP (Drule.ISPECL [l, n] SYM_WORD_DIV_LSR) lt_thm 696 in 697 Thm.TRANS thm1 thm2 698 end 699 handle HOL_ERR _ => raise ERR "WORD_DIV_LSR_CONV" "" 700 | Domain => raise ERR "WORD_DIV_LSR_CONV" "Divide by zero" 701 702 (* 703 e.g. WORD_MOD_BITS_CONV ``word_mod w 8w : word16`` 704 |- word_mod w 8w = (2 -- 0) w 705 *) 706 707 fun WORD_MOD_BITS_CONV tm = 708 let 709 val (l, r) = wordsSyntax.dest_word_mod tm 710 val (v, ty) = wordsSyntax.dest_n2w r 711 val p = fst (wordsSyntax.dest_mod_word_literal r) 712 in 713 if p = Arbnum.zero 714 then raise ERR "" "" 715 else if p = Arbnum.one 716 then let 717 val p_tm = wordsSyntax.mk_n2w (one_tm, ty) 718 val p_thm = boolSyntax.mk_eq (r, p_tm) 719 |> WORD_EVAL_CONV |> EQT_ELIM 720 in 721 PURE_REWRITE_CONV [p_thm, WORD_MOD_1] tm 722 end 723 else let 724 val n = numSyntax.mk_numeral (Arbnum.less1 (Arbnum.log2 p)) 725 val dim_sub1 = 726 numSyntax.mk_minus (wordsSyntax.mk_dimindex ty, one_tm) 727 val lt_thm = numSyntax.mk_less (n, dim_sub1) 728 |> (Conv.RAND_CONV (Conv.LAND_CONV SIZES_CONV) 729 THENC numLib.REDUCE_CONV) 730 |> Drule.EQT_ELIM 731 val exp_thm = 732 boolSyntax.mk_eq 733 (wordsSyntax.mk_n2w (v, ty), 734 wordsSyntax.mk_n2w 735 (numSyntax.mk_exp (two_tm, numSyntax.mk_suc n), ty)) 736 |> WORD_EVAL_CONV 737 |> Drule.EQT_ELIM 738 val thm1 = Rewrite.PURE_ONCE_REWRITE_CONV [exp_thm] tm 739 val thm2 = Thm.MP (Drule.ISPECL [l, n] WORD_MOD_POW2) lt_thm 740 in 741 Thm.TRANS thm1 thm2 742 end 743 end 744 handle HOL_ERR _ => raise ERR "WORD_MOD_BITS_CONV" "" 745end 746 747(* ------------------------------------------------------------------------- *) 748 749val is_known_word_size = not o is_vartype o wordsSyntax.dim_of 750 751local 752 val cnv = PURE_ONCE_REWRITE_CONV [GSYM n2w_mod] 753 THENC Conv.DEPTH_CONV SIZES_CONV 754 THENC numLib.REDUCE_CONV 755in 756 fun WORD_LITERAL_REDUCE_CONV t = 757 if is_known_word_size t then cnv t else numLib.REDUCE_CONV t 758end 759 760val WORD_ADD_REDUCE_CONV = 761 PURE_REWRITE_CONV WORD_LITERAL_ADD_thms THENC WORD_LITERAL_REDUCE_CONV 762 763val gci_word_mul = 764 let 765 val cnv = PURE_REWRITE_CONV WORD_LITERAL_MULT_thms 766 THENC WORD_LITERAL_REDUCE_CONV 767 in 768 GenPolyCanon.GCI 769 {dest = wordsSyntax.dest_word_mul, 770 is_literal = fn t => is_word_literal t 771 orelse wordsSyntax.is_word_L t 772 orelse wordsSyntax.is_word_L2 t, 773 assoc_mode = GenPolyCanon.L_Cflipped, 774 assoc = WORD_MULT_ASSOC, 775 symassoc = GSYM WORD_MULT_ASSOC, 776 comm = WORD_MULT_COMM, 777 l_asscomm = GenPolyCanon.derive_l_asscomm WORD_MULT_ASSOC WORD_MULT_COMM, 778 r_asscomm = GenPolyCanon.derive_r_asscomm WORD_MULT_ASSOC WORD_MULT_COMM, 779 non_coeff = I, 780 merge = cnv, 781 postnorm = ALL_CONV, 782 left_id = WORD_MULT_LEFT_1, 783 right_id = List.nth (word_mult_clauses, 3), 784 reducer = cnv} 785 end 786 787local 788 fun is_good t = 789 let 790 val (l, r) = wordsSyntax.dest_word_mul t 791 in 792 is_word_literal l 793 end 794 handle HOL_ERR _ => false 795 fun non_coeff t = 796 if is_good t 797 then boolSyntax.rand t 798 else if is_word_literal t 799 then mk_var (" ", Term.type_of t) 800 else t 801 val cnv = REWR_CONV (GSYM WORD_MULT_LEFT_1) 802 fun add_coeff (t:term) : thm = if is_good t then ALL_CONV t else cnv t 803 val distrib = GSYM WORD_RIGHT_ADD_DISTRIB 804 fun merge t = 805 let 806 val (l, r) = wordsSyntax.dest_word_add t 807 in 808 if is_word_literal l andalso is_word_literal r 809 then WORD_ADD_REDUCE_CONV t 810 else (Conv.BINOP_CONV add_coeff 811 THENC REWR_CONV distrib 812 THENC LAND_CONV WORD_ADD_REDUCE_CONV) t 813 end 814in 815 val gci_word_add = GenPolyCanon.GCI 816 {dest = wordsSyntax.dest_word_add, 817 is_literal = is_word_literal, 818 assoc_mode = GenPolyCanon.L, 819 assoc = WORD_ADD_ASSOC, 820 symassoc = GSYM WORD_ADD_ASSOC, 821 comm = WORD_ADD_COMM, 822 l_asscomm = GenPolyCanon.derive_l_asscomm WORD_ADD_ASSOC WORD_ADD_COMM, 823 r_asscomm = GenPolyCanon.derive_r_asscomm WORD_ADD_ASSOC WORD_ADD_COMM, 824 non_coeff = non_coeff, 825 merge = merge, 826 postnorm = REWRITE_CONV word_mult_clauses, 827 left_id = CONJUNCT2 WORD_ADD_0, 828 right_id = CONJUNCT1 WORD_ADD_0, 829 reducer = WORD_ADD_REDUCE_CONV} 830end 831 832local 833 val cnv1 = 834 PURE_REWRITE_CONV 835 [INT_MAX_def, word_L_def, word_H_def, SYM_WORD_NEG_1, w2n_n2w] 836 THENC DEPTH_CONV SIZES_CONV 837 THENC numLib.REDUCE_CONV 838 val cnv2 = CHANGED_CONV (PURE_REWRITE_CONV [WORD_H_WORD_L, SYM_WORD_NEG_1]) 839 val cnv3 = CHANGED_CONV (PURE_REWRITE_CONV [word_0_n2w, word_1_n2w]) 840in 841 fun WORD_CONST_CONV t = 842 if is_known_word_size t andalso is_word_lht t then cnv1 t else cnv2 t 843 fun WORD_w2n_CONV t = 844 let 845 val x = wordsSyntax.dest_w2n t 846 in 847 if wordsSyntax.is_n2w x 848 then (if is_known_word_size x then cnv1 else cnv3) t 849 else raise ERR "WORD_w2n_CONV" "Not w2n of word literal" 850 end 851end 852 853local 854 val cnv1 = Conv.REWR_CONV word_2comp_n2w 855 THENC Conv.REWR_CONV (GSYM n2w_mod) 856 THENC Conv.DEPTH_CONV SIZES_CONV THENC numLib.REDUCE_CONV 857 val cnv2 = Conv.REWR_CONV WORD_NEG_0 858 val cnv3 = PURE_REWRITE_CONV [WORD_NEG_L] 859 THENC PURE_ONCE_REWRITE_CONV [WORD_NEG_MUL] 860in 861 fun WORD_NEG_CONV t = 862 let 863 val x = wordsSyntax.dest_word_2comp t 864 in 865 if wordsSyntax.is_n2w x 866 then if is_known_word_size t andalso not (is_word_one x) 867 then cnv1 t 868 else if is_word_zero x 869 then cnv2 t 870 else raise ERR "WORD_NEG_CONV" "Negative 'a word literal" 871 else cnv3 t 872 end 873end 874 875local 876 val cnv1 = PURE_ONCE_REWRITE_CONV [n2w_11] 877 THENC Conv.DEPTH_CONV SIZES_CONV 878 THENC numLib.REDUCE_CONV 879 val cnv2 = PURE_ONCE_REWRITE_CONV [GSYM WORD_EQ_SUB_ZERO] 880 fun err s = raise ERR "WORD_ARITH_EQ_CONV" s 881in 882 fun WORD_ARITH_EQ_CONV t = 883 let 884 val (x, y) = boolSyntax.dest_eq t 885 in 886 if wordsSyntax.is_word_type (Term.type_of y) 887 then if is_known_word_size x 888 andalso wordsSyntax.is_n2w x 889 andalso wordsSyntax.is_n2w y 890 then cnv1 t 891 else if is_word_zero y 892 then err "RHS is zero" 893 else cnv2 t 894 else err "Not word equality" 895 end 896end 897 898fun is_eq_word_L tm = 899 let 900 val ty = wordsSyntax.dim_of tm 901 val tm = boolSyntax.mk_eq (tm, wordsSyntax.mk_word_L ty) 902 in 903 Lib.can Drule.EQT_ELIM (WORD_EVAL_CONV tm) 904 end 905 906fun is_negative tm = 907 Lib.can Drule.EQT_ELIM (WORD_EVAL_CONV (wordsSyntax.mk_word_msb tm)) 908 909fun is_neg_term t = 910 wordsSyntax.is_word_2comp t 911 orelse 912 if wordsSyntax.is_n2w t 913 then is_known_word_size t 914 andalso is_negative t 915 andalso not (is_eq_word_L t) 916 else if wordsSyntax.is_word_add t 917 then is_neg_term (fst (wordsSyntax.dest_word_add t)) 918 else wordsSyntax.is_word_mul t 919 andalso is_neg_term (fst (wordsSyntax.dest_word_mul t)) 920 921local 922 val cnv = Conv.REWR_CONV (GSYM WORD_NEG_EQ_0) 923in 924 fun FIX_SIGN_OF_NEG_TERM_CONV t = 925 let 926 val (x, y) = dest_eq t 927 in 928 if is_word_zero y andalso is_neg_term x 929 then cnv t 930 else raise ERR "FIX_SIGN_OF_NEG_TERM_CONV" "Not neg term with zero RHS" 931 end 932end 933 934local 935 fun gen_dest_word_literal t = 936 case Lib.total wordsSyntax.dest_word_2comp t of 937 SOME n => 938 Arbint.negate (Arbint.fromNat (wordsSyntax.dest_word_literal n)) 939 | NONE => Arbint.fromNat (wordsSyntax.dest_word_literal t) 940 fun gen_is_negative pick_word_l tm = 941 if is_known_word_size tm 942 then is_negative tm andalso (pick_word_l orelse not (is_eq_word_L tm)) 943 else Arbint.<= (gen_dest_word_literal tm, Arbint.fromInt ~1) 944 fun is_zero tm = 945 case Lib.total gen_dest_word_literal tm of 946 SOME i => i = Arbint.zero 947 | NONE => false 948 fun pick_left_coeff x z = 949 if is_known_word_size x 950 then gen_is_negative false (wordsSyntax.mk_word_sub (x, z)) 951 else Arbint.< (gen_dest_word_literal x, gen_dest_word_literal z) 952 fun partition_same t l = List.partition (fn (_, y) => y = t) l 953 fun pick_coeff_terms a = 954 fn ([], l) => a @ List.filter (gen_is_negative true o fst) l 955 | ((x, y) :: t, l) => 956 (case partition_same y l of 957 ([], _) => 958 pick_coeff_terms 959 (if gen_is_negative false x then (x, y) :: a else a) (t, l) 960 | ([(z, _)], r) => 961 pick_coeff_terms 962 ((if pick_left_coeff x z then x else z, y) :: a) (t, r) 963 | _ => raise ERR "pick_coeff_terms" "") 964 fun join_coeff_terms (z as (_, y)) l = 965 if Lib.all (fn (_, x) => x <> y) l 966 then z::l 967 else raise ERR "join_coeff_terms" "" 968 fun mk_one tm = wordsSyntax.mk_n2w (``1n``, wordsSyntax.dim_of tm) 969 fun get_coeff_terms a tm = 970 case Lib.total boolSyntax.dest_strip_comb tm of 971 SOME ("words$word_add", [l, r]) => 972 get_coeff_terms (get_coeff_terms a l) r 973 | SOME ("words$word_mul", [l, r]) => 974 if is_zero l 975 then raise ERR "get_coeff_terms" "zero" 976 else if is_word_literal l 977 then join_coeff_terms (l, r) a 978 else join_coeff_terms (mk_one tm, tm) a 979 | _ => if is_zero tm 980 then raise ERR "get_coeff_terms" "zero" 981 else if is_word_literal tm 982 then join_coeff_terms (tm, mk_one tm) a 983 else join_coeff_terms (mk_one tm, tm) a 984 val lcancel_sub = Conv.GSYM wordsTheory.WORD_LCANCEL_SUB 985 fun mk_cancel_thm x = 986 let 987 val p = wordsSyntax.mk_word_mul x 988 val ty = Term.type_of p 989 val fvs = Term.free_vars p 990 val x = Term.variant fvs (Term.mk_var ("x", ty)) 991 val y = Term.variant fvs (Term.mk_var ("y", ty)) 992 in 993 lcancel_sub 994 |> Thm.INST_TYPE [Type.alpha |-> wordsSyntax.dest_word_type ty] 995 |> Drule.SPECL [x, p, y] 996 end 997 fun compare_coeff (x, y) = 998 Term.compare (wordsSyntax.mk_word_mul x, wordsSyntax.mk_word_mul y) 999 val is_lit_coeff = fn [r] => wordsSyntax.is_word_literal (snd r) 1000 | _ => false 1001 fun is_word_L_lit tm = is_word_literal tm andalso is_eq_word_L tm 1002 fun swap_sides l = 1003 fn [] => false 1004 | r => 1005 not (is_lit_coeff r) 1006 andalso 1007 let 1008 val (xl, fl) = List.partition (is_word_L_lit o fst) l 1009 in 1010 if List.null xl 1011 then case Int.compare (List.length l, List.length r) of 1012 EQUAL => 1013 Lib.list_compare compare_coeff (r, l) = GREATER 1014 | LESS => true 1015 | GREATER => false 1016 else case Int.compare 1017 (List.length l, List.length xl + List.length r) of 1018 EQUAL => Lib.list_compare compare_coeff (r, fl) = GREATER 1019 | LESS => false 1020 | GREATER => true 1021 end 1022in 1023 fun WORD_CANCEL_CONV tm = 1024 let 1025 val (l, r) = boolSyntax.dest_eq tm 1026 val _ = wordsSyntax.is_word_type (Term.type_of l) 1027 andalso not (wordsSyntax.is_word_sub l) 1028 orelse raise ERR "WORD_CANCEL_CONV" "Is subraction" 1029 val l = if is_zero l then [] else get_coeff_terms [] l 1030 val r = if is_zero r then [] else get_coeff_terms [] r 1031 in 1032 case pick_coeff_terms [] (l, r) of 1033 [] => if swap_sides l r 1034 then Conv.REWR_CONV boolTheory.EQ_SYM_EQ tm 1035 else raise ERR "WORD_CANCEL_CONV" "Nothing to cancel" 1036 | ps => (List.foldl 1037 (fn (p, cnv) => cnv THENC Conv.REWR_CONV (mk_cancel_thm p)) 1038 Conv.ALL_CONV ps) tm 1039 end 1040end 1041 1042fun WORD_MULT_CANON_CONV t = 1043 if wordsSyntax.is_word_type (type_of t) 1044 then GenPolyCanon.gencanon gci_word_mul t 1045 else raise ERR "WORD_MULT_CANON_CONV" "Can only be applied to word terms" 1046 1047fun WORD_ADD_CANON_CONV t = 1048 if wordsSyntax.is_word_type (type_of t) 1049 then GenPolyCanon.gencanon gci_word_add t 1050 else raise ERR "WORD_ADD_CANON_CONV" "Can only be applied to word terms" 1051 1052val WORD_MULT_ss = 1053 simpLib.merge_ss 1054 [simpLib.rewrites (NEG_EQ_0::word_mult_clauses), 1055 simpLib.std_conv_ss 1056 {conv = CHANGED_CONV WORD_MULT_CANON_CONV, 1057 name = "WORD_MULT_CANON_CONV", 1058 pats = [``words$word_mul (w:'a word) y``]}] 1059 1060val WORD_ADD_ss = 1061 simpLib.std_conv_ss 1062 {conv = CHANGED_CONV WORD_ADD_CANON_CONV, 1063 name = "WORD_ADD_CANON_CONV", 1064 pats = [``words$word_add (w:'a word) y``]} 1065 1066val WORD_SUBTRACT_ss = 1067 simpLib.named_merge_ss "word subtract" 1068 [simpLib.rewrites [word_sub_def], 1069 simpLib.std_conv_ss 1070 {conv = WORD_NEG_CONV, 1071 name = "WORD_NEG_CONV", 1072 pats = [``words$word_2comp (w:'a word)``, 1073 ``words$word_sub (w:'a word) y``]}] 1074 1075val WORD_w2n_ss = 1076 simpLib.merge_ss 1077 [simpLib.rewrites [word_0_n2w], 1078 simpLib.std_conv_ss 1079 {conv = WORD_w2n_CONV, 1080 name = "WORD_w2n_CONV", 1081 pats = [``words$w2n (^n2w ^Na)``]}] 1082 1083val WORD_CONST_ss = 1084 simpLib.std_conv_ss 1085 {conv = WORD_CONST_CONV, 1086 name = "WORD_CONST_CONV", 1087 pats = [``words$word_L :'a word``, 1088 ``words$word_H :'a word``, 1089 ``words$word_T :'a word``]} 1090 1091val WORD_ARITH_EQ_ss = 1092 simpLib.named_merge_ss "word arith eq" 1093 [simpLib.rewrites 1094 [WORD_LEFT_ADD_DISTRIB, WORD_RIGHT_ADD_DISTRIB, 1095 WORD_LSL_NUMERAL, WORD_NOT, hd (CONJUNCTS SHIFT_ZERO)], 1096 simpLib.std_conv_ss 1097 {conv = WORD_ARITH_EQ_CONV, 1098 name = "WORD_ARITH_EQ_CONV", 1099 pats = [``w = y :'a word``]}] 1100 1101val WORD_CANCEL_ss = 1102 simpLib.named_merge_ss "word cancel" 1103 [simpLib.rewrites 1104 [WORD_LEFT_ADD_DISTRIB, WORD_RIGHT_ADD_DISTRIB, 1105 WORD_NOT, hd (CONJUNCTS SHIFT_ZERO)], 1106 simpLib.std_conv_ss 1107 {conv = WORD_CANCEL_CONV, 1108 name = "WORD_CANCEL_CONV", 1109 pats = [``w = y :'a word``]}] 1110 1111val WORD_ABS_ss = 1112 simpLib.rewrites 1113 [word_abs_word_abs, word_abs_neg, 1114 ONCE_REWRITE_RULE [WORD_NEG_MUL] word_abs_neg] 1115 1116val WORD_ARITH_ss = 1117 simpLib.named_merge_ss "word arith" 1118 [WORD_MULT_ss, WORD_ADD_ss, WORD_SUBTRACT_ss, WORD_w2n_ss, WORD_CONST_ss, 1119 WORD_ABS_ss] 1120 1121local 1122 val conv = SIMP_CONV (std_ss++WORD_ARITH_EQ_ss++WORD_ARITH_ss) [] 1123in 1124 val WORD_ARITH_CONV = 1125 conv THENC (ONCE_DEPTH_CONV FIX_SIGN_OF_NEG_TERM_CONV) THENC conv 1126end 1127 1128(* ------------------------------------------------------------------------- *) 1129 1130val BITWISE_CONV = 1131 let open numeral_bitTheory in 1132 computeLib.compset_conv (reduceLib.num_compset()) 1133 [computeLib.Defs [NUMERAL_BITWISE, iBITWISE, numeral_log2, numeral_ilog2], 1134 computeLib.Convs [(``fcp$dimindex:'a itself->num``, 1, SIZES_CONV)]] 1135 end 1136 1137val WORD_LITERAL_AND_thms = 1138 (numLib.SUC_RULE o REWRITE_RULE [WORD_NOT_NUMERAL]) WORD_LITERAL_AND 1139 1140val WORD_LITERAL_OR_thms = 1141 (numLib.SUC_RULE o REWRITE_RULE [WORD_NOT_NUMERAL]) WORD_LITERAL_OR 1142 1143val GSYM_WORD_OR_ASSOC = GSYM WORD_OR_ASSOC 1144val GSYM_WORD_AND_ASSOC = GSYM WORD_AND_ASSOC 1145val GSYM_WORD_XOR_ASSOC = GSYM WORD_XOR_ASSOC 1146 1147val WORD_OR_CLAUSES2 = REWRITE_RULE [SYM_WORD_NEG_1] WORD_OR_CLAUSES 1148val WORD_AND_CLAUSES2 = REWRITE_RULE [SYM_WORD_NEG_1] WORD_AND_CLAUSES 1149val WORD_XOR_CLAUSES2 = REWRITE_RULE [SYM_WORD_NEG_1] WORD_XOR_CLAUSES 1150 1151val word_or_clauses = CONJUNCTS (Q.SPEC `a` WORD_OR_CLAUSES2) 1152val word_and_clauses = CONJUNCTS (Q.SPEC `a` WORD_AND_CLAUSES2) 1153val word_xor_clauses = CONJUNCTS (Q.SPEC `a` WORD_XOR_CLAUSES2) 1154 1155val WORD_AND_LEFT_T = hd word_and_clauses 1156val WORD_OR_RIGHT_T = hd (tl word_or_clauses) 1157val WORD_XOR_RIGHT_T = hd (tl word_xor_clauses) 1158 1159local 1160 val WORD_REDUCE_CONV = 1161 PURE_REWRITE_CONV [WORD_AND_CLAUSES2] 1162 THENC PURE_REWRITE_CONV [WORD_LITERAL_AND_thms] 1163 THENC BITWISE_CONV 1164in 1165 val gci_word_and = 1166 GenPolyCanon.GCI 1167 {dest = wordsSyntax.dest_word_and, 1168 is_literal = is_word_literal, 1169 assoc_mode = GenPolyCanon.L_Cflipped, 1170 assoc = GSYM_WORD_AND_ASSOC, 1171 symassoc = WORD_AND_ASSOC, 1172 comm = WORD_AND_COMM, 1173 l_asscomm = 1174 GenPolyCanon.derive_l_asscomm GSYM_WORD_AND_ASSOC WORD_AND_COMM, 1175 r_asscomm = 1176 GenPolyCanon.derive_r_asscomm GSYM_WORD_AND_ASSOC WORD_AND_COMM, 1177 non_coeff = Lib.I, 1178 merge = WORD_REDUCE_CONV, 1179 postnorm = ALL_CONV, 1180 left_id = WORD_AND_LEFT_T, 1181 right_id = hd (tl word_and_clauses), 1182 reducer = WORD_REDUCE_CONV} 1183end 1184 1185local 1186 fun is_good t = 1187 let 1188 val (l, r) = wordsSyntax.dest_word_and t 1189 in 1190 is_word_literal l 1191 end 1192 handle HOL_ERR _ => false 1193 fun non_coeff t = 1194 if is_good t 1195 then boolSyntax.rand t 1196 else if is_word_literal t 1197 then Term.mk_var (" ", type_of t) 1198 else t 1199 fun add_coeff (t: term) : thm = 1200 if is_good t then ALL_CONV t else REWR_CONV (GSYM WORD_AND_LEFT_T) t 1201in 1202 local 1203 val distrib = GSYM WORD_RIGHT_AND_OVER_OR 1204 val cnv1 = 1205 PURE_REWRITE_CONV [WORD_OR_CLAUSES2] 1206 THENC PURE_REWRITE_CONV [WORD_LITERAL_OR_thms] 1207 THENC BITWISE_CONV 1208 THENC WORD_LITERAL_REDUCE_CONV 1209 val cnv2 = Conv.BINOP_CONV add_coeff 1210 THENC Conv.REWR_CONV distrib 1211 THENC Conv.LAND_CONV cnv1 1212 fun merge t = 1213 let 1214 val (l, r) = wordsSyntax.dest_word_or t 1215 in 1216 (if is_word_literal l andalso is_word_literal r 1217 then cnv1 1218 else cnv2) t 1219 end 1220 in 1221 val gci_word_or = 1222 GenPolyCanon.GCI 1223 {dest = wordsSyntax.dest_word_or, 1224 is_literal = is_word_literal, 1225 assoc_mode = GenPolyCanon.R, 1226 assoc = GSYM_WORD_OR_ASSOC, 1227 symassoc = WORD_OR_ASSOC, 1228 comm = WORD_OR_COMM, 1229 l_asscomm = 1230 GenPolyCanon.derive_l_asscomm GSYM_WORD_OR_ASSOC WORD_OR_COMM, 1231 r_asscomm = 1232 GenPolyCanon.derive_r_asscomm GSYM_WORD_OR_ASSOC WORD_OR_COMM, 1233 non_coeff = non_coeff, 1234 merge = merge, 1235 postnorm = ALL_CONV, 1236 left_id = hd word_or_clauses, 1237 right_id = WORD_OR_RIGHT_T, 1238 reducer = cnv1} 1239 end 1240 local 1241 val distrib = GSYM WORD_RIGHT_AND_OVER_XOR 1242 val cnv1 = 1243 PURE_REWRITE_CONV [WORD_XOR_CLAUSES2] 1244 THENC PURE_REWRITE_CONV [WORD_NOT_XOR, WORD_LITERAL_XOR] 1245 THENC BITWISE_CONV 1246 THENC WORD_LITERAL_REDUCE_CONV 1247 val cnv2 = Conv.BINOP_CONV add_coeff 1248 THENC Conv.REWR_CONV distrib 1249 THENC LAND_CONV cnv1 1250 fun merge t = 1251 let 1252 val (l, r) = wordsSyntax.dest_word_xor t 1253 in 1254 (if is_word_literal l andalso is_word_literal r 1255 then cnv1 1256 else cnv2) t 1257 end 1258 in 1259 val gci_word_xor = 1260 GenPolyCanon.GCI 1261 {dest = wordsSyntax.dest_word_xor, 1262 is_literal = is_word_literal, 1263 assoc_mode = GenPolyCanon.R, 1264 assoc = GSYM_WORD_XOR_ASSOC, 1265 symassoc = WORD_XOR_ASSOC, 1266 comm = WORD_XOR_COMM, 1267 l_asscomm = 1268 GenPolyCanon.derive_l_asscomm GSYM_WORD_XOR_ASSOC WORD_XOR_COMM, 1269 r_asscomm = 1270 GenPolyCanon.derive_r_asscomm GSYM_WORD_XOR_ASSOC WORD_XOR_COMM, 1271 non_coeff = non_coeff, 1272 merge = merge, 1273 postnorm = ALL_CONV, 1274 left_id = hd word_xor_clauses, 1275 right_id = hd (tl word_xor_clauses), 1276 reducer = cnv1} 1277 end 1278end 1279 1280local 1281 val cnv1 = PURE_REWRITE_CONV [REWRITE_RULE [SYM_WORD_NEG_1] WORD_NOT_0] 1282 val cnv2 = PURE_REWRITE_CONV [word_1comp_n2w] 1283 THENC Conv.DEPTH_CONV SIZES_CONV 1284 THENC numLib.REDUCE_CONV 1285 val cnv3 = PURE_REWRITE_CONV [WORD_NOT_NUMERAL] THENC numLib.REDUCE_CONV 1286in 1287 fun WORD_COMP_CONV t = 1288 let 1289 val x = wordsSyntax.dest_word_1comp t 1290 in 1291 if is_known_word_size t 1292 then if is_word_zero x 1293 then cnv1 t 1294 else if wordsSyntax.is_word_literal x 1295 then cnv2 t 1296 else raise ERR "WORD_COMP_CONV" "Must be word literal" 1297 else cnv3 t 1298 end 1299end 1300 1301local 1302 val cnv = 1303 GenPolyCanon.gencanon gci_word_and 1304 THENC Conv.TRY_CONV 1305 (Conv.LAND_CONV UINT_MAX_CONV 1306 THENC Conv.REWR_CONV WORD_AND_LEFT_T) 1307in 1308 fun WORD_AND_CANON_CONV t = 1309 if wordsSyntax.is_word_type (type_of t) 1310 then cnv t 1311 else raise ERR "WORD_AND_CANON_CONV" "Can only be applied to word terms" 1312end 1313 1314local 1315 val cnv = 1316 GenPolyCanon.gencanon gci_word_or 1317 THENC Conv.TRY_CONV 1318 (Conv.RAND_CONV UINT_MAX_CONV 1319 THENC Conv.REWR_CONV WORD_OR_RIGHT_T) 1320in 1321 fun WORD_OR_CANON_CONV t = 1322 if wordsSyntax.is_word_type (type_of t) 1323 then cnv t 1324 else raise ERR "WORD_OR_CANON_CONV" "Can only be applied to word terms" 1325end 1326 1327local 1328 val cnv = 1329 GenPolyCanon.gencanon gci_word_xor 1330 THENC Conv.TRY_CONV 1331 (Conv.RAND_CONV UINT_MAX_CONV 1332 THENC Conv.REWR_CONV WORD_XOR_RIGHT_T) 1333in 1334 fun WORD_XOR_CANON_CONV t = 1335 if wordsSyntax.is_word_type (type_of t) 1336 then cnv t 1337 else raise ERR "WORD_XOR_CANON_CONV" "Can only be applied to word terms" 1338end 1339 1340val WORD_COMP_ss = 1341 simpLib.merge_ss 1342 [simpLib.rewrites 1343 [WORD_DE_MORGAN_THM, WORD_NOT_NOT, WORD_NOT_NEG_0, SYM_WORD_NEG_1, 1344 REWRITE_RULE [GSYM arithmeticTheory.PRE_SUB1] WORD_NOT_NEG_NUMERAL], 1345 simpLib.std_conv_ss 1346 {conv = reduceLib.PRE_CONV, 1347 name = "PRE_CONV", 1348 pats = [``prim_rec$PRE ^Na``]}, 1349 simpLib.std_conv_ss 1350 {conv = WORD_COMP_CONV, 1351 name = "WORD_COMP_CONV", 1352 pats = [``words$word_1comp (^n2w n) :'a word``]}] 1353 1354val WORD_AND_ss = 1355 simpLib.merge_ss 1356 [simpLib.rewrites [WORD_AND_CLAUSES2, WORD_AND_COMP, WORD_NAND_NOT_AND, 1357 WORD_AND_ABSORD, ONCE_REWRITE_RULE [WORD_AND_COMM] WORD_AND_ABSORD], 1358 simpLib.std_conv_ss 1359 {conv = WORD_AND_CANON_CONV, 1360 name = "WORD_AND_CANON_CONV", 1361 pats = [``words$word_and (w:'a word) y``]}] 1362 1363val WORD_XOR_ss = 1364 simpLib.merge_ss 1365 [simpLib.rewrites [WORD_XOR_CLAUSES2, WORD_NOT_XOR, WORD_XNOR_NOT_XOR], 1366 simpLib.std_conv_ss 1367 {conv = WORD_XOR_CANON_CONV, 1368 name = "WORD_XOR_CANON_CONV", 1369 pats = [``words$word_xor (w:'a word) y``]}] 1370 1371val WORD_OR_ss = 1372 let 1373 val thm = REWRITE_RULE [SYM_WORD_NEG_1] WORD_OR_COMP 1374 in 1375 simpLib.merge_ss 1376 [simpLib.rewrites 1377 [WORD_OR_CLAUSES2, WORD_NOR_NOT_OR, 1378 thm, ONCE_REWRITE_RULE [WORD_OR_COMM] thm], 1379 simpLib.std_conv_ss 1380 {conv = WORD_OR_CANON_CONV, 1381 name = "WORD_OR_CANON_CONV", 1382 pats = [``words$word_or (w:'a word) y``]}] 1383 end 1384 1385val WORD_LOGIC_ss = 1386 simpLib.named_merge_ss "word logic" 1387 [WORD_COMP_ss, WORD_AND_ss, WORD_OR_ss, WORD_XOR_ss] 1388 1389val WORD_LOGIC_CONV = 1390 SIMP_CONV (bool_ss++WORD_LOGIC_ss) 1391 [WORD_LEFT_AND_OVER_OR, WORD_RIGHT_AND_OVER_OR, REFL_CLAUSE] 1392 1393(* ------------------------------------------------------------------------- *) 1394 1395val ROL_ROR_MOD_RWT = Q.prove( 1396 `!n w:'a word. fcp$dimindex (:'a) <= n ==> 1397 (words$word_rol w n = 1398 words$word_rol w (arithmetic$MOD n (fcp$dimindex (:'a)))) /\ 1399 (words$word_ror w n = 1400 words$word_ror w (arithmetic$MOD n (fcp$dimindex (:'a))))`, 1401 SRW_TAC [] [Once (GSYM ROL_MOD), Once (GSYM ROR_MOD)]) 1402 1403val ASR_ROR_ROL_UINT_MAX = Q.prove( 1404 `(!m n. (n2w n = -1w: 'a word) ==> (n2w n >> m = -1w: 'a word)) /\ 1405 (!m n. (n2w n = -1w: 'a word) ==> (n2w n #>> m = -1w: 'a word)) /\ 1406 (!m n. (n2w n = -1w: 'a word) ==> (n2w n #<< m = -1w: 'a word))`, 1407 SIMP_TAC std_ss [WORD_NEG_1, ASR_UINT_MAX, ROR_UINT_MAX, word_rol_def] 1408 ) 1409 1410val WORD_SHIFT_ss = 1411 simpLib.named_rewrites "word shift" 1412 ([SHIFT_ZERO, ZERO_SHIFT, word_rrx_0, word_rrx_word_T, lsr_1_word_T, 1413 LSL_ADD, LSR_ADD, ASR_ADD, ROR_ROL, ROR_ADD, ROL_ADD, ROL_ROR_MOD_RWT, 1414 ASR_ROR_ROL_UINT_MAX, WORD_ADD_LSL, GSYM WORD_2COMP_LSL, 1415 GSYM LSL_BITWISE, GSYM LSR_BITWISE, GSYM ROR_BITWISE, GSYM ROL_BITWISE, 1416 LSL_LIMIT, LSR_LIMIT, REWRITE_RULE [SYM_WORD_NEG_1] ASR_LIMIT] @ 1417 List.map (REWRITE_RULE [w2n_n2w] o Q.SPECL [`w`, `n2w n`]) 1418 [word_lsl_bv_def, word_lsr_bv_def, word_asr_bv_def, 1419 word_ror_bv_def, word_rol_bv_def]) 1420 1421(* ------------------------------------------------------------------------- *) 1422 1423local 1424 fun odd n = Arbnum.mod2 n = Arbnum.one 1425 fun num2list' i l n = 1426 if n = Arbnum.zero 1427 then l 1428 else num2list' (Arbnum.plus1 i) (if odd n then i :: l else l) 1429 (Arbnum.div2 n) 1430 val num2list = num2list' Arbnum.zero [] 1431 1432 fun shift_n t n = 1433 if n = Arbnum.zero 1434 then t 1435 else wordsSyntax.mk_word_lsl (t, numSyntax.mk_numeral n) 1436 1437 fun sum_n l = 1438 List.foldl (fn (a, b) => wordsSyntax.mk_word_add (b, a)) (hd l) (tl l) 1439 1440 fun mk_sum_shifts (ty, v) = 1441 sum_n (List.map (shift_n (Term.mk_var ("x", ty))) (num2list v)) 1442 1443 val MUL_PLUS1 = List.nth (CONJUNCTS (SPEC_ALL WORD_MULT_CLAUSES), 4) 1444 |> SYM |> GEN_ALL 1445 1446 val MUL_DISTRIB = GSYM WORD_RIGHT_ADD_DISTRIB 1447 1448 val cnv = Conv.TRY_CONV 1449 (Conv.REWR_CONV WORD_LSL_NUMERAL 1450 THENC Conv.LAND_CONV WORD_EVAL_CONV) 1451 fun LSL_CONV tm = 1452 (if wordsSyntax.is_word_add tm 1453 then Conv.BINOP_CONV LSL_CONV 1454 else cnv) tm 1455 1456 val cnv = Conv.REWR_CONV MUL_PLUS1 ORELSEC Conv.REWR_CONV MUL_DISTRIB 1457 fun MUL_DISTRIB_CONV tm = 1458 (if wordsSyntax.is_word_add tm 1459 then Conv.LAND_CONV MUL_DISTRIB_CONV THENC cnv 1460 else Conv.ALL_CONV) tm 1461 1462 val LSL_MUL_CONV = 1463 LSL_CONV 1464 THENC MUL_DISTRIB_CONV 1465 THENC Conv.LAND_CONV WORD_ADD_REDUCE_CONV 1466in 1467 fun WORD_MUL_LSL_CONV tm = 1468 let 1469 val (l, r) = wordsSyntax.dest_word_mul tm 1470 val (v, sz) = wordsSyntax.dest_mod_word_literal l 1471 handle HOL_ERR _ => 1472 (wordsSyntax.dest_word_literal l, Arbnum.zero) 1473 val v2 = wordsSyntax.dest_word_literal l 1474 val conv = 1475 if v <> v2 1476 then Conv.REWR_CONV 1477 (Drule.EQT_ELIM 1478 (word_EQ_CONV 1479 (mk_eq (l, wordsSyntax.mk_word (v, sz))))) 1480 else Thm.REFL 1481 val thm = Conv.LAND_CONV conv tm 1482 val tm = rhs (concl thm) 1483 val rwt = 1484 if v = Arbnum.zero 1485 then hd word_mult_clauses 1486 else if v = Arbnum.one 1487 then List.nth (word_mult_clauses, 2) 1488 else SYM (LSL_MUL_CONV (mk_sum_shifts (Term.type_of tm, v))) 1489 in 1490 Thm.TRANS thm (Conv.REWR_CONV rwt tm) 1491 end 1492end 1493 1494val WORD_MUL_LSL_ss = 1495 simpLib.named_merge_ss "word mul lsl" 1496 [simpLib.std_conv_ss 1497 {conv = WORD_MUL_LSL_CONV, 1498 name = "WORD_MUL_LSL_CONV", 1499 pats = [``words$word_mul (^n2w ^Na) w:'a word``]}] 1500 1501(* ------------------------------------------------------------------------- *) 1502 1503fun WORD_LIT_CONV tm = 1504 let 1505 val ty = wordsSyntax.dim_of tm 1506 val (n, sz) = wordsSyntax.dest_mod_word_literal tm 1507 val res = if n <> Arbnum.zero 1508 andalso sz <> Arbnum.one 1509 andalso Arbnum.log2 n = Arbnum.less1 sz 1510 then wordsSyntax.mk_word_2comp 1511 (wordsSyntax.mk_n2w (numLib.mk_numeral 1512 (Arbnum.-(Arbnum.pow (Arbnum.two, sz), n)), ty)) 1513 else wordsSyntax.mk_n2w (numLib.mk_numeral n, ty) 1514 val _ = not (term_eq res tm) orelse raise Conv.UNCHANGED 1515 in 1516 boolSyntax.mk_eq (tm, res) |> WORD_EVAL_CONV |> Drule.EQT_ELIM 1517 end 1518 1519val NEG1_WORD1 = Drule.EQT_ELIM (WORD_EVAL_CONV ``-1w = 1w : word1``) 1520 1521fun WORD_SUB_CONV tm = 1522 Conv.CHANGED_CONV 1523 (SIMP_CONV (bool_ss++WORD_MULT_ss++WORD_SUBTRACT_ss) [] 1524 THENC DEPTH_CONV WORD_LIT_CONV 1525 THENC PURE_REWRITE_CONV [WORD_SUB_INTRO, WORD_NEG_SUB, WORD_SUB_RNEG, 1526 WORD_NEG_NEG, WORD_MULT_CLAUSES, NEG1_WORD1]) tm 1527 handle HOL_ERR (err as {origin_function, ...}) => 1528 if origin_function = "CHANGED_CONV" 1529 then raise Conv.UNCHANGED 1530 else raise HOL_ERR err 1531 1532val WORD_SUB_ss = 1533 simpLib.name_ss "WORD_SUB" 1534 (simpLib.std_conv_ss 1535 {name = "WORD_SUB_CONV", pats = [], conv = WORD_SUB_CONV}) 1536 1537(* ------------------------------------------------------------------------- *) 1538 1539(* 1540 1541Examples of EXTEND_EXTRACT_CONV: 1542 1543 EXTEND_EXTRACT_CONV ``(16 >< 11) (w: word32) : word64`` 1544 |- (16 >< 11) (w: word32) = w2w ((16 >< 11) w :word6) :word64 1545 1546 EXTEND_EXTRACT_CONV ``(30 >< 1) (w: word32) : word32`` 1547 |- (31 >< 0) (w: word32) : word32 = w2w ((30 >< 1) w : word30) 1548 1549 EXTEND_EXTRACT_CONV ``(31 >< 0) (w: word32) : word64`` 1550 |- (31 >< 0) (w: word32) : word64 = w2w w 1551 1552 EXTEND_EXTRACT_CONV ``(31 >< 0) (w: word32) : word32`` 1553 |- (31 >< 0) (w: word32) : word32 = w 1554 1555*) 1556 1557local 1558 val err = ERR "EXTRACT_ID_CONV" "not a suitable extract" 1559 val thm = wordsTheory.WORD_w2w_EXTRACT 1560 |> Thm.INST_TYPE [Type.beta |-> Type.alpha] 1561 |> REWRITE_RULE [wordsTheory.w2w_id] 1562 |> GSYM 1563 fun EXTRACT_ID_CONV tm = 1564 let 1565 val (h, l, w, ty) = Lib.with_exn wordsSyntax.dest_word_extract tm err 1566 val n = fcpLib.index_to_num ty 1567 val p = fcpLib.index_to_num (wordsSyntax.dim_of w) 1568 in 1569 if p = n andalso numSyntax.dest_numeral l = Arbnum.zero andalso 1570 Arbnum.plus1 (numSyntax.dest_numeral h) = n 1571 then thm 1572 |> Drule.ISPEC w 1573 |> Conv.CONV_RULE 1574 (Conv.LAND_CONV 1575 (Conv.RATOR_CONV 1576 (Conv.LAND_CONV 1577 (Conv.LAND_CONV SIZES_CONV 1578 THENC numLib.REDUCE_CONV)))) 1579 else raise err 1580 end 1581 val w2w_ID_CONV = Conv.TRY_CONV (Conv.REWR_CONV wordsTheory.w2w_id) 1582in 1583 fun EXTEND_EXTRACT_CONV tm = 1584 let 1585 val (h, l, w, ty) = wordsSyntax.dest_word_extract tm 1586 val B = fcpLib.index_to_num ty 1587 val C = 1588 Arbnum.- 1589 (Arbnum.plus1 (numLib.dest_numeral h), numLib.dest_numeral l) 1590 in 1591 if Arbnum.<= (C, B) 1592 then let 1593 val c_ty = fcpLib.index_type C 1594 val c_tm = 1595 boolSyntax.mk_eq 1596 (fcpSyntax.mk_dimindex c_ty, 1597 numSyntax.mk_minus (numSyntax.mk_plus (h, ``1n``), l)) 1598 val c_thm = 1599 (Conv.LHS_CONV SIZES_CONV THENC numLib.REDUCE_CONV) c_tm 1600 val c_thm = Drule.EQT_ELIM c_thm 1601 in 1602 Drule.MATCH_MP 1603 (Thm.INST_TYPE [Type.beta |-> ty, Type.gamma |-> c_ty] 1604 (Drule.ISPECL [h, l, w] wordsTheory.EXTEND_EXTRACT)) 1605 c_thm 1606 |> Conv.CONV_RULE 1607 (Conv.RAND_CONV 1608 (Conv.TRY_CONV 1609 (Conv.RAND_CONV EXTRACT_ID_CONV 1610 THENC w2w_ID_CONV))) 1611 end 1612 else raise ERR "EXTEND_EXTRACT_CONV" "" 1613 end 1614end 1615 1616val LET_RULE = SIMP_RULE (bool_ss++boolSimps.LET_ss) [] 1617val OR_AND_COMM_RULE = ONCE_REWRITE_RULE [WORD_ADD_COMM, WORD_OR_COMM] 1618 1619val WORD_EXTRACT_ss = 1620 simpLib.named_merge_ss "word extract" 1621 [simpLib.std_conv_ss 1622 {conv = WORD_EVAL_CONV, 1623 name = "WORD_EVAL_CONV", 1624 pats = [``words$word_replicate ^Na (w:'a word):'b word``]}, 1625 simpLib.rewrites 1626 ([WORD_EXTRACT_ZERO, WORD_EXTRACT_ZERO2, WORD_EXTRACT_ZERO3, 1627 WORD_EXTRACT_LSL, WORD_EXTRACT_LSL2, word_extract_eq_n2w, word_concat_def, 1628 LET_RULE word_join_def, word_rol_def, LET_RULE word_ror, word_asr, 1629 word_lsr_n2w, WORD_EXTRACT_COMP_THM, WORD_EXTRACT_MIN_HIGH, 1630 EXTRACT_JOIN, EXTRACT_JOIN_LSL, EXTRACT_JOIN_ADD, EXTRACT_JOIN_ADD_LSL, 1631 OR_AND_COMM_RULE EXTRACT_JOIN, OR_AND_COMM_RULE EXTRACT_JOIN_LSL, 1632 OR_AND_COMM_RULE EXTRACT_JOIN_ADD, OR_AND_COMM_RULE 1633 EXTRACT_JOIN_ADD_LSL, GSYM WORD_EXTRACT_OVER_BITWISE, 1634 (GEN_ALL o Q.ISPEC `words$word_extract h l :'a word->'b word`) COND_RAND, 1635 WORD_BITS_EXTRACT, WORD_w2w_EXTRACT, sw2sw_w2w, word_lsb, word_msb] @ 1636 map (REWRITE_RULE [WORD_BITS_EXTRACT]) 1637 [WORD_ALL_BITS, WORD_SLICE_THM, WORD_BIT_BITS])] 1638 1639(* ------------------------------------------------------------------------- *) 1640 1641local 1642 val thm = Drule.SPEC_ALL wordsTheory.word_concat_assoc 1643 val etm = thm |> Thm.concl |> boolSyntax.rand 1644 val ety = etm |> boolSyntax.rhs 1645 |> wordsSyntax.dest_word_concat |> snd 1646 |> wordsSyntax.dim_of 1647 val mtch = Drule.INST_TY_TERM o Term.match_term (boolSyntax.lhs etm) 1648 val err = ERR "WORD_CONCAT_ASSOC_CONV" "" 1649 fun attempt f a = Lib.with_exn f a err 1650 val rule = 1651 Conv.CONV_RULE 1652 (Conv.LAND_CONV (Conv.DEPTH_CONV SIZES_CONV THENC numLib.REDUCE_CONV) 1653 THENC Conv.REWR_CONV ConseqConvTheory.IMP_CLAUSES_TX) 1654in 1655 fun WORD_CONCAT_ASSOC_CONV tm = 1656 let 1657 val (ab, c) = attempt wordsSyntax.dest_word_concat tm 1658 val (a, b) = attempt wordsSyntax.dest_word_concat ab 1659 in 1660 case List.map (Lib.total wordsSyntax.size_of) [a, b, c, ab, tm] of 1661 [SOME na, SOME nb, SOME nc, SOME nab, SOME ntm] => 1662 if Arbnum.+ (na, nb) = nab andalso Arbnum.+ (nab, nc) = ntm 1663 then let 1664 val bc_ty = fcpSyntax.mk_numeric_type (Arbnum.+ (nb, nc)) 1665 in 1666 attempt (rule o Thm.INST_TYPE [ety |-> bc_ty] o mtch tm) thm 1667 end 1668 else raise err 1669 | _ => raise err 1670 end 1671end 1672 1673val WORD_CONCAT_ASSOC_ss = 1674 simpLib.std_conv_ss 1675 {conv = WORD_CONCAT_ASSOC_CONV, name = "WORD_CONCAT_ASSOC_CONV", 1676 pats = 1677 [``((((a:'a word) @@ (b:'b word)):'d word) @@ (c:'c word)):'e word``]} 1678 1679(* ------------------------------------------------------------------------- *) 1680 1681local 1682 val WORD_NO_SUB_ARITH_ss = 1683 simpLib.named_merge_ss "word arith" 1684 [WORD_MULT_ss, WORD_ADD_ss, WORD_w2n_ss, WORD_CONST_ss, WORD_ABS_ss] 1685 1686 val ssfrags = 1687 [WORD_LOGIC_ss, WORD_NO_SUB_ARITH_ss, WORD_SUBTRACT_ss, WORD_SHIFT_ss, 1688 WORD_GROUND_ss, BIT_ss, SIZES_ss, simpLib.rewrites [WORD_0_LS]] 1689in 1690 val WORD_ss = simpLib.named_merge_ss "words" ssfrags 1691 val _ = augment_srw_ss ssfrags 1692end 1693 1694val WORD_CONV = SIMP_CONV (std_ss++WORD_ss++WORD_EXTRACT_ss) 1695 [WORD_LEFT_ADD_DISTRIB, WORD_RIGHT_ADD_DISTRIB, 1696 WORD_LEFT_AND_OVER_OR, WORD_RIGHT_AND_OVER_OR] 1697 1698(* ------------------------------------------------------------------------- *) 1699 1700local 1701 open listTheory 1702 val cnv = 1703 computeLib.compset_conv (reduceLib.num_compset()) 1704 [computeLib.Defs 1705 [foldl_reduce_and, foldl_reduce_or, foldl_reduce_xor, 1706 foldl_reduce_nand, foldl_reduce_nor, foldl_reduce_xnor, 1707 GENLIST_AUX_compute, GENLIST_GENLIST_AUX, FOLDL, HD, TL], 1708 computeLib.Convs [(``fcp$dimindex:'a itself -> num``, 1, SIZES_CONV)]] 1709 fun reduce_thm f ty = 1710 if Lib.can (fcpLib.index_to_num o dest_word_type) ty 1711 then cnv (f (Term.mk_var ("w", ty))) 1712 else raise ERR "EXPAND_REDUCE_CONV" "" 1713in 1714 fun EXPAND_REDUCE_CONV tm = 1715 let 1716 val (f, w) = 1717 case boolSyntax.dest_strip_comb tm of 1718 ("words$reduce_and", [w]) => (wordsSyntax.mk_reduce_and, w) 1719 | ("words$reduce_or", [w]) => (wordsSyntax.mk_reduce_or, w) 1720 | ("words$reduce_xor", [w]) => (wordsSyntax.mk_reduce_xor, w) 1721 | ("words$reduce_nand", [w]) => (wordsSyntax.mk_reduce_nand, w) 1722 | ("words$reduce_nor", [w]) => (wordsSyntax.mk_reduce_nor, w) 1723 | ("words$reduce_xnor", [w]) => (wordsSyntax.mk_reduce_xnor, w) 1724 | _ => raise ERR "EXPAND_REDUCE_CONV" "" 1725 in 1726 Conv.REWR_CONV (reduce_thm f (Term.type_of w)) tm 1727 end 1728end 1729 1730(* ------------------------------------------------------------------------- *) 1731 1732local 1733 val reduce = rhs o concl o numLib.REDUCE_CONV 1734 1735 fun log2_of tm = 1736 case Lib.total numSyntax.dest_numeral (reduce tm) of 1737 SOME i => (Arbnum.log2 i handle Domain => raise ERR "log2_of" "zero") 1738 | NONE => raise ERR "num_to_2exp" "Not a number" 1739 1740 val SYM_BITS_THM = GSYM bitTheory.BITS_THM 1741 val SYM_BITS_ZERO3 = GSYM bitTheory.BITS_ZERO3 1742 val SYM_BITS_THM2 = GSYM bitTheory.BITS_THM2 1743 val MOD_DIMINDEX2 = REWRITE_RULE [dimword_def] MOD_DIMINDEX 1744 1745 fun err s = raise ERR "BITS_INTRO_CONV" s 1746 fun BITS_INTRO_CONV tm = 1747 (case Lib.total boolSyntax.dest_strip_comb tm of 1748 SOME ("arithmetic$MOD", [m, n]) => 1749 (case Lib.total boolSyntax.dest_strip_comb m of 1750 SOME ("arithmetic$DIV", [p, q]) => 1751 let 1752 val _ = not (numSyntax.is_numeral p) orelse err "" 1753 val l = log2_of q 1754 val h = numSyntax.mk_numeral 1755 (Arbnum.less1 (Arbnum.+(log2_of n, l))) 1756 in 1757 Thm.TRANS (numLib.REDUCE_CONV tm) 1758 (SYM_BITS_THM 1759 |> Drule.SPECL [h, numSyntax.mk_numeral l, p] 1760 |> Conv.CONV_RULE (Conv.LHS_CONV numLib.REDUCE_CONV)) 1761 end 1762 | _ => 1763 let 1764 val _ = not (numSyntax.is_numeral m) orelse err "" 1765 val h = numSyntax.mk_numeral (Arbnum.less1 (log2_of n)) 1766 in 1767 Thm.TRANS (numLib.REDUCE_CONV tm) 1768 (SYM_BITS_ZERO3 1769 |> Drule.SPECL [h, m] 1770 |> Conv.CONV_RULE (Conv.LHS_CONV numLib.REDUCE_CONV)) 1771 end) 1772 | SOME ("arithmetic$DIV", [m, n]) => 1773 (case Lib.total boolSyntax.dest_strip_comb m of 1774 SOME ("arithmetic$MOD", [p, q]) => 1775 let 1776 val _ = not (numSyntax.is_numeral p) orelse err "" 1777 val l = numSyntax.mk_numeral (log2_of n) 1778 val h = numSyntax.mk_numeral (Arbnum.less1 (log2_of q)) 1779 in 1780 Thm.TRANS (numLib.REDUCE_CONV tm) 1781 (SYM_BITS_THM2 1782 |> Drule.SPECL [h, l, p] 1783 |> Conv.CONV_RULE (Conv.LHS_CONV numLib.REDUCE_CONV)) 1784 end 1785 | _ => err "Could not convert to BITS") 1786 | _ => err "Could not convert to BITS") 1787 handle HOL_ERR _ => err "Could not convert to BITS" 1788in 1789 val BITS_INTRO_CONV = 1790 PURE_REWRITE_CONV [MOD_DIMINDEX, MOD_DIMINDEX2, SYM_BITS_THM, 1791 SYM_BITS_ZERO3, SYM_BITS_THM2] 1792 THENC TOP_DEPTH_CONV BITS_INTRO_CONV 1793end 1794 1795val BITS_INTRO_ss = 1796 simpLib.name_ss "BITS_INTRO" 1797 (simpLib.std_conv_ss 1798 {name = "BITS_INTRO_CONV", 1799 pats = [``a MOD b``, ``(a MOD b) DIV c``], 1800 conv = BITS_INTRO_CONV}) 1801 1802(* WORD_BIT_INDEX_CONV true: convert ``word_bit i w`` to ``w ' i`` 1803 WORD_BIT_INDEX_CONV false: convert ``w ' i`` to ``word_bit i w`` *) 1804 1805fun WORD_BIT_INDEX_CONV toindex = 1806 let 1807 val (dest, thm) = 1808 if toindex 1809 then (wordsSyntax.dest_word_bit, Conv.GSYM wordsTheory.word_bit) 1810 else (Lib.swap o fcpSyntax.dest_fcp_index, wordsTheory.word_bit) 1811 in 1812 fn tm => 1813 let 1814 val (b, w) = dest tm 1815 val lt = 1816 (b, fcpSyntax.mk_dimindex (wordsSyntax.dim_of w)) 1817 |> numSyntax.mk_less 1818 |> (Conv.RAND_CONV SIZES_CONV THENC numLib.REDUCE_CONV) 1819 |> Drule.EQT_ELIM 1820 in 1821 Drule.ISPEC w (Drule.MATCH_MP thm lt) 1822 end 1823 handle HOL_ERR {origin_function = "EQT_ELIM", ...} => 1824 raise ERR "WORD_BIT_INDEX_CONV" "index too large" 1825 end 1826 1827(* ------------------------------------------------------------------------- *) 1828 1829local 1830 val n2w_LOWER_ss = 1831 rewrites 1832 ([n2w_BITS, n2w_sub, n2w_sub_eq_0] @ 1833 List.map GSYM 1834 [wordsTheory.word_add_n2w, 1835 wordsTheory.word_mul_n2w, 1836 wordsTheory.w2w_def, 1837 wordsTheory.w2w_id]) 1838 1839 fun num_lt tm = 1840 case Lib.total boolSyntax.dest_strip_comb tm 1841 of SOME ("arithmetic$MOD", [m, n]) => 1842 (case Lib.total numSyntax.dest_numeral n 1843 of SOME i => 1844 if Arbnum.< (Arbnum.zero, i) then 1845 [Thm.MP 1846 (Drule.SPECL [m, n] arithmeticTheory.MOD_LESS) 1847 (numLib.DECIDE (numSyntax.mk_less (numSyntax.zero_tm, n)))] 1848 else 1849 [] 1850 | NONE => []) 1851 | SOME ("bit$BITS", [h, l, n]) => 1852 if numSyntax.is_numeral h then 1853 if numSyntax.is_numeral l then 1854 [Conv.CONV_RULE (Conv.RAND_CONV numLib.REDUCE_CONV) 1855 (Drule.SPECL [h, l, n] bitTheory.BITSLT_THM)] 1856 else 1857 [Conv.CONV_RULE (Conv.RAND_CONV numLib.REDUCE_CONV) 1858 (Drule.SPECL [h, l, n] BITSLT_THM2)] 1859 else 1860 [] 1861 | SOME ("words$w2n", [w]) => 1862 if Lib.can fcpSyntax.dest_numeric_type (wordsSyntax.dim_of w) then 1863 [Conv.CONV_RULE (Conv.RAND_CONV SIZES_CONV) 1864 (Drule.ISPEC w wordsTheory.w2n_lt)] 1865 else 1866 [] 1867 | SOME ("arithmetic$+", [a, b]) => num_lt a @ num_lt b 1868 | SOME ("arithmetic$-", [a, b]) => num_lt a @ num_lt b 1869 | SOME ("arithmetic$*", [a, b]) => num_lt a @ num_lt b 1870 | SOME ("arithmetic$DIV", [a, b]) => num_lt a 1871 | _ => [] 1872 1873 fun LT_THMS_TAC tm = 1874 case Lib.total num_lt tm 1875 of SOME thms => MAP_EVERY ASSUME_TAC thms 1876 | NONE => ALL_TAC 1877 1878 val word_eq_imp_num_eq = Q.prove( 1879 `!m n. (n2w m = n2w n : 'a word) /\ 1880 m < dimword(:'a) /\ 1881 n < dimword(:'a) ==> (m = n)`, 1882 SRW_TAC [] [] THEN FULL_SIMP_TAC arith_ss []) 1883 1884 val word_lt_imp_num_lt = Q.prove( 1885 `!m n. (n2w m) <+ (n2w n : 'a word) /\ 1886 m < dimword(:'a) /\ 1887 n < dimword(:'a) ==> (m < n)`, 1888 SRW_TAC [] [word_lo_n2w] THEN FULL_SIMP_TAC arith_ss []) 1889 1890 val word_ls_imp_num_ls = Q.prove( 1891 `!m n. (n2w m) <=+ (n2w n : 'a word) /\ 1892 m < dimword(:'a) /\ 1893 n < dimword(:'a) ==> (m <= n)`, 1894 SRW_TAC [] [word_ls_n2w] THEN FULL_SIMP_TAC arith_ss []) 1895 1896 fun get_intro_thm tm = 1897 case Lib.total boolSyntax.dest_strip_comb tm 1898 of SOME ("min$=", [l, r]) => SOME (word_eq_imp_num_eq, l, r) 1899 | SOME ("prim_rec$<", [l, r]) => SOME (word_lt_imp_num_lt, l, r) 1900 | SOME ("arithmetic$<=", [l, r]) => SOME (word_ls_imp_num_ls, l, r) 1901 | _ => NONE 1902 1903 val n2w_INTRO: int -> tactic = 1904 fn sz => fn (asl, g) => 1905 case get_intro_thm g 1906 of SOME (intro_thm, l, r) => 1907 let 1908 val typ = fcpSyntax.mk_int_numeric_type sz 1909 val sz_thm = SIZES_CONV (wordsSyntax.mk_dimword typ) 1910 val sz = rhs (concl sz_thm) 1911 val l_lt = numSyntax.mk_less (l, sz) 1912 val r_lt = numSyntax.mk_less (r, sz) 1913 in 1914 (Tactic.MATCH_MP_TAC 1915 (Drule.SPECL [l, r] 1916 (Thm.INST_TYPE [Type.alpha |-> typ] intro_thm)) 1917 THEN LT_THMS_TAC l 1918 THEN LT_THMS_TAC r 1919 THEN Tactical.SUBGOAL_THEN l_lt 1920 (fn thm => REWRITE_TAC [thm, sz_thm]) 1921 THENL [ 1922 bossLib.ASM_SIMP_TAC arith_ss [], 1923 Tactical.SUBGOAL_THEN r_lt (fn thm => REWRITE_TAC [thm]) 1924 THENL [ 1925 bossLib.ASM_SIMP_TAC arith_ss [], 1926 bossLib.ASM_SIMP_TAC (arith_ss++SIZES_ss++n2w_LOWER_ss) [] 1927 ] 1928 ]) (asl, g) 1929 end 1930 | NONE => FAIL_TAC "Unsuitable goal" (asl, g) 1931in 1932 fun n2w_INTRO_TAC sz = 1933 SIMP_TAC (arith_ss++BITS_INTRO_ss) [] THEN n2w_INTRO sz 1934end 1935 1936(* ------------------------------------------------------------------------- *) 1937 1938val LESS_THM = numLib.SUC_RULE prim_recTheory.LESS_THM 1939 1940val LESS_COR = 1941 [``(prim_rec$< m (arithmetic$NUMERAL (arithmetic$BIT1 n))) ==> (P:bool)``, 1942 ``(prim_rec$< m (arithmetic$NUMERAL (arithmetic$BIT2 n))) ==> (P:bool)``] 1943 |> map (GEN_ALL o REWRITE_CONV [LESS_THM, DISJ_IMP_THM]) |> LIST_CONJ 1944 1945local 1946 val word_n2w_le = Q.prove( 1947 `!a. w2n (n2w a :'a word) <= a MOD dimword(:'a)`, 1948 SIMP_TAC std_ss [w2n_n2w]) 1949 1950 val word_n2w_le2 = Q.prove( 1951 `!a. w2n (n2w a :'a word) <= a`, 1952 SIMP_TAC std_ss [w2n_n2w, bitTheory.MOD_LEQ, ZERO_LT_dimword]) 1953 1954 val word_extract_le = Q.prove( 1955 `!a:'a word h l. w2n ((h >< l) a : 'b word) <= w2n a`, 1956 Cases THEN SRW_TAC [] [word_extract_n2w] 1957 THEN SRW_TAC [] [bitTheory.BITS_COMP_THM2, MOD_DIMINDEX] 1958 THEN SRW_TAC [] [arithmeticTheory.MIN_DEF, bitTheory.BITS_LEQ]) 1959 1960 val word_add_le = Q.prove( 1961 `!a:'a word b. w2n (a + b) <= w2n a + w2n b`, 1962 Cases THEN Cases 1963 THEN SIMP_TAC std_ss [bitTheory.MOD_LEQ, word_add_def, w2n_n2w, 1964 ZERO_LT_dimword]) 1965 1966 val word_mul_le = Q.prove( 1967 `!a:'a word b. w2n (a * b) <= w2n a * w2n b`, 1968 Cases THEN Cases 1969 THEN SIMP_TAC std_ss [bitTheory.MOD_LEQ, word_mul_def, w2n_n2w, 1970 ZERO_LT_dimword]) 1971 1972 val word_lsl_le = Q.prove( 1973 `!a:'a word b. w2n (a << b) <= w2n a * 2 ** b`, 1974 Cases THEN SRW_TAC [] [word_lsl_n2w, bitTheory.MOD_LEQ, ZERO_LT_dimword]) 1975 1976 val word_div_le = Q.prove( 1977 `!a:'a word b. 1978 0 < b MOD dimword (:'a) ==> 1979 w2n (a // n2w b) <= w2n a DIV b MOD dimword (:'a)`, 1980 Cases THEN STRIP_TAC 1981 THEN Cases_on `b MOD dimword (:'a) = 1` 1982 THENL 1983 [SRW_TAC [numSimps.ARITH_ss] [word_div_def, w2n_n2w], 1984 Cases_on `n = 0` 1985 THEN SRW_TAC [numSimps.ARITH_ss] [word_div_def, w2n_n2w, 1986 arithmeticTheory.ZERO_DIV, bitTheory.MOD_LEQ, ZERO_LT_dimword]]) 1987 1988 val word_div_le2_lem = Q.prove( 1989 `!n. 0 < (SUC (2 * n)) MOD dimword (:'a)`, 1990 SRW_TAC [] [arithmeticTheory.ADD1, bitTheory.MOD_PLUS_1, ZERO_LT_dimword, 1991 DECIDE ``0n < n = (n <> 0)``] 1992 THEN STRIP_ASSUME_TAC EXISTS_HB 1993 THEN ASM_SIMP_TAC arith_ss 1994 [arithmeticTheory.EXP, GSYM arithmeticTheory.MOD_COMMON_FACTOR, 1995 bitTheory.ZERO_LT_TWOEXP, dimword_def, GSYM arithmeticTheory.ADD1] 1996 THEN `ODD (SUC (2 * n MOD 2 ** m))` 1997 by (REWRITE_TAC [arithmeticTheory.ODD_EXISTS] 1998 THEN Q.EXISTS_TAC `n MOD 2 ** m` THEN REWRITE_TAC []) 1999 THEN RULE_ASSUM_TAC (SIMP_RULE std_ss 2000 [arithmeticTheory.ODD_EVEN, arithmeticTheory.EVEN_EXISTS]) 2001 THEN POP_ASSUM (Q.SPEC_THEN `2 ** m` ASSUME_TAC) 2002 THEN ASM_REWRITE_TAC []) 2003 2004 val word_div_le2 = Q.prove( 2005 `!a:'a word b. ODD b ==> w2n (a // n2w b) <= w2n a`, 2006 Cases THEN REPEAT STRIP_TAC 2007 THEN IMP_RES_TAC (CONJUNCT2 (SPEC_ALL arithmeticTheory.EVEN_ODD_EXISTS)) 2008 THEN POP_ASSUM SUBST1_TAC 2009 THEN SRW_TAC [numSimps.ARITH_ss] [word_div_def, w2n_n2w] 2010 THEN `n DIV SUC (2 * m) MOD dimword (:'a) <= n` 2011 by SIMP_TAC std_ss [arithmeticTheory.DIV_LESS_EQ, word_div_le2_lem] 2012 THEN SRW_TAC [numSimps.ARITH_ss] []) 2013 2014 val word_extract_order1 = Q.prove( 2015 `!a : 'a word b h l. w2n a < b ==> w2n ((h >< l) a : 'b word) < b`, 2016 REPEAT STRIP_TAC 2017 THEN Q.SPECL_THEN [`w2n ((h >< l) a : 'b word)`, `w2n a`] 2018 MATCH_MP_TAC arithmeticTheory.LESS_EQ_LESS_TRANS 2019 THEN ASM_REWRITE_TAC [word_extract_le]) 2020 2021 val word_extract_order2 = Q.prove( 2022 `!a : 'a word b h l. w2n a <= b ==> w2n ((h >< l) a : 'b word) <= b`, 2023 REPEAT STRIP_TAC 2024 THEN Q.SPECL_THEN [`w2n ((h >< l) a : 'b word)`, `w2n a`] 2025 MATCH_MP_TAC arithmeticTheory.LESS_EQ_TRANS 2026 THEN ASM_REWRITE_TAC [word_extract_le]) 2027 2028 val word_add_order1 = Q.prove( 2029 `!a : 'a word b m n. w2n a <= m /\ w2n b <= n ==> w2n (a + b) <= m + n`, 2030 REPEAT STRIP_TAC 2031 THEN `w2n a + w2n b <= m + n` by DECIDE_TAC 2032 THEN Q.SPECL_THEN [`w2n (a + b)`, `w2n a + w2n b`] 2033 MATCH_MP_TAC arithmeticTheory.LESS_EQ_TRANS 2034 THEN ASM_REWRITE_TAC [word_add_le]) 2035 2036 val word_add_order2 = Q.prove( 2037 `!a : 'a word b m n. w2n a <= m /\ w2n b < n ==> w2n (a + b) < m + n`, 2038 REPEAT STRIP_TAC 2039 THEN `w2n a + w2n b < m + n` by DECIDE_TAC 2040 THEN Q.SPECL_THEN [`w2n (a + b)`, `w2n a + w2n b`] 2041 MATCH_MP_TAC arithmeticTheory.LESS_EQ_LESS_TRANS 2042 THEN ASM_REWRITE_TAC [word_add_le]) 2043 2044 val word_add_order3 = Q.prove( 2045 `!a : 'a word b m n. w2n a < m /\ w2n b <= n ==> w2n (a + b) < m + n`, 2046 REPEAT STRIP_TAC 2047 THEN `w2n a + w2n b < m + n` by DECIDE_TAC 2048 THEN Q.SPECL_THEN [`w2n (a + b)`, `w2n a + w2n b`] 2049 MATCH_MP_TAC arithmeticTheory.LESS_EQ_LESS_TRANS 2050 THEN ASM_REWRITE_TAC [word_add_le]) 2051 2052 val word_add_order4 = Q.prove( 2053 `!a : 'a word b m n. w2n a < m /\ w2n b < n ==> w2n (a + b) < m + n - 1`, 2054 REPEAT STRIP_TAC 2055 THEN `w2n a + w2n b < m + n - 1` by DECIDE_TAC 2056 THEN Q.SPECL_THEN [`w2n (a + b)`, `w2n a + w2n b`] 2057 MATCH_MP_TAC arithmeticTheory.LESS_EQ_LESS_TRANS 2058 THEN ASM_REWRITE_TAC [word_add_le]) 2059 2060 val word_mul_order1 = Q.prove( 2061 `!a : 'a word b m n. w2n a <= m /\ w2n b <= n ==> w2n (a * b) <= m * n`, 2062 REPEAT STRIP_TAC 2063 THEN `w2n a * w2n b <= m * n` 2064 by ASM_SIMP_TAC std_ss [arithmeticTheory.LESS_MONO_MULT2] 2065 THEN Q.SPECL_THEN [`w2n (a * b)`, `w2n a * w2n b`] 2066 MATCH_MP_TAC arithmeticTheory.LESS_EQ_TRANS 2067 THEN ASM_REWRITE_TAC [word_mul_le]) 2068 2069 val word_mul_order2 = Q.prove( 2070 `!a : 'a word b m n. w2n a <= m /\ w2n b < n ==> w2n (a * b) <= m * n`, 2071 REPEAT STRIP_TAC 2072 THEN `w2n a * w2n b <= m * n` 2073 by ASM_SIMP_TAC arith_ss [arithmeticTheory.LESS_MONO_MULT2] 2074 THEN Q.SPECL_THEN [`w2n (a * b)`, `w2n a * w2n b`] 2075 MATCH_MP_TAC arithmeticTheory.LESS_EQ_TRANS 2076 THEN ASM_SIMP_TAC arith_ss [word_mul_le]) 2077 2078 val word_mul_order3 = Q.prove( 2079 `!a : 'a word b m n. w2n a < m /\ w2n b <= n ==> w2n (a * b) <= m * n`, 2080 REPEAT STRIP_TAC 2081 THEN `w2n a * w2n b <= m * n` 2082 by ASM_SIMP_TAC arith_ss [arithmeticTheory.LESS_MONO_MULT2] 2083 THEN Q.SPECL_THEN [`w2n (a * b)`, `w2n a * w2n b`] 2084 MATCH_MP_TAC arithmeticTheory.LESS_EQ_TRANS 2085 THEN ASM_SIMP_TAC arith_ss [word_mul_le]) 2086 2087 val word_mul_order4 = Q.prove( 2088 `!a : 'a word b m n. w2n a < m /\ w2n b < n ==> w2n (a * b) <= m * n`, 2089 REPEAT STRIP_TAC 2090 THEN `w2n a * w2n b <= m * n` 2091 by ASM_SIMP_TAC arith_ss [arithmeticTheory.LESS_MONO_MULT2] 2092 THEN Q.SPECL_THEN [`w2n (a * b)`, `w2n a * w2n b`] 2093 MATCH_MP_TAC arithmeticTheory.LESS_EQ_TRANS 2094 THEN ASM_SIMP_TAC arith_ss [word_mul_le]) 2095 2096 val word_lsl_order1 = Q.prove( 2097 `!a:'a word b n. w2n a < n ==> w2n (a << b) < n * 2 ** b`, 2098 REPEAT STRIP_TAC 2099 THEN Q.SPECL_THEN [`w2n (a << b)`, `w2n a * 2 ** b`] 2100 MATCH_MP_TAC arithmeticTheory.LESS_EQ_LESS_TRANS 2101 THEN ASM_REWRITE_TAC [arithmeticTheory.LT_MULT_RCANCEL, 2102 bitTheory.ZERO_LT_TWOEXP, word_lsl_le]) 2103 2104 val word_lsl_order2 = Q.prove( 2105 `!a:'a word b n. w2n a <= n ==> w2n (a << b) <= n * 2 ** b`, 2106 REPEAT STRIP_TAC 2107 THEN Q.SPECL_THEN [`w2n (a << b)`, `w2n a * 2 ** b`] 2108 MATCH_MP_TAC arithmeticTheory.LESS_EQ_TRANS 2109 THEN ASM_REWRITE_TAC [arithmeticTheory.LE_MULT_RCANCEL, 2110 bitTheory.ZERO_LT_TWOEXP, word_lsl_le]) 2111 2112 val word_div_order_lem = 2113 word_div_le |> SPEC_ALL 2114 |> Q.DISCH `b < dimword (:'a)` 2115 |> SIMP_RULE arith_ss [] 2116 2117 val word_div_order1 = Q.prove( 2118 `!a:'a word b n. 2119 0 < b /\ b < dimword (:'a) /\ w2n a <= n ==> 2120 w2n (a // n2w b) <= n DIV b`, 2121 REPEAT STRIP_TAC 2122 THEN Q.SPECL_THEN [`w2n (a // n2w b)`, `w2n a DIV b MOD dimword (:'a)`] 2123 MATCH_MP_TAC arithmeticTheory.LESS_EQ_TRANS 2124 THEN ASM_SIMP_TAC arith_ss [arithmeticTheory.DIV_LE_MONOTONE, 2125 word_div_order_lem]) 2126 2127 val word_div_order2 = Q.prove( 2128 `!a:'a word b n. 2129 0 < b /\ b < dimword (:'a) /\ w2n a < n ==> 2130 w2n (a // n2w b) <= n DIV b`, 2131 REPEAT STRIP_TAC 2132 THEN Q.SPECL_THEN [`w2n (a // n2w b)`, `w2n a DIV b MOD dimword (:'a)`] 2133 MATCH_MP_TAC arithmeticTheory.LESS_EQ_TRANS 2134 THEN ASM_SIMP_TAC arith_ss [arithmeticTheory.DIV_LE_MONOTONE, 2135 word_div_order_lem]) 2136 2137 val word_div_order3 = Q.prove( 2138 `!a:'a word b n. 2139 ODD b /\ w2n a <= n ==> w2n (a // n2w b) <= n`, 2140 REPEAT STRIP_TAC 2141 THEN Q.SPECL_THEN [`w2n (a // n2w b)`, `w2n a`] 2142 MATCH_MP_TAC arithmeticTheory.LESS_EQ_TRANS 2143 THEN ASM_SIMP_TAC std_ss [word_div_le2]) 2144 2145 val word_div_order4 = Q.prove( 2146 `!a:'a word b n. 2147 ODD b /\ w2n a < n ==> w2n (a // n2w b) < n`, 2148 REPEAT STRIP_TAC 2149 THEN Q.SPECL_THEN [`w2n (a // n2w b)`, `w2n a`] 2150 MATCH_MP_TAC arithmeticTheory.LESS_EQ_LESS_TRANS 2151 THEN ASM_SIMP_TAC std_ss [word_div_le2]) 2152 2153 val word_type = wordsSyntax.dest_word_type o type_of 2154 val arb_thm = boolSyntax.arb |> Term.inst [alpha |-> bool] |> ASSUME 2155 val SIZE_RULE = CONV_RULE (DEPTH_CONV SIZES_CONV) 2156 val RAND_REDUCE_RULE = CONV_RULE (RAND_CONV numLib.REDUCE_CONV) 2157 2158 datatype bound = LE_BOUND of Arbnum.num 2159 | LT_BOUND of Arbnum.num 2160 | NO_BOUND 2161 2162 fun bnd thm = let val tm = concl thm in 2163 case Lib.total numSyntax.dest_less tm 2164 of SOME (_, n) => 2165 (case Lib.total numSyntax.dest_numeral n 2166 of SOME v => LT_BOUND v 2167 | NONE => NO_BOUND) 2168 | NONE => 2169 (case Lib.total numSyntax.dest_leq tm 2170 of SOME (_, n) => 2171 (case Lib.total numSyntax.dest_numeral n 2172 of SOME v => LE_BOUND v 2173 | NONE => NO_BOUND) 2174 | NONE => NO_BOUND) 2175 end 2176 2177 (* bounds for: + * n2w >< // << *) 2178 fun mk_bounds_thm t = let 2179 val w = wordsSyntax.dest_w2n t 2180 val thm1 = SIZE_RULE (Drule.ISPEC w w2n_lt) 2181 fun default () = case bnd thm1 2182 of LT_BOUND _ => thm1 2183 | _ => raise ERR "mk_bounds_thm" 2184 "can't compute bound" 2185 fun sub_bound x = mk_bounds_thm (wordsSyntax.mk_w2n x) 2186 handle HOL_ERR _ => arb_thm 2187 in 2188 case Lib.total boolSyntax.dest_strip_comb w 2189 of SOME ("words$word_extract", args as [h, l, a]) => let 2190 val thm2 = WORD_EXTRACT_LT 2191 |> Thm.INST_TYPE 2192 [alpha |-> word_type a, beta |-> word_type w] 2193 |> Drule.SPECL args 2194 |> RAND_REDUCE_RULE 2195 val thm3 = sub_bound a 2196 fun thm3_order th b = 2197 MATCH_MP 2198 (th |> Thm.INST_TYPE 2199 [alpha |-> word_type a, beta |-> word_type w] 2200 |> Drule.SPECL [a, numSyntax.mk_numeral b, h, l]) 2201 thm3 2202 val thm3_order1 = thm3_order word_extract_order1 2203 val thm3_order2 = thm3_order word_extract_order2 2204 in 2205 case (bnd thm1, bnd thm2, bnd thm3) 2206 of (LT_BOUND _, NO_BOUND, NO_BOUND) => thm1 2207 | (NO_BOUND, LT_BOUND _, NO_BOUND) => thm2 2208 | (NO_BOUND, NO_BOUND, LT_BOUND b1) => thm3_order1 b1 2209 | (NO_BOUND, NO_BOUND, LE_BOUND b1) => thm3_order2 b1 2210 | (LT_BOUND b1, LT_BOUND b2, NO_BOUND) => 2211 if Arbnum.<= (b1, b2) then thm1 else thm2 2212 | (LT_BOUND b1, NO_BOUND, LT_BOUND b2) => 2213 if Arbnum.<= (b1, b2) then thm1 else thm3_order1 b2 2214 | (NO_BOUND, LT_BOUND b1, LT_BOUND b2) => 2215 if Arbnum.<= (b1, b2) then thm2 else thm3_order1 b2 2216 | (LT_BOUND b1, NO_BOUND, LE_BOUND b2) => 2217 if Arbnum.<= (b1, Arbnum.plus1 b2) then 2218 thm1 2219 else 2220 thm3_order2 b2 2221 | (NO_BOUND, LT_BOUND b1, LE_BOUND b2) => 2222 if Arbnum.<= (b1, Arbnum.plus1 b2) then 2223 thm2 2224 else 2225 thm3_order2 b2 2226 | (LT_BOUND b1, LT_BOUND b2, LT_BOUND b3) => 2227 if Arbnum.<= (b1, b2) then 2228 if Arbnum.<= (b1, b3) then thm1 else thm3_order1 b3 2229 else 2230 if Arbnum.<= (b2, b3) then thm2 else thm3_order1 b3 2231 | (LT_BOUND b1, LT_BOUND b2, LE_BOUND b3) => 2232 if Arbnum.<= (b1, b2) then 2233 if Arbnum.<= (b1, Arbnum.plus1 b3) then 2234 thm1 2235 else 2236 thm3_order1 b3 2237 else 2238 if Arbnum.<= (b2, Arbnum.plus1 b3) then 2239 thm2 2240 else 2241 thm3_order1 b3 2242 | _ => raise ERR "mk_bounds_thm" "can't compute bound" 2243 end 2244 | SOME ("words$n2w", [n]) => let 2245 val thm2 = if is_known_word_size w then 2246 word_n2w_le 2247 |> Thm.SPEC n 2248 |> Thm.INST_TYPE 2249 [alpha |-> wordsSyntax.dim_of w] 2250 |> SIZE_RULE 2251 |> numLib.REDUCE_RULE 2252 else 2253 word_n2w_le2 |> Thm.SPEC n 2254 in 2255 case (bnd thm1, bnd thm2) 2256 of (LT_BOUND _, NO_BOUND) => thm1 2257 | (NO_BOUND, LE_BOUND _) => thm2 2258 | (LT_BOUND b1, LE_BOUND b2) => 2259 if Arbnum.<= (b1, Arbnum.plus1 b2) then thm1 else thm2 2260 | _ => raise ERR "mk_bounds_thm" "can't compute bound" 2261 end 2262 | SOME ("words$word_add", [a, b]) => let 2263 val thm2 = sub_bound a 2264 fun f th thm3 = MATCH_MP th (CONJ thm2 thm3) 2265 |> RAND_REDUCE_RULE 2266 in 2267 case (bnd thm1, bnd thm2) 2268 of (LT_BOUND _, NO_BOUND) => thm1 2269 | (NO_BOUND, LT_BOUND _) => 2270 let val thm3 = sub_bound b in 2271 case bnd thm3 2272 of LT_BOUND _ => f word_add_order4 thm3 2273 | LE_BOUND _ => f word_add_order3 thm3 2274 | NO_BOUND => 2275 raise ERR "mk_bounds_thm" "can't compute bound" 2276 end 2277 | (NO_BOUND, LE_BOUND _) => 2278 let val thm3 = sub_bound b in 2279 case bnd thm3 2280 of LT_BOUND _ => f word_add_order2 thm3 2281 | LE_BOUND _ => f word_add_order1 thm3 2282 | NO_BOUND => 2283 raise ERR "mk_bounds_thm" "can't compute bound" 2284 end 2285 | (LT_BOUND b1, LT_BOUND b2) => 2286 if Arbnum.<= (b1, b2) then 2287 thm1 2288 else let val thm3 = sub_bound b in 2289 case bnd thm3 2290 of LT_BOUND b3 => 2291 if Arbnum.< (b1, Arbnum.+(b2, b3)) then 2292 thm1 2293 else 2294 f word_add_order4 thm3 2295 | LE_BOUND b3 => 2296 if Arbnum.<= (b1, Arbnum.+(b2, b3)) then 2297 thm1 2298 else 2299 f word_add_order3 thm3 2300 | NO_BOUND => 2301 raise ERR "mk_bounds_thm" "can't compute bound" 2302 end 2303 | (LT_BOUND b1, LE_BOUND b2) => 2304 if Arbnum.<= (b1, Arbnum.plus1 b2) then 2305 thm1 2306 else let val thm3 = sub_bound b in 2307 case bnd thm3 2308 of LT_BOUND b3 => 2309 if Arbnum.<= (b1, Arbnum.+(b2, b3)) then 2310 thm1 2311 else 2312 f word_add_order2 thm3 2313 | LE_BOUND b3 => 2314 if Arbnum.<= (b1, Arbnum.+(b2, b3)) then 2315 thm1 2316 else 2317 f word_add_order1 thm3 2318 | NO_BOUND => 2319 raise ERR "mk_bounds_thm" "can't compute bound" 2320 end 2321 | _ => raise ERR "mk_bounds_thm" "can't compute bound" 2322 end 2323 | SOME ("words$word_mul", [a, b]) => let 2324 val thm2 = sub_bound a 2325 in 2326 case bnd thm2 2327 of LT_BOUND b2 => let 2328 val thm3 = sub_bound b 2329 fun f th = MATCH_MP th (CONJ thm2 thm3) 2330 |> RAND_REDUCE_RULE 2331 in 2332 case (bnd thm1, bnd thm3) 2333 of (NO_BOUND, LT_BOUND b3) => f word_mul_order4 2334 | (NO_BOUND, LE_BOUND b3) => f word_mul_order3 2335 | (LT_BOUND b1, LT_BOUND b3) => 2336 if Arbnum.<= (b1, Arbnum.plus1 (Arbnum.*(b2, b3))) 2337 then thm1 else f word_mul_order4 2338 | (LT_BOUND b1, LE_BOUND b3) => 2339 if Arbnum.<= (b1, Arbnum.plus1 (Arbnum.*(b2, b3))) 2340 then thm1 else f word_mul_order3 2341 | (LT_BOUND _, NO_BOUND) => thm1 2342 | _ => raise ERR "mk_bounds_thm" "can't compute bound" 2343 end 2344 | LE_BOUND b2 => let 2345 val thm3 = sub_bound b 2346 fun f th = MATCH_MP th (CONJ thm2 thm3) 2347 |> RAND_REDUCE_RULE 2348 in 2349 case (bnd thm1, bnd thm3) 2350 of (NO_BOUND, LT_BOUND b3) => f word_mul_order2 2351 | (NO_BOUND, LE_BOUND b3) => f word_mul_order1 2352 | (LT_BOUND b1, LT_BOUND b3) => 2353 if Arbnum.<= (b1, Arbnum.plus1 (Arbnum.*(b2, b3))) 2354 then thm1 else f word_mul_order2 2355 | (LT_BOUND b1, LE_BOUND b3) => 2356 if Arbnum.<= (b1, Arbnum.plus1 (Arbnum.*(b2, b3))) 2357 then thm1 else f word_mul_order1 2358 | (LT_BOUND _, NO_BOUND) => thm1 2359 | _ => raise ERR "mk_bounds_thm" "can't compute bound" 2360 end 2361 | NO_BOUND => default () 2362 end 2363 | SOME ("words$word_lsl", args as [a, b]) => 2364 (case Lib.total numLib.dest_numeral b 2365 of SOME v => let 2366 val thm2 = sub_bound a 2367 fun f b = Arbnum.*(b, Arbnum.pow (Arbnum.two, v)) 2368 fun g thm = MATCH_MP (Drule.ISPECL args thm) thm2 2369 |> RAND_REDUCE_RULE 2370 in 2371 case (bnd thm1, bnd thm2) 2372 of (NO_BOUND, LT_BOUND _) => g word_lsl_order1 2373 | (NO_BOUND, LE_BOUND _) => g word_lsl_order2 2374 | (LT_BOUND b1, LT_BOUND b2) => 2375 if Arbnum.<= (b1, f b2) then 2376 thm1 2377 else 2378 g word_lsl_order1 2379 | (LT_BOUND b1, LE_BOUND b2) => 2380 if Arbnum.<= (b1, Arbnum.plus1 (f b2)) then 2381 thm1 2382 else 2383 g word_lsl_order2 2384 | _ => raise ERR "mk_bounds_thm" "can't compute bound" 2385 end 2386 | NONE => default ()) 2387 | SOME ("words$word_div", [a, b]) => 2388 (case Lib.total wordsSyntax.dest_n2w b 2389 of SOME (n, ty) => 2390 (case (Lib.total numLib.dest_numeral n, 2391 Lib.total fcpLib.index_to_num ty) 2392 of (SOME v, SOME w) => 2393 if v = Arbnum.zero orelse 2394 Arbnum.>= (v, Arbnum.pow (Arbnum.two, w)) 2395 then 2396 default () 2397 else let 2398 val thm2 = sub_bound a 2399 fun thm3 () = 2400 numSyntax.mk_less (numSyntax.zero_tm, n) 2401 |> bossLib.DECIDE 2402 fun thm4 () = numSyntax.mk_less (n, 2403 wordsSyntax.mk_dimword ty) 2404 |> WORD_EVAL_CONV 2405 |> EQT_ELIM 2406 fun g thm = MATCH_MP (Drule.ISPECL [a, n] thm) 2407 (LIST_CONJ [thm3 (), thm4 (), thm2]) 2408 |> RAND_REDUCE_RULE 2409 in 2410 case bnd thm2 2411 of LT_BOUND _ => g word_div_order2 2412 | LE_BOUND _ => g word_div_order1 2413 | _ => raise ERR "mk_bounds_thm" 2414 "can't compute bound" 2415 end 2416 | (SOME v, NONE) => 2417 if Arbnum.mod2 v = Arbnum.zero then 2418 raise ERR "mk_bounds_thm" "can't compute bound" 2419 else let 2420 val thm2 = sub_bound a 2421 fun thm3 () = numSyntax.mk_odd n 2422 |> numLib.REDUCE_CONV 2423 |> EQT_ELIM 2424 fun g thm = MATCH_MP (Drule.ISPECL [a, n] thm) 2425 (CONJ (thm3 ()) thm2) 2426 in 2427 case bnd thm2 2428 of LT_BOUND _ => g word_div_order4 2429 | LE_BOUND _ => g word_div_order3 2430 | _ => raise ERR "mk_bounds_thm" 2431 "can't compute bound" 2432 end 2433 | _ => default ()) 2434 | NONE => default ()) 2435 | _ => default () 2436 end 2437in 2438 fun mk_bounds_thms t = 2439 let val l = t |> find_terms wordsSyntax.is_w2n 2440 |> Lib.mk_set 2441 |> Lib.mapfilter mk_bounds_thm 2442 in 2443 if null l then 2444 TRUTH 2445 else 2446 LIST_CONJ l 2447 end 2448end 2449 2450val EXISTS_NUMBER = Q.prove( 2451 `!P. (?w:'a word. P (words$w2n w)) = (?n. n < words$dimword(:'a) /\ P n)`, 2452 STRIP_TAC THEN EQ_TAC THEN SRW_TAC [] [] 2453 THENL [Q.EXISTS_TAC `words$w2n w`, Q.EXISTS_TAC `words$n2w n`] 2454 THEN ASM_SIMP_TAC std_ss [w2n_lt, w2n_n2w]) 2455 2456fun EXISTS_WORD_CONV t = 2457 if is_exists t then 2458 let val v = fst (dest_exists t) in 2459 if wordsSyntax.is_word_type (type_of v) then 2460 (UNBETA_CONV v THENC SIMP_CONV (std_ss++SIZES_ss) [EXISTS_NUMBER]) t 2461 else 2462 raise ERR "EXISTS_WORD_CONV" "Not an \"exists word\" term." 2463 end 2464 else 2465 raise ERR "EXISTS_WORD_CONV" "Not an exists term." 2466 2467local 2468 val word_join = SIMP_RULE (std_ss++boolSimps.LET_ss) [] word_join_def 2469 val rw = [word_0, word_T, word_L, word_xor_def, word_or_def, word_and_def, 2470 word_1comp_def, REWRITE_RULE [SYM_WORD_NEG_1] word_T, 2471 pred_setTheory.NOT_IN_EMPTY, 2472 Q.ISPEC `0n` pred_setTheory.IN_INSERT, 2473 Q.ISPEC `^Na` pred_setTheory.IN_INSERT, 2474 fcpTheory.FCP_UPDATE_def, LESS_COR, sw2sw, w2w, word_replicate_def, 2475 word_join, word_concat_def, word_reverse_def, word_modify_def, 2476 word_lsl_def, word_lsr_def, word_asr_def, word_ror_def, 2477 word_rol_def, word_rrx_def, word_msb_def, word_lsb_def, 2478 word_extract_def, word_bits_def, word_slice_def, word_bit_def, 2479 word_signed_bits_def, 2480 ``(if b then x:'a word else y) ' i = if b then x ' i else y ' i`` 2481 |> simpLib.SIMP_PROVE std_ss [COND_RAND, COND_RATOR] |> GEN_ALL] 2482 val thms = [WORD_ADD_LEFT_LO, WORD_ADD_LEFT_LS, 2483 WORD_ADD_RIGHT_LS, WORD_ADD_RIGHT_LO] 2484 val thms2 = map (GEN_ALL o Q.SPEC `^n2w n`) 2485 [WORD_ADD_LEFT_LO2, WORD_ADD_LEFT_LS2, 2486 WORD_ADD_RIGHT_LO2, WORD_ADD_RIGHT_LS2] 2487 val rw3 = [WORD_LT_LO, WORD_LE_LS, WORD_GREATER, WORD_GREATER_EQ, 2488 CONV_RULE WORD_ARITH_CONV WORD_LS_T, 2489 CONV_RULE WORD_ARITH_CONV WORD_LESS_EQ_H] @ 2490 map (Q.SPECL [`^n2w m`, `^n2w n`]) thms @ 2491 thms2 @ map (ONCE_REWRITE_RULE [WORD_ADD_COMM]) thms2 2492 val rw4 = [Q.SPECL [`w:'a word`, `^n2w m`, `^n2w n`] WORD_ADD_EQ_SUB, 2493 Q.SPECL [`w:'a word`, `words$word_2comp (^n2w m)`, `^n2w n`] 2494 WORD_ADD_EQ_SUB, 2495 REWRITE_RULE [GSYM w2n_11, word_0_n2w] NOT_INT_MIN_ZERO, 2496 REWRITE_RULE [WORD_LO, word_0_n2w] ZERO_LO_INT_MIN, 2497 WORD_LO, WORD_LS, WORD_HI, WORD_HS, GSYM w2n_11] 2498 val UINT_MAX_CONV = 2499 let 2500 val cnv = 2501 Conv.CHANGED_CONV 2502 (PURE_REWRITE_CONV [UINT_MAX_def, word_T_def, WORD_NEG_1, w2n_n2w] 2503 THENC Conv.DEPTH_CONV SIZES_CONV 2504 THENC numLib.REDUCE_CONV) 2505 in 2506 fn t => 2507 if is_known_word_size t 2508 then cnv t 2509 else raise ERR "UINT_MAX_CONV" "Not of known size" 2510 end 2511 val UINT_MAX_ss = 2512 simpLib.std_conv_ss 2513 {conv = UINT_MAX_CONV, 2514 name = "UINT_MAX_CONV", 2515 pats = [``words$word_2comp 1w :'a word``, ``words$word_T :'a word``]} 2516 val DECIDE_CONV = EQT_INTRO o DECIDE 2517 fun EQ_CONV t = (if term_eq T t orelse term_eq F t then 2518 ALL_CONV else NO_CONV) t 2519 val trace_word_decide = ref 0 2520 val _ = Feedback.register_trace ("word decide", trace_word_decide, 1) 2521in 2522 val WORD_BIT_EQ_ss = 2523 simpLib.merge_ss 2524 [fcpLib.FCP_ss, SIZES_ss, simpLib.rewrites rw, 2525 simpLib.std_conv_ss 2526 {conv = CHANGED_CONV FORALL_AND_CONV, 2527 name = "FORALL_AND_CONV", 2528 pats = [``!x:'a. P /\ Q:bool``]}] 2529 fun WORD_BIT_EQ_CONV t = 2530 if is_eq t orelse wordsSyntax.is_index t then 2531 (SIMP_CONV (std_ss++WORD_BIT_EQ_ss++BIT_ss) [Q.SPEC `^Na` n2w_def] 2532 THENC TRY_CONV DECIDE_CONV) t 2533 else 2534 raise ERR "WORD_BIT_EQ_CONV" "Not a word equality" 2535 val WORD_BIT_EQ_ss = simpLib.named_merge_ss "word bit eq" 2536 [WORD_BIT_EQ_ss, numSimps.ARITH_ss] 2537 fun WORD_DP_PROVE dp t = 2538 let 2539 val thm1 = 2540 QCONV 2541 (WORD_CONV 2542 THENC 2543 SIMP_CONV (bool_ss++UINT_MAX_ss) rw3 2544 THENC 2545 SIMP_CONV (std_ss++boolSimps.LET_ss++UINT_MAX_ss++ 2546 WORD_w2n_ss++WORD_SUBTRACT_ss++WORD_ADD_ss) rw4 2547 THENC 2548 DEPTH_CONV EXISTS_WORD_CONV) t 2549 val t1 = rhs (concl thm1) 2550 val bnds = mk_bounds_thms t1 2551 val t2 = mk_imp (concl bnds, t1) 2552 val _ = if 0 < !trace_word_decide then 2553 (print ("Trying to prove:\n"); 2554 Parse.print_term t2; 2555 print "\n") 2556 else 2557 () 2558 val thm2 = dp t2 2559 val conv = RAND_CONV (PURE_ONCE_REWRITE_CONV [GSYM thm1]) 2560 in 2561 MP (CONV_RULE conv thm2) bnds 2562 end 2563 fun WORD_DP pre_conv dp tm = 2564 let 2565 fun conv t = 2566 if term_eq T t then 2567 ALL_CONV t 2568 else 2569 STRIP_QUANT_CONV (EQT_INTRO o (WORD_DP_PROVE dp)) t 2570 in 2571 EQT_ELIM 2572 ((pre_conv THENC DEPTH_CONV (WORD_BIT_EQ_CONV THENC EQ_CONV) 2573 THENC DEPTH_CONV (conv THENC EQ_CONV) 2574 THENC REWRITE_CONV []) tm) 2575 end handle UNCHANGED => raise ERR "WORD_DP" "Failed to prove goal" 2576 val WORD_ARITH_PROVE = WORD_DP WORD_ARITH_CONV DECIDE 2577 val WORD_DECIDE = WORD_DP WORD_CONV DECIDE 2578end 2579 2580fun is_word_term tm = 2581 let 2582 open numSyntax 2583 in 2584 if is_forall tm 2585 then is_word_term (#Body (Rsyntax.dest_forall tm)) 2586 else if is_exists tm 2587 then is_word_term (#Body (Rsyntax.dest_exists tm)) 2588 else if is_neg tm 2589 then is_word_term (dest_neg tm) 2590 else if is_conj tm orelse is_disj tm orelse is_imp tm 2591 then is_word_term (rand (rator tm)) andalso is_word_term (rand tm) 2592 else if is_eq tm 2593 then let 2594 val typ = type_of (rand tm) 2595 in 2596 (typ = num) orelse is_word_type typ 2597 end 2598 else is_less tm 2599 orelse is_leq tm 2600 orelse is_greater tm 2601 orelse is_geq tm 2602 orelse is_index tm 2603 orelse is_word_lt tm 2604 orelse is_word_le tm 2605 orelse is_word_gt tm 2606 orelse is_word_ge tm 2607 orelse is_word_hi tm 2608 orelse is_word_lo tm 2609 orelse is_word_hs tm 2610 orelse is_word_ls tm 2611 end 2612 2613fun MP_ASSUM_TAC tm (asl, w) = 2614 let 2615 val (ob, asl') = Lib.pluck (Lib.equal tm) asl 2616 in 2617 MP_TAC (Thm.ASSUME ob) (asl', w) 2618 end 2619 2620fun WORD_DECIDE_TAC (asl, w) = 2621 (EVERY (map MP_ASSUM_TAC (List.filter is_word_term asl)) 2622 THEN CONV_TAC (EQT_INTRO o WORD_DECIDE)) (asl, w) 2623 2624(* ------------------------------------------------------------------------- *) 2625 2626fun mk_word_size n = 2627 let 2628 val N = Arbnum.fromInt n 2629 val SN = Int.toString n 2630 val typ = fcpLib.index_type N 2631 val TYPE = mk_type ("cart", [bool, typ]) 2632 val dimindex = fcpLib.DIMINDEX N 2633 val finite = fcpLib.FINITE N 2634 fun save x = Feedback.trace ("Theory.save_thm_reporting", 0) save_thm x 2635 val _ = save ("dimindex_" ^ SN, dimindex) 2636 val _ = save ("finite_" ^ SN, finite) 2637 val INT_MIN = save ("INT_MIN_" ^ SN, 2638 (SIMP_RULE std_ss [dimindex] o 2639 Thm.INST_TYPE [``:'a`` |-> typ]) INT_MIN_def) 2640 val dimword = save ("dimword_" ^ SN, 2641 (SIMP_RULE std_ss [INT_MIN] o 2642 Thm.INST_TYPE [``:'a`` |-> typ]) dimword_IS_TWICE_INT_MIN) 2643 in 2644 type_abbrev ("word" ^ SN, TYPE) 2645 end 2646 2647val dest_word_literal = fst o wordsSyntax.dest_mod_word_literal 2648 2649(* ------------------------------------------------------------------------- *) 2650 2651val Cases_word = Cases 2652val Cases_on_word = Cases_on 2653 2654val LESS_CONV = computeLib.compset_conv (reduceLib.num_compset()) 2655 [computeLib.Defs [wordsTheory.NUMERAL_LESS_THM]] 2656 2657local 2658 val tac = 2659 POP_ASSUM 2660 (fn th => 2661 STRIP_ASSUME_TAC 2662 (CONV_RULE (DEPTH_CONV SIZES_CONV THENC LESS_CONV) th)) 2663 THEN POP_ASSUM SUBST_ALL_TAC 2664in 2665 val Cases_word_value = Cases THEN tac 2666 fun Cases_on_word_value t = Cases_on t THEN tac 2667end 2668 2669val Induct_word = 2670 recInduct WORD_INDUCT 2671 THEN CONJ_TAC 2672 THENL [ALL_TAC, 2673 CONV_TAC 2674 (QCONV 2675 (TRY_CONV 2676 (STRIP_QUANT_CONV (RATOR_CONV (DEPTH_CONV SIZES_CONV))))) 2677 THEN NTAC 3 STRIP_TAC] 2678 2679(* ------------------------------------------------------------------------- *) 2680 2681val word_pp_mode = ref 0 2682val word_cast_on = ref false 2683val int_word_pp = ref false 2684 2685local 2686 fun lsr (x, y) = 2687 if x = Arbnum.zero orelse y = Arbnum.zero 2688 then x 2689 else lsr (Arbnum.div2 x, Arbnum.less1 y) 2690 2691 fun int_word (v, m) = 2692 if !int_word_pp andalso m <> Arbnum.zero 2693 then let 2694 val top = lsr (v, Arbnum.less1 m) 2695 val neg = top = Arbnum.one 2696 val nv = 2697 if neg then Arbnum.- (Arbnum.pow (Arbnum.two, m), v) else v 2698 in 2699 (neg, nv) 2700 end 2701 else (false, v) 2702in 2703 fun print_word f Gs backend sys ppfns gravs d t = 2704 let 2705 open Portable term_pp_types smpp 2706 infix >> 2707 val {add_string=str, add_break=brk,...} = 2708 ppfns: term_pp_types.ppstream_funs 2709 val (n, x) = dest_n2w t 2710 val m = fcpLib.index_to_num x handle HOL_ERR _ => Arbnum.zero 2711 val v = numSyntax.dest_numeral n 2712 val (neg, v) = int_word (v, m) 2713 in 2714 (if !Globals.show_types orelse !word_cast_on 2715 then str "(" 2716 else nothing) 2717 >> (if neg then str "-" else nothing) 2718 >> str (f (Arbnum.toInt m, v) ^ "w") 2719 >> (if !Globals.show_types orelse !word_cast_on 2720 then brk (1, 2) 2721 >> lift pp_type (type_of t) 2722 >> str ")" 2723 else nothing) 2724 end 2725 handle HOL_ERR _ => raise term_pp_types.UserPP_Failed 2726end 2727 2728fun output_words_as f = 2729 Parse.temp_add_user_printer 2730 ("wordsLib.print_word", ``words$n2w x : 'a word``, print_word f) 2731 2732val _ = Feedback.register_trace ("word printing", word_pp_mode, 6) 2733val _ = Feedback.register_btrace ("word pp as 2's comp", int_word_pp) 2734 2735local 2736 val hexsplit = Arbnum.fromHexString "10000" 2737in 2738 val _ = output_words_as 2739 (fn (l, v) => 2740 if !word_pp_mode = 0 andalso Arbnum.<= (hexsplit, v) 2741 then "0x" ^ Arbnum.toHexString v 2742 else if !word_pp_mode = 0 orelse !word_pp_mode = 3 2743 then Arbnum.toString v 2744 else if !word_pp_mode = 1 2745 then "0b" ^ Arbnum.toBinString v 2746 else if !word_pp_mode = 2 2747 then if !base_tokens.allow_octal_input 2748 orelse Arbnum.< (v, Arbnum.fromInt 8) 2749 then "0" ^ Arbnum.toOctString v 2750 else ( Feedback.HOL_MESG 2751 "Octal output is only supported when \ 2752 \base_tokens.allow_octal_input is true." 2753 ; Arbnum.toString v 2754 ) 2755 else if !word_pp_mode = 6 andalso l mod 4 = 0 2756 then "0x" ^ StringCvt.padLeft #"0" (l div 4) (Arbnum.toHexString v) 2757 else if !word_pp_mode = 4 orelse !word_pp_mode = 6 2758 then "0x" ^ Arbnum.toHexString v 2759 else if !word_pp_mode = 5 2760 then "0b" ^ StringCvt.padLeft #"0" l (Arbnum.toBinString v) 2761 else raise ERR "output_words_as" "invalid printing mode") 2762end 2763 2764fun output_words_as_bin () = set_trace "word printing" 1 2765fun output_words_as_dec () = set_trace "word printing" 3 2766fun output_words_as_hex () = set_trace "word printing" 4 2767fun output_words_as_padded_bin () = set_trace "word printing" 5 2768fun output_words_as_padded_hex () = set_trace "word printing" 6 2769 2770fun output_words_as_oct () = 2771 (base_tokens.allow_octal_input := true; set_trace "word printing" 2) 2772 2773fun remove_word_printer () = 2774 General.ignore (Parse.remove_user_printer "wordsLib.print_word") 2775 2776(* ------------------------------------------------------------------------- 2777 A pretty-printer that shows the types for ><, w2w and @@ 2778 ------------------------------------------------------------------------- *) 2779 2780fun word_cast Gs backend syspr ppfns (pg, lg, rg) d t = 2781 let 2782 open Portable term_pp_types smpp 2783 infix >> 2784 val ppfns : ppstream_funs = ppfns 2785 val {add_string = str, add_break = brk, ublock,...} = ppfns 2786 fun stype tm = String.extract (type_to_string (type_of tm), 1, NONE) 2787 fun delim i act = 2788 case pg of 2789 Prec (j, _) => if i <= j then act else nothing 2790 | _ => nothing 2791 val (f, x) = strip_comb t 2792 fun sys g d t = syspr {gravs = g, depth = d, binderp = false} t 2793 in 2794 case (dest_thy_const f, x) of 2795 ({Name = "n2w", Thy = "words", Ty = ty}, [a]) => 2796 let 2797 val prec = Prec (2000, "n2w") 2798 in 2799 ublock INCONSISTENT 0 2800 (delim 200 (str "(") 2801 >> str "(n2w " 2802 >> lift pp_type ty 2803 >> str ")" 2804 >> brk (1, 2) 2805 >> sys (prec, prec, prec) (d - 1) a 2806 >> delim 200 (str ")")) 2807 end 2808 | ({Name = "w2w", Thy = "words", Ty = ty}, [a]) => 2809 let 2810 val prec = Prec (2000, "w2w") 2811 in 2812 ublock INCONSISTENT 0 2813 (delim 200 (str "(") 2814 >> str "(w2w " 2815 >> lift pp_type ty 2816 >> str ")" 2817 >> brk (1, 2) 2818 >> sys (prec, prec, prec) (d - 1) a 2819 >> delim 200 (str ")")) 2820 end 2821 | ({Name = "sw2sw", Thy = "words", Ty = ty}, [a]) => 2822 let 2823 val prec = Prec (2000, "sw2sw") 2824 in 2825 ublock INCONSISTENT 0 2826 (delim 200 (str "(") 2827 >> str "(sw2sw " 2828 >> lift pp_type ty 2829 >> str ")" 2830 >> brk (1, 2) 2831 >> sys (prec, prec, prec) (d - 1) a 2832 >> delim 200 (str ")")) 2833 end 2834 | ({Name = "word_concat", Thy = "words", Ty = ty}, [a, b]) => 2835 let 2836 val prec = Prec (2000, "word_concat") 2837 in 2838 ublock INCONSISTENT 0 2839 (delim 200 (str "(") 2840 >> str "(word_concat " 2841 >> lift pp_type ty 2842 >> str ")" 2843 >> brk (1, 2) 2844 >> sys (prec, prec, prec) (d - 1) a 2845 >> brk (1, 0) 2846 >> sys (prec, prec, prec) (d - 1) b 2847 >> delim 200 (str ")")) 2848 end 2849 | ({Name = "word_extract", Thy = "words", Ty = ty}, [h, l, a]) => 2850 let 2851 val prec = Prec (2000, "word_extract") 2852 in 2853 ublock INCONSISTENT 0 2854 (delim 200 (str "(") 2855 >> str "(" 2856 >> str "(" 2857 >> sys (prec, prec, prec) (d - 1) h 2858 >> brk (1, 2) 2859 >> str "><" 2860 >> brk (1, 2) 2861 >> sys (prec, prec, prec) (d - 1) l 2862 >> str ")" 2863 >> brk (1, 2) 2864 >> lift pp_type (type_of (list_mk_comb (f, [h, l]))) 2865 >> str ")" 2866 >> brk (1, 2) 2867 >> sys (prec, prec, prec) (d - 1) a 2868 >> delim 200 (str ")")) 2869 end 2870 | _ => raise term_pp_types.UserPP_Failed 2871 end 2872 handle HOL_ERR _ => raise term_pp_types.UserPP_Failed 2873 2874fun add_word_cast_printer () = 2875 (word_cast_on := true 2876 ; Parse.temp_add_user_printer 2877 ("wordsLib.word_cast", ``f:'b word``, word_cast)) 2878 2879fun remove_word_cast_printer () = 2880 (word_cast_on := false; Parse.remove_user_printer "wordsLib.word_cast"; ()) 2881 2882(* ------------------------------------------------------------------------- 2883 Guessing the word length for the result of extraction (><), 2884 concatenate (@@), word_replicate and concat_word_list 2885 ------------------------------------------------------------------------- *) 2886 2887val notify_on_word_length_guess = ref true 2888val guessing_word_lengths = ref false 2889 2890val _ = Feedback.register_btrace ("notify word length guesses", 2891 notify_on_word_length_guess) 2892 2893val _ = Feedback.register_btrace ("guess word lengths", 2894 guessing_word_lengths) 2895 2896fun guess_lengths () = set_trace "guess word lengths" 1 2897fun dont_guess_lengths () = set_trace "guess word lengths" 0 2898 2899fun t2s t = String.extract (Hol_pp.type_to_string t, 1, NONE) 2900 2901fun LENGTH_INST t = 2902 let 2903 open numSyntax 2904 val word_type = wordsSyntax.dest_word_type o type_of 2905 val ty = word_type t 2906 in 2907 if Type.polymorphic ty 2908 then case boolSyntax.dest_strip_comb t of 2909 ("words$word_extract", [h, l, _]) => 2910 let 2911 val nh = dest_numeral h 2912 val nl = dest_numeral l 2913 val nt = Arbnum.- (Arbnum.plus1 nh, nl) 2914 in 2915 ty |-> fcpLib.index_type nt 2916 end 2917 | ("words$word_concat", [a, b]) => 2918 let 2919 val na = fcpLib.index_to_num (word_type a) 2920 val nb = fcpLib.index_to_num (word_type b) 2921 val nt = Arbnum.+ (na, nb) 2922 in 2923 ty |-> fcpLib.index_type nt 2924 end 2925 | ("words$word_replicate", [m, a]) => 2926 let 2927 val nm = dest_numeral m 2928 val na = fcpLib.index_to_num (word_type a) 2929 val nt = Arbnum.* (nm, na) 2930 in 2931 ty |-> fcpLib.index_type nt 2932 end 2933 | ("words$concat_word_list", [l]) => 2934 let 2935 val (ls, tyl) = listSyntax.dest_list l 2936 val nl = 2937 fcpLib.index_to_num (wordsSyntax.dest_word_type tyl) 2938 val nt = Arbnum.* (Arbnum.fromInt (length ls), nl) 2939 in 2940 ty |-> fcpLib.index_type nt 2941 end 2942 | _ => raise ERR "LENGTH_INST" "" 2943 else raise ERR "LENGTH_INST" "" 2944 end 2945 2946fun inst_word_lengths tm = 2947 case Lib.total (HolKernel.find_term (Lib.can LENGTH_INST)) tm of 2948 NONE => tm 2949 | SOME subtm => 2950 let 2951 val (theinst as {redex, residue}) = LENGTH_INST subtm 2952 val _ = if !Globals.interactive andalso !notify_on_word_length_guess 2953 then Feedback.HOL_MESG 2954 (String.concat ["assigning word length: ", 2955 t2s redex, " <- ", t2s residue]) 2956 else () 2957 in 2958 inst_word_lengths (Term.inst [theinst] tm) 2959 end 2960 2961fun word_post_process_term t = 2962 if !guessing_word_lengths 2963 then inst_word_lengths (fcpLib.inst_fcp_lengths t) 2964 else t 2965 2966val _ = Parse.post_process_term := 2967 (word_post_process_term o !Parse.post_process_term) 2968 2969val operators = 2970 [("+", "word_add"), ("-", "word_sub"), ("numeric_negate", "word_2comp"), 2971 ("*", "word_mul"), ("<", "word_lt"), (">", "word_gt"), 2972 ("<=", "word_le"), (">=", "word_ge"), ("/", "word_quot")] 2973 2974fun deprecate_word () = 2975 app (fn (opname, name) => 2976 temp_send_to_back_overload opname {Name = name, Thy = "words"} 2977 handle HOL_ERR _ => ()) operators 2978 2979fun prefer_word () = 2980 app (fn (opname, name) => 2981 temp_bring_to_front_overload opname {Name = name, Thy = "words"} 2982 handle HOL_ERR _ => ()) operators 2983 2984val _ = Defn.const_eq_ref := (!Defn.const_eq_ref ORELSEC word_EQ_CONV) 2985 2986end 2987