# HG changeset patch
# User haftmann
# Date 1580070932 0
# Node ID 0bb0cb558bf9a3d9854d47788074414ed48b4322
# Parent  554385d4cf59499ee20fc2eb005cf8c3b5af8d60
sketches of ideas still to come

diff -r 554385d4cf59 -r 0bb0cb558bf9 src/HOL/ex/Bit_Operations.thy
--- a/src/HOL/ex/Bit_Operations.thy	Sun Jan 26 20:35:32 2020 +0000
+++ b/src/HOL/ex/Bit_Operations.thy	Sun Jan 26 20:35:32 2020 +0000
@@ -9,14 +9,49 @@
     Main
 begin
 
+lemma bit_push_bit_eq_int:
+  \<open>bit (push_bit m k) n \<longleftrightarrow> m \<le> n \<and> bit k (n - m)\<close> for k :: int
+proof (cases \<open>m \<le> n\<close>)
+  case True
+  then obtain q where \<open>n = m + q\<close>
+    using le_Suc_ex by blast
+  with True show ?thesis
+    by (simp add: push_bit_eq_mult bit_def power_add)
+next
+  case False
+  then obtain q where \<open>m = Suc (n + q)\<close>
+    using less_imp_Suc_add not_le by blast
+  with False show ?thesis
+    by (simp add: push_bit_eq_mult bit_def power_add)
+qed
+
 context semiring_bits
 begin
 
+(*lemma range_rec:
+  \<open>2 ^ Suc n - 1 = 1 + 2 * (2 ^ n - 1)\<close>
+  sorry
+
+lemma even_range_div_iff:
+  \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> 2 ^ n = 0 \<or> m \<le> n\<close>
+  sorry*)
+
+(*lemma even_range_iff [simp]:
+  \<open>even (2 ^ n - 1) \<longleftrightarrow> n = 0\<close>
+  by (induction n) (simp_all only: range_rec, simp_all)
+
+lemma bit_range_iff:
+  \<open>bit (2 ^ m - 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close>
+  by (simp add: bit_def even_range_div_iff not_le)*)
+
 end
 
 context semiring_bit_shifts
 begin
 
+(*lemma bit_push_bit_iff:
+  \<open>bit (push_bit m a) n \<longleftrightarrow> n \<ge> m \<and> 2 ^ n \<noteq> 0 \<and> bit a (n - m)\<close>*)
+
 end
 
 
@@ -94,21 +129,64 @@
   \<open>flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)\<close>
   by (simp add: flip_bit_def)
 
+lemma take_bit_and [simp]:
+  \<open>take_bit n (a AND b) = take_bit n a AND take_bit n b\<close>
+  by (auto simp add: bit_eq_iff bit_take_bit_iff bit_and_iff)
+
+lemma take_bit_or [simp]:
+  \<open>take_bit n (a OR b) = take_bit n a OR take_bit n b\<close>
+  by (auto simp add: bit_eq_iff bit_take_bit_iff bit_or_iff)
+
+lemma take_bit_xor [simp]:
+  \<open>take_bit n (a XOR b) = take_bit n a XOR take_bit n b\<close>
+  by (auto simp add: bit_eq_iff bit_take_bit_iff bit_xor_iff)
+
 end
 
 class ring_bit_operations = semiring_bit_operations + ring_parity +
   fixes not :: \<open>'a \<Rightarrow> 'a\<close>  (\<open>NOT\<close>)
