src/HOL/Library/More_List.thy
changeset 45145 d5086da3c32d
parent 44928 7ef6505bde7f
child 45146 5465824c1c8d
     1.1 --- a/src/HOL/Library/More_List.thy	Fri Oct 14 11:34:30 2011 +0200
     1.2 +++ b/src/HOL/Library/More_List.thy	Fri Oct 14 22:42:56 2011 +0200
     1.3 @@ -17,6 +17,7 @@
     1.4  declare (in complete_lattice) Inf_set_fold [code_unfold del]
     1.5  declare (in complete_lattice) Sup_set_fold [code_unfold del]
     1.6  
     1.7 +
     1.8  text {* Fold combinator with canonical argument order *}
     1.9  
    1.10  primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
    1.11 @@ -156,6 +157,7 @@
    1.12    "sort xs = fold insort xs []"
    1.13    by (rule sort_key_conv_fold) simp
    1.14  
    1.15 +
    1.16  text {* @{const Finite_Set.fold} and @{const fold} *}
    1.17  
    1.18  lemma (in comp_fun_commute) fold_set_remdups:
    1.19 @@ -268,6 +270,7 @@
    1.20    "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
    1.21    unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map ..
    1.22  
    1.23 +
    1.24  text {* @{text nth_map} *}
    1.25  
    1.26  definition nth_map :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    1.27 @@ -295,4 +298,15 @@
    1.28    "nth_map (Suc n) f (x # xs) = x # nth_map n f xs"
    1.29    by (simp add: nth_map_def)
    1.30  
    1.31 +
    1.32 +text {* monad operation *}
    1.33 +
    1.34 +definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
    1.35 +  "bind xs f = concat (map f xs)"
    1.36 +
    1.37 +lemma bind_simps [simp]:
    1.38 +  "bind [] f = []"
    1.39 +  "bind (x # xs) f = f x @ bind xs f"
    1.40 +  by (simp_all add: bind_def)
    1.41 +
    1.42  end