equal
deleted
inserted
replaced
12 imports Main Bits_Int |
12 imports Main Bits_Int |
13 begin |
13 begin |
14 |
14 |
15 definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" |
15 definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" |
16 where |
16 where |
17 "map2 f as bs = map (split f) (zip as bs)" |
17 "map2 f as bs = map (case_prod f) (zip as bs)" |
18 |
18 |
19 lemma map2_Nil [simp, code]: |
19 lemma map2_Nil [simp, code]: |
20 "map2 f [] ys = []" |
20 "map2 f [] ys = []" |
21 unfolding map2_def by auto |
21 unfolding map2_def by auto |
22 |
22 |