src/HOL/Word/WordBitwise.thy

 lemma uint_and: "uint (x AND y) = (uint x) AND (uint y)"
   by (simp add: word_and_def number_of_is_id word_no_wi [symmetric]
                 bin_trunc_ao(1) [symmetric]) 
 
 lemma word_ops_nth_size:
-  "n < size (x::'a::len0 word) ==> 
+  "n < size (x::'a word) ==> 
     (x OR y) !! n = (x !! n | y !! n) & 
     (x AND y) !! n = (x !! n & y !! n) & 
     (x XOR y) !! n = (x !! n ~= y !! n) & 
     (NOT x) !! n = (~ x !! n)"
   unfolding word_size word_no_wi word_test_bit_def word_log_defs
   by (clarsimp simp add : word_ubin.eq_norm nth_bintr bin_nth_ops)
 
 lemma word_ao_nth:
-  fixes x :: "'a::len0 word"
+  fixes x :: "'a word"
   shows "(x OR y) !! n = (x !! n | y !! n) & 
          (x AND y) !! n = (x !! n & y !! n)"
   apply (cases "n < size x")
    apply (drule_tac y = "y" in word_ops_nth_size)
    apply simp

   word_0_wi_Pls
   word_m1_wi_Min
   word_wi_log_defs
 
 lemma word_bw_assocs:
-  fixes x :: "'a::len0 word"
+  fixes x :: "'a word"
   shows
   "(x AND y) AND z = x AND y AND z"
   "(x OR y) OR z = x OR y OR z"
   "(x XOR y) XOR z = x XOR y XOR z"
   using word_of_int_Ex [where x=x] 
         word_of_int_Ex [where x=y] 
         word_of_int_Ex [where x=z]
   by (auto simp: bwsimps bbw_assocs)
   
 lemma word_bw_comms:
-  fixes x :: "'a::len0 word"
+  fixes x :: "'a word"
   shows
   "x AND y = y AND x"
   "x OR y = y OR x"
   "x XOR y = y XOR x"
   using word_of_int_Ex [where x=x] 
         word_of_int_Ex [where x=y] 
   by (auto simp: bwsimps bin_ops_comm)
   
 lemma word_bw_lcs:
-  fixes x :: "'a::len0 word"
+  fixes x :: "'a word"
   shows
   "y AND x AND z = x AND y AND z"
   "y OR x OR z = x OR y OR z"
   "y XOR x XOR z = x XOR y XOR z"
   using word_of_int_Ex [where x=x] 
         word_of_int_Ex [where x=y] 
         word_of_int_Ex [where x=z]
   by (auto simp: bwsimps)
 
 lemma word_log_esimps [simp]:
-  fixes x :: "'a::len0 word"
+  fixes x :: "'a word"
   shows
   "x AND 0 = 0"
   "x AND -1 = x"
   "x OR 0 = x"
   "x OR -1 = -1"

   "-1 XOR x = NOT x"
   using word_of_int_Ex [where x=x] 
   by (auto simp: bwsimps)
 
 lemma word_not_dist:
-  fixes x :: "'a::len0 word"
+  fixes x :: "'a word"
   shows
   "NOT (x OR y) = NOT x AND NOT y"
   "NOT (x AND y) = NOT x OR NOT y"
   using word_of_int_Ex [where x=x] 
         word_of_int_Ex [where x=y] 
   by (auto simp: bwsimps bbw_not_dist)
 
 lemma word_bw_same:
-  fixes x :: "'a::len0 word"
+  fixes x :: "'a word"
   shows
   "x AND x = x"
   "x OR x = x"
   "x XOR x = 0"
   using word_of_int_Ex [where x=x] 
   by (auto simp: bwsimps)
 
 lemma word_ao_absorbs [simp]:
-  fixes x :: "'a::len0 word"
+  fixes x :: "'a word"
   shows
   "x AND (y OR x) = x"
   "x OR y AND x = x"
   "x AND (x OR y) = x"
   "y AND x OR x = x"

   using word_of_int_Ex [where x=x] 
         word_of_int_Ex [where x=y] 
   by (auto simp: bwsimps)
 
 lemma word_not_not [simp]:
-  "NOT NOT (x::'a::len0 word) = x"
+  "NOT NOT (x::'a word) = x"
   using word_of_int_Ex [where x=x] 
   by (auto simp: bwsimps)
 
 lemma word_ao_dist:
