src/HOL/Word/WordDefinition.thy
author wenzelm
Thu Mar 26 20:08:55 2009 +0100 (2009-03-26)
changeset 30729 461ee3e49ad3
parent 29630 199e2fb7f588
child 30952 7ab2716dd93b
permissions -rw-r--r--
interpretation/interpret: prefixes are mandatory by default;
     1 (* 
     2   Author: Jeremy Dawson and Gerwin Klein, NICTA
     3   
     4   Basic definition of word type and basic theorems following from 
     5   the definition of the word type 
     6 *) 
     7 
     8 header {* Definition of Word Type *}
     9 
    10 theory WordDefinition
    11 imports Size BinBoolList TdThs
    12 begin
    13 
    14 subsection {* Type definition *}
    15 
    16 typedef (open word) 'a word = "{(0::int) ..< 2^len_of TYPE('a::len0)}"
    17   morphisms uint Abs_word by auto
    18 
    19 definition word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word" where
    20   -- {* representation of words using unsigned or signed bins, 
    21         only difference in these is the type class *}
    22   [code del]: "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)" 
    23 
    24 lemma uint_word_of_int [code]: "uint (word_of_int w \<Colon> 'a\<Colon>len0 word) = w mod 2 ^ len_of TYPE('a)"
    25   by (auto simp add: word_of_int_def bintrunc_mod2p intro: Abs_word_inverse)
    26 
    27 code_datatype word_of_int
    28 
    29 
    30 subsection {* Type conversions and casting *}
    31 
    32 definition sint :: "'a :: len word => int" where
    33   -- {* treats the most-significant-bit as a sign bit *}
    34   sint_uint: "sint w = sbintrunc (len_of TYPE ('a) - 1) (uint w)"
    35 
    36 definition unat :: "'a :: len0 word => nat" where
    37   "unat w = nat (uint w)"
    38 
    39 definition uints :: "nat => int set" where
    40   -- "the sets of integers representing the words"
    41   "uints n = range (bintrunc n)"
    42 
    43 definition sints :: "nat => int set" where
    44   "sints n = range (sbintrunc (n - 1))"
    45 
    46 definition unats :: "nat => nat set" where
    47   "unats n = {i. i < 2 ^ n}"
    48 
    49 definition norm_sint :: "nat => int => int" where
    50   "norm_sint n w = (w + 2 ^ (n - 1)) mod 2 ^ n - 2 ^ (n - 1)"
    51 
    52 definition scast :: "'a :: len word => 'b :: len word" where
    53   -- "cast a word to a different length"
    54   "scast w = word_of_int (sint w)"
    55 
    56 definition ucast :: "'a :: len0 word => 'b :: len0 word" where
    57   "ucast w = word_of_int (uint w)"
    58 
    59 instantiation word :: (len0) size
    60 begin
    61 
    62 definition
    63   word_size: "size (w :: 'a word) = len_of TYPE('a)"
    64 
    65 instance ..
    66 
    67 end
    68 
    69 definition source_size :: "('a :: len0 word => 'b) => nat" where
    70   -- "whether a cast (or other) function is to a longer or shorter length"
    71   "source_size c = (let arb = undefined ; x = c arb in size arb)"  
    72 
    73 definition target_size :: "('a => 'b :: len0 word) => nat" where
    74   "target_size c = size (c undefined)"
    75 
    76 definition is_up :: "('a :: len0 word => 'b :: len0 word) => bool" where
    77   "is_up c \<longleftrightarrow> source_size c <= target_size c"
    78 
    79 definition is_down :: "('a :: len0 word => 'b :: len0 word) => bool" where
    80   "is_down c \<longleftrightarrow> target_size c <= source_size c"
    81 
    82 definition of_bl :: "bool list => 'a :: len0 word" where
    83   "of_bl bl = word_of_int (bl_to_bin bl)"
    84 
    85 definition to_bl :: "'a :: len0 word => bool list" where
    86   "to_bl w = bin_to_bl (len_of TYPE ('a)) (uint w)"
    87 
    88 definition word_reverse :: "'a :: len0 word => 'a word" where
    89   "word_reverse w = of_bl (rev (to_bl w))"
    90 
    91 definition word_int_case :: "(int => 'b) => ('a :: len0 word) => 'b" where
    92   "word_int_case f w = f (uint w)"
    93 
    94 syntax
    95   of_int :: "int => 'a"
    96 translations
    97   "case x of of_int y => b" == "CONST word_int_case (%y. b) x"
    98 
    99 
   100 subsection  "Arithmetic operations"
   101 
   102 instantiation word :: (len0) "{number, uminus, minus, plus, one, zero, times, Divides.div, power, ord, bit}"
   103 begin
   104 
   105 definition
   106   word_0_wi: "0 = word_of_int 0"
   107 
   108 definition
   109   word_1_wi: "1 = word_of_int 1"
   110 
   111 definition
   112   word_add_def: "a + b = word_of_int (uint a + uint b)"
   113 
   114 definition
   115   word_sub_wi: "a - b = word_of_int (uint a - uint b)"
   116 
   117 definition
   118   word_minus_def: "- a = word_of_int (- uint a)"
   119 
   120 definition
   121   word_mult_def: "a * b = word_of_int (uint a * uint b)"
   122 
   123 definition
   124   word_div_def: "a div b = word_of_int (uint a div uint b)"
   125 
   126 definition
   127   word_mod_def: "a mod b = word_of_int (uint a mod uint b)"
   128 
   129 primrec power_word where
   130   "(a\<Colon>'a word) ^ 0 = 1"
   131   | "(a\<Colon>'a word) ^ Suc n = a * a ^ n"
   132 
   133 definition
   134   word_number_of_def: "number_of w = word_of_int w"
   135 
   136 definition
   137   word_le_def: "a \<le> b \<longleftrightarrow> uint a \<le> uint b"
   138 
   139 definition
   140   word_less_def: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> (y \<Colon> 'a word)"
   141 
   142 definition
   143   word_and_def: 
   144   "(a::'a word) AND b = word_of_int (uint a AND uint b)"
   145 
   146 definition
   147   word_or_def:  
   148   "(a::'a word) OR b = word_of_int (uint a OR uint b)"
   149 
   150 definition
   151   word_xor_def: 
   152   "(a::'a word) XOR b = word_of_int (uint a XOR uint b)"
   153 
   154 definition
   155   word_not_def: 
   156   "NOT (a::'a word) = word_of_int (NOT (uint a))"
   157 
   158 instance ..
   159 
   160 end 
   161 
   162 definition
   163   word_succ :: "'a :: len0 word => 'a word"
   164 where
   165   "word_succ a = word_of_int (Int.succ (uint a))"
   166 
   167 definition
   168   word_pred :: "'a :: len0 word => 'a word"
   169 where
   170   "word_pred a = word_of_int (Int.pred (uint a))"
   171 
   172 constdefs
   173   udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50)
   174   "a udvd b == EX n>=0. uint b = n * uint a"
   175 
   176   word_sle :: "'a :: len word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50)
   177   "a <=s b == sint a <= sint b"
   178 
   179   word_sless :: "'a :: len word => 'a word => bool" ("(_/ <s _)" [50, 51] 50)
   180   "(x <s y) == (x <=s y & x ~= y)"
   181 
   182 
   183 
   184 subsection "Bit-wise operations"
   185 
   186 instantiation word :: (len0) bits
   187 begin
   188 
   189 definition
   190   word_test_bit_def: "test_bit a = bin_nth (uint a)"
   191 
   192 definition
   193   word_set_bit_def: "set_bit a n x =
   194    word_of_int (bin_sc n (If x bit.B1 bit.B0) (uint a))"
   195 
   196 definition
   197   word_set_bits_def: "(BITS n. f n) = of_bl (bl_of_nth (len_of TYPE ('a)) f)"
   198 
   199 definition
   200   word_lsb_def: "lsb a \<longleftrightarrow> bin_last (uint a) = bit.B1"
   201 
   202 definition shiftl1 :: "'a word \<Rightarrow> 'a word" where
   203   "shiftl1 w = word_of_int (uint w BIT bit.B0)"
   204 
   205 definition shiftr1 :: "'a word \<Rightarrow> 'a word" where
   206   -- "shift right as unsigned or as signed, ie logical or arithmetic"
   207   "shiftr1 w = word_of_int (bin_rest (uint w))"
   208 
   209 definition
   210   shiftl_def: "w << n = (shiftl1 ^ n) w"
   211 
   212 definition
   213   shiftr_def: "w >> n = (shiftr1 ^ n) w"
   214 
   215 instance ..
   216 
   217 end
   218 
   219 instantiation word :: (len) bitss
   220 begin
   221 
   222 definition
   223   word_msb_def: 
   224   "msb a \<longleftrightarrow> bin_sign (sint a) = Int.Min"
   225 
   226 instance ..
   227 
   228 end
   229 
   230 constdefs
   231   setBit :: "'a :: len0 word => nat => 'a word" 
   232   "setBit w n == set_bit w n True"
   233 
   234   clearBit :: "'a :: len0 word => nat => 'a word" 
   235   "clearBit w n == set_bit w n False"
   236 
   237 
   238 subsection "Shift operations"
   239 
   240 constdefs
   241   sshiftr1 :: "'a :: len word => 'a word" 
   242   "sshiftr1 w == word_of_int (bin_rest (sint w))"
   243 
   244   bshiftr1 :: "bool => 'a :: len word => 'a word"
   245   "bshiftr1 b w == of_bl (b # butlast (to_bl w))"
   246 
   247   sshiftr :: "'a :: len word => nat => 'a word" (infixl ">>>" 55)
   248   "w >>> n == (sshiftr1 ^ n) w"
   249 
   250   mask :: "nat => 'a::len word"
   251   "mask n == (1 << n) - 1"
   252 
   253   revcast :: "'a :: len0 word => 'b :: len0 word"
   254   "revcast w ==  of_bl (takefill False (len_of TYPE('b)) (to_bl w))"
   255 
   256   slice1 :: "nat => 'a :: len0 word => 'b :: len0 word"
   257   "slice1 n w == of_bl (takefill False n (to_bl w))"
   258 
   259   slice :: "nat => 'a :: len0 word => 'b :: len0 word"
   260   "slice n w == slice1 (size w - n) w"
   261 
   262 
   263 subsection "Rotation"
   264 
   265 constdefs
   266   rotater1 :: "'a list => 'a list"
   267   "rotater1 ys == 
   268     case ys of [] => [] | x # xs => last ys # butlast ys"
   269 
   270   rotater :: "nat => 'a list => 'a list"
   271   "rotater n == rotater1 ^ n"
   272 
   273   word_rotr :: "nat => 'a :: len0 word => 'a :: len0 word"
   274   "word_rotr n w == of_bl (rotater n (to_bl w))"
   275 
   276   word_rotl :: "nat => 'a :: len0 word => 'a :: len0 word"
   277   "word_rotl n w == of_bl (rotate n (to_bl w))"
   278 
   279   word_roti :: "int => 'a :: len0 word => 'a :: len0 word"
   280   "word_roti i w == if i >= 0 then word_rotr (nat i) w
   281                     else word_rotl (nat (- i)) w"
   282 
   283 
   284 subsection "Split and cat operations"
   285 
   286 constdefs
   287   word_cat :: "'a :: len0 word => 'b :: len0 word => 'c :: len0 word"
   288   "word_cat a b == word_of_int (bin_cat (uint a) (len_of TYPE ('b)) (uint b))"
   289 
   290   word_split :: "'a :: len0 word => ('b :: len0 word) * ('c :: len0 word)"
   291   "word_split a == 
   292    case bin_split (len_of TYPE ('c)) (uint a) of 
   293      (u, v) => (word_of_int u, word_of_int v)"
   294 
   295   word_rcat :: "'a :: len0 word list => 'b :: len0 word"
   296   "word_rcat ws == 
   297   word_of_int (bin_rcat (len_of TYPE ('a)) (map uint ws))"
   298 
   299   word_rsplit :: "'a :: len0 word => 'b :: len word list"
   300   "word_rsplit w == 
   301   map word_of_int (bin_rsplit (len_of TYPE ('b)) (len_of TYPE ('a), uint w))"
   302 
   303 constdefs
   304   -- "Largest representable machine integer."
   305   max_word :: "'a::len word"
   306   "max_word \<equiv> word_of_int (2^len_of TYPE('a) - 1)"
   307 
   308 consts 
   309   of_bool :: "bool \<Rightarrow> 'a::len word"
   310 primrec
   311   "of_bool False = 0"
   312   "of_bool True = 1"
   313 
   314 
   315 lemmas of_nth_def = word_set_bits_def
   316 
   317 lemmas word_size_gt_0 [iff] = 
   318   xtr1 [OF word_size len_gt_0, standard]
   319 lemmas lens_gt_0 = word_size_gt_0 len_gt_0
   320 lemmas lens_not_0 [iff] = lens_gt_0 [THEN gr_implies_not0, standard]
   321 
   322 lemma uints_num: "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}"
   323   by (simp add: uints_def range_bintrunc)
   324 
   325 lemma sints_num: "sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}"
   326   by (simp add: sints_def range_sbintrunc)
   327 
   328 lemmas atLeastLessThan_alt = atLeastLessThan_def [unfolded 
   329   atLeast_def lessThan_def Collect_conj_eq [symmetric]]
   330   
   331 lemma mod_in_reps: "m > 0 ==> y mod m : {0::int ..< m}"
   332   unfolding atLeastLessThan_alt by auto
   333 
   334 lemma 
   335   uint_0:"0 <= uint x" and 
   336   uint_lt: "uint (x::'a::len0 word) < 2 ^ len_of TYPE('a)"
   337   by (auto simp: uint [simplified])
   338 
   339 lemma uint_mod_same:
   340   "uint x mod 2 ^ len_of TYPE('a) = uint (x::'a::len0 word)"
   341   by (simp add: int_mod_eq uint_lt uint_0)
   342 
   343 lemma td_ext_uint: 
   344   "td_ext (uint :: 'a word => int) word_of_int (uints (len_of TYPE('a::len0))) 
   345     (%w::int. w mod 2 ^ len_of TYPE('a))"
   346   apply (unfold td_ext_def')
   347   apply (simp add: uints_num word_of_int_def bintrunc_mod2p)
   348   apply (simp add: uint_mod_same uint_0 uint_lt
   349                    word.uint_inverse word.Abs_word_inverse int_mod_lem)
   350   done
   351 
   352 lemmas int_word_uint = td_ext_uint [THEN td_ext.eq_norm, standard]
   353 
   354 interpretation word_uint:
   355   td_ext "uint::'a::len0 word \<Rightarrow> int" 
   356          word_of_int 
   357          "uints (len_of TYPE('a::len0))"
   358          "\<lambda>w. w mod 2 ^ len_of TYPE('a::len0)"
   359   by (rule td_ext_uint)
   360   
   361 lemmas td_uint = word_uint.td_thm
   362 
   363 lemmas td_ext_ubin = td_ext_uint 
   364   [simplified len_gt_0 no_bintr_alt1 [symmetric]]
   365 
   366 interpretation word_ubin:
   367   td_ext "uint::'a::len0 word \<Rightarrow> int" 
   368          word_of_int 
   369          "uints (len_of TYPE('a::len0))"
   370          "bintrunc (len_of TYPE('a::len0))"
   371   by (rule td_ext_ubin)
   372 
   373 lemma sint_sbintrunc': 
   374   "sint (word_of_int bin :: 'a word) = 
   375     (sbintrunc (len_of TYPE ('a :: len) - 1) bin)"
   376   unfolding sint_uint 
   377   by (auto simp: word_ubin.eq_norm sbintrunc_bintrunc_lt)
   378 
   379 lemma uint_sint: 
   380   "uint w = bintrunc (len_of TYPE('a)) (sint (w :: 'a :: len word))"
   381   unfolding sint_uint by (auto simp: bintrunc_sbintrunc_le)
   382 
   383 lemma bintr_uint': 
   384   "n >= size w ==> bintrunc n (uint w) = uint w"
   385   apply (unfold word_size)
   386   apply (subst word_ubin.norm_Rep [symmetric]) 
   387   apply (simp only: bintrunc_bintrunc_min word_size min_def)
   388   apply simp
   389   done
   390 
   391 lemma wi_bintr': 
   392   "wb = word_of_int bin ==> n >= size wb ==> 
   393     word_of_int (bintrunc n bin) = wb"
   394   unfolding word_size
   395   by (clarsimp simp add : word_ubin.norm_eq_iff [symmetric] min_def)
   396 
   397 lemmas bintr_uint = bintr_uint' [unfolded word_size]
   398 lemmas wi_bintr = wi_bintr' [unfolded word_size]
   399 
   400 lemma td_ext_sbin: 
   401   "td_ext (sint :: 'a word => int) word_of_int (sints (len_of TYPE('a::len))) 
   402     (sbintrunc (len_of TYPE('a) - 1))"
   403   apply (unfold td_ext_def' sint_uint)
   404   apply (simp add : word_ubin.eq_norm)
   405   apply (cases "len_of TYPE('a)")
   406    apply (auto simp add : sints_def)
   407   apply (rule sym [THEN trans])
   408   apply (rule word_ubin.Abs_norm)
   409   apply (simp only: bintrunc_sbintrunc)
   410   apply (drule sym)
   411   apply simp
   412   done
   413 
   414 lemmas td_ext_sint = td_ext_sbin 
   415   [simplified len_gt_0 no_sbintr_alt2 Suc_pred' [symmetric]]
   416 
   417 (* We do sint before sbin, before sint is the user version
   418    and interpretations do not produce thm duplicates. I.e. 
   419    we get the name word_sint.Rep_eqD, but not word_sbin.Req_eqD,
   420    because the latter is the same thm as the former *)
   421 interpretation word_sint:
   422   td_ext "sint ::'a::len word => int" 
   423           word_of_int 
   424           "sints (len_of TYPE('a::len))"
   425           "%w. (w + 2^(len_of TYPE('a::len) - 1)) mod 2^len_of TYPE('a::len) -
   426                2 ^ (len_of TYPE('a::len) - 1)"
   427   by (rule td_ext_sint)
   428 
   429 interpretation word_sbin:
   430   td_ext "sint ::'a::len word => int" 
   431           word_of_int 
   432           "sints (len_of TYPE('a::len))"
   433           "sbintrunc (len_of TYPE('a::len) - 1)"
   434   by (rule td_ext_sbin)
   435 
   436 lemmas int_word_sint = td_ext_sint [THEN td_ext.eq_norm, standard]
   437 
   438 lemmas td_sint = word_sint.td
   439 
   440 lemma word_number_of_alt: "number_of b == word_of_int (number_of b)"
   441   unfolding word_number_of_def by (simp add: number_of_eq)
   442 
   443 lemma word_no_wi: "number_of = word_of_int"
   444   by (auto simp: word_number_of_def intro: ext)
   445 
   446 lemma to_bl_def': 
   447   "(to_bl :: 'a :: len0 word => bool list) =
   448     bin_to_bl (len_of TYPE('a)) o uint"
   449   by (auto simp: to_bl_def intro: ext)
   450 
   451 lemmas word_reverse_no_def [simp] = word_reverse_def [of "number_of w", standard]
   452 
   453 lemmas uints_mod = uints_def [unfolded no_bintr_alt1]
   454 
   455 lemma uint_bintrunc: "uint (number_of bin :: 'a word) = 
   456     number_of (bintrunc (len_of TYPE ('a :: len0)) bin)"
   457   unfolding word_number_of_def number_of_eq
   458   by (auto intro: word_ubin.eq_norm) 
   459 
   460 lemma sint_sbintrunc: "sint (number_of bin :: 'a word) = 
   461     number_of (sbintrunc (len_of TYPE ('a :: len) - 1) bin)" 
   462   unfolding word_number_of_def number_of_eq
   463   by (subst word_sbin.eq_norm) simp
   464 
   465 lemma unat_bintrunc: 
   466   "unat (number_of bin :: 'a :: len0 word) =
   467     number_of (bintrunc (len_of TYPE('a)) bin)"
   468   unfolding unat_def nat_number_of_def 
   469   by (simp only: uint_bintrunc)
   470 
   471 (* WARNING - these may not always be helpful *)
   472 declare 
   473   uint_bintrunc [simp] 
   474   sint_sbintrunc [simp] 
   475   unat_bintrunc [simp]
   476 
   477 lemma size_0_eq: "size (w :: 'a :: len0 word) = 0 ==> v = w"
   478   apply (unfold word_size)
   479   apply (rule word_uint.Rep_eqD)
   480   apply (rule box_equals)
   481     defer
   482     apply (rule word_ubin.norm_Rep)+
   483   apply simp
   484   done
   485 
   486 lemmas uint_lem = word_uint.Rep [unfolded uints_num mem_Collect_eq]
   487 lemmas sint_lem = word_sint.Rep [unfolded sints_num mem_Collect_eq]
   488 lemmas uint_ge_0 [iff] = uint_lem [THEN conjunct1, standard]
   489 lemmas uint_lt2p [iff] = uint_lem [THEN conjunct2, standard]
   490 lemmas sint_ge = sint_lem [THEN conjunct1, standard]
   491 lemmas sint_lt = sint_lem [THEN conjunct2, standard]
   492 
   493 lemma sign_uint_Pls [simp]: 
   494   "bin_sign (uint x) = Int.Pls"
   495   by (simp add: sign_Pls_ge_0 number_of_eq)
   496 
   497 lemmas uint_m2p_neg = iffD2 [OF diff_less_0_iff_less uint_lt2p, standard]
   498 lemmas uint_m2p_not_non_neg = 
   499   iffD2 [OF linorder_not_le uint_m2p_neg, standard]
   500 
   501 lemma lt2p_lem:
   502   "len_of TYPE('a) <= n ==> uint (w :: 'a :: len0 word) < 2 ^ n"
   503   by (rule xtr8 [OF _ uint_lt2p]) simp
   504 
   505 lemmas uint_le_0_iff [simp] = 
   506   uint_ge_0 [THEN leD, THEN linorder_antisym_conv1, standard]
   507 
   508 lemma uint_nat: "uint w == int (unat w)"
   509   unfolding unat_def by auto
   510 
   511 lemma uint_number_of:
   512   "uint (number_of b :: 'a :: len0 word) = number_of b mod 2 ^ len_of TYPE('a)"
   513   unfolding word_number_of_alt
   514   by (simp only: int_word_uint)
   515 
   516 lemma unat_number_of: 
   517   "bin_sign b = Int.Pls ==> 
   518   unat (number_of b::'a::len0 word) = number_of b mod 2 ^ len_of TYPE ('a)"
   519   apply (unfold unat_def)
   520   apply (clarsimp simp only: uint_number_of)
   521   apply (rule nat_mod_distrib [THEN trans])
   522     apply (erule sign_Pls_ge_0 [THEN iffD1])
   523    apply (simp_all add: nat_power_eq)
   524   done
   525 
   526 lemma sint_number_of: "sint (number_of b :: 'a :: len word) = (number_of b + 
   527     2 ^ (len_of TYPE('a) - 1)) mod 2 ^ len_of TYPE('a) -
   528     2 ^ (len_of TYPE('a) - 1)"
   529   unfolding word_number_of_alt by (rule int_word_sint)
   530 
   531 lemma word_of_int_bin [simp] : 
   532   "(word_of_int (number_of bin) :: 'a :: len0 word) = (number_of bin)"
   533   unfolding word_number_of_alt by auto
   534 
   535 lemma word_int_case_wi: 
   536   "word_int_case f (word_of_int i :: 'b word) = 
   537     f (i mod 2 ^ len_of TYPE('b::len0))"
   538   unfolding word_int_case_def by (simp add: word_uint.eq_norm)
   539 
   540 lemma word_int_split: 
   541   "P (word_int_case f x) = 
   542     (ALL i. x = (word_of_int i :: 'b :: len0 word) & 
   543       0 <= i & i < 2 ^ len_of TYPE('b) --> P (f i))"
   544   unfolding word_int_case_def
   545   by (auto simp: word_uint.eq_norm int_mod_eq')
   546 
   547 lemma word_int_split_asm: 
   548   "P (word_int_case f x) = 
   549     (~ (EX n. x = (word_of_int n :: 'b::len0 word) &
   550       0 <= n & n < 2 ^ len_of TYPE('b::len0) & ~ P (f n)))"
   551   unfolding word_int_case_def
   552   by (auto simp: word_uint.eq_norm int_mod_eq')
   553   
   554 lemmas uint_range' =
   555   word_uint.Rep [unfolded uints_num mem_Collect_eq, standard]
   556 lemmas sint_range' = word_sint.Rep [unfolded One_nat_def
   557   sints_num mem_Collect_eq, standard]
   558 
   559 lemma uint_range_size: "0 <= uint w & uint w < 2 ^ size w"
   560   unfolding word_size by (rule uint_range')
   561 
   562 lemma sint_range_size:
   563   "- (2 ^ (size w - Suc 0)) <= sint w & sint w < 2 ^ (size w - Suc 0)"
   564   unfolding word_size by (rule sint_range')
   565 
   566 lemmas sint_above_size = sint_range_size
   567   [THEN conjunct2, THEN [2] xtr8, folded One_nat_def, standard]
   568 
   569 lemmas sint_below_size = sint_range_size
   570   [THEN conjunct1, THEN [2] order_trans, folded One_nat_def, standard]
   571 
   572 lemma test_bit_eq_iff: "(test_bit (u::'a::len0 word) = test_bit v) = (u = v)"
   573   unfolding word_test_bit_def by (simp add: bin_nth_eq_iff)
   574 
   575 lemma test_bit_size [rule_format] : "(w::'a::len0 word) !! n --> n < size w"
   576   apply (unfold word_test_bit_def)
   577   apply (subst word_ubin.norm_Rep [symmetric])
   578   apply (simp only: nth_bintr word_size)
   579   apply fast
   580   done
   581 
   582 lemma word_eqI [rule_format] : 
   583   fixes u :: "'a::len0 word"
   584   shows "(ALL n. n < size u --> u !! n = v !! n) ==> u = v"
   585   apply (rule test_bit_eq_iff [THEN iffD1])
   586   apply (rule ext)
   587   apply (erule allE)
   588   apply (erule impCE)
   589    prefer 2
   590    apply assumption
   591   apply (auto dest!: test_bit_size simp add: word_size)
   592   done
   593 
   594 lemmas word_eqD = test_bit_eq_iff [THEN iffD2, THEN fun_cong, standard]
   595 
   596 lemma test_bit_bin': "w !! n = (n < size w & bin_nth (uint w) n)"
   597   unfolding word_test_bit_def word_size
   598   by (simp add: nth_bintr [symmetric])
   599 
   600 lemmas test_bit_bin = test_bit_bin' [unfolded word_size]
   601 
   602 lemma bin_nth_uint_imp': "bin_nth (uint w) n --> n < size w"
   603   apply (unfold word_size)
   604   apply (rule impI)
   605   apply (rule nth_bintr [THEN iffD1, THEN conjunct1])
   606   apply (subst word_ubin.norm_Rep)
   607   apply assumption
   608   done
   609 
   610 lemma bin_nth_sint': 
   611   "n >= size w --> bin_nth (sint w) n = bin_nth (sint w) (size w - 1)"
   612   apply (rule impI)
   613   apply (subst word_sbin.norm_Rep [symmetric])
   614   apply (simp add : nth_sbintr word_size)
   615   apply auto
   616   done
   617 
   618 lemmas bin_nth_uint_imp = bin_nth_uint_imp' [rule_format, unfolded word_size]
   619 lemmas bin_nth_sint = bin_nth_sint' [rule_format, unfolded word_size]
   620 
   621 (* type definitions theorem for in terms of equivalent bool list *)
   622 lemma td_bl: 
   623   "type_definition (to_bl :: 'a::len0 word => bool list) 
   624                    of_bl  
   625                    {bl. length bl = len_of TYPE('a)}"
   626   apply (unfold type_definition_def of_bl_def to_bl_def)
   627   apply (simp add: word_ubin.eq_norm)
   628   apply safe
   629   apply (drule sym)
   630   apply simp
   631   done
   632 
   633 interpretation word_bl:
   634   type_definition "to_bl :: 'a::len0 word => bool list"
   635                   of_bl  
   636                   "{bl. length bl = len_of TYPE('a::len0)}"
   637   by (rule td_bl)
   638 
   639 lemma word_size_bl: "size w == size (to_bl w)"
   640   unfolding word_size by auto
   641 
   642 lemma to_bl_use_of_bl:
   643   "(to_bl w = bl) = (w = of_bl bl \<and> length bl = length (to_bl w))"
   644   by (fastsimp elim!: word_bl.Abs_inverse [simplified])
   645 
   646 lemma to_bl_word_rev: "to_bl (word_reverse w) = rev (to_bl w)"
   647   unfolding word_reverse_def by (simp add: word_bl.Abs_inverse)
   648 
   649 lemma word_rev_rev [simp] : "word_reverse (word_reverse w) = w"
   650   unfolding word_reverse_def by (simp add : word_bl.Abs_inverse)
   651 
   652 lemma word_rev_gal: "word_reverse w = u ==> word_reverse u = w"
   653   by auto
   654 
   655 lemmas word_rev_gal' = sym [THEN word_rev_gal, symmetric, standard]
   656 
   657 lemmas length_bl_gt_0 [iff] = xtr1 [OF word_bl.Rep' len_gt_0, standard]
   658 lemmas bl_not_Nil [iff] = 
   659   length_bl_gt_0 [THEN length_greater_0_conv [THEN iffD1], standard]
   660 lemmas length_bl_neq_0 [iff] = length_bl_gt_0 [THEN gr_implies_not0]
   661 
   662 lemma hd_bl_sign_sint: "hd (to_bl w) = (bin_sign (sint w) = Int.Min)"
   663   apply (unfold to_bl_def sint_uint)
   664   apply (rule trans [OF _ bl_sbin_sign])
   665   apply simp
   666   done
   667 
   668 lemma of_bl_drop': 
   669   "lend = length bl - len_of TYPE ('a :: len0) ==> 
   670     of_bl (drop lend bl) = (of_bl bl :: 'a word)"
   671   apply (unfold of_bl_def)
   672   apply (clarsimp simp add : trunc_bl2bin [symmetric])
   673   done
   674 
   675 lemmas of_bl_no = of_bl_def [folded word_number_of_def]
   676 
   677 lemma test_bit_of_bl:  
   678   "(of_bl bl::'a::len0 word) !! n = (rev bl ! n \<and> n < len_of TYPE('a) \<and> n < length bl)"
   679   apply (unfold of_bl_def word_test_bit_def)
   680   apply (auto simp add: word_size word_ubin.eq_norm nth_bintr bin_nth_of_bl)
   681   done
   682 
   683 lemma no_of_bl: 
   684   "(number_of bin ::'a::len0 word) = of_bl (bin_to_bl (len_of TYPE ('a)) bin)"
   685   unfolding word_size of_bl_no by (simp add : word_number_of_def)
   686 
   687 lemma uint_bl: "to_bl w == bin_to_bl (size w) (uint w)"
   688   unfolding word_size to_bl_def by auto
   689 
   690 lemma to_bl_bin: "bl_to_bin (to_bl w) = uint w"
   691   unfolding uint_bl by (simp add : word_size)
   692 
   693 lemma to_bl_of_bin: 
   694   "to_bl (word_of_int bin::'a::len0 word) = bin_to_bl (len_of TYPE('a)) bin"
   695   unfolding uint_bl by (clarsimp simp add: word_ubin.eq_norm word_size)
   696 
   697 lemmas to_bl_no_bin [simp] = to_bl_of_bin [folded word_number_of_def]
   698 
   699 lemma to_bl_to_bin [simp] : "bl_to_bin (to_bl w) = uint w"
   700   unfolding uint_bl by (simp add : word_size)
   701   
   702 lemmas uint_bl_bin [simp] = trans [OF bin_bl_bin word_ubin.norm_Rep, standard]
   703 
   704 lemmas num_AB_u [simp] = word_uint.Rep_inverse 
   705   [unfolded o_def word_number_of_def [symmetric], standard]
   706 lemmas num_AB_s [simp] = word_sint.Rep_inverse 
   707   [unfolded o_def word_number_of_def [symmetric], standard]
   708 
   709 (* naturals *)
   710 lemma uints_unats: "uints n = int ` unats n"
   711   apply (unfold unats_def uints_num)
   712   apply safe
   713   apply (rule_tac image_eqI)
   714   apply (erule_tac nat_0_le [symmetric])
   715   apply auto
   716   apply (erule_tac nat_less_iff [THEN iffD2])
   717   apply (rule_tac [2] zless_nat_eq_int_zless [THEN iffD1])
   718   apply (auto simp add : nat_power_eq int_power)
   719   done
   720 
   721 lemma unats_uints: "unats n = nat ` uints n"
   722   by (auto simp add : uints_unats image_iff)
   723 
   724 lemmas bintr_num = word_ubin.norm_eq_iff 
   725   [symmetric, folded word_number_of_def, standard]
   726 lemmas sbintr_num = word_sbin.norm_eq_iff 
   727   [symmetric, folded word_number_of_def, standard]
   728 
   729 lemmas num_of_bintr = word_ubin.Abs_norm [folded word_number_of_def, standard]
   730 lemmas num_of_sbintr = word_sbin.Abs_norm [folded word_number_of_def, standard];
   731     
   732 (* don't add these to simpset, since may want bintrunc n w to be simplified;
   733   may want these in reverse, but loop as simp rules, so use following *)
   734 
   735 lemma num_of_bintr':
   736   "bintrunc (len_of TYPE('a :: len0)) a = b ==> 
   737     number_of a = (number_of b :: 'a word)"
   738   apply safe
   739   apply (rule_tac num_of_bintr [symmetric])
   740   done
   741 
   742 lemma num_of_sbintr':
   743   "sbintrunc (len_of TYPE('a :: len) - 1) a = b ==> 
   744     number_of a = (number_of b :: 'a word)"
   745   apply safe
   746   apply (rule_tac num_of_sbintr [symmetric])
   747   done
   748 
   749 lemmas num_abs_bintr = sym [THEN trans,
   750   OF num_of_bintr word_number_of_def, standard]
   751 lemmas num_abs_sbintr = sym [THEN trans,
   752   OF num_of_sbintr word_number_of_def, standard]
   753   
   754 (** cast - note, no arg for new length, as it's determined by type of result,
   755   thus in "cast w = w, the type means cast to length of w! **)
   756 
   757 lemma ucast_id: "ucast w = w"
   758   unfolding ucast_def by auto
   759 
   760 lemma scast_id: "scast w = w"
   761   unfolding scast_def by auto
   762 
   763 lemma ucast_bl: "ucast w == of_bl (to_bl w)"
   764   unfolding ucast_def of_bl_def uint_bl
   765   by (auto simp add : word_size)
   766 
   767 lemma nth_ucast: 
   768   "(ucast w::'a::len0 word) !! n = (w !! n & n < len_of TYPE('a))"
   769   apply (unfold ucast_def test_bit_bin)
   770   apply (simp add: word_ubin.eq_norm nth_bintr word_size) 
   771   apply (fast elim!: bin_nth_uint_imp)
   772   done
   773 
   774 (* for literal u(s)cast *)
   775 
   776 lemma ucast_bintr [simp]: 
   777   "ucast (number_of w ::'a::len0 word) = 
   778    number_of (bintrunc (len_of TYPE('a)) w)"
   779   unfolding ucast_def by simp
   780 
   781 lemma scast_sbintr [simp]: 
   782   "scast (number_of w ::'a::len word) = 
   783    number_of (sbintrunc (len_of TYPE('a) - Suc 0) w)"
   784   unfolding scast_def by simp
   785 
   786 lemmas source_size = source_size_def [unfolded Let_def word_size]
   787 lemmas target_size = target_size_def [unfolded Let_def word_size]
   788 lemmas is_down = is_down_def [unfolded source_size target_size]
   789 lemmas is_up = is_up_def [unfolded source_size target_size]
   790 
   791 lemmas is_up_down =  trans [OF is_up is_down [symmetric], standard]
   792 
   793 lemma down_cast_same': "uc = ucast ==> is_down uc ==> uc = scast"
   794   apply (unfold is_down)
   795   apply safe
   796   apply (rule ext)
   797   apply (unfold ucast_def scast_def uint_sint)
   798   apply (rule word_ubin.norm_eq_iff [THEN iffD1])
   799   apply simp
   800   done
   801 
   802 lemma word_rev_tf': 
   803   "r = to_bl (of_bl bl) ==> r = rev (takefill False (length r) (rev bl))"
   804   unfolding of_bl_def uint_bl
   805   by (clarsimp simp add: bl_bin_bl_rtf word_ubin.eq_norm word_size)
   806 
   807 lemmas word_rev_tf = refl [THEN word_rev_tf', unfolded word_bl.Rep', standard]
   808 
   809 lemmas word_rep_drop = word_rev_tf [simplified takefill_alt,
   810   simplified, simplified rev_take, simplified]
   811 
   812 lemma to_bl_ucast: 
   813   "to_bl (ucast (w::'b::len0 word) ::'a::len0 word) = 
   814    replicate (len_of TYPE('a) - len_of TYPE('b)) False @
   815    drop (len_of TYPE('b) - len_of TYPE('a)) (to_bl w)"
   816   apply (unfold ucast_bl)
   817   apply (rule trans)
   818    apply (rule word_rep_drop)
   819   apply simp
   820   done
   821 
   822 lemma ucast_up_app': 
   823   "uc = ucast ==> source_size uc + n = target_size uc ==> 
   824     to_bl (uc w) = replicate n False @ (to_bl w)"
   825   by (auto simp add : source_size target_size to_bl_ucast)
   826 
   827 lemma ucast_down_drop': 
   828   "uc = ucast ==> source_size uc = target_size uc + n ==> 
   829     to_bl (uc w) = drop n (to_bl w)"
   830   by (auto simp add : source_size target_size to_bl_ucast)
   831 
   832 lemma scast_down_drop': 
   833   "sc = scast ==> source_size sc = target_size sc + n ==> 
   834     to_bl (sc w) = drop n (to_bl w)"
   835   apply (subgoal_tac "sc = ucast")
   836    apply safe
   837    apply simp
   838    apply (erule refl [THEN ucast_down_drop'])
   839   apply (rule refl [THEN down_cast_same', symmetric])
   840   apply (simp add : source_size target_size is_down)
   841   done
   842 
   843 lemma sint_up_scast': 
   844   "sc = scast ==> is_up sc ==> sint (sc w) = sint w"
   845   apply (unfold is_up)
   846   apply safe
   847   apply (simp add: scast_def word_sbin.eq_norm)
   848   apply (rule box_equals)
   849     prefer 3
   850     apply (rule word_sbin.norm_Rep)
   851    apply (rule sbintrunc_sbintrunc_l)
   852    defer
   853    apply (subst word_sbin.norm_Rep)
   854    apply (rule refl)
   855   apply simp
   856   done
   857 
   858 lemma uint_up_ucast':
   859   "uc = ucast ==> is_up uc ==> uint (uc w) = uint w"
   860   apply (unfold is_up)
   861   apply safe
   862   apply (rule bin_eqI)
   863   apply (fold word_test_bit_def)
   864   apply (auto simp add: nth_ucast)
   865   apply (auto simp add: test_bit_bin)
   866   done
   867     
   868 lemmas down_cast_same = refl [THEN down_cast_same']
   869 lemmas ucast_up_app = refl [THEN ucast_up_app']
   870 lemmas ucast_down_drop = refl [THEN ucast_down_drop']
   871 lemmas scast_down_drop = refl [THEN scast_down_drop']
   872 lemmas uint_up_ucast = refl [THEN uint_up_ucast']
   873 lemmas sint_up_scast = refl [THEN sint_up_scast']
   874 
   875 lemma ucast_up_ucast': "uc = ucast ==> is_up uc ==> ucast (uc w) = ucast w"
   876   apply (simp (no_asm) add: ucast_def)
   877   apply (clarsimp simp add: uint_up_ucast)
   878   done
   879     
   880 lemma scast_up_scast': "sc = scast ==> is_up sc ==> scast (sc w) = scast w"
   881   apply (simp (no_asm) add: scast_def)
   882   apply (clarsimp simp add: sint_up_scast)
   883   done
   884     
   885 lemma ucast_of_bl_up': 
   886   "w = of_bl bl ==> size bl <= size w ==> ucast w = of_bl bl"
   887   by (auto simp add : nth_ucast word_size test_bit_of_bl intro!: word_eqI)
   888 
   889 lemmas ucast_up_ucast = refl [THEN ucast_up_ucast']
   890 lemmas scast_up_scast = refl [THEN scast_up_scast']
   891 lemmas ucast_of_bl_up = refl [THEN ucast_of_bl_up']
   892 
   893 lemmas ucast_up_ucast_id = trans [OF ucast_up_ucast ucast_id]
   894 lemmas scast_up_scast_id = trans [OF scast_up_scast scast_id]
   895 
   896 lemmas isduu = is_up_down [where c = "ucast", THEN iffD2]
   897 lemmas isdus = is_up_down [where c = "scast", THEN iffD2]
   898 lemmas ucast_down_ucast_id = isduu [THEN ucast_up_ucast_id]
   899 lemmas scast_down_scast_id = isdus [THEN ucast_up_ucast_id]
   900 
   901 lemma up_ucast_surj:
   902   "is_up (ucast :: 'b::len0 word => 'a::len0 word) ==> 
   903    surj (ucast :: 'a word => 'b word)"
   904   by (rule surjI, erule ucast_up_ucast_id)
   905 
   906 lemma up_scast_surj:
   907   "is_up (scast :: 'b::len word => 'a::len word) ==> 
   908    surj (scast :: 'a word => 'b word)"
   909   by (rule surjI, erule scast_up_scast_id)
   910 
   911 lemma down_scast_inj:
   912   "is_down (scast :: 'b::len word => 'a::len word) ==> 
   913    inj_on (ucast :: 'a word => 'b word) A"
   914   by (rule inj_on_inverseI, erule scast_down_scast_id)
   915 
   916 lemma down_ucast_inj:
   917   "is_down (ucast :: 'b::len0 word => 'a::len0 word) ==> 
   918    inj_on (ucast :: 'a word => 'b word) A"
   919   by (rule inj_on_inverseI, erule ucast_down_ucast_id)
   920 
   921 lemma of_bl_append_same: "of_bl (X @ to_bl w) = w"
   922   by (rule word_bl.Rep_eqD) (simp add: word_rep_drop)
   923   
   924 lemma ucast_down_no': 
   925   "uc = ucast ==> is_down uc ==> uc (number_of bin) = number_of bin"
   926   apply (unfold word_number_of_def is_down)
   927   apply (clarsimp simp add: ucast_def word_ubin.eq_norm)
   928   apply (rule word_ubin.norm_eq_iff [THEN iffD1])
   929   apply (erule bintrunc_bintrunc_ge)
   930   done
   931     
   932 lemmas ucast_down_no = ucast_down_no' [OF refl]
   933 
   934 lemma ucast_down_bl': "uc = ucast ==> is_down uc ==> uc (of_bl bl) = of_bl bl"
   935   unfolding of_bl_no by clarify (erule ucast_down_no)
   936     
   937 lemmas ucast_down_bl = ucast_down_bl' [OF refl]
   938 
   939 lemmas slice_def' = slice_def [unfolded word_size]
   940 lemmas test_bit_def' = word_test_bit_def [THEN fun_cong]
   941 
   942 lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def
   943 lemmas word_log_bin_defs = word_log_defs
   944 
   945 text {* Executable equality *}
   946 
   947 instantiation word :: ("{len0}") eq
   948 begin
   949 
   950 definition eq_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" where
   951   "eq_word k l \<longleftrightarrow> HOL.eq (uint k) (uint l)"
   952 
   953 instance proof
   954 qed (simp add: eq eq_word_def)
   955 
   956 end
   957 
   958 end