--- 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
--- 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"
--- 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
--- 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