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