# HG changeset patch
# User haftmann
# Date 1522867956 -7200
# Node ID ac66cbe795e516051d54b0da4bf0d1e51c1229f2
# Parent  78a64f3f7125a29492db797a2b76cdbd4f611d4d
more bit operation conversions

diff -r 78a64f3f7125 -r ac66cbe795e5 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Tue Apr 03 15:36:51 2018 +0000
+++ b/src/HOL/Parity.thy	Wed Apr 04 20:52:36 2018 +0200
@@ -698,10 +698,83 @@
   "push_bit n (drop_bit n a) + take_bit n a = a"
   using div_mult_mod_eq by (simp add: push_bit_eq_mult take_bit_eq_mod drop_bit_eq_div)
 
+lemma push_bit_push_bit [simp]:
+  "push_bit m (push_bit n a) = push_bit (m + n) a"
+  by (simp add: push_bit_eq_mult power_add ac_simps)
+
 lemma take_bit_take_bit [simp]:
-  "take_bit n (take_bit n a) = take_bit n a"
-  by (simp add: take_bit_eq_mod)
-  
+  "take_bit m (take_bit n a) = take_bit (min m n) a"
+proof (cases "m \<le> n")
+  case True
+  then show ?thesis
+    by (simp add: take_bit_eq_mod not_le min_def mod_mod_cancel le_imp_power_dvd)
+next
+  case False
+  then have "n < m" and "min m n = n"
+    by simp_all
+  then have "2 ^ m = of_nat (2 ^ n) * of_nat (2 ^ (m - n))"
+    by (simp add: power_add [symmetric])
+  then have "a mod 2 ^ n mod 2 ^ m = a mod 2 ^ n mod (of_nat (2 ^ n) * of_nat (2 ^ (m - n)))"
+    by simp
+  also have "\<dots> = of_nat (2 ^ n) * (a mod 2 ^ n div of_nat (2 ^ n) mod of_nat (2 ^ (m - n))) + a mod 2 ^ n mod of_nat (2 ^ n)"
+    by (simp only: mod_mult2_eq')
+  finally show ?thesis
+    using \<open>min m n = n\<close> by (simp add: take_bit_eq_mod)
+qed
+
+lemma drop_bit_drop_bit [simp]:
+  "drop_bit m (drop_bit n a) = drop_bit (m + n) a"
+proof -
+  have "a div (2 ^ m * 2 ^ n) = a div (of_nat (2 ^ n) * of_nat (2 ^ m))"
+    by (simp add: ac_simps)
+  also have "\<dots> = a div of_nat (2 ^ n) div of_nat (2 ^ m)"
+    by (simp only: div_mult2_eq')
+  finally show ?thesis
+    by (simp add: drop_bit_eq_div power_add)
+qed
+
+lemma push_bit_take_bit:
+  "push_bit m (take_bit n a) = take_bit (m + n) (push_bit m a)"
+  by (simp add: push_bit_eq_mult take_bit_eq_mod power_add mult_mod_right ac_simps)
+
+lemma take_bit_push_bit:
+  "take_bit m (push_bit n a) = push_bit n (take_bit (m - n) a)"
+proof (cases "m \<le> n")
+  case True
+  then show ?thesis
+    by (simp_all add: push_bit_eq_mult take_bit_eq_mod mod_eq_0_iff_dvd dvd_power_le)
+next
+  case False
+  then show ?thesis
+    using push_bit_take_bit [of n "m - n" a]
+    by simp
+qed
+
+lemma take_bit_drop_bit:
+  "take_bit m (drop_bit n a) = drop_bit n (take_bit (m + n) a)"
+  using mod_mult2_eq' [of a "2 ^ n" "2 ^ m"]
+  by (simp add: drop_bit_eq_div take_bit_eq_mod power_add ac_simps)
+
+lemma drop_bit_take_bit:
+  "drop_bit m (take_bit n a) = take_bit (n - m) (drop_bit m a)"
+proof (cases "m \<le> n")
+  case True
+  then show ?thesis
+    using take_bit_drop_bit [of "n - m" m a] by simp
+next
+  case False
+  then have "a mod 2 ^ n div 2 ^ m = a mod 2 ^ n div 2 ^ (n + (m - n))"
+    by simp
+  also have "\<dots> = a mod 2 ^ n div (2 ^ n * 2 ^ (m - n))"
+    by (simp add: power_add)
+  also have "\<dots> = a mod 2 ^ n div (of_nat (2 ^ n) * of_nat (2 ^ (m - n)))"
+    by simp
+  also have "\<dots> = a mod 2 ^ n div of_nat (2 ^ n) div of_nat (2 ^ (m - n))"
+    by (simp only: div_mult2_eq')
+  finally show ?thesis
+    using False by (simp add: take_bit_eq_mod drop_bit_eq_div)
+qed
+
 lemma take_bit_0 [simp]:
   "take_bit 0 a = 0"
   by (simp add: take_bit_eq_mod)
@@ -794,35 +867,6 @@
   "push_bit n (a * 2) = push_bit n a * 2"
   by (simp add: push_bit_eq_mult ac_simps)
 
-lemma drop_bit_take_bit [simp]:
-  "drop_bit n (take_bit n a) = 0"
-  by (simp add: drop_bit_eq_div take_bit_eq_mod)
-
-lemma take_bit_drop_bit_commute:
-  "drop_bit m (take_bit n a) = take_bit (n - m) (drop_bit m a)"
-  for m n :: nat
-proof (cases "n \<ge> m")
-  case True
-  moreover define q where "q = n - m"
-  ultimately have "n - m = q" and "n = m + q"
-    by simp_all
-  moreover have "drop_bit m (take_bit (m + q) a) = take_bit q (drop_bit m a)"
-    using mod_mult2_eq' [of a "2 ^ m" "2 ^ q"]
-    by (simp add: drop_bit_eq_div take_bit_eq_mod power_add)
-  ultimately show ?thesis
-    by simp
-next
-  case False
-  moreover define q where "q = m - n"
-  ultimately have "m - n = q" and "m = n + q"
-    by simp_all
-  moreover have "drop_bit (n + q) (take_bit n a) = 0"
-    using div_mult2_eq' [of "a mod 2 ^ n" "2 ^ n" "2 ^ q"]
-    by (simp add: drop_bit_eq_div take_bit_eq_mod power_add div_mult2_eq)
-  ultimately show ?thesis
-    by simp
-qed
-
 end
 
 end