# HG changeset patch
# User haftmann
# Date 1581243661 0
# Node ID 7ae4dcf332ae9a52a47b45ad773385b3145acda3
# Parent  5d5be87330b5cb8f61961ebddc739817d9f2dbe9
more lemmas

diff -r 5d5be87330b5 -r 7ae4dcf332ae src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Feb 08 15:18:58 2020 +0100
+++ b/src/HOL/List.thy	Sun Feb 09 10:21:01 2020 +0000
@@ -2791,6 +2791,15 @@
     by (induct xs ys rule: list_induct2) (simp_all add: prod_eqI)
 qed
 
+lemma hd_zip:
+  \<open>hd (zip xs ys) = (hd xs, hd ys)\<close> if \<open>xs \<noteq> []\<close> and \<open>ys \<noteq> []\<close>
+  using that by (cases xs; cases ys) simp_all
+
+lemma last_zip:
+  \<open>last (zip xs ys) = (last xs, last ys)\<close> if \<open>xs \<noteq> []\<close> and \<open>ys \<noteq> []\<close>
+    and \<open>length xs = length ys\<close>
+  using that by (cases xs rule: rev_cases; cases ys rule: rev_cases) simp_all
+
 
 subsubsection \<open>\<^const>\<open>list_all2\<close>\<close>
 
diff -r 5d5be87330b5 -r 7ae4dcf332ae src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sat Feb 08 15:18:58 2020 +0100
+++ b/src/HOL/Parity.thy	Sun Feb 09 10:21:01 2020 +0000
@@ -1106,6 +1106,10 @@
   \<open>even (drop_bit n a) \<longleftrightarrow> \<not> bit a n\<close>
   by (simp add: bit_iff_odd_drop_bit)
 
+lemma div_push_bit_of_1_eq_drop_bit:
+  \<open>a div push_bit n 1 = drop_bit n a\<close>
+  by (simp add: push_bit_eq_mult drop_bit_eq_div)
+
 lemma bits_ident:
   "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)
diff -r 5d5be87330b5 -r 7ae4dcf332ae src/HOL/ex/Bit_Lists.thy
--- a/src/HOL/ex/Bit_Lists.thy	Sat Feb 08 15:18:58 2020 +0100
+++ b/src/HOL/ex/Bit_Lists.thy	Sun Feb 09 10:21:01 2020 +0000
@@ -8,16 +8,6 @@
     Word "HOL-Library.More_List"
 begin
 
-lemma hd_zip:
-  \<open>hd (zip xs ys) = (hd xs, hd ys)\<close> if \<open>xs \<noteq> []\<close> and \<open>ys \<noteq> []\<close>
-  using that by (cases xs; cases ys) simp_all
-
-lemma last_zip:
-  \<open>last (zip xs ys) = (last xs, last ys)\<close> if \<open>xs \<noteq> []\<close> and \<open>ys \<noteq> []\<close>
-    and \<open>length xs = length ys\<close>
-  using that by (cases xs rule: rev_cases; cases ys rule: rev_cases) simp_all
-
-
 subsection \<open>Fragments of algebraic bit representations\<close>
 
 context comm_semiring_1