-  fixes x :: "'a::len0 word"
+  fixes x :: "'a word"
   shows "(x OR y) AND z = x AND z OR y AND z"
   using word_of_int_Ex [where x=x] 
         word_of_int_Ex [where x=y] 
         word_of_int_Ex [where x=z]   
   by (auto simp: bwsimps bbw_ao_dist simp del: bin_ops_comm)
 
 lemma word_oa_dist:
-  fixes x :: "'a::len0 word"
+  fixes x :: "'a word"
   shows "x AND y OR z = (x OR z) AND (y OR z)"
   using word_of_int_Ex [where x=x] 
         word_of_int_Ex [where x=y] 
         word_of_int_Ex [where x=z]   
   by (auto simp: bwsimps bbw_oa_dist simp del: bin_ops_comm)
 
 lemma word_add_not [simp]: 
-  fixes x :: "'a::len0 word"
+  fixes x :: "'a word"
   shows "x + NOT x = -1"
   using word_of_int_Ex [where x=x] 
   by (auto simp: bwsimps bin_add_not)
 
 lemma word_plus_and_or [simp]:
-  fixes x :: "'a::len0 word"
+  fixes x :: "'a word"
   shows "(x AND y) + (x OR y) = x + y"
   using word_of_int_Ex [where x=x] 
         word_of_int_Ex [where x=y] 
   by (auto simp: bwsimps plus_and_or)
 
 lemma leoa:   
-  fixes x :: "'a::len0 word"
+  fixes x :: "'a word"
   shows "(w = (x OR y)) ==> (y = (w AND y))" by auto
 lemma leao: 
-  fixes x' :: "'a::len0 word"
+  fixes x' :: "'a word"
   shows "(w' = (x' AND y')) ==> (x' = (x' OR w'))" by auto 
 
 lemmas word_ao_equiv = leao [COMP leoa [COMP iffI]]
 
-lemma le_word_or2: "x <= x OR (y::'a::len0 word)"
+lemma le_word_or2: "x <= x OR (y::'a word)"
   unfolding word_le_def uint_or
   by (auto intro: le_int_or) 
 
 lemmas le_word_or1 = xtr3 [OF word_bw_comms (2) le_word_or2, standard]
 lemmas word_and_le1 =
   xtr3 [OF word_ao_absorbs (4) [symmetric] le_word_or2, standard]
 lemmas word_and_le2 =
   xtr3 [OF word_ao_absorbs (8) [symmetric] le_word_or2, standard]
 
-lemma word_lsb_alt: "lsb (w::'a::len0 word) = test_bit w 0"
+lemma word_lsb_alt: "lsb (w::'a word) = test_bit w 0"
   by (auto simp: word_test_bit_def word_lsb_def)
 
-lemma word_lsb_1_0: "lsb (1::'a::len word) & ~ lsb (0::'b::len0 word)"
+lemma word_lsb_1_0: "lsb (1::'a::finite word) & ~ lsb (0::'b word)"
   unfolding word_lsb_def word_1_no word_0_no by auto
 
 lemma word_lsb_int: "lsb w = (uint w mod 2 = 1)"
   unfolding word_lsb_def bin_last_mod by auto
 
 lemma word_msb_sint: "msb w = (sint w < 0)" 
   unfolding word_msb_def
   by (simp add : sign_Min_lt_0 number_of_is_id)
   
 lemma word_msb_no': 
-  "w = number_of bin ==> msb (w::'a::len word) = bin_nth bin (size w - 1)"
+  "w = number_of bin ==> msb (w::'a::finite word) = bin_nth bin (size w - 1)"
   unfolding word_msb_def word_number_of_def
   by (clarsimp simp add: word_sbin.eq_norm word_size bin_sign_lem)
 
 lemmas word_msb_no = refl [THEN word_msb_no', unfolded word_size]
 
-lemma word_msb_nth': "msb (w::'a::len word) = bin_nth (uint w) (size w - 1)"
+lemma word_msb_nth': "msb (w::'a::finite word) = bin_nth (uint w) (size w - 1)"
   apply (unfold word_size)
   apply (rule trans [OF _ word_msb_no])
   apply (simp add : word_number_of_def)
   done
 
 lemmas word_msb_nth = word_msb_nth' [unfolded word_size]
 
 lemma word_set_nth:
