introduced zip_with
authornipkow
Tue Sep 12 20:40:46 2017 +0200 (21 months ago)
changeset 66655e9be3d6995f9
parent 66654 4a812abde314
child 66656 8f4d252ce2fe
introduced zip_with
src/HOL/Library/Stirling.thy
src/HOL/List.thy
     1.1 --- a/src/HOL/Library/Stirling.thy	Tue Sep 12 12:14:38 2017 +0200
     1.2 +++ b/src/HOL/Library/Stirling.thy	Tue Sep 12 20:40:46 2017 +0200
     1.3 @@ -246,7 +246,7 @@
     1.4  \<close>
     1.5  
     1.6  definition zip_with_prev :: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'b list"
     1.7 -  where "zip_with_prev f x xs = map (\<lambda>(x,y). f x y) (zip (x # xs) xs)"
     1.8 +  where "zip_with_prev f x xs = zip_with f (x # xs) xs"
     1.9  
    1.10  lemma zip_with_prev_altdef:
    1.11    "zip_with_prev f x xs =
     2.1 --- a/src/HOL/List.thy	Tue Sep 12 12:14:38 2017 +0200
     2.2 +++ b/src/HOL/List.thy	Tue Sep 12 20:40:46 2017 +0200
     2.3 @@ -151,6 +151,9 @@
     2.4    \<comment> \<open>Warning: simpset does not contain this definition, but separate
     2.5         theorems for \<open>xs = []\<close> and \<open>xs = z # zs\<close>\<close>
     2.6  
     2.7 +abbreviation zip_with :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where
     2.8 +"zip_with f xs ys \<equiv> map (\<lambda>(x,y). f x y) (zip xs ys)"
     2.9 +
    2.10  primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
    2.11  "product [] _ = []" |
    2.12  "product (x#xs) ys = map (Pair x) ys @ product xs ys"