# HG changeset patch
# User haftmann
# Date 1593757109 0
# Node ID 8bff286878bf6cb81af9bb2fcfbfb934fc4809d0
# Parent  66beb9d92e4330f3057870bf6a31eed972fbd35f
misc lemma tuning

diff -r 66beb9d92e43 -r 8bff286878bf src/HOL/Divides.thy
--- 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" 
diff -r 66beb9d92e43 -r 8bff286878bf src/HOL/Library/Bit_Operations.thy
--- 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>
diff -r 66beb9d92e43 -r 8bff286878bf src/HOL/List.thy
--- 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>
 
diff -r 66beb9d92e43 -r 8bff286878bf src/HOL/Num.thy
--- 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"
diff -r 66beb9d92e43 -r 8bff286878bf src/HOL/Parity.thy
--- 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)
diff -r 66beb9d92e43 -r 8bff286878bf src/HOL/Word/Ancient_Numeral.thy
--- 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)
diff -r 66beb9d92e43 -r 8bff286878bf src/HOL/Word/Bits_Int.thy
--- 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>
 
diff -r 66beb9d92e43 -r 8bff286878bf src/HOL/Word/Word.thy
--- 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
 
diff -r 66beb9d92e43 -r 8bff286878bf src/HOL/ex/Word.thy
--- 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>