diff --git a/thys/Native_Word/Code_Symbolic_Bits_Int.thy b/thys/Native_Word/Code_Symbolic_Bits_Int.thy --- a/thys/Native_Word/Code_Symbolic_Bits_Int.thy +++ b/thys/Native_Word/Code_Symbolic_Bits_Int.thy @@ -1,124 +1,120 @@ (* Title: Code_Symbolic_Bits_Int.thy Author: Andreas Lochbihler, ETH Zurich *) chapter \Symbolic implementation of bit operations on int\ theory Code_Symbolic_Bits_Int imports "HOL-Word.Misc_set_bit" "HOL-Word.Misc_lsb" More_Bits_Int begin section \Implementations of bit operations on \<^typ>\int\ operating on symbolic representation\ -lemma not_minus_numeral_inc_eq: - \NOT (- numeral (Num.inc n)) = (numeral n :: int)\ - by (simp add: not_int_def sub_inc_One_eq) - lemma test_bit_int_code [code]: "bit (0::int) n = False" "bit (Int.Neg num.One) n = True" "bit (Int.Pos num.One) 0 = True" "bit (Int.Pos (num.Bit0 m)) 0 = False" "bit (Int.Pos (num.Bit1 m)) 0 = True" "bit (Int.Neg (num.Bit0 m)) 0 = False" "bit (Int.Neg (num.Bit1 m)) 0 = True" "bit (Int.Pos num.One) (Suc n) = False" "bit (Int.Pos (num.Bit0 m)) (Suc n) = bit (Int.Pos m) n" "bit (Int.Pos (num.Bit1 m)) (Suc n) = bit (Int.Pos m) n" "bit (Int.Neg (num.Bit0 m)) (Suc n) = bit (Int.Neg m) n" "bit (Int.Neg (num.Bit1 m)) (Suc n) = bit (Int.Neg (Num.inc m)) n" by (simp_all add: Num.add_One bit_Suc) lemma int_not_code [code]: "NOT (0 :: int) = -1" "NOT (Int.Pos n) = Int.Neg (Num.inc n)" "NOT (Int.Neg n) = Num.sub n num.One" by(simp_all add: Num.add_One int_not_def) lemma int_and_code [code]: fixes i j :: int shows "0 AND j = 0" "i AND 0 = 0" "Int.Pos n AND Int.Pos m = (case bitAND_num n m of None \ 0 | Some n' \ Int.Pos n')" "Int.Neg n AND Int.Neg m = NOT (Num.sub n num.One OR Num.sub m num.One)" "Int.Pos n AND Int.Neg num.One = Int.Pos n" "Int.Pos n AND Int.Neg (num.Bit0 m) = Num.sub (bitORN_num (Num.BitM m) n) num.One" "Int.Pos n AND Int.Neg (num.Bit1 m) = Num.sub (bitORN_num (num.Bit0 m) n) num.One" "Int.Neg num.One AND Int.Pos m = Int.Pos m" "Int.Neg (num.Bit0 n) AND Int.Pos m = Num.sub (bitORN_num (Num.BitM n) m) num.One" "Int.Neg (num.Bit1 n) AND Int.Pos m = Num.sub (bitORN_num (num.Bit0 n) m) num.One" apply (simp_all add: int_numeral_bitAND_num Num.add_One sub_inc_One_eq inc_BitM_eq not_minus_numeral_inc_eq flip: int_not_neg_numeral int_or_not_bitORN_num split: option.split) apply (simp_all add: ac_simps) done lemma int_or_code [code]: fixes i j :: int shows "0 OR j = j" "i OR 0 = i" "Int.Pos n OR Int.Pos m = Int.Pos (bitOR_num n m)" "Int.Neg n OR Int.Neg m = NOT (Num.sub n num.One AND Num.sub m num.One)" "Int.Pos n OR Int.Neg num.One = Int.Neg num.One" "Int.Pos n OR Int.Neg (num.Bit0 m) = (case bitANDN_num (Num.BitM m) n of None \ -1 | Some n' \ Int.Neg (Num.inc n'))" "Int.Pos n OR Int.Neg (num.Bit1 m) = (case bitANDN_num (num.Bit0 m) n of None \ -1 | Some n' \ Int.Neg (Num.inc n'))" "Int.Neg num.One OR Int.Pos m = Int.Neg num.One" "Int.Neg (num.Bit0 n) OR Int.Pos m = (case bitANDN_num (Num.BitM n) m of None \ -1 | Some n' \ Int.Neg (Num.inc n'))" "Int.Neg (num.Bit1 n) OR Int.Pos m = (case bitANDN_num (num.Bit0 n) m of None \ -1 | Some n' \ Int.Neg (Num.inc n'))" apply (simp_all add: int_numeral_bitOR_num flip: int_not_neg_numeral) apply (simp_all add: or_int_def int_and_comm int_not_and_bitANDN_num del: int_not_simps(4) split: option.split) apply (simp_all add: Num.add_One) done lemma int_xor_code [code]: fixes i j :: int shows "0 XOR j = j" "i XOR 0 = i" "Int.Pos n XOR Int.Pos m = (case bitXOR_num n m of None \ 0 | Some n' \ Int.Pos n')" "Int.Neg n XOR Int.Neg m = Num.sub n num.One XOR Num.sub m num.One" "Int.Neg n XOR Int.Pos m = NOT (Num.sub n num.One XOR Int.Pos m)" "Int.Pos n XOR Int.Neg m = NOT (Int.Pos n XOR Num.sub m num.One)" by(fold int_not_neg_numeral)(simp_all add: int_numeral_bitXOR_num int_xor_not cong: option.case_cong) lemma bin_rest_code: "bin_rest i = i >> 1" by (simp add: shiftr_int_def) lemma set_bits_code [code]: "set_bits = Code.abort (STR ''set_bits is unsupported on type int'') (\_. set_bits :: _ \ int)" by simp lemma fixes i :: int shows int_set_bit_True_conv_OR [code]: "set_bit i n True = i OR (1 << n)" and int_set_bit_False_conv_NAND [code]: "set_bit i n False = i AND NOT (1 << n)" and int_set_bit_conv_ops: "set_bit i n b = (if b then i OR (1 << n) else i AND NOT (1 << n))" by(simp_all add: set_bit_int_def bin_set_conv_OR bin_clr_conv_NAND) declare [[code drop: \drop_bit :: nat \ int \ int\]] lemma drop_bit_int_code [code]: fixes i :: int shows "drop_bit 0 i = i" "drop_bit (Suc n) 0 = (0 :: int)" "drop_bit (Suc n) (Int.Pos num.One) = 0" "drop_bit (Suc n) (Int.Pos (num.Bit0 m)) = drop_bit n (Int.Pos m)" "drop_bit (Suc n) (Int.Pos (num.Bit1 m)) = drop_bit n (Int.Pos m)" "drop_bit (Suc n) (Int.Neg num.One) = - 1" "drop_bit (Suc n) (Int.Neg (num.Bit0 m)) = drop_bit n (Int.Neg m)" "drop_bit (Suc n) (Int.Neg (num.Bit1 m)) = drop_bit n (Int.Neg (Num.inc m))" by (simp_all add: shiftr_eq_drop_bit drop_bit_Suc add_One) declare [[code drop: \push_bit :: nat \ int \ int\]] lemma push_bit_int_code [code]: "push_bit 0 i = i" "push_bit (Suc n) i = push_bit n (Int.dup i)" by (simp_all add: ac_simps) lemma int_lsb_code [code]: "lsb (0 :: int) = False" "lsb (Int.Pos num.One) = True" "lsb (Int.Pos (num.Bit0 w)) = False" "lsb (Int.Pos (num.Bit1 w)) = True" "lsb (Int.Neg num.One) = True" "lsb (Int.Neg (num.Bit0 w)) = False" "lsb (Int.Neg (num.Bit1 w)) = True" by simp_all end diff --git a/thys/Native_Word/Code_Target_Word_Base.thy b/thys/Native_Word/Code_Target_Word_Base.thy --- a/thys/Native_Word/Code_Target_Word_Base.thy +++ b/thys/Native_Word/Code_Target_Word_Base.thy @@ -1,440 +1,422 @@ (* Title: Code_Target_Word_Base.thy Author: Andreas Lochbihler, ETH Zurich *) chapter \Common base for target language implementations of word types\ theory Code_Target_Word_Base imports "HOL-Word.Word" "Word_Lib.Word_Lib" Bits_Integer begin -(* TODO: Move to Word ? *) -lemma dflt_size_word_pow_ne_zero [simp]: - "(2 :: 'a word) ^ (LENGTH('a::len) - Suc 0) \ 0" - by simp - -lemma push_bit_word_beyond [simp]: - \push_bit n w = 0\ if \LENGTH('a) \ n\ for w :: \'a::len word\ - using that by (transfer fixing: n) (simp add: take_bit_push_bit) - -lemma drop_bit_word_beyond [simp]: - \drop_bit n w = 0\ if \LENGTH('a) \ n\ for w :: \'a::len word\ - using that by (transfer fixing: n) (simp add: drop_bit_take_bit) - -lemma signed_drop_bit_beyond: - \signed_drop_bit n w = (if bit w (LENGTH('a) - Suc 0) then - 1 else 0)\ - if \LENGTH('a) \ n\ for w :: \'a::len word\ - by (rule bit_word_eqI) (simp add: bit_signed_drop_bit_iff that) - text \More lemmas\ lemma nat_div_eq_Suc_0_iff: "n div m = Suc 0 \ m \ n \ n < 2 * m" apply auto using div_greater_zero_iff apply fastforce apply (metis One_nat_def div_greater_zero_iff dividend_less_div_times mult.right_neutral mult_Suc mult_numeral_1 numeral_2_eq_2 zero_less_numeral) apply (simp add: div_nat_eqI) done lemma Suc_0_lt_2p_len_of: "Suc 0 < 2 ^ LENGTH('a :: len)" by (metis One_nat_def len_gt_0 lessI numeral_2_eq_2 one_less_power) lemma div_half_nat: fixes x y :: nat assumes "y \ 0" shows "(x div y, x mod y) = (let q = 2 * (x div 2 div y); r = x - q * y in if y \ r then (q + 1, r - y) else (q, r))" proof - let ?q = "2 * (x div 2 div y)" have q: "?q = x div y - x div y mod 2" by(metis div_mult2_eq mult.commute minus_mod_eq_mult_div [symmetric]) let ?r = "x - ?q * y" have r: "?r = x mod y + x div y mod 2 * y" by(simp add: q diff_mult_distrib minus_mod_eq_div_mult [symmetric])(metis diff_diff_cancel mod_less_eq_dividend mod_mult2_eq add.commute mult.commute) show ?thesis proof(cases "y \ x - ?q * y") case True with assms q have "x div y mod 2 \ 0" unfolding r by (metis Nat.add_0_right diff_0_eq_0 diff_Suc_1 le_div_geq mod2_gr_0 mod_div_trivial mult_0 neq0_conv numeral_1_eq_Suc_0 numerals(1)) hence "x div y = ?q + 1" unfolding q by simp moreover hence "x mod y = ?r - y" by simp(metis minus_div_mult_eq_mod [symmetric] diff_commute diff_diff_left mult_Suc) ultimately show ?thesis using True by(simp add: Let_def) next case False hence "x div y mod 2 = 0" unfolding r by(simp add: not_le)(metis Nat.add_0_right assms div_less div_mult_self2 mod_div_trivial mult.commute) hence "x div y = ?q" unfolding q by simp moreover hence "x mod y = ?r" by (metis minus_div_mult_eq_mod [symmetric]) ultimately show ?thesis using False by(simp add: Let_def) qed qed lemma unat_p2: "n < LENGTH('a :: len) \ unat (2 ^ n :: 'a word) = 2 ^ n" proof(induct n) case 0 thus ?case by simp next case (Suc n) then obtain n' where "LENGTH('a) = Suc n'" by(cases "LENGTH('a)") simp_all with Suc show ?case by (simp add: unat_word_ariths bintrunc_mod2p) qed lemma word_div_lt_eq_0: "x < y \ x div y = 0" for x :: "'a :: len word" by (simp add: word_eq_iff word_less_def word_test_bit_def uint_div) lemma word_div_eq_1_iff: "n div m = 1 \ n \ m \ unat n < 2 * unat (m :: 'a :: len word)" apply(simp only: word_arith_nat_defs word_le_nat_alt nat_div_eq_Suc_0_iff[symmetric]) apply(rule word_unat.Abs_inject) apply(simp only: unat_div[symmetric] word_unat.Rep) apply(simp add: unats_def Suc_0_lt_2p_len_of) done lemma div_half_word: fixes x y :: "'a :: len word" assumes "y \ 0" shows "(x div y, x mod y) = (let q = (x >> 1) div y << 1; r = x - q * y in if y \ r then (q + 1, r - y) else (q, r))" proof - obtain n where n: "x = of_nat n" "n < 2 ^ LENGTH('a)" by (rule that [of \unat x\]) simp_all moreover obtain m where m: "y = of_nat m" "m < 2 ^ LENGTH('a)" by (rule that [of \unat y\]) simp_all ultimately have [simp]: \unat (of_nat n :: 'a word) = n\ \unat (of_nat m :: 'a word) = m\ by (transfer, simp add: take_bit_of_nat take_bit_nat_eq_self_iff)+ let ?q = "(x >> 1) div y << 1" let ?q' = "2 * (n div 2 div m)" have "n div 2 div m < 2 ^ LENGTH('a)" using n by (metis of_nat_inverse unat_lt2p uno_simps(2)) hence q: "?q = of_nat ?q'" using n m by (auto simp add: shiftr_word_eq drop_bit_eq_div shiftl_t2n word_arith_nat_div uno_simps take_bit_nat_eq_self) from assms have "m \ 0" using m by -(rule notI, simp) from n have "2 * (n div 2 div m) < 2 ^ LENGTH('a)" by(metis mult.commute div_mult2_eq minus_mod_eq_mult_div [symmetric] less_imp_diff_less of_nat_inverse unat_lt2p uno_simps(2)) moreover have "2 * (n div 2 div m) * m < 2 ^ LENGTH('a)" using n unfolding div_mult2_eq[symmetric] by(subst (2) mult.commute)(simp add: minus_mod_eq_div_mult [symmetric] diff_mult_distrib minus_mod_eq_mult_div [symmetric] div_mult2_eq) moreover have "2 * (n div 2 div m) * m \ n" by (metis div_mult2_eq dtle mult.assoc mult.left_commute) ultimately have r: "x - ?q * y = of_nat (n - ?q' * m)" and "y \ x - ?q * y \ of_nat (n - ?q' * m) - y = of_nat (n - ?q' * m - m)" using n m unfolding q apply (simp_all add: of_nat_diff) apply (subst of_nat_diff) apply (simp_all add: word_le_nat_alt take_bit_nat_eq_self unat_sub_if' unat_word_ariths) apply (cases \2 \ LENGTH('a)\) apply (simp_all add: unat_word_ariths take_bit_nat_eq_self) done then show ?thesis using n m div_half_nat [OF \m \ 0\, of n] unfolding q by (simp add: word_le_nat_alt word_div_def word_mod_def Let_def take_bit_nat_eq_self flip: zdiv_int zmod_int split del: if_split split: if_split_asm) qed lemma word_test_bit_set_bits: "(BITS n. f n :: 'a :: len word) !! n \ n < LENGTH('a) \ f n" by (simp add: test_bit_eq_bit bit_set_bits_word_iff) lemma word_of_int_conv_set_bits: "word_of_int i = (BITS n. i !! n)" by (rule word_eqI) (auto simp add: word_test_bit_set_bits test_bit.eq_norm) lemma word_and_mask_or_conv_and_mask: "n !! index \ (n AND mask index) OR (1 << index) = n AND mask (index + 1)" for n :: \'a::len word\ by(rule word_eqI)(auto simp add: word_ao_nth word_size nth_shiftl simp del: shiftl_1) lemma uint_and_mask_or_full: fixes n :: "'a :: len word" assumes "n !! (LENGTH('a) - 1)" and "mask1 = mask (LENGTH('a) - 1)" and "mask2 = 1 << LENGTH('a) - 1" shows "uint (n AND mask1) OR mask2 = uint n" proof - have "mask2 = uint (1 << LENGTH('a) - 1 :: 'a word)" using assms by (simp add: uint_shiftl word_size bintrunc_shiftl del: shiftl_1) hence "uint (n AND mask1) OR mask2 = uint (n AND mask1 OR (1 << LENGTH('a) - 1 :: 'a word))" by(simp add: uint_or) also have "\ = uint (n AND mask (LENGTH('a) - 1 + 1))" using assms by(simp only: word_and_mask_or_conv_and_mask) also have "\ = uint n" by simp finally show ?thesis . qed text \Division on @{typ "'a word"} is unsigned, but Scala and OCaml only have signed division and modulus.\ lemmas word_sdiv_def = sdiv_word_def lemmas word_smod_def = smod_word_def lemma [code]: "x sdiv y = (let x' = sint x; y' = sint y; negative = (x' < 0) \ (y' < 0); result = abs x' div abs y' in word_of_int (if negative then -result else result))" for x y :: \'a::len word\ by (simp add: sdiv_word_def signed_divide_int_def sgn_if Let_def not_less not_le) lemma [code]: "x smod y = (let x' = sint x; y' = sint y; negative = (x' < 0); result = abs x' mod abs y' in word_of_int (if negative then -result else result))" for x y :: \'a::len word\ proof - have *: \k mod l = k - k div l * l\ for k l :: int by (simp add: minus_div_mult_eq_mod) show ?thesis by (simp add: smod_word_def signed_modulo_int_def signed_divide_int_def * sgn_if) (simp add: signed_eq_0_iff) qed text \ This algorithm implements unsigned division in terms of signed division. Taken from Hacker's Delight. \ lemma divmod_via_sdivmod: fixes x y :: "'a :: len word" assumes "y \ 0" shows "(x div y, x mod y) = (if 1 << (LENGTH('a) - 1) \ y then if x < y then (0, x) else (1, x - y) else let q = ((x >> 1) sdiv y) << 1; r = x - q * y in if r \ y then (q + 1, r - y) else (q, r))" proof(cases "1 << (LENGTH('a) - 1) \ y") case True note y = this show ?thesis proof(cases "x < y") case True then have "x mod y = x" by (cases x, cases y) (simp add: word_less_def word_mod_def) thus ?thesis using True y by(simp add: word_div_lt_eq_0) next case False obtain n where n: "y = of_nat n" "n < 2 ^ LENGTH('a)" by (rule that [of \unat y\]) simp_all have "unat x < 2 ^ LENGTH('a)" by(rule unat_lt2p) also have "\ = 2 * 2 ^ (LENGTH('a) - 1)" by(metis Suc_pred len_gt_0 power_Suc One_nat_def) also have "\ \ 2 * n" using y n by transfer (simp add: push_bit_of_1 take_bit_eq_mod) finally have div: "x div of_nat n = 1" using False n by (simp add: word_div_eq_1_iff take_bit_nat_eq_self) moreover have "x mod y = x - x div y * y" by (simp add: minus_div_mult_eq_mod) with div n have "x mod y = x - y" by simp ultimately show ?thesis using False y n by simp qed next case False note y = this obtain n where n: "x = of_nat n" "n < 2 ^ LENGTH('a)" by (rule that [of \unat x\]) simp_all hence "int n div 2 + 2 ^ (LENGTH('a) - Suc 0) < 2 ^ LENGTH('a)" by (cases "LENGTH('a)") (simp_all, simp only: of_nat_numeral [where ?'a = int, symmetric] zdiv_int [symmetric] of_nat_power [symmetric]) with y n have "sint (x >> 1) = uint (x >> 1)" by (simp add: sint_uint sbintrunc_mod2p shiftr_div_2n take_bit_nat_eq_self) moreover have "uint y + 2 ^ (LENGTH('a) - Suc 0) < 2 ^ LENGTH('a)" using y by (cases "LENGTH('a)") (simp_all add: not_le word_2p_lem word_size) then have "sint y = uint y" by (simp add: sint_uint sbintrunc_mod2p) ultimately show ?thesis using y apply (subst div_half_word [OF assms]) apply (simp add: sdiv_word_def signed_divide_int_def flip: uint_div) done qed text \More implementations tailored towards target-language implementations\ context includes integer.lifting begin lift_definition word_of_integer :: "integer \ 'a :: len word" is word_of_int . lemma word_of_integer_code [code]: "word_of_integer n = word_of_int (int_of_integer n)" by(simp add: word_of_integer.rep_eq) end lemma word_of_int_code: "uint (word_of_int x :: 'a word) = x AND mask (LENGTH('a :: len))" by (simp add: take_bit_eq_mask) context fixes f :: "nat \ bool" begin definition set_bits_aux :: \'a word \ nat \ 'a :: len word\ where \set_bits_aux w n = push_bit n w OR take_bit n (set_bits f)\ lemma set_bits_aux_conv: \set_bits_aux w n = (w << n) OR (set_bits f AND mask n)\ for w :: \'a::len word\ by (rule bit_word_eqI) (auto simp add: set_bits_aux_def shiftl_word_eq bit_and_iff bit_or_iff bit_push_bit_iff bit_take_bit_iff bit_mask_iff bit_set_bits_word_iff) corollary set_bits_conv_set_bits_aux: \set_bits f = (set_bits_aux 0 (LENGTH('a)) :: 'a :: len word)\ by (simp add: set_bits_aux_conv) lemma set_bits_aux_0 [simp]: \set_bits_aux w 0 = w\ by (simp add: set_bits_aux_conv) lemma set_bits_aux_Suc [simp]: \set_bits_aux w (Suc n) = set_bits_aux ((w << 1) OR (if f n then 1 else 0)) n\ by (simp add: set_bits_aux_def shiftl_word_eq bit_eq_iff bit_or_iff bit_push_bit_iff bit_take_bit_iff bit_set_bits_word_iff) (auto simp add: bit_exp_iff not_less bit_1_iff less_Suc_eq_le) lemma set_bits_aux_simps [code]: \set_bits_aux w 0 = w\ \set_bits_aux w (Suc n) = set_bits_aux ((w << 1) OR (if f n then 1 else 0)) n\ by simp_all end lemma word_of_int_via_signed: fixes mask assumes mask_def: "mask = Bit_Operations.mask (LENGTH('a))" and shift_def: "shift = 1 << LENGTH('a)" and index_def: "index = LENGTH('a) - 1" and overflow_def:"overflow = 1 << (LENGTH('a) - 1)" and least_def: "least = - overflow" shows "(word_of_int i :: 'a :: len word) = (let i' = i AND mask in if i' !! index then if i' - shift < least \ overflow \ i' - shift then arbitrary1 i' else word_of_int (i' - shift) else if i' < least \ overflow \ i' then arbitrary2 i' else word_of_int i')" proof - define i' where "i' = i AND mask" have "shift = mask + 1" unfolding assms by(simp add: bin_mask_p1_conv_shift) hence "i' < shift" by(simp add: mask_def i'_def int_and_le) show ?thesis proof(cases "i' !! index") case True then have unf: "i' = overflow OR i'" apply (simp add: assms i'_def shiftl_eq_push_bit push_bit_of_1 flip: take_bit_eq_mask) apply (rule bit_eqI) apply (auto simp add: bit_take_bit_iff bit_or_iff bit_exp_iff) done have "overflow \ i'" by(subst unf)(rule le_int_or, simp add: bin_sign_and assms i'_def) hence "i' - shift < least \ False" unfolding assms by(cases "LENGTH('a)")(simp_all add: not_less) moreover have "overflow \ i' - shift \ False" using \i' < shift\ unfolding assms by(cases "LENGTH('a)")(auto simp add: not_le elim: less_le_trans) moreover have "word_of_int (i' - shift) = (word_of_int i :: 'a word)" using \i' < shift\ by (simp add: i'_def shift_def mask_def shiftl_eq_push_bit push_bit_of_1 flip: take_bit_eq_mask) ultimately show ?thesis using True by(simp add: Let_def i'_def) next case False hence "i' = i AND Bit_Operations.mask (LENGTH('a) - 1)" unfolding assms i'_def by(clarsimp simp add: i'_def bin_nth_ops intro!: bin_eqI)(cases "LENGTH('a)", auto simp add: less_Suc_eq) also have "\ \ Bit_Operations.mask (LENGTH('a) - 1)" by(rule int_and_le) simp also have "\ < overflow" unfolding overflow_def by(simp add: bin_mask_p1_conv_shift[symmetric]) also have "least \ 0" unfolding least_def overflow_def by simp have "0 \ i'" by (simp add: i'_def mask_def) hence "least \ i'" using \least \ 0\ by simp moreover have "word_of_int i' = (word_of_int i :: 'a word)" by(rule word_eqI)(auto simp add: i'_def bin_nth_ops mask_def) ultimately show ?thesis using False by(simp add: Let_def i'_def) qed qed text \Quickcheck conversion functions\ notation scomp (infixl "\\" 60) definition qc_random_cnv :: "(natural \ 'a::term_of) \ natural \ Random.seed \ ('a \ (unit \ Code_Evaluation.term)) \ Random.seed" where "qc_random_cnv a_of_natural i = Random.range (i + 1) \\ (\k. Pair ( let n = a_of_natural k in (n, \_. Code_Evaluation.term_of n)))" no_notation scomp (infixl "\\" 60) definition qc_exhaustive_cnv :: "(natural \ 'a) \ ('a \ (bool \ term list) option) \ natural \ (bool \ term list) option" where "qc_exhaustive_cnv a_of_natural f d = Quickcheck_Exhaustive.exhaustive (%x. f (a_of_natural x)) d" definition qc_full_exhaustive_cnv :: "(natural \ ('a::term_of)) \ ('a \ (unit \ term) \ (bool \ term list) option) \ natural \ (bool \ term list) option" where "qc_full_exhaustive_cnv a_of_natural f d = Quickcheck_Exhaustive.full_exhaustive (%(x, xt). f (a_of_natural x, %_. Code_Evaluation.term_of (a_of_natural x))) d" declare [[quickcheck_narrowing_ghc_options = "-XTypeSynonymInstances"]] definition qc_narrowing_drawn_from :: "'a list \ integer \ _" where "qc_narrowing_drawn_from xs = foldr Quickcheck_Narrowing.sum (map Quickcheck_Narrowing.cons (butlast xs)) (Quickcheck_Narrowing.cons (last xs))" locale quickcheck_narrowing_samples = fixes a_of_integer :: "integer \ 'a \ 'a :: {partial_term_of, term_of}" and zero :: "'a" and tr :: "typerep" begin function narrowing_samples :: "integer \ 'a list" where "narrowing_samples i = (if i > 0 then let (a, a') = a_of_integer i in narrowing_samples (i - 1) @ [a, a'] else [zero])" by pat_completeness auto termination including integer.lifting proof(relation "measure nat_of_integer") fix i :: integer assume "0 < i" thus "(i - 1, i) \ measure nat_of_integer" by simp(transfer, simp) qed simp definition partial_term_of_sample :: "integer \ 'a" where "partial_term_of_sample i = (if i < 0 then undefined else if i = 0 then zero else if i mod 2 = 0 then snd (a_of_integer (i div 2)) else fst (a_of_integer (i div 2 + 1)))" lemma partial_term_of_code: "partial_term_of (ty :: 'a itself) (Quickcheck_Narrowing.Narrowing_variable p t) \ Code_Evaluation.Free (STR ''_'') tr" "partial_term_of (ty :: 'a itself) (Quickcheck_Narrowing.Narrowing_constructor i []) \ Code_Evaluation.term_of (partial_term_of_sample i)" by (rule partial_term_of_anything)+ end lemmas [code] = quickcheck_narrowing_samples.narrowing_samples.simps quickcheck_narrowing_samples.partial_term_of_sample_def text \ The separate code target \SML_word\ collects setups for the code generator that PolyML does not provide. \ setup \Code_Target.add_derived_target ("SML_word", [(Code_ML.target_SML, I)])\ code_identifier code_module Code_Target_Word_Base \ (SML) Word and (Haskell) Word and (OCaml) Word and (Scala) Word end diff --git a/thys/Word_Lib/Word_Lib.thy b/thys/Word_Lib/Word_Lib.thy --- a/thys/Word_Lib/Word_Lib.thy +++ b/thys/Word_Lib/Word_Lib.thy @@ -1,744 +1,735 @@ (* * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause *) section "Additional Word Operations" theory Word_Lib imports "HOL-Library.Signed_Division" "HOL-Word.Misc_set_bit" Word_Syntax Signed_Words begin definition ptr_add :: "'a :: len word \ nat \ 'a word" where "ptr_add ptr n \ ptr + of_nat n" definition complement :: "'a :: len word \ 'a word" where "complement x \ ~~ x" definition alignUp :: "'a::len word \ nat \ 'a word" where "alignUp x n \ x + 2 ^ n - 1 && complement (2 ^ n - 1)" (* standard notation for blocks of 2^n-1 words, usually aligned; abbreviation so it simplifies directly *) abbreviation mask_range :: "'a::len word \ nat \ 'a word set" where "mask_range p n \ {p .. p + mask n}" (* Haskellish names/syntax *) notation (input) test_bit ("testBit") definition w2byte :: "'a :: len word \ 8 word" where "w2byte \ ucast" lemmas sdiv_int_def = signed_divide_int_def lemmas smod_int_def = signed_modulo_int_def instantiation word :: (len) signed_division begin lift_definition signed_divide_word :: \'a::len word \ 'a word \ 'a word\ is \\k l. signed_take_bit (LENGTH('a) - Suc 0) k sdiv signed_take_bit (LENGTH('a) - Suc 0) l\ by (simp flip: signed_take_bit_decr_length_iff) lift_definition signed_modulo_word :: \'a::len word \ 'a word \ 'a word\ is \\k l. signed_take_bit (LENGTH('a) - Suc 0) k smod signed_take_bit (LENGTH('a) - Suc 0) l\ by (simp flip: signed_take_bit_decr_length_iff) instance .. end lemma sdiv_word_def [code]: \v sdiv w = word_of_int (sint v sdiv sint w)\ for v w :: \'a::len word\ by transfer simp lemma smod_word_def [code]: \v smod w = word_of_int (sint v smod sint w)\ for v w :: \'a::len word\ by transfer simp lemma sdiv_smod_id: \(a sdiv b) * b + (a smod b) = a\ for a b :: \'a::len word\ by (cases \sint a < 0\; cases \sint b < 0\) (simp_all add: signed_modulo_int_def sdiv_word_def smod_word_def) (* Tests *) lemma "( 4 :: word32) sdiv 4 = 1" "(-4 :: word32) sdiv 4 = -1" "(-3 :: word32) sdiv 4 = 0" "( 3 :: word32) sdiv -4 = 0" "(-3 :: word32) sdiv -4 = 0" "(-5 :: word32) sdiv -4 = 1" "( 5 :: word32) sdiv -4 = -1" by (simp_all add: sdiv_word_def signed_divide_int_def) lemma "( 4 :: word32) smod 4 = 0" "( 3 :: word32) smod 4 = 3" "(-3 :: word32) smod 4 = -3" "( 3 :: word32) smod -4 = 3" "(-3 :: word32) smod -4 = -3" "(-5 :: word32) smod -4 = -1" "( 5 :: word32) smod -4 = 1" by (simp_all add: smod_word_def signed_modulo_int_def signed_divide_int_def) (* Count leading zeros *) definition word_clz :: "'a::len word \ nat" where "word_clz w \ length (takeWhile Not (to_bl w))" (* Count trailing zeros *) definition word_ctz :: "'a::len word \ nat" where "word_ctz w \ length (takeWhile Not (rev (to_bl w)))" definition word_log2 :: "'a::len word \ nat" where "word_log2 (w::'a::len word) \ size w - 1 - word_clz w" (* Bit population count. Equivalent of __builtin_popcount. *) definition pop_count :: "('a::len) word \ nat" where "pop_count w \ length (filter id (to_bl w))" (* Sign extension from bit n *) definition sign_extend :: "nat \ 'a::len word \ 'a word" where "sign_extend n w \ if w !! n then w || ~~ (mask n) else w && mask n" lemma sign_extend_eq_signed_take_bit: \sign_extend = signed_take_bit\ proof (rule ext)+ fix n and w :: \'a::len word\ show \sign_extend n w = signed_take_bit n w\ proof (rule bit_word_eqI) fix q assume \q < LENGTH('a)\ then show \bit (sign_extend n w) q \ bit (signed_take_bit n w) q\ by (auto simp add: test_bit_eq_bit bit_signed_take_bit_iff sign_extend_def bit_and_iff bit_or_iff bit_not_iff bit_mask_iff not_less exp_eq_0_imp_not_bit not_le min_def) qed qed definition sign_extended :: "nat \ 'a::len word \ bool" where "sign_extended n w \ \i. n < i \ i < size w \ w !! i = w !! n" lemma ptr_add_0 [simp]: "ptr_add ref 0 = ref " unfolding ptr_add_def by simp lemma shiftl_power: "(shiftl1 ^^ x) (y::'a::len word) = 2 ^ x * y" apply (induct x) apply simp apply (simp add: shiftl1_2t) done lemmas of_bl_reasoning = to_bl_use_of_bl of_bl_append lemma uint_of_bl_is_bl_to_bin_drop: "length (dropWhile Not l) \ LENGTH('a) \ uint (of_bl l :: 'a::len word) = bl_to_bin l" apply transfer apply (simp add: take_bit_eq_mod) apply (rule Divides.mod_less) apply (rule bl_to_bin_ge0) using bl_to_bin_lt2p_drop apply (rule order.strict_trans2) apply simp done corollary uint_of_bl_is_bl_to_bin: "length l\LENGTH('a) \ uint ((of_bl::bool list\ ('a :: len) word) l) = bl_to_bin l" apply(rule uint_of_bl_is_bl_to_bin_drop) using le_trans length_dropWhile_le by blast lemma bin_to_bl_or: "bin_to_bl n (a OR b) = map2 (\) (bin_to_bl n a) (bin_to_bl n b)" using bl_or_aux_bin[where n=n and v=a and w=b and bs="[]" and cs="[]"] by simp lemma word_ops_nth [simp]: shows word_or_nth: "(x || y) !! n = (x !! n \ y !! n)" and word_and_nth: "(x && y) !! n = (x !! n \ y !! n)" and word_xor_nth: "(x xor y) !! n = (x !! n \ y !! n)" by ((cases "n < size x", auto dest: test_bit_size simp: word_ops_nth_size word_size)[1])+ (* simp del to avoid warning on the simp add in iff *) declare test_bit_1 [simp del, iff] (* test: *) lemma "1 < (1024::32 word) \ 1 \ (1024::32 word)" by simp lemma and_not_mask: "w AND NOT (mask n) = (w >> n) << n" for w :: \'a::len word\ apply (rule word_eqI) apply (simp add : word_ops_nth_size word_size) apply (simp add : nth_shiftr nth_shiftl) by auto lemma and_mask: "w AND mask n = (w << (size w - n)) >> (size w - n)" for w :: \'a::len word\ apply (rule word_eqI) apply (simp add : word_ops_nth_size word_size) apply (simp add : nth_shiftr nth_shiftl) by auto lemma AND_twice [simp]: "(w && m) && m = w && m" by (fact and.right_idem) lemma word_combine_masks: "w && m = z \ w && m' = z' \ w && (m || m') = (z || z')" by (auto simp: word_eq_iff) lemma nth_w2p_same: "(2^n :: 'a :: len word) !! n = (n < LENGTH('a))" by (simp add : nth_w2p) lemma p2_gt_0: "(0 < (2 ^ n :: 'a :: len word)) = (n < LENGTH('a))" - apply (simp add : word_gt_0) - apply safe - apply (erule swap) - apply (rule word_eqI) - apply (simp add : nth_w2p) - apply (drule word_eqD) - apply simp - apply (erule notE) - apply (erule nth_w2p_same [THEN iffD2]) - done + by (simp add : word_gt_0 not_le) lemmas uint_2p_alt = uint_2p [unfolded p2_gt_0] lemma shiftr_div_2n_w: "n < size w \ w >> n = w div (2^n :: 'a :: len word)" apply (unfold word_div_def) apply (simp add : uint_2p_alt word_size) apply (rule word_uint.Rep_inverse' [THEN sym]) apply (rule shiftr_div_2n) done lemmas less_def = less_eq [symmetric] lemmas le_def = not_less [symmetric, where ?'a = nat] lemmas p2_eq_0 [simp] = trans [OF eq_commute iffD2 [OF Not_eq_iff p2_gt_0, folded le_def, unfolded word_gt_0 not_not]] lemma neg_mask_is_div': "n < size w \ w AND NOT (mask n) = ((w div (2 ^ n)) * (2 ^ n))" for w :: \'a::len word\ by (simp add : and_not_mask shiftr_div_2n_w shiftl_t2n word_size) lemma neg_mask_is_div: "w AND NOT (mask n) = (w div 2^n) * 2^n" for w :: \'a::len word\ apply (cases "n < size w") apply (erule neg_mask_is_div') apply (simp add: word_size) apply (frule p2_gt_0 [THEN Not_eq_iff [THEN iffD2], THEN iffD2]) apply (simp add: word_gt_0 del: p2_eq_0) apply (rule word_eqI) apply (simp add: word_ops_nth_size word_size) done lemma and_mask_arith': "0 < n \ w AND mask n = (w * 2^(size w - n)) div 2^(size w - n)" for w :: \'a::len word\ by (simp add: and_mask shiftr_div_2n_w shiftl_t2n word_size mult.commute) lemmas p2len = iffD2 [OF p2_eq_0 order_refl] lemma and_mask_arith: "w AND mask n = (w * 2^(size w - n)) div 2^(size w - n)" for w :: \'a::len word\ apply (cases "0 < n") apply (auto elim!: and_mask_arith') apply (simp add: word_size) done lemma mask_2pm1: "mask n = 2 ^ n - (1 :: 'a::len word)" by (fact mask_eq_decr_exp) lemma add_mask_fold: "x + 2 ^ n - 1 = x + mask n" for x :: \'a::len word\ by (simp add: mask_eq_decr_exp) lemma word_and_mask_le_2pm1: "w && mask n \ 2 ^ n - 1" by (simp add: mask_2pm1[symmetric] word_and_le1) lemma is_aligned_AND_less_0: "u && mask n = 0 \ v < 2^n \ u && v = 0" apply (drule less_mask_eq) apply (simp add: mask_2pm1) apply (rule word_eqI) apply (clarsimp simp add: word_size) apply (drule_tac x=na in word_eqD) apply (drule_tac x=na in word_eqD) apply simp done lemma le_shiftr1: "u <= v \ shiftr1 u <= shiftr1 v" apply (unfold word_le_def shiftr1_eq word_ubin.eq_norm) apply (unfold bin_rest_trunc_i trans [OF bintrunc_bintrunc_l word_ubin.norm_Rep, unfolded word_ubin.norm_Rep, OF order_refl [THEN le_SucI]]) apply (case_tac "uint u" rule: bin_exhaust) apply (rename_tac bs bit) apply (case_tac "uint v" rule: bin_exhaust) apply (rename_tac bs' bit') apply (case_tac "bit") apply (case_tac "bit'", auto simp: less_eq_int_code)[1] apply (case_tac bit') apply (simp add: less_eq_int_code) apply (simp add: less_eq_int_code) done lemma le_shiftr: "u \ v \ u >> (n :: nat) \ (v :: 'a :: len word) >> n" apply (unfold shiftr_def) apply (induct_tac "n") apply auto apply (erule le_shiftr1) done lemma shiftr_mask_le: "n <= m \ mask n >> m = (0 :: 'a::len word)" apply (rule word_eqI) apply (simp add: word_size nth_shiftr) done lemmas shiftr_mask = order_refl [THEN shiftr_mask_le, simp] lemma word_leI: "(\n. \n < size (u::'a::len word); u !! n \ \ (v::'a::len word) !! n) \ u <= v" apply (rule xtr4) apply (rule word_and_le2) apply (rule word_eqI) apply (simp add: word_ao_nth) apply safe apply assumption apply (erule_tac [2] asm_rl) apply (unfold word_size) by auto lemma le_mask_iff: "(w \ mask n) = (w >> n = 0)" for w :: \'a::len word\ apply safe apply (rule word_le_0_iff [THEN iffD1]) apply (rule xtr3) apply (erule_tac [2] le_shiftr) apply simp apply (rule word_leI) apply (rename_tac n') apply (drule_tac x = "n' - n" in word_eqD) apply (simp add : nth_shiftr word_size) apply (case_tac "n <= n'") by auto lemma and_mask_eq_iff_shiftr_0: "(w AND mask n = w) = (w >> n = 0)" for w :: \'a::len word\ apply (unfold test_bit_eq_iff [THEN sym]) apply (rule iffI) apply (rule ext) apply (rule_tac [2] ext) apply (auto simp add : word_ao_nth nth_shiftr) apply (drule arg_cong) apply (drule iffD2) apply assumption apply (simp add : word_ao_nth) prefer 2 apply (simp add : word_size test_bit_bin) apply (drule_tac f = "%u. u !! (x - n)" in arg_cong) apply (simp add : nth_shiftr) apply (case_tac "n <= x") apply auto done lemmas and_mask_eq_iff_le_mask = trans [OF and_mask_eq_iff_shiftr_0 le_mask_iff [THEN sym]] lemma mask_shiftl_decompose: "mask m << n = mask (m + n) && ~~ (mask n)" by (auto intro!: word_eqI simp: and_not_mask nth_shiftl nth_shiftr word_size) lemma one_bit_shiftl: "set_bit 0 n True = (1 :: 'a :: len word) << n" apply (rule word_eqI) apply (auto simp add: test_bit_set_gen nth_shiftl word_size simp del: word_set_bit_0 shiftl_1) done lemmas one_bit_pow = trans [OF one_bit_shiftl shiftl_1] lemmas bin_sc_minus_simps = bin_sc_simps (2,3,4) [THEN [2] trans, OF bin_sc_minus [THEN sym]] lemma NOT_eq: "NOT (x :: 'a :: len word) = - x - 1" apply (cut_tac x = "x" in word_add_not) apply (drule add.commute [THEN trans]) apply (drule eq_diff_eq [THEN iffD2]) by simp lemma NOT_mask: "NOT (mask n :: 'a::len word) = - (2 ^ n)" by (simp add : NOT_eq mask_2pm1) lemma le_m1_iff_lt: "(x > (0 :: 'a :: len word)) = ((y \ x - 1) = (y < x))" by uint_arith lemmas gt0_iff_gem1 = iffD1 [OF iffD1 [OF iff_left_commute le_m1_iff_lt] order_refl] lemmas power_2_ge_iff = trans [OF gt0_iff_gem1 [THEN sym] p2_gt_0] lemma le_mask_iff_lt_2n: "n < len_of TYPE ('a) = (((w :: 'a :: len word) \ mask n) = (w < 2 ^ n))" unfolding mask_2pm1 by (rule trans [OF p2_gt_0 [THEN sym] le_m1_iff_lt]) lemmas mask_lt_2pn = le_mask_iff_lt_2n [THEN iffD1, THEN iffD1, OF _ order_refl] lemma bang_eq: fixes x :: "'a::len word" shows "(x = y) = (\n. x !! n = y !! n)" by (subst test_bit_eq_iff[symmetric]) fastforce lemma word_unat_power: "(2 :: 'a :: len word) ^ n = of_nat (2 ^ n)" by simp lemma of_nat_mono_maybe: assumes xlt: "x < 2 ^ len_of TYPE ('a)" shows "y < x \ of_nat y < (of_nat x :: 'a :: len word)" apply (subst word_less_nat_alt) apply (subst unat_of_nat)+ apply (subst mod_less) apply (erule order_less_trans [OF _ xlt]) apply (subst mod_less [OF xlt]) apply assumption done lemma shiftl_over_and_dist: fixes a::"'a::len word" shows "(a AND b) << c = (a << c) AND (b << c)" apply(rule word_eqI) apply(simp add: word_ao_nth nth_shiftl, safe) done lemma shiftr_over_and_dist: fixes a::"'a::len word" shows "a AND b >> c = (a >> c) AND (b >> c)" apply(rule word_eqI) apply(simp add:nth_shiftr word_ao_nth) done lemma sshiftr_over_and_dist: fixes a::"'a::len word" shows "a AND b >>> c = (a >>> c) AND (b >>> c)" apply(rule word_eqI) apply(simp add:nth_sshiftr word_ao_nth word_size) done lemma shiftl_over_or_dist: fixes a::"'a::len word" shows "a OR b << c = (a << c) OR (b << c)" apply(rule word_eqI) apply(simp add:nth_shiftl word_ao_nth, safe) done lemma shiftr_over_or_dist: fixes a::"'a::len word" shows "a OR b >> c = (a >> c) OR (b >> c)" apply(rule word_eqI) apply(simp add:nth_shiftr word_ao_nth) done lemma sshiftr_over_or_dist: fixes a::"'a::len word" shows "a OR b >>> c = (a >>> c) OR (b >>> c)" apply(rule word_eqI) apply(simp add:nth_sshiftr word_ao_nth word_size) done lemmas shift_over_ao_dists = shiftl_over_or_dist shiftr_over_or_dist sshiftr_over_or_dist shiftl_over_and_dist shiftr_over_and_dist sshiftr_over_and_dist lemma shiftl_shiftl: fixes a::"'a::len word" shows "a << b << c = a << (b + c)" apply(rule word_eqI) apply(auto simp:word_size nth_shiftl add.commute add.left_commute) done lemma shiftr_shiftr: fixes a::"'a::len word" shows "a >> b >> c = a >> (b + c)" apply(rule word_eqI) apply(simp add:word_size nth_shiftr add.left_commute add.commute) done lemma shiftl_shiftr1: fixes a::"'a::len word" shows "c \ b \ a << b >> c = a AND (mask (size a - b)) << (b - c)" apply(rule word_eqI) apply(auto simp:nth_shiftr nth_shiftl word_size word_ao_nth) done lemma shiftl_shiftr2: fixes a::"'a::len word" shows "b < c \ a << b >> c = (a >> (c - b)) AND (mask (size a - c))" apply(rule word_eqI) apply(auto simp:nth_shiftr nth_shiftl word_size word_ao_nth) done lemma shiftr_shiftl1: fixes a::"'a::len word" shows "c \ b \ a >> b << c = (a >> (b - c)) AND (NOT (mask c))" apply(rule word_eqI) apply(auto simp:nth_shiftr nth_shiftl word_size word_ops_nth_size) done lemma shiftr_shiftl2: fixes a::"'a::len word" shows "b < c \ a >> b << c = (a << (c - b)) AND (NOT (mask c))" apply(rule word_eqI) apply(auto simp:nth_shiftr nth_shiftl word_size word_ops_nth_size) done lemmas multi_shift_simps = shiftl_shiftl shiftr_shiftr shiftl_shiftr1 shiftl_shiftr2 shiftr_shiftl1 shiftr_shiftl2 lemma word_and_max_word: fixes a::"'a::len word" shows "x = max_word \ a AND x = a" by simp lemma word_and_full_mask_simp: \x && Bit_Operations.mask LENGTH('a) = x\ for x :: \'a::len word\ proof (rule bit_eqI) fix n assume \2 ^ n \ (0 :: 'a word)\ then have \n < LENGTH('a)\ by simp then show \bit (x && Bit_Operations.mask LENGTH('a)) n \ bit x n\ by (simp add: bit_and_iff bit_mask_iff) qed lemma word8_and_max_simp: \x && 0xFF = x\ for x :: \8 word\ using word_and_full_mask_simp [of x] by (simp add: numeral_eq_Suc mask_Suc_exp) lemma word16_and_max_simp: \x && 0xFFFF = x\ for x :: \16 word\ using word_and_full_mask_simp [of x] by (simp add: numeral_eq_Suc mask_Suc_exp) lemma word32_and_max_simp: \x && 0xFFFFFFFF = x\ for x :: \32 word\ using word_and_full_mask_simp [of x] by (simp add: numeral_eq_Suc mask_Suc_exp) lemma word64_and_max_simp: \x && 0xFFFFFFFFFFFFFFFF = x\ for x :: \64 word\ using word_and_full_mask_simp [of x] by (simp add: numeral_eq_Suc mask_Suc_exp) lemmas word_and_max_simps = word8_and_max_simp word16_and_max_simp word32_and_max_simp word64_and_max_simp lemma word_and_1_bl: fixes x::"'a::len word" shows "(x AND 1) = of_bl [x !! 0]" by (simp add: mod_2_eq_odd test_bit_word_eq and_one_eq) lemma word_1_and_bl: fixes x::"'a::len word" shows "(1 AND x) = of_bl [x !! 0]" by (simp add: mod_2_eq_odd test_bit_word_eq one_and_eq) lemma scast_scast_id [simp]: "scast (scast x :: ('a::len) signed word) = (x :: 'a word)" "scast (scast y :: ('a::len) word) = (y :: 'a signed word)" by (auto simp: is_up scast_up_scast_id) lemma scast_ucast_id [simp]: "scast (ucast (x :: 'a::len word) :: 'a signed word) = x" by (metis down_cast_same is_down len_signed order_refl scast_scast_id(1)) lemma ucast_scast_id [simp]: "ucast (scast (x :: 'a::len signed word) :: 'a word) = x" by (metis scast_scast_id(2) scast_ucast_id) lemma scast_of_nat [simp]: "scast (of_nat x :: 'a::len signed word) = (of_nat x :: 'a word)" by transfer simp lemma ucast_of_nat: "is_down (ucast :: 'a :: len word \ 'b :: len word) \ ucast (of_nat n :: 'a word) = (of_nat n :: 'b word)" by transfer simp (* shortcut for some specific lengths *) lemma word_fixed_sint_1[simp]: "sint (1::8 word) = 1" "sint (1::16 word) = 1" "sint (1::32 word) = 1" "sint (1::64 word) = 1" by (auto simp: sint_word_ariths) lemma word_sint_1 [simp]: "sint (1::'a::len word) = (if LENGTH('a) = 1 then -1 else 1)" by (cases \LENGTH('a)\) (simp_all add: not_le sint_uint le_Suc_eq sbintrunc_minus_simps) lemma scast_1': "(scast (1::'a::len word) :: 'b::len word) = (word_of_int (sbintrunc (LENGTH('a::len) - Suc 0) (1::int)))" by transfer simp lemma scast_1: "(scast (1::'a::len word) :: 'b::len word) = (if LENGTH('a) = 1 then -1 else 1)" by (fact signed_1) lemma scast_eq_scast_id [simp]: "((scast (a :: 'a::len signed word) :: 'a word) = scast b) = (a = b)" by (metis ucast_scast_id) lemma ucast_eq_ucast_id [simp]: "((ucast (a :: 'a::len word) :: 'a signed word) = ucast b) = (a = b)" by (metis scast_ucast_id) lemma scast_ucast_norm [simp]: "(ucast (a :: 'a::len word) = (b :: 'a signed word)) = (a = scast b)" "((b :: 'a signed word) = ucast (a :: 'a::len word)) = (a = scast b)" by (metis scast_ucast_id ucast_scast_id)+ lemma of_bl_drop: "of_bl (drop n xs) = (of_bl xs && mask (length xs - n))" apply (clarsimp simp: bang_eq test_bit_of_bl rev_nth cong: rev_conj_cong) apply (safe; simp add: word_size to_bl_nth) done lemma of_int_uint: "of_int (uint x) = x" by (fact word_of_int_uint) lemma shiftr_mask2: "n \ LENGTH('a) \ (mask n >> m :: ('a :: len) word) = mask (n - m)" apply (rule word_eqI) apply (simp add: nth_shiftr word_size) apply arith done corollary word_plus_and_or_coroll: "x && y = 0 \ x + y = x || y" using word_plus_and_or[where x=x and y=y] by simp corollary word_plus_and_or_coroll2: "(x && w) + (x && ~~ w) = x" apply (subst word_plus_and_or_coroll) apply (rule word_eqI, simp add: word_size word_ops_nth_size) apply (rule word_eqI, simp add: word_size word_ops_nth_size) apply blast done lemma less_le_mult_nat': "w * c < b * c ==> 0 \ c ==> Suc w * c \ b * (c::nat)" apply (rule mult_right_mono) apply (rule Suc_leI) apply (erule (1) mult_right_less_imp_less) apply assumption done lemmas less_le_mult_nat = less_le_mult_nat'[simplified distrib_right, simplified] (* FIXME: these should eventually be moved to HOL/Word. *) lemmas extra_sle_sless_unfolds [simp] = word_sle_eq[where a=0 and b=1] word_sle_eq[where a=0 and b="numeral n"] word_sle_eq[where a=1 and b=0] word_sle_eq[where a=1 and b="numeral n"] word_sle_eq[where a="numeral n" and b=0] word_sle_eq[where a="numeral n" and b=1] word_sless_alt[where a=0 and b=1] word_sless_alt[where a=0 and b="numeral n"] word_sless_alt[where a=1 and b=0] word_sless_alt[where a=1 and b="numeral n"] word_sless_alt[where a="numeral n" and b=0] word_sless_alt[where a="numeral n" and b=1] for n lemma to_bl_1: "to_bl (1::'a::len word) = replicate (LENGTH('a) - 1) False @ [True]" by (rule nth_equalityI) (auto simp add: to_bl_unfold nth_append rev_nth bit_1_iff not_less not_le) lemma list_of_false: "True \ set xs \ xs = replicate (length xs) False" by (induct xs, simp_all) lemma eq_zero_set_bl: "(w = 0) = (True \ set (to_bl w))" using list_of_false word_bl.Rep_inject by fastforce lemma diff_diff_less: "(i < m - (m - (n :: nat))) = (i < m \ i < n)" by auto lemma pop_count_0[simp]: "pop_count 0 = 0" by (clarsimp simp:pop_count_def) lemma pop_count_1[simp]: "pop_count 1 = 1" by (clarsimp simp:pop_count_def to_bl_1) lemma pop_count_0_imp_0: "(pop_count w = 0) = (w = 0)" apply (rule iffI) apply (clarsimp simp:pop_count_def) apply (subst (asm) filter_empty_conv) apply (clarsimp simp:eq_zero_set_bl) apply fast apply simp done end