src/HOL/Word/WordArith.thy
author chaieb
Sat Oct 20 12:09:33 2007 +0200 (2007-10-20)
changeset 25112 98824cc791c0
parent 24465 70f0214b3ecc
child 25134 3d4953e88449
permissions -rw-r--r--
fixed proofs
     1 (* 
     2     ID:         $Id$
     3     Author:     Jeremy Dawson and Gerwin Klein, NICTA
     4 
     5   contains arithmetic theorems for word, instantiations to
     6   arithmetic type classes and tactics for reducing word arithmetic
     7   to linear arithmetic on int or nat
     8 *) 
     9 
    10 header {* Word Arithmetic *}
    11 
    12 theory WordArith imports WordDefinition begin
    13 
    14 
    15 lemma word_less_alt: "(a < b) = (uint a < uint b)"
    16   unfolding word_less_def word_le_def
    17   by (auto simp del: word_uint.Rep_inject 
    18            simp: word_uint.Rep_inject [symmetric])
    19 
    20 lemma signed_linorder: "linorder word_sle word_sless"
    21   apply unfold_locales
    22       apply (unfold word_sle_def word_sless_def) 
    23   by auto 
    24 
    25 interpretation signed: linorder ["word_sle" "word_sless"] 
    26   by (rule signed_linorder)
    27 
    28 lemmas word_arith_wis [THEN meta_eq_to_obj_eq] = 
    29   word_add_def word_mult_def word_minus_def 
    30   word_succ_def word_pred_def word_0_wi word_1_wi
    31 
    32 lemma udvdI: 
    33   "0 \<le> n ==> uint b = n * uint a ==> a udvd b"
    34   by (auto simp: udvd_def)
    35 
    36 lemmas word_div_no [simp] = 
    37   word_div_def [of "number_of ?a" "number_of ?b"]
    38 
    39 lemmas word_mod_no [simp] = 
    40   word_mod_def [of "number_of ?a" "number_of ?b"]
    41 
    42 lemmas word_less_no [simp] = 
    43   word_less_def [of "number_of ?a" "number_of ?b"]
    44 
    45 lemmas word_le_no [simp] = 
    46   word_le_def [of "number_of ?a" "number_of ?b"]
    47 
    48 lemmas word_sless_no [simp] = 
    49   word_sless_def [of "number_of ?a" "number_of ?b"]
    50 
    51 lemmas word_sle_no [simp] = 
    52   word_sle_def [of "number_of ?a" "number_of ?b"]
    53 
    54 (* following two are available in class number_ring, 
    55   but convenient to have them here here;
    56   note - the number_ring versions, numeral_0_eq_0 and numeral_1_eq_1
    57   are in the default simpset, so to use the automatic simplifications for
    58   (eg) sint (number_of bin) on sint 1, must do
    59   (simp add: word_1_no del: numeral_1_eq_1) 
    60   *)
    61 lemmas word_0_wi_Pls = word_0_wi [folded Pls_def]
    62 lemmas word_0_no = word_0_wi_Pls [folded word_no_wi]
    63 
    64 lemma int_one_bin: "(1 :: int) == (Numeral.Pls BIT bit.B1)"
    65   unfolding Pls_def Bit_def by auto
    66 
    67 lemma word_1_no: 
    68   "(1 :: 'a :: len0 word) == number_of (Numeral.Pls BIT bit.B1)"
    69   unfolding word_1_wi word_number_of_def int_one_bin by auto
    70 
    71 lemma word_m1_wi: "-1 == word_of_int -1" 
    72   by (rule word_number_of_alt)
    73 
    74 lemma word_m1_wi_Min: "-1 = word_of_int Numeral.Min"
    75   by (simp add: word_m1_wi number_of_eq)
    76 
    77 lemma word_0_bl: "of_bl [] = 0" 
    78   unfolding word_0_wi of_bl_def by (simp add : Pls_def)
    79 
    80 lemma word_1_bl: "of_bl [True] = 1" 
    81   unfolding word_1_wi of_bl_def
    82   by (simp add : bl_to_bin_def Bit_def Pls_def)
    83 
    84 lemma uint_0 [simp] : "(uint 0 = 0)" 
    85   unfolding word_0_wi
    86   by (simp add: word_ubin.eq_norm Pls_def [symmetric])
    87 
    88 lemma of_bl_0 [simp] : "of_bl (replicate n False) = 0"
    89   by (simp add : word_0_wi of_bl_def bl_to_bin_rep_False Pls_def)
    90 
    91 lemma to_bl_0: 
    92   "to_bl (0::'a::len0 word) = replicate (len_of TYPE('a)) False"
    93   unfolding uint_bl
    94   by (simp add : word_size bin_to_bl_Pls Pls_def [symmetric])
    95 
    96 lemma uint_0_iff: "(uint x = 0) = (x = 0)"
    97   by (auto intro!: word_uint.Rep_eqD)
    98 
    99 lemma unat_0_iff: "(unat x = 0) = (x = 0)"
   100   unfolding unat_def by (auto simp add : nat_eq_iff uint_0_iff)
   101 
   102 lemma unat_0 [simp]: "unat 0 = 0"
   103   unfolding unat_def by auto
   104 
   105 lemma size_0_same': "size w = 0 ==> w = (v :: 'a :: len0 word)"
   106   apply (unfold word_size)
   107   apply (rule box_equals)
   108     defer
   109     apply (rule word_uint.Rep_inverse)+
   110   apply (rule word_ubin.norm_eq_iff [THEN iffD1])
   111   apply simp
   112   done
   113 
   114 lemmas size_0_same = size_0_same' [folded word_size]
   115 
   116 lemmas unat_eq_0 = unat_0_iff
   117 lemmas unat_eq_zero = unat_0_iff
   118 
   119 lemma unat_gt_0: "(0 < unat x) = (x ~= 0)"
   120   by (simp add : neq0_conv unat_0_iff [symmetric])
   121 
   122 lemma ucast_0 [simp] : "ucast 0 = 0"
   123   unfolding ucast_def
   124   by simp (simp add: word_0_wi)
   125 
   126 lemma sint_0 [simp] : "sint 0 = 0"
   127   unfolding sint_uint
   128   by (simp add: Pls_def [symmetric])
   129 
   130 lemma scast_0 [simp] : "scast 0 = 0"
   131   apply (unfold scast_def)
   132   apply simp
   133   apply (simp add: word_0_wi)
   134   done
   135 
   136 lemma sint_n1 [simp] : "sint -1 = -1"
   137   apply (unfold word_m1_wi_Min)
   138   apply (simp add: word_sbin.eq_norm)
   139   apply (unfold Min_def number_of_eq)
   140   apply simp
   141   done
   142 
   143 lemma scast_n1 [simp] : "scast -1 = -1"
   144   apply (unfold scast_def sint_n1)
   145   apply (unfold word_number_of_alt)
   146   apply (rule refl)
   147   done
   148 
   149 lemma uint_1 [simp] : "uint (1 :: 'a :: len word) = 1"
   150   unfolding word_1_wi
   151   by (simp add: word_ubin.eq_norm int_one_bin bintrunc_minus_simps)
   152 
   153 lemma unat_1 [simp] : "unat (1 :: 'a :: len word) = 1"
   154   by (unfold unat_def uint_1) auto
   155 
   156 lemma ucast_1 [simp] : "ucast (1 :: 'a :: len word) = 1"
   157   unfolding ucast_def word_1_wi
   158   by (simp add: word_ubin.eq_norm int_one_bin bintrunc_minus_simps)
   159 
   160 (* abstraction preserves the operations
   161   (the definitions tell this for bins in range uint) *)
   162 
   163 lemmas arths = 
   164   bintr_ariths [THEN word_ubin.norm_eq_iff [THEN iffD1],
   165                 folded word_ubin.eq_norm, standard]
   166 
   167 lemma wi_homs: 
   168   shows
   169   wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" and
   170   wi_hom_mult: "word_of_int a * word_of_int b = word_of_int (a * b)" and
   171   wi_hom_neg: "- word_of_int a = word_of_int (- a)" and
   172   wi_hom_succ: "word_succ (word_of_int a) = word_of_int (Numeral.succ a)" and
   173   wi_hom_pred: "word_pred (word_of_int a) = word_of_int (Numeral.pred a)"
   174   by (auto simp: word_arith_wis arths)
   175 
   176 lemmas wi_hom_syms = wi_homs [symmetric]
   177 
   178 lemma word_sub_def: "a - b == a + - (b :: 'a :: len0 word)"
   179   unfolding word_sub_wi diff_def
   180   by (simp only : word_uint.Rep_inverse wi_hom_syms)
   181     
   182 lemmas word_diff_minus = word_sub_def [THEN meta_eq_to_obj_eq, standard]
   183 
   184 lemma word_of_int_sub_hom:
   185   "(word_of_int a) - word_of_int b = word_of_int (a - b)"
   186   unfolding word_sub_def diff_def by (simp only : wi_homs)
   187 
   188 lemmas new_word_of_int_homs = 
   189   word_of_int_sub_hom wi_homs word_0_wi word_1_wi 
   190 
   191 lemmas new_word_of_int_hom_syms = new_word_of_int_homs [symmetric, standard]
   192 
   193 lemmas word_of_int_hom_syms =
   194   new_word_of_int_hom_syms [unfolded succ_def pred_def]
   195 
   196 lemmas word_of_int_homs =
   197   new_word_of_int_homs [unfolded succ_def pred_def]
   198 
   199 lemmas word_of_int_add_hom = word_of_int_homs (2)
   200 lemmas word_of_int_mult_hom = word_of_int_homs (3)
   201 lemmas word_of_int_minus_hom = word_of_int_homs (4)
   202 lemmas word_of_int_succ_hom = word_of_int_homs (5)
   203 lemmas word_of_int_pred_hom = word_of_int_homs (6)
   204 lemmas word_of_int_0_hom = word_of_int_homs (7)
   205 lemmas word_of_int_1_hom = word_of_int_homs (8)
   206 
   207 (* now, to get the weaker results analogous to word_div/mod_def *)
   208 
   209 lemmas word_arith_alts = 
   210   word_sub_wi [unfolded succ_def pred_def, THEN meta_eq_to_obj_eq, standard]
   211   word_arith_wis [unfolded succ_def pred_def, standard]
   212 
   213 lemmas word_sub_alt = word_arith_alts (1)
   214 lemmas word_add_alt = word_arith_alts (2)
   215 lemmas word_mult_alt = word_arith_alts (3)
   216 lemmas word_minus_alt = word_arith_alts (4)
   217 lemmas word_succ_alt = word_arith_alts (5)
   218 lemmas word_pred_alt = word_arith_alts (6)
   219 lemmas word_0_alt = word_arith_alts (7)
   220 lemmas word_1_alt = word_arith_alts (8)
   221 
   222 subsection  "Transferring goals from words to ints"
   223 
   224 lemma word_ths:  
   225   shows
   226   word_succ_p1:   "word_succ a = a + 1" and
   227   word_pred_m1:   "word_pred a = a - 1" and
   228   word_pred_succ: "word_pred (word_succ a) = a" and
   229   word_succ_pred: "word_succ (word_pred a) = a" and
   230   word_mult_succ: "word_succ a * b = b + a * b"
   231   by (rule word_uint.Abs_cases [of b],
   232       rule word_uint.Abs_cases [of a],
   233       simp add: pred_def succ_def add_commute mult_commute 
   234                 ring_distribs new_word_of_int_homs)+
   235 
   236 lemmas uint_cong = arg_cong [where f = uint]
   237 
   238 lemmas uint_word_ariths = 
   239   word_arith_alts [THEN trans [OF uint_cong int_word_uint], standard]
   240 
   241 lemmas uint_word_arith_bintrs = uint_word_ariths [folded bintrunc_mod2p]
   242 
   243 (* similar expressions for sint (arith operations) *)
   244 lemmas sint_word_ariths = uint_word_arith_bintrs
   245   [THEN uint_sint [symmetric, THEN trans],
   246   unfolded uint_sint bintr_arith1s bintr_ariths 
   247     len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep, standard]
   248 
   249 lemmas uint_div_alt = word_div_def
   250   [THEN meta_eq_to_obj_eq [THEN trans [OF uint_cong int_word_uint]], standard]
   251 lemmas uint_mod_alt = word_mod_def
   252   [THEN meta_eq_to_obj_eq [THEN trans [OF uint_cong int_word_uint]], standard]
   253 
   254 lemma word_pred_0_n1: "word_pred 0 = word_of_int -1"
   255   unfolding word_pred_def number_of_eq
   256   by (simp add : pred_def word_no_wi)
   257 
   258 lemma word_pred_0_Min: "word_pred 0 = word_of_int Numeral.Min"
   259   by (simp add: word_pred_0_n1 number_of_eq)
   260 
   261 lemma word_m1_Min: "- 1 = word_of_int Numeral.Min"
   262   unfolding Min_def by (simp only: word_of_int_hom_syms)
   263 
   264 lemma succ_pred_no [simp]:
   265   "word_succ (number_of bin) = number_of (Numeral.succ bin) & 
   266     word_pred (number_of bin) = number_of (Numeral.pred bin)"
   267   unfolding word_number_of_def by (simp add : new_word_of_int_homs)
   268 
   269 lemma word_sp_01 [simp] : 
   270   "word_succ -1 = 0 & word_succ 0 = 1 & word_pred 0 = -1 & word_pred 1 = 0"
   271   by (unfold word_0_no word_1_no) auto
   272 
   273 (* alternative approach to lifting arithmetic equalities *)
   274 lemma word_of_int_Ex:
   275   "\<exists>y. x = word_of_int y"
   276   by (rule_tac x="uint x" in exI) simp
   277 
   278 lemma word_arith_eqs:
   279   fixes a :: "'a::len0 word"
   280   fixes b :: "'a::len0 word"
   281   shows
   282   word_add_0: "0 + a = a" and
   283   word_add_0_right: "a + 0 = a" and
   284   word_mult_1: "1 * a = a" and
   285   word_mult_1_right: "a * 1 = a" and
   286   word_add_commute: "a + b = b + a" and
   287   word_add_assoc: "a + b + c = a + (b + c)" and
   288   word_add_left_commute: "a + (b + c) = b + (a + c)" and
   289   word_mult_commute: "a * b = b * a" and
   290   word_mult_assoc: "a * b * c = a * (b * c)" and
   291   word_mult_left_commute: "a * (b * c) = b * (a * c)" and
   292   word_left_distrib: "(a + b) * c = a * c + b * c" and
   293   word_right_distrib: "a * (b + c) = a * b + a * c" and
   294   word_left_minus: "- a + a = 0" and
   295   word_diff_0_right: "a - 0 = a" and
   296   word_diff_self: "a - a = 0"
   297   using word_of_int_Ex [of a] 
   298         word_of_int_Ex [of b] 
   299         word_of_int_Ex [of c]
   300   by (auto simp: word_of_int_hom_syms [symmetric]
   301                  zadd_0_right add_commute add_assoc add_left_commute
   302                  mult_commute mult_assoc mult_left_commute
   303                  plus_times.left_distrib plus_times.right_distrib)
   304   
   305 lemmas word_add_ac = word_add_commute word_add_assoc word_add_left_commute
   306 lemmas word_mult_ac = word_mult_commute word_mult_assoc word_mult_left_commute
   307   
   308 lemmas word_plus_ac0 = word_add_0 word_add_0_right word_add_ac
   309 lemmas word_times_ac1 = word_mult_1 word_mult_1_right word_mult_ac
   310 
   311 
   312 subsection "Order on fixed-length words"
   313 
   314 lemma word_order_trans: "x <= y ==> y <= z ==> x <= (z :: 'a :: len0 word)"
   315   unfolding word_le_def by auto
   316 
   317 lemma word_order_refl: "z <= (z :: 'a :: len0 word)"
   318   unfolding word_le_def by auto
   319 
   320 lemma word_order_antisym: "x <= y ==> y <= x ==> x = (y :: 'a :: len0 word)"
   321   unfolding word_le_def by (auto intro!: word_uint.Rep_eqD)
   322 
   323 lemma word_order_linear:
   324   "y <= x | x <= (y :: 'a :: len0 word)"
   325   unfolding word_le_def by auto
   326 
   327 lemma word_zero_le [simp] :
   328   "0 <= (y :: 'a :: len0 word)"
   329   unfolding word_le_def by auto
   330   
   331 instance word :: (len0) semigroup_add
   332   by intro_classes (simp add: word_add_assoc)
   333 
   334 instance word :: (len0) linorder
   335   by intro_classes (auto simp: word_less_def word_le_def)
   336 
   337 instance word :: (len0) ring
   338   by intro_classes
   339      (auto simp: word_arith_eqs word_diff_minus 
   340                  word_diff_self [unfolded word_diff_minus])
   341 
   342 lemma word_m1_ge [simp] : "word_pred 0 >= y"
   343   unfolding word_le_def
   344   by (simp only : word_pred_0_n1 word_uint.eq_norm m1mod2k) auto
   345 
   346 lemmas word_n1_ge [simp]  = word_m1_ge [simplified word_sp_01]
   347 
   348 lemmas word_not_simps [simp] = 
   349   word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD]
   350 
   351 lemma word_gt_0: "0 < y = (0 ~= (y :: 'a :: len0 word))"
   352   unfolding word_less_def by auto
   353 
   354 lemmas word_gt_0_no [simp] = word_gt_0 [of "number_of ?y"]
   355 
   356 lemma word_sless_alt: "(a <s b) == (sint a < sint b)"
   357   unfolding word_sle_def word_sless_def
   358   by (auto simp add : less_eq_less.less_le)
   359 
   360 lemma word_le_nat_alt: "(a <= b) = (unat a <= unat b)"
   361   unfolding unat_def word_le_def
   362   by (rule nat_le_eq_zle [symmetric]) simp
   363 
   364 lemma word_less_nat_alt: "(a < b) = (unat a < unat b)"
   365   unfolding unat_def word_less_alt
   366   by (rule nat_less_eq_zless [symmetric]) simp
   367   
   368 lemma wi_less: 
   369   "(word_of_int n < (word_of_int m :: 'a :: len0 word)) = 
   370     (n mod 2 ^ len_of TYPE('a) < m mod 2 ^ len_of TYPE('a))"
   371   unfolding word_less_alt by (simp add: word_uint.eq_norm)
   372 
   373 lemma wi_le: 
   374   "(word_of_int n <= (word_of_int m :: 'a :: len0 word)) = 
   375     (n mod 2 ^ len_of TYPE('a) <= m mod 2 ^ len_of TYPE('a))"
   376   unfolding word_le_def by (simp add: word_uint.eq_norm)
   377 
   378 lemma udvd_nat_alt: "a udvd b = (EX n>=0. unat b = n * unat a)"
   379   apply (unfold udvd_def)
   380   apply safe
   381    apply (simp add: unat_def nat_mult_distrib)
   382   apply (simp add: uint_nat int_mult)
   383   apply (rule exI)
   384   apply safe
   385    prefer 2
   386    apply (erule notE)
   387    apply (rule refl)
   388   apply force
   389   done
   390 
   391 lemma udvd_iff_dvd: "x udvd y <-> unat x dvd unat y"
   392   unfolding dvd_def udvd_nat_alt by force
   393 
   394 lemmas unat_mono = word_less_nat_alt [THEN iffD1, standard]
   395 
   396 lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) ==> (0 :: 'a word) ~= 1";
   397   unfolding word_arith_wis
   398   by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
   399 
   400 lemmas lenw1_zero_neq_one = len_gt_0 [THEN word_zero_neq_one]
   401 
   402 lemma no_no [simp] : "number_of (number_of b) = number_of b"
   403   by (simp add: number_of_eq)
   404 
   405 lemma unat_minus_one: "x ~= 0 ==> unat (x - 1) = unat x - 1"
   406   apply (unfold unat_def)
   407   apply (simp only: int_word_uint word_arith_alts rdmods)
   408   apply (subgoal_tac "uint x >= 1")
   409    prefer 2
   410    apply (drule contrapos_nn)
   411     apply (erule word_uint.Rep_inverse' [symmetric])
   412    apply (insert uint_ge_0 [of x])[1]
   413    apply arith
   414   apply (rule box_equals)
   415     apply (rule nat_diff_distrib)
   416      prefer 2
   417      apply assumption
   418     apply simp
   419    apply (subst mod_pos_pos_trivial)
   420      apply arith
   421     apply (insert uint_lt2p [of x])[1]
   422     apply arith
   423    apply (rule refl)
   424   apply simp
   425   done
   426     
   427 lemma measure_unat: "p ~= 0 ==> unat (p - 1) < unat p"
   428   by (simp add: unat_minus_one) (simp add: unat_0_iff [symmetric])
   429   
   430 lemmas uint_add_ge0 [simp] =
   431   add_nonneg_nonneg [OF uint_ge_0 uint_ge_0, standard]
   432 lemmas uint_mult_ge0 [simp] =
   433   mult_nonneg_nonneg [OF uint_ge_0 uint_ge_0, standard]
   434 
   435 lemma uint_sub_lt2p [simp]: 
   436   "uint (x :: 'a :: len0 word) - uint (y :: 'b :: len0 word) < 
   437     2 ^ len_of TYPE('a)"
   438   using uint_ge_0 [of y] uint_lt2p [of x] by arith
   439 
   440 
   441 subsection "Conditions for the addition (etc) of two words to overflow"
   442 
   443 lemma uint_add_lem: 
   444   "(uint x + uint y < 2 ^ len_of TYPE('a)) = 
   445     (uint (x + y :: 'a :: len0 word) = uint x + uint y)"
   446   by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
   447 
   448 lemma uint_mult_lem: 
   449   "(uint x * uint y < 2 ^ len_of TYPE('a)) = 
   450     (uint (x * y :: 'a :: len0 word) = uint x * uint y)"
   451   by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
   452 
   453 lemma uint_sub_lem: 
   454   "(uint x >= uint y) = (uint (x - y) = uint x - uint y)"
   455   by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
   456 
   457 lemma uint_add_le: "uint (x + y) <= uint x + uint y"
   458   unfolding uint_word_ariths by (auto simp: mod_add_if_z)
   459 
   460 lemma uint_sub_ge: "uint (x - y) >= uint x - uint y"
   461   unfolding uint_word_ariths by (auto simp: mod_sub_if_z)
   462 
   463 lemmas uint_sub_if' =
   464   trans [OF uint_word_ariths(1) mod_sub_if_z, simplified, standard]
   465 lemmas uint_plus_if' =
   466   trans [OF uint_word_ariths(2) mod_add_if_z, simplified, standard]
   467 
   468 
   469 subsection {* Definition of uint\_arith *}
   470 
   471 lemma word_of_int_inverse:
   472   "word_of_int r = a ==> 0 <= r ==> r < 2 ^ len_of TYPE('a) ==> 
   473    uint (a::'a::len0 word) = r"
   474   apply (erule word_uint.Abs_inverse' [rotated])
   475   apply (simp add: uints_num)
   476   done
   477 
   478 lemma uint_split:
   479   fixes x::"'a::len0 word"
   480   shows "P (uint x) = 
   481          (ALL i. word_of_int i = x & 0 <= i & i < 2^len_of TYPE('a) --> P i)"
   482   apply (fold word_int_case_def)
   483   apply (auto dest!: word_of_int_inverse simp: int_word_uint int_mod_eq'
   484               split: word_int_split)
   485   done
   486 
   487 lemma uint_split_asm:
   488   fixes x::"'a::len0 word"
   489   shows "P (uint x) = 
   490          (~(EX i. word_of_int i = x & 0 <= i & i < 2^len_of TYPE('a) & ~ P i))"
   491   by (auto dest!: word_of_int_inverse 
   492            simp: int_word_uint int_mod_eq'
   493            split: uint_split)
   494 
   495 lemmas uint_splits = uint_split uint_split_asm
   496 
   497 lemmas uint_arith_simps = 
   498   word_le_def word_less_alt
   499   word_uint.Rep_inject [symmetric] 
   500   uint_sub_if' uint_plus_if'
   501 
   502 (* use this to stop, eg, 2 ^ len_of TYPE (32) being simplified *)
   503 lemma power_False_cong: "False ==> a ^ b = c ^ d" 
   504   by auto
   505 
   506 (* uint_arith_tac: reduce to arithmetic on int, try to solve by arith *)
   507 ML {*
   508 fun uint_arith_ss_of ss = 
   509   ss addsimps @{thms uint_arith_simps}
   510      delsimps @{thms word_uint.Rep_inject}
   511      addsplits @{thms split_if_asm} 
   512      addcongs @{thms power_False_cong}
   513 
   514 fun uint_arith_tacs ctxt = 
   515   let fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty  
   516   in 
   517     [ CLASET' clarify_tac 1,
   518       SIMPSET' (full_simp_tac o uint_arith_ss_of) 1,
   519       ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms uint_splits} 
   520                                       addcongs @{thms power_False_cong})),
   521       rewrite_goals_tac @{thms word_size}, 
   522       ALLGOALS  (fn n => REPEAT (resolve_tac [allI, impI] n) THEN      
   523                          REPEAT (etac conjE n) THEN
   524                          REPEAT (dtac @{thm word_of_int_inverse} n 
   525                                  THEN atac n 
   526                                  THEN atac n)),
   527       TRYALL arith_tac' ]
   528   end
   529 
   530 fun uint_arith_tac ctxt = SELECT_GOAL (EVERY (uint_arith_tacs ctxt))
   531 *}
   532 
   533 method_setup uint_arith = 
   534   "Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (uint_arith_tac ctxt 1))" 
   535   "solving word arithmetic via integers and arith"
   536 
   537 
   538 subsection "More on overflows and monotonicity"
   539 
   540 lemma no_plus_overflow_uint_size: 
   541   "((x :: 'a :: len0 word) <= x + y) = (uint x + uint y < 2 ^ size x)"
   542   unfolding word_size by uint_arith
   543 
   544 lemmas no_olen_add = no_plus_overflow_uint_size [unfolded word_size]
   545 
   546 lemma no_ulen_sub: "((x :: 'a :: len0 word) >= x - y) = (uint y <= uint x)"
   547   by uint_arith
   548 
   549 lemma no_olen_add':
   550   fixes x :: "'a::len0 word"
   551   shows "(x \<le> y + x) = (uint y + uint x < 2 ^ len_of TYPE('a))"
   552   by (simp add: word_add_ac add_ac no_olen_add)
   553 
   554 lemmas olen_add_eqv = trans [OF no_olen_add no_olen_add' [symmetric], standard]
   555 
   556 lemmas uint_plus_simple_iff = trans [OF no_olen_add uint_add_lem, standard]
   557 lemmas uint_plus_simple = uint_plus_simple_iff [THEN iffD1, standard]
   558 lemmas uint_minus_simple_iff = trans [OF no_ulen_sub uint_sub_lem, standard]
   559 lemmas uint_minus_simple_alt = uint_sub_lem [folded word_le_def]
   560 lemmas word_sub_le_iff = no_ulen_sub [folded word_le_def]
   561 lemmas word_sub_le = word_sub_le_iff [THEN iffD2, standard]
   562 
   563 lemma word_less_sub1: 
   564   "(x :: 'a :: len word) ~= 0 ==> (1 < x) = (0 < x - 1)"
   565   by uint_arith
   566 
   567 lemma word_le_sub1: 
   568   "(x :: 'a :: len word) ~= 0 ==> (1 <= x) = (0 <= x - 1)"
   569   by uint_arith
   570 
   571 lemma sub_wrap_lt: 
   572   "((x :: 'a :: len0 word) < x - z) = (x < z)"
   573   by uint_arith
   574 
   575 lemma sub_wrap: 
   576   "((x :: 'a :: len0 word) <= x - z) = (z = 0 | x < z)"
   577   by uint_arith
   578 
   579 lemma plus_minus_not_NULL_ab: 
   580   "(x :: 'a :: len0 word) <= ab - c ==> c <= ab ==> c ~= 0 ==> x + c ~= 0"
   581   by uint_arith
   582 
   583 lemma plus_minus_no_overflow_ab: 
   584   "(x :: 'a :: len0 word) <= ab - c ==> c <= ab ==> x <= x + c" 
   585   by uint_arith
   586 
   587 lemma le_minus': 
   588   "(a :: 'a :: len0 word) + c <= b ==> a <= a + c ==> c <= b - a"
   589   by uint_arith
   590 
   591 lemma le_plus': 
   592   "(a :: 'a :: len0 word) <= b ==> c <= b - a ==> a + c <= b"
   593   by uint_arith
   594 
   595 lemmas le_plus = le_plus' [rotated]
   596 
   597 lemmas le_minus = leD [THEN thin_rl, THEN le_minus', standard]
   598 
   599 lemma word_plus_mono_right: 
   600   "(y :: 'a :: len0 word) <= z ==> x <= x + z ==> x + y <= x + z"
   601   by uint_arith
   602 
   603 lemma word_less_minus_cancel: 
   604   "y - x < z - x ==> x <= z ==> (y :: 'a :: len0 word) < z"
   605   by uint_arith
   606 
   607 lemma word_less_minus_mono_left: 
   608   "(y :: 'a :: len0 word) < z ==> x <= y ==> y - x < z - x"
   609   by uint_arith
   610 
   611 lemma word_less_minus_mono:  
   612   "a < c ==> d < b ==> a - b < a ==> c - d < c 
   613   ==> a - b < c - (d::'a::len word)"
   614   by uint_arith
   615 
   616 lemma word_le_minus_cancel: 
   617   "y - x <= z - x ==> x <= z ==> (y :: 'a :: len0 word) <= z"
   618   by uint_arith
   619 
   620 lemma word_le_minus_mono_left: 
   621   "(y :: 'a :: len0 word) <= z ==> x <= y ==> y - x <= z - x"
   622   by uint_arith
   623 
   624 lemma word_le_minus_mono:  
   625   "a <= c ==> d <= b ==> a - b <= a ==> c - d <= c 
   626   ==> a - b <= c - (d::'a::len word)"
   627   by uint_arith
   628 
   629 lemma plus_le_left_cancel_wrap: 
   630   "(x :: 'a :: len0 word) + y' < x ==> x + y < x ==> (x + y' < x + y) = (y' < y)"
   631   by uint_arith
   632 
   633 lemma plus_le_left_cancel_nowrap: 
   634   "(x :: 'a :: len0 word) <= x + y' ==> x <= x + y ==> 
   635     (x + y' < x + y) = (y' < y)" 
   636   by uint_arith
   637 
   638 lemma word_plus_mono_right2: 
   639   "(a :: 'a :: len0 word) <= a + b ==> c <= b ==> a <= a + c"
   640   by uint_arith
   641 
   642 lemma word_less_add_right: 
   643   "(x :: 'a :: len0 word) < y - z ==> z <= y ==> x + z < y"
   644   by uint_arith
   645 
   646 lemma word_less_sub_right: 
   647   "(x :: 'a :: len0 word) < y + z ==> y <= x ==> x - y < z"
   648   by uint_arith
   649 
   650 lemma word_le_plus_either: 
   651   "(x :: 'a :: len0 word) <= y | x <= z ==> y <= y + z ==> x <= y + z"
   652   by uint_arith
   653 
   654 lemma word_less_nowrapI: 
   655   "(x :: 'a :: len0 word) < z - k ==> k <= z ==> 0 < k ==> x < x + k"
   656   by uint_arith
   657 
   658 lemma inc_le: "(i :: 'a :: len word) < m ==> i + 1 <= m"
   659   by uint_arith
   660 
   661 lemma inc_i: 
   662   "(1 :: 'a :: len word) <= i ==> i < m ==> 1 <= (i + 1) & i + 1 <= m"
   663   by uint_arith
   664 
   665 lemma udvd_incr_lem:
   666   "up < uq ==> up = ua + n * uint K ==> 
   667     uq = ua + n' * uint K ==> up + uint K <= uq"
   668   apply clarsimp
   669   apply (drule less_le_mult)
   670   apply safe
   671   done
   672 
   673 lemma udvd_incr': 
   674   "p < q ==> uint p = ua + n * uint K ==> 
   675     uint q = ua + n' * uint K ==> p + K <= q" 
   676   apply (unfold word_less_alt word_le_def)
   677   apply (drule (2) udvd_incr_lem)
   678   apply (erule uint_add_le [THEN order_trans])
   679   done
   680 
   681 lemma udvd_decr': 
   682   "p < q ==> uint p = ua + n * uint K ==> 
   683     uint q = ua + n' * uint K ==> p <= q - K"
   684   apply (unfold word_less_alt word_le_def)
   685   apply (drule (2) udvd_incr_lem)
   686   apply (drule le_diff_eq [THEN iffD2])
   687   apply (erule order_trans)
   688   apply (rule uint_sub_ge)
   689   done
   690 
   691 lemmas udvd_incr_lem0 = udvd_incr_lem [where ua=0, simplified]
   692 lemmas udvd_incr0 = udvd_incr' [where ua=0, simplified]
   693 lemmas udvd_decr0 = udvd_decr' [where ua=0, simplified]
   694 
   695 lemma udvd_minus_le': 
   696   "xy < k ==> z udvd xy ==> z udvd k ==> xy <= k - z"
   697   apply (unfold udvd_def)
   698   apply clarify
   699   apply (erule (2) udvd_decr0)
   700   done
   701 
   702 lemma udvd_incr2_K: 
   703   "p < a + s ==> a <= a + s ==> K udvd s ==> K udvd p - a ==> a <= p ==> 
   704     0 < K ==> p <= p + K & p + K <= a + s"
   705   apply (unfold udvd_def)
   706   apply clarify
   707   apply (simp add: uint_arith_simps split: split_if_asm)
   708    prefer 2 
   709    apply (insert uint_range' [of s])[1]
   710    apply arith
   711   apply (drule add_commute [THEN xtr1])
   712   apply (simp add: diff_less_eq [symmetric])
   713   apply (drule less_le_mult)
   714    apply arith
   715   apply simp
   716   done
   717 
   718 (* links with rbl operations *)
   719 lemma word_succ_rbl:
   720   "to_bl w = bl ==> to_bl (word_succ w) = (rev (rbl_succ (rev bl)))"
   721   apply (unfold word_succ_def)
   722   apply clarify
   723   apply (simp add: to_bl_of_bin)
   724   apply (simp add: to_bl_def rbl_succ)
   725   done
   726 
   727 lemma word_pred_rbl:
   728   "to_bl w = bl ==> to_bl (word_pred w) = (rev (rbl_pred (rev bl)))"
   729   apply (unfold word_pred_def)
   730   apply clarify
   731   apply (simp add: to_bl_of_bin)
   732   apply (simp add: to_bl_def rbl_pred)
   733   done
   734 
   735 lemma word_add_rbl:
   736   "to_bl v = vbl ==> to_bl w = wbl ==> 
   737     to_bl (v + w) = (rev (rbl_add (rev vbl) (rev wbl)))"
   738   apply (unfold word_add_def)
   739   apply clarify
   740   apply (simp add: to_bl_of_bin)
   741   apply (simp add: to_bl_def rbl_add)
   742   done
   743 
   744 lemma word_mult_rbl:
   745   "to_bl v = vbl ==> to_bl w = wbl ==> 
   746     to_bl (v * w) = (rev (rbl_mult (rev vbl) (rev wbl)))"
   747   apply (unfold word_mult_def)
   748   apply clarify
   749   apply (simp add: to_bl_of_bin)
   750   apply (simp add: to_bl_def rbl_mult)
   751   done
   752 
   753 lemma rtb_rbl_ariths:
   754   "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_succ w)) = rbl_succ ys"
   755 
   756   "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_pred w)) = rbl_pred ys"
   757 
   758   "[| rev (to_bl v) = ys; rev (to_bl w) = xs |] 
   759   ==> rev (to_bl (v * w)) = rbl_mult ys xs"
   760 
   761   "[| rev (to_bl v) = ys; rev (to_bl w) = xs |] 
   762   ==> rev (to_bl (v + w)) = rbl_add ys xs"
   763   by (auto simp: rev_swap [symmetric] word_succ_rbl 
   764                  word_pred_rbl word_mult_rbl word_add_rbl)
   765 
   766 
   767 subsection "Arithmetic type class instantiations"
   768 
   769 instance word :: (len0) comm_monoid_add ..
   770 
   771 instance word :: (len0) comm_monoid_mult
   772   apply (intro_classes)
   773    apply (simp add: word_mult_commute)
   774   apply (simp add: word_mult_1)
   775   done
   776 
   777 instance word :: (len0) comm_semiring 
   778   by (intro_classes) (simp add : word_left_distrib)
   779 
   780 instance word :: (len0) ab_group_add ..
   781 
   782 instance word :: (len0) comm_ring ..
   783 
   784 instance word :: (len) comm_semiring_1 
   785   by (intro_classes) (simp add: lenw1_zero_neq_one)
   786 
   787 instance word :: (len) comm_ring_1 ..
   788 
   789 instance word :: (len0) comm_semiring_0 ..
   790 
   791 instance word :: (len0) order ..
   792 
   793 instance word :: (len) recpower
   794   by (intro_classes) (simp_all add: word_pow)
   795 
   796 (* note that iszero_def is only for class comm_semiring_1_cancel,
   797    which requires word length >= 1, ie 'a :: len word *) 
   798 lemma zero_bintrunc:
   799   "iszero (number_of x :: 'a :: len word) = 
   800     (bintrunc (len_of TYPE('a)) x = Numeral.Pls)"
   801   apply (unfold iszero_def word_0_wi word_no_wi)
   802   apply (rule word_ubin.norm_eq_iff [symmetric, THEN trans])
   803   apply (simp add : Pls_def [symmetric])
   804   done
   805 
   806 lemmas word_le_0_iff [simp] =
   807   word_zero_le [THEN leD, THEN linorder_antisym_conv1]
   808 
   809 lemma word_of_nat: "of_nat n = word_of_int (int n)"
   810   by (induct n) (auto simp add : word_of_int_hom_syms)
   811 
   812 lemma word_of_int: "of_int = word_of_int"
   813   apply (rule ext)
   814   apply (unfold of_int_def)
   815   apply (rule contentsI)
   816   apply safe
   817   apply (simp_all add: word_of_nat word_of_int_homs)
   818    defer
   819    apply (rule Rep_Integ_ne [THEN nonemptyE])
   820    apply (rule bexI)
   821     prefer 2
   822     apply assumption
   823    apply (auto simp add: RI_eq_diff)
   824   done
   825 
   826 lemma word_of_int_nat: 
   827   "0 <= x ==> word_of_int x = of_nat (nat x)"
   828   by (simp add: of_nat_nat word_of_int)
   829 
   830 lemma word_number_of_eq: 
   831   "number_of w = (of_int w :: 'a :: len word)"
   832   unfolding word_number_of_def word_of_int by auto
   833 
   834 instance word :: (len) number_ring
   835   by (intro_classes) (simp add : word_number_of_eq)
   836 
   837 lemma iszero_word_no [simp] : 
   838   "iszero (number_of bin :: 'a :: len word) = 
   839     iszero (number_of (bintrunc (len_of TYPE('a)) bin) :: int)"
   840   apply (simp add: zero_bintrunc number_of_is_id)
   841   apply (unfold iszero_def Pls_def)
   842   apply (rule refl)
   843   done
   844     
   845 
   846 subsection "Word and nat"
   847 
   848 lemma td_ext_unat':
   849   "n = len_of TYPE ('a :: len) ==> 
   850     td_ext (unat :: 'a word => nat) of_nat 
   851     (unats n) (%i. i mod 2 ^ n)"
   852   apply (unfold td_ext_def' unat_def word_of_nat unats_uints)
   853   apply (auto intro!: imageI simp add : word_of_int_hom_syms)
   854   apply (erule word_uint.Abs_inverse [THEN arg_cong])
   855   apply (simp add: int_word_uint nat_mod_distrib nat_power_eq)
   856   done
   857 
   858 lemmas td_ext_unat = refl [THEN td_ext_unat']
   859 lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm, standard]
   860 
   861 interpretation word_unat:
   862   td_ext ["unat::'a::len word => nat" 
   863           of_nat 
   864           "unats (len_of TYPE('a::len))"
   865           "%i. i mod 2 ^ len_of TYPE('a::len)"]
   866   by (rule td_ext_unat)
   867 
   868 lemmas td_unat = word_unat.td_thm
   869 
   870 lemmas unat_lt2p [iff] = word_unat.Rep [unfolded unats_def mem_Collect_eq]
   871 
   872 lemma unat_le: "y <= unat (z :: 'a :: len word) ==> y : unats (len_of TYPE ('a))"
   873   apply (unfold unats_def)
   874   apply clarsimp
   875   apply (rule xtrans, rule unat_lt2p, assumption) 
   876   done
   877 
   878 lemma word_nchotomy:
   879   "ALL w. EX n. (w :: 'a :: len word) = of_nat n & n < 2 ^ len_of TYPE ('a)"
   880   apply (rule allI)
   881   apply (rule word_unat.Abs_cases)
   882   apply (unfold unats_def)
   883   apply auto
   884   done
   885 
   886 lemma of_nat_eq:
   887   fixes w :: "'a::len word"
   888   shows "(of_nat n = w) = (\<exists>q. n = unat w + q * 2 ^ len_of TYPE('a))"
   889   apply (rule trans)
   890    apply (rule word_unat.inverse_norm)
   891   apply (rule iffI)
   892    apply (rule mod_eqD)
   893    apply simp
   894   apply clarsimp
   895   done
   896 
   897 lemma of_nat_eq_size: 
   898   "(of_nat n = w) = (EX q. n = unat w + q * 2 ^ size w)"
   899   unfolding word_size by (rule of_nat_eq)
   900 
   901 lemma of_nat_0:
   902   "(of_nat m = (0::'a::len word)) = (\<exists>q. m = q * 2 ^ len_of TYPE('a))"
   903   by (simp add: of_nat_eq)
   904 
   905 lemmas of_nat_2p = mult_1 [symmetric, THEN iffD2 [OF of_nat_0 exI]]
   906 
   907 lemma of_nat_gt_0: "of_nat k ~= 0 ==> 0 < k"
   908   by (cases k) auto
   909 
   910 lemma of_nat_neq_0: 
   911   "0 < k ==> k < 2 ^ len_of TYPE ('a :: len) ==> of_nat k ~= (0 :: 'a word)"
   912   by (clarsimp simp add : of_nat_0)
   913 
   914 lemma Abs_fnat_hom_add:
   915   "of_nat a + of_nat b = of_nat (a + b)"
   916   by simp
   917 
   918 lemma Abs_fnat_hom_mult:
   919   "of_nat a * of_nat b = (of_nat (a * b) :: 'a :: len word)"
   920   by (simp add: word_of_nat word_of_int_mult_hom zmult_int)
   921 
   922 lemma Abs_fnat_hom_Suc:
   923   "word_succ (of_nat a) = of_nat (Suc a)"
   924   by (simp add: word_of_nat word_of_int_succ_hom add_ac)
   925 
   926 lemma Abs_fnat_hom_0: "(0::'a::len word) = of_nat 0"
   927   by (simp add: word_of_nat word_0_wi)
   928 
   929 lemma Abs_fnat_hom_1: "(1::'a::len word) = of_nat (Suc 0)"
   930   by (simp add: word_of_nat word_1_wi)
   931 
   932 lemmas Abs_fnat_homs = 
   933   Abs_fnat_hom_add Abs_fnat_hom_mult Abs_fnat_hom_Suc 
   934   Abs_fnat_hom_0 Abs_fnat_hom_1
   935 
   936 lemma word_arith_nat_add:
   937   "a + b = of_nat (unat a + unat b)" 
   938   by simp
   939 
   940 lemma word_arith_nat_mult:
   941   "a * b = of_nat (unat a * unat b)"
   942   by (simp add: Abs_fnat_hom_mult [symmetric])
   943     
   944 lemma word_arith_nat_Suc:
   945   "word_succ a = of_nat (Suc (unat a))"
   946   by (subst Abs_fnat_hom_Suc [symmetric]) simp
   947 
   948 lemma word_arith_nat_div:
   949   "a div b = of_nat (unat a div unat b)"
   950   by (simp add: word_div_def word_of_nat zdiv_int uint_nat)
   951 
   952 lemma word_arith_nat_mod:
   953   "a mod b = of_nat (unat a mod unat b)"
   954   by (simp add: word_mod_def word_of_nat zmod_int uint_nat)
   955 
   956 lemmas word_arith_nat_defs =
   957   word_arith_nat_add word_arith_nat_mult
   958   word_arith_nat_Suc Abs_fnat_hom_0
   959   Abs_fnat_hom_1 word_arith_nat_div
   960   word_arith_nat_mod 
   961 
   962 lemmas unat_cong = arg_cong [where f = "unat"]
   963   
   964 lemmas unat_word_ariths = word_arith_nat_defs
   965   [THEN trans [OF unat_cong unat_of_nat], standard]
   966 
   967 lemmas word_sub_less_iff = word_sub_le_iff
   968   [simplified linorder_not_less [symmetric], simplified]
   969 
   970 lemma unat_add_lem: 
   971   "(unat x + unat y < 2 ^ len_of TYPE('a)) = 
   972     (unat (x + y :: 'a :: len word) = unat x + unat y)"
   973   unfolding unat_word_ariths
   974   by (auto intro!: trans [OF _ nat_mod_lem])
   975 
   976 lemma unat_mult_lem: 
   977   "(unat x * unat y < 2 ^ len_of TYPE('a)) = 
   978     (unat (x * y :: 'a :: len word) = unat x * unat y)"
   979   unfolding unat_word_ariths
   980   by (auto intro!: trans [OF _ nat_mod_lem])
   981 
   982 lemmas unat_plus_if' = 
   983   trans [OF unat_word_ariths(1) mod_nat_add, simplified, standard]
   984 
   985 lemma le_no_overflow: 
   986   "x <= b ==> a <= a + b ==> x <= a + (b :: 'a :: len0 word)"
   987   apply (erule order_trans)
   988   apply (erule olen_add_eqv [THEN iffD1])
   989   done
   990 
   991 lemmas un_ui_le = trans 
   992   [OF word_le_nat_alt [symmetric] 
   993       word_le_def [THEN meta_eq_to_obj_eq], 
   994    standard]
   995 
   996 lemma unat_sub_if_size:
   997   "unat (x - y) = (if unat y <= unat x 
   998    then unat x - unat y 
   999    else unat x + 2 ^ size x - unat y)"
  1000   apply (unfold word_size)
  1001   apply (simp add: un_ui_le)
  1002   apply (auto simp add: unat_def uint_sub_if')
  1003    apply (rule nat_diff_distrib)
  1004     prefer 3
  1005     apply (simp add: group_simps)
  1006     apply (rule nat_diff_distrib [THEN trans])
  1007       prefer 3
  1008       apply (subst nat_add_distrib)
  1009         prefer 3
  1010         apply (simp add: nat_power_eq)
  1011        apply auto
  1012   apply uint_arith
  1013   done
  1014 
  1015 lemmas unat_sub_if' = unat_sub_if_size [unfolded word_size]
  1016 
  1017 lemma unat_div: "unat ((x :: 'a :: len word) div y) = unat x div unat y"
  1018   apply (simp add : unat_word_ariths)
  1019   apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq'])
  1020   apply (rule div_le_dividend)
  1021   done
  1022 
  1023 lemma unat_mod: "unat ((x :: 'a :: len word) mod y) = unat x mod unat y"
  1024   apply (clarsimp simp add : unat_word_ariths)
  1025   apply (cases "unat y")
  1026    prefer 2
  1027    apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq'])
  1028    apply (rule mod_le_divisor)
  1029    apply auto
  1030   done
  1031 
  1032 lemma uint_div: "uint ((x :: 'a :: len word) div y) = uint x div uint y"
  1033   unfolding uint_nat by (simp add : unat_div zdiv_int)
  1034 
  1035 lemma uint_mod: "uint ((x :: 'a :: len word) mod y) = uint x mod uint y"
  1036   unfolding uint_nat by (simp add : unat_mod zmod_int)
  1037 
  1038 
  1039 subsection {* Definition of unat\_arith tactic *}
  1040 
  1041 lemma unat_split:
  1042   fixes x::"'a::len word"
  1043   shows "P (unat x) = 
  1044          (ALL n. of_nat n = x & n < 2^len_of TYPE('a) --> P n)"
  1045   by (auto simp: unat_of_nat)
  1046 
  1047 lemma unat_split_asm:
  1048   fixes x::"'a::len word"
  1049   shows "P (unat x) = 
  1050          (~(EX n. of_nat n = x & n < 2^len_of TYPE('a) & ~ P n))"
  1051   by (auto simp: unat_of_nat)
  1052 
  1053 lemmas of_nat_inverse = 
  1054   word_unat.Abs_inverse' [rotated, unfolded unats_def, simplified]
  1055 
  1056 lemmas unat_splits = unat_split unat_split_asm
  1057 
  1058 lemmas unat_arith_simps =
  1059   word_le_nat_alt word_less_nat_alt
  1060   word_unat.Rep_inject [symmetric]
  1061   unat_sub_if' unat_plus_if' unat_div unat_mod
  1062 
  1063 (* unat_arith_tac: tactic to reduce word arithmetic to nat, 
  1064    try to solve via arith *)
  1065 ML {*
  1066 fun unat_arith_ss_of ss = 
  1067   ss addsimps @{thms unat_arith_simps}
  1068      delsimps @{thms word_unat.Rep_inject}
  1069      addsplits @{thms split_if_asm}
  1070      addcongs @{thms power_False_cong}
  1071 
  1072 fun unat_arith_tacs ctxt =   
  1073   let fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty  
  1074   in 
  1075     [ CLASET' clarify_tac 1,
  1076       SIMPSET' (full_simp_tac o unat_arith_ss_of) 1,
  1077       ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms unat_splits} 
  1078                                        addcongs @{thms power_False_cong})),
  1079       rewrite_goals_tac @{thms word_size}, 
  1080       ALLGOALS  (fn n => REPEAT (resolve_tac [allI, impI] n) THEN      
  1081                          REPEAT (etac conjE n) THEN
  1082                          REPEAT (dtac @{thm of_nat_inverse} n THEN atac n)),
  1083       TRYALL arith_tac' ] 
  1084   end
  1085 
  1086 fun unat_arith_tac ctxt = SELECT_GOAL (EVERY (unat_arith_tacs ctxt))
  1087 *}
  1088 
  1089 method_setup unat_arith = 
  1090   "Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (unat_arith_tac ctxt 1))" 
  1091   "solving word arithmetic via natural numbers and arith"
  1092 
  1093 lemma no_plus_overflow_unat_size: 
  1094   "((x :: 'a :: len word) <= x + y) = (unat x + unat y < 2 ^ size x)" 
  1095   unfolding word_size by unat_arith
  1096 
  1097 lemma unat_sub: "b <= a ==> unat (a - b) = unat a - unat (b :: 'a :: len word)"
  1098   by unat_arith
  1099 
  1100 lemmas no_olen_add_nat = no_plus_overflow_unat_size [unfolded word_size]
  1101 
  1102 lemmas unat_plus_simple = trans [OF no_olen_add_nat unat_add_lem, standard]
  1103 
  1104 lemma word_div_mult: 
  1105   "(0 :: 'a :: len word) < y ==> unat x * unat y < 2 ^ len_of TYPE('a) ==> 
  1106     x * y div y = x"
  1107   apply unat_arith
  1108   apply clarsimp
  1109   apply (subst unat_mult_lem [THEN iffD1])
  1110   apply auto
  1111   done
  1112 
  1113 lemma div_lt': "(i :: 'a :: len word) <= k div x ==> 
  1114     unat i * unat x < 2 ^ len_of TYPE('a)"
  1115   apply unat_arith
  1116   apply clarsimp
  1117   apply (drule mult_le_mono1)
  1118   apply (erule order_le_less_trans)
  1119   apply (rule xtr7 [OF unat_lt2p div_mult_le])
  1120   done
  1121 
  1122 lemmas div_lt'' = order_less_imp_le [THEN div_lt']
  1123 
  1124 lemma div_lt_mult: "(i :: 'a :: len word) < k div x ==> 0 < x ==> i * x < k"
  1125   apply (frule div_lt'' [THEN unat_mult_lem [THEN iffD1]])
  1126   apply (simp add: unat_arith_simps)
  1127   apply (drule (1) mult_less_mono1)
  1128   apply (erule order_less_le_trans)
  1129   apply (rule div_mult_le)
  1130   done
  1131 
  1132 lemma div_le_mult: 
  1133   "(i :: 'a :: len word) <= k div x ==> 0 < x ==> i * x <= k"
  1134   apply (frule div_lt' [THEN unat_mult_lem [THEN iffD1]])
  1135   apply (simp add: unat_arith_simps)
  1136   apply (drule mult_le_mono1)
  1137   apply (erule order_trans)
  1138   apply (rule div_mult_le)
  1139   done
  1140 
  1141 lemma div_lt_uint': 
  1142   "(i :: 'a :: len word) <= k div x ==> uint i * uint x < 2 ^ len_of TYPE('a)"
  1143   apply (unfold uint_nat)
  1144   apply (drule div_lt')
  1145   apply (simp add: zmult_int zless_nat_eq_int_zless [symmetric] 
  1146                    nat_power_eq)
  1147   done
  1148 
  1149 lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint']
  1150 
  1151 lemma word_le_exists': 
  1152   "(x :: 'a :: len0 word) <= y ==> 
  1153     (EX z. y = x + z & uint x + uint z < 2 ^ len_of TYPE('a))"
  1154   apply (rule exI)
  1155   apply (rule conjI)
  1156   apply (rule zadd_diff_inverse)
  1157   apply uint_arith
  1158   done
  1159 
  1160 lemmas plus_minus_not_NULL = order_less_imp_le [THEN plus_minus_not_NULL_ab]
  1161 
  1162 lemmas plus_minus_no_overflow =
  1163   order_less_imp_le [THEN plus_minus_no_overflow_ab]
  1164   
  1165 lemmas mcs = word_less_minus_cancel word_less_minus_mono_left
  1166   word_le_minus_cancel word_le_minus_mono_left
  1167 
  1168 lemmas word_l_diffs = mcs [where y = "?w + ?x", unfolded add_diff_cancel]
  1169 lemmas word_diff_ls = mcs [where z = "?w + ?x", unfolded add_diff_cancel]
  1170 lemmas word_plus_mcs = word_diff_ls 
  1171   [where y = "?v + ?x", unfolded add_diff_cancel]
  1172 
  1173 lemmas le_unat_uoi = unat_le [THEN word_unat.Abs_inverse]
  1174 
  1175 lemmas thd = refl [THEN [2] split_div_lemma [THEN iffD2], THEN conjunct1]
  1176 
  1177 lemma thd1:
  1178   "a div b * b \<le> (a::nat)"
  1179   using gt_or_eq_0 [of b]
  1180   apply (rule disjE)
  1181    apply (erule xtr4 [OF thd mult_commute])
  1182   apply clarsimp
  1183   done
  1184 
  1185 lemmas uno_simps [THEN le_unat_uoi, standard] =
  1186   mod_le_divisor div_le_dividend thd1 
  1187 
  1188 lemma word_mod_div_equality:
  1189   "(n div b) * b + (n mod b) = (n :: 'a :: len word)"
  1190   apply (unfold word_less_nat_alt word_arith_nat_defs)
  1191   apply (cut_tac y="unat b" in gt_or_eq_0)
  1192   apply (erule disjE)
  1193    apply (simp add: mod_div_equality uno_simps)
  1194   apply simp
  1195   done
  1196 
  1197 lemma word_div_mult_le: "a div b * b <= (a::'a::len word)"
  1198   apply (unfold word_le_nat_alt word_arith_nat_defs)
  1199   apply (cut_tac y="unat b" in gt_or_eq_0)
  1200   apply (erule disjE)
  1201    apply (simp add: div_mult_le uno_simps)
  1202   apply simp
  1203   done
  1204 
  1205 lemma word_mod_less_divisor: "0 < n ==> m mod n < (n :: 'a :: len word)"
  1206   apply (simp only: word_less_nat_alt word_arith_nat_defs)
  1207   apply (clarsimp simp add : uno_simps)
  1208   done
  1209 
  1210 lemma word_of_int_power_hom: 
  1211   "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a :: len word)"
  1212   by (induct n) (simp_all add : word_of_int_hom_syms power_Suc)
  1213 
  1214 lemma word_arith_power_alt: 
  1215   "a ^ n = (word_of_int (uint a ^ n) :: 'a :: len word)"
  1216   by (simp add : word_of_int_power_hom [symmetric])
  1217 
  1218 lemma of_bl_length_less: 
  1219   "length x = k ==> k < len_of TYPE('a) ==> (of_bl x :: 'a :: len word) < 2 ^ k"
  1220   apply (unfold of_bl_no [unfolded word_number_of_def]
  1221                 word_less_alt word_number_of_alt)
  1222   apply safe
  1223   apply (simp (no_asm) add: word_of_int_power_hom word_uint.eq_norm 
  1224                        del: word_of_int_bin)
  1225   apply (simp add: mod_pos_pos_trivial)
  1226   apply (subst mod_pos_pos_trivial)
  1227     apply (rule bl_to_bin_ge0)
  1228    apply (rule order_less_trans)
  1229     apply (rule bl_to_bin_lt2p)
  1230    apply simp
  1231   apply (rule bl_to_bin_lt2p)    
  1232   done
  1233 
  1234 
  1235 subsection "Cardinality, finiteness of set of words"
  1236 
  1237 lemmas card_lessThan' = card_lessThan [unfolded lessThan_def]
  1238 
  1239 lemmas card_eq = word_unat.Abs_inj_on [THEN card_image,
  1240   unfolded word_unat.image, unfolded unats_def, standard]
  1241 
  1242 lemmas card_word = trans [OF card_eq card_lessThan', standard]
  1243 
  1244 lemma finite_word_UNIV: "finite (UNIV :: 'a :: len word set)"
  1245   apply (rule contrapos_np)
  1246    prefer 2
  1247    apply (erule card_infinite)
  1248   apply (simp add : card_word neq0_conv)
  1249   done
  1250 
  1251 lemma card_word_size: 
  1252   "card (UNIV :: 'a :: len word set) = (2 ^ size (x :: 'a word))"
  1253   unfolding word_size by (rule card_word)
  1254 
  1255 end 
  1256