# HG changeset patch
# User haftmann
# Date 1600336650 0
# Node ID 5193570b739a22d4403892e071fd4f4c174f4e4d
# Parent  d488d643e677c6be33ebe14bf03bc62120cbd655
more lemmas

diff -r d488d643e677 -r 5193570b739a src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Sep 15 08:57:47 2020 +0200
+++ b/src/HOL/Divides.thy	Thu Sep 17 09:57:30 2020 +0000
@@ -1251,6 +1251,87 @@
   code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
 
+subsection \<open>More on bit operations\<close>
+
+lemma take_bit_incr_eq:
+  \<open>take_bit n (k + 1) = 1 + take_bit n k\<close> if \<open>take_bit n k \<noteq> 2 ^ n - 1\<close>
+  for k :: int
+proof -
+  from that have \<open>2 ^ n \<noteq> k mod 2 ^ n + 1\<close>
+    by (simp add: take_bit_eq_mod)
+  moreover have \<open>k mod 2 ^ n < 2 ^ n\<close>
+    by simp
+  ultimately have *: \<open>k mod 2 ^ n + 1 < 2 ^ n\<close>
+    by linarith
+  have \<open>(k + 1) mod 2 ^ n = (k mod 2 ^ n + 1) mod 2 ^ n\<close>
+    by (simp add: mod_simps)
+  also have \<open>\<dots> = k mod 2 ^ n + 1\<close>
+    using * by (simp add: zmod_trival_iff)
+  finally have \<open>(k + 1) mod 2 ^ n = k mod 2 ^ n + 1\<close> .
+  then show ?thesis
+    by (simp add: take_bit_eq_mod)
+qed
+
+lemma take_bit_decr_eq:
+  \<open>take_bit n (k - 1) = take_bit n k - 1\<close> if \<open>take_bit n k \<noteq> 0\<close>
+  for k :: int
+proof -
+  from that have \<open>k mod 2 ^ n \<noteq> 0\<close>
+    by (simp add: take_bit_eq_mod)
+  moreover have \<open>k mod 2 ^ n \<ge> 0\<close> \<open>k mod 2 ^ n < 2 ^ n\<close>
+    by simp_all
+  ultimately have *: \<open>k mod 2 ^ n > 0\<close>
+    by linarith
+  have \<open>(k - 1) mod 2 ^ n = (k mod 2 ^ n - 1) mod 2 ^ n\<close>
+    by (simp add: mod_simps)
+  also have \<open>\<dots> = k mod 2 ^ n - 1\<close>
+    by (simp add: zmod_trival_iff)
+      (use \<open>k mod 2 ^ n < 2 ^ n\<close> * in linarith)
+  finally have \<open>(k - 1) mod 2 ^ n = k mod 2 ^ n - 1\<close> .
+  then show ?thesis
+    by (simp add: take_bit_eq_mod)
+qed
+
+lemma take_bit_int_less_eq_self_iff:
+  \<open>take_bit n k \<le> k \<longleftrightarrow> 0 \<le> k\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+  for k :: int
+proof
+  assume ?P
+  show ?Q
+  proof (rule ccontr)
+    assume \<open>\<not> 0 \<le> k\<close>
+    then have \<open>k < 0\<close>
+      by simp
+    with \<open>?P\<close>
+    have \<open>take_bit n k < 0\<close>
+      by (rule le_less_trans)
+    then show False
+      by simp
+  qed
+next
+  assume ?Q
+  then show ?P
+    by (simp add: take_bit_eq_mod zmod_le_nonneg_dividend)
+qed
+
+lemma take_bit_int_less_self_iff:
+  \<open>take_bit n k < k \<longleftrightarrow> 2 ^ n \<le> k\<close>
+  for k :: int
+  by (auto simp add: less_le take_bit_int_less_eq_self_iff take_bit_int_eq_self_iff
+    intro: order_trans [of 0 \<open>2 ^ n\<close> k])
+
+lemma take_bit_int_greater_self_iff:
+  \<open>k < take_bit n k \<longleftrightarrow> k < 0\<close>
+  for k :: int
+  using take_bit_int_less_eq_self_iff [of n k] by auto
+
+lemma take_bit_int_greater_eq_self_iff:
+  \<open>k \<le> take_bit n k \<longleftrightarrow> k < 2 ^ n\<close>
+  for k :: int
+  by (auto simp add: le_less take_bit_int_greater_self_iff take_bit_int_eq_self_iff
+    dest: sym not_sym intro: less_trans [of k 0 \<open>2 ^ n\<close>])
+
+
 subsection \<open>Lemmas of doubtful value\<close>
 
 lemma div_geq: "m div n = Suc ((m - n) div n)" if "0 < n" and " \<not> m < n" for m n :: nat
