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