added lemma; zip_with -> map2
authornipkow
Wed Sep 13 17:40:54 2017 +0200 (2017-09-13)
changeset 666568f4d252ce2fe
parent 66655 e9be3d6995f9
child 66657 6f82e2ad261a
added lemma; zip_with -> map2
src/HOL/Library/Stirling.thy
src/HOL/List.thy
     1.1 --- a/src/HOL/Library/Stirling.thy	Tue Sep 12 20:40:46 2017 +0200
     1.2 +++ b/src/HOL/Library/Stirling.thy	Wed Sep 13 17:40:54 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 = zip_with f (x # xs) xs"
     1.8 +  where "zip_with_prev f x xs = map2 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 20:40:46 2017 +0200
     2.2 +++ b/src/HOL/List.thy	Wed Sep 13 17:40:54 2017 +0200
     2.3 @@ -151,8 +151,8 @@
     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 +abbreviation map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where
    2.10 +"map2 f xs ys \<equiv> map (\<lambda>(x,y). f x y) (zip xs ys)"
    2.11  
    2.12  primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
    2.13  "product [] _ = []" |
    2.14 @@ -4396,12 +4396,12 @@
    2.15  done
    2.16  
    2.17  lemma nths_shift_lemma:
    2.18 -     "map fst [p<-zip xs [i..<i + length xs] . snd p : A] =
    2.19 -      map fst [p<-zip xs [0..<length xs] . snd p + i : A]"
    2.20 +  "map fst [p<-zip xs [i..<i + length xs] . snd p : A] =
    2.21 +   map fst [p<-zip xs [0..<length xs] . snd p + i : A]"
    2.22  by (induct xs rule: rev_induct) (simp_all add: add.commute)
    2.23  
    2.24  lemma nths_append:
    2.25 -     "nths (l @ l') A = nths l A @ nths l' {j. j + length l : A}"
    2.26 +  "nths (l @ l') A = nths l A @ nths l' {j. j + length l : A}"
    2.27  apply (unfold nths_def)
    2.28  apply (induct l' rule: rev_induct, simp)
    2.29  apply (simp add: upt_add_eq_append[of 0] nths_shift_lemma)
    2.30 @@ -4409,7 +4409,7 @@
    2.31  done
    2.32  
    2.33  lemma nths_Cons:
    2.34 -"nths (x # l) A = (if 0:A then [x] else []) @ nths l {j. Suc j : A}"
    2.35 +  "nths (x # l) A = (if 0:A then [x] else []) @ nths l {j. Suc j : A}"
    2.36  apply (induct l rule: rev_induct)
    2.37   apply (simp add: nths_def)
    2.38  apply (simp del: append_Cons add: append_Cons[symmetric] nths_append)
    2.39 @@ -4432,17 +4432,18 @@
    2.40  lemma nths_singleton [simp]: "nths [x] A = (if 0 : A then [x] else [])"
    2.41  by (simp add: nths_Cons)
    2.42  
    2.43 -
    2.44  lemma distinct_nthsI[simp]: "distinct xs \<Longrightarrow> distinct (nths xs I)"
    2.45 -  by (induct xs arbitrary: I) (auto simp: nths_Cons)
    2.46 -
    2.47 +by (induct xs arbitrary: I) (auto simp: nths_Cons)
    2.48  
    2.49  lemma nths_upt_eq_take [simp]: "nths l {..<n} = take n l"
    2.50 -  by (induct l rule: rev_induct)
    2.51 -     (simp_all split: nat_diff_split add: nths_append)
    2.52 +by (induct l rule: rev_induct)
    2.53 +   (simp_all split: nat_diff_split add: nths_append)
    2.54 +
    2.55 +lemma filter_eq_nths: "filter P xs = nths xs {i. i<length xs \<and> P(xs!i)}"
    2.56 +by(induction xs) (auto simp: nths_Cons)
    2.57  
    2.58  lemma filter_in_nths:
    2.59 - "distinct xs \<Longrightarrow> filter (%x. x \<in> set (nths xs s)) xs = nths xs s"
    2.60 +  "distinct xs \<Longrightarrow> filter (%x. x \<in> set (nths xs s)) xs = nths xs s"
    2.61  proof (induct xs arbitrary: s)
    2.62    case Nil thus ?case by simp
    2.63  next