src/HOL/Library/More_List.thy
 changeset 45145 d5086da3c32d parent 44928 7ef6505bde7f child 45146 5465824c1c8d
```--- a/src/HOL/Library/More_List.thy	Fri Oct 14 11:34:30 2011 +0200
+++ b/src/HOL/Library/More_List.thy	Fri Oct 14 22:42:56 2011 +0200
@@ -17,6 +17,7 @@
declare (in complete_lattice) Inf_set_fold [code_unfold del]
declare (in complete_lattice) Sup_set_fold [code_unfold del]

+
text {* Fold combinator with canonical argument order *}

primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
@@ -156,6 +157,7 @@
"sort xs = fold insort xs []"
by (rule sort_key_conv_fold) simp

+
text {* @{const Finite_Set.fold} and @{const fold} *}

lemma (in comp_fun_commute) fold_set_remdups:
@@ -268,6 +270,7 @@
"SUPR (set xs) f = fold (sup \<circ> f) xs bot"
unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map ..

+
text {* @{text nth_map} *}

definition nth_map :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
@@ -295,4 +298,15 @@
"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```