# HG changeset patch
# User haftmann
# Date 1592471250 0
# Node ID 428609096812ecda4c20467e9f835e6dae5e6d42
# Parent  2efc5b8c7456cbcfe71e8f6434f3b473ec93a2d0
more lemmas and less name space pollution

diff -r 2efc5b8c7456 -r 428609096812 src/HOL/Library/Z2.thy
--- a/src/HOL/Library/Z2.thy	Thu Jun 18 09:07:30 2020 +0000
+++ b/src/HOL/Library/Z2.thy	Thu Jun 18 09:07:30 2020 +0000
@@ -52,9 +52,14 @@
 lemma set_Bit_eq [simp]: "set (Bit P) = P"
   by (rule Bit_inverse) rule
 
-lemma bit_eq_iff: "x = y \<longleftrightarrow> (set x \<longleftrightarrow> set y)"
+context
+begin
+
+qualified lemma bit_eq_iff: "x = y \<longleftrightarrow> (set x \<longleftrightarrow> set y)"
   by (auto simp add: set_inject)
 
+end
+
 lemma Bit_inject [simp]: "Bit P = Bit Q \<longleftrightarrow> (P \<longleftrightarrow> Q)"
   by (auto simp add: Bit_inject)
 
@@ -74,7 +79,7 @@
 lemma bit_eq_iff_set:
   "b = 0 \<longleftrightarrow> \<not> set b"
   "b = 1 \<longleftrightarrow> set b"
-  by (simp_all add: bit_eq_iff)
+  by (simp_all add: Z2.bit_eq_iff)
 
 lemma Bit [simp, code]:
   "Bit False = 0"
@@ -82,10 +87,10 @@
   by (simp_all add: zero_bit_def one_bit_def)
 
 lemma bit_not_0_iff [iff]: "x \<noteq> 0 \<longleftrightarrow> x = 1" for x :: bit
-  by (simp add: bit_eq_iff)
+  by (simp add: Z2.bit_eq_iff)
 
 lemma bit_not_1_iff [iff]: "x \<noteq> 1 \<longleftrightarrow> x = 0" for x :: bit
-  by (simp add: bit_eq_iff)
+  by (simp add: Z2.bit_eq_iff)
 
 lemma [code]:
   "HOL.equal 0 b \<longleftrightarrow> \<not> set b"
@@ -175,6 +180,45 @@
 lemma (in ring_1) of_int_of_bit_eq: "of_int (of_bit b) = of_bit b"
   by (cases b) simp_all
 
+
+subsection \<open>Bit structure\<close>
+
+instantiation bit :: semidom_modulo
+begin
+
+definition modulo_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close>
+  where [simp]: \<open>a mod b = a * of_bool (b = 0)\<close> for a b :: bit
+
+instance
+  by standard simp
+
+end
+
+instance bit :: semiring_bits
+  apply standard
+                apply (auto simp add: power_0_left power_add)
+  apply (metis bit_not_1_iff of_bool_eq(2))
+  done
+
+lemma bit_bit_iff [simp]:
+  \<open>bit b n \<longleftrightarrow> b = 1 \<and> n = 0\<close> for b :: bit
+  by (cases b; cases n) (simp_all add: bit_Suc)
+
+instantiation bit :: semiring_bit_shifts
+begin
+
+definition push_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close>
+  where \<open>push_bit n b = (if n = 0 then b else 0)\<close> for b :: bit
+
+definition drop_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close>
+  where \<open>drop_bit n b = (if n = 0 then b else 0)\<close> for b :: bit
+
+instance
+  by standard (simp_all add: push_bit_bit_def drop_bit_bit_def)
+
+end
+
+
 hide_const (open) set
 
 end
diff -r 2efc5b8c7456 -r 428609096812 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu Jun 18 09:07:30 2020 +0000
+++ b/src/HOL/Word/Word.thy	Thu Jun 18 09:07:30 2020 +0000
@@ -445,6 +445,10 @@
     by transfer (simp_all add: mod_2_eq_odd take_bit_Suc)
 qed
 
+lemma exp_eq_zero_iff:
+  \<open>2 ^ n = (0 :: 'a::len word) \<longleftrightarrow> n \<ge> LENGTH('a)\<close>
+  by transfer simp
+
 
 subsection \<open>Ordering\<close>
 
@@ -680,7 +684,8 @@
   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 simp add: take_bit_Suc)
+    using that by transfer
+      (auto dest: le_Suc_ex simp add: mod_2_eq_odd take_bit_Suc elim!: evenE)
   show \<open>(2 :: 'a word) ^ m div 2 ^ n = of_bool ((2 :: 'a word) ^ m \<noteq> 0 \<and> n \<le> m) * 2 ^ (m - n)\<close>
     for m n :: nat
     by transfer (simp, simp add: exp_div_exp_eq)
@@ -3566,16 +3571,26 @@
 
 subsubsection \<open>Mask\<close>
 
-lemma nth_mask [OF refl, simp]: "m = mask n \<Longrightarrow> test_bit m i \<longleftrightarrow> i < n \<and> i < size m"
-  apply (unfold mask_def test_bit_bl)
-  apply (simp only: word_1_bl [symmetric] shiftl_of_bl)
-  apply (clarsimp simp add: word_size)
-  apply (simp only: of_bl_def mask_lem word_of_int_hom_syms add_diff_cancel2)
-  apply (fold of_bl_def)
-  apply (simp add: word_1_bl)
-  apply (rule test_bit_of_bl [THEN trans, unfolded test_bit_bl word_size])
-  apply auto
-  done
+lemma mask_eq:
+  \<open>mask n = 2 ^ n - 1\<close>
+  by (simp add: mask_def shiftl_word_eq push_bit_eq_mult)
+
+lemma mask_Suc_rec:
+  \<open>mask (Suc n) = 2 * mask n + 1\<close>
+  by (simp add: mask_eq)
+
+context
+begin
+
+qualified lemma bit_mask_iff [simp]:
+  \<open>bit (mask m :: 'a::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> n < m\<close>
+  by (simp add: mask_eq bit_mask_iff exp_eq_zero_iff not_le)
+
+end
+
+lemma nth_mask [simp]:
+  \<open>(mask n :: 'a::len word) !! i \<longleftrightarrow> i < n \<and> i < size (mask n :: 'a word)\<close>
+  by (auto simp add: test_bit_word_eq word_size)
 
 lemma mask_bl: "mask n = of_bl (replicate n True)"
   by (auto simp add : test_bit_of_bl word_size intro: word_eqI)