# 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 (\) (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 (\x y. x \ 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 (\) (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 \Simultaneous map\ - -definition map2 :: "('a \ 'b \ 'c) \ 'a list \ 'b list \ '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 \Auxiliary: Range projection\ definition bl_of_nth :: "nat \ (nat \ 'a) \ '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 (\) (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 (\) (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 (\) (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 \ 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 \ 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 (\) \ (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