# HG changeset patch
# User haftmann
# Date 1599468448 0
# Node ID bb002df3e82e3944021024f0c8578d1d1c3649a5
# Parent  5a6d8675bf4b72550e73a2b545205ee01d53a561
more on conversions

diff -r 5a6d8675bf4b -r bb002df3e82e src/HOL/Word/Conversions.thy
--- a/src/HOL/Word/Conversions.thy	Sat Sep 05 16:21:16 2020 +0000
+++ b/src/HOL/Word/Conversions.thy	Mon Sep 07 08:47:28 2020 +0000
@@ -13,6 +13,41 @@
 
 hide_const (open) unat uint sint word_of_int ucast scast
 
+context semiring_bits
+begin
+
+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
+
 
 subsection \<open>Conversions to word\<close>
 
@@ -246,8 +281,7 @@
     (auto simp add: bit_of_int_iff Bit_Operations.bit_signed_take_bit_iff min_def)
 
 lemma signed_push_bit_eq:
-  \<open>signed (push_bit n w) = take_bit (LENGTH('b) - Suc 0) (push_bit n (signed w))
-    OR of_bool (n < LENGTH('b) \<and> bit w (LENGTH('b) - Suc n)) * NOT (mask (LENGTH('b) - Suc 0))\<close>
+  \<open>signed (push_bit n w) = signed_take_bit (LENGTH('b) - 1) (push_bit n (signed w :: 'a))\<close>
   for w :: \<open>'b::len word\<close>
 proof (rule bit_eqI)
   fix m
@@ -256,18 +290,27 @@
   then have *: \<open>LENGTH('b) = Suc q\<close>
     by simp
   show \<open>bit (signed (push_bit n w)) m \<longleftrightarrow>
-    bit (take_bit (LENGTH('b) - Suc 0) (push_bit n (signed w)) OR
-      of_bool (n < LENGTH('b) \<and> bit w (LENGTH('b) - Suc n)) * NOT (mask (LENGTH('b) - Suc 0))) m\<close>
-  proof (cases \<open>n \<le> m\<close>)
+    bit (signed_take_bit (LENGTH('b) - 1) (push_bit n (signed w :: 'a))) m\<close>
+  proof (cases \<open>q \<le> m\<close>)
     case True
-    with \<open>2 ^ m \<noteq> 0\<close> have \<open>2 ^ (m - n) \<noteq> 0\<close>
-      by (metis (full_types) diff_add exp_add_not_zero_imp)
-    with True show ?thesis
-      by (auto simp add: * bit_signed_iff bit_push_bit_iff Parity.bit_push_bit_iff bit_or_iff bit_take_bit_iff bit_not_iff bit_mask_iff exp_eq_zero_iff min_def)
+    moreover define r where \<open>r = m - q\<close>
+    ultimately have \<open>m = q + r\<close>
+      by simp
+    moreover from \<open>m = q + r\<close> \<open>2 ^ m \<noteq> 0\<close> have \<open>2 ^ q \<noteq> 0\<close> \<open>2 ^ r \<noteq> 0\<close>
+      using exp_add_not_zero_imp_left [of q r] exp_add_not_zero_imp_right [of q r]
+      by simp_all
+    moreover from \<open>2 ^ q \<noteq> 0\<close> have \<open>2 ^ (q - n) \<noteq> 0\<close>
+      by (rule exp_not_zero_imp_exp_diff_not_zero)
+    ultimately show ?thesis
+      by (auto simp add: bit_signed_iff bit_signed_take_bit_iff bit_push_bit_iff Parity.bit_push_bit_iff
+      min_def * exp_eq_zero_iff le_diff_conv2)
   next
     case False
     then show ?thesis
-      by (simp add: * bit_signed_iff bit_push_bit_iff Parity.bit_push_bit_iff bit_or_iff bit_take_bit_iff bit_not_iff bit_mask_iff)
+      using exp_not_zero_imp_exp_diff_not_zero [of m n]
+      by (auto simp add: bit_signed_iff bit_signed_take_bit_iff bit_push_bit_iff Parity.bit_push_bit_iff
+      min_def not_le not_less * le_diff_conv2 less_diff_conv2 Parity.exp_eq_0_imp_not_bit exp_eq_0_imp_not_bit
+      exp_eq_zero_iff)
   qed
 qed
 
@@ -278,27 +321,32 @@
     (auto simp add: Bit_Operations.signed_take_bit_take_bit Bit_Operations.take_bit_signed_take_bit take_bit_of_int min_def less_Suc_eq)
 
 lemma signed_not_eq:
-  \<open>signed (NOT w) = take_bit LENGTH('b) (NOT (signed w)) OR of_bool (bit (NOT (signed w)) LENGTH('b)) * NOT (mask LENGTH('b))\<close>
+  \<open>signed (NOT w) = signed_take_bit LENGTH('b) (NOT (signed w))\<close>
   for w :: \<open>'b::len word\<close>
 proof (rule bit_eqI)
   fix n
   assume \<open>2 ^ n \<noteq> 0\<close>
+  define q where \<open>q = LENGTH('b) - Suc 0\<close>
+  then have *: \<open>LENGTH('b) = Suc q\<close>
+    by simp
   show \<open>bit (signed (NOT w)) n \<longleftrightarrow>
-    bit (take_bit LENGTH('b) (NOT (signed w)) OR
-    of_bool (bit (NOT (signed w)) LENGTH('b)) * NOT (mask LENGTH('b))) n\<close>
-  proof (cases \<open>LENGTH('b) \<le> n\<close>)
+    bit (signed_take_bit LENGTH('b) (NOT (signed w))) n\<close>
+  proof (cases \<open>q < n\<close>)
+    case True
+    moreover define r where \<open>r = n - Suc q\<close>
+    ultimately have \<open>n = r + Suc q\<close>
+      by simp
+    moreover from \<open>2 ^ n \<noteq> 0\<close> \<open>n = r + Suc q\<close>
+      have \<open>2 ^ Suc q \<noteq> 0\<close>
+      using exp_add_not_zero_imp_right by blast 
+    ultimately show ?thesis
+      by (simp add: * bit_signed_iff bit_not_iff bit_signed_take_bit_iff Bit_Operations.bit_not_iff min_def
+        exp_eq_zero_iff)
+  next
     case False
     then show ?thesis
-      by (auto simp add: bit_signed_iff bit_not_iff bit_or_iff bit_take_bit_iff bit_mask_iff Bit_Operations.bit_not_iff exp_eq_zero_iff)
-  next
-    case True
-    moreover define q where \<open>q = n - LENGTH('b)\<close>
-    ultimately have \<open>n = LENGTH('b) + q\<close>
-      by simp
-    with \<open>2 ^ n \<noteq> 0\<close> have \<open>2 ^ q \<noteq> 0\<close> \<open>2 ^ LENGTH('b) \<noteq> 0\<close>
-      by (simp_all add: power_add) (use mult_not_zero in blast)+
-    then show ?thesis
-      by (simp add: bit_signed_iff bit_not_iff bit_or_iff bit_take_bit_iff bit_mask_iff Bit_Operations.bit_not_iff exp_eq_zero_iff min_def not_le not_less le_diff_conv le_Suc_eq)
+      by (auto simp add: * bit_signed_iff bit_not_iff bit_signed_take_bit_iff Bit_Operations.bit_not_iff min_def
+        exp_eq_zero_iff)
   qed
 qed
 
@@ -445,31 +493,6 @@
   \<open>of_int (sint a) = signed a\<close>
   by transfer (simp_all add: take_bit_signed_take_bit)
 
-lemma sint_not_eq:
-  \<open>sint (NOT w) = signed_take_bit LENGTH('a) (NOT (sint w))\<close>
-  for w :: \<open>'a::len word\<close>
-  by (simp add: signed_not_eq signed_take_bit_def)
-
-lemma sint_push_bit_eq:
-  \<open>signed (push_bit n w) = signed_take_bit (LENGTH('a) - Suc 0) (push_bit n (signed w))\<close>
-  for w :: \<open>'a::len word\<close>
-  apply (transfer fixing: n; cases \<open>LENGTH('a)\<close>)
-   apply simp_all
-  apply (rule bit_eqI)
-  apply (simp add: bit_of_int_iff bit_signed_take_bit_iff bit_push_bit_iff min_def not_le le_diff_conv2)
-  apply auto
-           apply (metis le_add_diff_inverse mult_zero_left power_add)
-          apply (metis (no_types, lifting) diff_le_self le_add_diff_inverse mult_zero_left power_add)
-  using diff_diff_cancel apply fastforce
-  using diff_diff_cancel apply fastforce
-  apply (metis add_diff_cancel_right' diff_commute diff_le_self le_antisym less_imp_add_positive)
-      apply (metis le_add_diff_inverse mult_zero_left power_add)
-          apply (metis (no_types, lifting) diff_le_self le_add_diff_inverse mult_zero_left power_add)
-    apply (metis add.commute le_Suc_ex mult_zero_right power_add)
-   apply (metis le_add_diff_inverse mult_zero_left mult_zero_right power_add)
-  apply (metis le_add_diff_inverse mult_zero_right power_add)
-  done
-
 lemma sint_greater_eq:
   \<open>- (2 ^ (LENGTH('a) - Suc 0)) \<le> sint w\<close> for w :: \<open>'a::len word\<close>
 proof (cases \<open>bit w (LENGTH('a) - Suc 0)\<close>)
@@ -489,21 +512,44 @@
   by (cases \<open>bit w (LENGTH('a) - Suc 0)\<close>; transfer)
     (simp_all add: signed_take_bit_eq signed_take_bit_def take_bit_int_less_exp not_eq_complement mask_eq_exp_minus_1 OR_upper)
 
-context semiring_1
+context semiring_bit_shifts
+begin
+
+lemma unsigned_ucast_eq:
+  \<open>unsigned (ucast w :: 'c::len word) = take_bit LENGTH('c) (unsigned w)\<close>
+  for w :: \<open>'b::len word\<close>
+  by (rule bit_eqI) (simp add: bit_unsigned_iff Conversions.bit_unsigned_iff bit_take_bit_iff exp_eq_zero_iff not_le)
+
+end
+
+context ring_bit_operations
 begin
 
-lemma unsigned_ucase_eq:
-  \<open>unsigned (ucast w :: 'c::len word) = unsigned (take_bit LENGTH('c) w)\<close>
+lemma signed_ucast_eq:
+  \<open>signed (ucast w :: 'c::len word) = signed_take_bit (LENGTH('c) - Suc 0) (unsigned w)\<close>
   for w :: \<open>'b::len word\<close>
-  by transfer (simp add: ac_simps)
+proof (rule bit_eqI)
+  fix n
+  assume \<open>2 ^ n \<noteq> 0\<close>
+  then have \<open>2 ^ (min (LENGTH('c) - Suc 0) n) \<noteq> 0\<close>
+    by (simp add: min_def)
+      (metis (mono_tags) diff_diff_cancel local.exp_not_zero_imp_exp_diff_not_zero)
+  then show \<open>bit (signed (ucast w :: 'c::len word)) n \<longleftrightarrow> bit (signed_take_bit (LENGTH('c) - Suc 0) (unsigned w)) n\<close>
+    by (simp add: bit_signed_iff bit_unsigned_iff Conversions.bit_unsigned_iff bit_signed_take_bit_iff exp_eq_zero_iff not_le)
+qed
 
-lemma signed_ucast_eq:
-  \<open>signed (ucast w :: 'c::len word) =
-    take_bit (min LENGTH('b) LENGTH('c)) w OR of_bool (bit w (LENGTH('c) - Suc 0)) * NOT (mask LENGTH('c))\<close>
+lemma signed_scast_eq:
+  \<open>signed (scast w :: 'c::len word) = signed_take_bit (LENGTH('c) - Suc 0) (signed w)\<close>
   for w :: \<open>'b::len word\<close>
-  by (transfer, rule bit_eqI)
-    (simp_all add: bit_take_bit_iff bit_signed_take_bit_iff bit_or_iff bit_not_iff bit_mask_iff
-      not_less not_le min_def le_diff_conv less_diff_conv2 le_Suc_eq)
+proof (rule bit_eqI)
+  fix n
+  assume \<open>2 ^ n \<noteq> 0\<close>
+  then have \<open>2 ^ (min (LENGTH('c) - Suc 0) n) \<noteq> 0\<close>
+    by (simp add: min_def)
+      (metis (mono_tags) diff_diff_cancel local.exp_not_zero_imp_exp_diff_not_zero)
+  then show \<open>bit (signed (scast w :: 'c::len word)) n \<longleftrightarrow> bit (signed_take_bit (LENGTH('c) - Suc 0) (signed w)) n\<close>
+    by (simp add: bit_signed_iff bit_unsigned_iff Conversions.bit_signed_iff bit_signed_take_bit_iff exp_eq_zero_iff not_le)
+qed
 
 end
 
diff -r 5a6d8675bf4b -r bb002df3e82e src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sat Sep 05 16:21:16 2020 +0000
+++ b/src/HOL/Word/Word.thy	Mon Sep 07 08:47:28 2020 +0000
@@ -1042,6 +1042,22 @@
   \<open>((=) ===> pcr_word ===> pcr_word) flip_bit flip_bit\<close>
   by (unfold flip_bit_def) transfer_prover
 
+lemma signed_take_bit_word_transfer [transfer_rule]:
+  \<open>((=) ===> pcr_word ===> pcr_word)
+    (\<lambda>n k. signed_take_bit n (take_bit LENGTH('a::len) k))
+    (signed_take_bit :: nat \<Rightarrow> 'a word \<Rightarrow> 'a word)\<close>
+proof -
+  let ?K = \<open>\<lambda>n (k :: int). take_bit (min LENGTH('a) n) k OR of_bool (n < LENGTH('a) \<and> bit k n) * NOT (mask n)\<close>
+  let ?W = \<open>\<lambda>n (w :: 'a word). take_bit n w OR of_bool (bit w n) * NOT (mask n)\<close>
+  have \<open>((=) ===> pcr_word ===> pcr_word) ?K ?W\<close>
+    by transfer_prover
+  also have \<open>?K = (\<lambda>n k. signed_take_bit n (take_bit LENGTH('a::len) k))\<close>
+    by (simp add: fun_eq_iff signed_take_bit_def bit_take_bit_iff ac_simps)
+  also have \<open>?W = signed_take_bit\<close>
+    by (simp add: fun_eq_iff signed_take_bit_def)
+  finally show ?thesis .
+qed
+
 end
 
 instantiation word :: (len) semiring_bit_syntax