diff --git a/src/HOL/Library/Bit_Operations.thy b/src/HOL/Library/Bit_Operations.thy --- a/src/HOL/Library/Bit_Operations.thy +++ b/src/HOL/Library/Bit_Operations.thy @@ -1,1921 +1,1939 @@ (* Author: Florian Haftmann, TUM *) section \Bit operations in suitable algebraic structures\ theory Bit_Operations imports Main "HOL-Library.Boolean_Algebra" begin subsection \Bit operations\ class semiring_bit_operations = semiring_bit_shifts + fixes "and" :: \'a \ 'a \ 'a\ (infixr \AND\ 64) and or :: \'a \ 'a \ 'a\ (infixr \OR\ 59) and xor :: \'a \ 'a \ 'a\ (infixr \XOR\ 59) and mask :: \nat \ 'a\ and set_bit :: \nat \ 'a \ 'a\ and unset_bit :: \nat \ 'a \ 'a\ and flip_bit :: \nat \ 'a \ 'a\ assumes bit_and_iff [bit_simps]: \bit (a AND b) n \ bit a n \ bit b n\ and bit_or_iff [bit_simps]: \bit (a OR b) n \ bit a n \ bit b n\ and bit_xor_iff [bit_simps]: \bit (a XOR b) n \ bit a n \ bit b n\ and mask_eq_exp_minus_1: \mask n = 2 ^ n - 1\ and set_bit_eq_or: \set_bit n a = a OR push_bit n 1\ and bit_unset_bit_iff [bit_simps]: \bit (unset_bit m a) n \ bit a n \ m \ n\ and flip_bit_eq_xor: \flip_bit n a = a XOR push_bit n 1\ begin text \ We want the bitwise operations to bind slightly weaker than \+\ and \-\. For the sake of code generation the operations \<^const>\and\, \<^const>\or\ and \<^const>\xor\ are specified as definitional class operations. \ sublocale "and": semilattice \(AND)\ by standard (auto simp add: bit_eq_iff bit_and_iff) sublocale or: semilattice_neutr \(OR)\ 0 by standard (auto simp add: bit_eq_iff bit_or_iff) sublocale xor: comm_monoid \(XOR)\ 0 by standard (auto simp add: bit_eq_iff bit_xor_iff) lemma even_and_iff: \even (a AND b) \ even a \ even b\ using bit_and_iff [of a b 0] by auto lemma even_or_iff: \even (a OR b) \ even a \ even b\ using bit_or_iff [of a b 0] by auto lemma even_xor_iff: \even (a XOR b) \ (even a \ even b)\ using bit_xor_iff [of a b 0] by auto lemma zero_and_eq [simp]: "0 AND a = 0" by (simp add: bit_eq_iff bit_and_iff) lemma and_zero_eq [simp]: "a AND 0 = 0" by (simp add: bit_eq_iff bit_and_iff) lemma one_and_eq: "1 AND a = a mod 2" by (simp add: bit_eq_iff bit_and_iff) (auto simp add: bit_1_iff) lemma and_one_eq: "a AND 1 = a mod 2" using one_and_eq [of a] by (simp add: ac_simps) lemma one_or_eq: "1 OR a = a + of_bool (even a)" by (simp add: bit_eq_iff bit_or_iff add.commute [of _ 1] even_bit_succ_iff) (auto simp add: bit_1_iff) lemma or_one_eq: "a OR 1 = a + of_bool (even a)" using one_or_eq [of a] by (simp add: ac_simps) lemma one_xor_eq: "1 XOR a = a + of_bool (even a) - of_bool (odd a)" by (simp add: bit_eq_iff bit_xor_iff add.commute [of _ 1] even_bit_succ_iff) (auto simp add: bit_1_iff odd_bit_iff_bit_pred elim: oddE) lemma xor_one_eq: "a XOR 1 = a + of_bool (even a) - of_bool (odd a)" using one_xor_eq [of a] by (simp add: ac_simps) lemma take_bit_and [simp]: \take_bit n (a AND b) = take_bit n a AND take_bit n b\ by (auto simp add: bit_eq_iff bit_take_bit_iff bit_and_iff) lemma take_bit_or [simp]: \take_bit n (a OR b) = take_bit n a OR take_bit n b\ by (auto simp add: bit_eq_iff bit_take_bit_iff bit_or_iff) lemma take_bit_xor [simp]: \take_bit n (a XOR b) = take_bit n a XOR take_bit n b\ by (auto simp add: bit_eq_iff bit_take_bit_iff bit_xor_iff) lemma push_bit_and [simp]: \push_bit n (a AND b) = push_bit n a AND push_bit n b\ by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_and_iff) lemma push_bit_or [simp]: \push_bit n (a OR b) = push_bit n a OR push_bit n b\ by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_or_iff) lemma push_bit_xor [simp]: \push_bit n (a XOR b) = push_bit n a XOR push_bit n b\ by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_xor_iff) lemma drop_bit_and [simp]: \drop_bit n (a AND b) = drop_bit n a AND drop_bit n b\ by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_and_iff) lemma drop_bit_or [simp]: \drop_bit n (a OR b) = drop_bit n a OR drop_bit n b\ by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_or_iff) lemma drop_bit_xor [simp]: \drop_bit n (a XOR b) = drop_bit n a XOR drop_bit n b\ by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_xor_iff) lemma bit_mask_iff [bit_simps]: \bit (mask m) n \ 2 ^ n \ 0 \ n < m\ by (simp add: mask_eq_exp_minus_1 bit_mask_iff) lemma even_mask_iff: \even (mask n) \ n = 0\ using bit_mask_iff [of n 0] by auto lemma mask_0 [simp]: \mask 0 = 0\ by (simp add: mask_eq_exp_minus_1) lemma mask_Suc_0 [simp]: \mask (Suc 0) = 1\ by (simp add: mask_eq_exp_minus_1 add_implies_diff sym) lemma mask_Suc_exp: \mask (Suc n) = 2 ^ n OR mask n\ by (rule bit_eqI) (auto simp add: bit_or_iff bit_mask_iff bit_exp_iff not_less le_less_Suc_eq) lemma mask_Suc_double: \mask (Suc n) = 1 OR 2 * mask n\ proof (rule bit_eqI) fix q assume \2 ^ q \ 0\ show \bit (mask (Suc n)) q \ bit (1 OR 2 * mask n) q\ by (cases q) (simp_all add: even_mask_iff even_or_iff bit_or_iff bit_mask_iff bit_exp_iff bit_double_iff not_less le_less_Suc_eq bit_1_iff, auto simp add: mult_2) qed lemma mask_numeral: \mask (numeral n) = 1 + 2 * mask (pred_numeral n)\ by (simp add: numeral_eq_Suc mask_Suc_double one_or_eq ac_simps) lemma take_bit_mask [simp]: \take_bit m (mask n) = mask (min m n)\ by (rule bit_eqI) (simp add: bit_simps) lemma take_bit_eq_mask: \take_bit n a = a AND mask n\ by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_and_iff bit_mask_iff) lemma or_eq_0_iff: \a OR b = 0 \ a = 0 \ b = 0\ by (auto simp add: bit_eq_iff bit_or_iff) lemma disjunctive_add: \a + b = a OR b\ if \\n. \ bit a n \ \ bit b n\ by (rule bit_eqI) (use that in \simp add: bit_disjunctive_add_iff bit_or_iff\) lemma bit_iff_and_drop_bit_eq_1: \bit a n \ drop_bit n a AND 1 = 1\ by (simp add: bit_iff_odd_drop_bit and_one_eq odd_iff_mod_2_eq_one) lemma bit_iff_and_push_bit_not_eq_0: \bit a n \ a AND push_bit n 1 \ 0\ apply (cases \2 ^ n = 0\) apply (simp_all add: push_bit_of_1 bit_eq_iff bit_and_iff bit_push_bit_iff exp_eq_0_imp_not_bit) apply (simp_all add: bit_exp_iff) done lemmas set_bit_def = set_bit_eq_or lemma bit_set_bit_iff [bit_simps]: \bit (set_bit m a) n \ bit a n \ (m = n \ 2 ^ n \ 0)\ by (auto simp add: set_bit_def push_bit_of_1 bit_or_iff bit_exp_iff) lemma even_set_bit_iff: \even (set_bit m a) \ even a \ m \ 0\ using bit_set_bit_iff [of m a 0] by auto lemma even_unset_bit_iff: \even (unset_bit m a) \ even a \ m = 0\ using bit_unset_bit_iff [of m a 0] by auto +lemma and_exp_eq_0_iff_not_bit: + \a AND 2 ^ n = 0 \ \ bit a n\ (is \?P \ ?Q\) +proof + assume ?Q + then show ?P + by (auto intro: bit_eqI simp add: bit_simps) +next + assume ?P + show ?Q + proof (rule notI) + assume \bit a n\ + then have \a AND 2 ^ n = 2 ^ n\ + by (auto intro: bit_eqI simp add: bit_simps) + with \?P\ show False + using \bit a n\ exp_eq_0_imp_not_bit by auto + qed +qed + lemmas flip_bit_def = flip_bit_eq_xor lemma bit_flip_bit_iff [bit_simps]: \bit (flip_bit m a) n \ (m = n \ \ bit a n) \ 2 ^ n \ 0\ by (auto simp add: flip_bit_def push_bit_of_1 bit_xor_iff bit_exp_iff exp_eq_0_imp_not_bit) lemma even_flip_bit_iff: \even (flip_bit m a) \ \ (even a \ m = 0)\ using bit_flip_bit_iff [of m a 0] by auto lemma set_bit_0 [simp]: \set_bit 0 a = 1 + 2 * (a div 2)\ proof (rule bit_eqI) fix m assume *: \2 ^ m \ 0\ then show \bit (set_bit 0 a) m = bit (1 + 2 * (a div 2)) m\ by (simp add: bit_set_bit_iff bit_double_iff even_bit_succ_iff) (cases m, simp_all add: bit_Suc) qed lemma set_bit_Suc: \set_bit (Suc n) a = a mod 2 + 2 * set_bit n (a div 2)\ proof (rule bit_eqI) fix m assume *: \2 ^ m \ 0\ show \bit (set_bit (Suc n) a) m \ bit (a mod 2 + 2 * set_bit n (a div 2)) m\ proof (cases m) case 0 then show ?thesis by (simp add: even_set_bit_iff) next case (Suc m) with * have \2 ^ m \ 0\ using mult_2 by auto show ?thesis by (cases a rule: parity_cases) (simp_all add: bit_set_bit_iff bit_double_iff even_bit_succ_iff *, simp_all add: Suc \2 ^ m \ 0\ bit_Suc) qed qed lemma unset_bit_0 [simp]: \unset_bit 0 a = 2 * (a div 2)\ proof (rule bit_eqI) fix m assume *: \2 ^ m \ 0\ then show \bit (unset_bit 0 a) m = bit (2 * (a div 2)) m\ by (simp add: bit_unset_bit_iff bit_double_iff) (cases m, simp_all add: bit_Suc) qed lemma unset_bit_Suc: \unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)\ proof (rule bit_eqI) fix m assume *: \2 ^ m \ 0\ then show \bit (unset_bit (Suc n) a) m \ bit (a mod 2 + 2 * unset_bit n (a div 2)) m\ proof (cases m) case 0 then show ?thesis by (simp add: even_unset_bit_iff) next case (Suc m) show ?thesis by (cases a rule: parity_cases) (simp_all add: bit_unset_bit_iff bit_double_iff even_bit_succ_iff *, simp_all add: Suc bit_Suc) qed qed lemma flip_bit_0 [simp]: \flip_bit 0 a = of_bool (even a) + 2 * (a div 2)\ proof (rule bit_eqI) fix m assume *: \2 ^ m \ 0\ then show \bit (flip_bit 0 a) m = bit (of_bool (even a) + 2 * (a div 2)) m\ by (simp add: bit_flip_bit_iff bit_double_iff even_bit_succ_iff) (cases m, simp_all add: bit_Suc) qed lemma flip_bit_Suc: \flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)\ proof (rule bit_eqI) fix m assume *: \2 ^ m \ 0\ show \bit (flip_bit (Suc n) a) m \ bit (a mod 2 + 2 * flip_bit n (a div 2)) m\ proof (cases m) case 0 then show ?thesis by (simp add: even_flip_bit_iff) next case (Suc m) with * have \2 ^ m \ 0\ using mult_2 by auto show ?thesis by (cases a rule: parity_cases) (simp_all add: bit_flip_bit_iff bit_double_iff even_bit_succ_iff, simp_all add: Suc \2 ^ m \ 0\ bit_Suc) qed qed lemma flip_bit_eq_if: \flip_bit n a = (if bit a n then unset_bit else set_bit) n a\ by (rule bit_eqI) (auto simp add: bit_set_bit_iff bit_unset_bit_iff bit_flip_bit_iff) lemma take_bit_set_bit_eq: \take_bit n (set_bit m a) = (if n \ m then take_bit n a else set_bit m (take_bit n a))\ by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_set_bit_iff) lemma take_bit_unset_bit_eq: \take_bit n (unset_bit m a) = (if n \ m then take_bit n a else unset_bit m (take_bit n a))\ by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_unset_bit_iff) lemma take_bit_flip_bit_eq: \take_bit n (flip_bit m a) = (if n \ m then take_bit n a else flip_bit m (take_bit n a))\ by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_flip_bit_iff) end class ring_bit_operations = semiring_bit_operations + ring_parity + fixes not :: \'a \ 'a\ (\NOT\) assumes bit_not_iff [bit_simps]: \\n. bit (NOT a) n \ 2 ^ n \ 0 \ \ bit a n\ assumes minus_eq_not_minus_1: \- a = NOT (a - 1)\ begin text \ For the sake of code generation \<^const>\not\ is specified as definitional class operation. Note that \<^const>\not\ has no sensible definition for unlimited but only positive bit strings (type \<^typ>\nat\). \ lemma bits_minus_1_mod_2_eq [simp]: \(- 1) mod 2 = 1\ by (simp add: mod_2_eq_odd) lemma not_eq_complement: \NOT a = - a - 1\ using minus_eq_not_minus_1 [of \a + 1\] by simp lemma minus_eq_not_plus_1: \- a = NOT a + 1\ using not_eq_complement [of a] by simp lemma bit_minus_iff [bit_simps]: \bit (- a) n \ 2 ^ n \ 0 \ \ bit (a - 1) n\ by (simp add: minus_eq_not_minus_1 bit_not_iff) lemma even_not_iff [simp]: "even (NOT a) \ odd a" using bit_not_iff [of a 0] by auto lemma bit_not_exp_iff [bit_simps]: \bit (NOT (2 ^ m)) n \ 2 ^ n \ 0 \ n \ m\ by (auto simp add: bit_not_iff bit_exp_iff) lemma bit_minus_1_iff [simp]: \bit (- 1) n \ 2 ^ n \ 0\ by (simp add: bit_minus_iff) lemma bit_minus_exp_iff [bit_simps]: \bit (- (2 ^ m)) n \ 2 ^ n \ 0 \ n \ m\ by (auto simp add: bit_simps simp flip: mask_eq_exp_minus_1) lemma bit_minus_2_iff [simp]: \bit (- 2) n \ 2 ^ n \ 0 \ n > 0\ by (simp add: bit_minus_iff bit_1_iff) lemma not_one [simp]: "NOT 1 = - 2" by (simp add: bit_eq_iff bit_not_iff) (simp add: bit_1_iff) sublocale "and": semilattice_neutr \(AND)\ \- 1\ by standard (rule bit_eqI, simp add: bit_and_iff) sublocale bit: boolean_algebra \(AND)\ \(OR)\ NOT 0 \- 1\ rewrites \bit.xor = (XOR)\ proof - interpret bit: boolean_algebra \(AND)\ \(OR)\ NOT 0 \- 1\ by standard (auto simp add: bit_and_iff bit_or_iff bit_not_iff intro: bit_eqI) show \boolean_algebra (AND) (OR) NOT 0 (- 1)\ by standard show \boolean_algebra.xor (AND) (OR) NOT = (XOR)\ by (rule ext, rule ext, rule bit_eqI) (auto simp add: bit.xor_def bit_and_iff bit_or_iff bit_xor_iff bit_not_iff) qed lemma and_eq_not_not_or: \a AND b = NOT (NOT a OR NOT b)\ by simp lemma or_eq_not_not_and: \a OR b = NOT (NOT a AND NOT b)\ by simp lemma not_add_distrib: \NOT (a + b) = NOT a - b\ by (simp add: not_eq_complement algebra_simps) lemma not_diff_distrib: \NOT (a - b) = NOT a + b\ using not_add_distrib [of a \- b\] by simp lemma (in ring_bit_operations) and_eq_minus_1_iff: \a AND b = - 1 \ a = - 1 \ b = - 1\ proof assume \a = - 1 \ b = - 1\ then show \a AND b = - 1\ by simp next assume \a AND b = - 1\ have *: \bit a n\ \bit b n\ if \2 ^ n \ 0\ for n proof - from \a AND b = - 1\ have \bit (a AND b) n = bit (- 1) n\ by (simp add: bit_eq_iff) then show \bit a n\ \bit b n\ using that by (simp_all add: bit_and_iff) qed have \a = - 1\ by (rule bit_eqI) (simp add: *) moreover have \b = - 1\ by (rule bit_eqI) (simp add: *) ultimately show \a = - 1 \ b = - 1\ by simp qed lemma disjunctive_diff: \a - b = a AND NOT b\ if \\n. bit b n \ bit a n\ proof - have \NOT a + b = NOT a OR b\ by (rule disjunctive_add) (auto simp add: bit_not_iff dest: that) then have \NOT (NOT a + b) = NOT (NOT a OR b)\ by simp then show ?thesis by (simp add: not_add_distrib) qed lemma push_bit_minus: \push_bit n (- a) = - push_bit n a\ by (simp add: push_bit_eq_mult) lemma take_bit_not_take_bit: \take_bit n (NOT (take_bit n a)) = take_bit n (NOT a)\ by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff) lemma take_bit_not_iff: "take_bit n (NOT a) = take_bit n (NOT b) \ take_bit n a = take_bit n b" apply (simp add: bit_eq_iff) apply (simp add: bit_not_iff bit_take_bit_iff bit_exp_iff) apply (use exp_eq_0_imp_not_bit in blast) done lemma take_bit_not_eq_mask_diff: \take_bit n (NOT a) = mask n - take_bit n a\ proof - have \take_bit n (NOT a) = take_bit n (NOT (take_bit n a))\ by (simp add: take_bit_not_take_bit) also have \\ = mask n AND NOT (take_bit n a)\ by (simp add: take_bit_eq_mask ac_simps) also have \\ = mask n - take_bit n a\ by (subst disjunctive_diff) (auto simp add: bit_take_bit_iff bit_mask_iff exp_eq_0_imp_not_bit) finally show ?thesis by simp qed lemma mask_eq_take_bit_minus_one: \mask n = take_bit n (- 1)\ by (simp add: bit_eq_iff bit_mask_iff bit_take_bit_iff conj_commute) lemma take_bit_minus_one_eq_mask: \take_bit n (- 1) = mask n\ by (simp add: mask_eq_take_bit_minus_one) lemma minus_exp_eq_not_mask: \- (2 ^ n) = NOT (mask n)\ by (rule bit_eqI) (simp add: bit_minus_iff bit_not_iff flip: mask_eq_exp_minus_1) lemma push_bit_minus_one_eq_not_mask: \push_bit n (- 1) = NOT (mask n)\ by (simp add: push_bit_eq_mult minus_exp_eq_not_mask) lemma take_bit_not_mask_eq_0: \take_bit m (NOT (mask n)) = 0\ if \n \ m\ by (rule bit_eqI) (use that in \simp add: bit_take_bit_iff bit_not_iff bit_mask_iff\) lemma unset_bit_eq_and_not: \unset_bit n a = a AND NOT (push_bit n 1)\ by (rule bit_eqI) (auto simp add: bit_simps) lemmas unset_bit_def = unset_bit_eq_and_not end subsection \Instance \<^typ>\int\\ lemma int_bit_bound: fixes k :: int obtains n where \\m. n \ m \ bit k m \ bit k n\ and \n > 0 \ bit k (n - 1) \ bit k n\ proof - obtain q where *: \\m. q \ m \ bit k m \ bit k q\ proof (cases \k \ 0\) case True moreover from power_gt_expt [of 2 \nat k\] have \k < 2 ^ nat k\ by simp ultimately have *: \k div 2 ^ nat k = 0\ by simp show thesis proof (rule that [of \nat k\]) fix m assume \nat k \ m\ then show \bit k m \ bit k (nat k)\ by (auto simp add: * bit_iff_odd power_add zdiv_zmult2_eq dest!: le_Suc_ex) qed next case False moreover from power_gt_expt [of 2 \nat (- k)\] have \- k \ 2 ^ nat (- k)\ by simp ultimately have \- k div - (2 ^ nat (- k)) = - 1\ by (subst div_pos_neg_trivial) simp_all then have *: \k div 2 ^ nat (- k) = - 1\ by simp show thesis proof (rule that [of \nat (- k)\]) fix m assume \nat (- k) \ m\ then show \bit k m \ bit k (nat (- k))\ by (auto simp add: * bit_iff_odd power_add zdiv_zmult2_eq minus_1_div_exp_eq_int dest!: le_Suc_ex) qed qed show thesis proof (cases \\m. bit k m \ bit k q\) case True then have \bit k 0 \ bit k q\ by blast with True that [of 0] show thesis by simp next case False then obtain r where **: \bit k r \ bit k q\ by blast have \r < q\ by (rule ccontr) (use * [of r] ** in simp) define N where \N = {n. n < q \ bit k n \ bit k q}\ moreover have \finite N\ \r \ N\ using ** N_def \r < q\ by auto moreover define n where \n = Suc (Max N)\ ultimately have \\m. n \ m \ bit k m \ bit k n\ apply auto apply (metis (full_types, lifting) "*" Max_ge_iff Suc_n_not_le_n \finite N\ all_not_in_conv mem_Collect_eq not_le) apply (metis "*" Max_ge Suc_n_not_le_n \finite N\ linorder_not_less mem_Collect_eq) apply (metis "*" Max_ge Suc_n_not_le_n \finite N\ linorder_not_less mem_Collect_eq) apply (metis (full_types, lifting) "*" Max_ge_iff Suc_n_not_le_n \finite N\ all_not_in_conv mem_Collect_eq not_le) done have \bit k (Max N) \ bit k n\ by (metis (mono_tags, lifting) "*" Max_in N_def \\m. n \ m \ bit k m = bit k n\ \finite N\ \r \ N\ empty_iff le_cases mem_Collect_eq) show thesis apply (rule that [of n]) using \\m. n \ m \ bit k m = bit k n\ apply blast using \bit k (Max N) \ bit k n\ n_def by auto qed qed instantiation int :: ring_bit_operations begin definition not_int :: \int \ int\ where \not_int k = - k - 1\ lemma not_int_rec: "NOT k = of_bool (even k) + 2 * NOT (k div 2)" for k :: int by (auto simp add: not_int_def elim: oddE) lemma even_not_iff_int: \even (NOT k) \ odd k\ for k :: int by (simp add: not_int_def) lemma not_int_div_2: \NOT k div 2 = NOT (k div 2)\ for k :: int by (simp add: not_int_def) lemma bit_not_int_iff [bit_simps]: \bit (NOT k) n \ \ bit k n\ for k :: int by (simp add: bit_not_int_iff' not_int_def) function and_int :: \int \ int \ int\ where \(k::int) AND l = (if k \ {0, - 1} \ l \ {0, - 1} then - of_bool (odd k \ odd l) else of_bool (odd k \ odd l) + 2 * ((k div 2) AND (l div 2)))\ by auto termination by (relation \measure (\(k, l). nat (\k\ + \l\))\) auto declare and_int.simps [simp del] lemma and_int_rec: \k AND l = of_bool (odd k \ odd l) + 2 * ((k div 2) AND (l div 2))\ for k l :: int proof (cases \k \ {0, - 1} \ l \ {0, - 1}\) case True then show ?thesis by auto (simp_all add: and_int.simps) next case False then show ?thesis by (auto simp add: ac_simps and_int.simps [of k l]) qed lemma bit_and_int_iff: \bit (k AND l) n \ bit k n \ bit l n\ for k l :: int proof (induction n arbitrary: k l) case 0 then show ?case by (simp add: and_int_rec [of k l]) next case (Suc n) then show ?case by (simp add: and_int_rec [of k l] bit_Suc) qed lemma even_and_iff_int: \even (k AND l) \ even k \ even l\ for k l :: int using bit_and_int_iff [of k l 0] by auto definition or_int :: \int \ int \ int\ where \k OR l = NOT (NOT k AND NOT l)\ for k l :: int lemma or_int_rec: \k OR l = of_bool (odd k \ odd l) + 2 * ((k div 2) OR (l div 2))\ for k l :: int using and_int_rec [of \NOT k\ \NOT l\] by (simp add: or_int_def even_not_iff_int not_int_div_2) (simp_all add: not_int_def) lemma bit_or_int_iff: \bit (k OR l) n \ bit k n \ bit l n\ for k l :: int by (simp add: or_int_def bit_not_int_iff bit_and_int_iff) definition xor_int :: \int \ int \ int\ where \k XOR l = k AND NOT l OR NOT k AND l\ for k l :: int lemma xor_int_rec: \k XOR l = of_bool (odd k \ odd l) + 2 * ((k div 2) XOR (l div 2))\ for k l :: int by (simp add: xor_int_def or_int_rec [of \k AND NOT l\ \NOT k AND l\] even_and_iff_int even_not_iff_int) (simp add: and_int_rec [of \NOT k\ \l\] and_int_rec [of \k\ \NOT l\] not_int_div_2) lemma bit_xor_int_iff: \bit (k XOR l) n \ bit k n \ bit l n\ for k l :: int by (auto simp add: xor_int_def bit_or_int_iff bit_and_int_iff bit_not_int_iff) definition mask_int :: \nat \ int\ where \mask n = (2 :: int) ^ n - 1\ definition set_bit_int :: \nat \ int \ int\ where \set_bit n k = k OR push_bit n 1\ for k :: int definition unset_bit_int :: \nat \ int \ int\ where \unset_bit n k = k AND NOT (push_bit n 1)\ for k :: int definition flip_bit_int :: \nat \ int \ int\ where \flip_bit n k = k XOR push_bit n 1\ for k :: int instance proof fix k l :: int and m n :: nat show \- k = NOT (k - 1)\ by (simp add: not_int_def) show \bit (k AND l) n \ bit k n \ bit l n\ by (fact bit_and_int_iff) show \bit (k OR l) n \ bit k n \ bit l n\ by (fact bit_or_int_iff) show \bit (k XOR l) n \ bit k n \ bit l n\ by (fact bit_xor_int_iff) show \bit (unset_bit m k) n \ bit k n \ m \ n\ proof - have \unset_bit m k = k AND NOT (push_bit m 1)\ by (simp add: unset_bit_int_def) also have \NOT (push_bit m 1 :: int) = - (push_bit m 1 + 1)\ by (simp add: not_int_def) finally show ?thesis by (simp only: bit_simps bit_and_int_iff) (auto simp add: bit_simps) qed qed (simp_all add: bit_not_int_iff mask_int_def set_bit_int_def flip_bit_int_def) end lemma mask_half_int: \mask n div 2 = (mask (n - 1) :: int)\ by (cases n) (simp_all add: mask_eq_exp_minus_1 algebra_simps) lemma mask_nonnegative_int [simp]: \mask n \ (0::int)\ by (simp add: mask_eq_exp_minus_1) lemma not_mask_negative_int [simp]: \\ mask n < (0::int)\ by (simp add: not_less) lemma not_nonnegative_int_iff [simp]: \NOT k \ 0 \ k < 0\ for k :: int by (simp add: not_int_def) lemma not_negative_int_iff [simp]: \NOT k < 0 \ k \ 0\ for k :: int by (subst Not_eq_iff [symmetric]) (simp add: not_less not_le) lemma and_nonnegative_int_iff [simp]: \k AND l \ 0 \ k \ 0 \ l \ 0\ for k l :: int proof (induction k arbitrary: l rule: int_bit_induct) case zero then show ?case by simp next case minus then show ?case by simp next case (even k) then show ?case using and_int_rec [of \k * 2\ l] by (simp add: pos_imp_zdiv_nonneg_iff) next case (odd k) from odd have \0 \ k AND l div 2 \ 0 \ k \ 0 \ l div 2\ by simp then have \0 \ (1 + k * 2) div 2 AND l div 2 \ 0 \ (1 + k * 2) div 2\ 0 \ l div 2\ by simp with and_int_rec [of \1 + k * 2\ l] show ?case by auto qed lemma and_negative_int_iff [simp]: \k AND l < 0 \ k < 0 \ l < 0\ for k l :: int by (subst Not_eq_iff [symmetric]) (simp add: not_less) lemma and_less_eq: \k AND l \ k\ if \l < 0\ for k l :: int using that proof (induction k arbitrary: l rule: int_bit_induct) case zero then show ?case by simp next case minus then show ?case by simp next case (even k) from even.IH [of \l div 2\] even.hyps even.prems show ?case by (simp add: and_int_rec [of _ l]) next case (odd k) from odd.IH [of \l div 2\] odd.hyps odd.prems show ?case by (simp add: and_int_rec [of _ l]) qed lemma or_nonnegative_int_iff [simp]: \k OR l \ 0 \ k \ 0 \ l \ 0\ for k l :: int by (simp only: or_eq_not_not_and not_nonnegative_int_iff) simp lemma or_negative_int_iff [simp]: \k OR l < 0 \ k < 0 \ l < 0\ for k l :: int by (subst Not_eq_iff [symmetric]) (simp add: not_less) lemma or_greater_eq: \k OR l \ k\ if \l \ 0\ for k l :: int using that proof (induction k arbitrary: l rule: int_bit_induct) case zero then show ?case by simp next case minus then show ?case by simp next case (even k) from even.IH [of \l div 2\] even.hyps even.prems show ?case by (simp add: or_int_rec [of _ l]) next case (odd k) from odd.IH [of \l div 2\] odd.hyps odd.prems show ?case by (simp add: or_int_rec [of _ l]) qed lemma xor_nonnegative_int_iff [simp]: \k XOR l \ 0 \ (k \ 0 \ l \ 0)\ for k l :: int by (simp only: bit.xor_def or_nonnegative_int_iff) auto lemma xor_negative_int_iff [simp]: \k XOR l < 0 \ (k < 0) \ (l < 0)\ for k l :: int by (subst Not_eq_iff [symmetric]) (auto simp add: not_less) lemma OR_upper: \<^marker>\contributor \Stefan Berghofer\\ fixes x y :: int assumes "0 \ x" "x < 2 ^ n" "y < 2 ^ n" shows "x OR y < 2 ^ n" using assms proof (induction x arbitrary: y n rule: int_bit_induct) case zero then show ?case by simp next case minus then show ?case by simp next case (even x) from even.IH [of \n - 1\ \y div 2\] even.prems even.hyps show ?case by (cases n) (auto simp add: or_int_rec [of \_ * 2\] elim: oddE) next case (odd x) from odd.IH [of \n - 1\ \y div 2\] odd.prems odd.hyps show ?case by (cases n) (auto simp add: or_int_rec [of \1 + _ * 2\], linarith) qed lemma XOR_upper: \<^marker>\contributor \Stefan Berghofer\\ fixes x y :: int assumes "0 \ x" "x < 2 ^ n" "y < 2 ^ n" shows "x XOR y < 2 ^ n" using assms proof (induction x arbitrary: y n rule: int_bit_induct) case zero then show ?case by simp next case minus then show ?case by simp next case (even x) from even.IH [of \n - 1\ \y div 2\] even.prems even.hyps show ?case by (cases n) (auto simp add: xor_int_rec [of \_ * 2\] elim: oddE) next case (odd x) from odd.IH [of \n - 1\ \y div 2\] odd.prems odd.hyps show ?case by (cases n) (auto simp add: xor_int_rec [of \1 + _ * 2\]) qed lemma AND_lower [simp]: \<^marker>\contributor \Stefan Berghofer\\ fixes x y :: int assumes "0 \ x" shows "0 \ x AND y" using assms by simp lemma OR_lower [simp]: \<^marker>\contributor \Stefan Berghofer\\ fixes x y :: int assumes "0 \ x" "0 \ y" shows "0 \ x OR y" using assms by simp lemma XOR_lower [simp]: \<^marker>\contributor \Stefan Berghofer\\ fixes x y :: int assumes "0 \ x" "0 \ y" shows "0 \ x XOR y" using assms by simp lemma AND_upper1 [simp]: \<^marker>\contributor \Stefan Berghofer\\ fixes x y :: int assumes "0 \ x" shows "x AND y \ x" using assms proof (induction x arbitrary: y rule: int_bit_induct) case (odd k) then have \k AND y div 2 \ k\ by simp then show ?case by (simp add: and_int_rec [of \1 + _ * 2\]) qed (simp_all add: and_int_rec [of \_ * 2\]) lemmas AND_upper1' [simp] = order_trans [OF AND_upper1] \<^marker>\contributor \Stefan Berghofer\\ lemmas AND_upper1'' [simp] = order_le_less_trans [OF AND_upper1] \<^marker>\contributor \Stefan Berghofer\\ lemma AND_upper2 [simp]: \<^marker>\contributor \Stefan Berghofer\\ fixes x y :: int assumes "0 \ y" shows "x AND y \ y" using assms AND_upper1 [of y x] by (simp add: ac_simps) lemmas AND_upper2' [simp] = order_trans [OF AND_upper2] \<^marker>\contributor \Stefan Berghofer\\ lemmas AND_upper2'' [simp] = order_le_less_trans [OF AND_upper2] \<^marker>\contributor \Stefan Berghofer\\ lemma plus_and_or: \(x AND y) + (x OR y) = x + y\ for x y :: int proof (induction x arbitrary: y rule: int_bit_induct) case zero then show ?case by simp next case minus then show ?case by simp next case (even x) from even.IH [of \y div 2\] show ?case by (auto simp add: and_int_rec [of _ y] or_int_rec [of _ y] elim: oddE) next case (odd x) from odd.IH [of \y div 2\] show ?case by (auto simp add: and_int_rec [of _ y] or_int_rec [of _ y] elim: oddE) qed lemma set_bit_nonnegative_int_iff [simp]: \set_bit n k \ 0 \ k \ 0\ for k :: int by (simp add: set_bit_def) lemma set_bit_negative_int_iff [simp]: \set_bit n k < 0 \ k < 0\ for k :: int by (simp add: set_bit_def) lemma unset_bit_nonnegative_int_iff [simp]: \unset_bit n k \ 0 \ k \ 0\ for k :: int by (simp add: unset_bit_def) lemma unset_bit_negative_int_iff [simp]: \unset_bit n k < 0 \ k < 0\ for k :: int by (simp add: unset_bit_def) lemma flip_bit_nonnegative_int_iff [simp]: \flip_bit n k \ 0 \ k \ 0\ for k :: int by (simp add: flip_bit_def) lemma flip_bit_negative_int_iff [simp]: \flip_bit n k < 0 \ k < 0\ for k :: int by (simp add: flip_bit_def) lemma set_bit_greater_eq: \set_bit n k \ k\ for k :: int by (simp add: set_bit_def or_greater_eq) lemma unset_bit_less_eq: \unset_bit n k \ k\ for k :: int by (simp add: unset_bit_def and_less_eq) lemma set_bit_eq: \set_bit n k = k + of_bool (\ bit k n) * 2 ^ n\ for k :: int proof (rule bit_eqI) fix m show \bit (set_bit n k) m \ bit (k + of_bool (\ bit k n) * 2 ^ n) m\ proof (cases \m = n\) case True then show ?thesis apply (simp add: bit_set_bit_iff) apply (simp add: bit_iff_odd div_plus_div_distrib_dvd_right) done next case False then show ?thesis apply (clarsimp simp add: bit_set_bit_iff) apply (subst disjunctive_add) apply (clarsimp simp add: bit_exp_iff) apply (clarsimp simp add: bit_or_iff bit_exp_iff) done qed qed lemma unset_bit_eq: \unset_bit n k = k - of_bool (bit k n) * 2 ^ n\ for k :: int proof (rule bit_eqI) fix m show \bit (unset_bit n k) m \ bit (k - of_bool (bit k n) * 2 ^ n) m\ proof (cases \m = n\) case True then show ?thesis apply (simp add: bit_unset_bit_iff) apply (simp add: bit_iff_odd) using div_plus_div_distrib_dvd_right [of \2 ^ n\ \- (2 ^ n)\ k] apply (simp add: dvd_neg_div) done next case False then show ?thesis apply (clarsimp simp add: bit_unset_bit_iff) apply (subst disjunctive_diff) apply (clarsimp simp add: bit_exp_iff) apply (clarsimp simp add: bit_and_iff bit_not_iff bit_exp_iff) done qed qed lemma take_bit_eq_mask_iff: \take_bit n k = mask n \ take_bit n (k + 1) = 0\ (is \?P \ ?Q\) for k :: int proof assume ?P then have \take_bit n (take_bit n k + take_bit n 1) = 0\ by (simp add: mask_eq_exp_minus_1) then show ?Q by (simp only: take_bit_add) next assume ?Q then have \take_bit n (k + 1) - 1 = - 1\ by simp then have \take_bit n (take_bit n (k + 1) - 1) = take_bit n (- 1)\ by simp moreover have \take_bit n (take_bit n (k + 1) - 1) = take_bit n k\ by (simp add: take_bit_eq_mod mod_simps) ultimately show ?P by (simp add: take_bit_minus_one_eq_mask) qed lemma take_bit_eq_mask_iff_exp_dvd: \take_bit n k = mask n \ 2 ^ n dvd k + 1\ for k :: int by (simp add: take_bit_eq_mask_iff flip: take_bit_eq_0_iff) context ring_bit_operations begin lemma even_of_int_iff: \even (of_int k) \ even k\ by (induction k rule: int_bit_induct) simp_all lemma bit_of_int_iff [bit_simps]: \bit (of_int k) n \ (2::'a) ^ n \ 0 \ bit k n\ proof (cases \(2::'a) ^ n = 0\) case True then show ?thesis by (simp add: exp_eq_0_imp_not_bit) next case False then have \bit (of_int k) n \ bit k n\ proof (induction k arbitrary: n rule: int_bit_induct) case zero then show ?case by simp next case minus then show ?case by simp next case (even k) then show ?case using bit_double_iff [of \of_int k\ n] Parity.bit_double_iff [of k n] by (cases n) (auto simp add: ac_simps dest: mult_not_zero) next case (odd k) then show ?case using bit_double_iff [of \of_int k\ n] by (cases n) (auto simp add: ac_simps bit_double_iff even_bit_succ_iff Parity.bit_Suc dest: mult_not_zero) qed with False show ?thesis by simp qed lemma push_bit_of_int: \push_bit n (of_int k) = of_int (push_bit n k)\ by (simp add: push_bit_eq_mult semiring_bit_shifts_class.push_bit_eq_mult) lemma of_int_push_bit: \of_int (push_bit n k) = push_bit n (of_int k)\ by (simp add: push_bit_eq_mult semiring_bit_shifts_class.push_bit_eq_mult) lemma take_bit_of_int: \take_bit n (of_int k) = of_int (take_bit n k)\ by (rule bit_eqI) (simp add: bit_take_bit_iff Parity.bit_take_bit_iff bit_of_int_iff) lemma of_int_take_bit: \of_int (take_bit n k) = take_bit n (of_int k)\ by (rule bit_eqI) (simp add: bit_take_bit_iff Parity.bit_take_bit_iff bit_of_int_iff) lemma of_int_not_eq: \of_int (NOT k) = NOT (of_int k)\ by (rule bit_eqI) (simp add: bit_not_iff Bit_Operations.bit_not_iff bit_of_int_iff) lemma of_int_and_eq: \of_int (k AND l) = of_int k AND of_int l\ by (rule bit_eqI) (simp add: bit_of_int_iff bit_and_iff Bit_Operations.bit_and_iff) lemma of_int_or_eq: \of_int (k OR l) = of_int k OR of_int l\ by (rule bit_eqI) (simp add: bit_of_int_iff bit_or_iff Bit_Operations.bit_or_iff) lemma of_int_xor_eq: \of_int (k XOR l) = of_int k XOR of_int l\ by (rule bit_eqI) (simp add: bit_of_int_iff bit_xor_iff Bit_Operations.bit_xor_iff) lemma of_int_mask_eq: \of_int (mask n) = mask n\ by (induction n) (simp_all add: mask_Suc_double Bit_Operations.mask_Suc_double of_int_or_eq) end text \FIXME: The rule sets below are very large (24 rules for each operator). Is there a simpler way to do this?\ context begin private lemma eqI: \k = l\ if num: \\n. bit k (numeral n) \ bit l (numeral n)\ and even: \even k \ even l\ for k l :: int proof (rule bit_eqI) fix n show \bit k n \ bit l n\ proof (cases n) case 0 with even show ?thesis by simp next case (Suc n) with num [of \num_of_nat (Suc n)\] show ?thesis by (simp only: numeral_num_of_nat) qed qed lemma int_and_numerals [simp]: "numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND numeral y)" "numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (2 :: int) * (numeral x AND numeral y)" "numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND numeral y)" "numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x AND numeral y)" "numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND - numeral y)" "numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (2 :: int) * (numeral x AND - numeral (y + Num.One))" "numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND - numeral y)" "numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x AND - numeral (y + Num.One))" "- numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (2 :: int) * (- numeral x AND numeral y)" "- numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (2 :: int) * (- numeral x AND numeral y)" "- numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (2 :: int) * (- numeral (x + Num.One) AND numeral y)" "- numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) AND numeral y)" "- numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x AND - numeral y)" "- numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (2 :: int) * (- numeral x AND - numeral (y + Num.One))" "- numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (- numeral (x + Num.One) AND - numeral y)" "- numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) AND - numeral (y + Num.One))" "(1::int) AND numeral (Num.Bit0 y) = 0" "(1::int) AND numeral (Num.Bit1 y) = 1" "(1::int) AND - numeral (Num.Bit0 y) = 0" "(1::int) AND - numeral (Num.Bit1 y) = 1" "numeral (Num.Bit0 x) AND (1::int) = 0" "numeral (Num.Bit1 x) AND (1::int) = 1" "- numeral (Num.Bit0 x) AND (1::int) = 0" "- numeral (Num.Bit1 x) AND (1::int) = 1" by (auto simp add: bit_and_iff bit_minus_iff even_and_iff bit_double_iff even_bit_succ_iff add_One sub_inc_One_eq intro: eqI) lemma int_or_numerals [simp]: "numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (2 :: int) * (numeral x OR numeral y)" "numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR numeral y)" "numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x OR numeral y)" "numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR numeral y)" "numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (2 :: int) * (numeral x OR - numeral y)" "numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR - numeral (y + Num.One))" "numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x OR - numeral y)" "numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR - numeral (y + Num.One))" "- numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (2 :: int) * (- numeral x OR numeral y)" "- numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x OR numeral y)" "- numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR numeral y)" "- numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR numeral y)" "- numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x OR - numeral y)" "- numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x OR - numeral (y + Num.One))" "- numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR - numeral y)" "- numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR - numeral (y + Num.One))" "(1::int) OR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)" "(1::int) OR numeral (Num.Bit1 y) = numeral (Num.Bit1 y)" "(1::int) OR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)" "(1::int) OR - numeral (Num.Bit1 y) = - numeral (Num.Bit1 y)" "numeral (Num.Bit0 x) OR (1::int) = numeral (Num.Bit1 x)" "numeral (Num.Bit1 x) OR (1::int) = numeral (Num.Bit1 x)" "- numeral (Num.Bit0 x) OR (1::int) = - numeral (Num.BitM x)" "- numeral (Num.Bit1 x) OR (1::int) = - numeral (Num.Bit1 x)" by (auto simp add: bit_or_iff bit_minus_iff even_or_iff bit_double_iff even_bit_succ_iff add_One sub_inc_One_eq sub_BitM_One_eq intro: eqI) lemma int_xor_numerals [simp]: "numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (2 :: int) * (numeral x XOR numeral y)" "numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x XOR numeral y)" "numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x XOR numeral y)" "numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (2 :: int) * (numeral x XOR numeral y)" "numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (2 :: int) * (numeral x XOR - numeral y)" "numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x XOR - numeral (y + Num.One))" "numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x XOR - numeral y)" "numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (2 :: int) * (numeral x XOR - numeral (y + Num.One))" "- numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (2 :: int) * (- numeral x XOR numeral y)" "- numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x XOR numeral y)" "- numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) XOR numeral y)" "- numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (2 :: int) * (- numeral (x + Num.One) XOR numeral y)" "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x XOR - numeral y)" "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x XOR - numeral (y + Num.One))" "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) XOR - numeral y)" "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (2 :: int) * (- numeral (x + Num.One) XOR - numeral (y + Num.One))" "(1::int) XOR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)" "(1::int) XOR numeral (Num.Bit1 y) = numeral (Num.Bit0 y)" "(1::int) XOR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)" "(1::int) XOR - numeral (Num.Bit1 y) = - numeral (Num.Bit0 (y + Num.One))" "numeral (Num.Bit0 x) XOR (1::int) = numeral (Num.Bit1 x)" "numeral (Num.Bit1 x) XOR (1::int) = numeral (Num.Bit0 x)" "- numeral (Num.Bit0 x) XOR (1::int) = - numeral (Num.BitM x)" "- numeral (Num.Bit1 x) XOR (1::int) = - numeral (Num.Bit0 (x + Num.One))" by (auto simp add: bit_xor_iff bit_minus_iff even_xor_iff bit_double_iff even_bit_succ_iff add_One sub_inc_One_eq sub_BitM_One_eq intro: eqI) end subsection \Bit concatenation\ definition concat_bit :: \nat \ int \ int \ int\ where \concat_bit n k l = take_bit n k OR push_bit n l\ lemma bit_concat_bit_iff [bit_simps]: \bit (concat_bit m k l) n \ n < m \ bit k n \ m \ n \ bit l (n - m)\ by (simp add: concat_bit_def bit_or_iff bit_and_iff bit_take_bit_iff bit_push_bit_iff ac_simps) lemma concat_bit_eq: \concat_bit n k l = take_bit n k + push_bit n l\ by (simp add: concat_bit_def take_bit_eq_mask bit_and_iff bit_mask_iff bit_push_bit_iff disjunctive_add) lemma concat_bit_0 [simp]: \concat_bit 0 k l = l\ by (simp add: concat_bit_def) lemma concat_bit_Suc: \concat_bit (Suc n) k l = k mod 2 + 2 * concat_bit n (k div 2) l\ by (simp add: concat_bit_eq take_bit_Suc push_bit_double) lemma concat_bit_of_zero_1 [simp]: \concat_bit n 0 l = push_bit n l\ by (simp add: concat_bit_def) lemma concat_bit_of_zero_2 [simp]: \concat_bit n k 0 = take_bit n k\ by (simp add: concat_bit_def take_bit_eq_mask) lemma concat_bit_nonnegative_iff [simp]: \concat_bit n k l \ 0 \ l \ 0\ by (simp add: concat_bit_def) lemma concat_bit_negative_iff [simp]: \concat_bit n k l < 0 \ l < 0\ by (simp add: concat_bit_def) lemma concat_bit_assoc: \concat_bit n k (concat_bit m l r) = concat_bit (m + n) (concat_bit n k l) r\ by (rule bit_eqI) (auto simp add: bit_concat_bit_iff ac_simps) lemma concat_bit_assoc_sym: \concat_bit m (concat_bit n k l) r = concat_bit (min m n) k (concat_bit (m - n) l r)\ by (rule bit_eqI) (auto simp add: bit_concat_bit_iff ac_simps min_def) lemma concat_bit_eq_iff: \concat_bit n k l = concat_bit n r s \ take_bit n k = take_bit n r \ l = s\ (is \?P \ ?Q\) proof assume ?Q then show ?P by (simp add: concat_bit_def) next assume ?P then have *: \bit (concat_bit n k l) m = bit (concat_bit n r s) m\ for m by (simp add: bit_eq_iff) have \take_bit n k = take_bit n r\ proof (rule bit_eqI) fix m from * [of m] show \bit (take_bit n k) m \ bit (take_bit n r) m\ by (auto simp add: bit_take_bit_iff bit_concat_bit_iff) qed moreover have \push_bit n l = push_bit n s\ proof (rule bit_eqI) fix m from * [of m] show \bit (push_bit n l) m \ bit (push_bit n s) m\ by (auto simp add: bit_push_bit_iff bit_concat_bit_iff) qed then have \l = s\ by (simp add: push_bit_eq_mult) ultimately show ?Q by (simp add: concat_bit_def) qed lemma take_bit_concat_bit_eq: \take_bit m (concat_bit n k l) = concat_bit (min m n) k (take_bit (m - n) l)\ by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_concat_bit_iff min_def) lemma concat_bit_take_bit_eq: \concat_bit n (take_bit n b) = concat_bit n b\ by (simp add: concat_bit_def [abs_def]) subsection \Taking bits with sign propagation\ context ring_bit_operations begin definition signed_take_bit :: \nat \ 'a \ 'a\ where \signed_take_bit n a = take_bit n a OR (of_bool (bit a n) * NOT (mask n))\ lemma signed_take_bit_eq_if_positive: \signed_take_bit n a = take_bit n a\ if \\ bit a n\ using that by (simp add: signed_take_bit_def) lemma signed_take_bit_eq_if_negative: \signed_take_bit n a = take_bit n a OR NOT (mask n)\ if \bit a n\ using that by (simp add: signed_take_bit_def) lemma even_signed_take_bit_iff: \even (signed_take_bit m a) \ even a\ by (auto simp add: signed_take_bit_def even_or_iff even_mask_iff bit_double_iff) lemma bit_signed_take_bit_iff [bit_simps]: \bit (signed_take_bit m a) n \ 2 ^ n \ 0 \ bit a (min m n)\ by (simp add: signed_take_bit_def bit_take_bit_iff bit_or_iff bit_not_iff bit_mask_iff min_def not_le) (use exp_eq_0_imp_not_bit in blast) lemma signed_take_bit_0 [simp]: \signed_take_bit 0 a = - (a mod 2)\ by (simp add: signed_take_bit_def odd_iff_mod_2_eq_one) lemma signed_take_bit_Suc: \signed_take_bit (Suc n) a = a mod 2 + 2 * signed_take_bit n (a div 2)\ proof (rule bit_eqI) fix m assume *: \2 ^ m \ 0\ show \bit (signed_take_bit (Suc n) a) m \ bit (a mod 2 + 2 * signed_take_bit n (a div 2)) m\ proof (cases m) case 0 then show ?thesis by (simp add: even_signed_take_bit_iff) next case (Suc m) with * have \2 ^ m \ 0\ by (metis mult_not_zero power_Suc) with Suc show ?thesis by (simp add: bit_signed_take_bit_iff mod2_eq_if bit_double_iff even_bit_succ_iff ac_simps flip: bit_Suc) qed qed lemma signed_take_bit_of_0 [simp]: \signed_take_bit n 0 = 0\ by (simp add: signed_take_bit_def) lemma signed_take_bit_of_minus_1 [simp]: \signed_take_bit n (- 1) = - 1\ by (simp add: signed_take_bit_def take_bit_minus_one_eq_mask mask_eq_exp_minus_1) lemma signed_take_bit_Suc_1 [simp]: \signed_take_bit (Suc n) 1 = 1\ by (simp add: signed_take_bit_Suc) lemma signed_take_bit_rec: \signed_take_bit n a = (if n = 0 then - (a mod 2) else a mod 2 + 2 * signed_take_bit (n - 1) (a div 2))\ by (cases n) (simp_all add: signed_take_bit_Suc) lemma signed_take_bit_eq_iff_take_bit_eq: \signed_take_bit n a = signed_take_bit n b \ take_bit (Suc n) a = take_bit (Suc n) b\ proof - have \bit (signed_take_bit n a) = bit (signed_take_bit n b) \ bit (take_bit (Suc n) a) = bit (take_bit (Suc n) b)\ by (simp add: fun_eq_iff bit_signed_take_bit_iff bit_take_bit_iff not_le less_Suc_eq_le min_def) (use exp_eq_0_imp_not_bit in fastforce) then show ?thesis by (simp add: bit_eq_iff fun_eq_iff) qed lemma signed_take_bit_signed_take_bit [simp]: \signed_take_bit m (signed_take_bit n a) = signed_take_bit (min m n) a\ proof (rule bit_eqI) fix q show \bit (signed_take_bit m (signed_take_bit n a)) q \ bit (signed_take_bit (min m n) a) q\ by (simp add: bit_signed_take_bit_iff min_def bit_or_iff bit_not_iff bit_mask_iff bit_take_bit_iff) (use le_Suc_ex exp_add_not_zero_imp in blast) qed lemma signed_take_bit_take_bit: \signed_take_bit m (take_bit n a) = (if n \ m then take_bit n else signed_take_bit m) a\ by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_take_bit_iff) lemma take_bit_signed_take_bit: \take_bit m (signed_take_bit n a) = take_bit m a\ if \m \ Suc n\ using that by (rule le_SucE; intro bit_eqI) (auto simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def less_Suc_eq) end text \Modulus centered around 0\ lemma signed_take_bit_eq_concat_bit: \signed_take_bit n k = concat_bit n k (- of_bool (bit k n))\ by (simp add: concat_bit_def signed_take_bit_def push_bit_minus_one_eq_not_mask) lemma signed_take_bit_add: \signed_take_bit n (signed_take_bit n k + signed_take_bit n l) = signed_take_bit n (k + l)\ for k l :: int proof - have \take_bit (Suc n) (take_bit (Suc n) (signed_take_bit n k) + take_bit (Suc n) (signed_take_bit n l)) = take_bit (Suc n) (k + l)\ by (simp add: take_bit_signed_take_bit take_bit_add) then show ?thesis by (simp only: signed_take_bit_eq_iff_take_bit_eq take_bit_add) qed lemma signed_take_bit_diff: \signed_take_bit n (signed_take_bit n k - signed_take_bit n l) = signed_take_bit n (k - l)\ for k l :: int proof - have \take_bit (Suc n) (take_bit (Suc n) (signed_take_bit n k) - take_bit (Suc n) (signed_take_bit n l)) = take_bit (Suc n) (k - l)\ by (simp add: take_bit_signed_take_bit take_bit_diff) then show ?thesis by (simp only: signed_take_bit_eq_iff_take_bit_eq take_bit_diff) qed lemma signed_take_bit_minus: \signed_take_bit n (- signed_take_bit n k) = signed_take_bit n (- k)\ for k :: int proof - have \take_bit (Suc n) (- take_bit (Suc n) (signed_take_bit n k)) = take_bit (Suc n) (- k)\ by (simp add: take_bit_signed_take_bit take_bit_minus) then show ?thesis by (simp only: signed_take_bit_eq_iff_take_bit_eq take_bit_minus) qed lemma signed_take_bit_mult: \signed_take_bit n (signed_take_bit n k * signed_take_bit n l) = signed_take_bit n (k * l)\ for k l :: int proof - have \take_bit (Suc n) (take_bit (Suc n) (signed_take_bit n k) * take_bit (Suc n) (signed_take_bit n l)) = take_bit (Suc n) (k * l)\ by (simp add: take_bit_signed_take_bit take_bit_mult) then show ?thesis by (simp only: signed_take_bit_eq_iff_take_bit_eq take_bit_mult) qed lemma signed_take_bit_eq_take_bit_minus: \signed_take_bit n k = take_bit (Suc n) k - 2 ^ Suc n * of_bool (bit k n)\ for k :: int proof (cases \bit k n\) case True have \signed_take_bit n k = take_bit (Suc n) k OR NOT (mask (Suc n))\ by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_take_bit_iff bit_or_iff bit_not_iff bit_mask_iff less_Suc_eq True) then have \signed_take_bit n k = take_bit (Suc n) k + NOT (mask (Suc n))\ by (simp add: disjunctive_add bit_take_bit_iff bit_not_iff bit_mask_iff) with True show ?thesis by (simp flip: minus_exp_eq_not_mask) next case False show ?thesis by (rule bit_eqI) (simp add: False bit_signed_take_bit_iff bit_take_bit_iff min_def less_Suc_eq) qed lemma signed_take_bit_eq_take_bit_shift: \signed_take_bit n k = take_bit (Suc n) (k + 2 ^ n) - 2 ^ n\ for k :: int proof - have *: \take_bit n k OR 2 ^ n = take_bit n k + 2 ^ n\ by (simp add: disjunctive_add bit_exp_iff bit_take_bit_iff) have \take_bit n k - 2 ^ n = take_bit n k + NOT (mask n)\ by (simp add: minus_exp_eq_not_mask) also have \\ = take_bit n k OR NOT (mask n)\ by (rule disjunctive_add) (simp add: bit_exp_iff bit_take_bit_iff bit_not_iff bit_mask_iff) finally have **: \take_bit n k - 2 ^ n = take_bit n k OR NOT (mask n)\ . have \take_bit (Suc n) (k + 2 ^ n) = take_bit (Suc n) (take_bit (Suc n) k + take_bit (Suc n) (2 ^ n))\ by (simp only: take_bit_add) also have \take_bit (Suc n) k = 2 ^ n * of_bool (bit k n) + take_bit n k\ by (simp add: take_bit_Suc_from_most) finally have \take_bit (Suc n) (k + 2 ^ n) = take_bit (Suc n) (2 ^ (n + of_bool (bit k n)) + take_bit n k)\ by (simp add: ac_simps) also have \2 ^ (n + of_bool (bit k n)) + take_bit n k = 2 ^ (n + of_bool (bit k n)) OR take_bit n k\ by (rule disjunctive_add) (auto simp add: disjunctive_add bit_take_bit_iff bit_double_iff bit_exp_iff) finally show ?thesis using * ** by (simp add: signed_take_bit_def concat_bit_Suc min_def ac_simps) qed lemma signed_take_bit_nonnegative_iff [simp]: \0 \ signed_take_bit n k \ \ bit k n\ for k :: int by (simp add: signed_take_bit_def not_less concat_bit_def) lemma signed_take_bit_negative_iff [simp]: \signed_take_bit n k < 0 \ bit k n\ for k :: int by (simp add: signed_take_bit_def not_less concat_bit_def) lemma signed_take_bit_int_eq_self_iff: \signed_take_bit n k = k \ - (2 ^ n) \ k \ k < 2 ^ n\ for k :: int by (auto simp add: signed_take_bit_eq_take_bit_shift take_bit_int_eq_self_iff algebra_simps) lemma signed_take_bit_int_eq_self: \signed_take_bit n k = k\ if \- (2 ^ n) \ k\ \k < 2 ^ n\ for k :: int using that by (simp add: signed_take_bit_int_eq_self_iff) lemma signed_take_bit_int_less_eq_self_iff: \signed_take_bit n k \ k \ - (2 ^ n) \ k\ for k :: int by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_less_eq_self_iff algebra_simps) linarith lemma signed_take_bit_int_less_self_iff: \signed_take_bit n k < k \ 2 ^ n \ k\ for k :: int by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_less_self_iff algebra_simps) lemma signed_take_bit_int_greater_self_iff: \k < signed_take_bit n k \ k < - (2 ^ n)\ for k :: int by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_greater_self_iff algebra_simps) linarith lemma signed_take_bit_int_greater_eq_self_iff: \k \ signed_take_bit n k \ k < 2 ^ n\ for k :: int by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_greater_eq_self_iff algebra_simps) lemma signed_take_bit_int_greater_eq: \k + 2 ^ Suc n \ signed_take_bit n k\ if \k < - (2 ^ n)\ for k :: int using that take_bit_int_greater_eq [of \k + 2 ^ n\ \Suc n\] by (simp add: signed_take_bit_eq_take_bit_shift) lemma signed_take_bit_int_less_eq: \signed_take_bit n k \ k - 2 ^ Suc n\ if \k \ 2 ^ n\ for k :: int using that take_bit_int_less_eq [of \Suc n\ \k + 2 ^ n\] by (simp add: signed_take_bit_eq_take_bit_shift) lemma signed_take_bit_Suc_bit0 [simp]: \signed_take_bit (Suc n) (numeral (Num.Bit0 k)) = signed_take_bit n (numeral k) * (2 :: int)\ by (simp add: signed_take_bit_Suc) lemma signed_take_bit_Suc_bit1 [simp]: \signed_take_bit (Suc n) (numeral (Num.Bit1 k)) = signed_take_bit n (numeral k) * 2 + (1 :: int)\ by (simp add: signed_take_bit_Suc) lemma signed_take_bit_Suc_minus_bit0 [simp]: \signed_take_bit (Suc n) (- numeral (Num.Bit0 k)) = signed_take_bit n (- numeral k) * (2 :: int)\ by (simp add: signed_take_bit_Suc) lemma signed_take_bit_Suc_minus_bit1 [simp]: \signed_take_bit (Suc n) (- numeral (Num.Bit1 k)) = signed_take_bit n (- numeral k - 1) * 2 + (1 :: int)\ by (simp add: signed_take_bit_Suc) lemma signed_take_bit_numeral_bit0 [simp]: \signed_take_bit (numeral l) (numeral (Num.Bit0 k)) = signed_take_bit (pred_numeral l) (numeral k) * (2 :: int)\ by (simp add: signed_take_bit_rec) lemma signed_take_bit_numeral_bit1 [simp]: \signed_take_bit (numeral l) (numeral (Num.Bit1 k)) = signed_take_bit (pred_numeral l) (numeral k) * 2 + (1 :: int)\ by (simp add: signed_take_bit_rec) lemma signed_take_bit_numeral_minus_bit0 [simp]: \signed_take_bit (numeral l) (- numeral (Num.Bit0 k)) = signed_take_bit (pred_numeral l) (- numeral k) * (2 :: int)\ by (simp add: signed_take_bit_rec) lemma signed_take_bit_numeral_minus_bit1 [simp]: \signed_take_bit (numeral l) (- numeral (Num.Bit1 k)) = signed_take_bit (pred_numeral l) (- numeral k - 1) * 2 + (1 :: int)\ by (simp add: signed_take_bit_rec) lemma signed_take_bit_code [code]: \signed_take_bit n a = (let l = take_bit (Suc n) a in if bit l n then l + push_bit (Suc n) (- 1) else l)\ proof - have *: \take_bit (Suc n) a + push_bit n (- 2) = take_bit (Suc n) a OR NOT (mask (Suc n))\ by (auto simp add: bit_take_bit_iff bit_push_bit_iff bit_not_iff bit_mask_iff disjunctive_add simp flip: push_bit_minus_one_eq_not_mask) show ?thesis by (rule bit_eqI) (auto simp add: Let_def * bit_signed_take_bit_iff bit_take_bit_iff min_def less_Suc_eq bit_not_iff bit_mask_iff bit_or_iff) qed lemma not_minus_numeral_inc_eq: \NOT (- numeral (Num.inc n)) = (numeral n :: int)\ by (simp add: not_int_def sub_inc_One_eq) subsection \Instance \<^typ>\nat\\ instantiation nat :: semiring_bit_operations begin definition and_nat :: \nat \ nat \ nat\ where \m AND n = nat (int m AND int n)\ for m n :: nat definition or_nat :: \nat \ nat \ nat\ where \m OR n = nat (int m OR int n)\ for m n :: nat definition xor_nat :: \nat \ nat \ nat\ where \m XOR n = nat (int m XOR int n)\ for m n :: nat definition mask_nat :: \nat \ nat\ where \mask n = (2 :: nat) ^ n - 1\ definition set_bit_nat :: \nat \ nat \ nat\ where \set_bit m n = n OR push_bit m 1\ for m n :: nat definition unset_bit_nat :: \nat \ nat \ nat\ where \unset_bit m n = (if bit n m then n - push_bit m 1 else n)\ for m n :: nat definition flip_bit_nat :: \nat \ nat \ nat\ where \flip_bit m n = n XOR push_bit m 1\ for m n :: nat instance proof fix m n q :: nat show \bit (m AND n) q \ bit m q \ bit n q\ by (simp add: and_nat_def bit_simps) show \bit (m OR n) q \ bit m q \ bit n q\ by (simp add: or_nat_def bit_simps) show \bit (m XOR n) q \ bit m q \ bit n q\ by (simp add: xor_nat_def bit_simps) show \bit (unset_bit m n) q \ bit n q \ m \ q\ proof (cases \bit n m\) case False then show ?thesis by (auto simp add: unset_bit_nat_def) next case True have \push_bit m (drop_bit m n) + take_bit m n = n\ by (fact bits_ident) also from \bit n m\ have \drop_bit m n = 2 * drop_bit (Suc m) n + 1\ by (simp add: drop_bit_Suc drop_bit_half even_drop_bit_iff_not_bit ac_simps) finally have \push_bit m (2 * drop_bit (Suc m) n) + take_bit m n + push_bit m 1 = n\ by (simp only: push_bit_add ac_simps) then have \n - push_bit m 1 = push_bit m (2 * drop_bit (Suc m) n) + take_bit m n\ by simp then have \n - push_bit m 1 = push_bit m (2 * drop_bit (Suc m) n) OR take_bit m n\ by (simp add: or_nat_def bit_simps flip: disjunctive_add) with \bit n m\ show ?thesis by (auto simp add: unset_bit_nat_def or_nat_def bit_simps) qed qed (simp_all add: mask_nat_def set_bit_nat_def flip_bit_nat_def) end lemma and_nat_rec: \m AND n = of_bool (odd m \ odd n) + 2 * ((m div 2) AND (n div 2))\ for m n :: nat by (simp add: and_nat_def and_int_rec [of \int m\ \int n\] zdiv_int nat_add_distrib nat_mult_distrib) lemma or_nat_rec: \m OR n = of_bool (odd m \ odd n) + 2 * ((m div 2) OR (n div 2))\ for m n :: nat by (simp add: or_nat_def or_int_rec [of \int m\ \int n\] zdiv_int nat_add_distrib nat_mult_distrib) lemma xor_nat_rec: \m XOR n = of_bool (odd m \ odd n) + 2 * ((m div 2) XOR (n div 2))\ for m n :: nat by (simp add: xor_nat_def xor_int_rec [of \int m\ \int n\] zdiv_int nat_add_distrib nat_mult_distrib) lemma Suc_0_and_eq [simp]: \Suc 0 AND n = n mod 2\ using one_and_eq [of n] by simp lemma and_Suc_0_eq [simp]: \n AND Suc 0 = n mod 2\ using and_one_eq [of n] by simp lemma Suc_0_or_eq: \Suc 0 OR n = n + of_bool (even n)\ using one_or_eq [of n] by simp lemma or_Suc_0_eq: \n OR Suc 0 = n + of_bool (even n)\ using or_one_eq [of n] by simp lemma Suc_0_xor_eq: \Suc 0 XOR n = n + of_bool (even n) - of_bool (odd n)\ using one_xor_eq [of n] by simp lemma xor_Suc_0_eq: \n XOR Suc 0 = n + of_bool (even n) - of_bool (odd n)\ using xor_one_eq [of n] by simp context semiring_bit_operations begin lemma of_nat_and_eq: \of_nat (m AND n) = of_nat m AND of_nat n\ by (rule bit_eqI) (simp add: bit_of_nat_iff bit_and_iff Bit_Operations.bit_and_iff) lemma of_nat_or_eq: \of_nat (m OR n) = of_nat m OR of_nat n\ by (rule bit_eqI) (simp add: bit_of_nat_iff bit_or_iff Bit_Operations.bit_or_iff) lemma of_nat_xor_eq: \of_nat (m XOR n) = of_nat m XOR of_nat n\ by (rule bit_eqI) (simp add: bit_of_nat_iff bit_xor_iff Bit_Operations.bit_xor_iff) end context ring_bit_operations begin lemma of_nat_mask_eq: \of_nat (mask n) = mask n\ by (induction n) (simp_all add: mask_Suc_double Bit_Operations.mask_Suc_double of_nat_or_eq) end lemma Suc_mask_eq_exp: \Suc (mask n) = 2 ^ n\ by (simp add: mask_eq_exp_minus_1) lemma less_eq_mask: \n \ mask n\ by (simp add: mask_eq_exp_minus_1 le_diff_conv2) (metis Suc_mask_eq_exp diff_Suc_1 diff_le_diff_pow diff_zero le_refl not_less_eq_eq power_0) lemma less_mask: \n < mask n\ if \Suc 0 < n\ proof - define m where \m = n - 2\ with that have *: \n = m + 2\ by simp have \Suc (Suc (Suc m)) < 4 * 2 ^ m\ by (induction m) simp_all then have \Suc (m + 2) < Suc (mask (m + 2))\ by (simp add: Suc_mask_eq_exp) then have \m + 2 < mask (m + 2)\ by (simp add: less_le) with * show ?thesis by simp qed subsection \Instances for \<^typ>\integer\ and \<^typ>\natural\\ unbundle integer.lifting natural.lifting instantiation integer :: ring_bit_operations begin lift_definition not_integer :: \integer \ integer\ is not . lift_definition and_integer :: \integer \ integer \ integer\ is \and\ . lift_definition or_integer :: \integer \ integer \ integer\ is or . lift_definition xor_integer :: \integer \ integer \ integer\ is xor . lift_definition mask_integer :: \nat \ integer\ is mask . lift_definition set_bit_integer :: \nat \ integer \ integer\ is set_bit . lift_definition unset_bit_integer :: \nat \ integer \ integer\ is unset_bit . lift_definition flip_bit_integer :: \nat \ integer \ integer\ is flip_bit . instance by (standard; transfer) (simp_all add: minus_eq_not_minus_1 mask_eq_exp_minus_1 bit_not_iff bit_and_iff bit_or_iff bit_xor_iff set_bit_def bit_unset_bit_iff flip_bit_def) end lemma [code]: \mask n = 2 ^ n - (1::integer)\ by (simp add: mask_eq_exp_minus_1) instantiation natural :: semiring_bit_operations begin lift_definition and_natural :: \natural \ natural \ natural\ is \and\ . lift_definition or_natural :: \natural \ natural \ natural\ is or . lift_definition xor_natural :: \natural \ natural \ natural\ is xor . lift_definition mask_natural :: \nat \ natural\ is mask . lift_definition set_bit_natural :: \nat \ natural \ natural\ is set_bit . lift_definition unset_bit_natural :: \nat \ natural \ natural\ is unset_bit . lift_definition flip_bit_natural :: \nat \ natural \ natural\ is flip_bit . instance by (standard; transfer) (simp_all add: mask_eq_exp_minus_1 bit_and_iff bit_or_iff bit_xor_iff set_bit_def bit_unset_bit_iff flip_bit_def) end lemma [code]: \integer_of_natural (mask n) = mask n\ by transfer (simp add: mask_eq_exp_minus_1 of_nat_diff) lifting_update integer.lifting lifting_forget integer.lifting lifting_update natural.lifting lifting_forget natural.lifting subsection \Key ideas of bit operations\ text \ When formalizing bit operations, it is tempting to represent bit values as explicit lists over a binary type. This however is a bad idea, mainly due to the inherent ambiguities in representation concerning repeating leading bits. Hence this approach avoids such explicit lists altogether following an algebraic path: \<^item> Bit values are represented by numeric types: idealized unbounded bit values can be represented by type \<^typ>\int\, bounded bit values by quotient types over \<^typ>\int\. \<^item> (A special case are idealized unbounded bit values ending in @{term [source] 0} which can be represented by type \<^typ>\nat\ but only support a restricted set of operations). \<^item> From this idea follows that \<^item> multiplication by \<^term>\2 :: int\ is a bit shift to the left and \<^item> division by \<^term>\2 :: int\ is a bit shift to the right. \<^item> Concerning bounded bit values, iterated shifts to the left may result in eliminating all bits by shifting them all beyond the boundary. The property \<^prop>\(2 :: int) ^ n \ 0\ represents that \<^term>\n\ is \<^emph>\not\ beyond that boundary. \<^item> The projection on a single bit is then @{thm bit_iff_odd [where ?'a = int, no_vars]}. \<^item> This leads to the most fundamental properties of bit values: \<^item> Equality rule: @{thm bit_eqI [where ?'a = int, no_vars]} \<^item> Induction rule: @{thm bits_induct [where ?'a = int, no_vars]} \<^item> Typical operations are characterized as follows: \<^item> Singleton \<^term>\n\th bit: \<^term>\(2 :: int) ^ n\ \<^item> Bit mask upto bit \<^term>\n\: @{thm mask_eq_exp_minus_1 [where ?'a = int, no_vars]} \<^item> Left shift: @{thm push_bit_eq_mult [where ?'a = int, no_vars]} \<^item> Right shift: @{thm drop_bit_eq_div [where ?'a = int, no_vars]} \<^item> Truncation: @{thm take_bit_eq_mod [where ?'a = int, no_vars]} \<^item> Negation: @{thm bit_not_iff [where ?'a = int, no_vars]} \<^item> And: @{thm bit_and_iff [where ?'a = int, no_vars]} \<^item> Or: @{thm bit_or_iff [where ?'a = int, no_vars]} \<^item> Xor: @{thm bit_xor_iff [where ?'a = int, no_vars]} \<^item> Set a single bit: @{thm set_bit_def [where ?'a = int, no_vars]} \<^item> Unset a single bit: @{thm unset_bit_def [where ?'a = int, no_vars]} \<^item> Flip a single bit: @{thm flip_bit_def [where ?'a = int, no_vars]} \<^item> Signed truncation, or modulus centered around \<^term>\0::int\: @{thm signed_take_bit_def [no_vars]} \<^item> Bit concatenation: @{thm concat_bit_def [no_vars]} \<^item> (Bounded) conversion from and to a list of bits: @{thm horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]} \ code_identifier type_class semiring_bits \ (SML) Bit_Operations.semiring_bits and (OCaml) Bit_Operations.semiring_bits and (Haskell) Bit_Operations.semiring_bits and (Scala) Bit_Operations.semiring_bits | class_relation semiring_bits < semiring_parity \ (SML) Bit_Operations.semiring_parity_semiring_bits and (OCaml) Bit_Operations.semiring_parity_semiring_bits and (Haskell) Bit_Operations.semiring_parity_semiring_bits and (Scala) Bit_Operations.semiring_parity_semiring_bits | constant bit \ (SML) Bit_Operations.bit and (OCaml) Bit_Operations.bit and (Haskell) Bit_Operations.bit and (Scala) Bit_Operations.bit | class_instance nat :: semiring_bits \ (SML) Bit_Operations.semiring_bits_nat and (OCaml) Bit_Operations.semiring_bits_nat and (Haskell) Bit_Operations.semiring_bits_nat and (Scala) Bit_Operations.semiring_bits_nat | class_instance int :: semiring_bits \ (SML) Bit_Operations.semiring_bits_int and (OCaml) Bit_Operations.semiring_bits_int and (Haskell) Bit_Operations.semiring_bits_int and (Scala) Bit_Operations.semiring_bits_int | type_class semiring_bit_shifts \ (SML) Bit_Operations.semiring_bit_shifts and (OCaml) Bit_Operations.semiring_bit_shifts and (Haskell) Bit_Operations.semiring_bits and (Scala) Bit_Operations.semiring_bit_shifts | class_relation semiring_bit_shifts < semiring_bits \ (SML) Bit_Operations.semiring_bits_semiring_bit_shifts and (OCaml) Bit_Operations.semiring_bits_semiring_bit_shifts and (Haskell) Bit_Operations.semiring_bits_semiring_bit_shifts and (Scala) Bit_Operations.semiring_bits_semiring_bit_shifts | constant push_bit \ (SML) Bit_Operations.push_bit and (OCaml) Bit_Operations.push_bit and (Haskell) Bit_Operations.push_bit and (Scala) Bit_Operations.push_bit | constant drop_bit \ (SML) Bit_Operations.drop_bit and (OCaml) Bit_Operations.drop_bit and (Haskell) Bit_Operations.drop_bit and (Scala) Bit_Operations.drop_bit | constant take_bit \ (SML) Bit_Operations.take_bit and (OCaml) Bit_Operations.take_bit and (Haskell) Bit_Operations.take_bit and (Scala) Bit_Operations.take_bit | class_instance nat :: semiring_bit_shifts \ (SML) Bit_Operations.semiring_bit_shifts and (OCaml) Bit_Operations.semiring_bit_shifts and (Haskell) Bit_Operations.semiring_bit_shifts and (Scala) Bit_Operations.semiring_bit_shifts | class_instance int :: semiring_bit_shifts \ (SML) Bit_Operations.semiring_bit_shifts and (OCaml) Bit_Operations.semiring_bit_shifts and (Haskell) Bit_Operations.semiring_bit_shifts and (Scala) Bit_Operations.semiring_bit_shifts end diff --git a/src/HOL/Library/Word.thy b/src/HOL/Library/Word.thy --- a/src/HOL/Library/Word.thy +++ b/src/HOL/Library/Word.thy @@ -1,4393 +1,4403 @@ (* Title: HOL/Library/Word.thy Author: Jeremy Dawson and Gerwin Klein, NICTA, et. al. *) section \A type of finite bit strings\ theory Word imports "HOL-Library.Type_Length" "HOL-Library.Boolean_Algebra" "HOL-Library.Bit_Operations" begin subsection \Preliminaries\ lemma signed_take_bit_decr_length_iff: \signed_take_bit (LENGTH('a::len) - Suc 0) k = signed_take_bit (LENGTH('a) - Suc 0) l \ take_bit LENGTH('a) k = take_bit LENGTH('a) l\ by (cases \LENGTH('a)\) (simp_all add: signed_take_bit_eq_iff_take_bit_eq) subsection \Fundamentals\ subsubsection \Type definition\ quotient_type (overloaded) 'a word = int / \\k l. take_bit LENGTH('a) k = take_bit LENGTH('a::len) l\ morphisms rep Word by (auto intro!: equivpI reflpI sympI transpI) hide_const (open) rep \ \only for foundational purpose\ hide_const (open) Word \ \only for code generation\ subsubsection \Basic arithmetic\ instantiation word :: (len) comm_ring_1 begin lift_definition zero_word :: \'a word\ is 0 . lift_definition one_word :: \'a word\ is 1 . lift_definition plus_word :: \'a word \ 'a word \ 'a word\ is \(+)\ by (auto simp add: take_bit_eq_mod intro: mod_add_cong) lift_definition minus_word :: \'a word \ 'a word \ 'a word\ is \(-)\ by (auto simp add: take_bit_eq_mod intro: mod_diff_cong) lift_definition uminus_word :: \'a word \ 'a word\ is uminus by (auto simp add: take_bit_eq_mod intro: mod_minus_cong) lift_definition times_word :: \'a word \ 'a word \ 'a word\ is \(*)\ by (auto simp add: take_bit_eq_mod intro: mod_mult_cong) instance by (standard; transfer) (simp_all add: algebra_simps) end context includes lifting_syntax notes power_transfer [transfer_rule] transfer_rule_of_bool [transfer_rule] transfer_rule_numeral [transfer_rule] transfer_rule_of_nat [transfer_rule] transfer_rule_of_int [transfer_rule] begin lemma power_transfer_word [transfer_rule]: \(pcr_word ===> (=) ===> pcr_word) (^) (^)\ by transfer_prover lemma [transfer_rule]: \((=) ===> pcr_word) of_bool of_bool\ by transfer_prover lemma [transfer_rule]: \((=) ===> pcr_word) numeral numeral\ by transfer_prover lemma [transfer_rule]: \((=) ===> pcr_word) int of_nat\ by transfer_prover lemma [transfer_rule]: \((=) ===> pcr_word) (\k. k) of_int\ proof - have \((=) ===> pcr_word) of_int of_int\ by transfer_prover then show ?thesis by (simp add: id_def) qed lemma [transfer_rule]: \(pcr_word ===> (\)) even ((dvd) 2 :: 'a::len word \ bool)\ proof - have even_word_unfold: "even k \ (\l. take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l))" (is "?P \ ?Q") for k :: int proof assume ?P then show ?Q by auto next assume ?Q then obtain l where "take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l)" .. then have "even (take_bit LENGTH('a) k)" by simp then show ?P by simp qed show ?thesis by (simp only: even_word_unfold [abs_def] dvd_def [where ?'a = "'a word", abs_def]) transfer_prover qed end lemma exp_eq_zero_iff [simp]: \2 ^ n = (0 :: 'a::len word) \ n \ LENGTH('a)\ by transfer auto lemma word_exp_length_eq_0 [simp]: \(2 :: 'a::len word) ^ LENGTH('a) = 0\ by simp subsubsection \Basic tool setup\ ML_file \Tools/word_lib.ML\ subsubsection \Basic code generation setup\ context begin qualified lift_definition the_int :: \'a::len word \ int\ is \take_bit LENGTH('a)\ . end lemma [code abstype]: \Word.Word (Word.the_int w) = w\ by transfer simp lemma Word_eq_word_of_int [code_post, simp]: \Word.Word = of_int\ by (rule; transfer) simp quickcheck_generator word constructors: \0 :: 'a::len word\, \numeral :: num \ 'a::len word\ instantiation word :: (len) equal begin lift_definition equal_word :: \'a word \ 'a word \ bool\ is \\k l. take_bit LENGTH('a) k = take_bit LENGTH('a) l\ by simp instance by (standard; transfer) rule end lemma [code]: \HOL.equal v w \ HOL.equal (Word.the_int v) (Word.the_int w)\ by transfer (simp add: equal) lemma [code]: \Word.the_int 0 = 0\ by transfer simp lemma [code]: \Word.the_int 1 = 1\ by transfer simp lemma [code]: \Word.the_int (v + w) = take_bit LENGTH('a) (Word.the_int v + Word.the_int w)\ for v w :: \'a::len word\ by transfer (simp add: take_bit_add) lemma [code]: \Word.the_int (- w) = (let k = Word.the_int w in if w = 0 then 0 else 2 ^ LENGTH('a) - k)\ for w :: \'a::len word\ by transfer (auto simp add: take_bit_eq_mod zmod_zminus1_eq_if) lemma [code]: \Word.the_int (v - w) = take_bit LENGTH('a) (Word.the_int v - Word.the_int w)\ for v w :: \'a::len word\ by transfer (simp add: take_bit_diff) lemma [code]: \Word.the_int (v * w) = take_bit LENGTH('a) (Word.the_int v * Word.the_int w)\ for v w :: \'a::len word\ by transfer (simp add: take_bit_mult) subsubsection \Basic conversions\ abbreviation word_of_nat :: \nat \ 'a::len word\ where \word_of_nat \ of_nat\ abbreviation word_of_int :: \int \ 'a::len word\ where \word_of_int \ of_int\ lemma word_of_nat_eq_iff: \word_of_nat m = (word_of_nat n :: 'a::len word) \ take_bit LENGTH('a) m = take_bit LENGTH('a) n\ by transfer (simp add: take_bit_of_nat) lemma word_of_int_eq_iff: \word_of_int k = (word_of_int l :: 'a::len word) \ take_bit LENGTH('a) k = take_bit LENGTH('a) l\ by transfer rule lemma word_of_nat_eq_0_iff [simp]: \word_of_nat n = (0 :: 'a::len word) \ 2 ^ LENGTH('a) dvd n\ using word_of_nat_eq_iff [where ?'a = 'a, of n 0] by (simp add: take_bit_eq_0_iff) lemma word_of_int_eq_0_iff [simp]: \word_of_int k = (0 :: 'a::len word) \ 2 ^ LENGTH('a) dvd k\ using word_of_int_eq_iff [where ?'a = 'a, of k 0] by (simp add: take_bit_eq_0_iff) context semiring_1 begin lift_definition unsigned :: \'b::len word \ 'a\ is \of_nat \ nat \ take_bit LENGTH('b)\ by simp lemma unsigned_0 [simp]: \unsigned 0 = 0\ by transfer simp lemma unsigned_1 [simp]: \unsigned 1 = 1\ by transfer simp lemma unsigned_numeral [simp]: \unsigned (numeral n :: 'b::len word) = of_nat (take_bit LENGTH('b) (numeral n))\ by transfer (simp add: nat_take_bit_eq) lemma unsigned_neg_numeral [simp]: \unsigned (- numeral n :: 'b::len word) = of_nat (nat (take_bit LENGTH('b) (- numeral n)))\ by transfer simp end context semiring_1 begin lemma unsigned_of_nat [simp]: \unsigned (word_of_nat n :: 'b::len word) = of_nat (take_bit LENGTH('b) n)\ by transfer (simp add: nat_eq_iff take_bit_of_nat) lemma unsigned_of_int [simp]: \unsigned (word_of_int k :: 'b::len word) = of_nat (nat (take_bit LENGTH('b) k))\ by transfer simp end context semiring_char_0 begin lemma unsigned_word_eqI: \v = w\ if \unsigned v = unsigned w\ using that by transfer (simp add: eq_nat_nat_iff) lemma word_eq_iff_unsigned: \v = w \ unsigned v = unsigned w\ by (auto intro: unsigned_word_eqI) lemma inj_unsigned [simp]: \inj unsigned\ by (rule injI) (simp add: unsigned_word_eqI) lemma unsigned_eq_0_iff: \unsigned w = 0 \ w = 0\ using word_eq_iff_unsigned [of w 0] by simp end context ring_1 begin lift_definition signed :: \'b::len word \ 'a\ is \of_int \ signed_take_bit (LENGTH('b) - Suc 0)\ by (simp flip: signed_take_bit_decr_length_iff) lemma signed_0 [simp]: \signed 0 = 0\ by transfer simp lemma signed_1 [simp]: \signed (1 :: 'b::len word) = (if LENGTH('b) = 1 then - 1 else 1)\ by (transfer fixing: uminus; cases \LENGTH('b)\) (auto dest: gr0_implies_Suc) lemma signed_minus_1 [simp]: \signed (- 1 :: 'b::len word) = - 1\ by (transfer fixing: uminus) simp lemma signed_numeral [simp]: \signed (numeral n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b) - 1) (numeral n))\ by transfer simp lemma signed_neg_numeral [simp]: \signed (- numeral n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b) - 1) (- numeral n))\ by transfer simp lemma signed_of_nat [simp]: \signed (word_of_nat n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b) - Suc 0) (int n))\ by transfer simp lemma signed_of_int [simp]: \signed (word_of_int n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b) - Suc 0) n)\ by transfer simp end context ring_char_0 begin lemma signed_word_eqI: \v = w\ if \signed v = signed w\ using that by transfer (simp flip: signed_take_bit_decr_length_iff) lemma word_eq_iff_signed: \v = w \ signed v = signed w\ by (auto intro: signed_word_eqI) lemma inj_signed [simp]: \inj signed\ by (rule injI) (simp add: signed_word_eqI) lemma signed_eq_0_iff: \signed w = 0 \ w = 0\ using word_eq_iff_signed [of w 0] by simp end abbreviation unat :: \'a::len word \ nat\ where \unat \ unsigned\ abbreviation uint :: \'a::len word \ int\ where \uint \ unsigned\ abbreviation sint :: \'a::len word \ int\ where \sint \ signed\ abbreviation ucast :: \'a::len word \ 'b::len word\ where \ucast \ unsigned\ abbreviation scast :: \'a::len word \ 'b::len word\ where \scast \ signed\ context includes lifting_syntax begin lemma [transfer_rule]: \(pcr_word ===> (=)) (nat \ take_bit LENGTH('a)) (unat :: 'a::len word \ nat)\ using unsigned.transfer [where ?'a = nat] by simp lemma [transfer_rule]: \(pcr_word ===> (=)) (take_bit LENGTH('a)) (uint :: 'a::len word \ int)\ using unsigned.transfer [where ?'a = int] by (simp add: comp_def) lemma [transfer_rule]: \(pcr_word ===> (=)) (signed_take_bit (LENGTH('a) - Suc 0)) (sint :: 'a::len word \ int)\ using signed.transfer [where ?'a = int] by simp lemma [transfer_rule]: \(pcr_word ===> pcr_word) (take_bit LENGTH('a)) (ucast :: 'a::len word \ 'b::len word)\ proof (rule rel_funI) fix k :: int and w :: \'a word\ assume \pcr_word k w\ then have \w = word_of_int k\ by (simp add: pcr_word_def cr_word_def relcompp_apply) moreover have \pcr_word (take_bit LENGTH('a) k) (ucast (word_of_int k :: 'a word))\ by transfer (simp add: pcr_word_def cr_word_def relcompp_apply) ultimately show \pcr_word (take_bit LENGTH('a) k) (ucast w)\ by simp qed lemma [transfer_rule]: \(pcr_word ===> pcr_word) (signed_take_bit (LENGTH('a) - Suc 0)) (scast :: 'a::len word \ 'b::len word)\ proof (rule rel_funI) fix k :: int and w :: \'a word\ assume \pcr_word k w\ then have \w = word_of_int k\ by (simp add: pcr_word_def cr_word_def relcompp_apply) moreover have \pcr_word (signed_take_bit (LENGTH('a) - Suc 0) k) (scast (word_of_int k :: 'a word))\ by transfer (simp add: pcr_word_def cr_word_def relcompp_apply) ultimately show \pcr_word (signed_take_bit (LENGTH('a) - Suc 0) k) (scast w)\ by simp qed end lemma of_nat_unat [simp]: \of_nat (unat w) = unsigned w\ by transfer simp lemma of_int_uint [simp]: \of_int (uint w) = unsigned w\ by transfer simp lemma of_int_sint [simp]: \of_int (sint a) = signed a\ by transfer (simp_all add: take_bit_signed_take_bit) lemma nat_uint_eq [simp]: \nat (uint w) = unat w\ by transfer simp lemma sgn_uint_eq [simp]: \sgn (uint w) = of_bool (w \ 0)\ by transfer (simp add: less_le) text \Aliasses only for code generation\ context begin qualified lift_definition of_int :: \int \ 'a::len word\ is \take_bit LENGTH('a)\ . qualified lift_definition of_nat :: \nat \ 'a::len word\ is \int \ take_bit LENGTH('a)\ . qualified lift_definition the_nat :: \'a::len word \ nat\ is \nat \ take_bit LENGTH('a)\ by simp qualified lift_definition the_signed_int :: \'a::len word \ int\ is \signed_take_bit (LENGTH('a) - Suc 0)\ by (simp add: signed_take_bit_decr_length_iff) qualified lift_definition cast :: \'a::len word \ 'b::len word\ is \take_bit LENGTH('a)\ by simp qualified lift_definition signed_cast :: \'a::len word \ 'b::len word\ is \signed_take_bit (LENGTH('a) - Suc 0)\ by (metis signed_take_bit_decr_length_iff) end lemma [code_abbrev, simp]: \Word.the_int = uint\ by transfer rule lemma [code]: \Word.the_int (Word.of_int k :: 'a::len word) = take_bit LENGTH('a) k\ by transfer simp lemma [code_abbrev, simp]: \Word.of_int = word_of_int\ by (rule; transfer) simp lemma [code]: \Word.the_int (Word.of_nat n :: 'a::len word) = take_bit LENGTH('a) (int n)\ by transfer (simp add: take_bit_of_nat) lemma [code_abbrev, simp]: \Word.of_nat = word_of_nat\ by (rule; transfer) (simp add: take_bit_of_nat) lemma [code]: \Word.the_nat w = nat (Word.the_int w)\ by transfer simp lemma [code_abbrev, simp]: \Word.the_nat = unat\ by (rule; transfer) simp lemma [code]: \Word.the_signed_int w = signed_take_bit (LENGTH('a) - Suc 0) (Word.the_int w)\ for w :: \'a::len word\ by transfer (simp add: signed_take_bit_take_bit) lemma [code_abbrev, simp]: \Word.the_signed_int = sint\ by (rule; transfer) simp lemma [code]: \Word.the_int (Word.cast w :: 'b::len word) = take_bit LENGTH('b) (Word.the_int w)\ for w :: \'a::len word\ by transfer simp lemma [code_abbrev, simp]: \Word.cast = ucast\ by (rule; transfer) simp lemma [code]: \Word.the_int (Word.signed_cast w :: 'b::len word) = take_bit LENGTH('b) (Word.the_signed_int w)\ for w :: \'a::len word\ by transfer simp lemma [code_abbrev, simp]: \Word.signed_cast = scast\ by (rule; transfer) simp lemma [code]: \unsigned w = of_nat (nat (Word.the_int w))\ by transfer simp lemma [code]: \signed w = of_int (Word.the_signed_int w)\ by transfer simp subsubsection \Basic ordering\ instantiation word :: (len) linorder begin lift_definition less_eq_word :: "'a word \ 'a word \ bool" is "\a b. take_bit LENGTH('a) a \ take_bit LENGTH('a) b" by simp lift_definition less_word :: "'a word \ 'a word \ bool" is "\a b. take_bit LENGTH('a) a < take_bit LENGTH('a) b" by simp instance by (standard; transfer) auto end interpretation word_order: ordering_top \(\)\ \(<)\ \- 1 :: 'a::len word\ by (standard; transfer) (simp add: take_bit_eq_mod zmod_minus1) interpretation word_coorder: ordering_top \(\)\ \(>)\ \0 :: 'a::len word\ by (standard; transfer) simp lemma word_of_nat_less_eq_iff: \word_of_nat m \ (word_of_nat n :: 'a::len word) \ take_bit LENGTH('a) m \ take_bit LENGTH('a) n\ by transfer (simp add: take_bit_of_nat) lemma word_of_int_less_eq_iff: \word_of_int k \ (word_of_int l :: 'a::len word) \ take_bit LENGTH('a) k \ take_bit LENGTH('a) l\ by transfer rule lemma word_of_nat_less_iff: \word_of_nat m < (word_of_nat n :: 'a::len word) \ take_bit LENGTH('a) m < take_bit LENGTH('a) n\ by transfer (simp add: take_bit_of_nat) lemma word_of_int_less_iff: \word_of_int k < (word_of_int l :: 'a::len word) \ take_bit LENGTH('a) k < take_bit LENGTH('a) l\ by transfer rule lemma word_le_def [code]: "a \ b \ uint a \ uint b" by transfer rule lemma word_less_def [code]: "a < b \ uint a < uint b" by transfer rule lemma word_greater_zero_iff: \a > 0 \ a \ 0\ for a :: \'a::len word\ by transfer (simp add: less_le) lemma of_nat_word_less_eq_iff: \of_nat m \ (of_nat n :: 'a::len word) \ take_bit LENGTH('a) m \ take_bit LENGTH('a) n\ by transfer (simp add: take_bit_of_nat) lemma of_nat_word_less_iff: \of_nat m < (of_nat n :: 'a::len word) \ take_bit LENGTH('a) m < take_bit LENGTH('a) n\ by transfer (simp add: take_bit_of_nat) lemma of_int_word_less_eq_iff: \of_int k \ (of_int l :: 'a::len word) \ take_bit LENGTH('a) k \ take_bit LENGTH('a) l\ by transfer rule lemma of_int_word_less_iff: \of_int k < (of_int l :: 'a::len word) \ take_bit LENGTH('a) k < take_bit LENGTH('a) l\ by transfer rule subsection \Enumeration\ lemma inj_on_word_of_nat: \inj_on (word_of_nat :: nat \ 'a::len word) {0..<2 ^ LENGTH('a)}\ by (rule inj_onI; transfer) (simp_all add: take_bit_int_eq_self) lemma UNIV_word_eq_word_of_nat: \(UNIV :: 'a::len word set) = word_of_nat ` {0..<2 ^ LENGTH('a)}\ (is \_ = ?A\) proof show \word_of_nat ` {0..<2 ^ LENGTH('a)} \ UNIV\ by simp show \UNIV \ ?A\ proof fix w :: \'a word\ show \w \ (word_of_nat ` {0..<2 ^ LENGTH('a)} :: 'a word set)\ by (rule image_eqI [of _ _ \unat w\]; transfer) simp_all qed qed instantiation word :: (len) enum begin definition enum_word :: \'a word list\ where \enum_word = map word_of_nat [0..<2 ^ LENGTH('a)]\ definition enum_all_word :: \('a word \ bool) \ bool\ where \enum_all_word = Ball UNIV\ definition enum_ex_word :: \('a word \ bool) \ bool\ where \enum_ex_word = Bex UNIV\ lemma [code]: \Enum.enum_all P \ Ball UNIV P\ \Enum.enum_ex P \ Bex UNIV P\ for P :: \'a word \ bool\ by (simp_all add: enum_all_word_def enum_ex_word_def) instance by standard (simp_all add: UNIV_word_eq_word_of_nat inj_on_word_of_nat enum_word_def enum_all_word_def enum_ex_word_def distinct_map) end subsection \Bit-wise operations\ instantiation word :: (len) semiring_modulo begin lift_definition divide_word :: \'a word \ 'a word \ 'a word\ is \\a b. take_bit LENGTH('a) a div take_bit LENGTH('a) b\ by simp lift_definition modulo_word :: \'a word \ 'a word \ 'a word\ is \\a b. take_bit LENGTH('a) a mod take_bit LENGTH('a) b\ by simp instance proof show "a div b * b + a mod b = a" for a b :: "'a word" proof transfer fix k l :: int define r :: int where "r = 2 ^ LENGTH('a)" then have r: "take_bit LENGTH('a) k = k mod r" for k by (simp add: take_bit_eq_mod) have "k mod r = ((k mod r) div (l mod r) * (l mod r) + (k mod r) mod (l mod r)) mod r" by (simp add: div_mult_mod_eq) also have "... = (((k mod r) div (l mod r) * (l mod r)) mod r + (k mod r) mod (l mod r)) mod r" by (simp add: mod_add_left_eq) also have "... = (((k mod r) div (l mod r) * l) mod r + (k mod r) mod (l mod r)) mod r" by (simp add: mod_mult_right_eq) finally have "k mod r = ((k mod r) div (l mod r) * l + (k mod r) mod (l mod r)) mod r" by (simp add: mod_simps) with r show "take_bit LENGTH('a) (take_bit LENGTH('a) k div take_bit LENGTH('a) l * l + take_bit LENGTH('a) k mod take_bit LENGTH('a) l) = take_bit LENGTH('a) k" by simp qed qed end instance word :: (len) semiring_parity proof show "\ 2 dvd (1::'a word)" by transfer simp show even_iff_mod_2_eq_0: "2 dvd a \ a mod 2 = 0" for a :: "'a word" by transfer (simp_all add: mod_2_eq_odd take_bit_Suc) show "\ 2 dvd a \ a mod 2 = 1" for a :: "'a word" by transfer (simp_all add: mod_2_eq_odd take_bit_Suc) qed lemma word_bit_induct [case_names zero even odd]: \P a\ if word_zero: \P 0\ and word_even: \\a. P a \ 0 < a \ a < 2 ^ (LENGTH('a) - Suc 0) \ P (2 * a)\ and word_odd: \\a. P a \ a < 2 ^ (LENGTH('a) - Suc 0) \ P (1 + 2 * a)\ for P and a :: \'a::len word\ proof - define m :: nat where \m = LENGTH('a) - Suc 0\ then have l: \LENGTH('a) = Suc m\ by simp define n :: nat where \n = unat a\ then have \n < 2 ^ LENGTH('a)\ by transfer (simp add: take_bit_eq_mod) then have \n < 2 * 2 ^ m\ by (simp add: l) then have \P (of_nat n)\ proof (induction n rule: nat_bit_induct) case zero show ?case by simp (rule word_zero) next case (even n) then have \n < 2 ^ m\ by simp with even.IH have \P (of_nat n)\ by simp moreover from \n < 2 ^ m\ even.hyps have \0 < (of_nat n :: 'a word)\ by (auto simp add: word_greater_zero_iff l) moreover from \n < 2 ^ m\ have \(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - Suc 0)\ using of_nat_word_less_iff [where ?'a = 'a, of n \2 ^ m\] by (simp add: l take_bit_eq_mod) ultimately have \P (2 * of_nat n)\ by (rule word_even) then show ?case by simp next case (odd n) then have \Suc n \ 2 ^ m\ by simp with odd.IH have \P (of_nat n)\ by simp moreover from \Suc n \ 2 ^ m\ have \(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - Suc 0)\ using of_nat_word_less_iff [where ?'a = 'a, of n \2 ^ m\] by (simp add: l take_bit_eq_mod) ultimately have \P (1 + 2 * of_nat n)\ by (rule word_odd) then show ?case by simp qed moreover have \of_nat (nat (uint a)) = a\ by transfer simp ultimately show ?thesis by (simp add: n_def) qed lemma bit_word_half_eq: \(of_bool b + a * 2) div 2 = a\ if \a < 2 ^ (LENGTH('a) - Suc 0)\ for a :: \'a::len word\ proof (cases \2 \ LENGTH('a::len)\) case False have \of_bool (odd k) < (1 :: int) \ even k\ for k :: int by auto with False that show ?thesis by transfer (simp add: eq_iff) next case True obtain n where length: \LENGTH('a) = Suc n\ by (cases \LENGTH('a)\) simp_all show ?thesis proof (cases b) case False moreover have \a * 2 div 2 = a\ using that proof transfer fix k :: int from length have \k * 2 mod 2 ^ LENGTH('a) = (k mod 2 ^ n) * 2\ by simp moreover assume \take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a) - Suc 0))\ with \LENGTH('a) = Suc n\ have \k mod 2 ^ LENGTH('a) = k mod 2 ^ n\ by (simp add: take_bit_eq_mod divmod_digit_0) ultimately have \take_bit LENGTH('a) (k * 2) = take_bit LENGTH('a) k * 2\ by (simp add: take_bit_eq_mod) with True show \take_bit LENGTH('a) (take_bit LENGTH('a) (k * 2) div take_bit LENGTH('a) 2) = take_bit LENGTH('a) k\ by simp qed ultimately show ?thesis by simp next case True moreover have \(1 + a * 2) div 2 = a\ using that proof transfer fix k :: int from length have \(1 + k * 2) mod 2 ^ LENGTH('a) = 1 + (k mod 2 ^ n) * 2\ using pos_zmod_mult_2 [of \2 ^ n\ k] by (simp add: ac_simps) moreover assume \take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a) - Suc 0))\ with \LENGTH('a) = Suc n\ have \k mod 2 ^ LENGTH('a) = k mod 2 ^ n\ by (simp add: take_bit_eq_mod divmod_digit_0) ultimately have \take_bit LENGTH('a) (1 + k * 2) = 1 + take_bit LENGTH('a) k * 2\ by (simp add: take_bit_eq_mod) with True show \take_bit LENGTH('a) (take_bit LENGTH('a) (1 + k * 2) div take_bit LENGTH('a) 2) = take_bit LENGTH('a) k\ by (auto simp add: take_bit_Suc) qed ultimately show ?thesis by simp qed qed lemma even_mult_exp_div_word_iff: \even (a * 2 ^ m div 2 ^ n) \ \ ( m \ n \ n < LENGTH('a) \ odd (a div 2 ^ (n - m)))\ for a :: \'a::len word\ by transfer (auto simp flip: drop_bit_eq_div simp add: even_drop_bit_iff_not_bit bit_take_bit_iff, simp_all flip: push_bit_eq_mult add: bit_push_bit_iff_int) instantiation word :: (len) semiring_bits begin lift_definition bit_word :: \'a word \ nat \ bool\ is \\k n. n < LENGTH('a) \ bit k n\ proof fix k l :: int and n :: nat assume *: \take_bit LENGTH('a) k = take_bit LENGTH('a) l\ show \n < LENGTH('a) \ bit k n \ n < LENGTH('a) \ bit l n\ proof (cases \n < LENGTH('a)\) case True from * have \bit (take_bit LENGTH('a) k) n \ bit (take_bit LENGTH('a) l) n\ by simp then show ?thesis by (simp add: bit_take_bit_iff) next case False then show ?thesis by simp qed qed instance proof show \P a\ if stable: \\a. a div 2 = a \ P a\ and rec: \\a b. P a \ (of_bool b + 2 * a) div 2 = a \ P (of_bool b + 2 * a)\ for P and a :: \'a word\ proof (induction a rule: word_bit_induct) case zero have \0 div 2 = (0::'a word)\ by transfer simp with stable [of 0] show ?case by simp next case (even a) with rec [of a False] show ?case using bit_word_half_eq [of a False] by (simp add: ac_simps) next case (odd a) with rec [of a True] show ?case using bit_word_half_eq [of a True] by (simp add: ac_simps) qed show \bit a n \ odd (a div 2 ^ n)\ for a :: \'a word\ and n by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit bit_iff_odd_drop_bit) show \0 div a = 0\ for a :: \'a word\ by transfer simp show \a div 1 = a\ for a :: \'a word\ by transfer simp have \
: "\i n. (i::int) mod 2 ^ n = 0 \ 0 < i mod 2 ^ n" by (metis le_less take_bit_eq_mod take_bit_nonnegative) have less_power: "\n i p. (i::int) mod numeral p ^ n < numeral p ^ n" by simp show \a mod b div b = 0\ for a b :: \'a word\ apply transfer apply (simp add: take_bit_eq_mod mod_eq_0_iff_dvd dvd_def) by (metis (no_types, hide_lams) "\
" Euclidean_Division.pos_mod_bound Euclidean_Division.pos_mod_sign le_less_trans mult_eq_0_iff take_bit_eq_mod take_bit_nonnegative zdiv_eq_0_iff zmod_le_nonneg_dividend) show \(1 + a) div 2 = a div 2\ if \even a\ for a :: \'a word\ using that by transfer (auto dest: le_Suc_ex simp add: take_bit_Suc elim!: evenE) show \(2 :: 'a word) ^ m div 2 ^ n = of_bool ((2 :: 'a word) ^ m \ 0 \ n \ m) * 2 ^ (m - n)\ for m n :: nat by transfer (simp, simp add: exp_div_exp_eq) show "a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)" for a :: "'a word" and m n :: nat apply transfer apply (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: drop_bit_eq_div) apply (simp add: drop_bit_take_bit) done show "a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n" for a :: "'a word" and m n :: nat by transfer (auto simp flip: take_bit_eq_mod simp add: ac_simps) show \a * 2 ^ m mod 2 ^ n = a mod 2 ^ (n - m) * 2 ^ m\ if \m \ n\ for a :: "'a word" and m n :: nat using that apply transfer apply (auto simp flip: take_bit_eq_mod) apply (auto simp flip: push_bit_eq_mult simp add: push_bit_take_bit split: split_min_lin) done show \a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\ for a :: "'a word" and m n :: nat by transfer (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: take_bit_eq_mod drop_bit_eq_div split: split_min_lin) show \even ((2 ^ m - 1) div (2::'a word) ^ n) \ 2 ^ n = (0::'a word) \ m \ n\ for m n :: nat by transfer (auto simp add: take_bit_of_mask even_mask_div_iff) show \even (a * 2 ^ m div 2 ^ n) \ n < m \ (2::'a word) ^ n = 0 \ m \ n \ even (a div 2 ^ (n - m))\ for a :: \'a word\ and m n :: nat proof transfer show \even (take_bit LENGTH('a) (k * 2 ^ m) div take_bit LENGTH('a) (2 ^ n)) \ n < m \ take_bit LENGTH('a) ((2::int) ^ n) = take_bit LENGTH('a) 0 \ (m \ n \ even (take_bit LENGTH('a) k div take_bit LENGTH('a) (2 ^ (n - m))))\ for m n :: nat and k l :: int by (auto simp flip: take_bit_eq_mod drop_bit_eq_div push_bit_eq_mult simp add: div_push_bit_of_1_eq_drop_bit drop_bit_take_bit drop_bit_push_bit_int [of n m]) qed qed end lemma bit_word_eqI: \a = b\ if \\n. n < LENGTH('a) \ bit a n \ bit b n\ for a b :: \'a::len word\ using that by transfer (auto simp add: nat_less_le bit_eq_iff bit_take_bit_iff) lemma bit_imp_le_length: \n < LENGTH('a)\ if \bit w n\ for w :: \'a::len word\ using that by transfer simp lemma not_bit_length [simp]: \\ bit w LENGTH('a)\ for w :: \'a::len word\ by transfer simp lemma finite_bit_word [simp]: \finite {n. bit w n}\ for w :: \'a::len word\ proof - have \{n. bit w n} \ {0..LENGTH('a)}\ by (auto dest: bit_imp_le_length) moreover have \finite {0..LENGTH('a)}\ by simp ultimately show ?thesis by (rule finite_subset) qed +lemma bit_numeral_word_iff [simp]: + \bit (numeral w :: 'a::len word) n + \ n < LENGTH('a) \ bit (numeral w :: int) n\ + by transfer simp + +lemma bit_neg_numeral_word_iff [simp]: + \bit (- numeral w :: 'a::len word) n + \ n < LENGTH('a) \ bit (- numeral w :: int) n\ + by transfer simp + instantiation word :: (len) semiring_bit_shifts begin lift_definition push_bit_word :: \nat \ 'a word \ 'a word\ is push_bit proof - show \take_bit LENGTH('a) (push_bit n k) = take_bit LENGTH('a) (push_bit n l)\ if \take_bit LENGTH('a) k = take_bit LENGTH('a) l\ for k l :: int and n :: nat proof - from that have \take_bit (LENGTH('a) - n) (take_bit LENGTH('a) k) = take_bit (LENGTH('a) - n) (take_bit LENGTH('a) l)\ by simp moreover have \min (LENGTH('a) - n) LENGTH('a) = LENGTH('a) - n\ by simp ultimately show ?thesis by (simp add: take_bit_push_bit) qed qed lift_definition drop_bit_word :: \nat \ 'a word \ 'a word\ is \\n. drop_bit n \ take_bit LENGTH('a)\ by (simp add: take_bit_eq_mod) lift_definition take_bit_word :: \nat \ 'a word \ 'a word\ is \\n. take_bit (min LENGTH('a) n)\ by (simp add: ac_simps) (simp only: flip: take_bit_take_bit) instance proof show \push_bit n a = a * 2 ^ n\ for n :: nat and a :: \'a word\ by transfer (simp add: push_bit_eq_mult) show \drop_bit n a = a div 2 ^ n\ for n :: nat and a :: \'a word\ by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit) show \take_bit n a = a mod 2 ^ n\ for n :: nat and a :: \'a word\ by transfer (auto simp flip: take_bit_eq_mod) qed end lemma [code]: \push_bit n w = w * 2 ^ n\ for w :: \'a::len word\ by (fact push_bit_eq_mult) lemma [code]: \Word.the_int (drop_bit n w) = drop_bit n (Word.the_int w)\ by transfer (simp add: drop_bit_take_bit min_def le_less less_diff_conv) lemma [code]: \Word.the_int (take_bit n w) = (if n < LENGTH('a::len) then take_bit n (Word.the_int w) else Word.the_int w)\ for w :: \'a::len word\ by transfer (simp add: not_le not_less ac_simps min_absorb2) instantiation word :: (len) ring_bit_operations begin lift_definition not_word :: \'a word \ 'a word\ is not by (simp add: take_bit_not_iff) lift_definition and_word :: \'a word \ 'a word \ 'a word\ is \and\ by simp lift_definition or_word :: \'a word \ 'a word \ 'a word\ is or by simp lift_definition xor_word :: \'a word \ 'a word \ 'a word\ is xor by simp lift_definition mask_word :: \nat \ 'a word\ is mask . lift_definition set_bit_word :: \nat \ 'a word \ 'a word\ is set_bit by (simp add: set_bit_def) lift_definition unset_bit_word :: \nat \ 'a word \ 'a word\ is unset_bit by (simp add: unset_bit_def) lift_definition flip_bit_word :: \nat \ 'a word \ 'a word\ is flip_bit by (simp add: flip_bit_def) instance by (standard; transfer) (auto simp add: minus_eq_not_minus_1 mask_eq_exp_minus_1 bit_simps set_bit_def flip_bit_def) end lemma [code_abbrev]: \push_bit n 1 = (2 :: 'a::len word) ^ n\ by (fact push_bit_of_1) lemma [code]: \NOT w = Word.of_int (NOT (Word.the_int w))\ for w :: \'a::len word\ by transfer (simp add: take_bit_not_take_bit) lemma [code]: \Word.the_int (v AND w) = Word.the_int v AND Word.the_int w\ by transfer simp lemma [code]: \Word.the_int (v OR w) = Word.the_int v OR Word.the_int w\ by transfer simp lemma [code]: \Word.the_int (v XOR w) = Word.the_int v XOR Word.the_int w\ by transfer simp lemma [code]: \Word.the_int (mask n :: 'a::len word) = mask (min LENGTH('a) n)\ by transfer simp lemma [code]: \set_bit n w = w OR push_bit n 1\ for w :: \'a::len word\ by (fact set_bit_eq_or) lemma [code]: \unset_bit n w = w AND NOT (push_bit n 1)\ for w :: \'a::len word\ by (fact unset_bit_eq_and_not) lemma [code]: \flip_bit n w = w XOR push_bit n 1\ for w :: \'a::len word\ by (fact flip_bit_eq_xor) context includes lifting_syntax begin lemma set_bit_word_transfer [transfer_rule]: \((=) ===> pcr_word ===> pcr_word) set_bit set_bit\ by (unfold set_bit_def) transfer_prover lemma unset_bit_word_transfer [transfer_rule]: \((=) ===> pcr_word ===> pcr_word) unset_bit unset_bit\ by (unfold unset_bit_def) transfer_prover lemma flip_bit_word_transfer [transfer_rule]: \((=) ===> pcr_word ===> pcr_word) flip_bit flip_bit\ by (unfold flip_bit_def) transfer_prover lemma signed_take_bit_word_transfer [transfer_rule]: \((=) ===> pcr_word ===> pcr_word) (\n k. signed_take_bit n (take_bit LENGTH('a::len) k)) (signed_take_bit :: nat \ 'a word \ 'a word)\ proof - let ?K = \\n (k :: int). take_bit (min LENGTH('a) n) k OR of_bool (n < LENGTH('a) \ bit k n) * NOT (mask n)\ let ?W = \\n (w :: 'a word). take_bit n w OR of_bool (bit w n) * NOT (mask n)\ have \((=) ===> pcr_word ===> pcr_word) ?K ?W\ by transfer_prover also have \?K = (\n k. signed_take_bit n (take_bit LENGTH('a::len) k))\ by (simp add: fun_eq_iff signed_take_bit_def bit_take_bit_iff ac_simps) also have \?W = signed_take_bit\ by (simp add: fun_eq_iff signed_take_bit_def) finally show ?thesis . qed end subsection \Conversions including casts\ subsubsection \Generic unsigned conversion\ context semiring_bits begin lemma bit_unsigned_iff [bit_simps]: \bit (unsigned w) n \ 2 ^ n \ 0 \ bit w n\ for w :: \'b::len word\ by (transfer fixing: bit) (simp add: bit_of_nat_iff bit_nat_iff bit_take_bit_iff) end context semiring_bit_shifts begin lemma unsigned_push_bit_eq: \unsigned (push_bit n w) = take_bit LENGTH('b) (push_bit n (unsigned w))\ for w :: \'b::len word\ proof (rule bit_eqI) fix m assume \2 ^ m \ 0\ show \bit (unsigned (push_bit n w)) m = bit (take_bit LENGTH('b) (push_bit n (unsigned w))) m\ proof (cases \n \ m\) case True with \2 ^ m \ 0\ have \2 ^ (m - n) \ 0\ by (metis (full_types) diff_add exp_add_not_zero_imp) with True show ?thesis by (simp add: bit_unsigned_iff bit_push_bit_iff Parity.bit_push_bit_iff bit_take_bit_iff not_le exp_eq_zero_iff ac_simps) next case False then show ?thesis by (simp add: not_le bit_unsigned_iff bit_push_bit_iff Parity.bit_push_bit_iff bit_take_bit_iff) qed qed lemma unsigned_take_bit_eq: \unsigned (take_bit n w) = take_bit n (unsigned w)\ for w :: \'b::len word\ by (rule bit_eqI) (simp add: bit_unsigned_iff bit_take_bit_iff Parity.bit_take_bit_iff) end context unique_euclidean_semiring_with_bit_shifts begin lemma unsigned_drop_bit_eq: \unsigned (drop_bit n w) = drop_bit n (take_bit LENGTH('b) (unsigned w))\ for w :: \'b::len word\ by (rule bit_eqI) (auto simp add: bit_unsigned_iff bit_take_bit_iff bit_drop_bit_eq Parity.bit_drop_bit_eq dest: bit_imp_le_length) end context semiring_bit_operations begin lemma unsigned_and_eq: \unsigned (v AND w) = unsigned v AND unsigned w\ for v w :: \'b::len word\ by (rule bit_eqI) (simp add: bit_unsigned_iff bit_and_iff Bit_Operations.bit_and_iff) lemma unsigned_or_eq: \unsigned (v OR w) = unsigned v OR unsigned w\ for v w :: \'b::len word\ by (rule bit_eqI) (simp add: bit_unsigned_iff bit_or_iff Bit_Operations.bit_or_iff) lemma unsigned_xor_eq: \unsigned (v XOR w) = unsigned v XOR unsigned w\ for v w :: \'b::len word\ by (rule bit_eqI) (simp add: bit_unsigned_iff bit_xor_iff Bit_Operations.bit_xor_iff) end context ring_bit_operations begin lemma unsigned_not_eq: \unsigned (NOT w) = take_bit LENGTH('b) (NOT (unsigned w))\ for w :: \'b::len word\ by (rule bit_eqI) (simp add: bit_unsigned_iff bit_take_bit_iff bit_not_iff Bit_Operations.bit_not_iff exp_eq_zero_iff not_le) end context unique_euclidean_semiring_numeral begin lemma unsigned_greater_eq [simp]: \0 \ unsigned w\ for w :: \'b::len word\ by (transfer fixing: less_eq) simp lemma unsigned_less [simp]: \unsigned w < 2 ^ LENGTH('b)\ for w :: \'b::len word\ by (transfer fixing: less) simp end context linordered_semidom begin lemma word_less_eq_iff_unsigned: "a \ b \ unsigned a \ unsigned b" by (transfer fixing: less_eq) (simp add: nat_le_eq_zle) lemma word_less_iff_unsigned: "a < b \ unsigned a < unsigned b" by (transfer fixing: less) (auto dest: preorder_class.le_less_trans [OF take_bit_nonnegative]) end subsubsection \Generic signed conversion\ context ring_bit_operations begin lemma bit_signed_iff [bit_simps]: \bit (signed w) n \ 2 ^ n \ 0 \ bit w (min (LENGTH('b) - Suc 0) n)\ for w :: \'b::len word\ by (transfer fixing: bit) (auto simp add: bit_of_int_iff Bit_Operations.bit_signed_take_bit_iff min_def) lemma signed_push_bit_eq: \signed (push_bit n w) = signed_take_bit (LENGTH('b) - Suc 0) (push_bit n (signed w :: 'a))\ for w :: \'b::len word\ proof (rule bit_eqI) fix m assume \2 ^ m \ 0\ define q where \q = LENGTH('b) - Suc 0\ then have *: \LENGTH('b) = Suc q\ by simp show \bit (signed (push_bit n w)) m \ bit (signed_take_bit (LENGTH('b) - Suc 0) (push_bit n (signed w :: 'a))) m\ proof (cases \q \ m\) case True moreover define r where \r = m - q\ ultimately have \m = q + r\ by simp moreover from \m = q + r\ \2 ^ m \ 0\ have \2 ^ q \ 0\ \2 ^ r \ 0\ using exp_add_not_zero_imp_left [of q r] exp_add_not_zero_imp_right [of q r] by simp_all moreover from \2 ^ q \ 0\ have \2 ^ (q - n) \ 0\ by (rule exp_not_zero_imp_exp_diff_not_zero) ultimately show ?thesis by (auto simp add: bit_signed_iff bit_signed_take_bit_iff bit_push_bit_iff Parity.bit_push_bit_iff min_def * exp_eq_zero_iff le_diff_conv2) next case False then show ?thesis using exp_not_zero_imp_exp_diff_not_zero [of m n] by (auto simp add: bit_signed_iff bit_signed_take_bit_iff bit_push_bit_iff Parity.bit_push_bit_iff min_def not_le not_less * le_diff_conv2 less_diff_conv2 Parity.exp_eq_0_imp_not_bit exp_eq_0_imp_not_bit exp_eq_zero_iff) qed qed lemma signed_take_bit_eq: \signed (take_bit n w) = (if n < LENGTH('b) then take_bit n (signed w) else signed w)\ for w :: \'b::len word\ by (transfer fixing: take_bit; cases \LENGTH('b)\) (auto simp add: Bit_Operations.signed_take_bit_take_bit Bit_Operations.take_bit_signed_take_bit take_bit_of_int min_def less_Suc_eq) lemma signed_not_eq: \signed (NOT w) = signed_take_bit LENGTH('b) (NOT (signed w))\ for w :: \'b::len word\ proof (rule bit_eqI) fix n assume \2 ^ n \ 0\ define q where \q = LENGTH('b) - Suc 0\ then have *: \LENGTH('b) = Suc q\ by simp show \bit (signed (NOT w)) n \ bit (signed_take_bit LENGTH('b) (NOT (signed w))) n\ proof (cases \q < n\) case True moreover define r where \r = n - Suc q\ ultimately have \n = r + Suc q\ by simp moreover from \2 ^ n \ 0\ \n = r + Suc q\ have \2 ^ Suc q \ 0\ using exp_add_not_zero_imp_right by blast ultimately show ?thesis by (simp add: * bit_signed_iff bit_not_iff bit_signed_take_bit_iff Bit_Operations.bit_not_iff min_def exp_eq_zero_iff) next case False then show ?thesis by (auto simp add: * bit_signed_iff bit_not_iff bit_signed_take_bit_iff Bit_Operations.bit_not_iff min_def exp_eq_zero_iff) qed qed lemma signed_and_eq: \signed (v AND w) = signed v AND signed w\ for v w :: \'b::len word\ by (rule bit_eqI) (simp add: bit_signed_iff bit_and_iff Bit_Operations.bit_and_iff) lemma signed_or_eq: \signed (v OR w) = signed v OR signed w\ for v w :: \'b::len word\ by (rule bit_eqI) (simp add: bit_signed_iff bit_or_iff Bit_Operations.bit_or_iff) lemma signed_xor_eq: \signed (v XOR w) = signed v XOR signed w\ for v w :: \'b::len word\ by (rule bit_eqI) (simp add: bit_signed_iff bit_xor_iff Bit_Operations.bit_xor_iff) end subsubsection \More\ lemma sint_greater_eq: \- (2 ^ (LENGTH('a) - Suc 0)) \ sint w\ for w :: \'a::len word\ proof (cases \bit w (LENGTH('a) - Suc 0)\) case True then show ?thesis by transfer (simp add: signed_take_bit_eq_if_negative minus_exp_eq_not_mask or_greater_eq ac_simps) next have *: \- (2 ^ (LENGTH('a) - Suc 0)) \ (0::int)\ by simp case False then show ?thesis by transfer (auto simp add: signed_take_bit_eq intro: order_trans *) qed lemma sint_less: \sint w < 2 ^ (LENGTH('a) - Suc 0)\ for w :: \'a::len word\ by (cases \bit w (LENGTH('a) - Suc 0)\; transfer) (simp_all add: signed_take_bit_eq signed_take_bit_def not_eq_complement mask_eq_exp_minus_1 OR_upper) lemma unat_div_distrib: \unat (v div w) = unat v div unat w\ proof transfer fix k l have \nat (take_bit LENGTH('a) k) div nat (take_bit LENGTH('a) l) \ nat (take_bit LENGTH('a) k)\ by (rule div_le_dividend) also have \nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\ by (simp add: nat_less_iff) finally show \(nat \ take_bit LENGTH('a)) (take_bit LENGTH('a) k div take_bit LENGTH('a) l) = (nat \ take_bit LENGTH('a)) k div (nat \ take_bit LENGTH('a)) l\ by (simp add: nat_take_bit_eq div_int_pos_iff nat_div_distrib take_bit_nat_eq_self_iff) qed lemma unat_mod_distrib: \unat (v mod w) = unat v mod unat w\ proof transfer fix k l have \nat (take_bit LENGTH('a) k) mod nat (take_bit LENGTH('a) l) \ nat (take_bit LENGTH('a) k)\ by (rule mod_less_eq_dividend) also have \nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\ by (simp add: nat_less_iff) finally show \(nat \ take_bit LENGTH('a)) (take_bit LENGTH('a) k mod take_bit LENGTH('a) l) = (nat \ take_bit LENGTH('a)) k mod (nat \ take_bit LENGTH('a)) l\ by (simp add: nat_take_bit_eq mod_int_pos_iff less_le nat_mod_distrib take_bit_nat_eq_self_iff) qed lemma uint_div_distrib: \uint (v div w) = uint v div uint w\ proof - have \int (unat (v div w)) = int (unat v div unat w)\ by (simp add: unat_div_distrib) then show ?thesis by (simp add: of_nat_div) qed lemma unat_drop_bit_eq: \unat (drop_bit n w) = drop_bit n (unat w)\ by (rule bit_eqI) (simp add: bit_unsigned_iff bit_drop_bit_eq) lemma uint_mod_distrib: \uint (v mod w) = uint v mod uint w\ proof - have \int (unat (v mod w)) = int (unat v mod unat w)\ by (simp add: unat_mod_distrib) then show ?thesis by (simp add: of_nat_mod) qed context semiring_bit_shifts begin lemma unsigned_ucast_eq: \unsigned (ucast w :: 'c::len word) = take_bit LENGTH('c) (unsigned w)\ for w :: \'b::len word\ by (rule bit_eqI) (simp add: bit_unsigned_iff Word.bit_unsigned_iff bit_take_bit_iff exp_eq_zero_iff not_le) end context ring_bit_operations begin lemma signed_ucast_eq: \signed (ucast w :: 'c::len word) = signed_take_bit (LENGTH('c) - Suc 0) (unsigned w)\ for w :: \'b::len word\ proof (rule bit_eqI) fix n assume \2 ^ n \ 0\ then have \2 ^ (min (LENGTH('c) - Suc 0) n) \ 0\ by (simp add: min_def) (metis (mono_tags) diff_diff_cancel exp_not_zero_imp_exp_diff_not_zero) then show \bit (signed (ucast w :: 'c::len word)) n \ bit (signed_take_bit (LENGTH('c) - Suc 0) (unsigned w)) n\ by (simp add: bit_signed_iff bit_unsigned_iff Word.bit_unsigned_iff bit_signed_take_bit_iff exp_eq_zero_iff not_le) qed lemma signed_scast_eq: \signed (scast w :: 'c::len word) = signed_take_bit (LENGTH('c) - Suc 0) (signed w)\ for w :: \'b::len word\ proof (rule bit_eqI) fix n assume \2 ^ n \ 0\ then have \2 ^ (min (LENGTH('c) - Suc 0) n) \ 0\ by (simp add: min_def) (metis (mono_tags) diff_diff_cancel exp_not_zero_imp_exp_diff_not_zero) then show \bit (signed (scast w :: 'c::len word)) n \ bit (signed_take_bit (LENGTH('c) - Suc 0) (signed w)) n\ by (simp add: bit_signed_iff bit_unsigned_iff Word.bit_signed_iff bit_signed_take_bit_iff exp_eq_zero_iff not_le) qed end lemma uint_nonnegative: "0 \ uint w" by (fact unsigned_greater_eq) lemma uint_bounded: "uint w < 2 ^ LENGTH('a)" for w :: "'a::len word" by (fact unsigned_less) lemma uint_idem: "uint w mod 2 ^ LENGTH('a) = uint w" for w :: "'a::len word" by transfer (simp add: take_bit_eq_mod) lemma word_uint_eqI: "uint a = uint b \ a = b" by (fact unsigned_word_eqI) lemma word_uint_eq_iff: "a = b \ uint a = uint b" by (fact word_eq_iff_unsigned) lemma uint_word_of_int_eq: \uint (word_of_int k :: 'a::len word) = take_bit LENGTH('a) k\ by transfer rule lemma uint_word_of_int: "uint (word_of_int k :: 'a::len word) = k mod 2 ^ LENGTH('a)" by (simp add: uint_word_of_int_eq take_bit_eq_mod) lemma word_of_int_uint: "word_of_int (uint w) = w" by transfer simp lemma word_div_def [code]: "a div b = word_of_int (uint a div uint b)" by transfer rule lemma word_mod_def [code]: "a mod b = word_of_int (uint a mod uint b)" by transfer rule lemma split_word_all: "(\x::'a::len word. PROP P x) \ (\x. PROP P (word_of_int x))" proof fix x :: "'a word" assume "\x. PROP P (word_of_int x)" then have "PROP P (word_of_int (uint x))" . then show "PROP P x" by (simp only: word_of_int_uint) qed lemma sint_uint: \sint w = signed_take_bit (LENGTH('a) - Suc 0) (uint w)\ for w :: \'a::len word\ by (cases \LENGTH('a)\; transfer) (simp_all add: signed_take_bit_take_bit) lemma unat_eq_nat_uint: \unat w = nat (uint w)\ by simp lemma ucast_eq: \ucast w = word_of_int (uint w)\ by transfer simp lemma scast_eq: \scast w = word_of_int (sint w)\ by transfer simp lemma uint_0_eq: \uint 0 = 0\ by (fact unsigned_0) lemma uint_1_eq: \uint 1 = 1\ by (fact unsigned_1) lemma word_m1_wi: "- 1 = word_of_int (- 1)" by simp lemma uint_0_iff: "uint x = 0 \ x = 0" by (auto simp add: unsigned_word_eqI) lemma unat_0_iff: "unat x = 0 \ x = 0" by (auto simp add: unsigned_word_eqI) lemma unat_0: "unat 0 = 0" by (fact unsigned_0) lemma unat_gt_0: "0 < unat x \ x \ 0" by (auto simp: unat_0_iff [symmetric]) lemma ucast_0: "ucast 0 = 0" by (fact unsigned_0) lemma sint_0: "sint 0 = 0" by (fact signed_0) lemma scast_0: "scast 0 = 0" by (fact signed_0) lemma sint_n1: "sint (- 1) = - 1" by (fact signed_minus_1) lemma scast_n1: "scast (- 1) = - 1" by (fact signed_minus_1) lemma uint_1: "uint (1::'a::len word) = 1" by (fact uint_1_eq) lemma unat_1: "unat (1::'a::len word) = 1" by (fact unsigned_1) lemma ucast_1: "ucast (1::'a::len word) = 1" by (fact unsigned_1) instantiation word :: (len) size begin lift_definition size_word :: \'a word \ nat\ is \\_. LENGTH('a)\ .. instance .. end lemma word_size [code]: \size w = LENGTH('a)\ for w :: \'a::len word\ by (fact size_word.rep_eq) lemma word_size_gt_0 [iff]: "0 < size w" for w :: "'a::len word" by (simp add: word_size) lemmas lens_gt_0 = word_size_gt_0 len_gt_0 lemma lens_not_0 [iff]: \size w \ 0\ for w :: \'a::len word\ by auto lift_definition source_size :: \('a::len word \ 'b) \ nat\ is \\_. LENGTH('a)\ . lift_definition target_size :: \('a \ 'b::len word) \ nat\ is \\_. LENGTH('b)\ .. lift_definition is_up :: \('a::len word \ 'b::len word) \ bool\ is \\_. LENGTH('a) \ LENGTH('b)\ .. lift_definition is_down :: \('a::len word \ 'b::len word) \ bool\ is \\_. LENGTH('a) \ LENGTH('b)\ .. lemma is_up_eq: \is_up f \ source_size f \ target_size f\ for f :: \'a::len word \ 'b::len word\ by (simp add: source_size.rep_eq target_size.rep_eq is_up.rep_eq) lemma is_down_eq: \is_down f \ target_size f \ source_size f\ for f :: \'a::len word \ 'b::len word\ by (simp add: source_size.rep_eq target_size.rep_eq is_down.rep_eq) lift_definition word_int_case :: \(int \ 'b) \ 'a::len word \ 'b\ is \\f. f \ take_bit LENGTH('a)\ by simp lemma word_int_case_eq_uint [code]: \word_int_case f w = f (uint w)\ by transfer simp translations "case x of XCONST of_int y \ b" \ "CONST word_int_case (\y. b) x" "case x of (XCONST of_int :: 'a) y \ b" \ "CONST word_int_case (\y. b) x" subsection \Arithmetic operations\ text \Legacy theorems:\ lemma word_add_def [code]: "a + b = word_of_int (uint a + uint b)" by transfer (simp add: take_bit_add) lemma word_sub_wi [code]: "a - b = word_of_int (uint a - uint b)" by transfer (simp add: take_bit_diff) lemma word_mult_def [code]: "a * b = word_of_int (uint a * uint b)" by transfer (simp add: take_bit_eq_mod mod_simps) lemma word_minus_def [code]: "- a = word_of_int (- uint a)" by transfer (simp add: take_bit_minus) lemma word_0_wi: "0 = word_of_int 0" by transfer simp lemma word_1_wi: "1 = word_of_int 1" by transfer simp lift_definition word_succ :: "'a::len word \ 'a word" is "\x. x + 1" by (auto simp add: take_bit_eq_mod intro: mod_add_cong) lift_definition word_pred :: "'a::len word \ 'a word" is "\x. x - 1" by (auto simp add: take_bit_eq_mod intro: mod_diff_cong) lemma word_succ_alt [code]: "word_succ a = word_of_int (uint a + 1)" by transfer (simp add: take_bit_eq_mod mod_simps) lemma word_pred_alt [code]: "word_pred a = word_of_int (uint a - 1)" by transfer (simp add: take_bit_eq_mod mod_simps) lemmas word_arith_wis = word_add_def word_sub_wi word_mult_def word_minus_def word_succ_alt word_pred_alt word_0_wi word_1_wi lemma wi_homs: shows wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" and wi_hom_sub: "word_of_int a - word_of_int b = word_of_int (a - b)" and wi_hom_mult: "word_of_int a * word_of_int b = word_of_int (a * b)" and wi_hom_neg: "- word_of_int a = word_of_int (- a)" and wi_hom_succ: "word_succ (word_of_int a) = word_of_int (a + 1)" and wi_hom_pred: "word_pred (word_of_int a) = word_of_int (a - 1)" by (transfer, simp)+ lemmas wi_hom_syms = wi_homs [symmetric] lemmas word_of_int_homs = wi_homs word_0_wi word_1_wi lemmas word_of_int_hom_syms = word_of_int_homs [symmetric] lemma double_eq_zero_iff: \2 * a = 0 \ a = 0 \ a = 2 ^ (LENGTH('a) - Suc 0)\ for a :: \'a::len word\ proof - define n where \n = LENGTH('a) - Suc 0\ then have *: \LENGTH('a) = Suc n\ by simp have \a = 0\ if \2 * a = 0\ and \a \ 2 ^ (LENGTH('a) - Suc 0)\ using that by transfer (auto simp add: take_bit_eq_0_iff take_bit_eq_mod *) moreover have \2 ^ LENGTH('a) = (0 :: 'a word)\ by transfer simp then have \2 * 2 ^ (LENGTH('a) - Suc 0) = (0 :: 'a word)\ by (simp add: *) ultimately show ?thesis by auto qed subsection \Ordering\ lift_definition word_sle :: \'a::len word \ 'a word \ bool\ is \\k l. signed_take_bit (LENGTH('a) - Suc 0) k \ signed_take_bit (LENGTH('a) - Suc 0) l\ by (simp flip: signed_take_bit_decr_length_iff) lift_definition word_sless :: \'a::len word \ 'a word \ bool\ is \\k l. signed_take_bit (LENGTH('a) - Suc 0) k < signed_take_bit (LENGTH('a) - Suc 0) l\ by (simp flip: signed_take_bit_decr_length_iff) notation word_sle ("'(\s')") and word_sle ("(_/ \s _)" [51, 51] 50) and word_sless ("'(a <=s b \ sint a \ sint b\ by transfer simp lemma [code]: \a sint a < sint b\ by transfer simp lemma signed_ordering: \ordering word_sle word_sless\ apply (standard; transfer) using signed_take_bit_decr_length_iff by force+ lemma signed_linorder: \class.linorder word_sle word_sless\ by (standard; transfer) (auto simp add: signed_take_bit_decr_length_iff) interpretation signed: linorder word_sle word_sless by (fact signed_linorder) lemma word_sless_eq: \x x <=s y \ x \ y\ by (fact signed.less_le) lemma word_less_alt: "a < b \ uint a < uint b" by (fact word_less_def) lemma word_zero_le [simp]: "0 \ y" for y :: "'a::len word" by (fact word_coorder.extremum) lemma word_m1_ge [simp] : "word_pred 0 \ y" (* FIXME: delete *) by transfer (simp add: take_bit_minus_one_eq_mask mask_eq_exp_minus_1 ) lemma word_n1_ge [simp]: "y \ -1" for y :: "'a::len word" by (fact word_order.extremum) 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" for y :: "'a::len word" by (simp add: less_le) lemmas word_gt_0_no [simp] = word_gt_0 [of "numeral y"] for y lemma word_sless_alt: "a sint a < sint b" by transfer simp lemma word_le_nat_alt: "a \ b \ unat a \ unat b" by transfer (simp add: nat_le_eq_zle) lemma word_less_nat_alt: "a < b \ unat a < unat b" by transfer (auto simp add: less_le [of 0]) lemmas unat_mono = word_less_nat_alt [THEN iffD1] instance word :: (len) wellorder proof fix P :: "'a word \ bool" and a assume *: "(\b. (\a. a < b \ P a) \ P b)" have "wf (measure unat)" .. moreover have "{(a, b :: ('a::len) word). a < b} \ measure unat" by (auto simp add: word_less_nat_alt) ultimately have "wf {(a, b :: ('a::len) word). a < b}" by (rule wf_subset) then show "P a" using * by induction blast qed lemma wi_less: "(word_of_int n < (word_of_int m :: 'a::len word)) = (n mod 2 ^ LENGTH('a) < m mod 2 ^ LENGTH('a))" by transfer (simp add: take_bit_eq_mod) lemma wi_le: "(word_of_int n \ (word_of_int m :: 'a::len word)) = (n mod 2 ^ LENGTH('a) \ m mod 2 ^ LENGTH('a))" by transfer (simp add: take_bit_eq_mod) subsection \Bit-wise operations\ lemma uint_take_bit_eq: \uint (take_bit n w) = take_bit n (uint w)\ by transfer (simp add: ac_simps) lemma take_bit_word_eq_self: \take_bit n w = w\ if \LENGTH('a) \ n\ for w :: \'a::len word\ using that by transfer simp lemma take_bit_length_eq [simp]: \take_bit LENGTH('a) w = w\ for w :: \'a::len word\ by (rule take_bit_word_eq_self) simp lemma bit_word_of_int_iff: \bit (word_of_int k :: 'a::len word) n \ n < LENGTH('a) \ bit k n\ by transfer rule lemma bit_uint_iff: \bit (uint w) n \ n < LENGTH('a) \ bit w n\ for w :: \'a::len word\ by transfer (simp add: bit_take_bit_iff) lemma bit_sint_iff: \bit (sint w) n \ n \ LENGTH('a) \ bit w (LENGTH('a) - 1) \ bit w n\ for w :: \'a::len word\ by transfer (auto simp add: bit_signed_take_bit_iff min_def le_less not_less) lemma bit_word_ucast_iff: \bit (ucast w :: 'b::len word) n \ n < LENGTH('a) \ n < LENGTH('b) \ bit w n\ for w :: \'a::len word\ by transfer (simp add: bit_take_bit_iff ac_simps) lemma bit_word_scast_iff: \bit (scast w :: 'b::len word) n \ n < LENGTH('b) \ (bit w n \ LENGTH('a) \ n \ bit w (LENGTH('a) - Suc 0))\ for w :: \'a::len word\ by transfer (auto simp add: bit_signed_take_bit_iff le_less min_def) lift_definition shiftl1 :: \'a::len word \ 'a word\ is \(*) 2\ by (auto simp add: take_bit_eq_mod intro: mod_mult_cong) lemma shiftl1_eq: \shiftl1 w = word_of_int (2 * uint w)\ by transfer (simp add: take_bit_eq_mod mod_simps) lemma shiftl1_eq_mult_2: \shiftl1 = (*) 2\ by (rule ext, transfer) simp lemma bit_shiftl1_iff [bit_simps]: \bit (shiftl1 w) n \ 0 < n \ n < LENGTH('a) \ bit w (n - 1)\ for w :: \'a::len word\ by (simp add: shiftl1_eq_mult_2 bit_double_iff not_le) (simp add: ac_simps) lift_definition shiftr1 :: \'a::len word \ 'a word\ \ \shift right as unsigned or as signed, ie logical or arithmetic\ is \\k. take_bit LENGTH('a) k div 2\ by simp lemma shiftr1_eq_div_2: \shiftr1 w = w div 2\ by transfer simp lemma bit_shiftr1_iff [bit_simps]: \bit (shiftr1 w) n \ bit w (Suc n)\ by transfer (auto simp flip: bit_Suc simp add: bit_take_bit_iff) lemma shiftr1_eq: \shiftr1 w = word_of_int (uint w div 2)\ by transfer simp lemma bit_word_iff_drop_bit_and [code]: \bit a n \ drop_bit n a AND 1 = 1\ for a :: \'a::len word\ by (simp add: bit_iff_odd_drop_bit odd_iff_mod_2_eq_one and_one_eq) lemma word_not_def: "NOT (a::'a::len word) = word_of_int (NOT (uint a))" and word_and_def: "(a::'a word) AND b = word_of_int (uint a AND uint b)" and word_or_def: "(a::'a word) OR b = word_of_int (uint a OR uint b)" and word_xor_def: "(a::'a word) XOR b = word_of_int (uint a XOR uint b)" by (transfer, simp add: take_bit_not_take_bit)+ lift_definition setBit :: \'a::len word \ nat \ 'a word\ is \\k n. set_bit n k\ by (simp add: take_bit_set_bit_eq) lemma set_Bit_eq: \setBit w n = set_bit n w\ by transfer simp lemma bit_setBit_iff [bit_simps]: \bit (setBit w m) n \ (m = n \ n < LENGTH('a) \ bit w n)\ for w :: \'a::len word\ by transfer (auto simp add: bit_set_bit_iff) lift_definition clearBit :: \'a::len word \ nat \ 'a word\ is \\k n. unset_bit n k\ by (simp add: take_bit_unset_bit_eq) lemma clear_Bit_eq: \clearBit w n = unset_bit n w\ by transfer simp lemma bit_clearBit_iff [bit_simps]: \bit (clearBit w m) n \ m \ n \ bit w n\ for w :: \'a::len word\ by transfer (auto simp add: bit_unset_bit_iff) definition even_word :: \'a::len word \ bool\ where [code_abbrev]: \even_word = even\ lemma even_word_iff [code]: \even_word a \ a AND 1 = 0\ by (simp add: and_one_eq even_iff_mod_2_eq_zero even_word_def) lemma map_bit_range_eq_if_take_bit_eq: \map (bit k) [0.. if \take_bit n k = take_bit n l\ for k l :: int using that proof (induction n arbitrary: k l) case 0 then show ?case by simp next case (Suc n) from Suc.prems have \take_bit n (k div 2) = take_bit n (l div 2)\ by (simp add: take_bit_Suc) then have \map (bit (k div 2)) [0.. by (rule Suc.IH) moreover have \bit (r div 2) = bit r \ Suc\ for r :: int by (simp add: fun_eq_iff bit_Suc) moreover from Suc.prems have \even k \ even l\ by (auto simp add: take_bit_Suc elim!: evenE oddE) arith+ ultimately show ?case by (simp only: map_Suc_upt upt_conv_Cons flip: list.map_comp) simp qed lemma take_bit_word_Bit0_eq [simp]: \take_bit (numeral n) (numeral (num.Bit0 m) :: 'a::len word) = 2 * take_bit (pred_numeral n) (numeral m)\ (is ?P) and take_bit_word_Bit1_eq [simp]: \take_bit (numeral n) (numeral (num.Bit1 m) :: 'a::len word) = 1 + 2 * take_bit (pred_numeral n) (numeral m)\ (is ?Q) and take_bit_word_minus_Bit0_eq [simp]: \take_bit (numeral n) (- numeral (num.Bit0 m) :: 'a::len word) = 2 * take_bit (pred_numeral n) (- numeral m)\ (is ?R) and take_bit_word_minus_Bit1_eq [simp]: \take_bit (numeral n) (- numeral (num.Bit1 m) :: 'a::len word) = 1 + 2 * take_bit (pred_numeral n) (- numeral (Num.inc m))\ (is ?S) proof - define w :: \'a::len word\ where \w = numeral m\ moreover define q :: nat where \q = pred_numeral n\ ultimately have num: \numeral m = w\ \numeral (num.Bit0 m) = 2 * w\ \numeral (num.Bit1 m) = 1 + 2 * w\ \numeral (Num.inc m) = 1 + w\ \pred_numeral n = q\ \numeral n = Suc q\ by (simp_all only: w_def q_def numeral_Bit0 [of m] numeral_Bit1 [of m] ac_simps numeral_inc numeral_eq_Suc flip: mult_2) have even: \take_bit (Suc q) (2 * w) = 2 * take_bit q w\ for w :: \'a::len word\ by (rule bit_word_eqI) (auto simp add: bit_take_bit_iff bit_double_iff) have odd: \take_bit (Suc q) (1 + 2 * w) = 1 + 2 * take_bit q w\ for w :: \'a::len word\ by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_double_iff even_bit_succ_iff) show ?P using even [of w] by (simp add: num) show ?Q using odd [of w] by (simp add: num) show ?R using even [of \- w\] by (simp add: num) show ?S using odd [of \- (1 + w)\] by (simp add: num) qed subsection \More shift operations\ lift_definition signed_drop_bit :: \nat \ 'a word \ 'a::len word\ is \\n. drop_bit n \ signed_take_bit (LENGTH('a) - Suc 0)\ using signed_take_bit_decr_length_iff by (simp add: take_bit_drop_bit) force lemma bit_signed_drop_bit_iff [bit_simps]: \bit (signed_drop_bit m w) n \ bit w (if LENGTH('a) - m \ n \ n < LENGTH('a) then LENGTH('a) - 1 else m + n)\ for w :: \'a::len word\ apply transfer apply (auto simp add: bit_drop_bit_eq bit_signed_take_bit_iff not_le min_def) apply (metis add.commute le_antisym less_diff_conv less_eq_decr_length_iff) apply (metis le_antisym less_eq_decr_length_iff) done lemma [code]: \Word.the_int (signed_drop_bit n w) = take_bit LENGTH('a) (drop_bit n (Word.the_signed_int w))\ for w :: \'a::len word\ by transfer simp lemma signed_drop_bit_signed_drop_bit [simp]: \signed_drop_bit m (signed_drop_bit n w) = signed_drop_bit (m + n) w\ for w :: \'a::len word\ proof (cases \LENGTH('a)\) case 0 then show ?thesis using len_not_eq_0 by blast next case (Suc n) then show ?thesis by (force simp add: bit_signed_drop_bit_iff not_le less_diff_conv ac_simps intro!: bit_word_eqI) qed lemma signed_drop_bit_0 [simp]: \signed_drop_bit 0 w = w\ by transfer (simp add: take_bit_signed_take_bit) lemma sint_signed_drop_bit_eq: \sint (signed_drop_bit n w) = drop_bit n (sint w)\ proof (cases \LENGTH('a) = 0 \ n=0\) case False then show ?thesis apply simp apply (rule bit_eqI) by (auto simp add: bit_sint_iff bit_drop_bit_eq bit_signed_drop_bit_iff dest: bit_imp_le_length) qed auto lift_definition sshiftr1 :: \'a::len word \ 'a word\ is \\k. take_bit LENGTH('a) (signed_take_bit (LENGTH('a) - Suc 0) k div 2)\ by (simp flip: signed_take_bit_decr_length_iff) lift_definition bshiftr1 :: \bool \ 'a::len word \ 'a word\ is \\b k. take_bit LENGTH('a) k div 2 + of_bool b * 2 ^ (LENGTH('a) - Suc 0)\ by (fact arg_cong) lemma sshiftr1_eq_signed_drop_bit_Suc_0: \sshiftr1 = signed_drop_bit (Suc 0)\ by (rule ext) (transfer, simp add: drop_bit_Suc) lemma sshiftr1_eq: \sshiftr1 w = word_of_int (sint w div 2)\ by transfer simp subsection \Rotation\ lift_definition word_rotr :: \nat \ 'a::len word \ 'a::len word\ is \\n k. concat_bit (LENGTH('a) - n mod LENGTH('a)) (drop_bit (n mod LENGTH('a)) (take_bit LENGTH('a) k)) (take_bit (n mod LENGTH('a)) k)\ subgoal for n k l by (simp add: concat_bit_def nat_le_iff less_imp_le take_bit_tightened [of \LENGTH('a)\ k l \n mod LENGTH('a::len)\]) done lift_definition word_rotl :: \nat \ 'a::len word \ 'a::len word\ is \\n k. concat_bit (n mod LENGTH('a)) (drop_bit (LENGTH('a) - n mod LENGTH('a)) (take_bit LENGTH('a) k)) (take_bit (LENGTH('a) - n mod LENGTH('a)) k)\ subgoal for n k l by (simp add: concat_bit_def nat_le_iff less_imp_le take_bit_tightened [of \LENGTH('a)\ k l \LENGTH('a) - n mod LENGTH('a::len)\]) done lift_definition word_roti :: \int \ 'a::len word \ 'a::len word\ is \\r k. concat_bit (LENGTH('a) - nat (r mod int LENGTH('a))) (drop_bit (nat (r mod int LENGTH('a))) (take_bit LENGTH('a) k)) (take_bit (nat (r mod int LENGTH('a))) k)\ subgoal for r k l by (simp add: concat_bit_def nat_le_iff less_imp_le take_bit_tightened [of \LENGTH('a)\ k l \nat (r mod int LENGTH('a::len))\]) done lemma word_rotl_eq_word_rotr [code]: \word_rotl n = (word_rotr (LENGTH('a) - n mod LENGTH('a)) :: 'a::len word \ 'a word)\ by (rule ext, cases \n mod LENGTH('a) = 0\; transfer) simp_all lemma word_roti_eq_word_rotr_word_rotl [code]: \word_roti i w = (if i \ 0 then word_rotr (nat i) w else word_rotl (nat (- i)) w)\ proof (cases \i \ 0\) case True moreover define n where \n = nat i\ ultimately have \i = int n\ by simp moreover have \word_roti (int n) = (word_rotr n :: _ \ 'a word)\ by (rule ext, transfer) (simp add: nat_mod_distrib) ultimately show ?thesis by simp next case False moreover define n where \n = nat (- i)\ ultimately have \i = - int n\ \n > 0\ by simp_all moreover have \word_roti (- int n) = (word_rotl n :: _ \ 'a word)\ by (rule ext, transfer) (simp add: zmod_zminus1_eq_if flip: of_nat_mod of_nat_diff) ultimately show ?thesis by simp qed lemma bit_word_rotr_iff [bit_simps]: \bit (word_rotr m w) n \ n < LENGTH('a) \ bit w ((n + m) mod LENGTH('a))\ for w :: \'a::len word\ proof transfer fix k :: int and m n :: nat define q where \q = m mod LENGTH('a)\ have \q < LENGTH('a)\ by (simp add: q_def) then have \q \ LENGTH('a)\ by simp have \m mod LENGTH('a) = q\ by (simp add: q_def) moreover have \(n + m) mod LENGTH('a) = (n + q) mod LENGTH('a)\ by (subst mod_add_right_eq [symmetric]) (simp add: \m mod LENGTH('a) = q\) moreover have \n < LENGTH('a) \ bit (concat_bit (LENGTH('a) - q) (drop_bit q (take_bit LENGTH('a) k)) (take_bit q k)) n \ n < LENGTH('a) \ bit k ((n + q) mod LENGTH('a))\ using \q < LENGTH('a)\ by (cases \q + n \ LENGTH('a)\) (auto simp add: bit_concat_bit_iff bit_drop_bit_eq bit_take_bit_iff le_mod_geq ac_simps) ultimately show \n < LENGTH('a) \ bit (concat_bit (LENGTH('a) - m mod LENGTH('a)) (drop_bit (m mod LENGTH('a)) (take_bit LENGTH('a) k)) (take_bit (m mod LENGTH('a)) k)) n \ n < LENGTH('a) \ (n + m) mod LENGTH('a) < LENGTH('a) \ bit k ((n + m) mod LENGTH('a))\ by simp qed lemma bit_word_rotl_iff [bit_simps]: \bit (word_rotl m w) n \ n < LENGTH('a) \ bit w ((n + (LENGTH('a) - m mod LENGTH('a))) mod LENGTH('a))\ for w :: \'a::len word\ by (simp add: word_rotl_eq_word_rotr bit_word_rotr_iff) lemma bit_word_roti_iff [bit_simps]: \bit (word_roti k w) n \ n < LENGTH('a) \ bit w (nat ((int n + k) mod int LENGTH('a)))\ for w :: \'a::len word\ proof transfer fix k l :: int and n :: nat define m where \m = nat (k mod int LENGTH('a))\ have \m < LENGTH('a)\ by (simp add: nat_less_iff m_def) then have \m \ LENGTH('a)\ by simp have \k mod int LENGTH('a) = int m\ by (simp add: nat_less_iff m_def) moreover have \(int n + k) mod int LENGTH('a) = int ((n + m) mod LENGTH('a))\ by (subst mod_add_right_eq [symmetric]) (simp add: of_nat_mod \k mod int LENGTH('a) = int m\) moreover have \n < LENGTH('a) \ bit (concat_bit (LENGTH('a) - m) (drop_bit m (take_bit LENGTH('a) l)) (take_bit m l)) n \ n < LENGTH('a) \ bit l ((n + m) mod LENGTH('a))\ using \m < LENGTH('a)\ by (cases \m + n \ LENGTH('a)\) (auto simp add: bit_concat_bit_iff bit_drop_bit_eq bit_take_bit_iff nat_less_iff not_le not_less ac_simps le_diff_conv le_mod_geq) ultimately show \n < LENGTH('a) \ bit (concat_bit (LENGTH('a) - nat (k mod int LENGTH('a))) (drop_bit (nat (k mod int LENGTH('a))) (take_bit LENGTH('a) l)) (take_bit (nat (k mod int LENGTH('a))) l)) n \ n < LENGTH('a) \ nat ((int n + k) mod int LENGTH('a)) < LENGTH('a) \ bit l (nat ((int n + k) mod int LENGTH('a)))\ by simp qed lemma uint_word_rotr_eq: \uint (word_rotr n w) = concat_bit (LENGTH('a) - n mod LENGTH('a)) (drop_bit (n mod LENGTH('a)) (uint w)) (uint (take_bit (n mod LENGTH('a)) w))\ for w :: \'a::len word\ apply transfer by (simp add: min.absorb2 take_bit_concat_bit_eq) lemma [code]: \Word.the_int (word_rotr n w) = concat_bit (LENGTH('a) - n mod LENGTH('a)) (drop_bit (n mod LENGTH('a)) (Word.the_int w)) (Word.the_int (take_bit (n mod LENGTH('a)) w))\ for w :: \'a::len word\ using uint_word_rotr_eq [of n w] by simp subsection \Split and cat operations\ lift_definition word_cat :: \'a::len word \ 'b::len word \ 'c::len word\ is \\k l. concat_bit LENGTH('b) l (take_bit LENGTH('a) k)\ by (simp add: bit_eq_iff bit_concat_bit_iff bit_take_bit_iff) lemma word_cat_eq: \(word_cat v w :: 'c::len word) = push_bit LENGTH('b) (ucast v) + ucast w\ for v :: \'a::len word\ and w :: \'b::len word\ by transfer (simp add: concat_bit_eq ac_simps) lemma word_cat_eq' [code]: \word_cat a b = word_of_int (concat_bit LENGTH('b) (uint b) (uint a))\ for a :: \'a::len word\ and b :: \'b::len word\ by transfer (simp add: concat_bit_take_bit_eq) lemma bit_word_cat_iff [bit_simps]: \bit (word_cat v w :: 'c::len word) n \ n < LENGTH('c) \ (if n < LENGTH('b) then bit w n else bit v (n - LENGTH('b)))\ for v :: \'a::len word\ and w :: \'b::len word\ by transfer (simp add: bit_concat_bit_iff bit_take_bit_iff) definition word_split :: \'a::len word \ 'b::len word \ 'c::len word\ where \word_split w = (ucast (drop_bit LENGTH('c) w) :: 'b::len word, ucast w :: 'c::len word)\ definition word_rcat :: \'a::len word list \ 'b::len word\ where \word_rcat = word_of_int \ horner_sum uint (2 ^ LENGTH('a)) \ rev\ subsection \More on conversions\ lemma int_word_sint: \sint (word_of_int x :: 'a::len word) = (x + 2 ^ (LENGTH('a) - 1)) mod 2 ^ LENGTH('a) - 2 ^ (LENGTH('a) - 1)\ by transfer (simp flip: take_bit_eq_mod add: signed_take_bit_eq_take_bit_shift) lemma sint_sbintrunc': "sint (word_of_int bin :: 'a word) = signed_take_bit (LENGTH('a::len) - 1) bin" by simp lemma uint_sint: "uint w = take_bit LENGTH('a) (sint w)" for w :: "'a::len word" by transfer (simp add: take_bit_signed_take_bit) lemma bintr_uint: "LENGTH('a) \ n \ take_bit n (uint w) = uint w" for w :: "'a::len word" by transfer (simp add: min_def) lemma wi_bintr: "LENGTH('a::len) \ n \ word_of_int (take_bit n w) = (word_of_int w :: 'a word)" by transfer simp lemma word_numeral_alt: "numeral b = word_of_int (numeral b)" by (induct b, simp_all only: numeral.simps word_of_int_homs) declare word_numeral_alt [symmetric, code_abbrev] lemma word_neg_numeral_alt: "- numeral b = word_of_int (- numeral b)" by (simp only: word_numeral_alt wi_hom_neg) declare word_neg_numeral_alt [symmetric, code_abbrev] lemma uint_bintrunc [simp]: "uint (numeral bin :: 'a word) = take_bit (LENGTH('a::len)) (numeral bin)" by transfer rule lemma uint_bintrunc_neg [simp]: "uint (- numeral bin :: 'a word) = take_bit (LENGTH('a::len)) (- numeral bin)" by transfer rule lemma sint_sbintrunc [simp]: "sint (numeral bin :: 'a word) = signed_take_bit (LENGTH('a::len) - 1) (numeral bin)" by transfer simp lemma sint_sbintrunc_neg [simp]: "sint (- numeral bin :: 'a word) = signed_take_bit (LENGTH('a::len) - 1) (- numeral bin)" by transfer simp lemma unat_bintrunc [simp]: "unat (numeral bin :: 'a::len word) = nat (take_bit (LENGTH('a)) (numeral bin))" by transfer simp lemma unat_bintrunc_neg [simp]: "unat (- numeral bin :: 'a::len word) = nat (take_bit (LENGTH('a)) (- numeral bin))" by transfer simp lemma size_0_eq: "size w = 0 \ v = w" for v w :: "'a::len word" by transfer simp lemma uint_ge_0 [iff]: "0 \ uint x" by (fact unsigned_greater_eq) lemma uint_lt2p [iff]: "uint x < 2 ^ LENGTH('a)" for x :: "'a::len word" by (fact unsigned_less) lemma sint_ge: "- (2 ^ (LENGTH('a) - 1)) \ sint x" for x :: "'a::len word" using sint_greater_eq [of x] by simp lemma sint_lt: "sint x < 2 ^ (LENGTH('a) - 1)" for x :: "'a::len word" using sint_less [of x] by simp lemma uint_m2p_neg: "uint x - 2 ^ LENGTH('a) < 0" for x :: "'a::len word" by (simp only: diff_less_0_iff_less uint_lt2p) lemma uint_m2p_not_non_neg: "\ 0 \ uint x - 2 ^ LENGTH('a)" for x :: "'a::len word" by (simp only: not_le uint_m2p_neg) lemma lt2p_lem: "LENGTH('a) \ n \ uint w < 2 ^ n" for w :: "'a::len word" using uint_bounded [of w] by (rule less_le_trans) simp lemma uint_le_0_iff [simp]: "uint x \ 0 \ uint x = 0" by (fact uint_ge_0 [THEN leD, THEN antisym_conv1]) lemma uint_nat: "uint w = int (unat w)" by transfer simp lemma uint_numeral: "uint (numeral b :: 'a::len word) = numeral b mod 2 ^ LENGTH('a)" by (simp flip: take_bit_eq_mod add: of_nat_take_bit) lemma uint_neg_numeral: "uint (- numeral b :: 'a::len word) = - numeral b mod 2 ^ LENGTH('a)" by (simp flip: take_bit_eq_mod add: of_nat_take_bit) lemma unat_numeral: "unat (numeral b :: 'a::len word) = numeral b mod 2 ^ LENGTH('a)" by transfer (simp add: take_bit_eq_mod nat_mod_distrib nat_power_eq) lemma sint_numeral: "sint (numeral b :: 'a::len word) = (numeral b + 2 ^ (LENGTH('a) - 1)) mod 2 ^ LENGTH('a) - 2 ^ (LENGTH('a) - 1)" by (metis int_word_sint word_numeral_alt) lemma word_of_int_0 [simp, code_post]: "word_of_int 0 = 0" by (fact of_int_0) lemma word_of_int_1 [simp, code_post]: "word_of_int 1 = 1" by (fact of_int_1) lemma word_of_int_neg_1 [simp]: "word_of_int (- 1) = - 1" by (simp add: wi_hom_syms) lemma word_of_int_numeral [simp] : "(word_of_int (numeral bin) :: 'a::len word) = numeral bin" by (fact of_int_numeral) lemma word_of_int_neg_numeral [simp]: "(word_of_int (- numeral bin) :: 'a::len word) = - numeral bin" by (fact of_int_neg_numeral) lemma word_int_case_wi: "word_int_case f (word_of_int i :: 'b word) = f (i mod 2 ^ LENGTH('b::len))" by transfer (simp add: take_bit_eq_mod) lemma word_int_split: "P (word_int_case f x) = (\i. x = (word_of_int i :: 'b::len word) \ 0 \ i \ i < 2 ^ LENGTH('b) \ P (f i))" by transfer (auto simp add: take_bit_eq_mod) lemma word_int_split_asm: "P (word_int_case f x) = (\n. x = (word_of_int n :: 'b::len word) \ 0 \ n \ n < 2 ^ LENGTH('b::len) \ \ P (f n))" by transfer (auto simp add: take_bit_eq_mod) lemma uint_range_size: "0 \ uint w \ uint w < 2 ^ size w" by transfer simp lemma sint_range_size: "- (2 ^ (size w - Suc 0)) \ sint w \ sint w < 2 ^ (size w - Suc 0)" by (simp add: word_size sint_greater_eq sint_less) lemma sint_above_size: "2 ^ (size w - 1) \ x \ sint w < x" for w :: "'a::len word" unfolding word_size by (rule less_le_trans [OF sint_lt]) lemma sint_below_size: "x \ - (2 ^ (size w - 1)) \ x \ sint w" for w :: "'a::len word" unfolding word_size by (rule order_trans [OF _ sint_ge]) subsection \Testing bits\ lemma bin_nth_uint_imp: "bit (uint w) n \ n < LENGTH('a)" for w :: "'a::len word" by transfer (simp add: bit_take_bit_iff) lemma bin_nth_sint: "LENGTH('a) \ n \ bit (sint w) n = bit (sint w) (LENGTH('a) - 1)" for w :: "'a::len word" by (transfer fixing: n) (simp add: bit_signed_take_bit_iff le_diff_conv min_def) lemma num_of_bintr': "take_bit (LENGTH('a::len)) (numeral a :: int) = (numeral b) \ numeral a = (numeral b :: 'a word)" proof (transfer fixing: a b) assume \take_bit LENGTH('a) (numeral a :: int) = numeral b\ then have \take_bit LENGTH('a) (take_bit LENGTH('a) (numeral a :: int)) = take_bit LENGTH('a) (numeral b)\ by simp then show \take_bit LENGTH('a) (numeral a :: int) = take_bit LENGTH('a) (numeral b)\ by simp qed lemma num_of_sbintr': "signed_take_bit (LENGTH('a::len) - 1) (numeral a :: int) = (numeral b) \ numeral a = (numeral b :: 'a word)" proof (transfer fixing: a b) assume \signed_take_bit (LENGTH('a) - 1) (numeral a :: int) = numeral b\ then have \take_bit LENGTH('a) (signed_take_bit (LENGTH('a) - 1) (numeral a :: int)) = take_bit LENGTH('a) (numeral b)\ by simp then show \take_bit LENGTH('a) (numeral a :: int) = take_bit LENGTH('a) (numeral b)\ by (simp add: take_bit_signed_take_bit) qed lemma num_abs_bintr: "(numeral x :: 'a word) = word_of_int (take_bit (LENGTH('a::len)) (numeral x))" by transfer simp lemma num_abs_sbintr: "(numeral x :: 'a word) = word_of_int (signed_take_bit (LENGTH('a::len) - 1) (numeral x))" by transfer (simp add: take_bit_signed_take_bit) text \ \cast\ -- note, no arg for new length, as it's determined by type of result, thus in \cast w = w\, the type means cast to length of \w\! \ lemma bit_ucast_iff: \bit (ucast a :: 'a::len word) n \ n < LENGTH('a::len) \ Parity.bit a n\ by transfer (simp add: bit_take_bit_iff) lemma ucast_id [simp]: "ucast w = w" by transfer simp lemma scast_id [simp]: "scast w = w" by transfer (simp add: take_bit_signed_take_bit) lemma ucast_mask_eq: \ucast (mask n :: 'b word) = mask (min LENGTH('b::len) n)\ by (simp add: bit_eq_iff) (auto simp add: bit_mask_iff bit_ucast_iff exp_eq_zero_iff) \ \literal u(s)cast\ lemma ucast_bintr [simp]: "ucast (numeral w :: 'a::len word) = word_of_int (take_bit (LENGTH('a)) (numeral w))" by transfer simp (* TODO: neg_numeral *) lemma scast_sbintr [simp]: "scast (numeral w ::'a::len word) = word_of_int (signed_take_bit (LENGTH('a) - Suc 0) (numeral w))" by transfer simp lemma source_size: "source_size (c::'a::len word \ _) = LENGTH('a)" by transfer simp lemma target_size: "target_size (c::_ \ 'b::len word) = LENGTH('b)" by transfer simp lemma is_down: "is_down c \ LENGTH('b) \ LENGTH('a)" for c :: "'a::len word \ 'b::len word" by transfer simp lemma is_up: "is_up c \ LENGTH('a) \ LENGTH('b)" for c :: "'a::len word \ 'b::len word" by transfer simp lemma is_up_down: \is_up c \ is_down d\ for c :: \'a::len word \ 'b::len word\ and d :: \'b::len word \ 'a::len word\ by transfer simp context fixes dummy_types :: \'a::len \ 'b::len\ begin private abbreviation (input) UCAST :: \'a::len word \ 'b::len word\ where \UCAST == ucast\ private abbreviation (input) SCAST :: \'a::len word \ 'b::len word\ where \SCAST == scast\ lemma down_cast_same: \UCAST = scast\ if \is_down UCAST\ by (rule ext, use that in transfer) (simp add: take_bit_signed_take_bit) lemma sint_up_scast: \sint (SCAST w) = sint w\ if \is_up SCAST\ using that by transfer (simp add: min_def Suc_leI le_diff_iff) lemma uint_up_ucast: \uint (UCAST w) = uint w\ if \is_up UCAST\ using that by transfer (simp add: min_def) lemma ucast_up_ucast: \ucast (UCAST w) = ucast w\ if \is_up UCAST\ using that by transfer (simp add: ac_simps) lemma ucast_up_ucast_id: \ucast (UCAST w) = w\ if \is_up UCAST\ using that by (simp add: ucast_up_ucast) lemma scast_up_scast: \scast (SCAST w) = scast w\ if \is_up SCAST\ using that by transfer (simp add: ac_simps) lemma scast_up_scast_id: \scast (SCAST w) = w\ if \is_up SCAST\ using that by (simp add: scast_up_scast) lemma isduu: \is_up UCAST\ if \is_down d\ for d :: \'b word \ 'a word\ using that is_up_down [of UCAST d] by simp lemma isdus: \is_up SCAST\ if \is_down d\ for d :: \'b word \ 'a word\ using that is_up_down [of SCAST d] by simp lemmas ucast_down_ucast_id = isduu [THEN ucast_up_ucast_id] lemmas scast_down_scast_id = isdus [THEN scast_up_scast_id] lemma up_ucast_surj: \surj (ucast :: 'b word \ 'a word)\ if \is_up UCAST\ by (rule surjI) (use that in \rule ucast_up_ucast_id\) lemma up_scast_surj: \surj (scast :: 'b word \ 'a word)\ if \is_up SCAST\ by (rule surjI) (use that in \rule scast_up_scast_id\) lemma down_ucast_inj: \inj_on UCAST A\ if \is_down (ucast :: 'b word \ 'a word)\ by (rule inj_on_inverseI) (use that in \rule ucast_down_ucast_id\) lemma down_scast_inj: \inj_on SCAST A\ if \is_down (scast :: 'b word \ 'a word)\ by (rule inj_on_inverseI) (use that in \rule scast_down_scast_id\) lemma ucast_down_wi: \UCAST (word_of_int x) = word_of_int x\ if \is_down UCAST\ using that by transfer simp lemma ucast_down_no: \UCAST (numeral bin) = numeral bin\ if \is_down UCAST\ using that by transfer simp end lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def lemma bit_last_iff: \bit w (LENGTH('a) - Suc 0) \ sint w < 0\ (is \?P \ ?Q\) for w :: \'a::len word\ proof - have \?P \ bit (uint w) (LENGTH('a) - Suc 0)\ by (simp add: bit_uint_iff) also have \\ \ ?Q\ by (simp add: sint_uint) finally show ?thesis . qed lemma drop_bit_eq_zero_iff_not_bit_last: \drop_bit (LENGTH('a) - Suc 0) w = 0 \ \ bit w (LENGTH('a) - Suc 0)\ for w :: "'a::len word" proof (cases \LENGTH('a)\) case (Suc n) then show ?thesis apply transfer apply (simp add: take_bit_drop_bit) by (simp add: bit_iff_odd_drop_bit drop_bit_take_bit min.absorb2 odd_iff_mod_2_eq_one) qed auto subsection \Word Arithmetic\ lemmas word_div_no [simp] = word_div_def [of "numeral a" "numeral b"] for a b lemmas word_mod_no [simp] = word_mod_def [of "numeral a" "numeral b"] for a b lemmas word_less_no [simp] = word_less_def [of "numeral a" "numeral b"] for a b lemmas word_le_no [simp] = word_le_def [of "numeral a" "numeral b"] for a b lemmas word_sless_no [simp] = word_sless_eq [of "numeral a" "numeral b"] for a b lemmas word_sle_no [simp] = word_sle_eq [of "numeral a" "numeral b"] for a b lemma size_0_same': "size w = 0 \ w = v" for v w :: "'a::len word" by (unfold word_size) simp lemmas size_0_same = size_0_same' [unfolded word_size] lemmas unat_eq_0 = unat_0_iff lemmas unat_eq_zero = unat_0_iff subsection \Transferring goals from words to ints\ lemma word_ths: shows word_succ_p1: "word_succ a = a + 1" and word_pred_m1: "word_pred a = a - 1" and word_pred_succ: "word_pred (word_succ a) = a" and word_succ_pred: "word_succ (word_pred a) = a" and word_mult_succ: "word_succ a * b = b + a * b" by (transfer, simp add: algebra_simps)+ lemma uint_cong: "x = y \ uint x = uint y" by simp lemma uint_word_ariths: fixes a b :: "'a::len word" shows "uint (a + b) = (uint a + uint b) mod 2 ^ LENGTH('a::len)" and "uint (a - b) = (uint a - uint b) mod 2 ^ LENGTH('a)" and "uint (a * b) = uint a * uint b mod 2 ^ LENGTH('a)" and "uint (- a) = - uint a mod 2 ^ LENGTH('a)" and "uint (word_succ a) = (uint a + 1) mod 2 ^ LENGTH('a)" and "uint (word_pred a) = (uint a - 1) mod 2 ^ LENGTH('a)" and "uint (0 :: 'a word) = 0 mod 2 ^ LENGTH('a)" and "uint (1 :: 'a word) = 1 mod 2 ^ LENGTH('a)" by (simp_all only: word_arith_wis uint_word_of_int_eq flip: take_bit_eq_mod) lemma uint_word_arith_bintrs: fixes a b :: "'a::len word" shows "uint (a + b) = take_bit (LENGTH('a)) (uint a + uint b)" and "uint (a - b) = take_bit (LENGTH('a)) (uint a - uint b)" and "uint (a * b) = take_bit (LENGTH('a)) (uint a * uint b)" and "uint (- a) = take_bit (LENGTH('a)) (- uint a)" and "uint (word_succ a) = take_bit (LENGTH('a)) (uint a + 1)" and "uint (word_pred a) = take_bit (LENGTH('a)) (uint a - 1)" and "uint (0 :: 'a word) = take_bit (LENGTH('a)) 0" and "uint (1 :: 'a word) = take_bit (LENGTH('a)) 1" by (simp_all add: uint_word_ariths take_bit_eq_mod) lemma sint_word_ariths: fixes a b :: "'a::len word" shows "sint (a + b) = signed_take_bit (LENGTH('a) - 1) (sint a + sint b)" and "sint (a - b) = signed_take_bit (LENGTH('a) - 1) (sint a - sint b)" and "sint (a * b) = signed_take_bit (LENGTH('a) - 1) (sint a * sint b)" and "sint (- a) = signed_take_bit (LENGTH('a) - 1) (- sint a)" and "sint (word_succ a) = signed_take_bit (LENGTH('a) - 1) (sint a + 1)" and "sint (word_pred a) = signed_take_bit (LENGTH('a) - 1) (sint a - 1)" and "sint (0 :: 'a word) = signed_take_bit (LENGTH('a) - 1) 0" and "sint (1 :: 'a word) = signed_take_bit (LENGTH('a) - 1) 1" subgoal by transfer (simp add: signed_take_bit_add) subgoal by transfer (simp add: signed_take_bit_diff) subgoal by transfer (simp add: signed_take_bit_mult) subgoal by transfer (simp add: signed_take_bit_minus) apply (metis of_int_sint scast_id sint_sbintrunc' wi_hom_succ) apply (metis of_int_sint scast_id sint_sbintrunc' wi_hom_pred) apply (simp_all add: sint_uint) done lemma word_pred_0_n1: "word_pred 0 = word_of_int (- 1)" unfolding word_pred_m1 by simp lemma succ_pred_no [simp]: "word_succ (numeral w) = numeral w + 1" "word_pred (numeral w) = numeral w - 1" "word_succ (- numeral w) = - numeral w + 1" "word_pred (- numeral w) = - numeral w - 1" by (simp_all add: word_succ_p1 word_pred_m1) lemma word_sp_01 [simp]: "word_succ (- 1) = 0 \ word_succ 0 = 1 \ word_pred 0 = - 1 \ word_pred 1 = 0" by (simp_all add: word_succ_p1 word_pred_m1) \ \alternative approach to lifting arithmetic equalities\ lemma word_of_int_Ex: "\y. x = word_of_int y" by (rule_tac x="uint x" in exI) simp subsection \Order on fixed-length words\ lift_definition udvd :: \'a::len word \ 'a::len word \ bool\ (infixl \udvd\ 50) is \\k l. take_bit LENGTH('a) k dvd take_bit LENGTH('a) l\ by simp lemma udvd_iff_dvd: \x udvd y \ unat x dvd unat y\ by transfer (simp add: nat_dvd_iff) lemma udvd_iff_dvd_int: \v udvd w \ uint v dvd uint w\ by transfer rule lemma udvdI [intro]: \v udvd w\ if \unat w = unat v * unat u\ proof - from that have \unat v dvd unat w\ .. then show ?thesis by (simp add: udvd_iff_dvd) qed lemma udvdE [elim]: fixes v w :: \'a::len word\ assumes \v udvd w\ obtains u :: \'a word\ where \unat w = unat v * unat u\ proof (cases \v = 0\) case True moreover from True \v udvd w\ have \w = 0\ by transfer simp ultimately show thesis using that by simp next case False then have \unat v > 0\ by (simp add: unat_gt_0) from \v udvd w\ have \unat v dvd unat w\ by (simp add: udvd_iff_dvd) then obtain n where \unat w = unat v * n\ .. moreover have \n < 2 ^ LENGTH('a)\ proof (rule ccontr) assume \\ n < 2 ^ LENGTH('a)\ then have \n \ 2 ^ LENGTH('a)\ by (simp add: not_le) then have \unat v * n \ 2 ^ LENGTH('a)\ using \unat v > 0\ mult_le_mono [of 1 \unat v\ \2 ^ LENGTH('a)\ n] by simp with \unat w = unat v * n\ have \unat w \ 2 ^ LENGTH('a)\ by simp with unsigned_less [of w, where ?'a = nat] show False by linarith qed ultimately have \unat w = unat v * unat (word_of_nat n :: 'a word)\ by (auto simp add: take_bit_nat_eq_self_iff intro: sym) with that show thesis . qed lemma udvd_imp_mod_eq_0: \w mod v = 0\ if \v udvd w\ using that by transfer simp lemma mod_eq_0_imp_udvd [intro?]: \v udvd w\ if \w mod v = 0\ proof - from that have \unat (w mod v) = unat 0\ by simp then have \unat w mod unat v = 0\ by (simp add: unat_mod_distrib) then have \unat v dvd unat w\ .. then show ?thesis by (simp add: udvd_iff_dvd) qed lemma udvd_imp_dvd: \v dvd w\ if \v udvd w\ for v w :: \'a::len word\ proof - from that obtain u :: \'a word\ where \unat w = unat v * unat u\ .. then have \(word_of_nat (unat w) :: 'a word) = word_of_nat (unat v * unat u)\ by simp then have \w = v * u\ by simp then show \v dvd w\ .. qed lemma exp_dvd_iff_exp_udvd: \2 ^ n dvd w \ 2 ^ n udvd w\ for v w :: \'a::len word\ proof assume \2 ^ n udvd w\ then show \2 ^ n dvd w\ by (rule udvd_imp_dvd) next assume \2 ^ n dvd w\ then obtain u :: \'a word\ where \w = 2 ^ n * u\ .. then have \w = push_bit n u\ by (simp add: push_bit_eq_mult) then show \2 ^ n udvd w\ by transfer (simp add: take_bit_push_bit dvd_eq_mod_eq_0 flip: take_bit_eq_mod) qed lemma udvd_nat_alt: \a udvd b \ (\n. unat b = n * unat a)\ by (auto simp add: udvd_iff_dvd) lemma udvd_unfold_int: \a udvd b \ (\n\0. uint b = n * uint a)\ unfolding udvd_iff_dvd_int by (metis dvd_div_mult_self dvd_triv_right uint_div_distrib uint_ge_0) lemma unat_minus_one: \unat (w - 1) = unat w - 1\ if \w \ 0\ proof - have "0 \ uint w" by (fact uint_nonnegative) moreover from that have "0 \ uint w" by (simp add: uint_0_iff) ultimately have "1 \ uint w" by arith from uint_lt2p [of w] have "uint w - 1 < 2 ^ LENGTH('a)" by arith with \1 \ uint w\ have "(uint w - 1) mod 2 ^ LENGTH('a) = uint w - 1" by (auto intro: mod_pos_pos_trivial) with \1 \ uint w\ have "nat ((uint w - 1) mod 2 ^ LENGTH('a)) = nat (uint w) - 1" by (auto simp del: nat_uint_eq) then show ?thesis by (simp only: unat_eq_nat_uint word_arith_wis mod_diff_right_eq) (metis of_int_1 uint_word_of_int unsigned_1) qed lemma measure_unat: "p \ 0 \ unat (p - 1) < unat p" by (simp add: unat_minus_one) (simp add: unat_0_iff [symmetric]) lemmas uint_add_ge0 [simp] = add_nonneg_nonneg [OF uint_ge_0 uint_ge_0] lemmas uint_mult_ge0 [simp] = mult_nonneg_nonneg [OF uint_ge_0 uint_ge_0] lemma uint_sub_lt2p [simp]: "uint x - uint y < 2 ^ LENGTH('a)" for x :: "'a::len word" and y :: "'b::len word" 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 ^ LENGTH('a)) = (uint (x + y) = uint x + uint y)" for x y :: "'a::len word" by (metis add.right_neutral add_mono_thms_linordered_semiring(1) mod_pos_pos_trivial of_nat_0_le_iff uint_lt2p uint_nat uint_word_ariths(1)) lemma uint_mult_lem: "(uint x * uint y < 2 ^ LENGTH('a)) = (uint (x * y) = uint x * uint y)" for x y :: "'a::len word" by (metis mod_pos_pos_trivial uint_lt2p uint_mult_ge0 uint_word_ariths(3)) lemma uint_sub_lem: "uint x \ uint y \ uint (x - y) = uint x - uint y" by (metis diff_ge_0_iff_ge of_nat_0_le_iff uint_nat uint_sub_lt2p uint_word_of_int unique_euclidean_semiring_numeral_class.mod_less word_sub_wi) lemma uint_add_le: "uint (x + y) \ uint x + uint y" unfolding uint_word_ariths by (simp add: zmod_le_nonneg_dividend) lemma uint_sub_ge: "uint (x - y) \ uint x - uint y" unfolding uint_word_ariths by (simp flip: take_bit_eq_mod add: take_bit_int_greater_eq_self_iff) lemma int_mod_ge: \a \ a mod n\ if \a < n\ \0 < n\ for a n :: int proof (cases \a < 0\) case True with \0 < n\ show ?thesis by (metis less_trans not_less pos_mod_conj) next case False with \a < n\ show ?thesis by simp qed lemma mod_add_if_z: "\x < z; y < z; 0 \ y; 0 \ x; 0 \ z\ \ (x + y) mod z = (if x + y < z then x + y else x + y - z)" for x y z :: int apply (simp add: not_less) by (metis (no_types) add_strict_mono diff_ge_0_iff_ge diff_less_eq minus_mod_self2 mod_pos_pos_trivial) lemma uint_plus_if': "uint (a + b) = (if uint a + uint b < 2 ^ LENGTH('a) then uint a + uint b else uint a + uint b - 2 ^ LENGTH('a))" for a b :: "'a::len word" using mod_add_if_z [of "uint a" _ "uint b"] by (simp add: uint_word_ariths) lemma mod_sub_if_z: "\x < z; y < z; 0 \ y; 0 \ x; 0 \ z\ \ (x - y) mod z = (if y \ x then x - y else x - y + z)" for x y z :: int using mod_pos_pos_trivial [of "x - y + z" z] by (auto simp add: not_le) lemma uint_sub_if': "uint (a - b) = (if uint b \ uint a then uint a - uint b else uint a - uint b + 2 ^ LENGTH('a))" for a b :: "'a::len word" using mod_sub_if_z [of "uint a" _ "uint b"] by (simp add: uint_word_ariths) subsection \Definition of \uint_arith\\ lemma word_of_int_inverse: "word_of_int r = a \ 0 \ r \ r < 2 ^ LENGTH('a) \ uint a = r" for a :: "'a::len word" by transfer (simp add: take_bit_int_eq_self) lemma uint_split: "P (uint x) = (\i. word_of_int i = x \ 0 \ i \ i < 2^LENGTH('a) \ P i)" for x :: "'a::len word" by transfer (auto simp add: take_bit_eq_mod) lemma uint_split_asm: "P (uint x) = (\i. word_of_int i = x \ 0 \ i \ i < 2^LENGTH('a) \ \ P i)" for x :: "'a::len word" by auto (metis take_bit_int_eq_self_iff) lemmas uint_splits = uint_split uint_split_asm lemmas uint_arith_simps = word_le_def word_less_alt word_uint_eq_iff uint_sub_if' uint_plus_if' \ \use this to stop, eg. \2 ^ LENGTH(32)\ being simplified\ lemma power_False_cong: "False \ a ^ b = c ^ d" by auto \ \\uint_arith_tac\: reduce to arithmetic on int, try to solve by arith\ ML \ val uint_arith_simpset = @{context} |> fold Simplifier.add_simp @{thms uint_arith_simps} |> fold Splitter.add_split @{thms if_split_asm} |> fold Simplifier.add_cong @{thms power_False_cong} |> simpset_of; fun uint_arith_tacs ctxt = let fun arith_tac' n t = Arith_Data.arith_tac ctxt n t handle Cooper.COOPER _ => Seq.empty; in [ clarify_tac ctxt 1, full_simp_tac (put_simpset uint_arith_simpset ctxt) 1, ALLGOALS (full_simp_tac (put_simpset HOL_ss ctxt |> fold Splitter.add_split @{thms uint_splits} |> fold Simplifier.add_cong @{thms power_False_cong})), rewrite_goals_tac ctxt @{thms word_size}, ALLGOALS (fn n => REPEAT (resolve_tac ctxt [allI, impI] n) THEN REPEAT (eresolve_tac ctxt [conjE] n) THEN REPEAT (dresolve_tac ctxt @{thms word_of_int_inverse} n THEN assume_tac ctxt n THEN assume_tac ctxt n)), TRYALL arith_tac' ] end fun uint_arith_tac ctxt = SELECT_GOAL (EVERY (uint_arith_tacs ctxt)) \ method_setup uint_arith = \Scan.succeed (SIMPLE_METHOD' o uint_arith_tac)\ "solving word arithmetic via integers and arith" subsection \More on overflows and monotonicity\ lemma no_plus_overflow_uint_size: "x \ x + y \ uint x + uint y < 2 ^ size x" for x y :: "'a::len word" unfolding word_size by uint_arith lemmas no_olen_add = no_plus_overflow_uint_size [unfolded word_size] lemma no_ulen_sub: "x \ x - y \ uint y \ uint x" for x y :: "'a::len word" by uint_arith lemma no_olen_add': "x \ y + x \ uint y + uint x < 2 ^ LENGTH('a)" for x y :: "'a::len word" by (simp add: ac_simps no_olen_add) lemmas olen_add_eqv = trans [OF no_olen_add no_olen_add' [symmetric]] lemmas uint_plus_simple_iff = trans [OF no_olen_add uint_add_lem] lemmas uint_plus_simple = uint_plus_simple_iff [THEN iffD1] lemmas uint_minus_simple_iff = trans [OF no_ulen_sub uint_sub_lem] lemmas uint_minus_simple_alt = uint_sub_lem [folded word_le_def] lemmas word_sub_le_iff = no_ulen_sub [folded word_le_def] lemmas word_sub_le = word_sub_le_iff [THEN iffD2] lemma word_less_sub1: "x \ 0 \ 1 < x \ 0 < x - 1" for x :: "'a::len word" by uint_arith lemma word_le_sub1: "x \ 0 \ 1 \ x \ 0 \ x - 1" for x :: "'a::len word" by uint_arith lemma sub_wrap_lt: "x < x - z \ x < z" for x z :: "'a::len word" by uint_arith lemma sub_wrap: "x \ x - z \ z = 0 \ x < z" for x z :: "'a::len word" by uint_arith lemma plus_minus_not_NULL_ab: "x \ ab - c \ c \ ab \ c \ 0 \ x + c \ 0" for x ab c :: "'a::len word" by uint_arith lemma plus_minus_no_overflow_ab: "x \ ab - c \ c \ ab \ x \ x + c" for x ab c :: "'a::len word" by uint_arith lemma le_minus': "a + c \ b \ a \ a + c \ c \ b - a" for a b c :: "'a::len word" by uint_arith lemma le_plus': "a \ b \ c \ b - a \ a + c \ b" for a b c :: "'a::len word" by uint_arith lemmas le_plus = le_plus' [rotated] lemmas le_minus = leD [THEN thin_rl, THEN le_minus'] (* FIXME *) lemma word_plus_mono_right: "y \ z \ x \ x + z \ x + y \ x + z" for x y z :: "'a::len word" by uint_arith lemma word_less_minus_cancel: "y - x < z - x \ x \ z \ y < z" for x y z :: "'a::len word" by uint_arith lemma word_less_minus_mono_left: "y < z \ x \ y \ y - x < z - x" for x y z :: "'a::len word" by uint_arith lemma word_less_minus_mono: "a < c \ d < b \ a - b < a \ c - d < c \ a - b < c - d" for a b c d :: "'a::len word" by uint_arith lemma word_le_minus_cancel: "y - x \ z - x \ x \ z \ y \ z" for x y z :: "'a::len word" by uint_arith lemma word_le_minus_mono_left: "y \ z \ x \ y \ y - x \ z - x" for x y z :: "'a::len word" by uint_arith lemma word_le_minus_mono: "a \ c \ d \ b \ a - b \ a \ c - d \ c \ a - b \ c - d" for a b c d :: "'a::len word" by uint_arith lemma plus_le_left_cancel_wrap: "x + y' < x \ x + y < x \ x + y' < x + y \ y' < y" for x y y' :: "'a::len word" by uint_arith lemma plus_le_left_cancel_nowrap: "x \ x + y' \ x \ x + y \ x + y' < x + y \ y' < y" for x y y' :: "'a::len word" by uint_arith lemma word_plus_mono_right2: "a \ a + b \ c \ b \ a \ a + c" for a b c :: "'a::len word" by uint_arith lemma word_less_add_right: "x < y - z \ z \ y \ x + z < y" for x y z :: "'a::len word" by uint_arith lemma word_less_sub_right: "x < y + z \ y \ x \ x - y < z" for x y z :: "'a::len word" by uint_arith lemma word_le_plus_either: "x \ y \ x \ z \ y \ y + z \ x \ y + z" for x y z :: "'a::len word" by uint_arith lemma word_less_nowrapI: "x < z - k \ k \ z \ 0 < k \ x < x + k" for x z k :: "'a::len word" by uint_arith lemma inc_le: "i < m \ i + 1 \ m" for i m :: "'a::len word" by uint_arith lemma inc_i: "1 \ i \ i < m \ 1 \ i + 1 \ i + 1 \ m" for i m :: "'a::len word" by uint_arith lemma udvd_incr_lem: "up < uq \ up = ua + n * uint K \ uq = ua + n' * uint K \ up + uint K \ uq" by auto (metis int_distrib(1) linorder_not_less mult.left_neutral mult_right_mono uint_nonnegative zless_imp_add1_zle) lemma udvd_incr': "p < q \ uint p = ua + n * uint K \ uint q = ua + n' * uint K \ p + K \ q" unfolding word_less_alt word_le_def by (metis (full_types) order_trans udvd_incr_lem uint_add_le) lemma udvd_decr': assumes "p < q" "uint p = ua + n * uint K" "uint q = ua + n' * uint K" shows "uint q = ua + n' * uint K \ p \ q - K" proof - have "\w wa. uint (w::'a word) \ uint wa + uint (w - wa)" by (metis (no_types) add_diff_cancel_left' diff_add_cancel uint_add_le) moreover have "uint K + uint p \ uint q" using assms by (metis (no_types) add_diff_cancel_left' diff_add_cancel udvd_incr_lem word_less_def) ultimately show ?thesis by (meson add_le_cancel_left order_trans word_less_eq_iff_unsigned) qed lemmas udvd_incr_lem0 = udvd_incr_lem [where ua=0, unfolded add_0_left] lemmas udvd_incr0 = udvd_incr' [where ua=0, unfolded add_0_left] lemmas udvd_decr0 = udvd_decr' [where ua=0, unfolded add_0_left] lemma udvd_minus_le': "xy < k \ z udvd xy \ z udvd k \ xy \ k - z" unfolding udvd_unfold_int by (meson udvd_decr0) lemma udvd_incr2_K: "p < a + s \ a \ a + s \ K udvd s \ K udvd p - a \ a \ p \ 0 < K \ p \ p + K \ p + K \ a + s" unfolding udvd_unfold_int apply (simp add: uint_arith_simps split: if_split_asm) apply (metis (no_types, hide_lams) le_add_diff_inverse le_less_trans udvd_incr_lem) using uint_lt2p [of s] by simp subsection \Arithmetic type class instantiations\ lemmas word_le_0_iff [simp] = word_zero_le [THEN leD, THEN antisym_conv1] lemma word_of_int_nat: "0 \ x \ word_of_int x = of_nat (nat x)" by simp text \ note that \iszero_def\ is only for class \comm_semiring_1_cancel\, which requires word length \\ 1\, ie \'a::len word\ \ lemma iszero_word_no [simp]: "iszero (numeral bin :: 'a::len word) = iszero (take_bit LENGTH('a) (numeral bin :: int))" by (metis iszero_def uint_0_iff uint_bintrunc) text \Use \iszero\ to simplify equalities between word numerals.\ lemmas word_eq_numeral_iff_iszero [simp] = eq_numeral_iff_iszero [where 'a="'a::len word"] subsection \Word and nat\ lemma word_nchotomy: "\w :: 'a::len word. \n. w = of_nat n \ n < 2 ^ LENGTH('a)" by (metis of_nat_unat ucast_id unsigned_less) lemma of_nat_eq: "of_nat n = w \ (\q. n = unat w + q * 2 ^ LENGTH('a))" for w :: "'a::len word" using mod_div_mult_eq [of n "2 ^ LENGTH('a)", symmetric] by (auto simp flip: take_bit_eq_mod) lemma of_nat_eq_size: "of_nat n = w \ (\q. n = unat w + q * 2 ^ size w)" unfolding word_size by (rule of_nat_eq) lemma of_nat_0: "of_nat m = (0::'a::len word) \ (\q. m = q * 2 ^ LENGTH('a))" by (simp add: of_nat_eq) lemma of_nat_2p [simp]: "of_nat (2 ^ LENGTH('a)) = (0::'a::len word)" by (fact mult_1 [symmetric, THEN iffD2 [OF of_nat_0 exI]]) lemma of_nat_gt_0: "of_nat k \ 0 \ 0 < k" by (cases k) auto lemma of_nat_neq_0: "0 < k \ k < 2 ^ LENGTH('a::len) \ of_nat k \ (0 :: 'a word)" by (auto simp add : of_nat_0) lemma Abs_fnat_hom_add: "of_nat a + of_nat b = of_nat (a + b)" by simp lemma Abs_fnat_hom_mult: "of_nat a * of_nat b = (of_nat (a * b) :: 'a::len word)" by (simp add: wi_hom_mult) lemma Abs_fnat_hom_Suc: "word_succ (of_nat a) = of_nat (Suc a)" by transfer (simp add: ac_simps) lemma Abs_fnat_hom_0: "(0::'a::len word) = of_nat 0" by simp lemma Abs_fnat_hom_1: "(1::'a::len word) = of_nat (Suc 0)" by simp lemmas Abs_fnat_homs = Abs_fnat_hom_add Abs_fnat_hom_mult Abs_fnat_hom_Suc Abs_fnat_hom_0 Abs_fnat_hom_1 lemma word_arith_nat_add: "a + b = of_nat (unat a + unat b)" by simp lemma word_arith_nat_mult: "a * b = of_nat (unat a * unat b)" by simp lemma word_arith_nat_Suc: "word_succ a = of_nat (Suc (unat a))" by (subst Abs_fnat_hom_Suc [symmetric]) simp lemma word_arith_nat_div: "a div b = of_nat (unat a div unat b)" by (metis of_int_of_nat_eq of_nat_unat of_nat_div word_div_def) lemma word_arith_nat_mod: "a mod b = of_nat (unat a mod unat b)" by (metis of_int_of_nat_eq of_nat_mod of_nat_unat word_mod_def) lemmas word_arith_nat_defs = word_arith_nat_add word_arith_nat_mult word_arith_nat_Suc Abs_fnat_hom_0 Abs_fnat_hom_1 word_arith_nat_div word_arith_nat_mod lemma unat_cong: "x = y \ unat x = unat y" by (fact arg_cong) lemma unat_of_nat: \unat (word_of_nat x :: 'a::len word) = x mod 2 ^ LENGTH('a)\ by transfer (simp flip: take_bit_eq_mod add: nat_take_bit_eq) lemmas unat_word_ariths = word_arith_nat_defs [THEN trans [OF unat_cong unat_of_nat]] lemmas word_sub_less_iff = word_sub_le_iff [unfolded linorder_not_less [symmetric] Not_eq_iff] lemma unat_add_lem: "unat x + unat y < 2 ^ LENGTH('a) \ unat (x + y) = unat x + unat y" for x y :: "'a::len word" by (metis mod_less unat_word_ariths(1) unsigned_less) lemma unat_mult_lem: "unat x * unat y < 2 ^ LENGTH('a) \ unat (x * y) = unat x * unat y" for x y :: "'a::len word" by (metis mod_less unat_word_ariths(2) unsigned_less) lemma unat_plus_if': \unat (a + b) = (if unat a + unat b < 2 ^ LENGTH('a) then unat a + unat b else unat a + unat b - 2 ^ LENGTH('a))\ for a b :: \'a::len word\ apply (auto simp: unat_word_ariths not_less le_iff_add) by (metis add.commute add_less_cancel_right add_strict_mono mod_less unsigned_less) lemma le_no_overflow: "x \ b \ a \ a + b \ x \ a + b" for a b x :: "'a::len word" using word_le_plus_either by blast lemmas un_ui_le = trans [OF word_le_nat_alt [symmetric] word_le_def] lemma unat_sub_if_size: "unat (x - y) = (if unat y \ unat x then unat x - unat y else unat x + 2 ^ size x - unat y)" proof - { assume xy: "\ uint y \ uint x" have "nat (uint x - uint y + 2 ^ LENGTH('a)) = nat (uint x + 2 ^ LENGTH('a) - uint y)" by simp also have "... = nat (uint x + 2 ^ LENGTH('a)) - nat (uint y)" by (simp add: nat_diff_distrib') also have "... = nat (uint x) + 2 ^ LENGTH('a) - nat (uint y)" by (metis nat_add_distrib nat_eq_numeral_power_cancel_iff order_less_imp_le unsigned_0 unsigned_greater_eq unsigned_less) finally have "nat (uint x - uint y + 2 ^ LENGTH('a)) = nat (uint x) + 2 ^ LENGTH('a) - nat (uint y)" . } then show ?thesis unfolding word_size by (metis nat_diff_distrib' uint_sub_if' un_ui_le unat_eq_nat_uint unsigned_greater_eq) qed lemmas unat_sub_if' = unat_sub_if_size [unfolded word_size] lemma uint_div: \uint (x div y) = uint x div uint y\ by (fact uint_div_distrib) lemma unat_div: \unat (x div y) = unat x div unat y\ by (fact unat_div_distrib) lemma uint_mod: \uint (x mod y) = uint x mod uint y\ by (fact uint_mod_distrib) lemma unat_mod: \unat (x mod y) = unat x mod unat y\ by (fact unat_mod_distrib) text \Definition of \unat_arith\ tactic\ lemma unat_split: "P (unat x) \ (\n. of_nat n = x \ n < 2^LENGTH('a) \ P n)" for x :: "'a::len word" by auto (metis take_bit_nat_eq_self_iff) lemma unat_split_asm: "P (unat x) \ (\n. of_nat n = x \ n < 2^LENGTH('a) \ \ P n)" for x :: "'a::len word" by auto (metis take_bit_nat_eq_self_iff) lemma of_nat_inverse: \word_of_nat r = a \ r < 2 ^ LENGTH('a) \ unat a = r\ for a :: \'a::len word\ by (metis mod_if unat_of_nat) lemma word_unat_eq_iff: \v = w \ unat v = unat w\ for v w :: \'a::len word\ by (fact word_eq_iff_unsigned) lemmas unat_splits = unat_split unat_split_asm lemmas unat_arith_simps = word_le_nat_alt word_less_nat_alt word_unat_eq_iff unat_sub_if' unat_plus_if' unat_div unat_mod \ \\unat_arith_tac\: tactic to reduce word arithmetic to \nat\, try to solve via \arith\\ ML \ val unat_arith_simpset = @{context} (* TODO: completely explicitly determined simpset *) |> fold Simplifier.del_simp @{thms unsigned_of_nat unsigned_of_int} |> fold Simplifier.add_simp @{thms unat_arith_simps} |> fold Splitter.add_split @{thms if_split_asm} |> fold Simplifier.add_cong @{thms power_False_cong} |> simpset_of fun unat_arith_tacs ctxt = let fun arith_tac' n t = Arith_Data.arith_tac ctxt n t handle Cooper.COOPER _ => Seq.empty; in [ clarify_tac ctxt 1, full_simp_tac (put_simpset unat_arith_simpset ctxt) 1, ALLGOALS (full_simp_tac (put_simpset HOL_ss ctxt |> fold Splitter.add_split @{thms unat_splits} |> fold Simplifier.add_cong @{thms power_False_cong})), rewrite_goals_tac ctxt @{thms word_size}, ALLGOALS (fn n => REPEAT (resolve_tac ctxt [allI, impI] n) THEN REPEAT (eresolve_tac ctxt [conjE] n) THEN REPEAT (dresolve_tac ctxt @{thms of_nat_inverse} n THEN assume_tac ctxt n)), TRYALL arith_tac' ] end fun unat_arith_tac ctxt = SELECT_GOAL (EVERY (unat_arith_tacs ctxt)) \ method_setup unat_arith = \Scan.succeed (SIMPLE_METHOD' o unat_arith_tac)\ "solving word arithmetic via natural numbers and arith" lemma no_plus_overflow_unat_size: "x \ x + y \ unat x + unat y < 2 ^ size x" for x y :: "'a::len word" unfolding word_size by unat_arith lemmas no_olen_add_nat = no_plus_overflow_unat_size [unfolded word_size] lemmas unat_plus_simple = trans [OF no_olen_add_nat unat_add_lem] lemma word_div_mult: "\0 < y; unat x * unat y < 2 ^ LENGTH('a)\ \ x * y div y = x" for x y :: "'a::len word" by (simp add: unat_eq_zero unat_mult_lem word_arith_nat_div) lemma div_lt': "i \ k div x \ unat i * unat x < 2 ^ LENGTH('a)" for i k x :: "'a::len word" by unat_arith (meson le_less_trans less_mult_imp_div_less not_le unsigned_less) lemmas div_lt'' = order_less_imp_le [THEN div_lt'] lemma div_lt_mult: "\i < k div x; 0 < x\ \ i * x < k" for i k x :: "'a::len word" by (metis div_le_mono div_lt'' not_le unat_div word_div_mult word_less_iff_unsigned) lemma div_le_mult: "\i \ k div x; 0 < x\ \ i * x \ k" for i k x :: "'a::len word" by (metis div_lt' less_mult_imp_div_less not_less unat_arith_simps(2) unat_div unat_mult_lem) lemma div_lt_uint': "i \ k div x \ uint i * uint x < 2 ^ LENGTH('a)" for i k x :: "'a::len word" unfolding uint_nat by (metis div_lt' int_ops(7) of_nat_unat uint_mult_lem unat_mult_lem) lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint'] lemma word_le_exists': "x \ y \ \z. y = x + z \ uint x + uint z < 2 ^ LENGTH('a)" for x y z :: "'a::len word" by (metis add.commute diff_add_cancel no_olen_add) lemmas plus_minus_not_NULL = order_less_imp_le [THEN plus_minus_not_NULL_ab] lemmas plus_minus_no_overflow = order_less_imp_le [THEN plus_minus_no_overflow_ab] lemmas mcs = word_less_minus_cancel word_less_minus_mono_left word_le_minus_cancel word_le_minus_mono_left lemmas word_l_diffs = mcs [where y = "w + x", unfolded add_diff_cancel] for w x lemmas word_diff_ls = mcs [where z = "w + x", unfolded add_diff_cancel] for w x lemmas word_plus_mcs = word_diff_ls [where y = "v + x", unfolded add_diff_cancel] for v x lemma le_unat_uoi: \y \ unat z \ unat (word_of_nat y :: 'a word) = y\ for z :: \'a::len word\ by transfer (simp add: nat_take_bit_eq take_bit_nat_eq_self_iff le_less_trans) lemmas thd = times_div_less_eq_dividend lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend lemma word_mod_div_equality: "(n div b) * b + (n mod b) = n" for n b :: "'a::len word" by (fact div_mult_mod_eq) lemma word_div_mult_le: "a div b * b \ a" for a b :: "'a::len word" by (metis div_le_mult mult_not_zero order.not_eq_order_implies_strict order_refl word_zero_le) lemma word_mod_less_divisor: "0 < n \ m mod n < n" for m n :: "'a::len word" by (simp add: unat_arith_simps) lemma word_of_int_power_hom: "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a::len word)" by (induct n) (simp_all add: wi_hom_mult [symmetric]) lemma word_arith_power_alt: "a ^ n = (word_of_int (uint a ^ n) :: 'a::len word)" by (simp add : word_of_int_power_hom [symmetric]) lemma unatSuc: "1 + n \ 0 \ unat (1 + n) = Suc (unat n)" for n :: "'a::len word" by unat_arith subsection \Cardinality, finiteness of set of words\ lemma inj_on_word_of_int: \inj_on (word_of_int :: int \ 'a word) {0..<2 ^ LENGTH('a::len)}\ unfolding inj_on_def by (metis atLeastLessThan_iff word_of_int_inverse) lemma range_uint: \range (uint :: 'a word \ int) = {0..<2 ^ LENGTH('a::len)}\ apply transfer apply (auto simp add: image_iff) apply (metis take_bit_int_eq_self_iff) done lemma UNIV_eq: \(UNIV :: 'a word set) = word_of_int ` {0..<2 ^ LENGTH('a::len)}\ by (auto simp add: image_iff) (metis atLeastLessThan_iff linorder_not_le uint_split) lemma card_word: "CARD('a word) = 2 ^ LENGTH('a::len)" by (simp add: UNIV_eq card_image inj_on_word_of_int) lemma card_word_size: "CARD('a word) = 2 ^ size x" for x :: "'a::len word" unfolding word_size by (rule card_word) instance word :: (len) finite by standard (simp add: UNIV_eq) subsection \Bitwise Operations on Words\ lemma word_wi_log_defs: "NOT (word_of_int a) = word_of_int (NOT a)" "word_of_int a AND word_of_int b = word_of_int (a AND b)" "word_of_int a OR word_of_int b = word_of_int (a OR b)" "word_of_int a XOR word_of_int b = word_of_int (a XOR b)" by (transfer, rule refl)+ lemma word_no_log_defs [simp]: "NOT (numeral a) = word_of_int (NOT (numeral a))" "NOT (- numeral a) = word_of_int (NOT (- numeral a))" "numeral a AND numeral b = word_of_int (numeral a AND numeral b)" "numeral a AND - numeral b = word_of_int (numeral a AND - numeral b)" "- numeral a AND numeral b = word_of_int (- numeral a AND numeral b)" "- numeral a AND - numeral b = word_of_int (- numeral a AND - numeral b)" "numeral a OR numeral b = word_of_int (numeral a OR numeral b)" "numeral a OR - numeral b = word_of_int (numeral a OR - numeral b)" "- numeral a OR numeral b = word_of_int (- numeral a OR numeral b)" "- numeral a OR - numeral b = word_of_int (- numeral a OR - numeral b)" "numeral a XOR numeral b = word_of_int (numeral a XOR numeral b)" "numeral a XOR - numeral b = word_of_int (numeral a XOR - numeral b)" "- numeral a XOR numeral b = word_of_int (- numeral a XOR numeral b)" "- numeral a XOR - numeral b = word_of_int (- numeral a XOR - numeral b)" by (transfer, rule refl)+ text \Special cases for when one of the arguments equals 1.\ lemma word_bitwise_1_simps [simp]: "NOT (1::'a::len word) = -2" "1 AND numeral b = word_of_int (1 AND numeral b)" "1 AND - numeral b = word_of_int (1 AND - numeral b)" "numeral a AND 1 = word_of_int (numeral a AND 1)" "- numeral a AND 1 = word_of_int (- numeral a AND 1)" "1 OR numeral b = word_of_int (1 OR numeral b)" "1 OR - numeral b = word_of_int (1 OR - numeral b)" "numeral a OR 1 = word_of_int (numeral a OR 1)" "- numeral a OR 1 = word_of_int (- numeral a OR 1)" "1 XOR numeral b = word_of_int (1 XOR numeral b)" "1 XOR - numeral b = word_of_int (1 XOR - numeral b)" "numeral a XOR 1 = word_of_int (numeral a XOR 1)" "- numeral a XOR 1 = word_of_int (- numeral a XOR 1)" by (transfer, simp)+ text \Special cases for when one of the arguments equals -1.\ lemma word_bitwise_m1_simps [simp]: "NOT (-1::'a::len word) = 0" "(-1::'a::len word) AND x = x" "x AND (-1::'a::len word) = x" "(-1::'a::len word) OR x = -1" "x OR (-1::'a::len word) = -1" " (-1::'a::len word) XOR x = NOT x" "x XOR (-1::'a::len word) = NOT x" by (transfer, simp)+ lemma uint_and: \uint (x AND y) = uint x AND uint y\ by transfer simp lemma uint_or: \uint (x OR y) = uint x OR uint y\ by transfer simp lemma uint_xor: \uint (x XOR y) = uint x XOR uint y\ by transfer simp \ \get from commutativity, associativity etc of \int_and\ etc to same for \word_and etc\\ lemmas bwsimps = wi_hom_add word_wi_log_defs lemma word_bw_assocs: "(x AND y) AND z = x AND y AND z" "(x OR y) OR z = x OR y OR z" "(x XOR y) XOR z = x XOR y XOR z" for x :: "'a::len word" by (fact ac_simps)+ lemma word_bw_comms: "x AND y = y AND x" "x OR y = y OR x" "x XOR y = y XOR x" for x :: "'a::len word" by (fact ac_simps)+ lemma word_bw_lcs: "y AND x AND z = x AND y AND z" "y OR x OR z = x OR y OR z" "y XOR x XOR z = x XOR y XOR z" for x :: "'a::len word" by (fact ac_simps)+ lemma word_log_esimps: "x AND 0 = 0" "x AND -1 = x" "x OR 0 = x" "x OR -1 = -1" "x XOR 0 = x" "x XOR -1 = NOT x" "0 AND x = 0" "-1 AND x = x" "0 OR x = x" "-1 OR x = -1" "0 XOR x = x" "-1 XOR x = NOT x" for x :: "'a::len word" by simp_all lemma word_not_dist: "NOT (x OR y) = NOT x AND NOT y" "NOT (x AND y) = NOT x OR NOT y" for x :: "'a::len word" by simp_all lemma word_bw_same: "x AND x = x" "x OR x = x" "x XOR x = 0" for x :: "'a::len word" by simp_all lemma word_ao_absorbs [simp]: "x AND (y OR x) = x" "x OR y AND x = x" "x AND (x OR y) = x" "y AND x OR x = x" "(y OR x) AND x = x" "x OR x AND y = x" "(x OR y) AND x = x" "x AND y OR x = x" for x :: "'a::len word" by (auto intro: bit_eqI simp add: bit_and_iff bit_or_iff) lemma word_not_not [simp]: "NOT (NOT x) = x" for x :: "'a::len word" by (fact bit.double_compl) lemma word_ao_dist: "(x OR y) AND z = x AND z OR y AND z" for x :: "'a::len word" by (fact bit.conj_disj_distrib2) lemma word_oa_dist: "x AND y OR z = (x OR z) AND (y OR z)" for x :: "'a::len word" by (fact bit.disj_conj_distrib2) lemma word_add_not [simp]: "x + NOT x = -1" for x :: "'a::len word" by (simp add: not_eq_complement) lemma word_plus_and_or [simp]: "(x AND y) + (x OR y) = x + y" for x :: "'a::len word" by transfer (simp add: plus_and_or) lemma leoa: "w = x OR y \ y = w AND y" for x :: "'a::len word" by auto lemma leao: "w' = x' AND y' \ x' = x' OR w'" for x' :: "'a::len word" by auto lemma word_ao_equiv: "w = w OR w' \ w' = w AND w'" for w w' :: "'a::len word" by (auto intro: leoa leao) lemma le_word_or2: "x \ x OR y" for x y :: "'a::len word" by (simp add: or_greater_eq uint_or word_le_def) lemmas le_word_or1 = xtrans(3) [OF word_bw_comms (2) le_word_or2] lemmas word_and_le1 = xtrans(3) [OF word_ao_absorbs (4) [symmetric] le_word_or2] lemmas word_and_le2 = xtrans(3) [OF word_ao_absorbs (8) [symmetric] le_word_or2] lemma bit_horner_sum_bit_word_iff [bit_simps]: \bit (horner_sum of_bool (2 :: 'a::len word) bs) n \ n < min LENGTH('a) (length bs) \ bs ! n\ by transfer (simp add: bit_horner_sum_bit_iff) definition word_reverse :: \'a::len word \ 'a word\ where \word_reverse w = horner_sum of_bool 2 (rev (map (bit w) [0.. lemma bit_word_reverse_iff [bit_simps]: \bit (word_reverse w) n \ n < LENGTH('a) \ bit w (LENGTH('a) - Suc n)\ for w :: \'a::len word\ by (cases \n < LENGTH('a)\) (simp_all add: word_reverse_def bit_horner_sum_bit_word_iff rev_nth) lemma word_rev_rev [simp] : "word_reverse (word_reverse w) = w" by (rule bit_word_eqI) (auto simp add: bit_word_reverse_iff bit_imp_le_length Suc_diff_Suc) lemma word_rev_gal: "word_reverse w = u \ word_reverse u = w" by (metis word_rev_rev) lemma word_rev_gal': "u = word_reverse w \ w = word_reverse u" by simp lemma uint_2p: "(0::'a::len word) < 2 ^ n \ uint (2 ^ n::'a::len word) = 2 ^ n" by (cases \n < LENGTH('a)\; transfer; force) lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a::len word) = 2 ^ n" by (induct n) (simp_all add: wi_hom_syms) subsection \Shifting, Rotating, and Splitting Words\ lemma shiftl1_wi [simp]: "shiftl1 (word_of_int w) = word_of_int (2 * w)" by transfer simp lemma shiftl1_numeral [simp]: "shiftl1 (numeral w) = numeral (Num.Bit0 w)" unfolding word_numeral_alt shiftl1_wi by simp lemma shiftl1_neg_numeral [simp]: "shiftl1 (- numeral w) = - numeral (Num.Bit0 w)" unfolding word_neg_numeral_alt shiftl1_wi by simp lemma shiftl1_0 [simp] : "shiftl1 0 = 0" by transfer simp lemma shiftl1_def_u: "shiftl1 w = word_of_int (2 * uint w)" by (fact shiftl1_eq) lemma shiftl1_def_s: "shiftl1 w = word_of_int (2 * sint w)" by (simp add: shiftl1_def_u wi_hom_syms) lemma shiftr1_0 [simp]: "shiftr1 0 = 0" by transfer simp lemma sshiftr1_0 [simp]: "sshiftr1 0 = 0" by transfer simp lemma sshiftr1_n1 [simp]: "sshiftr1 (- 1) = - 1" by transfer simp text \ see paper page 10, (1), (2), \shiftr1_def\ is of the form of (1), where \f\ (ie \_ div 2\) takes normal arguments to normal results, thus we get (2) from (1) \ lemma uint_shiftr1: "uint (shiftr1 w) = uint w div 2" using drop_bit_eq_div [of 1 \uint w\, symmetric] by transfer (simp add: drop_bit_take_bit min_def) lemma bit_sshiftr1_iff [bit_simps]: \bit (sshiftr1 w) n \ bit w (if n = LENGTH('a) - 1 then LENGTH('a) - 1 else Suc n)\ for w :: \'a::len word\ apply transfer by (auto simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def le_Suc_eq simp flip: bit_Suc) lemma shiftr1_div_2: "uint (shiftr1 w) = uint w div 2" by (fact uint_shiftr1) lemma sshiftr1_div_2: "sint (sshiftr1 w) = sint w div 2" using sint_signed_drop_bit_eq [of 1 w] by (simp add: drop_bit_Suc sshiftr1_eq_signed_drop_bit_Suc_0) lemma bit_bshiftr1_iff [bit_simps]: \bit (bshiftr1 b w) n \ b \ n = LENGTH('a) - 1 \ bit w (Suc n)\ for w :: \'a::len word\ apply transfer apply (subst disjunctive_add) apply (auto simp add: bit_take_bit_iff bit_or_iff bit_exp_iff simp flip: bit_Suc) done subsubsection \shift functions in terms of lists of bools\ lemma shiftl1_rev: "shiftl1 w = word_reverse (shiftr1 (word_reverse w))" by (intro bit_word_eqI) (auto simp add: bit_shiftl1_iff bit_word_reverse_iff bit_shiftr1_iff Suc_diff_Suc) \ \note -- the following results use \'a::len word < number_ring\\ lemma shiftl1_2t: "shiftl1 w = 2 * w" for w :: "'a::len word" by (simp add: shiftl1_eq wi_hom_mult [symmetric]) lemma shiftl1_p: "shiftl1 w = w + w" for w :: "'a::len word" by (simp add: shiftl1_2t) lemma shiftr1_bintr [simp]: "(shiftr1 (numeral w) :: 'a::len word) = word_of_int (take_bit LENGTH('a) (numeral w) div 2)" by transfer simp lemma sshiftr1_sbintr [simp]: "(sshiftr1 (numeral w) :: 'a::len word) = word_of_int (signed_take_bit (LENGTH('a) - 1) (numeral w) div 2)" by transfer simp text \TODO: rules for \<^term>\- (numeral n)\\ lemma drop_bit_word_numeral [simp]: \drop_bit (numeral n) (numeral k) = (word_of_int (drop_bit (numeral n) (take_bit LENGTH('a) (numeral k))) :: 'a::len word)\ by transfer simp lemma False_map2_or: "\set xs \ {False}; length ys = length xs\ \ map2 (\) xs ys = ys" by (induction xs arbitrary: ys) (auto simp: length_Suc_conv) lemma align_lem_or: assumes "length xs = n + m" "length ys = n + m" and "drop m xs = replicate n False" "take m ys = replicate m False" shows "map2 (\) xs ys = take m xs @ drop m ys" using assms proof (induction xs arbitrary: ys m) case (Cons a xs) then show ?case by (cases m) (auto simp: length_Suc_conv False_map2_or) qed auto lemma False_map2_and: "\set xs \ {False}; length ys = length xs\ \ map2 (\) xs ys = xs" by (induction xs arbitrary: ys) (auto simp: length_Suc_conv) lemma align_lem_and: assumes "length xs = n + m" "length ys = n + m" and "drop m xs = replicate n False" "take m ys = replicate m False" shows "map2 (\) xs ys = replicate (n + m) False" using assms proof (induction xs arbitrary: ys m) case (Cons a xs) then show ?case by (cases m) (auto simp: length_Suc_conv set_replicate_conv_if False_map2_and) qed auto subsubsection \Mask\ lemma minus_1_eq_mask: \- 1 = (mask LENGTH('a) :: 'a::len word)\ by (rule bit_eqI) (simp add: bit_exp_iff bit_mask_iff exp_eq_zero_iff) lemma mask_eq_decr_exp: \mask n = 2 ^ n - (1 :: 'a::len word)\ by (fact mask_eq_exp_minus_1) lemma mask_Suc_rec: \mask (Suc n) = 2 * mask n + (1 :: 'a::len word)\ by (simp add: mask_eq_exp_minus_1) context begin qualified lemma bit_mask_iff [bit_simps]: \bit (mask m :: 'a::len word) n \ n < min LENGTH('a) m\ by (simp add: bit_mask_iff exp_eq_zero_iff not_le) end lemma mask_bin: "mask n = word_of_int (take_bit n (- 1))" by transfer (simp add: take_bit_minus_one_eq_mask) lemma and_mask_bintr: "w AND mask n = word_of_int (take_bit n (uint w))" by transfer (simp add: ac_simps take_bit_eq_mask) lemma and_mask_wi: "word_of_int i AND mask n = word_of_int (take_bit n i)" by (auto simp add: and_mask_bintr min_def not_le wi_bintr) lemma and_mask_wi': "word_of_int i AND mask n = (word_of_int (take_bit (min LENGTH('a) n) i) :: 'a::len word)" by (auto simp add: and_mask_wi min_def wi_bintr) lemma and_mask_no: "numeral i AND mask n = word_of_int (take_bit n (numeral i))" unfolding word_numeral_alt by (rule and_mask_wi) lemma and_mask_mod_2p: "w AND mask n = word_of_int (uint w mod 2 ^ n)" by (simp only: and_mask_bintr take_bit_eq_mod) lemma uint_mask_eq: \uint (mask n :: 'a::len word) = mask (min LENGTH('a) n)\ by transfer simp lemma and_mask_lt_2p: "uint (w AND mask n) < 2 ^ n" by (metis take_bit_eq_mask take_bit_int_less_exp unsigned_take_bit_eq) lemma mask_eq_iff: "w AND mask n = w \ uint w < 2 ^ n" apply (auto simp flip: take_bit_eq_mask) apply (metis take_bit_int_eq_self_iff uint_take_bit_eq) apply (simp add: take_bit_int_eq_self unsigned_take_bit_eq word_uint_eqI) done lemma and_mask_dvd: "2 ^ n dvd uint w \ w AND mask n = 0" by (simp flip: take_bit_eq_mask take_bit_eq_mod unsigned_take_bit_eq add: dvd_eq_mod_eq_0 uint_0_iff) lemma and_mask_dvd_nat: "2 ^ n dvd unat w \ w AND mask n = 0" by (simp flip: take_bit_eq_mask take_bit_eq_mod unsigned_take_bit_eq add: dvd_eq_mod_eq_0 unat_0_iff uint_0_iff) lemma word_2p_lem: "n < size w \ w < 2 ^ n = (uint w < 2 ^ n)" for w :: "'a::len word" by transfer simp lemma less_mask_eq: fixes x :: "'a::len word" assumes "x < 2 ^ n" shows "x AND mask n = x" by (metis (no_types) assms lt2p_lem mask_eq_iff not_less word_2p_lem word_size) lemmas mask_eq_iff_w2p = trans [OF mask_eq_iff word_2p_lem [symmetric]] lemmas and_mask_less' = iffD2 [OF word_2p_lem and_mask_lt_2p, simplified word_size] lemma and_mask_less_size: "n < size x \ x AND mask n < 2 ^ n" for x :: \'a::len word\ unfolding word_size by (erule and_mask_less') lemma word_mod_2p_is_mask [OF refl]: "c = 2 ^ n \ c > 0 \ x mod c = x AND mask n" for c x :: "'a::len word" by (auto simp: word_mod_def uint_2p and_mask_mod_2p) lemma mask_eqs: "(a AND mask n) + b AND mask n = a + b AND mask n" "a + (b AND mask n) AND mask n = a + b AND mask n" "(a AND mask n) - b AND mask n = a - b AND mask n" "a - (b AND mask n) AND mask n = a - b AND mask n" "a * (b AND mask n) AND mask n = a * b AND mask n" "(b AND mask n) * a AND mask n = b * a AND mask n" "(a AND mask n) + (b AND mask n) AND mask n = a + b AND mask n" "(a AND mask n) - (b AND mask n) AND mask n = a - b AND mask n" "(a AND mask n) * (b AND mask n) AND mask n = a * b AND mask n" "- (a AND mask n) AND mask n = - a AND mask n" "word_succ (a AND mask n) AND mask n = word_succ a AND mask n" "word_pred (a AND mask n) AND mask n = word_pred a AND mask n" using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b] unfolding take_bit_eq_mask [symmetric] by (transfer; simp add: take_bit_eq_mod mod_simps)+ lemma mask_power_eq: "(x AND mask n) ^ k AND mask n = x ^ k AND mask n" for x :: \'a::len word\ using word_of_int_Ex [where x=x] unfolding take_bit_eq_mask [symmetric] by (transfer; simp add: take_bit_eq_mod mod_simps)+ lemma mask_full [simp]: "mask LENGTH('a) = (- 1 :: 'a::len word)" by transfer (simp add: take_bit_minus_one_eq_mask) subsubsection \Slices\ definition slice1 :: \nat \ 'a::len word \ 'b::len word\ where \slice1 n w = (if n < LENGTH('a) then ucast (drop_bit (LENGTH('a) - n) w) else push_bit (n - LENGTH('a)) (ucast w))\ lemma bit_slice1_iff [bit_simps]: \bit (slice1 m w :: 'b::len word) n \ m - LENGTH('a) \ n \ n < min LENGTH('b) m \ bit w (n + (LENGTH('a) - m) - (m - LENGTH('a)))\ for w :: \'a::len word\ by (auto simp add: slice1_def bit_ucast_iff bit_drop_bit_eq bit_push_bit_iff not_less not_le ac_simps dest: bit_imp_le_length) definition slice :: \nat \ 'a::len word \ 'b::len word\ where \slice n = slice1 (LENGTH('a) - n)\ lemma bit_slice_iff [bit_simps]: \bit (slice m w :: 'b::len word) n \ n < min LENGTH('b) (LENGTH('a) - m) \ bit w (n + LENGTH('a) - (LENGTH('a) - m))\ for w :: \'a::len word\ by (simp add: slice_def word_size bit_slice1_iff) lemma slice1_0 [simp] : "slice1 n 0 = 0" unfolding slice1_def by simp lemma slice_0 [simp] : "slice n 0 = 0" unfolding slice_def by auto lemma ucast_slice1: "ucast w = slice1 (size w) w" unfolding slice1_def by (simp add: size_word.rep_eq) lemma ucast_slice: "ucast w = slice 0 w" by (simp add: slice_def slice1_def) lemma slice_id: "slice 0 t = t" by (simp only: ucast_slice [symmetric] ucast_id) lemma rev_slice1: \slice1 n (word_reverse w :: 'b::len word) = word_reverse (slice1 k w :: 'a::len word)\ if \n + k = LENGTH('a) + LENGTH('b)\ proof (rule bit_word_eqI) fix m assume *: \m < LENGTH('a)\ from that have **: \LENGTH('b) = n + k - LENGTH('a)\ by simp show \bit (slice1 n (word_reverse w :: 'b word) :: 'a word) m \ bit (word_reverse (slice1 k w :: 'a word)) m\ unfolding bit_slice1_iff bit_word_reverse_iff using * ** by (cases \n \ LENGTH('a)\; cases \k \ LENGTH('a)\) auto qed lemma rev_slice: "n + k + LENGTH('a::len) = LENGTH('b::len) \ slice n (word_reverse (w::'b word)) = word_reverse (slice k w :: 'a word)" unfolding slice_def word_size by (simp add: rev_slice1) subsubsection \Revcast\ definition revcast :: \'a::len word \ 'b::len word\ where \revcast = slice1 LENGTH('b)\ lemma bit_revcast_iff [bit_simps]: \bit (revcast w :: 'b::len word) n \ LENGTH('b) - LENGTH('a) \ n \ n < LENGTH('b) \ bit w (n + (LENGTH('a) - LENGTH('b)) - (LENGTH('b) - LENGTH('a)))\ for w :: \'a::len word\ by (simp add: revcast_def bit_slice1_iff) lemma revcast_slice1 [OF refl]: "rc = revcast w \ slice1 (size rc) w = rc" by (simp add: revcast_def word_size) lemma revcast_rev_ucast [OF refl refl refl]: "cs = [rc, uc] \ rc = revcast (word_reverse w) \ uc = ucast w \ rc = word_reverse uc" by (metis rev_slice1 revcast_slice1 ucast_slice1 word_size) lemma revcast_ucast: "revcast w = word_reverse (ucast (word_reverse w))" using revcast_rev_ucast [of "word_reverse w"] by simp lemma ucast_revcast: "ucast w = word_reverse (revcast (word_reverse w))" by (fact revcast_rev_ucast [THEN word_rev_gal']) lemma ucast_rev_revcast: "ucast (word_reverse w) = word_reverse (revcast w)" by (fact revcast_ucast [THEN word_rev_gal']) text "linking revcast and cast via shift" lemmas wsst_TYs = source_size target_size word_size lemmas sym_notr = not_iff [THEN iffD2, THEN not_sym, THEN not_iff [THEN iffD1]] subsection \Split and cat\ lemmas word_split_bin' = word_split_def lemmas word_cat_bin' = word_cat_eq \ \this odd result is analogous to \ucast_id\, result to the length given by the result type\ lemma word_cat_id: "word_cat a b = b" by transfer (simp add: take_bit_concat_bit_eq) lemma word_cat_split_alt: "\size w \ size u + size v; word_split w = (u,v)\ \ word_cat u v = w" unfolding word_split_def by (rule bit_word_eqI) (auto simp add: bit_word_cat_iff not_less word_size bit_ucast_iff bit_drop_bit_eq) lemmas word_cat_split_size = sym [THEN [2] word_cat_split_alt [symmetric]] subsubsection \Split and slice\ lemma split_slices: assumes "word_split w = (u, v)" shows "u = slice (size v) w \ v = slice 0 w" unfolding word_size proof (intro conjI) have \
: "\n. \ucast (drop_bit LENGTH('b) w) = u; LENGTH('c) < LENGTH('b)\ \ \ bit u n" by (metis bit_take_bit_iff bit_word_of_int_iff diff_is_0_eq' drop_bit_take_bit less_imp_le less_nat_zero_code of_int_uint unsigned_drop_bit_eq) show "u = slice LENGTH('b) w" proof (rule bit_word_eqI) show "bit u n = bit ((slice LENGTH('b) w)::'a word) n" if "n < LENGTH('a)" for n using assms bit_imp_le_length unfolding word_split_def bit_slice_iff by (fastforce simp add: \
ac_simps word_size bit_ucast_iff bit_drop_bit_eq) qed show "v = slice 0 w" by (metis Pair_inject assms ucast_slice word_split_bin') qed lemma slice_cat1 [OF refl]: "\wc = word_cat a b; size a + size b \ size wc\ \ slice (size b) wc = a" by (rule bit_word_eqI) (auto simp add: bit_slice_iff bit_word_cat_iff word_size) lemmas slice_cat2 = trans [OF slice_id word_cat_id] lemma cat_slices: "\a = slice n c; b = slice 0 c; n = size b; size c \ size a + size b\ \ word_cat a b = c" by (rule bit_word_eqI) (auto simp add: bit_slice_iff bit_word_cat_iff word_size) lemma word_split_cat_alt: assumes "w = word_cat u v" and size: "size u + size v \ size w" shows "word_split w = (u,v)" proof - have "ucast ((drop_bit LENGTH('c) (word_cat u v))::'a word) = u" "ucast ((word_cat u v)::'a word) = v" using assms by (auto simp add: word_size bit_ucast_iff bit_drop_bit_eq bit_word_cat_iff intro: bit_eqI) then show ?thesis by (simp add: assms(1) word_split_bin') qed lemma horner_sum_uint_exp_Cons_eq: \horner_sum uint (2 ^ LENGTH('a)) (w # ws) = concat_bit LENGTH('a) (uint w) (horner_sum uint (2 ^ LENGTH('a)) ws)\ for ws :: \'a::len word list\ by (simp add: bintr_uint concat_bit_eq push_bit_eq_mult) lemma bit_horner_sum_uint_exp_iff: \bit (horner_sum uint (2 ^ LENGTH('a)) ws) n \ n div LENGTH('a) < length ws \ bit (ws ! (n div LENGTH('a))) (n mod LENGTH('a))\ for ws :: \'a::len word list\ proof (induction ws arbitrary: n) case Nil then show ?case by simp next case (Cons w ws) then show ?case by (cases \n \ LENGTH('a)\) (simp_all only: horner_sum_uint_exp_Cons_eq, simp_all add: bit_concat_bit_iff le_div_geq le_mod_geq bit_uint_iff Cons) qed subsection \Rotation\ lemma word_rotr_word_rotr_eq: \word_rotr m (word_rotr n w) = word_rotr (m + n) w\ by (rule bit_word_eqI) (simp add: bit_word_rotr_iff ac_simps mod_add_right_eq) lemma word_rot_lem: "\l + k = d + k mod l; n < l\ \ ((d + n) mod l) = n" for l::nat by (metis (no_types, lifting) add.commute add.right_neutral add_diff_cancel_left' mod_if mod_mult_div_eq mod_mult_self2 mod_self) lemma word_rot_rl [simp]: \word_rotl k (word_rotr k v) = v\ proof (rule bit_word_eqI) show "bit (word_rotl k (word_rotr k v)) n = bit v n" if "n < LENGTH('a)" for n using that by (auto simp: word_rot_lem word_rotl_eq_word_rotr word_rotr_word_rotr_eq bit_word_rotr_iff algebra_simps split: nat_diff_split) qed lemma word_rot_lr [simp]: \word_rotr k (word_rotl k v) = v\ proof (rule bit_word_eqI) show "bit (word_rotr k (word_rotl k v)) n = bit v n" if "n < LENGTH('a)" for n using that by (auto simp add: word_rot_lem word_rotl_eq_word_rotr word_rotr_word_rotr_eq bit_word_rotr_iff algebra_simps split: nat_diff_split) qed lemma word_rot_gal: \word_rotr n v = w \ word_rotl n w = v\ by auto lemma word_rot_gal': \w = word_rotr n v \ v = word_rotl n w\ by auto lemma word_rotr_rev: \word_rotr n w = word_reverse (word_rotl n (word_reverse w))\ proof (rule bit_word_eqI) fix m assume \m < LENGTH('a)\ moreover have \1 + ((int m + int n mod int LENGTH('a)) mod int LENGTH('a) + ((int LENGTH('a) * 2) mod int LENGTH('a) - (1 + (int m + int n mod int LENGTH('a)))) mod int LENGTH('a)) = int LENGTH('a)\ apply (cases \(1 + (int m + int n mod int LENGTH('a))) mod int LENGTH('a) = 0\) using zmod_zminus1_eq_if [of \1 + (int m + int n mod int LENGTH('a))\ \int LENGTH('a)\] apply simp_all apply (auto simp add: algebra_simps) apply (metis (mono_tags, hide_lams) Abs_fnat_hom_add mod_Suc mod_mult_self2_is_0 of_nat_Suc of_nat_mod semiring_char_0_class.of_nat_neq_0) apply (metis (no_types, hide_lams) Abs_fnat_hom_add less_not_refl mod_Suc of_nat_Suc of_nat_gt_0 of_nat_mod) done then have \int ((m + n) mod LENGTH('a)) = int (LENGTH('a) - Suc ((LENGTH('a) - Suc m + LENGTH('a) - n mod LENGTH('a)) mod LENGTH('a)))\ using \m < LENGTH('a)\ by (simp only: of_nat_mod mod_simps) (simp add: of_nat_diff of_nat_mod Suc_le_eq add_less_mono algebra_simps mod_simps) then have \(m + n) mod LENGTH('a) = LENGTH('a) - Suc ((LENGTH('a) - Suc m + LENGTH('a) - n mod LENGTH('a)) mod LENGTH('a))\ by simp ultimately show \bit (word_rotr n w) m \ bit (word_reverse (word_rotl n (word_reverse w))) m\ by (simp add: word_rotl_eq_word_rotr bit_word_rotr_iff bit_word_reverse_iff) qed lemma word_roti_0 [simp]: "word_roti 0 w = w" by transfer simp lemma word_roti_add: "word_roti (m + n) w = word_roti m (word_roti n w)" by (rule bit_word_eqI) (simp add: bit_word_roti_iff nat_less_iff mod_simps ac_simps) lemma word_roti_conv_mod': "word_roti n w = word_roti (n mod int (size w)) w" by transfer simp lemmas word_roti_conv_mod = word_roti_conv_mod' [unfolded word_size] subsubsection \"Word rotation commutes with bit-wise operations\ \ \using locale to not pollute lemma namespace\ locale word_rotate begin lemma word_rot_logs: "word_rotl n (NOT v) = NOT (word_rotl n v)" "word_rotr n (NOT v) = NOT (word_rotr n v)" "word_rotl n (x AND y) = word_rotl n x AND word_rotl n y" "word_rotr n (x AND y) = word_rotr n x AND word_rotr n y" "word_rotl n (x OR y) = word_rotl n x OR word_rotl n y" "word_rotr n (x OR y) = word_rotr n x OR word_rotr n y" "word_rotl n (x XOR y) = word_rotl n x XOR word_rotl n y" "word_rotr n (x XOR y) = word_rotr n x XOR word_rotr n y" by (rule bit_word_eqI, auto simp add: bit_word_rotl_iff bit_word_rotr_iff bit_and_iff bit_or_iff bit_xor_iff bit_not_iff algebra_simps not_le)+ end lemmas word_rot_logs = word_rotate.word_rot_logs lemma word_rotx_0 [simp] : "word_rotr i 0 = 0 \ word_rotl i 0 = 0" by transfer simp_all lemma word_roti_0' [simp] : "word_roti n 0 = 0" by transfer simp declare word_roti_eq_word_rotr_word_rotl [simp] subsection \Maximum machine word\ lemma word_int_cases: fixes x :: "'a::len word" obtains n where "x = word_of_int n" and "0 \ n" and "n < 2^LENGTH('a)" by (rule that [of \uint x\]) simp_all lemma word_nat_cases [cases type: word]: fixes x :: "'a::len word" obtains n where "x = of_nat n" and "n < 2^LENGTH('a)" by (rule that [of \unat x\]) simp_all lemma max_word_max [intro!]: \n \ - 1\ for n :: \'a::len word\ by (fact word_order.extremum) lemma word_of_int_2p_len: "word_of_int (2 ^ LENGTH('a)) = (0::'a::len word)" by simp lemma word_pow_0: "(2::'a::len word) ^ LENGTH('a) = 0" by (fact word_exp_length_eq_0) lemma max_word_wrap: \x + 1 = 0 \ x = - 1\ for x :: \'a::len word\ by (simp add: eq_neg_iff_add_eq_0) lemma word_and_max: \x AND - 1 = x\ for x :: \'a::len word\ by (fact word_log_esimps) lemma word_or_max: \x OR - 1 = - 1\ for x :: \'a::len word\ by (fact word_log_esimps) lemma word_ao_dist2: "x AND (y OR z) = x AND y OR x AND z" for x y z :: "'a::len word" by (fact bit.conj_disj_distrib) lemma word_oa_dist2: "x OR y AND z = (x OR y) AND (x OR z)" for x y z :: "'a::len word" by (fact bit.disj_conj_distrib) lemma word_and_not [simp]: "x AND NOT x = 0" for x :: "'a::len word" by (fact bit.conj_cancel_right) lemma word_or_not [simp]: \x OR NOT x = - 1\ for x :: \'a::len word\ by (fact bit.disj_cancel_right) lemma word_xor_and_or: "x XOR y = x AND NOT y OR NOT x AND y" for x y :: "'a::len word" by (fact bit.xor_def) lemma uint_lt_0 [simp]: "uint x < 0 = False" by (simp add: linorder_not_less) lemma shiftr1_1 [simp]: "shiftr1 (1::'a::len word) = 0" by transfer simp lemma word_less_1 [simp]: "x < 1 \ x = 0" for x :: "'a::len word" by (simp add: word_less_nat_alt unat_0_iff) lemma uint_plus_if_size: "uint (x + y) = (if uint x + uint y < 2^size x then uint x + uint y else uint x + uint y - 2^size x)" by (simp add: take_bit_eq_mod word_size uint_word_of_int_eq uint_plus_if') lemma unat_plus_if_size: "unat (x + y) = (if unat x + unat y < 2^size x then unat x + unat y else unat x + unat y - 2^size x)" for x y :: "'a::len word" by (simp add: size_word.rep_eq unat_arith_simps) lemma word_neq_0_conv: "w \ 0 \ 0 < w" for w :: "'a::len word" by (fact word_coorder.not_eq_extremum) lemma max_lt: "unat (max a b div c) = unat (max a b) div unat c" for c :: "'a::len word" by (fact unat_div) lemma uint_sub_if_size: "uint (x - y) = (if uint y \ uint x then uint x - uint y else uint x - uint y + 2^size x)" by (simp add: size_word.rep_eq uint_sub_if') lemma unat_sub: \unat (a - b) = unat a - unat b\ if \b \ a\ by (meson that unat_sub_if_size word_le_nat_alt) lemmas word_less_sub1_numberof [simp] = word_less_sub1 [of "numeral w"] for w lemmas word_le_sub1_numberof [simp] = word_le_sub1 [of "numeral w"] for w lemma word_of_int_minus: "word_of_int (2^LENGTH('a) - i) = (word_of_int (-i)::'a::len word)" by simp lemma word_of_int_inj: \(word_of_int x :: 'a::len word) = word_of_int y \ x = y\ if \0 \ x \ x < 2 ^ LENGTH('a)\ \0 \ y \ y < 2 ^ LENGTH('a)\ using that by (transfer fixing: x y) (simp add: take_bit_int_eq_self) lemma word_le_less_eq: "x \ y \ x = y \ x < y" for x y :: "'z::len word" by (auto simp add: order_class.le_less) lemma mod_plus_cong: fixes b b' :: int assumes 1: "b = b'" and 2: "x mod b' = x' mod b'" and 3: "y mod b' = y' mod b'" and 4: "x' + y' = z'" shows "(x + y) mod b = z' mod b'" proof - from 1 2[symmetric] 3[symmetric] have "(x + y) mod b = (x' mod b' + y' mod b') mod b'" by (simp add: mod_add_eq) also have "\ = (x' + y') mod b'" by (simp add: mod_add_eq) finally show ?thesis by (simp add: 4) qed lemma mod_minus_cong: fixes b b' :: int assumes "b = b'" and "x mod b' = x' mod b'" and "y mod b' = y' mod b'" and "x' - y' = z'" shows "(x - y) mod b = z' mod b'" using assms [symmetric] by (auto intro: mod_diff_cong) lemma word_induct_less [case_names zero less]: \P m\ if zero: \P 0\ and less: \\n. n < m \ P n \ P (1 + n)\ for m :: \'a::len word\ proof - define q where \q = unat m\ with less have \\n. n < word_of_nat q \ P n \ P (1 + n)\ by simp then have \P (word_of_nat q :: 'a word)\ proof (induction q) case 0 show ?case by (simp add: zero) next case (Suc q) show ?case proof (cases \1 + word_of_nat q = (0 :: 'a word)\) case True then show ?thesis by (simp add: zero) next case False then have *: \word_of_nat q < (word_of_nat (Suc q) :: 'a word)\ by (simp add: unatSuc word_less_nat_alt) then have **: \n < (1 + word_of_nat q :: 'a word) \ n \ (word_of_nat q :: 'a word)\ for n by (metis (no_types, lifting) add.commute inc_le le_less_trans not_less of_nat_Suc) have \P (word_of_nat q)\ by (simp add: "**" Suc.IH Suc.prems) with * have \P (1 + word_of_nat q)\ by (rule Suc.prems) then show ?thesis by simp qed qed with \q = unat m\ show ?thesis by simp qed lemma word_induct: "P 0 \ (\n. P n \ P (1 + n)) \ P m" for P :: "'a::len word \ bool" by (rule word_induct_less) lemma word_induct2 [case_names zero suc, induct type]: "P 0 \ (\n. 1 + n \ 0 \ P n \ P (1 + n)) \ P n" for P :: "'b::len word \ bool" by (induction rule: word_induct_less; force) subsection \Recursion combinator for words\ definition word_rec :: "'a \ ('b::len word \ 'a \ 'a) \ 'b word \ 'a" where "word_rec forZero forSuc n = rec_nat forZero (forSuc \ of_nat) (unat n)" lemma word_rec_0 [simp]: "word_rec z s 0 = z" by (simp add: word_rec_def) lemma word_rec_Suc [simp]: "1 + n \ 0 \ word_rec z s (1 + n) = s n (word_rec z s n)" for n :: "'a::len word" by (simp add: unatSuc word_rec_def) lemma word_rec_Pred: "n \ 0 \ word_rec z s n = s (n - 1) (word_rec z s (n - 1))" by (metis add.commute diff_add_cancel word_rec_Suc) lemma word_rec_in: "f (word_rec z (\_. f) n) = word_rec (f z) (\_. f) n" by (induct n) (simp_all add: word_rec_Suc) lemma word_rec_in2: "f n (word_rec z f n) = word_rec (f 0 z) (f \ (+) 1) n" by (induct n) (simp_all add: word_rec_Suc) lemma word_rec_twice: "m \ n \ word_rec z f n = word_rec (word_rec z f (n - m)) (f \ (+) (n - m)) m" proof (induction n arbitrary: z f) case zero then show ?case by (metis diff_0_right word_le_0_iff word_rec_0) next case (suc n z f) show ?case proof (cases "1 + (n - m) = 0") case True then show ?thesis by (simp add: add_diff_eq) next case False then have eq: "1 + n - m = 1 + (n - m)" by simp with False have "m \ n" by (metis "suc.prems" add.commute dual_order.antisym eq_iff_diff_eq_0 inc_le leI) with False "suc.hyps" show ?thesis using suc.IH [of "f 0 z" "f \ (+) 1"] by (simp add: word_rec_in2 eq add.assoc o_def) qed qed lemma word_rec_id: "word_rec z (\_. id) n = z" by (induct n) auto lemma word_rec_id_eq: "(\m. m < n \ f m = id) \ word_rec z f n = z" by (induction n) (auto simp add: unatSuc unat_arith_simps(2)) lemma word_rec_max: assumes "\m\n. m \ - 1 \ f m = id" shows "word_rec z f (- 1) = word_rec z f n" proof - have \
: "\m. \m < - 1 - n\ \ (f \ (+) n) m = id" using assms by (metis (mono_tags, lifting) add.commute add_diff_cancel_left' comp_apply less_le olen_add_eqv plus_minus_no_overflow word_n1_ge) have "word_rec z f (- 1) = word_rec (word_rec z f (- 1 - (- 1 - n))) (f \ (+) (- 1 - (- 1 - n))) (- 1 - n)" by (meson word_n1_ge word_rec_twice) also have "... = word_rec z f n" by (metis (no_types, lifting) \
diff_add_cancel minus_diff_eq uminus_add_conv_diff word_rec_id_eq) finally show ?thesis . qed subsection \More\ lemma mask_1: "mask 1 = 1" by simp lemma mask_Suc_0: "mask (Suc 0) = 1" by simp lemma bin_last_bintrunc: "odd (take_bit l n) \ l > 0 \ odd n" 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) subsection \SMT support\ ML_file \Tools/smt_word.ML\ end