# HG changeset patch
# User haftmann
# Date 1571510463 -7200
# Node ID 38298c04c12e4f373fbe2a649306686fad3a7dff
# Parent  3ed399935d7c602dba239e258b23b1ddc5d3dda5
more lemmas

diff -r 3ed399935d7c -r 38298c04c12e src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Oct 19 16:16:24 2019 +0200
+++ b/src/HOL/List.thy	Sat Oct 19 20:41:03 2019 +0200
@@ -2698,6 +2698,42 @@
   with xs ys show ?thesis ..
 qed
 
+lemma semilattice_map2:
+  "semilattice (map2 (\<^bold>*))" if "semilattice (\<^bold>*)"
+    for f (infixl "\<^bold>*" 70)
+proof -
+  from that interpret semilattice f .
+  show ?thesis
+  proof
+    show "map2 (\<^bold>*) (map2 (\<^bold>*) xs ys) zs = map2 (\<^bold>*) xs (map2 (\<^bold>*) ys zs)"
+      for xs ys zs :: "'a list"
+    proof (induction "zip xs (zip ys zs)" arbitrary: xs ys zs)
+      case Nil
+      from Nil [symmetric] show ?case
+        by (auto simp add: zip_eq_Nil_iff)
+    next
+      case (Cons xyz xyzs)
+      from Cons.hyps(2) [symmetric] show ?case
+        by (rule zip_eq_ConsE) (erule zip_eq_ConsE,
+          auto intro: Cons.hyps(1) simp add: ac_simps)
+    qed
+    show "map2 (\<^bold>*) xs ys = map2 (\<^bold>*) ys xs"
+      for xs ys :: "'a list"
+    proof (induction "zip xs ys" arbitrary: xs ys)
+      case Nil
+      then show ?case
+        by (auto simp add: zip_eq_Nil_iff dest: sym)
+    next
+      case (Cons xy xys)
+      from Cons.hyps(2) [symmetric] show ?case
+        by (rule zip_eq_ConsE) (auto intro: Cons.hyps(1) simp add: ac_simps)
+    qed
+    show "map2 (\<^bold>*) xs xs = xs"
+      for xs :: "'a list"
+      by (induction xs) simp_all
+  qed
+qed
+
 lemma pair_list_eqI:
   assumes "map fst xs = map fst ys" and "map snd xs = map snd ys"
   shows "xs = ys"
diff -r 3ed399935d7c -r 38298c04c12e src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sat Oct 19 16:16:24 2019 +0200
+++ b/src/HOL/Parity.thy	Sat Oct 19 20:41:03 2019 +0200
@@ -448,6 +448,38 @@
   finally show ?thesis .
 qed
 
+lemma numeral_Bit0_div_2:
+  "numeral (num.Bit0 n) div 2 = numeral n"
+proof -
+  have "numeral (num.Bit0 n) = numeral n + numeral n"
+    by (simp only: numeral.simps)
+  also have "\<dots> = numeral n * 2"
+    by (simp add: mult_2_right)
+  finally have "numeral (num.Bit0 n) div 2 = numeral n * 2 div 2"
+    by simp
+  also have "\<dots> = numeral n"
+    by (rule nonzero_mult_div_cancel_right) simp
+  finally show ?thesis .
+qed
+
+lemma numeral_Bit1_div_2:
+  "numeral (num.Bit1 n) div 2 = numeral n"
+proof -
+  have "numeral (num.Bit1 n) = numeral n + numeral n + 1"
+    by (simp only: numeral.simps)
+  also have "\<dots> = numeral n * 2 + 1"
+    by (simp add: mult_2_right)
+  finally have "numeral (num.Bit1 n) div 2 = (numeral n * 2 + 1) div 2"
+    by simp
+  also have "\<dots> = numeral n * 2 div 2 + 1 div 2"
+    using dvd_triv_right by (rule div_plus_div_distrib_dvd_left)
+  also have "\<dots> = numeral n * 2 div 2"
+    by simp
+  also have "\<dots> = numeral n"
+    by (rule nonzero_mult_div_cancel_right) simp
+  finally show ?thesis .
+qed
+
 end
 
 class unique_euclidean_ring_with_nat = ring + unique_euclidean_semiring_with_nat
@@ -1061,4 +1093,8 @@
   "drop_bit n (Suc 0) = of_bool (n = 0)"
   using drop_bit_of_1 [where ?'a = nat] by simp
 
+lemma push_bit_minus_one:
+  "push_bit n (- 1 :: int) = - (2 ^ n)"
+  by (simp add: push_bit_eq_mult)
+
 end