-  "set_bit w n (test_bit w n) = (w::'a::len0 word)"
+  "set_bit w n (test_bit w n) = (w::'a word)"
   unfolding word_test_bit_def word_set_bit_def by auto
 
 lemma test_bit_set: 
-  fixes w :: "'a::len0 word"
+  fixes w :: "'a word"
   shows "(set_bit w n x) !! n = (n < size w & x)"
   unfolding word_size word_test_bit_def word_set_bit_def
   by (clarsimp simp add : word_ubin.eq_norm nth_bintr)
 
 lemma test_bit_set_gen: 
-  fixes w :: "'a::len0 word"
+  fixes w :: "'a word"
   shows "test_bit (set_bit w n x) m = 
          (if m = n then n < size w & x else test_bit w m)"
   apply (unfold word_size word_test_bit_def word_set_bit_def)
   apply (clarsimp simp add: word_ubin.eq_norm nth_bintr bin_nth_sc_gen)
   apply (auto elim!: test_bit_size [unfolded word_size]
               simp add: word_test_bit_def [symmetric])
   done
 
 lemma msb_nth':
-  fixes w :: "'a::len word"
+  fixes w :: "'a::finite word"
   shows "msb w = w !! (size w - 1)"
   unfolding word_msb_nth' word_test_bit_def by simp
 
 lemmas msb_nth = msb_nth' [unfolded word_size]
 
-lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN
+lemmas msb0 = zero_less_card_finite [THEN diff_Suc_less, THEN
   word_ops_nth_size [unfolded word_size], standard]
 lemmas msb1 = msb0 [where i = 0]
 lemmas word_ops_msb = msb1 [unfolded msb_nth [symmetric, unfolded One_nat_def]]
 
-lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size], standard]
+lemmas lsb0 = zero_less_card_finite [THEN word_ops_nth_size [unfolded word_size], standard]
 lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt]
 
 lemma word_set_set_same: 
-  fixes w :: "'a::len0 word"
+  fixes w :: "'a word"
   shows "set_bit (set_bit w n x) n y = set_bit w n y" 
   by (rule word_eqI) (simp add : test_bit_set_gen word_size)
     
 lemma word_set_set_diff: 
-  fixes w :: "'a::len0 word"
+  fixes w :: "'a word"
   assumes "m ~= n"
   shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x" 
   by (rule word_eqI) (clarsimp simp add : test_bit_set_gen word_size prems)
     
 lemma test_bit_no': 