diff -r d488d643e677 -r 5193570b739a src/HOL/Library/Bit_Operations.thy
--- a/src/HOL/Library/Bit_Operations.thy	Tue Sep 15 08:57:47 2020 +0200
+++ b/src/HOL/Library/Bit_Operations.thy	Thu Sep 17 09:57:30 2020 +0000
@@ -1106,23 +1106,45 @@
   for k :: int
   by (simp add: signed_take_bit_def not_less concat_bit_def)
 
-lemma signed_take_bit_greater_eq:
+lemma signed_take_bit_int_eq_self_iff:
+  \<open>signed_take_bit n k = k \<longleftrightarrow> - (2 ^ n) \<le> k \<and> k < 2 ^ n\<close>
+  for k :: int
+  by (auto simp add: signed_take_bit_eq_take_bit_shift take_bit_int_eq_self_iff algebra_simps)
+
+lemma signed_take_bit_int_less_eq_self_iff:
+  \<open>signed_take_bit n k \<le> k \<longleftrightarrow> - (2 ^ n) \<le> k\<close>
+  for k :: int
+  by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_less_eq_self_iff algebra_simps)
+    linarith
+
+lemma signed_take_bit_int_less_self_iff:
+  \<open>signed_take_bit n k < k \<longleftrightarrow> 2 ^ n \<le> k\<close>
+  for k :: int
+  by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_less_self_iff algebra_simps)
+
+lemma signed_take_bit_int_greater_self_iff:
+  \<open>k < signed_take_bit n k \<longleftrightarrow> k < - (2 ^ n)\<close>
+  for k :: int
+  by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_greater_self_iff algebra_simps)
+    linarith
+
+lemma signed_take_bit_int_greater_eq_self_iff:
+  \<open>k \<le> signed_take_bit n k \<longleftrightarrow> k < 2 ^ n\<close>
+  for k :: int
+  by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_greater_eq_self_iff algebra_simps)
+
+lemma signed_take_bit_int_greater_eq:
   \<open>k + 2 ^ Suc n \<le> signed_take_bit n k\<close> if \<open>k < - (2 ^ n)\<close>
   for k :: int
   using that take_bit_greater_eq [of \<open>k + 2 ^ n\<close> \<open>Suc n\<close>]
   by (simp add: signed_take_bit_eq_take_bit_shift)
 
-lemma signed_take_bit_less_eq:
+lemma signed_take_bit_int_less_eq:
   \<open>signed_take_bit n k \<le> k - 2 ^ Suc n\<close> if \<open>k \<ge> 2 ^ n\<close>
   for k :: int
   using that take_bit_less_eq [of \<open>Suc n\<close> \<open>k + 2 ^ n\<close>]
   by (simp add: signed_take_bit_eq_take_bit_shift)
 
-lemma signed_take_bit_eq_self:
-  \<open>signed_take_bit n k = k\<close> if \<open>- (2 ^ n) \<le> k\<close> \<open>k < 2 ^ n\<close>
-  for k :: int
-  using that by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_eq_self)
-
 lemma signed_take_bit_Suc_bit0 [simp]:
   \<open>signed_take_bit (Suc n) (numeral (Num.Bit0 k)) = signed_take_bit n (numeral k) * (2 :: int)\<close>
   by (simp add: signed_take_bit_Suc)
