--- a/src/HOL/Code_Numeral.thy Fri Nov 15 21:09:03 2019 +0100
+++ b/src/HOL/Code_Numeral.thy Sun Nov 17 20:44:35 2019 +0000
@@ -297,7 +297,9 @@
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)+
+ (fact bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div
+ bits_div_0 bits_div_by_1 bit_mod_div_trivial even_succ_div_2
+ div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq)+
end
@@ -991,7 +993,9 @@
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)+
+ (fact bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div
+ bits_div_0 bits_div_by_1 bit_mod_div_trivial even_succ_div_2
+ div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq)+
end
--- a/src/HOL/Divides.thy Fri Nov 15 21:09:03 2019 +0100
+++ b/src/HOL/Divides.thy Sun Nov 17 20:44:35 2019 +0000
@@ -393,26 +393,6 @@
zero_less_mult_iff distrib_left [symmetric]
zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: if_split_asm)
-lemma zdiv_zmult2_eq:
- fixes a b c :: int
- assumes "0 \<le> c"
- shows "a div (b * c) = (a div b) div c"
-proof (cases "b = 0")
- case False
- with assms show ?thesis
- by (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN div_int_unique])
-qed auto
-
-lemma zmod_zmult2_eq:
- fixes a b c :: int
- assumes "0 \<le> c"
- shows "a mod (b * c) = b * (a div b mod c) + a mod b"
-proof (cases "b = 0")
- case False
- with assms show ?thesis
- by (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN mod_int_unique])
-qed auto
-
lemma div_pos_geq:
fixes k l :: int
assumes "0 < l" and "l \<le> k"
--- a/src/HOL/Lattices.thy Fri Nov 15 21:09:03 2019 +0100
+++ b/src/HOL/Lattices.thy Sun Nov 17 20:44:35 2019 +0000
@@ -772,6 +772,14 @@
lemma split_max [no_atp]: "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)"
by (simp add: max_def)
+lemma split_min_lin [no_atp]:
+ \<open>P (min a b) \<longleftrightarrow> (b = a \<longrightarrow> P a) \<and> (a < b \<longrightarrow> P a) \<and> (b < a \<longrightarrow> P b)\<close>
+ by (cases a b rule: linorder_cases) (auto simp add: min.absorb1 min.absorb2)
+
+lemma split_max_lin [no_atp]:
+ \<open>P (max a b) \<longleftrightarrow> (b = a \<longrightarrow> P a) \<and> (a < b \<longrightarrow> P b) \<and> (b < a \<longrightarrow> P a)\<close>
+ by (cases a b rule: linorder_cases) (auto simp add: max.absorb1 max.absorb2)
+
lemma min_of_mono: "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)" for f :: "'a \<Rightarrow> 'b::linorder"
by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)
--- a/src/HOL/Parity.thy Fri Nov 15 21:09:03 2019 +0100
+++ b/src/HOL/Parity.thy Sun Nov 17 20:44:35 2019 +0000
@@ -480,6 +480,17 @@
finally show ?thesis .
qed
+lemma exp_mod_exp:
+ \<open>2 ^ m mod 2 ^ n = of_bool (m < n) * 2 ^ m\<close>
+proof -
+ have \<open>(2::nat) ^ m mod 2 ^ n = of_bool (m < n) * 2 ^ m\<close> (is \<open>?lhs = ?rhs\<close>)
+ by (auto simp add: not_less monoid_mult_class.power_add dest!: le_Suc_ex)
+ then have \<open>of_nat ?lhs = of_nat ?rhs\<close>
+ by simp
+ then show ?thesis
+ by (simp add: of_nat_mod)
+qed
+
end
class unique_euclidean_ring_with_nat = ring + unique_euclidean_semiring_with_nat
@@ -600,6 +611,7 @@
qed
qed
+
subsection \<open>Parity and powers\<close>
context ring_1
@@ -745,16 +757,99 @@
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])
+lemma zdiv_zmult2_eq:
+ \<open>a div (b * c) = (a div b) div c\<close> if \<open>c \<ge> 0\<close> for a b c :: int
+proof (cases \<open>b \<ge> 0\<close>)
+ case True
+ with that show ?thesis
+ using div_mult2_eq' [of a \<open>nat b\<close> \<open>nat c\<close>] by simp
+next
+ case False
+ with that show ?thesis
+ using div_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp
+qed
+
+lemma zmod_zmult2_eq:
+ \<open>a mod (b * c) = b * (a div b mod c) + a mod b\<close> if \<open>c \<ge> 0\<close> for a b c :: int
+proof (cases \<open>b \<ge> 0\<close>)
+ case True
+ with that show ?thesis
+ using mod_mult2_eq' [of a \<open>nat b\<close> \<open>nat c\<close>] by simp
+next
+ case False
+ with that show ?thesis
+ using mod_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp
+qed
+
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>
+ assumes bit_eq_rec: \<open>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>
+ assumes bits_div_0 [simp]: \<open>0 div a = 0\<close>
+ and bits_div_by_1 [simp]: \<open>a div 1 = a\<close>
+ and bit_mod_div_trivial [simp]: \<open>a mod b div b = 0\<close>
+ and even_succ_div_2 [simp]: \<open>even a \<Longrightarrow> (1 + a) div 2 = a div 2\<close>
+ and div_exp_eq: \<open>a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)\<close>
+ and mod_exp_eq: \<open>a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n\<close>
+ and mult_exp_mod_exp_eq: \<open>m \<le> n \<Longrightarrow> (a * 2 ^ m) mod (2 ^ n) = (a mod 2 ^ (n - m)) * 2 ^ m\<close>
+ and div_exp_mod_exp_eq: \<open>a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\<close>
+begin
+
+lemma bits_1_div_2 [simp]:
+ \<open>1 div 2 = 0\<close>
+ using even_succ_div_2 [of 0] by simp
+
+lemma bits_1_div_exp [simp]:
+ \<open>1 div 2 ^ n = of_bool (n = 0)\<close>
+ using div_exp_eq [of 1 1] by (cases n) simp_all
+
+lemma even_succ_div_exp [simp]:
+ \<open>(1 + a) div 2 ^ n = a div 2 ^ n\<close> if \<open>even a\<close> and \<open>n > 0\<close>
+proof (cases n)
+ case 0
+ with that show ?thesis
+ by simp
+next
+ case (Suc n)
+ with \<open>even a\<close> have \<open>(1 + a) div 2 ^ Suc n = a div 2 ^ Suc n\<close>
+ proof (induction n)
+ case 0
+ then show ?case
+ by simp
+ next
+ case (Suc n)
+ then show ?case
+ using div_exp_eq [of _ 1 \<open>Suc n\<close>, symmetric]
+ by simp
+ qed
+ with Suc show ?thesis
+ by simp
+qed
+
+lemma even_succ_mod_exp [simp]:
+ \<open>(1 + a) mod 2 ^ n = 1 + (a mod 2 ^ n)\<close> if \<open>even a\<close> and \<open>n > 0\<close>
+ using div_mult_mod_eq [of \<open>1 + a\<close> \<open>2 ^ n\<close>] that
+ apply simp
+ by (metis local.add.left_commute local.add_left_cancel local.div_mult_mod_eq)
+
+lemma bits_mod_by_1 [simp]:
+ \<open>a mod 1 = 0\<close>
+ using div_mult_mod_eq [of a 1] by simp
+
+lemma bits_mod_0 [simp]:
+ \<open>0 mod a = 0\<close>
+ using div_mult_mod_eq [of 0 a] by simp
+
+lemma one_mod_two_eq_one [simp]:
+ \<open>1 mod 2 = 1\<close>
+ by (simp add: mod2_eq_if)
+
+end
lemma nat_bit_induct [case_names zero even odd]:
"P n" if zero: "P 0"
@@ -787,9 +882,6 @@
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)
@@ -809,7 +901,18 @@
with rec [of n True] show ?case
by simp
qed
-qed
+ show \<open>q mod 2 ^ m mod 2 ^ n = q mod 2 ^ min m n\<close>
+ for q m n :: nat
+ apply (auto simp add: less_iff_Suc_add power_add mod_mod_cancel split: split_min_lin)
+ apply (metis div_mult2_eq mod_div_trivial mod_eq_self_iff_div_eq_0 mod_mult_self2_is_0 power_commutes)
+ done
+ show \<open>(q * 2 ^ m) mod (2 ^ n) = (q mod 2 ^ (n - m)) * 2 ^ m\<close> if \<open>m \<le> n\<close>
+ for q m n :: nat
+ using that
+ apply (auto simp add: mod_mod_cancel div_mult2_eq power_add mod_mult2_eq le_iff_add split: split_min_lin)
+ apply (simp add: mult.commute)
+ done
+qed (auto simp add: div_mult2_eq mod_mult2_eq power_add)
lemma int_bit_induct [case_names zero minus even odd]:
"P k" if zero_int: "P 0"
@@ -870,9 +973,6 @@
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)
@@ -896,7 +996,21 @@
with rec [of k True] show ?case
by (simp add: ac_simps)
qed
-qed
+ show \<open>k mod 2 ^ m mod 2 ^ n = k mod 2 ^ min m n\<close>
+ for m n :: nat and k :: int
+ using mod_exp_eq [of \<open>nat k\<close> m n]
+ apply (auto simp add: mod_mod_cancel zdiv_zmult2_eq power_add zmod_zmult2_eq le_iff_add split: split_min_lin)
+ apply (auto simp add: less_iff_Suc_add mod_mod_cancel power_add)
+ apply (simp only: flip: mult.left_commute [of \<open>2 ^ m\<close>])
+ apply (subst zmod_zmult2_eq) apply simp_all
+ done
+ show \<open>(k * 2 ^ m) mod (2 ^ n) = (k mod 2 ^ (n - m)) * 2 ^ m\<close>
+ if \<open>m \<le> n\<close> for m n :: nat and k :: int
+ using that
+ apply (auto simp add: power_add zmod_zmult2_eq le_iff_add split: split_min_lin)
+ apply (simp add: ac_simps)
+ done
+qed (auto simp add: zdiv_zmult2_eq zmod_zmult2_eq power_add)
class semiring_bit_shifts = semiring_bits +
fixes push_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
@@ -920,6 +1034,146 @@
differently wrt. code generation.
\<close>
+lemma bit_ident:
+ "push_bit n (drop_bit n a) + take_bit n a = a"
+ using div_mult_mod_eq by (simp add: push_bit_eq_mult take_bit_eq_mod drop_bit_eq_div)
+
+lemma push_bit_push_bit [simp]:
+ "push_bit m (push_bit n a) = push_bit (m + n) a"
+ by (simp add: push_bit_eq_mult power_add ac_simps)
+
+lemma push_bit_0_id [simp]:
+ "push_bit 0 = id"
+ by (simp add: fun_eq_iff push_bit_eq_mult)
+
+lemma push_bit_of_0 [simp]:
+ "push_bit n 0 = 0"
+ by (simp add: push_bit_eq_mult)
+
+lemma push_bit_of_1:
+ "push_bit n 1 = 2 ^ n"
+ by (simp add: push_bit_eq_mult)
+
+lemma push_bit_Suc [simp]:
+ "push_bit (Suc n) a = push_bit n (a * 2)"
+ by (simp add: push_bit_eq_mult ac_simps)
+
+lemma push_bit_double:
+ "push_bit n (a * 2) = push_bit n a * 2"
+ by (simp add: push_bit_eq_mult ac_simps)
+
+lemma push_bit_add:
+ "push_bit n (a + b) = push_bit n a + push_bit n b"
+ by (simp add: push_bit_eq_mult algebra_simps)
+
+lemma take_bit_0 [simp]:
+ "take_bit 0 a = 0"
+ by (simp add: take_bit_eq_mod)
+
+lemma take_bit_Suc [simp]:
+ \<open>take_bit (Suc n) a = take_bit n (a div 2) * 2 + of_bool (odd a)\<close>
+proof -
+ have \<open>take_bit (Suc n) (a div 2 * 2 + of_bool (odd a)) = take_bit n (a div 2) * 2 + of_bool (odd a)\<close>
+ using even_succ_mod_exp [of \<open>2 * (a div 2)\<close> \<open>Suc n\<close>]
+ mult_exp_mod_exp_eq [of 1 \<open>Suc n\<close> \<open>a div 2\<close>]
+ by (auto simp add: take_bit_eq_mod ac_simps)
+ then show ?thesis
+ using div_mult_mod_eq [of a 2] by (simp add: mod_2_eq_odd)
+qed
+
+lemma take_bit_of_0 [simp]:
+ "take_bit n 0 = 0"
+ by (simp add: take_bit_eq_mod)
+
+lemma take_bit_of_1 [simp]:
+ "take_bit n 1 = of_bool (n > 0)"
+ by (cases n) simp_all
+
+lemma drop_bit_of_0 [simp]:
+ "drop_bit n 0 = 0"
+ by (simp add: drop_bit_eq_div)
+
+lemma drop_bit_of_1 [simp]:
+ "drop_bit n 1 = of_bool (n = 0)"
+ by (simp add: drop_bit_eq_div)
+
+lemma drop_bit_0 [simp]:
+ "drop_bit 0 = id"
+ by (simp add: fun_eq_iff drop_bit_eq_div)
+
+lemma drop_bit_Suc [simp]:
+ "drop_bit (Suc n) a = drop_bit n (a div 2)"
+ using div_exp_eq [of a 1] by (simp add: drop_bit_eq_div)
+
+lemma drop_bit_half:
+ "drop_bit n (a div 2) = drop_bit n a div 2"
+ by (induction n arbitrary: a) simp_all
+
+lemma drop_bit_of_bool [simp]:
+ "drop_bit n (of_bool d) = of_bool (n = 0 \<and> d)"
+ by (cases n) simp_all
+
+lemma take_bit_eq_0_imp_dvd:
+ "take_bit n a = 0 \<Longrightarrow> 2 ^ n dvd a"
+ by (simp add: take_bit_eq_mod mod_0_imp_dvd)
+
+lemma even_take_bit_eq [simp]:
+ \<open>even (take_bit n a) \<longleftrightarrow> n = 0 \<or> even a\<close>
+ by (cases n) simp_all
+
+lemma take_bit_take_bit [simp]:
+ "take_bit m (take_bit n a) = take_bit (min m n) a"
+ by (simp add: take_bit_eq_mod mod_exp_eq ac_simps)
+
+lemma drop_bit_drop_bit [simp]:
+ "drop_bit m (drop_bit n a) = drop_bit (m + n) a"
+ by (simp add: drop_bit_eq_div power_add div_exp_eq ac_simps)
+
+lemma push_bit_take_bit:
+ "push_bit m (take_bit n a) = take_bit (m + n) (push_bit m a)"
+ apply (simp add: push_bit_eq_mult take_bit_eq_mod power_add ac_simps)
+ using mult_exp_mod_exp_eq [of m \<open>m + n\<close> a] apply (simp add: ac_simps power_add)
+ done
+
+lemma take_bit_push_bit:
+ "take_bit m (push_bit n a) = push_bit n (take_bit (m - n) a)"
+proof (cases "m \<le> n")
+ case True
+ then show ?thesis
+ apply (simp add:)
+ apply (simp_all add: push_bit_eq_mult take_bit_eq_mod)
+ apply (auto dest!: le_Suc_ex simp add: power_add ac_simps)
+ using mult_exp_mod_exp_eq [of m m \<open>a * 2 ^ n\<close> for n]
+ apply (simp add: ac_simps)
+ done
+next
+ case False
+ then show ?thesis
+ using push_bit_take_bit [of n "m - n" a]
+ by simp
+qed
+
+lemma take_bit_drop_bit:
+ "take_bit m (drop_bit n a) = drop_bit n (take_bit (m + n) a)"
+ by (simp add: drop_bit_eq_div take_bit_eq_mod ac_simps div_exp_mod_exp_eq)
+
+lemma drop_bit_take_bit:
+ "drop_bit m (take_bit n a) = take_bit (n - m) (drop_bit m a)"
+proof (cases "m \<le> n")
+ case True
+ then show ?thesis
+ using take_bit_drop_bit [of "n - m" m a] by simp
+next
+ case False
+ then obtain q where \<open>m = n + q\<close>
+ by (auto simp add: not_le dest: less_imp_Suc_add)
+ then have \<open>drop_bit m (take_bit n a) = 0\<close>
+ using div_exp_eq [of \<open>a mod 2 ^ n\<close> n q]
+ by (simp add: take_bit_eq_mod drop_bit_eq_div)
+ with False show ?thesis
+ by simp
+qed
+
end
instantiation nat :: semiring_bit_shifts
@@ -962,115 +1216,18 @@
unique_euclidean_semiring_with_nat + semiring_bit_shifts
begin
-lemma bit_ident:
- "push_bit n (drop_bit n a) + take_bit n a = a"
- using div_mult_mod_eq by (simp add: push_bit_eq_mult take_bit_eq_mod drop_bit_eq_div)
-
-lemma push_bit_push_bit [simp]:
- "push_bit m (push_bit n a) = push_bit (m + n) a"
- by (simp add: push_bit_eq_mult power_add ac_simps)
-
-lemma take_bit_take_bit [simp]:
- "take_bit m (take_bit n a) = take_bit (min m n) a"
-proof (cases "m \<le> n")
- case True
- then show ?thesis
- by (simp add: take_bit_eq_mod not_le min_def mod_mod_cancel le_imp_power_dvd)
-next
- case False
- then have "n < m" and "min m n = n"
- by simp_all
- then have "2 ^ m = of_nat (2 ^ n) * of_nat (2 ^ (m - n))"
- by (simp add: power_add [symmetric])
- then have "a mod 2 ^ n mod 2 ^ m = a mod 2 ^ n mod (of_nat (2 ^ n) * of_nat (2 ^ (m - n)))"
- by simp
- also have "\<dots> = of_nat (2 ^ n) * (a mod 2 ^ n div of_nat (2 ^ n) mod of_nat (2 ^ (m - n))) + a mod 2 ^ n mod of_nat (2 ^ n)"
- by (simp only: mod_mult2_eq')
- finally show ?thesis
- using \<open>min m n = n\<close> by (simp add: take_bit_eq_mod)
-qed
-
-lemma drop_bit_drop_bit [simp]:
- "drop_bit m (drop_bit n a) = drop_bit (m + n) a"
-proof -
- have "a div (2 ^ m * 2 ^ n) = a div (of_nat (2 ^ n) * of_nat (2 ^ m))"
- by (simp add: ac_simps)
- also have "\<dots> = a div of_nat (2 ^ n) div of_nat (2 ^ m)"
- by (simp only: div_mult2_eq')
- finally show ?thesis
- by (simp add: drop_bit_eq_div power_add)
-qed
-
-lemma push_bit_take_bit:
- "push_bit m (take_bit n a) = take_bit (m + n) (push_bit m a)"
- by (simp add: push_bit_eq_mult take_bit_eq_mod power_add mult_mod_right ac_simps)
+lemma take_bit_of_exp [simp]:
+ \<open>take_bit m (2 ^ n) = of_bool (n < m) * 2 ^ n\<close>
+ by (simp add: take_bit_eq_mod exp_mod_exp)
-lemma take_bit_push_bit:
- "take_bit m (push_bit n a) = push_bit n (take_bit (m - n) a)"
-proof (cases "m \<le> n")
- case True
- then show ?thesis
- by (simp_all add: push_bit_eq_mult take_bit_eq_mod mod_eq_0_iff_dvd dvd_power_le)
-next
- case False
- then show ?thesis
- using push_bit_take_bit [of n "m - n" a]
- by simp
-qed
-
-lemma take_bit_drop_bit:
- "take_bit m (drop_bit n a) = drop_bit n (take_bit (m + n) a)"
- using mod_mult2_eq' [of a "2 ^ n" "2 ^ m"]
- by (simp add: drop_bit_eq_div take_bit_eq_mod power_add ac_simps)
-
-lemma drop_bit_take_bit:
- "drop_bit m (take_bit n a) = take_bit (n - m) (drop_bit m a)"
-proof (cases "m \<le> n")
- case True
- then show ?thesis
- using take_bit_drop_bit [of "n - m" m a] by simp
-next
- case False
- then have "a mod 2 ^ n div 2 ^ m = a mod 2 ^ n div 2 ^ (n + (m - n))"
- by simp
- also have "\<dots> = a mod 2 ^ n div (2 ^ n * 2 ^ (m - n))"
- by (simp add: power_add)
- also have "\<dots> = a mod 2 ^ n div (of_nat (2 ^ n) * of_nat (2 ^ (m - n)))"
- by simp
- also have "\<dots> = a mod 2 ^ n div of_nat (2 ^ n) div of_nat (2 ^ (m - n))"
- by (simp only: div_mult2_eq')
- finally show ?thesis
- using False by (simp add: take_bit_eq_mod drop_bit_eq_div)
-qed
-
-lemma push_bit_0_id [simp]:
- "push_bit 0 = id"
- by (simp add: fun_eq_iff push_bit_eq_mult)
-
-lemma push_bit_of_0 [simp]:
- "push_bit n 0 = 0"
- by (simp add: push_bit_eq_mult)
-
-lemma push_bit_of_1:
- "push_bit n 1 = 2 ^ n"
- by (simp add: push_bit_eq_mult)
-
-lemma push_bit_Suc [simp]:
- "push_bit (Suc n) a = push_bit n (a * 2)"
- by (simp add: push_bit_eq_mult ac_simps)
-
-lemma push_bit_double:
- "push_bit n (a * 2) = push_bit n a * 2"
- by (simp add: push_bit_eq_mult ac_simps)
+lemma take_bit_of_2 [simp]:
+ \<open>take_bit n 2 = of_bool (2 \<le> n) * 2\<close>
+ using take_bit_of_exp [of n 1] by simp
lemma push_bit_eq_0_iff [simp]:
"push_bit n a = 0 \<longleftrightarrow> a = 0"
by (simp add: push_bit_eq_mult)
-lemma push_bit_add:
- "push_bit n (a + b) = push_bit n a + push_bit n b"
- by (simp add: push_bit_eq_mult algebra_simps)
-
lemma push_bit_numeral [simp]:
"push_bit (numeral l) (numeral k) = push_bit (pred_numeral l) (numeral (Num.Bit0 k))"
by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric]) (simp add: ac_simps)
@@ -1079,31 +1236,6 @@
"push_bit n (of_nat m) = of_nat (push_bit n m)"
by (simp add: push_bit_eq_mult Parity.push_bit_eq_mult)
-lemma take_bit_0 [simp]:
- "take_bit 0 a = 0"
- by (simp add: take_bit_eq_mod)
-
-lemma take_bit_Suc [simp]:
- "take_bit (Suc n) a = take_bit n (a div 2) * 2 + of_bool (odd a)"
-proof -
- have "1 + 2 * (a div 2) mod (2 * 2 ^ n) = (a div 2 * 2 + a mod 2) mod (2 * 2 ^ n)"
- if "odd a"
- using that mod_mult2_eq' [of "1 + 2 * (a div 2)" 2 "2 ^ n"]
- by (simp add: ac_simps odd_iff_mod_2_eq_one mult_mod_right)
- also have "\<dots> = a mod (2 * 2 ^ n)"
- by (simp only: div_mult_mod_eq)
- finally show ?thesis
- by (simp add: take_bit_eq_mod algebra_simps mult_mod_right)
-qed
-
-lemma take_bit_of_0 [simp]:
- "take_bit n 0 = 0"
- by (simp add: take_bit_eq_mod)
-
-lemma take_bit_of_1 [simp]:
- "take_bit n 1 = of_bool (n > 0)"
- by (simp add: take_bit_eq_mod)
-
lemma take_bit_add:
"take_bit n (take_bit n a + take_bit n b) = take_bit n (a + b)"
by (simp add: take_bit_eq_mod mod_simps)
@@ -1116,10 +1248,6 @@
"take_bit n 1 = 0 \<longleftrightarrow> n = 0"
by (simp add: take_bit_eq_mod)
-lemma even_take_bit_eq [simp]:
- "even (take_bit n a) \<longleftrightarrow> n = 0 \<or> even a"
- by (cases n) (simp_all add: take_bit_eq_mod dvd_mod_iff)
-
lemma take_bit_numeral_bit0 [simp]:
"take_bit (numeral l) (numeral (Num.Bit0 k)) = take_bit (pred_numeral l) (numeral k) * 2"
by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric] take_bit_Suc
@@ -1134,45 +1262,6 @@
"take_bit n (of_nat m) = of_nat (take_bit n m)"
by (simp add: take_bit_eq_mod Parity.take_bit_eq_mod of_nat_mod [of m "2 ^ n"])
-lemma drop_bit_0 [simp]:
- "drop_bit 0 = id"
- by (simp add: fun_eq_iff drop_bit_eq_div)
-
-lemma drop_bit_of_0 [simp]:
- "drop_bit n 0 = 0"
- by (simp add: drop_bit_eq_div)
-
-lemma drop_bit_of_1 [simp]:
- "drop_bit n 1 = of_bool (n = 0)"
- by (simp add: drop_bit_eq_div)
-
-lemma drop_bit_Suc [simp]:
- "drop_bit (Suc n) a = drop_bit n (a div 2)"
-proof (cases "even a")
- case True
- then obtain b where "a = 2 * b" ..
- moreover have "drop_bit (Suc n) (2 * b) = drop_bit n b"
- by (simp add: drop_bit_eq_div)
- ultimately show ?thesis
- by simp
-next
- case False
- then obtain b where "a = 2 * b + 1" ..
- moreover have "drop_bit (Suc n) (2 * b + 1) = drop_bit n b"
- using div_mult2_eq' [of "1 + b * 2" 2 "2 ^ n"]
- by (auto simp add: drop_bit_eq_div ac_simps)
- ultimately show ?thesis
- by simp
-qed
-
-lemma drop_bit_half:
- "drop_bit n (a div 2) = drop_bit n a div 2"
- by (induction n arbitrary: a) simp_all
-
-lemma drop_bit_of_bool [simp]:
- "drop_bit n (of_bool d) = of_bool (n = 0 \<and> d)"
- by (cases n) simp_all
-
lemma drop_bit_numeral_bit0 [simp]:
"drop_bit (numeral l) (numeral (Num.Bit0 k)) = drop_bit (pred_numeral l) (numeral k)"
by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric] drop_bit_Suc
--- a/src/HOL/ex/Word.thy Fri Nov 15 21:09:03 2019 +0100
+++ b/src/HOL/ex/Word.thy Sun Nov 17 20:44:35 2019 +0000
@@ -12,6 +12,10 @@
subsection \<open>Preliminaries\<close>
+lemma length_not_greater_eq_2_iff [simp]:
+ \<open>\<not> 2 \<le> LENGTH('a::len) \<longleftrightarrow> LENGTH('a) = 1\<close>
+ by (auto simp add: not_le dest: less_2_cases)
+
lemma take_bit_uminus:
"take_bit n (- (take_bit n k)) = take_bit n (- k)" for k :: int
by (simp add: take_bit_eq_mod mod_minus_eq)
@@ -565,22 +569,14 @@
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 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 (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)
+ 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 \<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>
@@ -598,6 +594,56 @@
with rec [of a True] show ?case
using bit_word_half_eq [of a True] by (simp add: ac_simps)
qed
+ show \<open>0 div a = 0\<close>
+ for a :: \<open>'a word\<close>
+ by transfer simp
+ show \<open>a div 1 = a\<close>
+ for a :: \<open>'a word\<close>
+ by transfer simp
+ show \<open>a mod b div b = 0\<close>
+ for a b :: \<open>'a word\<close>
+ apply transfer
+ apply (simp add: take_bit_eq_mod)
+ apply (subst (3) mod_pos_pos_trivial [of _ \<open>2 ^ LENGTH('a)\<close>])
+ apply simp_all
+ apply (metis le_less mod_by_0 pos_mod_conj zero_less_numeral zero_less_power)
+ using pos_mod_bound [of \<open>2 ^ LENGTH('a)\<close>] apply simp
+ proof -
+ fix aa :: int and ba :: int
+ have f1: "\<And>i n. (i::int) mod 2 ^ n = 0 \<or> 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) \<and> ba mod 2 ^ len_of (TYPE('a)::'a itself) \<noteq> 0 \<or> 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 \<open>(1 + a) div 2 = a div 2\<close>
+ if \<open>even a\<close>
+ for a :: \<open>'a word\<close>
+ using that by transfer (auto dest: le_Suc_ex)
+ 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
+ apply transfer
+ apply (auto simp flip: take_bit_eq_mod)
+ apply (simp add: ac_simps)
+ done
+ show \<open>a * 2 ^ m mod 2 ^ n = a mod 2 ^ (n - m) * 2 ^ m\<close>
+ if \<open>m \<le> n\<close> 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 \<open>a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\<close>
+ for a :: "'a word" and m n :: nat
+ apply transfer
+ apply (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)
+ done
qed
instantiation word :: (len) semiring_bit_shifts