-  fixes w :: "'a::len0 word"
+  fixes w :: "'a word"
   shows "w = number_of bin ==> test_bit w n = (n < size w & bin_nth bin n)"
   unfolding word_test_bit_def word_number_of_def word_size
   by (simp add : nth_bintr [symmetric] word_ubin.eq_norm)
 
 lemmas test_bit_no = 
   refl [THEN test_bit_no', unfolded word_size, THEN eq_reflection, standard]
 
-lemma nth_0: "~ (0::'a::len0 word) !! n"
+lemma nth_0: "~ (0::'a word) !! n"
   unfolding test_bit_no word_0_no by auto
 
 lemma nth_sint: 
-  fixes w :: "'a::len word"
-  defines "l \<equiv> len_of TYPE ('a)"
+  fixes w :: "'a::finite word"
+  defines "l \<equiv> CARD('a)"
   shows "bin_nth (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))"
   unfolding sint_uint l_def
   by (clarsimp simp add: nth_sbintr word_test_bit_def [symmetric])
 
 lemma word_lsb_no: 
-  "lsb (number_of bin :: 'a :: len word) = (bin_last bin = bit.B1)"
+  "lsb (number_of bin :: 'a :: finite word) = (bin_last bin = bit.B1)"
   unfolding word_lsb_alt test_bit_no by auto
 
 lemma word_set_no: 
-  "set_bit (number_of bin::'a::len0 word) n b = 
+  "set_bit (number_of bin::'a word) n b = 
     number_of (bin_sc n (if b then bit.B1 else bit.B0) bin)"
   apply (unfold word_set_bit_def word_number_of_def [symmetric])
   apply (rule word_eqI)
   apply (clarsimp simp: word_size bin_nth_sc_gen number_of_is_id 
                         test_bit_no nth_bintr)

 lemmas setBit_no = setBit_def [THEN trans [OF meta_eq_to_obj_eq word_set_no],
   simplified if_simps, THEN eq_reflection, standard]
 lemmas clearBit_no = clearBit_def [THEN trans [OF meta_eq_to_obj_eq word_set_no],
   simplified if_simps, THEN eq_reflection, standard]
 
-lemma word_msb_n1: "msb (-1::'a::len word)"
+lemma word_msb_n1: "msb (-1::'a::finite word)"
   unfolding word_msb_def sint_sbintrunc number_of_is_id bin_sign_lem
   by (rule bin_nth_Min)
 
 declare word_set_set_same [simp] word_set_nth [simp]
   test_bit_no [simp] word_set_no [simp] nth_0 [simp]
   setBit_no [simp] clearBit_no [simp]
   word_lsb_no [simp] word_msb_no [simp] word_msb_n1 [simp] word_lsb_1_0 [simp]
 
 lemma word_set_nth_iff: 
-  "(set_bit w n b = w) = (w !! n = b | n >= size (w::'a::len0 word))"
+  "(set_bit w n b = w) = (w !! n = b | n >= size (w::'a word))"
   apply (rule iffI)
    apply (rule disjCI)
    apply (drule word_eqD)
    apply (erule sym [THEN trans])
    apply (simp add: test_bit_set)

   apply force
   done
 
 lemma test_bit_2p': 
   "w = word_of_int (2 ^ n) ==> 
-    w !! m = (m = n & m < size (w :: 'a :: len word))"
+    w !! m = (m = n & m < size (w :: 'a :: finite word))"
   unfolding word_test_bit_def word_size
   by (auto simp add: word_ubin.eq_norm nth_bintr nth_2p_bin)
 
 lemmas test_bit_2p = refl [THEN test_bit_2p', unfolded word_size]
 
 lemmas nth_w2p = test_bit_2p [unfolded of_int_number_of_eq
   word_of_int [symmetric] of_int_power]
 
 lemma uint_2p: 
-  "(0::'a::len word) < 2 ^ n ==> uint (2 ^ n::'a::len word) = 2 ^ n"
+  "(0::'a::finite word) < 2 ^ n ==> uint (2 ^ n::'a::finite word) = 2 ^ n"
   apply (unfold word_arith_power_alt)
-  apply (case_tac "len_of TYPE ('a)")
+  apply (case_tac "CARD('a)")
    apply clarsimp
   apply (case_tac "nat")
    apply clarsimp
    apply (case_tac "n")
     apply (clarsimp simp add : word_1_wi [symmetric])

   apply (drule word_gt_0 [THEN iffD1])
   apply (safe intro!: word_eqI bin_nth_lem ext)
      apply (auto simp add: test_bit_2p nth_2p_bin word_test_bit_def [symmetric])
   done
 
-lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a :: len word) = 2 ^ n" 
+lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a :: finite word) = 2 ^ n" 
   apply (unfold word_arith_power_alt)
-  apply (case_tac "len_of TYPE ('a)")
+  apply (case_tac "CARD('a)")
    apply clarsimp
   apply (case_tac "nat")
    apply (rule word_ubin.norm_eq_iff [THEN iffD1]) 
    apply (rule box_equals) 
      apply (rule_tac [2] bintr_ariths (1))+ 
    apply (clarsimp simp add : number_of_is_id)
   apply simp 
   done
 
-lemma bang_is_le: "x !! m ==> 2 ^ m <= (x :: 'a :: len word)" 
+lemma bang_is_le: "x !! m ==> 2 ^ m <= (x :: 'a :: finite word)" 
   apply (rule xtr3) 
   apply (rule_tac [2] y = "x" in le_word_or2)
   apply (rule word_eqI)
   apply (auto simp add: word_ao_nth nth_w2p word_size)
   done
 
 lemma word_clr_le: 
-  fixes w :: "'a::len0 word"
+  fixes w :: "'a word"
   shows "w >= set_bit w n False"
   apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
   apply simp
   apply (rule order_trans)
    apply (rule bintr_bin_clr_le)
   apply simp
   done
 
 lemma word_set_ge: 
-  fixes w :: "'a::len word"
+  fixes w :: "'a::finite word"
   shows "w <= set_bit w n True"
   apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
   apply simp
   apply (rule order_trans [OF _ bintr_bin_set_ge])
   apply simp