diff -r d488d643e677 -r 5193570b739a src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Tue Sep 15 08:57:47 2020 +0200
+++ b/src/HOL/Parity.thy	Thu Sep 17 09:57:30 2020 +0000
@@ -1024,6 +1024,37 @@
   qed
 qed
 
+lemma
+  exp_add_not_zero_imp_left: \<open>2 ^ m \<noteq> 0\<close>
+  and exp_add_not_zero_imp_right: \<open>2 ^ n \<noteq> 0\<close>
+  if \<open>2 ^ (m + n) \<noteq> 0\<close>
+proof -
+  have \<open>\<not> (2 ^ m = 0 \<or> 2 ^ n = 0)\<close>
+  proof (rule notI)
+    assume \<open>2 ^ m = 0 \<or> 2 ^ n = 0\<close>
+    then have \<open>2 ^ (m + n) = 0\<close>
+      by (rule disjE) (simp_all add: power_add)
+    with that show False ..
+  qed
+  then show \<open>2 ^ m \<noteq> 0\<close> and \<open>2 ^ n \<noteq> 0\<close>
+    by simp_all
+qed
+
+lemma exp_not_zero_imp_exp_diff_not_zero:
+  \<open>2 ^ (n - m) \<noteq> 0\<close> if \<open>2 ^ n \<noteq> 0\<close>
+proof (cases \<open>m \<le> n\<close>)
+  case True
+  moreover define q where \<open>q = n - m\<close>
+  ultimately have \<open>n = m + q\<close>
+    by simp
+  with that show ?thesis
+    by (simp add: exp_add_not_zero_imp_right)
+next
+  case False
+  with that show ?thesis
+    by simp
+qed
+
 end
 
 lemma nat_bit_induct [case_names zero even odd]:
@@ -1147,7 +1178,7 @@
     also have "\<dots> = - int (2 * n) - 1"
       by (simp add: algebra_simps)
     finally show ?case
-      using even by simp
+      using even.prems by simp
   next
     case (odd n)
     have "P (- int (Suc n) * 2)"
@@ -1155,7 +1186,7 @@
     also have "\<dots> = - int (Suc (2 * n)) - 1"
       by (simp add: algebra_simps)
     finally show ?case
-      using odd by simp
+      using odd.prems by simp
   qed
 qed
 
@@ -1584,6 +1615,56 @@
   \<open>bit (push_bit m k) n \<longleftrightarrow> m \<le> n \<and> bit k (n - m)\<close> for k :: int
   by (auto simp add: bit_push_bit_iff)
 
+lemma take_bit_nat_less_exp:
+  \<open>take_bit n m < 2 ^ n\<close> for n m ::nat 
+  by (simp add: take_bit_eq_mod)
+
+lemma take_bit_nat_eq_self_iff:
+  \<open>take_bit n m = m \<longleftrightarrow> m < 2 ^ n\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+  for n m :: nat
+proof
+  assume ?P
+  moreover note take_bit_nat_less_exp [of n m]
+  ultimately show ?Q
+    by simp
+next
+  assume ?Q
+  then show ?P
+    by (simp add: take_bit_eq_mod)
+qed
+
+lemma take_bit_nat_less_eq_self:
+  \<open>take_bit n m \<le> m\<close> for n m :: nat
+  by (simp add: take_bit_eq_mod)
+
+lemma take_bit_nonnegative [simp]:
+  \<open>take_bit n k \<ge> 0\<close>
+    for k :: int
+  by (simp add: take_bit_eq_mod)
+
+lemma not_take_bit_negative [simp]:
+  \<open>\<not> take_bit n k < 0\<close>
+    for k :: int
+  by (simp add: not_less)
+
+lemma take_bit_int_less_exp:
+  \<open>take_bit n k < 2 ^ n\<close> for k :: int
+  by (simp add: take_bit_eq_mod)
+
+lemma take_bit_int_eq_self_iff:
+  \<open>take_bit n k = k \<longleftrightarrow> 0 \<le> k \<and> k < 2 ^ n\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+  for k :: int
+proof
+  assume ?P
+  moreover note take_bit_int_less_exp [of n k] take_bit_nonnegative [of n k]
+  ultimately show ?Q
+    by simp
+next
+  assume ?Q
+  then show ?P
+    by (simp add: take_bit_eq_mod)
+qed
+
 class unique_euclidean_semiring_with_bit_shifts =
   unique_euclidean_semiring_with_nat + semiring_bit_shifts
 begin
