acl2/ml/signedintScript.sml

231     ``!a. BIT (dimindex (:'a) - 1) (w2n (a:'a word)) =
299 (*     sw2i x : Convert the word x to a signed integer                       *)
300 (*     i2sw x : Convert the integer x to a word                              *)
314 val sw2i_def = Define `sw2i (x:'a word) =
323                         else n2w (Num m):'b word`;
706     ``sw2i (x:'a word) = extend (& (w2n x)) (dimindex (:'a))``,
715     (REWRITE_RULE [GSYM sw2i_thm] (Q.SPEC `& (w2n (a:'a word))`
734 (* sw2i_i2sw : |- !x. sw2i ((i2sw x) : 'a word) = extend x (dimindex (:'a))  *)
737 val rwr1 = prove(``& (w2n (x:'a word)) - & (2 ** dimindex (:'a)):int =
743                         ~ & (dimword (:'a) - w2n (x:'a word) - 1)``,
747     `w2n (x:'a word) = dimword (:'a) - 1` by ARITH_TAC THEN
761     ``!x. i2sw (sw2i x) = sw2sw (x:'a word) : 'b word``,
785     ``!x. sw2i ((i2sw x):'a word) = extend x (dimindex (:'a))``,
815     ``!a. sw2i (- a:'a word) = extend (~ (sw2i a)) (dimindex (:'a))``,
825     ``!a b. sw2i (a + (b:'a word)) =
833     ``!a b. sw2i (a - (b:'a word)) =
847     ``!a b. sw2i (a * b : 'a word) =
881                           2i ** (dimindex (:'a)) - iand (& (w2n (a:'a word)))
882                                 (& (w2n (b:'a word)))``,
1105 val plem1 = prove(``!b. ~(b = 0w : 'a word) ==>
1106       ((w2n (a:'a word) DIV w2n b) MOD 2 ** dimindex (:'a) = w2n a DIV w2n b)``,
1192 val lem5 = prove(``~(w2n a = 0) ==> (2 ** dimindex (:'a) - w2n (a:'a word))
1193                          DIV (2 ** dimindex (:'a) - w2n (b:'a word))
1199                 (2 ** dimindex (:'a) - w2n (a:'a word)) DIV w2n (b:'a word)
1223                (sw2i (a / b : 'a word) = (sw2i a) quot (sw2i b))``,
1238     TRY (PAT_ASSUM ``~(a / b= 0w:'a word)`` MP_TAC) THEN
1239     TRY (PAT_ASSUM ``a / b= 0w:'a word`` MP_TAC) THEN
1271 val sw2i_div_T = prove(``sw2i ((a:'a word) / UINT_MAXw) =
1272         extend (sw2i a quot sw2i (UINT_MAXw:'a word)) (dimindex (:'a))``,
1288     ``!a b. ~(b = 0w) ==> (sw2i ((a:'a word) / b) =
1299 val bit_lem = prove(``~BIT (dimindex (:'b) - 1) (w2n (a:'b word) DIV 2)``,
1319                (prove(``w2n (a:'a word) DIV 2 < 2 ** (dimindex (:'a) - 1)``,
1323                (w2n (a:'a word) = 0) \/ (w2n a = 1)``,
1328                (AP_TERM ``n2w:num -> 'a word`` (SPEC_ALL w2n_lsr)),rwr2,rwr3,
1391     ``sw2i ((a:'a word) << b) = extend (sw2i a * 2 ** b) (dimindex (:'a))``,
1414                      (BIT b (w2n (a : 'a word)) = a ' b)``,
1423              (ODD (w2n (a >> b)) = 2 ** b <= w2n (a:'a word) MOD 2 ** SUC b)``,
1430     ``!a b. b < dimindex (:'a) ==> (a ' b = ibit b (sw2i (a:'a word)))``,
1460 (* sw2i_n2w : |- !a. sw2i (n2w a : 'a word) = extend (& a) (dimindex (:'a))  *)
1470     ``!a. sw2i (n2w a : 'a word) = extend (& a) (dimindex (:'a))``,
1478 (* Theorems relating word definitions to definitions using operators         *)
1511                  ((n2w n :'a word) ' i = BIT i n)``,word_asr_def,
1520              ``i < dimindex (:'a) ==> ((n2w n :'a word) ' i = BIT i n)``,