# HG changeset patch # User huffman # Date 1187809761 -7200 # Node ID 058c5613a86f72a6b4863f2595878c46c558f9fa # Parent 61b10ffb2549b3772d06160bf3df748d6081ff73 removed Word/Size.thy; replaced len_of TYPE('a) with CARD('a); replaced axclass len with class finite; replaced axclass len0 with class type diff -r 61b10ffb2549 -r 058c5613a86f src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Aug 22 20:59:19 2007 +0200 +++ b/src/HOL/IsaMakefile Wed Aug 22 21:09:21 2007 +0200 @@ -814,7 +814,6 @@ Library/Boolean_Algebra.thy Library/Numeral_Type.thy \ Word/Num_Lemmas.thy \ Word/TdThs.thy \ - Word/Size.thy \ Word/BinGeneral.thy \ Word/BinOperations.thy \ Word/BinBoolList.thy \ diff -r 61b10ffb2549 -r 058c5613a86f src/HOL/Word/Size.thy --- a/src/HOL/Word/Size.thy Wed Aug 22 20:59:19 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,54 +0,0 @@ -(* - ID: $Id$ - Author: John Matthews, Galois Connections, Inc., copyright 2006 - - A typeclass for parameterizing types by size. - Used primarily to parameterize machine word sizes. -*) -theory Size -imports Numeral_Type -begin - -text {* - The aim of this is to allow any type as index type, but to provide a - default instantiation for numeral types. This independence requires - some duplication with the definitions in Numeral\_Type. -*} -axclass len0 < type - -consts - len_of :: "('a :: len0 itself) => nat" - -text {* - Some theorems are only true on words with length greater 0. -*} -axclass len < len0 - len_gt_0 [iff]: "0 < len_of TYPE ('a :: len0)" - -instance num0 :: len0 .. -instance num1 :: len0 .. -instance bit0 :: (len0) len0 .. -instance bit1 :: (len0) len0 .. - -defs (overloaded) - len_num0: "len_of (x::num0 itself) == 0" - len_num1: "len_of (x::num1 itself) == 1" - len_bit0: "len_of (x::'a::len0 bit0 itself) == 2 * len_of TYPE ('a)" - len_bit1: "len_of (x::'a::len0 bit1 itself) == 2 * len_of TYPE ('a) + 1" - -lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1 - -instance num1 :: len by (intro_classes) simp -instance bit0 :: (len) len by (intro_classes) simp -instance bit1 :: (len0) len by (intro_classes) simp - --- "Examples:" -lemma "len_of TYPE(17) = 17" by simp -lemma "len_of TYPE(0) = 0" by simp - --- "not simplified:" -lemma "len_of TYPE('a::len0) = x" - oops - -end - diff -r 61b10ffb2549 -r 058c5613a86f src/HOL/Word/WordArith.thy --- a/src/HOL/Word/WordArith.thy Wed Aug 22 20:59:19 2007 +0200 +++ b/src/HOL/Word/WordArith.thy Wed Aug 22 21:09:21 2007 +0200 @@ -29,7 +29,7 @@ unfolding Pls_def Bit_def by auto lemma word_1_no: - "(1 :: 'a :: len0 word) == number_of (Numeral.Pls BIT bit.B1)" + "(1 :: 'a word) == number_of (Numeral.Pls BIT bit.B1)" unfolding word_1_wi word_number_of_def int_one_bin by auto lemma word_m1_wi: "-1 == word_of_int -1" @@ -51,7 +51,7 @@ lemma unat_0 [simp]: "unat 0 = 0" unfolding unat_def by auto -lemma size_0_same': "size w = 0 ==> w = (v :: 'a :: len0 word)" +lemma size_0_same': "size w = 0 ==> w = (v :: 'a word)" apply (unfold word_size) apply (rule box_equals) defer @@ -95,14 +95,14 @@ apply (rule refl) done -lemma uint_1 [simp] : "uint (1 :: 'a :: len word) = 1" +lemma uint_1 [simp] : "uint (1 :: 'a :: finite word) = 1" unfolding word_1_wi by (simp add: word_ubin.eq_norm int_one_bin bintrunc_minus_simps) -lemma unat_1 [simp] : "unat (1 :: 'a :: len word) = 1" +lemma unat_1 [simp] : "unat (1 :: 'a :: finite word) = 1" by (unfold unat_def uint_1) auto -lemma ucast_1 [simp] : "ucast (1 :: 'a :: len word) = 1" +lemma ucast_1 [simp] : "ucast (1 :: 'a :: finite word) = 1" unfolding ucast_def word_1_wi by (simp add: word_ubin.eq_norm int_one_bin bintrunc_minus_simps) @@ -124,7 +124,7 @@ lemmas wi_hom_syms = wi_homs [symmetric] -lemma word_sub_def: "a - b == a + - (b :: 'a :: len0 word)" +lemma word_sub_def: "a - b == a + - (b :: 'a word)" unfolding word_sub_wi diff_def by (simp only : word_uint.Rep_inverse wi_hom_syms) @@ -193,7 +193,7 @@ lemmas sint_word_ariths = uint_word_arith_bintrs [THEN uint_sint [symmetric, THEN trans], unfolded uint_sint bintr_arith1s bintr_ariths - len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep, standard] + zero_less_card_finite [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep, standard] lemma word_pred_0_n1: "word_pred 0 = word_of_int -1" unfolding word_pred_def number_of_eq @@ -220,8 +220,8 @@ by (rule_tac x="uint x" in exI) simp lemma word_arith_eqs: - fixes a :: "'a::len0 word" - fixes b :: "'a::len0 word" + fixes a :: "'a word" + fixes b :: "'a word" shows word_add_0: "0 + a = a" and word_add_0_right: "a + 0 = a" and @@ -252,10 +252,10 @@ lemmas word_plus_ac0 = word_add_0 word_add_0_right word_add_ac lemmas word_times_ac1 = word_mult_1 word_mult_1_right word_mult_ac -instance word :: (len0) semigroup_add +instance word :: (type) semigroup_add by intro_classes (simp add: word_add_assoc) -instance word :: (len0) ring +instance word :: (type) ring by intro_classes (auto simp: word_arith_eqs word_diff_minus word_diff_self [unfolded word_diff_minus]) @@ -263,16 +263,16 @@ subsection "Order on fixed-length words" -instance word :: (len0) ord +instance word :: (type) ord word_le_def: "a <= b == uint a <= uint b" word_less_def: "x < y == x <= y & x ~= y" .. constdefs - word_sle :: "'a :: len word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50) + word_sle :: "'a :: finite word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50) "a <=s b == sint a <= sint b" - word_sless :: "'a :: len word => 'a word => bool" ("(_/ 'a word => bool" ("(_/ y <= z ==> x <= (z :: 'a :: len0 word)" +lemma word_order_trans: "x <= y ==> y <= z ==> x <= (z :: 'a word)" unfolding word_le_def by auto -lemma word_order_refl: "z <= (z :: 'a :: len0 word)" +lemma word_order_refl: "z <= (z :: 'a word)" unfolding word_le_def by auto -lemma word_order_antisym: "x <= y ==> y <= x ==> x = (y :: 'a :: len0 word)" +lemma word_order_antisym: "x <= y ==> y <= x ==> x = (y :: 'a word)" unfolding word_le_def by (auto intro!: word_uint.Rep_eqD) lemma word_order_linear: - "y <= x | x <= (y :: 'a :: len0 word)" + "y <= x | x <= (y :: 'a word)" unfolding word_le_def by auto lemma word_zero_le [simp] : - "0 <= (y :: 'a :: len0 word)" + "0 <= (y :: 'a word)" unfolding word_le_def by auto -instance word :: (len0) linorder +instance word :: (type) linorder by intro_classes (auto simp: word_less_def word_le_def) lemma word_m1_ge [simp] : "word_pred 0 >= y" @@ -329,7 +329,7 @@ lemmas word_not_simps [simp] = word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD] -lemma word_gt_0: "0 < y = (0 ~= (y :: 'a :: len0 word))" +lemma word_gt_0: "0 < y = (0 ~= (y :: 'a word))" unfolding word_less_def by auto lemmas word_gt_0_no [simp] = word_gt_0 [of "number_of ?y"] @@ -347,13 +347,13 @@ by (rule nat_less_eq_zless [symmetric]) simp lemma wi_less: - "(word_of_int n < (word_of_int m :: 'a :: len0 word)) = - (n mod 2 ^ len_of TYPE('a) < m mod 2 ^ len_of TYPE('a))" + "(word_of_int n < (word_of_int m :: 'a word)) = + (n mod 2 ^ CARD('a) < m mod 2 ^ CARD('a))" unfolding word_less_alt by (simp add: word_uint.eq_norm) lemma wi_le: - "(word_of_int n <= (word_of_int m :: 'a :: len0 word)) = - (n mod 2 ^ len_of TYPE('a) <= m mod 2 ^ len_of TYPE('a))" + "(word_of_int n <= (word_of_int m :: 'a word)) = + (n mod 2 ^ CARD('a) <= m mod 2 ^ CARD('a))" unfolding word_le_def by (simp add: word_uint.eq_norm) lemmas unat_mono = word_less_nat_alt [THEN iffD1, standard] @@ -362,7 +362,7 @@ subsection "Divisibility" definition - udvd :: "'a::len word \ 'a word \ bool" (infixl "udvd" 50) where + udvd :: "'a::finite word \ 'a word \ bool" (infixl "udvd" 50) where "a udvd b \ \n\0. uint b = n * uint a" lemma udvdI: @@ -388,7 +388,7 @@ subsection "Division with remainder" -instance word :: (len0) Divides.div +instance word :: (type) Divides.div word_div_def: "a div b == word_of_int (uint a div uint b)" word_mod_def: "a mod b == word_of_int (uint a mod uint b)" .. @@ -405,11 +405,11 @@ [THEN meta_eq_to_obj_eq [THEN trans [OF uint_cong int_word_uint]], standard] -lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) ==> (0 :: 'a word) ~= 1"; +lemma word_zero_neq_one: "0 < CARD('a) ==> (0 :: 'a word) ~= 1"; unfolding word_arith_wis by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc) -lemmas lenw1_zero_neq_one = len_gt_0 [THEN word_zero_neq_one] +lemmas lenw1_zero_neq_one = zero_less_card_finite [THEN word_zero_neq_one] lemma no_no [simp] : "number_of (number_of b) = number_of b" by (simp add: number_of_eq) @@ -445,21 +445,21 @@ mult_nonneg_nonneg [OF uint_ge_0 uint_ge_0, standard] lemma uint_sub_lt2p [simp]: - "uint (x :: 'a :: len0 word) - uint (y :: 'b :: len0 word) < - 2 ^ len_of TYPE('a)" + "uint (x :: 'a word) - uint (y :: 'b word) < + 2 ^ CARD('a)" using uint_ge_0 [of y] uint_lt2p [of x] by arith subsection "Conditions for the addition (etc) of two words to overflow" lemma uint_add_lem: - "(uint x + uint y < 2 ^ len_of TYPE('a)) = - (uint (x + y :: 'a :: len0 word) = uint x + uint y)" + "(uint x + uint y < 2 ^ CARD('a)) = + (uint (x + y :: 'a word) = uint x + uint y)" by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem]) lemma uint_mult_lem: - "(uint x * uint y < 2 ^ len_of TYPE('a)) = - (uint (x * y :: 'a :: len0 word) = uint x * uint y)" + "(uint x * uint y < 2 ^ CARD('a)) = + (uint (x * y :: 'a word) = uint x * uint y)" by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem]) lemma uint_sub_lem: @@ -481,25 +481,25 @@ subsection {* Definition of uint\_arith *} lemma word_of_int_inverse: - "word_of_int r = a ==> 0 <= r ==> r < 2 ^ len_of TYPE('a) ==> - uint (a::'a::len0 word) = r" + "word_of_int r = a ==> 0 <= r ==> r < 2 ^ CARD('a) ==> + uint (a::'a word) = r" apply (erule word_uint.Abs_inverse' [rotated]) apply (simp add: uints_num) done lemma uint_split: - fixes x::"'a::len0 word" + fixes x::"'a word" shows "P (uint x) = - (ALL i. word_of_int i = x & 0 <= i & i < 2^len_of TYPE('a) --> P i)" + (ALL i. word_of_int i = x & 0 <= i & i < 2^CARD('a) --> P i)" apply (fold word_int_case_def) apply (auto dest!: word_of_int_inverse simp: int_word_uint int_mod_eq' split: word_int_split) done lemma uint_split_asm: - fixes x::"'a::len0 word" + fixes x::"'a word" shows "P (uint x) = - (~(EX i. word_of_int i = x & 0 <= i & i < 2^len_of TYPE('a) & ~ P i))" + (~(EX i. word_of_int i = x & 0 <= i & i < 2^CARD('a) & ~ P i))" by (auto dest!: word_of_int_inverse simp: int_word_uint int_mod_eq' split: uint_split) @@ -511,7 +511,7 @@ word_uint.Rep_inject [symmetric] uint_sub_if' uint_plus_if' -(* use this to stop, eg, 2 ^ len_of TYPE (32) being simplified *) +(* use this to stop, eg, 2 ^ CARD(32) being simplified *) lemma power_False_cong: "False ==> a ^ b = c ^ d" by auto @@ -550,17 +550,17 @@ subsection "More on overflows and monotonicity" lemma no_plus_overflow_uint_size: - "((x :: 'a :: len0 word) <= x + y) = (uint x + uint y < 2 ^ size x)" + "((x :: 'a word) <= x + y) = (uint x + uint y < 2 ^ size x)" unfolding word_size by uint_arith lemmas no_olen_add = no_plus_overflow_uint_size [unfolded word_size] -lemma no_ulen_sub: "((x :: 'a :: len0 word) >= x - y) = (uint y <= uint x)" +lemma no_ulen_sub: "((x :: 'a word) >= x - y) = (uint y <= uint x)" by uint_arith lemma no_olen_add': - fixes x :: "'a::len0 word" - shows "(x \ y + x) = (uint y + uint x < 2 ^ len_of TYPE('a))" + fixes x :: "'a word" + shows "(x \ y + x) = (uint y + uint x < 2 ^ CARD('a))" by (simp add: word_add_ac add_ac no_olen_add) lemmas olen_add_eqv = trans [OF no_olen_add no_olen_add' [symmetric], standard] @@ -573,35 +573,35 @@ lemmas word_sub_le = word_sub_le_iff [THEN iffD2, standard] lemma word_less_sub1: - "(x :: 'a :: len word) ~= 0 ==> (1 < x) = (0 < x - 1)" + "(x :: 'a :: finite word) ~= 0 ==> (1 < x) = (0 < x - 1)" by uint_arith lemma word_le_sub1: - "(x :: 'a :: len word) ~= 0 ==> (1 <= x) = (0 <= x - 1)" + "(x :: 'a :: finite word) ~= 0 ==> (1 <= x) = (0 <= x - 1)" by uint_arith lemma sub_wrap_lt: - "((x :: 'a :: len0 word) < x - z) = (x < z)" + "((x :: 'a word) < x - z) = (x < z)" by uint_arith lemma sub_wrap: - "((x :: 'a :: len0 word) <= x - z) = (z = 0 | x < z)" + "((x :: 'a word) <= x - z) = (z = 0 | x < z)" by uint_arith lemma plus_minus_not_NULL_ab: - "(x :: 'a :: len0 word) <= ab - c ==> c <= ab ==> c ~= 0 ==> x + c ~= 0" + "(x :: 'a word) <= ab - c ==> c <= ab ==> c ~= 0 ==> x + c ~= 0" by uint_arith lemma plus_minus_no_overflow_ab: - "(x :: 'a :: len0 word) <= ab - c ==> c <= ab ==> x <= x + c" + "(x :: 'a word) <= ab - c ==> c <= ab ==> x <= x + c" by uint_arith lemma le_minus': - "(a :: 'a :: len0 word) + c <= b ==> a <= a + c ==> c <= b - a" + "(a :: 'a word) + c <= b ==> a <= a + c ==> c <= b - a" by uint_arith lemma le_plus': - "(a :: 'a :: len0 word) <= b ==> c <= b - a ==> a + c <= b" + "(a :: 'a word) <= b ==> c <= b - a ==> a + c <= b" by uint_arith lemmas le_plus = le_plus' [rotated] @@ -609,69 +609,69 @@ lemmas le_minus = leD [THEN thin_rl, THEN le_minus', standard] lemma word_plus_mono_right: - "(y :: 'a :: len0 word) <= z ==> x <= x + z ==> x + y <= x + z" + "(y :: 'a word) <= z ==> x <= x + z ==> x + y <= x + z" by uint_arith lemma word_less_minus_cancel: - "y - x < z - x ==> x <= z ==> (y :: 'a :: len0 word) < z" + "y - x < z - x ==> x <= z ==> (y :: 'a word) < z" by uint_arith lemma word_less_minus_mono_left: - "(y :: 'a :: len0 word) < z ==> x <= y ==> y - x < z - x" + "(y :: 'a word) < z ==> x <= y ==> y - x < z - x" by uint_arith lemma word_less_minus_mono: "a < c ==> d < b ==> a - b < a ==> c - d < c - ==> a - b < c - (d::'a::len word)" + ==> a - b < c - (d::'a::finite word)" by uint_arith lemma word_le_minus_cancel: - "y - x <= z - x ==> x <= z ==> (y :: 'a :: len0 word) <= z" + "y - x <= z - x ==> x <= z ==> (y :: 'a word) <= z" by uint_arith lemma word_le_minus_mono_left: - "(y :: 'a :: len0 word) <= z ==> x <= y ==> y - x <= z - x" + "(y :: 'a word) <= z ==> x <= y ==> y - x <= z - x" by uint_arith lemma word_le_minus_mono: "a <= c ==> d <= b ==> a - b <= a ==> c - d <= c - ==> a - b <= c - (d::'a::len word)" + ==> a - b <= c - (d::'a::finite word)" by uint_arith lemma plus_le_left_cancel_wrap: - "(x :: 'a :: len0 word) + y' < x ==> x + y < x ==> (x + y' < x + y) = (y' < y)" + "(x :: 'a word) + y' < x ==> x + y < x ==> (x + y' < x + y) = (y' < y)" by uint_arith lemma plus_le_left_cancel_nowrap: - "(x :: 'a :: len0 word) <= x + y' ==> x <= x + y ==> + "(x :: 'a word) <= x + y' ==> x <= x + y ==> (x + y' < x + y) = (y' < y)" by uint_arith lemma word_plus_mono_right2: - "(a :: 'a :: len0 word) <= a + b ==> c <= b ==> a <= a + c" + "(a :: 'a word) <= a + b ==> c <= b ==> a <= a + c" by uint_arith lemma word_less_add_right: - "(x :: 'a :: len0 word) < y - z ==> z <= y ==> x + z < y" + "(x :: 'a word) < y - z ==> z <= y ==> x + z < y" by uint_arith lemma word_less_sub_right: - "(x :: 'a :: len0 word) < y + z ==> y <= x ==> x - y < z" + "(x :: 'a word) < y + z ==> y <= x ==> x - y < z" by uint_arith lemma word_le_plus_either: - "(x :: 'a :: len0 word) <= y | x <= z ==> y <= y + z ==> x <= y + z" + "(x :: 'a word) <= y | x <= z ==> y <= y + z ==> x <= y + z" by uint_arith lemma word_less_nowrapI: - "(x :: 'a :: len0 word) < z - k ==> k <= z ==> 0 < k ==> x < x + k" + "(x :: 'a word) < z - k ==> k <= z ==> 0 < k ==> x < x + k" by uint_arith -lemma inc_le: "(i :: 'a :: len word) < m ==> i + 1 <= m" +lemma inc_le: "(i :: 'a :: finite word) < m ==> i + 1 <= m" by uint_arith lemma inc_i: - "(1 :: 'a :: len word) <= i ==> i < m ==> 1 <= (i + 1) & i + 1 <= m" + "(1 :: 'a :: finite word) <= i ==> i < m ==> 1 <= (i + 1) & i + 1 <= m" by uint_arith lemma udvd_incr_lem: @@ -729,36 +729,36 @@ subsection "Arithmetic type class instantiations" -instance word :: (len0) comm_monoid_add .. +instance word :: (type) comm_monoid_add .. -instance word :: (len0) comm_monoid_mult +instance word :: (type) comm_monoid_mult apply (intro_classes) apply (simp add: word_mult_commute) apply (simp add: word_mult_1) done -instance word :: (len0) comm_semiring +instance word :: (type) comm_semiring by (intro_classes) (simp add : word_left_distrib) -instance word :: (len0) ab_group_add .. +instance word :: (type) ab_group_add .. -instance word :: (len0) comm_ring .. +instance word :: (type) comm_ring .. -instance word :: (len) comm_semiring_1 +instance word :: (finite) comm_semiring_1 by (intro_classes) (simp add: lenw1_zero_neq_one) -instance word :: (len) comm_ring_1 .. +instance word :: (finite) comm_ring_1 .. -instance word :: (len0) comm_semiring_0 .. +instance word :: (type) comm_semiring_0 .. -instance word :: (len) recpower +instance word :: (finite) recpower by (intro_classes) (simp_all add: word_pow) (* note that iszero_def is only for class comm_semiring_1_cancel, - which requires word length >= 1, ie 'a :: len word *) + which requires word length >= 1, ie 'a :: finite word *) lemma zero_bintrunc: - "iszero (number_of x :: 'a :: len word) = - (bintrunc (len_of TYPE('a)) x = Numeral.Pls)" + "iszero (number_of x :: 'a :: finite word) = + (bintrunc CARD('a) x = Numeral.Pls)" apply (unfold iszero_def word_0_wi word_no_wi) apply (rule word_ubin.norm_eq_iff [symmetric, THEN trans]) apply (simp add : Pls_def [symmetric]) @@ -781,15 +781,15 @@ by (simp add: of_nat_nat word_of_int) lemma word_number_of_eq: - "number_of w = (of_int w :: 'a :: len word)" + "number_of w = (of_int w :: 'a :: finite word)" unfolding word_number_of_def word_of_int by auto -instance word :: (len) number_ring +instance word :: (finite) number_ring by (intro_classes) (simp add : word_number_of_eq) lemma iszero_word_no [simp] : - "iszero (number_of bin :: 'a :: len word) = - iszero (number_of (bintrunc (len_of TYPE('a)) bin) :: int)" + "iszero (number_of bin :: 'a :: finite word) = + iszero (number_of (bintrunc CARD('a) bin) :: int)" apply (simp add: zero_bintrunc number_of_is_id) apply (unfold iszero_def Pls_def) apply (rule refl) @@ -799,7 +799,7 @@ subsection "Word and nat" lemma td_ext_unat': - "n = len_of TYPE ('a :: len) ==> + "n = CARD('a :: finite) ==> td_ext (unat :: 'a word => nat) of_nat (unats n) (%i. i mod 2 ^ n)" apply (unfold td_ext_def' unat_def word_of_nat unats_uints) @@ -812,24 +812,24 @@ lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm, standard] interpretation word_unat: - td_ext ["unat::'a::len word => nat" + td_ext ["unat::'a::finite word => nat" of_nat - "unats (len_of TYPE('a::len))" - "%i. i mod 2 ^ len_of TYPE('a::len)"] + "unats CARD('a::finite)" + "%i. i mod 2 ^ CARD('a::finite)"] by (rule td_ext_unat) lemmas td_unat = word_unat.td_thm lemmas unat_lt2p [iff] = word_unat.Rep [unfolded unats_def mem_Collect_eq] -lemma unat_le: "y <= unat (z :: 'a :: len word) ==> y : unats (len_of TYPE ('a))" +lemma unat_le: "y <= unat (z :: 'a :: finite word) ==> y : unats CARD('a)" apply (unfold unats_def) apply clarsimp apply (rule xtrans, rule unat_lt2p, assumption) done lemma word_nchotomy: - "ALL w. EX n. (w :: 'a :: len word) = of_nat n & n < 2 ^ len_of TYPE ('a)" + "ALL w. EX n. (w :: 'a :: finite word) = of_nat n & n < 2 ^ CARD('a)" apply (rule allI) apply (rule word_unat.Abs_cases) apply (unfold unats_def) @@ -837,8 +837,8 @@ done lemma of_nat_eq: - fixes w :: "'a::len word" - shows "(of_nat n = w) = (\q. n = unat w + q * 2 ^ len_of TYPE('a))" + fixes w :: "'a::finite word" + shows "(of_nat n = w) = (\q. n = unat w + q * 2 ^ CARD('a))" apply (rule trans) apply (rule word_unat.inverse_norm) apply (rule iffI) @@ -852,7 +852,7 @@ unfolding word_size by (rule of_nat_eq) lemma of_nat_0: - "(of_nat m = (0::'a::len word)) = (\q. m = q * 2 ^ len_of TYPE('a))" + "(of_nat m = (0::'a::finite word)) = (\q. m = q * 2 ^ CARD('a))" by (simp add: of_nat_eq) lemmas of_nat_2p = mult_1 [symmetric, THEN iffD2 [OF of_nat_0 exI]] @@ -861,7 +861,7 @@ by (cases k) auto lemma of_nat_neq_0: - "0 < k ==> k < 2 ^ len_of TYPE ('a :: len) ==> of_nat k ~= (0 :: 'a word)" + "0 < k ==> k < 2 ^ CARD('a :: finite) ==> of_nat k ~= (0 :: 'a word)" by (clarsimp simp add : of_nat_0) lemma Abs_fnat_hom_add: @@ -869,17 +869,17 @@ by simp lemma Abs_fnat_hom_mult: - "of_nat a * of_nat b = (of_nat (a * b) :: 'a :: len word)" + "of_nat a * of_nat b = (of_nat (a * b) :: 'a :: finite word)" by (simp add: word_of_nat word_of_int_mult_hom zmult_int) lemma Abs_fnat_hom_Suc: "word_succ (of_nat a) = of_nat (Suc a)" by (simp add: word_of_nat word_of_int_succ_hom add_ac) -lemma Abs_fnat_hom_0: "(0::'a::len word) = of_nat 0" +lemma Abs_fnat_hom_0: "(0::'a::finite word) = of_nat 0" by (simp add: word_of_nat word_0_wi) -lemma Abs_fnat_hom_1: "(1::'a::len word) = of_nat (Suc 0)" +lemma Abs_fnat_hom_1: "(1::'a::finite word) = of_nat (Suc 0)" by (simp add: word_of_nat word_1_wi) lemmas Abs_fnat_homs = @@ -921,14 +921,14 @@ [simplified linorder_not_less [symmetric], simplified] lemma unat_add_lem: - "(unat x + unat y < 2 ^ len_of TYPE('a)) = - (unat (x + y :: 'a :: len word) = unat x + unat y)" + "(unat x + unat y < 2 ^ CARD('a)) = + (unat (x + y :: 'a :: finite word) = unat x + unat y)" unfolding unat_word_ariths by (auto intro!: trans [OF _ nat_mod_lem]) lemma unat_mult_lem: - "(unat x * unat y < 2 ^ len_of TYPE('a)) = - (unat (x * y :: 'a :: len word) = unat x * unat y)" + "(unat x * unat y < 2 ^ CARD('a)) = + (unat (x * y :: 'a :: finite word) = unat x * unat y)" unfolding unat_word_ariths by (auto intro!: trans [OF _ nat_mod_lem]) @@ -936,7 +936,7 @@ trans [OF unat_word_ariths(1) mod_nat_add, simplified, standard] lemma le_no_overflow: - "x <= b ==> a <= a + b ==> x <= a + (b :: 'a :: len0 word)" + "x <= b ==> a <= a + b ==> x <= a + (b :: 'a word)" apply (erule order_trans) apply (erule olen_add_eqv [THEN iffD1]) done @@ -967,13 +967,13 @@ lemmas unat_sub_if' = unat_sub_if_size [unfolded word_size] -lemma unat_div: "unat ((x :: 'a :: len word) div y) = unat x div unat y" +lemma unat_div: "unat ((x :: 'a :: finite word) div y) = unat x div unat y" apply (simp add : unat_word_ariths) apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq']) apply (rule div_le_dividend) done -lemma unat_mod: "unat ((x :: 'a :: len word) mod y) = unat x mod unat y" +lemma unat_mod: "unat ((x :: 'a :: finite word) mod y) = unat x mod unat y" apply (clarsimp simp add : unat_word_ariths) apply (cases "unat y") prefer 2 @@ -982,25 +982,25 @@ apply auto done -lemma uint_div: "uint ((x :: 'a :: len word) div y) = uint x div uint y" +lemma uint_div: "uint ((x :: 'a :: finite word) div y) = uint x div uint y" unfolding uint_nat by (simp add : unat_div zdiv_int) -lemma uint_mod: "uint ((x :: 'a :: len word) mod y) = uint x mod uint y" +lemma uint_mod: "uint ((x :: 'a :: finite word) mod y) = uint x mod uint y" unfolding uint_nat by (simp add : unat_mod zmod_int) subsection {* Definition of unat\_arith tactic *} lemma unat_split: - fixes x::"'a::len word" + fixes x::"'a::finite word" shows "P (unat x) = - (ALL n. of_nat n = x & n < 2^len_of TYPE('a) --> P n)" + (ALL n. of_nat n = x & n < 2^CARD('a) --> P n)" by (auto simp: unat_of_nat) lemma unat_split_asm: - fixes x::"'a::len word" + fixes x::"'a::finite word" shows "P (unat x) = - (~(EX n. of_nat n = x & n < 2^len_of TYPE('a) & ~ P n))" + (~(EX n. of_nat n = x & n < 2^CARD('a) & ~ P n))" by (auto simp: unat_of_nat) lemmas of_nat_inverse = @@ -1044,10 +1044,10 @@ "solving word arithmetic via natural numbers and arith" lemma no_plus_overflow_unat_size: - "((x :: 'a :: len word) <= x + y) = (unat x + unat y < 2 ^ size x)" + "((x :: 'a :: finite word) <= x + y) = (unat x + unat y < 2 ^ size x)" unfolding word_size by unat_arith -lemma unat_sub: "b <= a ==> unat (a - b) = unat a - unat (b :: 'a :: len word)" +lemma unat_sub: "b <= a ==> unat (a - b) = unat a - unat (b :: 'a :: finite word)" by unat_arith lemmas no_olen_add_nat = no_plus_overflow_unat_size [unfolded word_size] @@ -1055,7 +1055,7 @@ lemmas unat_plus_simple = trans [OF no_olen_add_nat unat_add_lem, standard] lemma word_div_mult: - "(0 :: 'a :: len word) < y ==> unat x * unat y < 2 ^ len_of TYPE('a) ==> + "(0 :: 'a :: finite word) < y ==> unat x * unat y < 2 ^ CARD('a) ==> x * y div y = x" apply unat_arith apply clarsimp @@ -1063,8 +1063,8 @@ apply auto done -lemma div_lt': "(i :: 'a :: len word) <= k div x ==> - unat i * unat x < 2 ^ len_of TYPE('a)" +lemma div_lt': "(i :: 'a :: finite word) <= k div x ==> + unat i * unat x < 2 ^ CARD('a)" apply unat_arith apply clarsimp apply (drule mult_le_mono1) @@ -1074,7 +1074,7 @@ lemmas div_lt'' = order_less_imp_le [THEN div_lt'] -lemma div_lt_mult: "(i :: 'a :: len word) < k div x ==> 0 < x ==> i * x < k" +lemma div_lt_mult: "(i :: 'a :: finite word) < k div x ==> 0 < x ==> i * x < k" apply (frule div_lt'' [THEN unat_mult_lem [THEN iffD1]]) apply (simp add: unat_arith_simps) apply (drule (1) mult_less_mono1) @@ -1083,7 +1083,7 @@ done lemma div_le_mult: - "(i :: 'a :: len word) <= k div x ==> 0 < x ==> i * x <= k" + "(i :: 'a :: finite word) <= k div x ==> 0 < x ==> i * x <= k" apply (frule div_lt' [THEN unat_mult_lem [THEN iffD1]]) apply (simp add: unat_arith_simps) apply (drule mult_le_mono1) @@ -1092,7 +1092,7 @@ done lemma div_lt_uint': - "(i :: 'a :: len word) <= k div x ==> uint i * uint x < 2 ^ len_of TYPE('a)" + "(i :: 'a :: finite word) <= k div x ==> uint i * uint x < 2 ^ CARD('a)" apply (unfold uint_nat) apply (drule div_lt') apply (simp add: zmult_int zless_nat_eq_int_zless [symmetric] @@ -1102,8 +1102,8 @@ lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint'] lemma word_le_exists': - "(x :: 'a :: len0 word) <= y ==> - (EX z. y = x + z & uint x + uint z < 2 ^ len_of TYPE('a))" + "(x :: 'a word) <= y ==> + (EX z. y = x + z & uint x + uint z < 2 ^ CARD('a))" apply (rule exI) apply (rule conjI) apply (rule zadd_diff_inverse) @@ -1139,7 +1139,7 @@ mod_le_divisor div_le_dividend thd1 lemma word_mod_div_equality: - "(n div b) * b + (n mod b) = (n :: 'a :: len word)" + "(n div b) * b + (n mod b) = (n :: 'a :: finite word)" apply (unfold word_less_nat_alt word_arith_nat_defs) apply (cut_tac y="unat b" in gt_or_eq_0) apply (erule disjE) @@ -1147,7 +1147,7 @@ apply simp done -lemma word_div_mult_le: "a div b * b <= (a::'a::len word)" +lemma word_div_mult_le: "a div b * b <= (a::'a::finite word)" apply (unfold word_le_nat_alt word_arith_nat_defs) apply (cut_tac y="unat b" in gt_or_eq_0) apply (erule disjE) @@ -1155,17 +1155,17 @@ apply simp done -lemma word_mod_less_divisor: "0 < n ==> m mod n < (n :: 'a :: len word)" +lemma word_mod_less_divisor: "0 < n ==> m mod n < (n :: 'a :: finite word)" apply (simp only: word_less_nat_alt word_arith_nat_defs) apply (clarsimp simp add : uno_simps) done lemma word_of_int_power_hom: - "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a :: len word)" + "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a :: finite word)" by (induct n) (simp_all add : word_of_int_hom_syms power_Suc) lemma word_arith_power_alt: - "a ^ n = (word_of_int (uint a ^ n) :: 'a :: len word)" + "a ^ n = (word_of_int (uint a ^ n) :: 'a :: finite word)" by (simp add : word_of_int_power_hom [symmetric]) @@ -1178,7 +1178,7 @@ lemmas card_word = trans [OF card_eq card_lessThan', standard] -lemma finite_word_UNIV: "finite (UNIV :: 'a :: len word set)" +lemma finite_word_UNIV: "finite (UNIV :: 'a :: finite word set)" apply (rule contrapos_np) prefer 2 apply (erule card_infinite) @@ -1186,7 +1186,7 @@ done lemma card_word_size: - "card (UNIV :: 'a :: len word set) = (2 ^ size (x :: 'a word))" + "card (UNIV :: 'a :: finite word set) = (2 ^ size (x :: 'a word))" unfolding word_size by (rule card_word) end diff -r 61b10ffb2549 -r 058c5613a86f src/HOL/Word/WordBitwise.thy --- a/src/HOL/Word/WordBitwise.thy Wed Aug 22 20:59:19 2007 +0200 +++ b/src/HOL/Word/WordBitwise.thy Wed Aug 22 21:09:21 2007 +0200 @@ -38,7 +38,7 @@ 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) & @@ -47,7 +47,7 @@ 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") @@ -66,7 +66,7 @@ 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" @@ -77,7 +77,7 @@ 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" @@ -87,7 +87,7 @@ 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" @@ -98,7 +98,7 @@ 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" @@ -116,7 +116,7 @@ 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" @@ -125,7 +125,7 @@ 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" @@ -134,7 +134,7 @@ 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" @@ -149,12 +149,12 @@ 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] @@ -162,7 +162,7 @@ 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] @@ -170,28 +170,28 @@ 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) @@ -201,10 +201,10 @@ 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)" @@ -215,13 +215,13 @@ 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) @@ -230,17 +230,17 @@ 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) @@ -250,33 +250,33 @@ 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) @@ -284,22 +284,22 @@ 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 \ len_of TYPE ('a)" + fixes w :: "'a::finite word" + defines "l \ 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) @@ -312,7 +312,7 @@ 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) @@ -322,7 +322,7 @@ 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) @@ -338,7 +338,7 @@ 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) @@ -348,9 +348,9 @@ 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 @@ -362,9 +362,9 @@ 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]) @@ -374,7 +374,7 @@ 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) @@ -382,7 +382,7 @@ 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 @@ -392,7 +392,7 @@ 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 diff -r 61b10ffb2549 -r 058c5613a86f src/HOL/Word/WordBoolList.thy --- a/src/HOL/Word/WordBoolList.thy Wed Aug 22 20:59:19 2007 +0200 +++ b/src/HOL/Word/WordBoolList.thy Wed Aug 22 21:09:21 2007 +0200 @@ -8,33 +8,33 @@ theory WordBoolList imports BinBoolList WordBitwise begin constdefs - of_bl :: "bool list => 'a :: len0 word" + of_bl :: "bool list => 'a word" "of_bl bl == word_of_int (bl_to_bin bl)" - to_bl :: "'a :: len0 word => bool list" + to_bl :: "'a word => bool list" "to_bl w == - bin_to_bl (len_of TYPE ('a)) (uint w)" + bin_to_bl CARD('a) (uint w)" - word_reverse :: "'a :: len0 word => 'a word" + word_reverse :: "'a word => 'a word" "word_reverse w == of_bl (rev (to_bl w))" defs (overloaded) word_set_bits_def: - "(BITS n. f n)::'a::len0 word == of_bl (bl_of_nth (len_of TYPE ('a)) f)" + "(BITS n. f n)::'a word == of_bl (bl_of_nth CARD('a) f)" lemmas of_nth_def = word_set_bits_def lemma to_bl_def': - "(to_bl :: 'a :: len0 word => bool list) = - bin_to_bl (len_of TYPE('a)) o uint" + "(to_bl :: 'a word => bool list) = + bin_to_bl CARD('a) o uint" by (auto simp: to_bl_def intro: ext) lemmas word_reverse_no_def [simp] = word_reverse_def [of "number_of ?w"] (* type definitions theorem for in terms of equivalent bool list *) lemma td_bl: - "type_definition (to_bl :: 'a::len0 word => bool list) + "type_definition (to_bl :: 'a word => bool list) of_bl - {bl. length bl = len_of TYPE('a)}" + {bl. length bl = CARD('a)}" apply (unfold type_definition_def of_bl_def to_bl_def) apply (simp add: word_ubin.eq_norm) apply safe @@ -43,9 +43,9 @@ done interpretation word_bl: - type_definition ["to_bl :: 'a::len0 word => bool list" + type_definition ["to_bl :: 'a word => bool list" of_bl - "{bl. length bl = len_of TYPE('a::len0)}"] + "{bl. length bl = CARD('a)}"] by (rule td_bl) lemma word_size_bl: "size w == size (to_bl w)" @@ -66,7 +66,7 @@ lemmas word_rev_gal' = sym [THEN word_rev_gal, symmetric, standard] -lemmas length_bl_gt_0 [iff] = xtr1 [OF word_bl.Rep' len_gt_0, standard] +lemmas length_bl_gt_0 [iff] = xtr1 [OF word_bl.Rep' zero_less_card_finite, standard] lemmas bl_not_Nil [iff] = length_bl_gt_0 [THEN length_greater_0_conv [THEN iffD1], standard] lemmas length_bl_neq_0 [iff] = length_bl_gt_0 [THEN gr_implies_not0] @@ -78,7 +78,7 @@ done lemma of_bl_drop': - "lend = length bl - len_of TYPE ('a :: len0) ==> + "lend = length bl - CARD('a) ==> of_bl (drop lend bl) = (of_bl bl :: 'a word)" apply (unfold of_bl_def) apply (clarsimp simp add : trunc_bl2bin [symmetric]) @@ -87,13 +87,13 @@ lemmas of_bl_no = of_bl_def [folded word_number_of_def] lemma test_bit_of_bl: - "(of_bl bl::'a::len0 word) !! n = (rev bl ! n \ n < len_of TYPE('a) \ n < length bl)" + "(of_bl bl::'a word) !! n = (rev bl ! n \ n < CARD('a) \ n < length bl)" apply (unfold of_bl_def word_test_bit_def) apply (auto simp add: word_size word_ubin.eq_norm nth_bintr bin_nth_of_bl) done lemma no_of_bl: - "(number_of bin ::'a::len0 word) = of_bl (bin_to_bl (len_of TYPE ('a)) bin)" + "(number_of bin ::'a word) = of_bl (bin_to_bl CARD('a) bin)" unfolding word_size of_bl_no by (simp add : word_number_of_def) lemma uint_bl: "to_bl w == bin_to_bl (size w) (uint w)" @@ -103,7 +103,7 @@ unfolding uint_bl by (simp add : word_size) lemma to_bl_of_bin: - "to_bl (word_of_int bin::'a::len0 word) = bin_to_bl (len_of TYPE('a)) bin" + "to_bl (word_of_int bin::'a word) = bin_to_bl CARD('a) bin" unfolding uint_bl by (clarsimp simp add: word_ubin.eq_norm word_size) lemmas to_bl_no_bin [simp] = to_bl_of_bin [folded word_number_of_def] @@ -131,9 +131,9 @@ by (auto simp add : word_size) lemma to_bl_ucast: - "to_bl (ucast (w::'b::len0 word) ::'a::len0 word) = - replicate (len_of TYPE('a) - len_of TYPE('b)) False @ - drop (len_of TYPE('b) - len_of TYPE('a)) (to_bl w)" + "to_bl (ucast (w::'b word) ::'a word) = + replicate (CARD('a) - CARD('b)) False @ + drop (CARD('b) - CARD('a)) (to_bl w)" apply (unfold ucast_bl) apply (rule trans) apply (rule word_rep_drop) @@ -190,7 +190,7 @@ by (simp add : word_0_wi of_bl_def bl_to_bin_rep_False Pls_def) lemma to_bl_0: - "to_bl (0::'a::len0 word) = replicate (len_of TYPE('a)) False" + "to_bl (0::'a word) = replicate CARD('a) False" unfolding uint_bl by (simp add : word_size bin_to_bl_Pls Pls_def [symmetric]) @@ -243,7 +243,7 @@ word_pred_rbl word_mult_rbl word_add_rbl) lemma of_bl_length_less: - "length x = k ==> k < len_of TYPE('a) ==> (of_bl x :: 'a :: len word) < 2 ^ k" + "length x = k ==> k < CARD('a) ==> (of_bl x :: 'a :: finite word) < 2 ^ k" apply (unfold of_bl_no [unfolded word_number_of_def] word_less_alt word_number_of_alt) apply safe @@ -276,7 +276,7 @@ unfolding to_bl_def word_log_defs by (simp add: bl_and_bin number_of_is_id word_no_wi [symmetric]) -lemma word_lsb_last: "lsb (w::'a::len word) = last (to_bl w)" +lemma word_lsb_last: "lsb (w::'a::finite word) = last (to_bl w)" apply (unfold word_lsb_def uint_bl bin_to_bl_def) apply (rule_tac bin="uint w" in bin_exhaust) apply (cases "size w") @@ -284,7 +284,7 @@ apply (auto simp add: bin_to_bl_aux_alt) done -lemma word_msb_alt: "msb (w::'a::len word) = hd (to_bl w)" +lemma word_msb_alt: "msb (w::'a::finite word) = hd (to_bl w)" apply (unfold word_msb_nth uint_bl) apply (subst hd_conv_nth) apply (rule length_greater_0_conv [THEN iffD1]) @@ -318,7 +318,7 @@ unfolding of_bl_def bl_to_bin_rep_F by auto lemma td_ext_nth': - "n = size (w::'a::len0 word) ==> ofn = set_bits ==> [w, ofn g] = l ==> + "n = size (w::'a word) ==> ofn = set_bits ==> [w, ofn g] = l ==> td_ext test_bit ofn {f. ALL i. f i --> i < n} (%h i. h i & i < n)" apply (unfold word_size td_ext_def') apply safe @@ -339,10 +339,10 @@ lemmas td_ext_nth = td_ext_nth' [OF refl refl refl, unfolded word_size] interpretation test_bit: - td_ext ["op !! :: 'a::len0 word => nat => bool" + td_ext ["op !! :: 'a word => nat => bool" set_bits - "{f. \i. f i \ i < len_of TYPE('a::len0)}" - "(\h i. h i \ i < len_of TYPE('a::len0))"] + "{f. \i. f i \ i < CARD('a)}" + "(\h i. h i \ i < CARD('a))"] by (rule td_ext_nth) declare test_bit.Rep' [simp del] @@ -351,7 +351,7 @@ lemmas td_nth = test_bit.td_thm lemma to_bl_n1: - "to_bl (-1::'a::len0 word) = replicate (len_of TYPE ('a)) True" + "to_bl (-1::'a word) = replicate CARD('a) True" apply (rule word_bl.Abs_inverse') apply simp apply (rule word_eqI) diff -r 61b10ffb2549 -r 058c5613a86f src/HOL/Word/WordDefinition.thy --- a/src/HOL/Word/WordDefinition.thy Wed Aug 22 20:59:19 2007 +0200 +++ b/src/HOL/Word/WordDefinition.thy Wed Aug 22 21:09:21 2007 +0200 @@ -8,12 +8,13 @@ header {* Definition of Word Type *} -theory WordDefinition imports Size BinOperations TdThs begin +theory WordDefinition +imports Numeral_Type BinOperations TdThs begin typedef (open word) 'a word - = "{(0::int) ..< 2^len_of TYPE('a::len0)}" by auto + = "{(0::int) ..< 2^CARD('a)}" by auto -instance word :: (len0) number .. +instance word :: (type) number .. instance word :: (type) minus .. instance word :: (type) plus .. instance word :: (type) one .. @@ -30,17 +31,17 @@ constdefs -- {* representation of words using unsigned or signed bins, only difference in these is the type class *} - word_of_int :: "int => 'a :: len0 word" - "word_of_int w == Abs_word (bintrunc (len_of TYPE ('a)) w)" + word_of_int :: "int => 'a word" + "word_of_int w == Abs_word (bintrunc CARD('a) w)" -- {* uint and sint cast a word to an integer, uint treats the word as unsigned, sint treats the most-significant-bit as a sign bit *} - uint :: "'a :: len0 word => int" + uint :: "'a word => int" "uint w == Rep_word w" - sint :: "'a :: len word => int" - sint_uint: "sint w == sbintrunc (len_of TYPE ('a) - 1) (uint w)" - unat :: "'a :: len0 word => nat" + sint :: "'a :: finite word => int" + sint_uint: "sint w == sbintrunc (CARD('a) - 1) (uint w)" + unat :: "'a word => nat" "unat w == nat (uint w)" -- "the sets of integers representing the words" @@ -54,11 +55,11 @@ "norm_sint n w == (w + 2 ^ (n - 1)) mod 2 ^ n - 2 ^ (n - 1)" defs (overloaded) - word_size: "size (w :: 'a :: len0 word) == len_of TYPE('a)" + word_size: "size (w :: 'a word) == CARD('a)" word_number_of_def: "number_of w == word_of_int w" constdefs - word_int_case :: "(int => 'b) => ('a :: len0 word) => 'b" + word_int_case :: "(int => 'b) => ('a word) => 'b" "word_int_case f w == f (uint w)" syntax @@ -70,18 +71,18 @@ subsection "Arithmetic operations" defs (overloaded) - word_1_wi: "(1 :: ('a :: len0) word) == word_of_int 1" - word_0_wi: "(0 :: ('a :: len0) word) == word_of_int 0" + word_1_wi: "(1 :: ('a) word) == word_of_int 1" + word_0_wi: "(0 :: ('a) word) == word_of_int 0" constdefs - word_succ :: "'a :: len0 word => 'a word" + word_succ :: "'a word => 'a word" "word_succ a == word_of_int (Numeral.succ (uint a))" - word_pred :: "'a :: len0 word => 'a word" + word_pred :: "'a word => 'a word" "word_pred a == word_of_int (Numeral.pred (uint a))" consts - word_power :: "'a :: len0 word => nat => 'a word" + word_power :: "'a word => nat => 'a word" primrec "word_power a 0 = 1" "word_power a (Suc n) = a * word_power a n" @@ -98,46 +99,46 @@ defs (overloaded) word_and_def: - "(a::'a::len0 word) AND b == word_of_int (uint a AND uint b)" + "(a::'a word) AND b == word_of_int (uint a AND uint b)" word_or_def: - "(a::'a::len0 word) OR b == word_of_int (uint a OR uint b)" + "(a::'a word) OR b == word_of_int (uint a OR uint b)" word_xor_def: - "(a::'a::len0 word) XOR b == word_of_int (uint a XOR uint b)" + "(a::'a word) XOR b == word_of_int (uint a XOR uint b)" word_not_def: - "NOT (a::'a::len0 word) == word_of_int (NOT (uint a))" + "NOT (a::'a word) == word_of_int (NOT (uint a))" word_test_bit_def: - "test_bit (a::'a::len0 word) == bin_nth (uint a)" + "test_bit (a::'a word) == bin_nth (uint a)" word_set_bit_def: - "set_bit (a::'a::len0 word) n x == + "set_bit (a::'a word) n x == word_of_int (bin_sc n (If x bit.B1 bit.B0) (uint a))" word_lsb_def: - "lsb (a::'a::len0 word) == bin_last (uint a) = bit.B1" + "lsb (a::'a word) == bin_last (uint a) = bit.B1" word_msb_def: - "msb (a::'a::len word) == bin_sign (sint a) = Numeral.Min" + "msb (a::'a::finite word) == bin_sign (sint a) = Numeral.Min" constdefs - setBit :: "'a :: len0 word => nat => 'a word" + setBit :: "'a word => nat => 'a word" "setBit w n == set_bit w n True" - clearBit :: "'a :: len0 word => nat => 'a word" + clearBit :: "'a word => nat => 'a word" "clearBit w n == set_bit w n False" constdefs -- "Largest representable machine integer." - max_word :: "'a::len word" - "max_word \ word_of_int (2^len_of TYPE('a) - 1)" + max_word :: "'a::finite word" + "max_word \ word_of_int (2^CARD('a) - 1)" consts - of_bool :: "bool \ 'a::len word" + of_bool :: "bool \ 'a::finite word" primrec "of_bool False = 0" "of_bool True = 1" @@ -145,8 +146,8 @@ lemmas word_size_gt_0 [iff] = - xtr1 [OF word_size [THEN meta_eq_to_obj_eq] len_gt_0, standard] -lemmas lens_gt_0 = word_size_gt_0 len_gt_0 + xtr1 [OF word_size [THEN meta_eq_to_obj_eq] zero_less_card_finite, standard] +lemmas lens_gt_0 = word_size_gt_0 zero_less_card_finite lemmas lens_not_0 [iff] = lens_gt_0 [THEN gr_implies_not0, standard] lemma uints_num: "uints n = {i. 0 \ i \ i < 2 ^ n}" @@ -163,16 +164,16 @@ lemma Rep_word_0:"0 <= Rep_word x" and - Rep_word_lt: "Rep_word (x::'a::len0 word) < 2 ^ len_of TYPE('a)" + Rep_word_lt: "Rep_word (x::'a word) < 2 ^ CARD('a)" by (auto simp: Rep_word [simplified]) lemma Rep_word_mod_same: - "Rep_word x mod 2 ^ len_of TYPE('a) = Rep_word (x::'a::len0 word)" + "Rep_word x mod 2 ^ CARD('a) = Rep_word (x::'a word)" by (simp add: int_mod_eq Rep_word_lt Rep_word_0) lemma td_ext_uint: - "td_ext (uint :: 'a word => int) word_of_int (uints (len_of TYPE('a::len0))) - (%w::int. w mod 2 ^ len_of TYPE('a))" + "td_ext (uint :: 'a word => int) word_of_int (uints CARD('a)) + (%w::int. w mod 2 ^ CARD('a))" apply (unfold td_ext_def') apply (simp add: uints_num uint_def word_of_int_def bintrunc_mod2p) apply (simp add: Rep_word_mod_same Rep_word_0 Rep_word_lt @@ -182,33 +183,34 @@ lemmas int_word_uint = td_ext_uint [THEN td_ext.eq_norm, standard] interpretation word_uint: - td_ext ["uint::'a::len0 word \ int" + td_ext ["uint::'a word \ int" word_of_int - "uints (len_of TYPE('a::len0))" - "\w. w mod 2 ^ len_of TYPE('a::len0)"] + "uints CARD('a)" + "\w. w mod 2 ^ CARD('a)"] by (rule td_ext_uint) lemmas td_uint = word_uint.td_thm lemmas td_ext_ubin = td_ext_uint - [simplified len_gt_0 no_bintr_alt1 [symmetric]] + [simplified zero_less_card_finite no_bintr_alt1 [symmetric]] interpretation word_ubin: - td_ext ["uint::'a::len0 word \ int" + td_ext ["uint::'a word \ int" word_of_int - "uints (len_of TYPE('a::len0))" - "bintrunc (len_of TYPE('a::len0))"] + "uints CARD('a)" + "bintrunc CARD('a)"] by (rule td_ext_ubin) lemma sint_sbintrunc': "sint (word_of_int bin :: 'a word) = - (sbintrunc (len_of TYPE ('a :: len) - 1) bin)" + (sbintrunc (CARD('a :: finite) - 1) bin)" unfolding sint_uint by (auto simp: word_ubin.eq_norm sbintrunc_bintrunc_lt) lemma uint_sint: - "uint w = bintrunc (len_of TYPE('a)) (sint (w :: 'a :: len word))" + "uint w = bintrunc CARD('a) (sint (w :: 'a :: finite word))" unfolding sint_uint by (auto simp: bintrunc_sbintrunc_le) + lemma bintr_uint': "n >= size w ==> bintrunc n (uint w) = uint w" @@ -228,11 +230,11 @@ lemmas wi_bintr = wi_bintr' [unfolded word_size] lemma td_ext_sbin: - "td_ext (sint :: 'a word => int) word_of_int (sints (len_of TYPE('a::len))) - (sbintrunc (len_of TYPE('a) - 1))" + "td_ext (sint :: 'a word => int) word_of_int (sints CARD('a::finite)) + (sbintrunc (CARD('a) - 1))" apply (unfold td_ext_def' sint_uint) apply (simp add : word_ubin.eq_norm) - apply (cases "len_of TYPE('a)") + apply (cases "CARD('a)") apply (auto simp add : sints_def) apply (rule sym [THEN trans]) apply (rule word_ubin.Abs_norm) @@ -242,25 +244,25 @@ done lemmas td_ext_sint = td_ext_sbin - [simplified len_gt_0 no_sbintr_alt2 Suc_pred' [symmetric]] + [simplified zero_less_card_finite no_sbintr_alt2 Suc_pred' [symmetric]] (* We do sint before sbin, before sint is the user version and interpretations do not produce thm duplicates. I.e. we get the name word_sint.Rep_eqD, but not word_sbin.Req_eqD, because the latter is the same thm as the former *) interpretation word_sint: - td_ext ["sint ::'a::len word => int" + td_ext ["sint ::'a::finite word => int" word_of_int - "sints (len_of TYPE('a::len))" - "%w. (w + 2^(len_of TYPE('a::len) - 1)) mod 2^len_of TYPE('a::len) - - 2 ^ (len_of TYPE('a::len) - 1)"] + "sints CARD('a::finite)" + "%w. (w + 2^(CARD('a::finite) - 1)) mod 2^CARD('a::finite) - + 2 ^ (CARD('a::finite) - 1)"] by (rule td_ext_sint) interpretation word_sbin: - td_ext ["sint ::'a::len word => int" + td_ext ["sint ::'a::finite word => int" word_of_int - "sints (len_of TYPE('a::len))" - "sbintrunc (len_of TYPE('a::len) - 1)"] + "sints CARD('a::finite)" + "sbintrunc (CARD('a::finite) - 1)"] by (rule td_ext_sbin) lemmas int_word_sint = td_ext_sint [THEN td_ext.eq_norm, standard] @@ -276,18 +278,18 @@ lemmas uints_mod = uints_def [unfolded no_bintr_alt1] lemma uint_bintrunc: "uint (number_of bin :: 'a word) = - number_of (bintrunc (len_of TYPE ('a :: len0)) bin)" + number_of (bintrunc CARD('a) bin)" unfolding word_number_of_def number_of_eq by (auto intro: word_ubin.eq_norm) lemma sint_sbintrunc: "sint (number_of bin :: 'a word) = - number_of (sbintrunc (len_of TYPE ('a :: len) - 1) bin)" + number_of (sbintrunc (CARD('a :: finite) - 1) bin)" unfolding word_number_of_def number_of_eq by (auto intro!: word_sbin.eq_norm simp del: one_is_Suc_zero) lemma unat_bintrunc: - "unat (number_of bin :: 'a :: len0 word) = - number_of (bintrunc (len_of TYPE('a)) bin)" + "unat (number_of bin :: 'a word) = + number_of (bintrunc CARD('a) bin)" unfolding unat_def nat_number_of_def by (simp only: uint_bintrunc) @@ -297,7 +299,7 @@ sint_sbintrunc [simp] unat_bintrunc [simp] -lemma size_0_eq: "size (w :: 'a :: len0 word) = 0 ==> v = w" +lemma size_0_eq: "size (w :: 'a word) = 0 ==> v = w" apply (unfold word_size) apply (rule word_uint.Rep_eqD) apply (rule box_equals) @@ -322,7 +324,7 @@ iffD2 [OF linorder_not_le uint_m2p_neg, standard] lemma lt2p_lem: - "len_of TYPE('a) <= n ==> uint (w :: 'a :: len0 word) < 2 ^ n" + "CARD('a) <= n ==> uint (w :: 'a word) < 2 ^ n" by (rule xtr8 [OF _ uint_lt2p]) simp lemmas uint_le_0_iff [simp] = @@ -332,13 +334,13 @@ unfolding unat_def by auto lemma uint_number_of: - "uint (number_of b :: 'a :: len0 word) = number_of b mod 2 ^ len_of TYPE('a)" + "uint (number_of b :: 'a word) = number_of b mod 2 ^ CARD('a)" unfolding word_number_of_alt by (simp only: int_word_uint) lemma unat_number_of: "bin_sign b = Numeral.Pls ==> - unat (number_of b::'a::len0 word) = number_of b mod 2 ^ len_of TYPE ('a)" + unat (number_of b::'a word) = number_of b mod 2 ^ CARD('a)" apply (unfold unat_def) apply (clarsimp simp only: uint_number_of) apply (rule nat_mod_distrib [THEN trans]) @@ -346,31 +348,31 @@ apply (simp_all add: nat_power_eq) done -lemma sint_number_of: "sint (number_of b :: 'a :: len word) = (number_of b + - 2 ^ (len_of TYPE('a) - 1)) mod 2 ^ len_of TYPE('a) - - 2 ^ (len_of TYPE('a) - 1)" +lemma sint_number_of: "sint (number_of b :: 'a :: finite word) = (number_of b + + 2 ^ (CARD('a) - 1)) mod 2 ^ CARD('a) - + 2 ^ (CARD('a) - 1)" unfolding word_number_of_alt by (rule int_word_sint) lemma word_of_int_bin [simp] : - "(word_of_int (number_of bin) :: 'a :: len0 word) = (number_of bin)" + "(word_of_int (number_of bin) :: 'a word) = (number_of bin)" unfolding word_number_of_alt by auto lemma word_int_case_wi: "word_int_case f (word_of_int i :: 'b word) = - f (i mod 2 ^ len_of TYPE('b::len0))" + f (i mod 2 ^ CARD('b))" unfolding word_int_case_def by (simp add: word_uint.eq_norm) lemma word_int_split: "P (word_int_case f x) = - (ALL i. x = (word_of_int i :: 'b :: len0 word) & - 0 <= i & i < 2 ^ len_of TYPE('b) --> P (f i))" + (ALL i. x = (word_of_int i :: 'b word) & + 0 <= i & i < 2 ^ CARD('b) --> P (f i))" unfolding word_int_case_def by (auto simp: word_uint.eq_norm int_mod_eq') lemma word_int_split_asm: "P (word_int_case f x) = - (~ (EX n. x = (word_of_int n :: 'b::len0 word) & - 0 <= n & n < 2 ^ len_of TYPE('b::len0) & ~ P (f n)))" + (~ (EX n. x = (word_of_int n :: 'b word) & + 0 <= n & n < 2 ^ CARD('b) & ~ P (f n)))" unfolding word_int_case_def by (auto simp: word_uint.eq_norm int_mod_eq') @@ -392,10 +394,10 @@ lemmas sint_below_size = sint_range_size [THEN conjunct1, THEN [2] order_trans, folded One_nat_def, standard] -lemma test_bit_eq_iff: "(test_bit (u::'a::len0 word) = test_bit v) = (u = v)" +lemma test_bit_eq_iff: "(test_bit (u::'a word) = test_bit v) = (u = v)" unfolding word_test_bit_def by (simp add: bin_nth_eq_iff) -lemma test_bit_size [rule_format] : "(w::'a::len0 word) !! n --> n < size w" +lemma test_bit_size [rule_format] : "(w::'a word) !! n --> n < size w" apply (unfold word_test_bit_def) apply (subst word_ubin.norm_Rep [symmetric]) apply (simp only: nth_bintr word_size) @@ -403,7 +405,7 @@ done lemma word_eqI [rule_format] : - fixes u :: "'a::len0 word" + fixes u :: "'a word" shows "(ALL n. n < size u --> u !! n = v !! n) ==> u = v" apply (rule test_bit_eq_iff [THEN iffD1]) apply (rule ext) @@ -475,14 +477,14 @@ may want these in reverse, but loop as simp rules, so use following *) lemma num_of_bintr': - "bintrunc (len_of TYPE('a :: len0)) a = b ==> + "bintrunc CARD('a) a = b ==> number_of a = (number_of b :: 'a word)" apply safe apply (rule_tac num_of_bintr [symmetric]) done lemma num_of_sbintr': - "sbintrunc (len_of TYPE('a :: len) - 1) a = b ==> + "sbintrunc (CARD('a :: finite) - 1) a = b ==> number_of a = (number_of b :: 'a word)" apply safe apply (rule_tac num_of_sbintr [symmetric]) @@ -503,19 +505,19 @@ constdefs -- "cast a word to a different length" - scast :: "'a :: len word => 'b :: len word" + scast :: "'a :: finite word => 'b :: finite word" "scast w == word_of_int (sint w)" - ucast :: "'a :: len0 word => 'b :: len0 word" + ucast :: "'a word => 'b word" "ucast w == word_of_int (uint w)" -- "whether a cast (or other) function is to a longer or shorter length" - source_size :: "('a :: len0 word => 'b) => nat" + source_size :: "('a word => 'b) => nat" "source_size c == let arb = arbitrary ; x = c arb in size arb" - target_size :: "('a => 'b :: len0 word) => nat" + target_size :: "('a => 'b word) => nat" "target_size c == size (c arbitrary)" - is_up :: "('a :: len0 word => 'b :: len0 word) => bool" + is_up :: "('a word => 'b word) => bool" "is_up c == source_size c <= target_size c" - is_down :: "('a :: len0 word => 'b :: len0 word) => bool" + is_down :: "('a word => 'b word) => bool" "is_down c == target_size c <= source_size c" (** cast - note, no arg for new length, as it's determined by type of result, @@ -528,7 +530,7 @@ unfolding scast_def by auto lemma nth_ucast: - "(ucast w::'a::len0 word) !! n = (w !! n & n < len_of TYPE('a))" + "(ucast w::'a word) !! n = (w !! n & n < CARD('a))" apply (unfold ucast_def test_bit_bin) apply (simp add: word_ubin.eq_norm nth_bintr word_size) apply (fast elim!: bin_nth_uint_imp) @@ -537,13 +539,13 @@ (* for literal u(s)cast *) lemma ucast_bintr [simp]: - "ucast (number_of w ::'a::len0 word) = - number_of (bintrunc (len_of TYPE('a)) w)" + "ucast (number_of w ::'a word) = + number_of (bintrunc CARD('a) w)" unfolding ucast_def by simp lemma scast_sbintr [simp]: - "scast (number_of w ::'a::len word) = - number_of (sbintrunc (len_of TYPE('a) - Suc 0) w)" + "scast (number_of w ::'a::finite word) = + number_of (sbintrunc (CARD('a) - Suc 0) w)" unfolding scast_def by simp lemmas source_size = source_size_def [unfolded Let_def word_size] @@ -616,22 +618,22 @@ lemmas scast_down_scast_id = isdus [THEN ucast_up_ucast_id] lemma up_ucast_surj: - "is_up (ucast :: 'b::len0 word => 'a::len0 word) ==> + "is_up (ucast :: 'b word => 'a word) ==> surj (ucast :: 'a word => 'b word)" by (rule surjI, erule ucast_up_ucast_id) lemma up_scast_surj: - "is_up (scast :: 'b::len word => 'a::len word) ==> + "is_up (scast :: 'b::finite word => 'a::finite word) ==> surj (scast :: 'a word => 'b word)" by (rule surjI, erule scast_up_scast_id) lemma down_scast_inj: - "is_down (scast :: 'b::len word => 'a::len word) ==> + "is_down (scast :: 'b::finite word => 'a::finite word) ==> inj_on (ucast :: 'a word => 'b word) A" by (rule inj_on_inverseI, erule scast_down_scast_id) lemma down_ucast_inj: - "is_down (ucast :: 'b::len0 word => 'a::len0 word) ==> + "is_down (ucast :: 'b word => 'a word) ==> inj_on (ucast :: 'a word => 'b word) A" by (rule inj_on_inverseI, erule ucast_down_ucast_id) diff -r 61b10ffb2549 -r 058c5613a86f src/HOL/Word/WordExamples.thy --- a/src/HOL/Word/WordExamples.thy Wed Aug 22 20:59:19 2007 +0200 +++ b/src/HOL/Word/WordExamples.thy Wed Aug 22 21:09:21 2007 +0200 @@ -21,12 +21,12 @@ -- "number ring simps" lemma - "27 + 11 = (38::'a::len word)" + "27 + 11 = (38::'a::finite word)" "27 + 11 = (6::5 word)" - "7 * 3 = (21::'a::len word)" - "11 - 27 = (-16::'a::len word)" - "- -11 = (11::'a::len word)" - "-40 + 1 = (-39::'a::len word)" + "7 * 3 = (21::'a::finite word)" + "11 - 27 = (-16::'a::finite word)" + "- -11 = (11::'a::finite word)" + "-40 + 1 = (-39::'a::finite word)" by simp_all lemma "word_pred 2 = 1" by simp @@ -56,12 +56,12 @@ lemma "scast (0b1010 :: 4 word) = (0b111010 :: 6 word)" by simp -- "reducing goals to nat or int and arith:" -lemma "i < x ==> i < (i + 1 :: 'a :: len word)" by unat_arith -lemma "i < x ==> i < (i + 1 :: 'a :: len word)" by uint_arith +lemma "i < x ==> i < (i + 1 :: 'a :: finite word)" by unat_arith +lemma "i < x ==> i < (i + 1 :: 'a :: finite word)" by uint_arith -- "bool lists" -lemma "of_bl [True, False, True, True] = (0b1011::'a::len word)" by simp +lemma "of_bl [True, False, True, True] = (0b1011::'a::finite word)" by simp lemma "to_bl (0b110::4 word) = [False, True, True, False]" by simp @@ -92,21 +92,21 @@ lemma "(0b11000 :: 10 word) !! n = (n = 4 \ n = 3)" by (auto simp add: bin_nth_Bit) -lemma "set_bit 55 7 True = (183::'a::len0 word)" by simp -lemma "set_bit 0b0010 7 True = (0b10000010::'a::len0 word)" by simp -lemma "set_bit 0b0010 1 False = (0::'a::len0 word)" by simp +lemma "set_bit 55 7 True = (183::'a word)" by simp +lemma "set_bit 0b0010 7 True = (0b10000010::'a word)" by simp +lemma "set_bit 0b0010 1 False = (0::'a word)" by simp -lemma "lsb (0b0101::'a::len word)" by simp -lemma "\ lsb (0b1000::'a::len word)" by simp +lemma "lsb (0b0101::'a::finite word)" by simp +lemma "\ lsb (0b1000::'a::finite word)" by simp lemma "\ msb (0b0101::4 word)" by simp lemma "msb (0b1000::4 word)" by simp -lemma "word_cat (27::4 word) (27::8 word) = (2843::'a::len word)" by simp +lemma "word_cat (27::4 word) (27::8 word) = (2843::'a::finite word)" by simp lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)" by simp -lemma "0b1011 << 2 = (0b101100::'a::len0 word)" by simp +lemma "0b1011 << 2 = (0b101100::'a word)" by simp lemma "0b1011 >> 2 = (0b10::8 word)" by simp lemma "0b1011 >>> 2 = (0b10::8 word)" by simp diff -r 61b10ffb2549 -r 058c5613a86f src/HOL/Word/WordGenLib.thy --- a/src/HOL/Word/WordGenLib.thy Wed Aug 22 20:59:19 2007 +0200 +++ b/src/HOL/Word/WordGenLib.thy Wed Aug 22 21:09:21 2007 +0200 @@ -14,17 +14,17 @@ declare of_nat_2p [simp] lemma word_int_cases: - "\\n. \(x ::'a::len0 word) = word_of_int n; 0 \ n; n < 2^len_of TYPE('a)\ \ P\ + "\\n. \(x ::'a word) = word_of_int n; 0 \ n; n < 2^CARD('a)\ \ P\ \ P" by (cases x rule: word_uint.Abs_cases) (simp add: uints_num) lemma word_nat_cases [cases type: word]: - "\\n. \(x ::'a::len word) = of_nat n; n < 2^len_of TYPE('a)\ \ P\ + "\\n. \(x ::'a::finite word) = of_nat n; n < 2^CARD('a)\ \ P\ \ P" by (cases x rule: word_unat.Abs_cases) (simp add: unats_def) lemma max_word_eq: - "(max_word::'a::len word) = 2^len_of TYPE('a) - 1" + "(max_word::'a::finite word) = 2^CARD('a) - 1" by (simp add: max_word_def word_of_int_hom_syms word_of_int_2p) lemma max_word_max [simp,intro!]: @@ -33,14 +33,14 @@ (simp add: max_word_def word_le_def int_word_uint int_mod_eq') lemma word_of_int_2p_len: - "word_of_int (2 ^ len_of TYPE('a)) = (0::'a::len0 word)" + "word_of_int (2 ^ CARD('a)) = (0::'a word)" by (subst word_uint.Abs_norm [symmetric]) (simp add: word_of_int_hom_syms) lemma word_pow_0: - "(2::'a::len word) ^ len_of TYPE('a) = 0" + "(2::'a::finite word) ^ CARD('a) = 0" proof - - have "word_of_int (2 ^ len_of TYPE('a)) = (0::'a word)" + have "word_of_int (2 ^ CARD('a)) = (0::'a word)" by (rule word_of_int_2p_len) thus ?thesis by (simp add: word_of_int_2p) qed @@ -53,18 +53,18 @@ done lemma max_word_minus: - "max_word = (-1::'a::len word)" + "max_word = (-1::'a::finite word)" proof - have "-1 + 1 = (0::'a word)" by simp thus ?thesis by (rule max_word_wrap [symmetric]) qed lemma max_word_bl [simp]: - "to_bl (max_word::'a::len word) = replicate (len_of TYPE('a)) True" + "to_bl (max_word::'a::finite word) = replicate CARD('a) True" by (subst max_word_minus to_bl_n1)+ simp lemma max_test_bit [simp]: - "(max_word::'a::len word) !! n = (n < len_of TYPE('a))" + "(max_word::'a::finite word) !! n = (n < CARD('a))" by (auto simp add: test_bit_bl word_size) lemma word_and_max [simp]: @@ -76,15 +76,15 @@ by (rule word_eqI) (simp add: word_ops_nth_size word_size) lemma word_ao_dist2: - "x AND (y OR z) = x AND y OR x AND (z::'a::len0 word)" + "x AND (y OR z) = x AND y OR x AND (z::'a word)" by (rule word_eqI) (auto simp add: word_ops_nth_size word_size) lemma word_oa_dist2: - "x OR y AND z = (x OR y) AND (x OR (z::'a::len0 word))" + "x OR y AND z = (x OR y) AND (x OR (z::'a word))" by (rule word_eqI) (auto simp add: word_ops_nth_size word_size) lemma word_and_not [simp]: - "x AND NOT x = (0::'a::len0 word)" + "x AND NOT x = (0::'a word)" by (rule word_eqI) (auto simp add: word_ops_nth_size word_size) lemma word_or_not [simp]: @@ -111,7 +111,7 @@ by (rule word_boolean) lemma word_xor_and_or: - "x XOR y = x AND NOT y OR NOT x AND (y::'a::len0 word)" + "x XOR y = x AND NOT y OR NOT x AND (y::'a word)" by (rule word_eqI) (auto simp add: word_ops_nth_size word_size) interpretation word_bool_alg: @@ -123,15 +123,15 @@ done lemma shiftr_0 [iff]: - "(x::'a::len0 word) >> 0 = x" + "(x::'a word) >> 0 = x" by (simp add: shiftr_bl) lemma shiftl_0 [simp]: - "(x :: 'a :: len word) << 0 = x" + "(x :: 'a :: finite word) << 0 = x" by (simp add: shiftl_t2n) lemma shiftl_1 [simp]: - "(1::'a::len word) << n = 2^n" + "(1::'a::finite word) << n = 2^n" by (simp add: shiftl_t2n) lemma uint_lt_0 [simp]: @@ -139,21 +139,21 @@ by (simp add: linorder_not_less) lemma shiftr1_1 [simp]: - "shiftr1 (1::'a::len word) = 0" + "shiftr1 (1::'a::finite word) = 0" by (simp add: shiftr1_def word_0_alt) lemma shiftr_1[simp]: - "(1::'a::len word) >> n = (if n = 0 then 1 else 0)" + "(1::'a::finite word) >> n = (if n = 0 then 1 else 0)" by (induct n) (auto simp: shiftr_def) lemma word_less_1 [simp]: - "((x::'a::len word) < 1) = (x = 0)" + "((x::'a::finite word) < 1) = (x = 0)" by (simp add: word_less_nat_alt unat_0_iff) lemma to_bl_mask: - "to_bl (mask n :: 'a::len word) = - replicate (len_of TYPE('a) - n) False @ - replicate (min (len_of TYPE('a)) n) True" + "to_bl (mask n :: 'a::finite word) = + replicate (CARD('a) - n) False @ + replicate (min CARD('a) n) True" by (simp add: mask_bl word_rep_drop min_def) lemma map_replicate_True: @@ -167,19 +167,19 @@ by (induct xs arbitrary: n) auto lemma bl_and_mask: - fixes w :: "'a::len word" + fixes w :: "'a::finite word" fixes n - defines "n' \ len_of TYPE('a) - n" + defines "n' \ CARD('a) - n" shows "to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)" proof - note [simp] = map_replicate_True map_replicate_False have "to_bl (w AND mask n) = - app2 op & (to_bl w) (to_bl (mask n::'a::len word))" + app2 op & (to_bl w) (to_bl (mask n::'a::finite word))" by (simp add: bl_word_and) also have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)" by simp also - have "app2 op & \ (to_bl (mask n::'a::len word)) = + have "app2 op & \ (to_bl (mask n::'a::finite word)) = replicate n' False @ drop n' (to_bl w)" unfolding to_bl_mask n'_def app2_def by (subst zip_append) auto @@ -193,7 +193,7 @@ by (simp add: takefill_alt rev_take) lemma map_nth_0 [simp]: - "map (op !! (0::'a::len0 word)) xs = replicate (length xs) False" + "map (op !! (0::'a word)) xs = replicate (length xs) False" by (induct xs) auto lemma uint_plus_if_size: @@ -206,7 +206,7 @@ word_size) lemma unat_plus_if_size: - "unat (x + (y::'a::len word)) = + "unat (x + (y::'a::finite word)) = (if unat x + unat y < 2^size x then unat x + unat y else @@ -217,7 +217,7 @@ done lemma word_neq_0_conv [simp]: - fixes w :: "'a :: len word" + fixes w :: "'a :: finite word" shows "(w \ 0) = (0 < w)" proof - have "0 \ w" by (rule word_zero_le) @@ -225,7 +225,7 @@ qed lemma max_lt: - "unat (max a b div c) = unat (max a b) div unat (c:: 'a :: len word)" + "unat (max a b div c) = unat (max a b) div unat (c:: 'a :: finite word)" apply (subst word_arith_nat_defs) apply (subst word_unat.eq_norm) apply (subst mod_if) @@ -253,12 +253,12 @@ lemmas unat_sub = unat_sub_simple lemma word_less_sub1: - fixes x :: "'a :: len word" + fixes x :: "'a :: finite word" shows "x \ 0 ==> 1 < x = (0 < x - 1)" by (simp add: unat_sub_if_size word_less_nat_alt) lemma word_le_sub1: - fixes x :: "'a :: len word" + fixes x :: "'a :: finite word" shows "x \ 0 ==> 1 \ x = (0 \ x - 1)" by (simp add: unat_sub_if_size order_le_less word_less_nat_alt) @@ -268,9 +268,9 @@ word_le_sub1 [of "number_of ?w"] lemma word_of_int_minus: - "word_of_int (2^len_of TYPE('a) - i) = (word_of_int (-i)::'a::len word)" + "word_of_int (2^CARD('a) - i) = (word_of_int (-i)::'a::finite word)" proof - - have x: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)" by simp + have x: "2^CARD('a) - i = -i + 2^CARD('a)" by simp show ?thesis apply (subst x) apply (subst word_uint.Abs_norm [symmetric], subst zmod_zadd_self2) @@ -282,7 +282,7 @@ word_uint.Abs_inject [unfolded uints_num, simplified] lemma word_le_less_eq: - "(x ::'z::len word) \ y = (x = y \ x < y)" + "(x ::'z::finite word) \ y = (x = y \ x < y)" by (auto simp add: word_less_def) lemma mod_plus_cong: @@ -312,7 +312,7 @@ done lemma word_induct_less: - "\P (0::'a::len word); \n. \n < m; P n\ \ P (1 + n)\ \ P m" + "\P (0::'a::finite word); \n. \n < m; P n\ \ P (1 + n)\ \ P m" apply (cases m) apply atomize apply (erule rev_mp)+ @@ -335,24 +335,24 @@ done lemma word_induct: - "\P (0::'a::len word); \n. P n \ P (1 + n)\ \ P m" + "\P (0::'a::finite word); \n. P n \ P (1 + n)\ \ P m" by (erule word_induct_less, simp) lemma word_induct2 [induct type]: - "\P 0; \n. \1 + n \ 0; P n\ \ P (1 + n)\ \ P (n::'b::len word)" + "\P 0; \n. \1 + n \ 0; P n\ \ P (1 + n)\ \ P (n::'b::finite word)" apply (rule word_induct, simp) apply (case_tac "1+n = 0", auto) done constdefs - word_rec :: "'a \ ('b::len word \ 'a \ 'a) \ 'b word \ 'a" + word_rec :: "'a \ ('b::finite word \ 'a \ 'a) \ 'b word \ 'a" "word_rec forZero forSuc n \ nat_rec forZero (forSuc \ of_nat) (unat n)" lemma word_rec_0: "word_rec z s 0 = z" by (simp add: word_rec_def) lemma word_rec_Suc: - "1 + n \ (0::'a::len word) \ word_rec z s (1 + n) = s n (word_rec z s n)" + "1 + n \ (0::'a::finite word) \ word_rec z s (1 + n) = s n (word_rec z s n)" apply (simp add: word_rec_def unat_word_ariths) apply (subst nat_mod_eq') apply (cut_tac x=n in unat_lt2p) @@ -448,7 +448,7 @@ done lemma unatSuc: - "1 + n \ (0::'a::len word) \ unat (1 + n) = Suc (unat n)" + "1 + n \ (0::'a::finite word) \ unat (1 + n) = Suc (unat n)" by unat_arith end diff -r 61b10ffb2549 -r 058c5613a86f src/HOL/Word/WordShift.thy --- a/src/HOL/Word/WordShift.thy Wed Aug 22 20:59:19 2007 +0200 +++ b/src/HOL/Word/WordShift.thy Wed Aug 22 21:09:21 2007 +0200 @@ -11,22 +11,22 @@ subsection "Bit shifting" constdefs - shiftl1 :: "'a :: len0 word => 'a word" + shiftl1 :: "'a word => 'a word" "shiftl1 w == word_of_int (uint w BIT bit.B0)" -- "shift right as unsigned or as signed, ie logical or arithmetic" - shiftr1 :: "'a :: len0 word => 'a word" + shiftr1 :: "'a word => 'a word" "shiftr1 w == word_of_int (bin_rest (uint w))" - sshiftr1 :: "'a :: len word => 'a word" + sshiftr1 :: "'a :: finite word => 'a word" "sshiftr1 w == word_of_int (bin_rest (sint w))" - sshiftr :: "'a :: len word => nat => 'a word" (infixl ">>>" 55) + sshiftr :: "'a :: finite word => nat => 'a word" (infixl ">>>" 55) "w >>> n == (sshiftr1 ^ n) w" defs (overloaded) - shiftl_def: "(w::'a::len0 word) << n == (shiftl1 ^ n) w" - shiftr_def: "(w::'a::len0 word) >> n == (shiftr1 ^ n) w" + shiftl_def: "(w::'a word) << n == (shiftl1 ^ n) w" + shiftr_def: "(w::'a word) >> n == (shiftr1 ^ n) w" lemma shiftl1_number [simp] : "shiftl1 (number_of w) = number_of (w BIT bit.B0)" @@ -58,10 +58,10 @@ lemma sshiftr1_n1 [simp] : "sshiftr1 -1 = -1" unfolding sshiftr1_def by auto -lemma shiftl_0 [simp] : "(0::'a::len0 word) << n = 0" +lemma shiftl_0 [simp] : "(0::'a word) << n = 0" unfolding shiftl_def by (induct n) auto -lemma shiftr_0 [simp] : "(0::'a::len0 word) >> n = 0" +lemma shiftr_0 [simp] : "(0::'a word) >> n = 0" unfolding shiftr_def by (induct n) auto lemma sshiftr_0 [simp] : "0 >>> n = 0" @@ -78,7 +78,7 @@ done lemma nth_shiftl' [rule_format]: - "ALL n. ((w::'a::len0 word) << m) !! n = (n < size w & n >= m & w !! (n - m))" + "ALL n. ((w::'a word) << m) !! n = (n < size w & n >= m & w !! (n - m))" apply (unfold shiftl_def) apply (induct "m") apply (force elim!: test_bit_size) @@ -97,7 +97,7 @@ done lemma nth_shiftr: - "\n. ((w::'a::len0 word) >> m) !! n = w !! (n + m)" + "\n. ((w::'a word) >> m) !! n = w !! (n + m)" apply (unfold shiftr_def) apply (induct "m") apply (auto simp add : nth_shiftr1) @@ -188,7 +188,7 @@ subsubsection "shift functions in terms of lists of bools" definition - bshiftr1 :: "bool => 'a :: len word => 'a word" where + bshiftr1 :: "bool => 'a :: finite word => 'a word" where "bshiftr1 b w == of_bl (b # butlast (to_bl w))" lemmas bshiftr1_no_bin [simp] = @@ -202,13 +202,11 @@ by (simp add: bl_to_bin_aux_append bl_to_bin_def) lemmas shiftl1_bl = shiftl1_of_bl - [where bl = "to_bl (?w :: ?'a :: len0 word)", simplified] + [where bl = "to_bl (?w :: ?'a word)", simplified] lemma bl_shiftl1: - "to_bl (shiftl1 (w :: 'a :: len word)) = tl (to_bl w) @ [False]" - apply (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons') - apply (fast intro!: Suc_leI) - done + "to_bl (shiftl1 (w :: 'a :: finite word)) = tl (to_bl w) @ [False]" + by (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons') lemma shiftr1_bl: "shiftr1 w = of_bl (butlast (to_bl w))" apply (unfold shiftr1_def uint_bl of_bl_def) @@ -217,15 +215,15 @@ done lemma bl_shiftr1: - "to_bl (shiftr1 (w :: 'a :: len word)) = False # butlast (to_bl w)" + "to_bl (shiftr1 (w :: 'a :: finite word)) = False # butlast (to_bl w)" unfolding shiftr1_bl - by (simp add : word_rep_drop len_gt_0 [THEN Suc_leI]) + by (simp add : word_rep_drop zero_less_card_finite [THEN Suc_leI]) -(* relate the two above : TODO - remove the :: len restriction on +(* relate the two above : TODO - remove the :: finite restriction on this theorem and others depending on it *) lemma shiftl1_rev: - "shiftl1 (w :: 'a :: len word) = word_reverse (shiftr1 (word_reverse w))" + "shiftl1 (w :: 'a :: finite word) = word_reverse (shiftr1 (word_reverse w))" apply (unfold word_reverse_def) apply (rule word_bl.Rep_inverse' [symmetric]) apply (simp add: bl_shiftl1 bl_shiftr1 word_bl.Abs_inverse) @@ -234,7 +232,7 @@ done lemma shiftl_rev: - "shiftl (w :: 'a :: len word) n = word_reverse (shiftr (word_reverse w) n)" + "shiftl (w :: 'a :: finite word) n = word_reverse (shiftr (word_reverse w) n)" apply (unfold shiftl_def shiftr_def) apply (induct "n") apply (auto simp add : shiftl1_rev) @@ -247,7 +245,7 @@ lemmas rev_shiftr = shiftl_rev [THEN word_rev_gal', standard] lemma bl_sshiftr1: - "to_bl (sshiftr1 (w :: 'a :: len word)) = hd (to_bl w) # butlast (to_bl w)" + "to_bl (sshiftr1 (w :: 'a :: finite word)) = hd (to_bl w) # butlast (to_bl w)" apply (unfold sshiftr1_def uint_bl word_size) apply (simp add: butlast_rest_bin word_ubin.eq_norm) apply (simp add: sint_uint) @@ -259,14 +257,13 @@ nth_bin_to_bl bin_nth.Suc [symmetric] nth_sbintr del: bin_nth.Suc) - apply force apply (rule impI) apply (rule_tac f = "bin_nth (uint w)" in arg_cong) apply simp done lemma drop_shiftr: - "drop n (to_bl ((w :: 'a :: len word) >> n)) = take (size w - n) (to_bl w)" + "drop n (to_bl ((w :: 'a :: finite word) >> n)) = take (size w - n) (to_bl w)" apply (unfold shiftr_def) apply (induct n) prefer 2 @@ -276,7 +273,7 @@ done lemma drop_sshiftr: - "drop n (to_bl ((w :: 'a :: len word) >>> n)) = take (size w - n) (to_bl w)" + "drop n (to_bl ((w :: 'a :: finite word) >>> n)) = take (size w - n) (to_bl w)" apply (unfold sshiftr_def) apply (induct n) prefer 2 @@ -286,7 +283,7 @@ done lemma take_shiftr [rule_format] : - "n <= size (w :: 'a :: len word) --> take n (to_bl (w >> n)) = + "n <= size (w :: 'a :: finite word) --> take n (to_bl (w >> n)) = replicate n False" apply (unfold shiftr_def) apply (induct n) @@ -298,7 +295,7 @@ done lemma take_sshiftr' [rule_format] : - "n <= size (w :: 'a :: len word) --> hd (to_bl (w >>> n)) = hd (to_bl w) & + "n <= size (w :: 'a :: finite word) --> hd (to_bl (w >>> n)) = hd (to_bl w) & take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))" apply (unfold sshiftr_def) apply (induct n) @@ -323,7 +320,7 @@ by (induct n) (auto simp: shiftl1_of_bl replicate_app_Cons_same) lemmas shiftl_bl = - shiftl_of_bl [where bl = "to_bl (?w :: ?'a :: len0 word)", simplified] + shiftl_of_bl [where bl = "to_bl (?w :: ?'a word)", simplified] lemmas shiftl_number [simp] = shiftl_def [where w="number_of ?w"] @@ -332,46 +329,46 @@ by (simp add: shiftl_bl word_rep_drop word_size min_def) lemma shiftl_zero_size: - fixes x :: "'a::len0 word" + fixes x :: "'a word" shows "size x <= n ==> x << n = 0" apply (unfold word_size) apply (rule word_eqI) apply (clarsimp simp add: shiftl_bl word_size test_bit_of_bl nth_append) done -(* note - the following results use 'a :: len word < number_ring *) +(* note - the following results use 'a :: finite word < number_ring *) -lemma shiftl1_2t: "shiftl1 (w :: 'a :: len word) = 2 * w" +lemma shiftl1_2t: "shiftl1 (w :: 'a :: finite word) = 2 * w" apply (simp add: shiftl1_def_u) apply (simp only: double_number_of_BIT [symmetric]) apply simp done -lemma shiftl1_p: "shiftl1 (w :: 'a :: len word) = w + w" +lemma shiftl1_p: "shiftl1 (w :: 'a :: finite word) = w + w" apply (simp add: shiftl1_def_u) apply (simp only: double_number_of_BIT [symmetric]) apply simp done -lemma shiftl_t2n: "shiftl (w :: 'a :: len word) n = 2 ^ n * w" +lemma shiftl_t2n: "shiftl (w :: 'a :: finite word) n = 2 ^ n * w" unfolding shiftl_def by (induct n) (auto simp: shiftl1_2t power_Suc) lemma shiftr1_bintr [simp]: - "(shiftr1 (number_of w) :: 'a :: len0 word) = - number_of (bin_rest (bintrunc (len_of TYPE ('a)) w))" + "(shiftr1 (number_of w) :: 'a word) = + number_of (bin_rest (bintrunc CARD('a) w))" unfolding shiftr1_def word_number_of_def by (simp add : word_ubin.eq_norm) lemma sshiftr1_sbintr [simp] : - "(sshiftr1 (number_of w) :: 'a :: len word) = - number_of (bin_rest (sbintrunc (len_of TYPE ('a) - 1) w))" + "(sshiftr1 (number_of w) :: 'a :: finite word) = + number_of (bin_rest (sbintrunc (CARD('a) - 1) w))" unfolding sshiftr1_def word_number_of_def by (simp add : word_sbin.eq_norm) lemma shiftr_no': "w = number_of bin ==> - (w::'a::len0 word) >> n = number_of ((bin_rest ^ n) (bintrunc (size w) bin))" + (w::'a word) >> n = number_of ((bin_rest ^ n) (bintrunc (size w) bin))" apply clarsimp apply (rule word_eqI) apply (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size) @@ -383,7 +380,7 @@ apply clarsimp apply (rule word_eqI) apply (auto simp: nth_sshiftr nth_rest_power_bin nth_sbintr word_size) - apply (subgoal_tac "na + n = len_of TYPE('a) - Suc 0", simp, simp)+ + apply (subgoal_tac "na + n = CARD('a) - Suc 0", simp, simp)+ done lemmas sshiftr_no [simp] = @@ -419,7 +416,7 @@ lemmas shiftr_bl = word_bl.Rep' [THEN eq_imp_le, THEN shiftr_bl_of, simplified word_size, simplified, THEN eq_reflection, standard] -lemma msb_shift': "msb (w::'a::len word) <-> (w >> (size w - 1)) ~= 0" +lemma msb_shift': "msb (w::'a::finite word) <-> (w >> (size w - 1)) ~= 0" apply (unfold shiftr_bl word_msb_alt) apply (simp add: word_size Suc_le_eq take_Suc) apply (cases "hd (to_bl w)") @@ -480,7 +477,7 @@ subsubsection "Mask" definition - mask :: "nat => 'a::len word" where + mask :: "nat => 'a::finite word" where "mask n == (1 << n) - 1" lemma nth_mask': "m = mask n ==> test_bit m i = (i < n & i < size m)" @@ -514,9 +511,9 @@ lemmas and_mask_wi = and_mask_no [unfolded word_number_of_def] lemma bl_and_mask: - "to_bl (w AND mask n :: 'a :: len word) = - replicate (len_of TYPE('a) - n) False @ - drop (len_of TYPE('a) - n) (to_bl w)" + "to_bl (w AND mask n :: 'a :: finite word) = + replicate (CARD('a) - n) False @ + drop (CARD('a) - n) (to_bl w)" apply (rule nth_equalityI) apply simp apply (clarsimp simp add: to_bl_nth word_size) @@ -563,14 +560,14 @@ done lemma word_2p_lem: - "n < size w ==> w < 2 ^ n = (uint (w :: 'a :: len word) < 2 ^ n)" + "n < size w ==> w < 2 ^ n = (uint (w :: 'a :: finite word) < 2 ^ n)" apply (unfold word_size word_less_alt word_number_of_alt) apply (clarsimp simp add: word_of_int_power_hom word_uint.eq_norm int_mod_eq' simp del: word_of_int_bin) done -lemma less_mask_eq: "x < 2 ^ n ==> x AND mask n = (x :: 'a :: len word)" +lemma less_mask_eq: "x < 2 ^ n ==> x AND mask n = (x :: 'a :: finite word)" apply (unfold word_less_alt word_number_of_alt) apply (clarsimp simp add: and_mask_mod_2p word_of_int_power_hom word_uint.eq_norm @@ -590,7 +587,7 @@ unfolding word_size by (erule and_mask_less') lemma word_mod_2p_is_mask': - "c = 2 ^ n ==> c > 0 ==> x mod c = (x :: 'a :: len word) AND mask n" + "c = 2 ^ n ==> c > 0 ==> x mod c = (x :: 'a :: finite word) AND mask n" by (clarsimp simp add: word_mod_def uint_2p and_mask_mod_2p) lemmas word_mod_2p_is_mask = refl [THEN word_mod_2p_is_mask'] @@ -620,8 +617,8 @@ subsubsection "Revcast" definition - revcast :: "'a :: len0 word => 'b :: len0 word" where - "revcast w == of_bl (takefill False (len_of TYPE('b)) (to_bl w))" + revcast :: "'a word => 'b word" where + "revcast w == of_bl (takefill False CARD('b) (to_bl w))" lemmas revcast_def' = revcast_def [simplified] lemmas revcast_def'' = revcast_def' [simplified word_size] @@ -629,8 +626,8 @@ revcast_def' [where w="number_of ?w", unfolded word_size] lemma to_bl_revcast: - "to_bl (revcast w :: 'a :: len0 word) = - takefill False (len_of TYPE ('a)) (to_bl w)" + "to_bl (revcast w :: 'a word) = + takefill False CARD('a) (to_bl w)" apply (unfold revcast_def' word_size) apply (rule word_bl.Abs_inverse) apply simp @@ -659,7 +656,7 @@ lemma revcast_down_uu': "rc = revcast ==> source_size rc = target_size rc + n ==> - rc (w :: 'a :: len word) = ucast (w >> n)" + rc (w :: 'a :: finite word) = ucast (w >> n)" apply (simp add: revcast_def') apply (rule word_bl.Rep_inverse') apply (rule trans, rule ucast_down_drop) @@ -670,7 +667,7 @@ lemma revcast_down_us': "rc = revcast ==> source_size rc = target_size rc + n ==> - rc (w :: 'a :: len word) = ucast (w >>> n)" + rc (w :: 'a :: finite word) = ucast (w >>> n)" apply (simp add: revcast_def') apply (rule word_bl.Rep_inverse') apply (rule trans, rule ucast_down_drop) @@ -681,7 +678,7 @@ lemma revcast_down_su': "rc = revcast ==> source_size rc = target_size rc + n ==> - rc (w :: 'a :: len word) = scast (w >> n)" + rc (w :: 'a :: finite word) = scast (w >> n)" apply (simp add: revcast_def') apply (rule word_bl.Rep_inverse') apply (rule trans, rule scast_down_drop) @@ -692,7 +689,7 @@ lemma revcast_down_ss': "rc = revcast ==> source_size rc = target_size rc + n ==> - rc (w :: 'a :: len word) = scast (w >>> n)" + rc (w :: 'a :: finite word) = scast (w >>> n)" apply (simp add: revcast_def') apply (rule word_bl.Rep_inverse') apply (rule trans, rule scast_down_drop) @@ -708,7 +705,7 @@ lemma cast_down_rev: "uc = ucast ==> source_size uc = target_size uc + n ==> - uc w = revcast ((w :: 'a :: len word) << n)" + uc w = revcast ((w :: 'a :: finite word) << n)" apply (unfold shiftl_rev) apply clarify apply (simp add: revcast_rev_ucast) @@ -720,7 +717,7 @@ lemma revcast_up': "rc = revcast ==> source_size rc + n = target_size rc ==> - rc w = (ucast w :: 'a :: len word) << n" + rc w = (ucast w :: 'a :: finite word) << n" apply (simp add: revcast_def') apply (rule word_bl.Rep_inverse') apply (simp add: takefill_alt) @@ -747,11 +744,11 @@ subsubsection "Slices" definition - slice1 :: "nat => 'a :: len0 word => 'b :: len0 word" where + slice1 :: "nat => 'a word => 'b word" where "slice1 n w == of_bl (takefill False n (to_bl w))" definition - slice :: "nat => 'a :: len0 word => 'b :: len0 word" where + slice :: "nat => 'a word => 'b word" where "slice n w == slice1 (size w - n) w" lemmas slice_def' = slice_def [unfolded word_size] @@ -788,8 +785,8 @@ done lemma nth_slice: - "(slice n w :: 'a :: len0 word) !! m = - (w !! (m + n) & m < len_of TYPE ('a))" + "(slice n w :: 'a word) !! m = + (w !! (m + n) & m < CARD('a))" unfolding slice_shiftr by (simp add : nth_ucast nth_shiftr) @@ -805,8 +802,8 @@ apply (unfold slice1_def word_size of_bl_def uint_bl) apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop takefill_append [symmetric]) - apply (rule_tac f = "%k. takefill False (len_of TYPE('a)) - (replicate k False @ bin_to_bl (len_of TYPE('b)) (uint w))" in arg_cong) + apply (rule_tac f = "%k. takefill False CARD('a) + (replicate k False @ bin_to_bl CARD('b) (uint w))" in arg_cong) apply arith done @@ -833,17 +830,17 @@ lemmas revcast_slice1 = refl [THEN revcast_slice1'] lemma slice1_tf_tf': - "to_bl (slice1 n w :: 'a :: len0 word) = - rev (takefill False (len_of TYPE('a)) (rev (takefill False n (to_bl w))))" + "to_bl (slice1 n w :: 'a word) = + rev (takefill False CARD('a) (rev (takefill False n (to_bl w))))" unfolding slice1_def by (rule word_rev_tf) lemmas slice1_tf_tf = slice1_tf_tf' [THEN word_bl.Rep_inverse', symmetric, standard] lemma rev_slice1: - "n + k = len_of TYPE('a) + len_of TYPE('b) \ - slice1 n (word_reverse w :: 'b :: len0 word) = - word_reverse (slice1 k w :: 'a :: len0 word)" + "n + k = CARD('a) + CARD('b) \ + slice1 n (word_reverse w :: 'b word) = + word_reverse (slice1 k w :: 'a word)" apply (unfold word_reverse_def slice1_tf_tf) apply (rule word_bl.Rep_inverse') apply (rule rev_swap [THEN iffD1]) @@ -871,10 +868,10 @@ criterion for overflow of addition of signed integers *} lemma sofl_test: - "(sint (x :: 'a :: len word) + sint y = sint (x + y)) = + "(sint (x :: 'a :: finite word) + sint y = sint (x + y)) = ((((x+y) XOR x) AND ((x+y) XOR y)) >> (size x - 1) = 0)" apply (unfold word_size) - apply (cases "len_of TYPE('a)", simp) + apply (cases "CARD('a)", simp) apply (subst msb_shift [THEN sym_notr]) apply (simp add: word_ops_msb) apply (simp add: word_msb_sint) @@ -902,29 +899,29 @@ subsection "Split and cat" constdefs - word_cat :: "'a :: len0 word => 'b :: len0 word => 'c :: len0 word" - "word_cat a b == word_of_int (bin_cat (uint a) (len_of TYPE ('b)) (uint b))" + word_cat :: "'a word => 'b word => 'c word" + "word_cat a b == word_of_int (bin_cat (uint a) CARD('b) (uint b))" - word_split :: "'a :: len0 word => ('b :: len0 word) * ('c :: len0 word)" + word_split :: "'a word => ('b word) * ('c word)" "word_split a == - case bin_split (len_of TYPE ('c)) (uint a) of + case bin_split CARD('c) (uint a) of (u, v) => (word_of_int u, word_of_int v)" - word_rcat :: "'a :: len0 word list => 'b :: len0 word" + word_rcat :: "'a word list => 'b word" "word_rcat ws == - word_of_int (bin_rcat (len_of TYPE ('a)) (map uint ws))" + word_of_int (bin_rcat CARD('a) (map uint ws))" - word_rsplit :: "'a :: len0 word => 'b :: len word list" + word_rsplit :: "'a word => 'b :: finite word list" "word_rsplit w == - map word_of_int (bin_rsplit (len_of TYPE ('b)) (len_of TYPE ('a), uint w))" + map word_of_int (bin_rsplit CARD('b) (CARD('a), uint w))" lemmas word_split_bin' = word_split_def [THEN meta_eq_to_obj_eq, standard] lemmas word_cat_bin' = word_cat_def [THEN meta_eq_to_obj_eq, standard] lemma word_rsplit_no: - "(word_rsplit (number_of bin :: 'b :: len0 word) :: 'a word list) = - map number_of (bin_rsplit (len_of TYPE('a :: len)) - (len_of TYPE('b), bintrunc (len_of TYPE('b)) bin))" + "(word_rsplit (number_of bin :: 'b word) :: 'a word list) = + map number_of (bin_rsplit CARD('a :: finite) + (CARD('b), bintrunc CARD('b) bin))" apply (unfold word_rsplit_def word_no_wi) apply (simp add: word_ubin.eq_norm) done @@ -946,7 +943,7 @@ done lemma of_bl_append: - "(of_bl (xs @ ys) :: 'a :: len word) = of_bl xs * 2^(length ys) + of_bl ys" + "(of_bl (xs @ ys) :: 'a :: finite word) = of_bl xs * 2^(length ys) + of_bl ys" apply (unfold of_bl_def) apply (simp add: bl_to_bin_app_cat bin_cat_num) apply (simp add: word_of_int_power_hom [symmetric] new_word_of_int_hom_syms) @@ -958,7 +955,7 @@ (auto simp add: test_bit_of_bl nth_append) lemma of_bl_True: - "(of_bl (True#xs)::'a::len word) = 2^length xs + of_bl xs" + "(of_bl (True#xs)::'a::finite word) = 2^length xs + of_bl xs" by (subst of_bl_append [where xs="[True]", simplified]) (simp add: word_1_bl) @@ -966,8 +963,8 @@ "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs" by (cases x) (simp_all add: of_bl_True) -lemma split_uint_lem: "bin_split n (uint (w :: 'a :: len0 word)) = (a, b) ==> - a = bintrunc (len_of TYPE('a) - n) a & b = bintrunc (len_of TYPE('a)) b" +lemma split_uint_lem: "bin_split n (uint (w :: 'a word)) = (a, b) ==> + a = bintrunc (CARD('a) - n) a & b = bintrunc CARD('a) b" apply (frule word_ubin.norm_Rep [THEN ssubst]) apply (drule bin_split_trunc1) apply (drule sym [THEN trans]) @@ -989,7 +986,7 @@ apply (clarsimp split: prod.splits) apply (frule split_uint_lem [THEN conjunct1]) apply (unfold word_size) - apply (cases "len_of TYPE('a) >= len_of TYPE('b)") + apply (cases "CARD('a) >= CARD('b)") defer apply (simp add: word_0_bl word_0_wi_Pls) apply (simp add : of_bl_def to_bl_def) @@ -1015,9 +1012,9 @@ done lemma word_split_bl_eq: - "(word_split (c::'a::len word) :: ('c :: len0 word * 'd :: len0 word)) = - (of_bl (take (len_of TYPE('a::len) - len_of TYPE('d::len0)) (to_bl c)), - of_bl (drop (len_of TYPE('a) - len_of TYPE('d)) (to_bl c)))" + "(word_split (c::'a::finite word) :: ('c word * 'd word)) = + (of_bl (take (CARD('a::finite) - CARD('d)) (to_bl c)), + of_bl (drop (CARD('a) - CARD('d)) (to_bl c)))" apply (rule word_split_bl [THEN iffD1]) apply (unfold word_size) apply (rule refl conjI)+ @@ -1060,14 +1057,13 @@ -- "limited hom result" lemma word_cat_hom: - "len_of TYPE('a::len0) <= len_of TYPE('b::len0) + len_of TYPE ('c::len0) + "CARD('a) <= CARD('b) + CARD('c) ==> (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) = word_of_int (bin_cat w (size b) (uint b))" apply (unfold word_cat_def word_size) apply (clarsimp simp add : word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm bintr_cat min_def) - apply arith done lemma word_cat_split_alt: @@ -1142,7 +1138,7 @@ by (simp add: bin_rsplit_aux_simp_alt Let_def split: split_split) lemma test_bit_rsplit: - "sw = word_rsplit w ==> m < size (hd sw :: 'a :: len word) ==> + "sw = word_rsplit w ==> m < size (hd sw :: 'a :: finite word) ==> k < length sw ==> (rev sw ! k) !! m = (w !! (k * size (hd sw) + m))" apply (unfold word_rsplit_def word_test_bit_def) apply (rule trans) @@ -1157,7 +1153,7 @@ apply (rule map_ident [THEN fun_cong]) apply (rule refl [THEN map_cong]) apply (simp add : word_ubin.eq_norm) - apply (erule bin_rsplit_size_sign [OF len_gt_0 refl]) + apply (erule bin_rsplit_size_sign [OF zero_less_card_finite refl]) done lemma word_rcat_bl: "word_rcat wl == of_bl (concat (map to_bl wl))" @@ -1170,10 +1166,10 @@ lemmas size_rcat_lem = size_rcat_lem' [unfolded word_size] -lemmas td_gal_lt_len = len_gt_0 [THEN td_gal_lt, standard] +lemmas td_gal_lt_len = zero_less_card_finite [THEN td_gal_lt, standard] lemma nth_rcat_lem' [rule_format] : - "sw = size (hd wl :: 'a :: len word) ==> (ALL n. n < size wl * sw --> + "sw = size (hd wl :: 'a :: finite word) ==> (ALL n. n < size wl * sw --> rev (concat (map to_bl wl)) ! n = rev (to_bl (rev wl ! (n div sw))) ! (n mod sw))" apply (unfold word_size) @@ -1188,7 +1184,7 @@ lemmas nth_rcat_lem = refl [THEN nth_rcat_lem', unfolded word_size] lemma test_bit_rcat: - "sw = size (hd wl :: 'a :: len word) ==> rc = word_rcat wl ==> rc !! n = + "sw = size (hd wl :: 'a :: finite word) ==> rc = word_rcat wl ==> rc !! n = (n < size rc & n div sw < size wl & (rev wl) ! (n div sw) !! (n mod sw))" apply (unfold word_rcat_bl word_size) apply (clarsimp simp add : @@ -1219,7 +1215,7 @@ lemmas word_rsplit_len_indep = word_rsplit_len_indep' [OF refl refl refl refl] lemma length_word_rsplit_size: - "n = len_of TYPE ('a :: len) ==> + "n = CARD('a :: finite) ==> (length (word_rsplit w :: 'a word list) <= m) = (size w <= m * n)" apply (unfold word_rsplit_def word_size) apply (clarsimp simp add : bin_rsplit_len_le) @@ -1229,12 +1225,12 @@ length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]] lemma length_word_rsplit_exp_size: - "n = len_of TYPE ('a :: len) ==> + "n = CARD('a :: finite) ==> length (word_rsplit w :: 'a word list) = (size w + n - 1) div n" unfolding word_rsplit_def by (clarsimp simp add : word_size bin_rsplit_len) lemma length_word_rsplit_even_size: - "n = len_of TYPE ('a :: len) ==> size w = m * n ==> + "n = CARD('a :: finite) ==> size w = m * n ==> length (word_rsplit w :: 'a word list) = m" by (clarsimp simp add : length_word_rsplit_exp_size given_quot_alt) @@ -1251,15 +1247,15 @@ apply (simp_all add: word_size refl [THEN length_word_rsplit_size [simplified le_def, simplified]]) apply safe - apply (erule xtr7, rule len_gt_0 [THEN dtle])+ + apply (erule xtr7, rule zero_less_card_finite [THEN dtle])+ done lemma size_word_rsplit_rcat_size': - "word_rcat (ws :: 'a :: len word list) = frcw ==> - size frcw = length ws * len_of TYPE ('a) ==> + "word_rcat (ws :: 'a :: finite word list) = frcw ==> + size frcw = length ws * CARD('a) ==> size (hd [word_rsplit frcw, ws]) = size ws" apply (clarsimp simp add : word_size length_word_rsplit_exp_size') - apply (fast intro: given_quot_alt) + apply (fast intro: given_quot_alt zero_less_card_finite) done lemmas size_word_rsplit_rcat_size = @@ -1272,8 +1268,8 @@ by (auto simp: add_commute) lemma word_rsplit_rcat_size': - "word_rcat (ws :: 'a :: len word list) = frcw ==> - size frcw = length ws * len_of TYPE ('a) ==> word_rsplit frcw = ws" + "word_rcat (ws :: 'a :: finite word list) = frcw ==> + size frcw = length ws * CARD('a) ==> word_rsplit frcw = ws" apply (frule size_word_rsplit_rcat_size, assumption) apply (clarsimp simp add : word_size) apply (rule nth_equalityI, assumption) @@ -1308,13 +1304,13 @@ rotater :: "nat => 'a list => 'a list" "rotater n == rotater1 ^ n" - word_rotr :: "nat => 'a :: len0 word => 'a :: len0 word" + word_rotr :: "nat => 'a word => 'a word" "word_rotr n w == of_bl (rotater n (to_bl w))" - word_rotl :: "nat => 'a :: len0 word => 'a :: len0 word" + word_rotl :: "nat => 'a word => 'a word" "word_rotl n w == of_bl (rotate n (to_bl w))" - word_roti :: "int => 'a :: len0 word => 'a :: len0 word" + word_roti :: "int => 'a word => 'a word" "word_roti i w == if i >= 0 then word_rotr (nat i) w else word_rotl (nat (- i)) w" @@ -1632,7 +1628,7 @@ simplified word_bl.Rep', standard] lemma bl_word_roti_dt': - "n = nat ((- i) mod int (size (w :: 'a :: len word))) ==> + "n = nat ((- i) mod int (size (w :: 'a :: finite word))) ==> to_bl (word_roti i w) = drop n (to_bl w) @ take n (to_bl w)" apply (unfold word_roti_def) apply (simp add: bl_word_rotl_dt bl_word_rotr_dt word_size)