@@ -1752,10 +1833,6 @@
   "drop_bit n (Suc 0) = of_bool (n = 0)"
   using drop_bit_of_1 [where ?'a = nat] by simp
 
-lemma take_bit_eq_self:
-  \<open>take_bit n m = m\<close> if \<open>m < 2 ^ n\<close> for n m :: nat
-  using that by (simp add: take_bit_eq_mod)
-
 lemma push_bit_minus_one:
   "push_bit n (- 1 :: int) = - (2 ^ n)"
   by (simp add: push_bit_eq_mult)
@@ -1782,24 +1859,6 @@
     for k l :: int
   by (simp add: take_bit_eq_mod mod_diff_eq)
 
-lemma take_bit_nonnegative [simp]:
-  \<open>take_bit n k \<ge> 0\<close>
-    for k :: int
-  by (simp add: take_bit_eq_mod)
-
-lemma not_take_bit_negative [simp]:
-  \<open>\<not> take_bit n k < 0\<close>
-    for k :: int
-  by (simp add: not_less)
-
-lemma take_bit_int_less_exp:
-  \<open>take_bit n k < 2 ^ n\<close> for k :: int
-  by (simp add: take_bit_eq_mod)
-
-lemma take_bit_int_eq_self:
-  \<open>take_bit n k = k\<close> if \<open>0 \<le> k\<close> \<open>k < 2 ^ n\<close> for k :: int
-  using that by (simp add: take_bit_eq_mod)
-
 lemma bit_imp_take_bit_positive:
   \<open>0 < take_bit m k\<close> if \<open>n < m\<close> and \<open>bit k n\<close> for k :: int
 proof (rule ccontr)
diff -r d488d643e677 -r 5193570b739a src/HOL/Word/Bits_Int.thy
--- a/src/HOL/Word/Bits_Int.thy	Tue Sep 15 08:57:47 2020 +0200
+++ b/src/HOL/Word/Bits_Int.thy	Thu Sep 17 09:57:30 2020 +0000
@@ -372,11 +372,11 @@
   
 lemma sbintrunc_inc:
   \<open>k + 2 ^ Suc n \<le> sbintrunc n k\<close> if \<open>k < - (2 ^ n)\<close>
-  using that by (fact signed_take_bit_greater_eq)
+  using that by (fact signed_take_bit_int_greater_eq)
   
 lemma sbintrunc_dec:
   \<open>sbintrunc n k \<le> k - 2 ^ (Suc n)\<close> if \<open>k \<ge> 2 ^ n\<close>
-  using that by (fact signed_take_bit_less_eq)
+  using that by (fact signed_take_bit_int_less_eq)
 
 lemma bintr_ge0: "0 \<le> bintrunc n w"
   by (simp add: bintrunc_mod2p)
diff -r d488d643e677 -r 5193570b739a src/HOL/Word/Conversions.thy
--- a/src/HOL/Word/Conversions.thy	Tue Sep 15 08:57:47 2020 +0200
+++ b/src/HOL/Word/Conversions.thy	Thu Sep 17 09:57:30 2020 +0000
@@ -455,7 +455,7 @@
     by (simp add: nat_less_iff take_bit_int_less_exp)
   finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k div take_bit LENGTH('a) l) =
     (nat \<circ> take_bit LENGTH('a)) k div (nat \<circ> take_bit LENGTH('a)) l\<close>
-    by (simp add: nat_take_bit_eq div_int_pos_iff nat_div_distrib take_bit_eq_self)
+    by (simp add: nat_take_bit_eq div_int_pos_iff nat_div_distrib take_bit_nat_eq_self_iff)
 qed
 
 lemma unat_mod_distrib:
@@ -468,7 +468,7 @@
     by (simp add: nat_less_iff take_bit_int_less_exp)
   finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k mod take_bit LENGTH('a) l) =
     (nat \<circ> take_bit LENGTH('a)) k mod (nat \<circ> take_bit LENGTH('a)) l\<close>
-    by (simp add: nat_take_bit_eq mod_int_pos_iff less_le nat_mod_distrib take_bit_eq_self)
+    by (simp add: nat_take_bit_eq mod_int_pos_iff less_le nat_mod_distrib take_bit_nat_eq_self_iff)
 qed
 
 lemma uint_div_distrib:
diff -r d488d643e677 -r 5193570b739a src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Tue Sep 15 08:57:47 2020 +0200
+++ b/src/HOL/Word/Word.thy	Thu Sep 17 09:57:30 2020 +0000
@@ -358,7 +358,7 @@
       by (auto simp add: word_greater_zero_iff of_nat_word_eq_0_iff l)
     moreover from \<open>n < 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - 1)\<close>
       using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>]
-      by (cases \<open>m = 0\<close>) (simp_all add: not_less take_bit_eq_self ac_simps l)
+      by (simp add: l take_bit_eq_mod)
     ultimately have \<open>P (2 * of_nat n)\<close>
       by (rule word_even)
     then show ?case
@@ -371,7 +371,7 @@
       by simp
     moreover from \<open>Suc n \<le> 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - 1)\<close>
       using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>]
