--- a/src/HOL/Divides.thy Fri Jul 03 06:18:27 2020 +0000
+++ b/src/HOL/Divides.thy Fri Jul 03 06:18:29 2020 +0000
@@ -495,6 +495,42 @@
lemma zmod_minus1: "0 < b \<Longrightarrow> - 1 mod b = b - 1" for b :: int
by (auto simp add: modulo_int_def)
+lemma minus_mod_int_eq:
+ \<open>- k mod l = l - 1 - (k - 1) mod l\<close> if \<open>l \<ge> 0\<close> for k l :: int
+proof (cases \<open>l = 0\<close>)
+ case True
+ then show ?thesis
+ by simp
+next
+ case False
+ with that have \<open>l > 0\<close>
+ by simp
+ then show ?thesis
+ proof (cases \<open>l dvd k\<close>)
+ case True
+ then obtain j where \<open>k = l * j\<close> ..
+ moreover have \<open>(l * j mod l - 1) mod l = l - 1\<close>
+ using \<open>l > 0\<close> by (simp add: zmod_minus1)
+ then have \<open>(l * j - 1) mod l = l - 1\<close>
+ by (simp only: mod_simps)
+ ultimately show ?thesis
+ by simp
+ next
+ case False
+ moreover have \<open>0 < k mod l\<close> \<open>k mod l < 1 + l\<close>
+ using \<open>0 < l\<close> le_imp_0_less False apply auto
+ using le_less apply fastforce
+ using pos_mod_bound [of l k] apply linarith
+ done
+ with \<open>l > 0\<close> have \<open>(k mod l - 1) mod l = k mod l - 1\<close>
+ by (simp add: zmod_trival_iff)
+ ultimately show ?thesis
+ apply (simp only: zmod_zminus1_eq_if)
+ apply (simp add: mod_eq_0_iff_dvd algebra_simps mod_simps)
+ done
+ qed
+qed
+
lemma div_neg_pos_less0:
fixes a::int
assumes "a < 0" "0 < b"
--- a/src/HOL/Library/Bit_Operations.thy Fri Jul 03 06:18:27 2020 +0000
+++ b/src/HOL/Library/Bit_Operations.thy Fri Jul 03 06:18:29 2020 +0000
@@ -257,17 +257,17 @@
qed
definition set_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
- where \<open>set_bit n a = a OR 2 ^ n\<close>
+ where \<open>set_bit n a = a OR push_bit n 1\<close>
definition unset_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
- where \<open>unset_bit n a = a AND NOT (2 ^ n)\<close>
+ where \<open>unset_bit n a = a AND NOT (push_bit n 1)\<close>
definition flip_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
- where \<open>flip_bit n a = a XOR 2 ^ n\<close>
+ where \<open>flip_bit n a = a XOR push_bit n 1\<close>
lemma bit_set_bit_iff:
\<open>bit (set_bit m a) n \<longleftrightarrow> bit a n \<or> (m = n \<and> 2 ^ n \<noteq> 0)\<close>
- by (auto simp add: set_bit_def bit_or_iff bit_exp_iff)
+ by (auto simp add: set_bit_def push_bit_of_1 bit_or_iff bit_exp_iff)
lemma even_set_bit_iff:
\<open>even (set_bit m a) \<longleftrightarrow> even a \<and> m \<noteq> 0\<close>
@@ -275,7 +275,7 @@
lemma bit_unset_bit_iff:
\<open>bit (unset_bit m a) n \<longleftrightarrow> bit a n \<and> m \<noteq> n\<close>
- by (auto simp add: unset_bit_def bit_and_iff bit_not_iff bit_exp_iff exp_eq_0_imp_not_bit)
+ by (auto simp add: unset_bit_def push_bit_of_1 bit_and_iff bit_not_iff bit_exp_iff exp_eq_0_imp_not_bit)
lemma even_unset_bit_iff:
\<open>even (unset_bit m a) \<longleftrightarrow> even a \<or> m = 0\<close>
@@ -283,7 +283,7 @@
lemma bit_flip_bit_iff:
\<open>bit (flip_bit m a) n \<longleftrightarrow> (m = n \<longleftrightarrow> \<not> bit a n) \<and> 2 ^ n \<noteq> 0\<close>
- by (auto simp add: flip_bit_def bit_xor_iff bit_exp_iff exp_eq_0_imp_not_bit)
+ by (auto simp add: flip_bit_def push_bit_of_1 bit_xor_iff bit_exp_iff exp_eq_0_imp_not_bit)
lemma even_flip_bit_iff:
\<open>even (flip_bit m a) \<longleftrightarrow> \<not> (even a \<longleftrightarrow> m = 0)\<close>
--- a/src/HOL/List.thy Fri Jul 03 06:18:27 2020 +0000
+++ b/src/HOL/List.thy Fri Jul 03 06:18:29 2020 +0000
@@ -4775,6 +4775,17 @@
lemma rotate_append: "rotate (length l) (l @ q) = q @ l"
by (induct l arbitrary: q) (auto simp add: rotate1_rotate_swap)
+lemma nth_rotate:
+ \<open>rotate m xs ! n = xs ! ((m + n) mod length xs)\<close> if \<open>n < length xs\<close>
+ using that apply (auto simp add: rotate_drop_take nth_append not_less less_diff_conv ac_simps dest!: le_Suc_ex)
+ apply (metis add.commute mod_add_right_eq mod_less)
+ apply (metis (no_types, lifting) Nat.diff_diff_right add.commute add_diff_cancel_right' diff_le_self dual_order.strict_trans2 length_greater_0_conv less_nat_zero_code list.size(3) mod_add_right_eq mod_add_self2 mod_le_divisor mod_less)
+ done
+
+lemma nth_rotate1:
+ \<open>rotate1 xs ! n = xs ! (Suc n mod length xs)\<close> if \<open>n < length xs\<close>
+ using that nth_rotate [of n xs 1] by simp
+
subsubsection \<open>\<^const>\<open>nths\<close> --- a generalization of \<^const>\<open>nth\<close> to sets\<close>
--- a/src/HOL/Num.thy Fri Jul 03 06:18:27 2020 +0000
+++ b/src/HOL/Num.thy Fri Jul 03 06:18:29 2020 +0000
@@ -209,6 +209,14 @@
lemma one_plus_BitM: "One + BitM n = Bit0 n"
unfolding add_One_commute BitM_plus_one ..
+lemma BitM_inc_eq:
+ \<open>Num.BitM (Num.inc n) = Num.Bit1 n\<close>
+ by (induction n) simp_all
+
+lemma inc_BitM_eq:
+ \<open>Num.inc (Num.BitM n) = num.Bit0 n\<close>
+ by (simp add: BitM_plus_one[symmetric] add_One)
+
text \<open>Squaring and exponentiation.\<close>
primrec sqr :: "num \<Rightarrow> num"
@@ -421,6 +429,10 @@
lemma numeral_BitM: "numeral (BitM n) = numeral (Bit0 n) - 1"
by (simp only: BitM_plus_one [symmetric] numeral_add numeral_One eq_diff_eq)
+lemma sub_inc_One_eq:
+ \<open>Num.sub (Num.inc n) num.One = numeral n\<close>
+ by (simp_all add: sub_def diff_eq_eq numeral_inc numeral.numeral_One)
+
lemma dbl_simps [simp]:
"dbl (- numeral k) = - dbl (numeral k)"
"dbl 0 = 0"
--- a/src/HOL/Parity.thy Fri Jul 03 06:18:27 2020 +0000
+++ b/src/HOL/Parity.thy Fri Jul 03 06:18:29 2020 +0000
@@ -1257,6 +1257,10 @@
"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]:
+ \<open>push_bit (numeral l) (numeral k) = push_bit (pred_numeral l) (numeral (Num.Bit0 k))\<close>
+ by (simp add: numeral_eq_Suc mult_2_right) (simp add: numeral_Bit0)
+
lemma take_bit_0 [simp]:
"take_bit 0 a = 0"
by (simp add: take_bit_eq_mod)
@@ -1378,7 +1382,7 @@
by (simp add: push_bit_eq_mult) auto
lemma bit_push_bit_iff:
- \<open>bit (push_bit m a) n \<longleftrightarrow> n \<ge> m \<and> 2 ^ n \<noteq> 0 \<and> (n < m \<or> bit a (n - m))\<close>
+ \<open>bit (push_bit m a) n \<longleftrightarrow> m \<le> n \<and> 2 ^ n \<noteq> 0 \<and> bit a (n - m)\<close>
by (auto simp add: bit_iff_odd push_bit_eq_mult even_mult_exp_div_exp_iff)
lemma bit_drop_bit_eq:
@@ -1492,10 +1496,6 @@
"push_bit n a = 0 \<longleftrightarrow> a = 0"
by (simp add: push_bit_eq_mult)
-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)
-
lemma push_bit_of_nat:
"push_bit n (of_nat m) = of_nat (push_bit n m)"
by (simp add: push_bit_eq_mult Parity.push_bit_eq_mult)
--- a/src/HOL/Word/Ancient_Numeral.thy Fri Jul 03 06:18:27 2020 +0000
+++ b/src/HOL/Word/Ancient_Numeral.thy Fri Jul 03 06:18:29 2020 +0000
@@ -66,7 +66,7 @@
"numeral (Num.Bit1 w) = numeral w BIT True"
"- numeral (Num.Bit0 w) = (- numeral w) BIT False"
"- numeral (Num.Bit1 w) = (- numeral (w + Num.One)) BIT True"
- by (simp_all add: add_One BitM_inc)
+ by (simp_all add: BitM_inc_eq add_One)
lemma less_Bits: "v BIT b < w BIT c \<longleftrightarrow> v < w \<or> v \<le> w \<and> \<not> b \<and> c"
by (auto simp: Bit_def)
--- a/src/HOL/Word/Bits_Int.thy Fri Jul 03 06:18:27 2020 +0000
+++ b/src/HOL/Word/Bits_Int.thy Fri Jul 03 06:18:29 2020 +0000
@@ -24,9 +24,6 @@
abbreviation (input) bin_rest :: "int \<Rightarrow> int"
where "bin_rest w \<equiv> w div 2"
-lemma BitM_inc: "Num.BitM (Num.inc w) = Num.Bit1 w"
- by (induct w) simp_all
-
lemma bin_last_numeral_simps [simp]:
"\<not> bin_last 0"
"bin_last 1"
@@ -572,6 +569,21 @@
lemmas rco_sbintr = sbintrunc_rest'
[THEN rco_lem [THEN fun_cong], unfolded o_def]
+lemma sbintrunc_code [code]:
+ "sbintrunc n k =
+ (let l = take_bit (Suc n) k
+ in if bit l n then l - push_bit n 2 else l)"
+proof (induction n arbitrary: k)
+ case 0
+ then show ?case
+ by (simp add: mod_2_eq_odd and_one_eq)
+next
+ case (Suc n)
+ from Suc [of \<open>k div 2\<close>]
+ show ?case
+ by (auto simp add: Let_def push_bit_eq_mult algebra_simps take_bit_Suc [of \<open>Suc n\<close>] bit_Suc elim!: evenE oddE)
+qed
+
subsection \<open>Splitting and concatenation\<close>
--- a/src/HOL/Word/Word.thy Fri Jul 03 06:18:27 2020 +0000
+++ b/src/HOL/Word/Word.thy Fri Jul 03 06:18:29 2020 +0000
@@ -15,64 +15,6 @@
Misc_Arithmetic
begin
-subsection \<open>Prelude\<close>
-
-lemma (in semiring_bit_shifts) bit_push_bit_iff: \<comment> \<open>TODO move\<close>
- \<open>bit (push_bit m a) n \<longleftrightarrow> m \<le> n \<and> 2 ^ n \<noteq> 0 \<and> bit a (n - m)\<close>
- by (auto simp add: bit_iff_odd push_bit_eq_mult even_mult_exp_div_exp_iff)
-
-lemma (in semiring_bit_shifts) push_bit_numeral [simp]: \<comment> \<open>TODO: move\<close>
- \<open>push_bit (numeral l) (numeral k) = push_bit (pred_numeral l) (numeral (Num.Bit0 k))\<close>
- by (simp add: numeral_eq_Suc mult_2_right) (simp add: numeral_Bit0)
-
-lemma minus_mod_int_eq: \<comment> \<open>TODO move\<close>
- \<open>- k mod l = l - 1 - (k - 1) mod l\<close> if \<open>l \<ge> 0\<close> for k l :: int
-proof (cases \<open>l = 0\<close>)
- case True
- then show ?thesis
- by simp
-next
- case False
- with that have \<open>l > 0\<close>
- by simp
- then show ?thesis
- proof (cases \<open>l dvd k\<close>)
- case True
- then obtain j where \<open>k = l * j\<close> ..
- moreover have \<open>(l * j mod l - 1) mod l = l - 1\<close>
- using \<open>l > 0\<close> by (simp add: zmod_minus1)
- then have \<open>(l * j - 1) mod l = l - 1\<close>
- by (simp only: mod_simps)
- ultimately show ?thesis
- by simp
- next
- case False
- moreover have \<open>0 < k mod l\<close> \<open>k mod l < 1 + l\<close>
- using \<open>0 < l\<close> le_imp_0_less pos_mod_conj False apply auto
- using le_less apply fastforce
- using pos_mod_bound [of l k] apply linarith
- done
- with \<open>l > 0\<close> have \<open>(k mod l - 1) mod l = k mod l - 1\<close>
- by (simp add: zmod_trival_iff)
- ultimately show ?thesis
- apply (simp only: zmod_zminus1_eq_if)
- apply (simp add: mod_eq_0_iff_dvd algebra_simps mod_simps)
- done
- qed
-qed
-
-lemma nth_rotate: \<comment> \<open>TODO move\<close>
- \<open>rotate m xs ! n = xs ! ((m + n) mod length xs)\<close> if \<open>n < length xs\<close>
- using that apply (auto simp add: rotate_drop_take nth_append not_less less_diff_conv ac_simps dest!: le_Suc_ex)
- apply (metis add.commute mod_add_right_eq mod_less)
- apply (metis (no_types, lifting) Nat.diff_diff_right add.commute add_diff_cancel_right' diff_le_self dual_order.strict_trans2 length_greater_0_conv less_nat_zero_code list.size(3) mod_add_right_eq mod_add_self2 mod_le_divisor mod_less)
- done
-
-lemma nth_rotate1: \<comment> \<open>TODO move\<close>
- \<open>rotate1 xs ! n = xs ! (Suc n mod length xs)\<close> if \<open>n < length xs\<close>
- using that nth_rotate [of n xs 1] by simp
-
-
subsection \<open>Type definition\<close>
quotient_type (overloaded) 'a word = int / \<open>\<lambda>k l. take_bit LENGTH('a) k = take_bit LENGTH('a::len) l\<close>
@@ -1006,7 +948,7 @@
lemma set_bit_unfold:
\<open>set_bit w n b = (if b then Bit_Operations.set_bit n w else unset_bit n w)\<close>
for w :: \<open>'a::len word\<close>
- apply (auto simp add: word_set_bit_def bin_clr_conv_NAND bin_set_conv_OR unset_bit_def set_bit_def shiftl_int_def; transfer)
+ apply (auto simp add: word_set_bit_def bin_clr_conv_NAND bin_set_conv_OR unset_bit_def set_bit_def shiftl_int_def push_bit_of_1; transfer)
apply simp_all
done
--- a/src/HOL/ex/Word.thy Fri Jul 03 06:18:27 2020 +0000
+++ b/src/HOL/ex/Word.thy Fri Jul 03 06:18:29 2020 +0000
@@ -37,7 +37,7 @@
qed
lemma signed_take_bit_Suc:
- "signed_take_bit (Suc n) k = signed_take_bit n (k div 2) * 2 + k mod 2"
+ "signed_take_bit (Suc n) k = k mod 2 + 2 * signed_take_bit n (k div 2)"
by (simp add: odd_iff_mod_2_eq_one signed_take_bit_eq_take_bit algebra_simps take_bit_Suc)
lemma signed_take_bit_of_0 [simp]:
@@ -80,6 +80,21 @@
qed
qed
+lemma signed_take_bit_code [code]:
+ \<open>signed_take_bit n k =
+ (let l = take_bit (Suc n) k
+ in if bit l n then l - push_bit n 2 else l)\<close>
+proof (induction n arbitrary: k)
+ case 0
+ then show ?case
+ by (simp add: mod_2_eq_odd and_one_eq)
+next
+ case (Suc n)
+ from Suc [of \<open>k div 2\<close>]
+ show ?case
+ by (auto simp add: Let_def push_bit_eq_mult algebra_simps take_bit_Suc [of \<open>Suc n\<close>] bit_Suc signed_take_bit_Suc elim!: evenE oddE)
+qed
+
subsection \<open>Bit strings as quotient type\<close>