src/HOL/More_List.thy

incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)

(* Author:  Florian Haftmann, TU Muenchen *)

header {* Operations on lists beyond the standard List theory *}

theory More_List
imports List
begin

text {* @{text nth_map} *}

definition nth_map :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
  "nth_map n f xs = (if n < length xs then
       take n xs @ [f (xs ! n)] @ drop (Suc n) xs
     else xs)"

lemma nth_map_id:
  "n \<ge> length xs \<Longrightarrow> nth_map n f xs = xs"
  by (simp add: nth_map_def)

lemma nth_map_unfold:
  "n < length xs \<Longrightarrow> nth_map n f xs = take n xs @ [f (xs ! n)] @ drop (Suc n) xs"
  by (simp add: nth_map_def)

lemma nth_map_Nil [simp]:
  "nth_map n f [] = []"
  by (simp add: nth_map_def)

lemma nth_map_zero [simp]:
  "nth_map 0 f (x # xs) = f x # xs"
  by (simp add: nth_map_def)

lemma nth_map_Suc [simp]:
  "nth_map (Suc n) f (x # xs) = x # nth_map n f xs"
  by (simp add: nth_map_def)


text {* monad operation *}

definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
  "bind xs f = concat (map f xs)"

lemma bind_simps [simp]:
  "bind [] f = []"
  "bind (x # xs) f = f x @ bind xs f"
  by (simp_all add: bind_def)

end