--- a/src/HOL/ex/Bit_Operations.thy Sat Nov 09 10:38:51 2019 +0000
+++ b/src/HOL/ex/Bit_Operations.thy Sat Nov 09 15:39:21 2019 +0000
@@ -9,248 +9,6 @@
Word
begin
-hide_const (open) drop_bit take_bit
-
-subsection \<open>Algebraic structures with bits\<close>
-
-class semiring_bits = semiring_parity +
- assumes bit_split_eq: \<open>\<And>a. of_bool (odd a) + 2 * (a div 2) = a\<close>
- and bit_eq_rec: \<open>\<And>a b. a = b \<longleftrightarrow> (even a = even b) \<and> a div 2 = b div 2\<close>
- and bit_induct [case_names stable rec]:
- \<open>(\<And>a. a div 2 = a \<Longrightarrow> P a)
- \<Longrightarrow> (\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a))
- \<Longrightarrow> P a\<close>
-
-
-subsubsection \<open>Instance \<^typ>\<open>nat\<close>\<close>
-
-instance nat :: semiring_bits
-proof
- show \<open>of_bool (odd n) + 2 * (n div 2) = n\<close>
- for n :: nat
- by simp
- show \<open>m = n \<longleftrightarrow> (even m \<longleftrightarrow> even n) \<and> m div 2 = n div 2\<close>
- for m n :: nat
- by (auto dest: odd_two_times_div_two_succ)
- show \<open>P n\<close> if stable: \<open>\<And>n. n div 2 = n \<Longrightarrow> P n\<close>
- and rec: \<open>\<And>n b. P n \<Longrightarrow> (of_bool b + 2 * n) div 2 = n \<Longrightarrow> P (of_bool b + 2 * n)\<close>
- for P and n :: nat
- proof (induction n rule: nat_bit_induct)
- case zero
- from stable [of 0] show ?case
- by simp
- next
- case (even n)
- with rec [of n False] show ?case
- by simp
- next
- case (odd n)
- with rec [of n True] show ?case
- by simp
- qed
-qed
-
-
-subsubsection \<open>Instance \<^typ>\<open>int\<close>\<close>
-
-instance int :: semiring_bits
-proof
- show \<open>of_bool (odd k) + 2 * (k div 2) = k\<close>
- for k :: int
- by (auto elim: oddE)
- show \<open>k = l \<longleftrightarrow> (even k \<longleftrightarrow> even l) \<and> k div 2 = l div 2\<close>
- for k l :: int
- by (auto dest: odd_two_times_div_two_succ)
- show \<open>P k\<close> if stable: \<open>\<And>k. k div 2 = k \<Longrightarrow> P k\<close>
- and rec: \<open>\<And>k b. P k \<Longrightarrow> (of_bool b + 2 * k) div 2 = k \<Longrightarrow> P (of_bool b + 2 * k)\<close>
- for P and k :: int
- proof (induction k rule: int_bit_induct)
- case zero
- from stable [of 0] show ?case
- by simp
- next
- case minus
- from stable [of \<open>- 1\<close>] show ?case
- by simp
- next
- case (even k)
- with rec [of k False] show ?case
- by (simp add: ac_simps)
- next
- case (odd k)
- with rec [of k True] show ?case
- by (simp add: ac_simps)
- qed
-qed
-
-
-subsubsection \<open>Instance \<^typ>\<open>'a word\<close>\<close>
-
-instance word :: (len) semiring_bits
-proof
- show \<open>of_bool (odd a) + 2 * (a div 2) = a\<close>
- for a :: \<open>'a word\<close>
- apply (cases \<open>even a\<close>; simp, transfer; cases rule: length_cases [where ?'a = 'a])
- apply auto
- apply (auto simp add: take_bit_eq_mod)
- apply (metis add.commute even_take_bit_eq len_not_eq_0 mod_mod_trivial odd_two_times_div_two_succ take_bit_eq_mod)
- done
- show \<open>a = b \<longleftrightarrow> (even a \<longleftrightarrow> even b) \<and> a div 2 = b div 2\<close>
- for a b :: \<open>'a word\<close>
- apply transfer
- apply (cases rule: length_cases [where ?'a = 'a])
- apply auto
- 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) diff_add_cancel dvd_div_mult_self even_take_bit_eq mult_2_right take_bit_add take_bit_minus)
- 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)
- done
- show \<open>P a\<close> if stable: \<open>\<And>a. a div 2 = a \<Longrightarrow> P a\<close>
- and rec: \<open>\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a)\<close>
- for P and a :: \<open>'a word\<close>
- 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
-qed
-
-
-subsection \<open>Bit shifts in suitable algebraic structures\<close>
-
-class semiring_bit_shifts = semiring_bits +
- fixes shift_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
- assumes shift_bit_eq_mult: \<open>shift_bit n a = a * 2 ^ n\<close>
- fixes drop_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
- assumes drop_bit_eq_div: \<open>drop_bit n a = a div 2 ^ n\<close>
-begin
-
-definition take_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
- where take_bit_eq_mod: \<open>take_bit n a = a mod 2 ^ n\<close>
-
-text \<open>
- Logically, \<^const>\<open>shift_bit\<close>,
- \<^const>\<open>drop_bit\<close> and \<^const>\<open>take_bit\<close> are just aliases; having them
- as separate operations makes proofs easier, otherwise proof automation
- would fiddle with concrete expressions \<^term>\<open>2 ^ n\<close> in a way obfuscating the basic
- algebraic relationships between those operations; having
- \<^const>\<open>push_bit\<close> and \<^const>\<open>drop_bit\<close> as definitional class operations
- takes into account that specific instances of these can be implemented
- differently wrt. code generation.
-\<close>
-
-end
-
-subsubsection \<open>Instance \<^typ>\<open>nat\<close>\<close>
-
-instantiation nat :: semiring_bit_shifts
-begin
-
-definition shift_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
- where \<open>shift_bit_nat n m = m * 2 ^ n\<close>
-
-definition drop_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
- where \<open>drop_bit_nat n m = m div 2 ^ n\<close>
-
-instance proof
- show \<open>shift_bit n m = m * 2 ^ n\<close> for n m :: nat
- by (simp add: shift_bit_nat_def)
- show \<open>drop_bit n m = m div 2 ^ n\<close> for n m :: nat
- by (simp add: drop_bit_nat_def)
-qed
-
-end
-
-
-subsubsection \<open>Instance \<^typ>\<open>int\<close>\<close>
-
-instantiation int :: semiring_bit_shifts
-begin
-
-definition shift_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
- where \<open>shift_bit_int n k = k * 2 ^ n\<close>
-
-definition drop_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
- where \<open>drop_bit_int n k = k div 2 ^ n\<close>
-
-instance proof
- show \<open>shift_bit n k = k * 2 ^ n\<close> for n :: nat and k :: int
- by (simp add: shift_bit_int_def)
- show \<open>drop_bit n k = k div 2 ^ n\<close> for n :: nat and k :: int
- by (simp add: drop_bit_int_def)
-qed
-
-end
-
-lemma shift_bit_eq_push_bit:
- \<open>shift_bit = (push_bit :: nat \<Rightarrow> int \<Rightarrow> int)\<close>
- by (simp add: fun_eq_iff push_bit_eq_mult shift_bit_eq_mult)
-
-lemma drop_bit_eq_drop_bit:
- \<open>drop_bit = (Parity.drop_bit :: nat \<Rightarrow> int \<Rightarrow> int)\<close>
- by (simp add: fun_eq_iff drop_bit_eq_div Parity.drop_bit_eq_div)
-
-lemma take_bit_eq_take_bit:
- \<open>take_bit = (Parity.take_bit :: nat \<Rightarrow> int \<Rightarrow> int)\<close>
- by (simp add: fun_eq_iff take_bit_eq_mod Parity.take_bit_eq_mod)
-
-
-subsubsection \<open>Instance \<^typ>\<open>'a word\<close>\<close>
-
-instantiation word :: (len) semiring_bit_shifts
-begin
-
-lift_definition shift_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
- is shift_bit
-proof -
- show \<open>Parity.take_bit LENGTH('a) (shift_bit n k) = Parity.take_bit LENGTH('a) (shift_bit n l)\<close>
- if \<open>Parity.take_bit LENGTH('a) k = Parity.take_bit LENGTH('a) l\<close> for k l :: int and n :: nat
- proof -
- from that
- have \<open>Parity.take_bit (LENGTH('a) - n) (Parity.take_bit LENGTH('a) k)
- = Parity.take_bit (LENGTH('a) - n) (Parity.take_bit LENGTH('a) l)\<close>
- by simp
- moreover have \<open>min (LENGTH('a) - n) LENGTH('a) = LENGTH('a) - n\<close>
- by simp
- ultimately show ?thesis
- by (simp add: shift_bit_eq_push_bit take_bit_push_bit)
- qed
-qed
-
-lift_definition drop_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
- is \<open>\<lambda>n. drop_bit n \<circ> take_bit LENGTH('a)\<close>
- by (simp add: take_bit_eq_mod Parity.take_bit_eq_mod)
-
-instance proof
- show \<open>shift_bit n a = a * 2 ^ n\<close> for n :: nat and a :: "'a word"
- by transfer (simp add: shift_bit_eq_mult)
- show \<open>drop_bit n a = a div 2 ^ n\<close> for n :: nat and a :: "'a word"
- proof (cases \<open>n < LENGTH('a)\<close>)
- case True
- then show ?thesis
- by transfer
- (simp add: Parity.take_bit_eq_mod take_bit_eq_mod drop_bit_eq_div)
- next
- case False
- then obtain m where n: \<open>n = LENGTH('a) + m\<close>
- by (auto simp add: not_less dest: le_Suc_ex)
- then show ?thesis
- by transfer
- (simp add: Parity.take_bit_eq_mod take_bit_eq_mod drop_bit_eq_div power_add zdiv_zmult2_eq)
- qed
-qed
-
-end
-
-
subsection \<open>Bit operations in suitable algebraic structures\<close>
class semiring_bit_operations = semiring_bit_shifts +
@@ -261,8 +19,7 @@
text \<open>
We want the bitwise operations to bind slightly weaker
- than \<open>+\<close> and \<open>-\<close>, but \<open>~~\<close> to
- bind slightly stronger than \<open>*\<close>.
+ than \<open>+\<close> and \<open>-\<close>.
For the sake of code generation
the operations \<^const>\<open>and\<close>, \<^const>\<open>or\<close> and \<^const>\<open>xor\<close>
are specified as definitional class operations.
@@ -273,7 +30,7 @@
where \<open>bit a n \<longleftrightarrow> odd (drop_bit n a)\<close>
definition map_bit :: \<open>nat \<Rightarrow> (bool \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a\<close>
- where \<open>map_bit n f a = take_bit n a + shift_bit n (of_bool (f (bit a n)) + drop_bit (Suc n) a)\<close>
+ where \<open>map_bit n f a = take_bit n a + push_bit n (of_bool (f (bit a n)) + drop_bit (Suc n) a)\<close>
definition set_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
where \<open>set_bit n = map_bit n top\<close>