-      by (cases \<open>m = 0\<close>) (simp_all add: not_less take_bit_eq_self ac_simps l)
+      by (simp add: l take_bit_eq_mod)
     ultimately have \<open>P (1 + 2 * of_nat n)\<close>
       by (rule word_odd)
     then show ?case
@@ -1396,8 +1396,8 @@
   "n = LENGTH('a::len) \<Longrightarrow>
     td_ext (unat :: 'a word \<Rightarrow> nat) of_nat (unats n) (\<lambda>i. i mod 2 ^ n)"
   apply (standard; transfer)
-     apply (simp_all add: unats_def take_bit_int_less_exp take_bit_of_nat take_bit_eq_self)
-  apply (simp add: take_bit_eq_mod)
+     apply (simp_all add: unats_def take_bit_int_less_exp take_bit_of_nat take_bit_nat_eq_self_iff
+      flip: take_bit_eq_mod)
   done
 
 lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm]
@@ -3882,7 +3882,7 @@
     by (cases \<open>LENGTH('a)\<close>) simp_all
   have *: \<open>sint x + sint y + 2 ^ Suc n > signed_take_bit n (sint x + sint y) \<Longrightarrow> sint x + sint y \<ge> - (2 ^ n)\<close>
     \<open>signed_take_bit n (sint x + sint y) > sint x + sint y - 2 ^ Suc n \<Longrightarrow> 2 ^ n > sint x + sint y\<close>
-    using signed_take_bit_greater_eq [of \<open>sint x + sint y\<close> n] signed_take_bit_less_eq [of n \<open>sint x + sint y\<close>]
+    using signed_take_bit_int_greater_eq [of \<open>sint x + sint y\<close> n] signed_take_bit_int_less_eq [of n \<open>sint x + sint y\<close>]
     by (auto intro: ccontr)
   have \<open>sint x + sint y = sint (x + y) \<longleftrightarrow>
     (sint (x + y) < 0 \<longleftrightarrow> sint x < 0) \<or>
@@ -4433,7 +4433,7 @@
     apply (subst take_bit_diff [symmetric])
     apply (subst nat_take_bit_eq)
     apply (simp add: nat_le_eq_zle)
-    apply (simp add: nat_diff_distrib take_bit_eq_self less_imp_diff_less bintr_lt2p)
+    apply (simp add: nat_diff_distrib take_bit_nat_eq_self_iff less_imp_diff_less bintr_lt2p)
     done
 qed