# HG changeset patch
# User haftmann
# Date 1555925635 0
# Node ID 49a65e3f04c94ea12d254b95d18fa3355769f644
# Parent  b4bf82ed0ad5acfd85b8825c75d4b1fad38e86ef
consolidated map2 clones

diff -r b4bf82ed0ad5 -r 49a65e3f04c9 src/HOL/Word/Bits_Int.thy
--- a/src/HOL/Word/Bits_Int.thy	Mon Apr 22 09:33:55 2019 +0000
+++ b/src/HOL/Word/Bits_Int.thy	Mon Apr 22 09:33:55 2019 +0000
@@ -2753,7 +2753,7 @@
 lemma bl_or_bin: "map2 (\<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)"
   by (simp add: bin_to_bl_def bl_or_aux_bin)
 
-lemma bl_xor_bin: "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)"
-  by (simp only: bin_to_bl_def bl_xor_aux_bin map2_Nil)
+lemma bl_xor_bin: "map2 (\<noteq>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)"
+  using bl_xor_aux_bin by (simp add: bin_to_bl_def)
 
 end
diff -r b4bf82ed0ad5 -r 49a65e3f04c9 src/HOL/Word/Misc_Auxiliary.thy
--- a/src/HOL/Word/Misc_Auxiliary.thy	Mon Apr 22 09:33:55 2019 +0000
+++ b/src/HOL/Word/Misc_Auxiliary.thy	Mon Apr 22 09:33:55 2019 +0000
@@ -140,21 +140,6 @@
   by (simp add: numeral_eq_Suc)
 
 
-subsection \<open>Simultaneous map\<close>
-
-definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
-  where "map2 f as bs = map (case_prod f) (zip as bs)"
-
-lemma map2_Nil [simp, code]: "map2 f [] ys = []"
-  by (auto simp: map2_def)
-
-lemma map2_Nil2 [simp, code]: "map2 f xs [] = []"
-  by (auto simp: map2_def)
-
-lemma map2_Cons [simp, code]: "map2 f (x # xs) (y # ys) = f x y # map2 f xs ys"
-  by (auto simp: map2_def)
-
-
 subsection \<open>Auxiliary: Range projection\<close>
 
 definition bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> 'a list"
diff -r b4bf82ed0ad5 -r 49a65e3f04c9 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Mon Apr 22 09:33:55 2019 +0000
+++ b/src/HOL/Word/Word.thy	Mon Apr 22 09:33:55 2019 +0000
@@ -2561,13 +2561,13 @@
   by (auto intro: word_eqI simp add: test_bit_set_gen word_size)
 
 lemma rbl_word_or: "rev (to_bl (x OR y)) = map2 (\<or>) (rev (to_bl x)) (rev (to_bl y))"
-  by (simp add: map2_def zip_rev bl_word_or rev_map)
+  by (simp add: zip_rev bl_word_or rev_map)
 
 lemma rbl_word_and: "rev (to_bl (x AND y)) = map2 (\<and>) (rev (to_bl x)) (rev (to_bl y))"
-  by (simp add: map2_def zip_rev bl_word_and rev_map)
+  by (simp add: zip_rev bl_word_and rev_map)
 
 lemma rbl_word_xor: "rev (to_bl (x XOR y)) = map2 (\<noteq>) (rev (to_bl x)) (rev (to_bl y))"
-  by (simp add: map2_def zip_rev bl_word_xor rev_map)
+  by (simp add: zip_rev bl_word_xor rev_map)
 
 lemma rbl_word_not: "rev (to_bl (NOT x)) = map Not (rev (to_bl x))"
   by (simp add: bl_word_not rev_map)
@@ -3026,7 +3026,7 @@
   apply (case_tac m)
    apply auto
   apply (drule_tac t="length xs" for xs in sym)
-  apply (auto simp: map2_def zip_replicate o_def)
+  apply (auto simp: zip_replicate o_def)
   done
 
 lemma align_lem_and [rule_format] :
@@ -3041,7 +3041,7 @@
   apply (case_tac m)
   apply auto
   apply (drule_tac t="length xs" for xs in sym)
-  apply (auto simp: map2_def zip_replicate o_def map_replicate_const)
+  apply (auto simp: zip_replicate o_def map_replicate_const)
   done
 
 lemma aligned_bl_add_size [OF refl]:
@@ -3924,7 +3924,6 @@
     butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys)"
   apply (induct xs)
    apply auto
-     apply (unfold map2_def)
      apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
   done
 
@@ -3940,7 +3939,7 @@
 lemma rotater1_map2:
   "length xs = length ys \<Longrightarrow>
     rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)"
-  by (simp add: map2_def rotater1_map rotater1_zip)
+  by (simp add: rotater1_map rotater1_zip)
 
 lemmas lrth =
   box_equals [OF asm_rl length_rotater [symmetric]
@@ -3955,7 +3954,7 @@
 lemma rotate1_map2:
   "length xs = length ys \<Longrightarrow>
     rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)"
-  by (cases xs; cases ys) (auto simp: map2_def)
+  by (cases xs; cases ys) auto
 
 lemmas lth = box_equals [OF asm_rl length_rotate [symmetric]
   length_rotate [symmetric], THEN rotate1_map2]
@@ -4307,7 +4306,7 @@
     by simp
   also have "map2 (\<and>) \<dots> (to_bl (mask n::'a::len word)) =
       replicate n' False @ drop n' (to_bl w)"
-    unfolding to_bl_mask n'_def map2_def by (subst zip_append) auto
+    unfolding to_bl_mask n'_def by (subst zip_append) auto
   finally show ?thesis .
 qed
 
diff -r b4bf82ed0ad5 -r 49a65e3f04c9 src/HOL/Word/Word_Bitwise.thy
--- a/src/HOL/Word/Word_Bitwise.thy	Mon Apr 22 09:33:55 2019 +0000
+++ b/src/HOL/Word/Word_Bitwise.thy	Mon Apr 22 09:33:55 2019 +0000
@@ -50,7 +50,7 @@
   done
 
 lemma rbl_word_if: "rev (to_bl (if P then x else y)) = map2 (If P) (rev (to_bl x)) (rev (to_bl y))"
-  by (simp add: map2_def split_def)
+  by (simp add: split_def)
 
 lemma rbl_add_carry_Cons:
   "(if car then rbl_succ else id) (rbl_add (x # xs) (y # ys)) =
@@ -496,7 +496,7 @@
    put_simpset no_split_ss \<^context> addsimps
     @{thms list.simps split_conv replicate.simps list.map
                                 zip_Cons_Cons zip_Nil drop_Suc_Cons drop_0 drop_Nil
-                                foldr.simps map2_Cons map2_Nil takefill_Suc_Cons
+                                foldr.simps list.map zip.simps(1) zip_Nil zip_Cons_Cons takefill_Suc_Cons
                                 takefill_Suc_Nil takefill.Z rbl_succ2_simps
                                 rbl_plus_simps rev_bin_to_bl_simps append.simps
                                 takefill_last_simps drop_nonempty_simps