src/integer/integer_wordScript.sml

27   i2w (i : int) : 'a word =
44   saturate_i2w i : 'a word =
53   saturate_i2sw i : 'a word =
62   saturate_sw2sw (w: 'a word) = saturate_i2sw (w2i w)`
65   saturate_w2sw (w: 'a word) = saturate_i2sw (&w2n w)`
68   saturate_sw2w (w: 'a word) = saturate_i2w (w2i w)`
71   signed_saturate_add (a: 'a word) (b: 'a word) =
72     saturate_i2sw (w2i a + w2i b) : 'a word`
75   signed_saturate_sub (a: 'a word) (b: 'a word) =
76     saturate_i2sw (w2i a - w2i b) : 'a word`
79   word_sdiv (a : 'a word) (b : 'a word) = i2w (w2i a / w2i b) : 'a word`
82   word_smod (a : 'a word) (b : 'a word) = i2w (w2i a % w2i b) : 'a word`
129       (w2i (n2w n : 'a word) = ~ &(dimword(:'a) - n))``,
161     (w2i (i2w i : 'a word) = i)``,
192   ``!i. word_msb (i2w i : 'a word) = &(INT_MIN(:'a)) <= i % &(dimword(:'a))``,
227   `!w:'a word. w2i w <= INT_MAX (:'a)`,
237   `!w:'a word. INT_MIN (:'a) <= w2i w`,
260   `!w:'a word. ?i. (w = i2w i) /\ INT_MIN (:'a) <= i /\ i <= INT_MAX (:'a)`,
286            (-n2w (Num (-i)) = n2w n : 'a word) /\
288                n2w (2 ** dimindex (:'b) - 2 ** dimindex (:'a) + n) : 'b word)`,
314        (sw2sw (i2w j : 'b word) = i2w j : 'a word)`,
318          (-n2w (Num (-j)) = n2w n : 'b word) /\
320            n2w (2 ** dimindex (:'a) - 2 ** dimindex (:'b) + n) : 'a word)`
397        (w2w (i2w i : 'b word) = i2w i : 'a word)`,
515            ``(-a + -b = -c : 'a word) = (a + b = c)``)]
559   `!w : 'a word. (w2i w = 0) = (w = 0w)`,
632      (i2w (i / 2 ** n) : 'a word = i2w i >> n)`,
701   `!w : 'a word.
702       INT_MIN (:'a) <= w2i (sw2sw w : 'b word) /\
703       w2i (sw2sw w : 'b word) <= INT_MAX (:'a)`,
708     \\ Q.ISPEC_THEN `sw2sw w : 'b word` ASSUME_TAC w2i_le
709     \\ Q.ISPEC_THEN `sw2sw w : 'b word` ASSUME_TAC w2i_ge
712     \\ Cases_on_i2w `w : 'a word`
722        ((i = w2i (i2w i : 'b word)) =
723         (i2w i = sw2sw (i2w i : 'b word) : 'a word))`,
730   `!a:'a word b:'b word.
732     ((w2i a = w2i b) = (sw2sw a = sw2sw b : 'c word))`,
736   \\ Cases_on_i2w `a:'a word`
737   \\ Cases_on_i2w `b:'b word`
745          (Num (w2i (n2w n : 'a word) % 2 ** m) = n MOD 2 ** m)`,
770   STRIP_TAC \\ Cases_on_i2w `w : 'a word`
778        (word_abs (i2w i) = n2w (Num (ABS i)) : 'a word)`,
827   `w2i (1w:'a word) = if dimindex(:'a) = 1 then -1 else 1`,
835   `w2i (INT_MINw: 'a word) = INT_MIN (:'a)`,
840   `w2i (UINT_MAXw: 'a word) = -1i`,
846   `w2i (INT_MAXw: 'a word) = INT_MAX (:'a)`,
854   `!w: 'a word. w2i w < 0 = w < 0w`,
855   STRIP_TAC \\ Cases_on_i2w `w: 'a word`
859   `!w:'a word. w <> INT_MINw ==> (w2i (-w) = -w2i w)`,
882   `i2w (INT_MIN (:'a)) = INT_MINw : 'a word`,
888   `i2w (INT_MAX (:'a)) = INT_MAXw : 'a word`,
894   `i2w (UINT_MAX (:'a)) = UINT_MAXw : 'a word`,
903        (word_msb (i2w i : 'a word) = i < 0)`,
921   `!n. n <= INT_MIN (:'a) ==> (w2n (i2w (&n) : 'a word) = n)`,
930   `!n. n <= INT_MAX (:'a) ==> (w2n (i2w (&n) : 'a word) = n)`,
953   \\ qmatch_goalsub_rename_tac `i2w i  / i2w j : 'a word`
970   \\ qmatch_goalsub_rename_tac `word_rem (i2w i) (i2w j) : 'a word`
1001   `!w: 'a word.
1002     saturate_w2sw w : 'b word =
1003       if dimindex(:'b) <= dimindex(:'a) /\ w2w (word_H: 'b word) <=+ w then
1048   `!w: 'a word.
1049     saturate_sw2w w : 'b word =
1057   \\ Cases_on `w < 0w : 'a word`
1082   `!w: 'a word.
1083     saturate_sw2sw w : 'b word =
1086       else if sw2sw (word_H: 'b word) <= w then
1088       else if w <= sw2sw (word_L: 'b word) then
1092   STRIP_TAC \\ Cases_on_i2w `w:'a word`
1110     \\ `n2w (INT_MAX (:'b)) : 'b word = i2w (&INT_MAX (:'b))`
1112     \\ `n2w (INT_MIN (:'b)) : 'b word = i2w (-&INT_MIN (:'b))`
1140   `!a b:'a word.
1156     Cases_on_i2w `a:'a word`
1166     Cases_on_i2w `a:'a word`
1175             wordsLib.WORD_ARITH_PROVE ``(a + b = c + a) = (b = c : 'a word)``]
1178            [wordsLib.WORD_ARITH_PROVE ``(a = -b : 'a word) = (-1w * a = b)``,
1183     \\ pop_assum (fn th => assume_tac (Q.SPEC `a:'a word` th) \\
1184                            assume_tac (Q.SPEC `b:'a word` th))
1203      0 <= w2i (i2w (i + j) : 'a word)`,
1226      w2i (i2w (i + j) : 'a word) < 0`,
1251   `!a b:'a word.
1259   \\ Cases_on_i2w `a : 'a word`
1260   \\ Cases_on_i2w `b : 'a word`
1321    `!n. n <= INT_MAX (:'a) ==> (w2i (i2w (&n) : 'a word) = &n)`,
1326    `!n. n <= INT_MIN (:'a) ==> (w2i (i2w (-&n) : 'a word) = -&n)`,
1402   `!x y : 'a word.
1411       \\ `!a: 'a word. a - INT_MINw = a + INT_MINw`
1427       >- (`INT_MINw + INT_MINw = 0w : 'a word`
1446   `!n. n2w (dimword(:'a) + n) = n2w n : 'a word`,
1468   `!w : 'a word. i2w (&w2n w) = w2w w : 'b word`,
1476   ``&w2n ((i2w n):'a word) = n % (& dimword (:'a))``,
1493   ``w2i (w:'a word) =