# HG changeset patch # User haftmann # Date 1596728234 0 # Node ID 0b21b2beadb5fed0f4d471bbfbdd2f44fbf66d81 # Parent c65614b556b2c9e46590e875ecedf07210cb4c65 tailored towards remaining essence diff -r c65614b556b2 -r 0b21b2beadb5 src/HOL/ROOT --- a/src/HOL/ROOT Thu Aug 06 17:51:37 2020 +0200 +++ b/src/HOL/ROOT Thu Aug 06 15:37:14 2020 +0000 @@ -612,6 +612,8 @@ description " Miscellaneous examples for Higher-Order Logic. " + sessions + "HOL-Word" theories Antiquote Argo_Examples @@ -693,7 +695,7 @@ Triangular_Numbers Unification While_Combinator_Example - Word + Word_Conversions veriT_Preprocessing theories [skip_proofs = false] SAT_Examples diff -r c65614b556b2 -r 0b21b2beadb5 src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Thu Aug 06 17:51:37 2020 +0200 +++ b/src/HOL/Word/Word.thy Thu Aug 06 15:37:14 2020 +0000 @@ -415,11 +415,11 @@ begin lemma [transfer_rule]: - "((=) ===> (pcr_word :: int \ 'a::len word \ bool)) of_bool of_bool" + "((=) ===> pcr_word) of_bool of_bool" by transfer_prover lemma [transfer_rule]: - "((=) ===> (pcr_word :: int \ 'a::len word \ bool)) numeral numeral" + "((=) ===> pcr_word) numeral numeral" by transfer_prover lemma [transfer_rule]: diff -r c65614b556b2 -r 0b21b2beadb5 src/HOL/ex/Bit_Lists.thy --- a/src/HOL/ex/Bit_Lists.thy Thu Aug 06 17:51:37 2020 +0200 +++ b/src/HOL/ex/Bit_Lists.thy Thu Aug 06 15:37:14 2020 +0000 @@ -5,7 +5,7 @@ theory Bit_Lists imports - Word "HOL-Library.More_List" + Word_Conversions "HOL-Library.More_List" begin subsection \Fragments of algebraic bit representations\ diff -r c65614b556b2 -r 0b21b2beadb5 src/HOL/ex/Word.thy --- a/src/HOL/ex/Word.thy Thu Aug 06 17:51:37 2020 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,670 +0,0 @@ -(* Author: Florian Haftmann, TUM -*) - -section \Proof of concept for algebraically founded bit word types\ - -theory Word - imports - Main - "HOL-Library.Type_Length" - "HOL-Library.Bit_Operations" -begin - -subsection \Bit strings as quotient type\ - -subsubsection \Basic properties\ - -quotient_type (overloaded) 'a word = int / "\k l. take_bit LENGTH('a) k = take_bit LENGTH('a::len) l" - by (auto intro!: equivpI reflpI sympI transpI) - -instantiation word :: (len) "{semiring_numeral, comm_semiring_0, comm_ring}" -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 plus - by (subst take_bit_add [symmetric]) (simp add: take_bit_add) - -lift_definition uminus_word :: "'a word \ 'a word" - is uminus - by (subst take_bit_minus [symmetric]) (simp add: take_bit_minus) - -lift_definition minus_word :: "'a word \ 'a word \ 'a word" - is minus - by (subst take_bit_diff [symmetric]) (simp add: take_bit_diff) - -lift_definition times_word :: "'a word \ 'a word \ 'a word" - is times - by (auto simp add: take_bit_eq_mod intro: mod_mult_cong) - -instance - by standard (transfer; simp add: algebra_simps)+ - -end - -instance word :: (len) comm_ring_1 - by standard (transfer; simp)+ - -quickcheck_generator word - constructors: - "zero_class.zero :: ('a::len) word", - "numeral :: num \ ('a::len) word", - "uminus :: ('a::len) word \ ('a::len) word" - -context - includes lifting_syntax - notes power_transfer [transfer_rule] -begin - -lemma power_transfer_word [transfer_rule]: - \(pcr_word ===> (=) ===> pcr_word) (^) (^)\ - by transfer_prover - -end - - -subsubsection \Conversions\ - -context - includes lifting_syntax - notes - 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 [transfer_rule]: - "((=) ===> (pcr_word :: int \ 'a::len word \ bool)) of_bool of_bool" - by transfer_prover - -lemma [transfer_rule]: - "((=) ===> (pcr_word :: int \ 'a::len word \ bool)) 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 - -end - -lemma abs_word_eq: - "abs_word = of_int" - by (rule ext) (transfer, rule) - -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 - -end - -context semiring_char_0 -begin - -lemma word_eq_iff_unsigned: - "a = b \ unsigned a = unsigned b" - by safe (transfer; simp add: eq_nat_nat_iff) - -end - -instantiation word :: (len) equal -begin - -definition equal_word :: "'a word \ 'a word \ bool" - where "equal_word a b \ (unsigned a :: int) = unsigned b" - -instance proof - fix a b :: "'a word" - show "HOL.equal a b \ a = b" - using word_eq_iff_unsigned [of a b] by (auto simp add: equal_word_def) -qed - -end - -context ring_1 -begin - -lift_definition signed :: "'b::len word \ 'a" - is "of_int \ signed_take_bit (LENGTH('b) - 1)" - by (cases \LENGTH('b)\) - (simp_all add: signed_take_bit_eq_iff_take_bit_eq [symmetric]) - -lemma signed_0 [simp]: - "signed 0 = 0" - by transfer simp - -end - -lemma unsigned_of_nat [simp]: - "unsigned (of_nat n :: 'a word) = take_bit LENGTH('a::len) n" - by transfer (simp add: nat_eq_iff take_bit_eq_mod zmod_int) - -lemma of_nat_unsigned [simp]: - "of_nat (unsigned a) = a" - by transfer simp - -lemma of_int_unsigned [simp]: - "of_int (unsigned a) = a" - by transfer simp - -lemma unsigned_nat_less: - \unsigned a < (2 ^ LENGTH('a) :: nat)\ for a :: \'a::len word\ - by transfer (simp add: take_bit_eq_mod) - -lemma unsigned_int_less: - \unsigned a < (2 ^ LENGTH('a) :: int)\ for a :: \'a::len word\ - by transfer (simp add: take_bit_eq_mod) - -context ring_char_0 -begin - -lemma word_eq_iff_signed: - "a = b \ signed a = signed b" - by safe (transfer; auto simp add: signed_take_bit_eq_iff_take_bit_eq) - -end - -lemma signed_of_int [simp]: - "signed (of_int k :: 'a word) = signed_take_bit (LENGTH('a::len) - 1) k" - by transfer simp - -lemma of_int_signed [simp]: - "of_int (signed a) = a" - by transfer (simp_all add: take_bit_signed_take_bit) - - -subsubsection \Properties\ - -lemma exp_eq_zero_iff: - \(2 :: 'a::len word) ^ n = 0 \ LENGTH('a) \ n\ - by transfer simp - - -subsubsection \Division\ - -instantiation word :: (len) 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 .. - -end - -lemma zero_word_div_eq [simp]: - \0 div a = 0\ for a :: \'a::len word\ - by transfer simp - -lemma div_zero_word_eq [simp]: - \a div 0 = 0\ for a :: \'a::len word\ - by transfer simp - -context - includes lifting_syntax -begin - -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 - -instance word :: (len) semiring_modulo -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 - -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 - - -subsubsection \Orderings\ - -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 - -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 - -lemma word_greater_zero_iff: - \a > 0 \ a \ 0\ for a :: \'a::len word\ - by transfer (simp add: less_le) - -lemma of_nat_word_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_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_nat_word_eq_0_iff: - \of_nat n = (0 :: 'a::len word) \ 2 ^ LENGTH('a) dvd n\ - using of_nat_word_eq_iff [where ?'a = 'a, of n 0] by (simp add: take_bit_eq_0_iff) - -lemma of_int_word_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_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 - -lemma of_int_word_eq_0_iff: - \of_int k = (0 :: 'a::len word) \ 2 ^ LENGTH('a) dvd k\ - using of_int_word_eq_iff [where ?'a = 'a, of k 0] by (simp add: take_bit_eq_0_iff) - - -subsection \Bit structure on \<^typ>\'a word\\ - -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) - 1) \ P (2 * a)\ - and word_odd: \\a. P a \ a < 2 ^ (LENGTH('a) - 1) \ P (1 + 2 * a)\ - for P and a :: \'a::len word\ -proof - - define m :: nat where \m = LENGTH('a) - 1\ - then have l: \LENGTH('a) = Suc m\ - by simp - define n :: nat where \n = unsigned a\ - then have \n < 2 ^ LENGTH('a)\ - by (simp add: unsigned_nat_less) - 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 of_nat_word_eq_0_iff l) - moreover from \n < 2 ^ m\ have \(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - 1)\ - using of_nat_word_less_iff [where ?'a = 'a, of n \2 ^ m\] - by (cases \m = 0\) (simp_all add: not_less take_bit_eq_self ac_simps l) - 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) - 1)\ - using of_nat_word_less_iff [where ?'a = 'a, of n \2 ^ m\] - by (cases \m = 0\) (simp_all add: not_less take_bit_eq_self ac_simps l) - ultimately have \P (1 + 2 * of_nat n)\ - by (rule word_odd) - then show ?case - by simp - qed - then 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 - from 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 - show \a mod b div b = 0\ - for a b :: \'a word\ - apply transfer - apply (simp add: take_bit_eq_mod) - apply (subst (3) mod_pos_pos_trivial [of _ \2 ^ LENGTH('a)\]) - apply simp_all - apply (metis le_less mod_by_0 pos_mod_conj zero_less_numeral zero_less_power) - using pos_mod_bound [of \2 ^ LENGTH('a)\] apply simp - proof - - fix aa :: int and ba :: int - have f1: "\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 "(0::int) < 2 ^ len_of (TYPE('a)::'a itself) \ ba mod 2 ^ len_of (TYPE('a)::'a itself) \ 0 \ aa mod 2 ^ len_of (TYPE('a)::'a itself) mod (ba mod 2 ^ len_of (TYPE('a)::'a itself)) < 2 ^ len_of (TYPE('a)::'a itself)" - by (metis (no_types) mod_by_0 unique_euclidean_semiring_numeral_class.pos_mod_bound zero_less_numeral zero_less_power) - then show "aa mod 2 ^ len_of (TYPE('a)::'a itself) mod (ba mod 2 ^ len_of (TYPE('a)::'a itself)) < 2 ^ len_of (TYPE('a)::'a itself)" - using f1 by (meson le_less less_le_trans unique_euclidean_semiring_numeral_class.pos_mod_bound) - qed - 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: mod_2_eq_odd 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 - -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 - -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 . - -instance by (standard; transfer) - (auto simp add: minus_eq_not_minus_1 mask_eq_exp_minus_1 - bit_not_iff bit_and_iff bit_or_iff bit_xor_iff) - -end - -definition even_word :: \'a::len word \ bool\ - where [code_abbrev]: \