-  assumes bits_even_minus_1_div_exp_iff [simp]: \<open>even (- 1 div 2 ^ n) \<longleftrightarrow> 2 ^ n = 0\<close>
   assumes bit_not_iff: \<open>\<And>n. bit (NOT a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit a n\<close>
+  assumes minus_eq_not_minus_1: \<open>- a = NOT (a - 1)\<close>
 begin
 
+text \<open>
+  For the sake of code generation \<^const>\<open>not\<close> is specified as
+  definitional class operation.  Note that \<^const>\<open>not\<close> has no
+  sensible definition for unlimited but only positive bit strings
+  (type \<^typ>\<open>nat\<close>).
+\<close>
+
 lemma bits_minus_1_mod_2_eq [simp]:
   \<open>(- 1) mod 2 = 1\<close>
   by (simp add: mod_2_eq_odd)
 
+lemma not_eq_complement:
+  \<open>NOT a = - a - 1\<close>
+  using minus_eq_not_minus_1 [of \<open>a + 1\<close>] by simp
+
+lemma minus_eq_not_plus_1:
+  \<open>- a = NOT a + 1\<close>
+  using not_eq_complement [of a] by simp
+
+lemma bit_minus_iff:
+  \<open>bit (- a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit (a - 1) n\<close>
+  by (simp add: minus_eq_not_minus_1 bit_not_iff)
+
+lemma bit_not_exp_iff:
+  \<open>bit (NOT (2 ^ m)) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n \<noteq> m\<close>
+  by (auto simp add: bit_not_iff bit_exp_iff)
+
 lemma bit_minus_1_iff [simp]:
   \<open>bit (- 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0\<close>
-  by (simp add: bit_def)
+  by (simp add: bit_minus_iff)
+
+lemma bit_minus_exp_iff:
+  \<open>bit (- (2 ^ m)) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n \<ge> m\<close>
+  oops
+
+lemma bit_minus_2_iff [simp]:
+  \<open>bit (- 2) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n > 0\<close>
+  by (simp add: bit_minus_iff bit_1_iff)
 
 sublocale bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
   rewrites \<open>bit.xor = (XOR)\<close>
@@ -116,6 +194,7 @@
   interpret bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
     apply standard
              apply (auto simp add: bit_eq_iff bit_and_iff bit_or_iff bit_not_iff)
+     apply (simp_all add: bit_exp_iff)
      apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
     apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
     done
@@ -123,21 +202,16 @@
     by standard
   show \<open>boolean_algebra.xor (AND) (OR) NOT = (XOR)\<close> 
     apply (auto simp add: fun_eq_iff bit.xor_def bit_eq_iff bit_and_iff bit_or_iff bit_not_iff bit_xor_iff)
-         apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
+         apply (simp add: bit_exp_iff, simp add: bit_def)
         apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
        apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
-      apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
-     apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
-    apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
+      apply (simp_all add: bit_exp_iff, simp_all add: bit_def)
     done
 qed
 
-text \<open>
-  For the sake of code generation \<^const>\<open>not\<close> is specified as
-  definitional class operation.  Note that \<^const>\<open>not\<close> has no
-  sensible definition for unlimited but only positive bit strings
-  (type \<^typ>\<open>nat\<close>).
-\<close>
+lemma take_bit_not_take_bit:
+  \<open>take_bit n (NOT (take_bit n a)) = take_bit n (NOT a)\<close>
+  by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff)
 
 end
 
@@ -700,6 +774,8 @@
 
 instance proof
   fix k l :: int and n :: nat
+  show \<open>- k = NOT (k - 1)\<close>
+    by (simp add: not_int_def)
   show \<open>bit (k AND l) n \<longleftrightarrow> bit k n \<and> bit l n\<close>
   proof (rule sym, induction n arbitrary: k l)
     case 0
@@ -736,7 +812,7 @@
 
 lemma one_and_int_eq [simp]:
   "1 AND k = k mod 2" for k :: int
-  using and_int.rec [of 1] by (simp add: mod2_eq_if)
+  by (simp add: bit_eq_iff bit_and_iff mod2_eq_if) (auto simp add: bit_1_iff)
 
 lemma and_one_int_eq [simp]:
   "k AND 1 = k mod 2" for k :: int
@@ -763,29 +839,9 @@
   for k l :: int
   by (simp add: take_bit_eq_mod mod_eq_dvd_iff dvd_diff_commute)
 
-lemma take_bit_not_iff:
+lemma take_bit_not_iff_int:
   "take_bit n (NOT k) = take_bit n (NOT l) \<longleftrightarrow> take_bit n k = take_bit n l"
   for k l :: int
   by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff_int)
 
-lemma take_bit_not_take_bit:
-  \<open>take_bit n (NOT (take_bit n k)) = take_bit n (NOT k)\<close>
-  for k :: int
-  by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff)
-
-lemma take_bit_and [simp]:
-  "take_bit n (k AND l) = take_bit n k AND take_bit n l"
-  for k l :: int
-  by (auto simp add: bit_eq_iff bit_take_bit_iff bit_and_iff)
-
-lemma take_bit_or [simp]:
-  "take_bit n (k OR l) = take_bit n k OR take_bit n l"
-  for k l :: int
-  by (auto simp add: bit_eq_iff bit_take_bit_iff bit_or_iff)
-
-lemma take_bit_xor [simp]:
-  "take_bit n (k XOR l) = take_bit n k XOR take_bit n l"
-  for k l :: int
-  by (auto simp add: bit_eq_iff bit_take_bit_iff bit_xor_iff)
-
 end
diff -r 554385d4cf59 -r 0bb0cb558bf9 src/HOL/ex/Word.thy
--- a/src/HOL/ex/Word.thy	Sun Jan 26 20:35:32 2020 +0000
+++ b/src/HOL/ex/Word.thy	Sun Jan 26 20:35:32 2020 +0000
@@ -540,6 +540,18 @@
   qed
 qed
 
+lemma even_mult_exp_div_word_iff:
+  \<open>even (a * 2 ^ m div 2 ^ n) \<longleftrightarrow> \<not> (
+    m \<le> n \<and>
+    n < LENGTH('a) \<and> odd (a div 2 ^ (n - m)))\<close> for a :: \<open>'a::len word\<close>
+  by transfer
+    (auto simp flip: drop_bit_eq_div simp add: even_drop_bit_iff_not_bit bit_take_bit_iff,
+      simp_all flip: push_bit_eq_mult add: bit_push_bit_eq_int)
+
+(*lemma even_range_div_iff_word:
+  \<open>even ((2 ^ m - 1) div (2::'a word) ^ n) \<longleftrightarrow> 2 ^ n = (0::'a::len word) \<or> m \<le> n\<close>
+  by transfer (auto simp add: take_bit_of_range even_range_div_iff)*)
+
 instance word :: (len) semiring_bits
 proof
   show \<open>P a\<close> if stable: \<open>\<And>a. a div 2 = a \<Longrightarrow> P a\<close>
@@ -663,10 +675,10 @@
 
 lift_definition not_word :: "'a word \<Rightarrow> 'a word"
   is not
-  by (simp add: take_bit_not_iff)
+  by (simp add: take_bit_not_iff_int)
 
 lift_definition and_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
-  is "and"
+  is \<open>and\<close>
   by simp
 
 lift_definition or_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
@@ -679,8 +691,8 @@
 
 instance proof
   fix a b :: \<open>'a word\<close> and n :: nat
-  show \<open>even (- 1 div (2 :: 'a word) ^ n) \<longleftrightarrow> (2 :: 'a word) ^ n = 0\<close>
-    by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit)
+  show \<open>- a = NOT (a - 1)\<close>
+    by transfer (simp add: minus_eq_not_minus_1)
   show \<open>bit (NOT a) n \<longleftrightarrow> (2 :: 'a word) ^ n \<noteq> 0 \<and> \<not> bit a n\<close>
     by transfer (simp add: bit_not_iff)
   show \<open>bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>