# HG changeset patch # User haftmann # Date 1574873673 0 # Node ID 8331063570d6b21b03f3fa62aee67c17fc5e262f # Parent 65192ac7eaf236ef070fb676c905f4a24ee3fbc8 bit accessor and fundamental properties diff -r 65192ac7eaf2 -r 8331063570d6 src/HOL/Parity.thy --- a/src/HOL/Parity.thy Fri Nov 29 21:53:02 2019 +0100 +++ b/src/HOL/Parity.thy Wed Nov 27 16:54:33 2019 +0000 @@ -30,6 +30,10 @@ using assms by (cases "even a") (simp_all add: even_iff_mod_2_eq_zero [symmetric] odd_iff_mod_2_eq_one [symmetric]) +lemma odd_of_bool_self [simp]: + \odd (of_bool p) \ p\ + by (cases p) simp_all + lemma not_mod_2_eq_0_eq_1 [simp]: "a mod 2 \ 0 \ a mod 2 = 1" by (cases a rule: parity_cases) simp_all @@ -562,11 +566,10 @@ qed -subsection \Abstract bit shifts\ +subsection \Abstract bit structures\ class semiring_bits = semiring_parity + - assumes bit_eq_rec: \a = b \ (even a = even b) \ a div 2 = b div 2\ - and bit_induct [case_names stable rec]: + assumes bit_induct [case_names stable rec]: \(\a. a div 2 = a \ P a) \ (\a b. P a \ (of_bool b + 2 * a) div 2 = a \ P (of_bool b + 2 * a)) \ P a\ @@ -629,6 +632,124 @@ \1 mod 2 = 1\ by (simp add: mod2_eq_if) +definition bit :: \'a \ nat \ bool\ + where \bit a n \ odd (a div 2 ^ n)\ + +lemma bit_0 [simp]: + \bit a 0 \ odd a\ + by (simp add: bit_def) + +lemma bit_Suc [simp]: + \bit a (Suc n) \ bit (a div 2) n\ + using div_exp_eq [of a 1 n] by (simp add: bit_def) + +context + fixes a + assumes stable: \a div 2 = a\ +begin + +lemma stable_imp_add_self: + \a + a mod 2 = 0\ +proof - + have \a div 2 * 2 + a mod 2 = a\ + by (fact div_mult_mod_eq) + then have \a * 2 + a mod 2 = a\ + by (simp add: stable) + then show ?thesis + by (simp add: mult_2_right ac_simps) +qed + +lemma stable_imp_bit_iff_odd: + \bit a n \ odd a\ + by (induction n) (simp_all add: stable) + +end + +lemma bit_iff_idd_imp_stable: + \a div 2 = a\ if \\n. bit a n \ odd a\ +using that proof (induction a rule: bit_induct) + case (stable a) + then show ?case + by simp +next + case (rec a b) + from rec.prems [of 1] have [simp]: \b = odd a\ + by (simp add: rec.hyps) + from rec.hyps have hyp: \(of_bool (odd a) + 2 * a) div 2 = a\ + by simp + have \bit a n \ odd a\ for n + using rec.prems [of \Suc n\] by (simp add: hyp) + then have \a div 2 = a\ + by (rule rec.IH) + then have \of_bool (odd a) + 2 * a = 2 * (a div 2) + of_bool (odd a)\ + by (simp add: ac_simps) + also have \\ = a\ + using mult_div_mod_eq [of 2 a] + by (simp add: of_bool_odd_eq_mod_2) + finally show ?case + using \a div 2 = a\ by (simp add: hyp) +qed + +lemma bit_eqI: + \a = b\ if \\n. bit a n \ bit b n\ +using that proof (induction a arbitrary: b rule: bit_induct) + case (stable a) + from stable(2) [of 0] have **: \even b \ even a\ + by simp + have \b div 2 = b\ + proof (rule bit_iff_idd_imp_stable) + fix n + from stable have *: \bit b n \ bit a n\ + by simp + also have \bit a n \ odd a\ + using stable by (simp add: stable_imp_bit_iff_odd) + finally show \bit b n \ odd b\ + by (simp add: **) + qed + from ** have \a mod 2 = b mod 2\ + by (simp add: mod2_eq_if) + then have \a mod 2 + (a + b) = b mod 2 + (a + b)\ + by simp + then have \a + a mod 2 + b = b + b mod 2 + a\ + by (simp add: ac_simps) + with \a div 2 = a\ \b div 2 = b\ show ?case + by (simp add: stable_imp_add_self) +next + case (rec a p) + from rec.prems [of 0] have [simp]: \p = odd b\ + by simp + from rec.hyps have \bit a n \ bit (b div 2) n\ for n + using rec.prems [of \Suc n\] by simp + then have \a = b div 2\ + by (rule rec.IH) + then have \2 * a = 2 * (b div 2)\ + by simp + then have \b mod 2 + 2 * a = b mod 2 + 2 * (b div 2)\ + by simp + also have \\ = b\ + by (fact mod_mult_div_eq) + finally show ?case + by (auto simp add: mod2_eq_if) +qed + +lemma bit_eq_iff: + \a = b \ (\n. bit a n \ bit b n)\ + by (auto intro: bit_eqI) + +lemma bit_eq_rec: + \a = b \ (even a \ even b) \ a div 2 = b div 2\ + apply (simp add: bit_eq_iff) + apply auto + using bit_0 apply blast + using bit_0 apply blast + using bit_Suc apply blast + using bit_Suc apply blast + apply (metis bit_eq_iff local.even_iff_mod_2_eq_zero local.mod_div_mult_eq) + apply (metis bit_eq_iff local.even_iff_mod_2_eq_zero local.mod_div_mult_eq) + apply (metis bit_eq_iff local.mod2_eq_if local.mod_div_mult_eq) + apply (metis bit_eq_iff local.mod2_eq_if local.mod_div_mult_eq) + done + end lemma nat_bit_induct [case_names zero even odd]: @@ -662,9 +783,6 @@ instance nat :: semiring_bits proof - show \m = n \ (even m \ even n) \ m div 2 = n div 2\ - for m n :: nat - by (auto dest: odd_two_times_div_two_succ) show \P n\ if stable: \\n. n div 2 = n \ P n\ and rec: \\n b. P n \ (of_bool b + 2 * n) div 2 = n \ P (of_bool b + 2 * n)\ for P and n :: nat @@ -753,9 +871,6 @@ instance int :: semiring_bits proof - show \k = l \ (even k \ even l) \ k div 2 = l div 2\ - for k l :: int - by (auto dest: odd_two_times_div_two_succ) show \P k\ if stable: \\k. k div 2 = k \ P k\ and rec: \\k b. P k \ (of_bool b + 2 * k) div 2 = k \ P (of_bool b + 2 * k)\ for P and k :: int @@ -954,6 +1069,14 @@ by simp qed +lemma bit_drop_bit_eq: + \bit (drop_bit n a) = bit a \ (+) n\ + by (simp add: bit_def fun_eq_iff ac_simps flip: drop_bit_eq_div) + +lemma bit_take_bit_iff: + \bit (take_bit m a) n \ n < m \ bit a n\ + by (simp add: bit_def drop_bit_take_bit not_le flip: drop_bit_eq_div) + end instantiation nat :: semiring_bit_shifts diff -r 65192ac7eaf2 -r 8331063570d6 src/HOL/Word/Bits_Int.thy --- a/src/HOL/Word/Bits_Int.thy Fri Nov 29 21:53:02 2019 +0100 +++ b/src/HOL/Word/Bits_Int.thy Wed Nov 27 16:54:33 2019 +0000 @@ -1623,7 +1623,8 @@ apply (case_tac bit, auto) done -lemma mod_BIT: "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit" +lemma mod_BIT: + "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit" for bit proof - have "2 * (bin mod 2 ^ n) + 1 = (2 * bin mod 2 ^ Suc n) + 1" by (simp add: mod_mult_mult1) diff -r 65192ac7eaf2 -r 8331063570d6 src/HOL/ex/Bit_Operations.thy --- a/src/HOL/ex/Bit_Operations.thy Fri Nov 29 21:53:02 2019 +0100 +++ b/src/HOL/ex/Bit_Operations.thy Wed Nov 27 16:54:33 2019 +0000 @@ -26,11 +26,8 @@ \ -definition bit :: \'a \ nat \ bool\ - where \bit a n \ odd (drop_bit n a)\ - definition map_bit :: \nat \ (bool \ bool) \ 'a \ 'a\ - where \map_bit n f a = take_bit n a + push_bit n (of_bool (f (bit a n)) + drop_bit (Suc n) a)\ + where \map_bit n f a = take_bit n a + push_bit n (of_bool (f (bit a n)) + 2 * drop_bit (Suc n) a)\ definition set_bit :: \nat \ 'a \ 'a\ where \set_bit n = map_bit n top\ @@ -42,11 +39,48 @@ where \flip_bit n = map_bit n Not\ text \ - The logical core are \<^const>\bit\ and \<^const>\map_bit\; having + Having <^const>\set_bit\, \<^const>\unset_bit\ and \<^const>\flip_bit\ as separate operations allows to implement them using bit masks later. \ +lemma stable_imp_drop_eq: + \drop_bit n a = a\ if \a div 2 = a\ + by (induction n) (simp_all add: that) + +lemma map_bit_0 [simp]: + \map_bit 0 f a = of_bool (f (odd a)) + 2 * (a div 2)\ + by (simp add: map_bit_def) + +lemma map_bit_Suc [simp]: + \map_bit (Suc n) f a = a mod 2 + 2 * map_bit n f (a div 2)\ + by (auto simp add: map_bit_def algebra_simps mod2_eq_if push_bit_add mult_2 + elim: evenE oddE) + +lemma set_bit_0 [simp]: + \set_bit 0 a = 1 + 2 * (a div 2)\ + by (simp add: set_bit_def) + +lemma set_bit_Suc [simp]: + \set_bit (Suc n) a = a mod 2 + 2 * set_bit n (a div 2)\ + by (simp add: set_bit_def) + +lemma unset_bit_0 [simp]: + \unset_bit 0 a = 2 * (a div 2)\ + by (simp add: unset_bit_def) + +lemma unset_bit_Suc [simp]: + \unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)\ + by (simp add: unset_bit_def) + +lemma flip_bit_0 [simp]: + \flip_bit 0 a = of_bool (even a) + 2 * (a div 2)\ + by (simp add: flip_bit_def) + +lemma flip_bit_Suc [simp]: + \flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)\ + by (simp add: flip_bit_def) + end class ring_bit_operations = semiring_bit_operations + ring_parity + @@ -126,7 +160,7 @@ next case (even m) with rec [of "2 * m"] rec [of _ q] show ?case - by (cases "even n") (auto dest: False_P_imp) + by (cases "even n") (auto simp add: ac_simps dest: False_P_imp) next case (odd m) with rec [of "Suc (2 * m)"] rec [of _ q] show ?case diff -r 65192ac7eaf2 -r 8331063570d6 src/HOL/ex/Word.thy --- a/src/HOL/ex/Word.thy Fri Nov 29 21:53:02 2019 +0100 +++ b/src/HOL/ex/Word.thy Wed Nov 27 16:54:33 2019 +0000 @@ -277,7 +277,7 @@ subsubsection \Properties\ -lemma length_cases: +lemma length_cases: \ \TODO get rid of\ obtains (triv) "LENGTH('a::len) = 1" "take_bit LENGTH('a) 2 = (0 :: int)" | (take_bit_2) "take_bit LENGTH('a) 2 = (2 :: int)" proof (cases "LENGTH('a) \ 2") @@ -569,15 +569,6 @@ instance word :: (len) semiring_bits proof - show \a = b \ (even a \ even b) \ a div 2 = b div 2\ - for a b :: \'a word\ - apply transfer - apply auto - apply (metis bit_ident drop_bit_eq_div drop_bit_half even_take_bit_eq even_two_times_div_two mod_div_trivial odd_two_times_div_two_succ take_bit_eq_mod) - apply (metis even_take_bit_eq len_not_eq_0) - apply (metis even_take_bit_eq len_not_eq_0) - apply (metis (no_types, hide_lams) div_0 drop_bit_eq_div drop_bit_half dvd_mult_div_cancel even_take_bit_eq mod_div_trivial mod_eq_self_iff_div_eq_0 take_bit_eq_mod) - done 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\