--- a/src/HOL/Code_Numeral.thy Sat Nov 09 10:38:51 2019 +0000
+++ b/src/HOL/Code_Numeral.thy Sat Nov 09 15:39:21 2019 +0000
@@ -287,17 +287,30 @@
instance integer :: unique_euclidean_ring_with_nat
by (standard; transfer) (simp_all add: of_nat_div division_segment_int_def)
-lemma [transfer_rule]:
- "rel_fun (=) (rel_fun pcr_integer pcr_integer) (push_bit :: _ \<Rightarrow> _ \<Rightarrow> int) (push_bit :: _ \<Rightarrow> _ \<Rightarrow> integer)"
- by (unfold push_bit_eq_mult [abs_def]) transfer_prover
+instantiation integer :: semiring_bit_shifts
+begin
+
+lift_definition push_bit_integer :: \<open>nat \<Rightarrow> integer \<Rightarrow> integer\<close>
+ is \<open>push_bit\<close> .
+
+lift_definition drop_bit_integer :: \<open>nat \<Rightarrow> integer \<Rightarrow> integer\<close>
+ is \<open>drop_bit\<close> .
+
+instance by (standard; transfer)
+ (fact bit_split_eq bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div)+
+
+end
lemma [transfer_rule]:
"rel_fun (=) (rel_fun pcr_integer pcr_integer) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> int) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> integer)"
by (unfold take_bit_eq_mod [abs_def]) transfer_prover
-lemma [transfer_rule]:
- "rel_fun (=) (rel_fun pcr_integer pcr_integer) (drop_bit :: _ \<Rightarrow> _ \<Rightarrow> int) (drop_bit :: _ \<Rightarrow> _ \<Rightarrow> integer)"
- by (unfold drop_bit_eq_div [abs_def]) transfer_prover
+instance integer :: unique_euclidean_semiring_with_bit_shifts ..
+
+lemma [code]:
+ \<open>push_bit n k = k * 2 ^ n\<close>
+ \<open>drop_bit n k = k div 2 ^ n\<close> for k :: integer
+ by (fact push_bit_eq_mult drop_bit_eq_div)+
instantiation integer :: unique_euclidean_semiring_numeral
begin
@@ -968,17 +981,30 @@
instance natural :: unique_euclidean_semiring_with_nat
by (standard; transfer) simp_all
-lemma [transfer_rule]:
- "rel_fun (=) (rel_fun pcr_natural pcr_natural) (push_bit :: _ \<Rightarrow> _ \<Rightarrow> nat) (push_bit :: _ \<Rightarrow> _ \<Rightarrow> natural)"
- by (unfold push_bit_eq_mult [abs_def]) transfer_prover
+instantiation natural :: semiring_bit_shifts
+begin
+
+lift_definition push_bit_natural :: \<open>nat \<Rightarrow> natural \<Rightarrow> natural\<close>
+ is \<open>push_bit\<close> .
+
+lift_definition drop_bit_natural :: \<open>nat \<Rightarrow> natural \<Rightarrow> natural\<close>
+ is \<open>drop_bit\<close> .
+
+instance by (standard; transfer)
+ (fact bit_split_eq bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div)+
+
+end
lemma [transfer_rule]:
"rel_fun (=) (rel_fun pcr_natural pcr_natural) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> nat) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> natural)"
by (unfold take_bit_eq_mod [abs_def]) transfer_prover
-lemma [transfer_rule]:
- "rel_fun (=) (rel_fun pcr_natural pcr_natural) (drop_bit :: _ \<Rightarrow> _ \<Rightarrow> nat) (drop_bit :: _ \<Rightarrow> _ \<Rightarrow> natural)"
- by (unfold drop_bit_eq_div [abs_def]) transfer_prover
+instance natural :: unique_euclidean_semiring_with_bit_shifts ..
+
+lemma [code]:
+ \<open>push_bit n m = m * 2 ^ n\<close>
+ \<open>drop_bit n m = m div 2 ^ n\<close> for m :: natural
+ by (fact push_bit_eq_mult drop_bit_eq_div)+
lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
is "nat :: int \<Rightarrow> nat"
--- a/src/HOL/Parity.thy Sat Nov 09 10:38:51 2019 +0000
+++ b/src/HOL/Parity.thy Sat Nov 09 15:39:21 2019 +0000
@@ -573,35 +573,6 @@
"n mod 2 \<noteq> Suc 0 \<longleftrightarrow> n mod 2 = 0"
using not_mod_2_eq_1_eq_0 [of n] by simp
-lemma nat_bit_induct [case_names zero even odd]:
- "P n" if zero: "P 0"
- and even: "\<And>n. P n \<Longrightarrow> n > 0 \<Longrightarrow> P (2 * n)"
- and odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
-proof (induction n rule: less_induct)
- case (less n)
- show "P n"
- proof (cases "n = 0")
- case True with zero show ?thesis by simp
- next
- case False
- with less have hyp: "P (n div 2)" by simp
- show ?thesis
- proof (cases "even n")
- case True
- then have "n \<noteq> 1"
- by auto
- with \<open>n \<noteq> 0\<close> have "n div 2 > 0"
- by simp
- with \<open>even n\<close> hyp even [of "n div 2"] show ?thesis
- by simp
- next
- case False
- with hyp odd [of "n div 2"] show ?thesis
- by simp
- qed
- qed
-qed
-
lemma odd_card_imp_not_empty:
\<open>A \<noteq> {}\<close> if \<open>odd (card A)\<close>
using that by auto
@@ -774,6 +745,72 @@
lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric])
+
+subsection \<open>Abstract bit shifts\<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>
+
+lemma nat_bit_induct [case_names zero even odd]:
+ "P n" if zero: "P 0"
+ and even: "\<And>n. P n \<Longrightarrow> n > 0 \<Longrightarrow> P (2 * n)"
+ and odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
+proof (induction n rule: less_induct)
+ case (less n)
+ show "P n"
+ proof (cases "n = 0")
+ case True with zero show ?thesis by simp
+ next
+ case False
+ with less have hyp: "P (n div 2)" by simp
+ show ?thesis
+ proof (cases "even n")
+ case True
+ then have "n \<noteq> 1"
+ by auto
+ with \<open>n \<noteq> 0\<close> have "n div 2 > 0"
+ by simp
+ with \<open>even n\<close> hyp even [of "n div 2"] show ?thesis
+ by simp
+ next
+ case False
+ with hyp odd [of "n div 2"] show ?thesis
+ by simp
+ qed
+ qed
+qed
+
+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
+
lemma int_bit_induct [case_names zero minus even odd]:
"P k" if zero_int: "P 0"
and minus_int: "P (- 1)"
@@ -831,27 +868,98 @@
qed
qed
+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
-subsection \<open>Abstract bit operations\<close>
-
-context semiring_parity
+class semiring_bit_shifts = semiring_bits +
+ fixes push_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
+ assumes push_bit_eq_mult: \<open>push_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
-text \<open>The primary purpose of the following operations is
- to avoid ad-hoc simplification of concrete expressions \<^term>\<open>2 ^ n\<close>\<close>
+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>
-definition push_bit :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
- where push_bit_eq_mult: "push_bit n a = a * 2 ^ n"
-
-definition take_bit :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
- where take_bit_eq_mod: "take_bit n a = a mod 2 ^ n"
-
-definition drop_bit :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
- where drop_bit_eq_div: "drop_bit n a = a div 2 ^ n"
+text \<open>
+ Logically, \<^const>\<open>push_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
-context unique_euclidean_semiring_with_nat
+instantiation nat :: semiring_bit_shifts
+begin
+
+definition push_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
+ where \<open>push_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>push_bit n m = m * 2 ^ n\<close> for n m :: nat
+ by (simp add: push_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
+
+instantiation int :: semiring_bit_shifts
+begin
+
+definition push_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
+ where \<open>push_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>push_bit n k = k * 2 ^ n\<close> for n :: nat and k :: int
+ by (simp add: push_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
+
+class unique_euclidean_semiring_with_bit_shifts =
+ unique_euclidean_semiring_with_nat + semiring_bit_shifts
begin
lemma bit_ident:
@@ -1081,6 +1189,10 @@
end
+instance nat :: unique_euclidean_semiring_with_bit_shifts ..
+
+instance int :: unique_euclidean_semiring_with_bit_shifts ..
+
lemma push_bit_of_Suc_0 [simp]:
"push_bit n (Suc 0) = 2 ^ n"
using push_bit_of_1 [where ?'a = nat] by simp
--- a/src/HOL/Set_Interval.thy Sat Nov 09 10:38:51 2019 +0000
+++ b/src/HOL/Set_Interval.thy Sat Nov 09 15:39:21 2019 +0000
@@ -2041,7 +2041,7 @@
by (subst sum_subtractf_nat) auto
-context unique_euclidean_semiring_with_nat
+context unique_euclidean_semiring_with_bit_shifts
begin
lemma take_bit_sum:
--- a/src/HOL/String.thy Sat Nov 09 10:38:51 2019 +0000
+++ b/src/HOL/String.thy Sat Nov 09 15:39:21 2019 +0000
@@ -45,7 +45,7 @@
end
-context unique_euclidean_semiring_with_nat
+context unique_euclidean_semiring_with_bit_shifts
begin
definition char_of :: "'a \<Rightarrow> char"
--- a/src/HOL/ex/Bit_Lists.thy Sat Nov 09 10:38:51 2019 +0000
+++ b/src/HOL/ex/Bit_Lists.thy Sat Nov 09 15:39:21 2019 +0000
@@ -26,7 +26,7 @@
end
-context unique_euclidean_semiring_with_nat
+context unique_euclidean_semiring_with_bit_shifts
begin
lemma unsigned_of_bits_append [simp]:
@@ -285,7 +285,7 @@
of_bits bs OR of_bits cs = of_bits (map2 (\<or>) bs cs)"
and xor_eq: "length bs = length cs \<Longrightarrow>
of_bits bs XOR of_bits cs = of_bits (map2 (\<noteq>) bs cs)"
- and shift_bit_eq: "shift_bit n a = of_bits (replicate n False @ bits_of a)"
+ and push_bit_eq: "push_bit n a = of_bits (replicate n False @ bits_of a)"
and drop_bit_eq: "n < length (bits_of a) \<Longrightarrow> drop_bit n a = of_bits (drop n (bits_of a))"
class ring_bit_representation = ring_bit_operations + semiring_bit_representation +
@@ -314,7 +314,7 @@
instance nat :: semiring_bit_representation
apply standard
apply (simp_all only: and_nat.of_bits or_nat.of_bits xor_nat.of_bits)
- apply (simp_all add: drop_bit_eq_div Parity.drop_bit_eq_div shift_bit_eq_mult push_bit_eq_mult)
+ apply simp_all
done
context zip_int
@@ -359,10 +359,9 @@
show "(of_bits \<circ> map Not \<circ> bits_of) k = NOT k"
by (induction k rule: int_bit_induct) (simp_all add: not_int_def)
qed
- show "shift_bit n k = of_bits (replicate n False @ bits_of k)"
+ show "push_bit n k = of_bits (replicate n False @ bits_of k)"
for k :: int and n :: nat
- by (cases "n = 0") (simp_all add: shift_bit_eq_push_bit)
-qed (simp_all add: and_int.of_bits or_int.of_bits xor_int.of_bits
- drop_bit_eq_drop_bit)
+ by (cases "n = 0") simp_all
+qed (simp_all add: and_int.of_bits or_int.of_bits xor_int.of_bits)
end
--- 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>
--- a/src/HOL/ex/Word.thy Sat Nov 09 10:38:51 2019 +0000
+++ b/src/HOL/ex/Word.thy Sat Nov 09 15:39:21 2019 +0000
@@ -562,4 +562,91 @@
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
+
+
+subsubsection \<open>Instance \<^typ>\<open>'a word\<close>\<close>
+
+instantiation word :: (len) semiring_bit_shifts
+begin
+
+lift_definition push_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+ is push_bit
+proof -
+ show \<open>Parity.take_bit LENGTH('a) (push_bit n k) = Parity.take_bit LENGTH('a) (push_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: 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)
+
+instance proof
+ show \<open>push_bit n a = a * 2 ^ n\<close> for n :: nat and a :: "'a word"
+ by transfer (simp add: push_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: 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: take_bit_eq_mod drop_bit_eq_div power_add zdiv_zmult2_eq)
+ qed
+qed
+
end
+
+end