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