monadic bind
authorhaftmann
Fri Oct 14 22:42:56 2011 +0200 (2011-10-14)
changeset 45145d5086da3c32d
parent 45142 97e81a8aa277
child 45146 5465824c1c8d
monadic bind
src/HOL/Library/Monad_Syntax.thy
src/HOL/Library/More_List.thy
     1.1 --- a/src/HOL/Library/Monad_Syntax.thy	Fri Oct 14 11:34:30 2011 +0200
     1.2 +++ b/src/HOL/Library/Monad_Syntax.thy	Fri Oct 14 22:42:56 2011 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Monad notation for arbitrary types *}
     1.5  
     1.6  theory Monad_Syntax
     1.7 -imports Main "~~/src/Tools/Adhoc_Overloading"
     1.8 +imports Main "~~/src/Tools/Adhoc_Overloading" "~~/src/HOL/Library/More_List"
     1.9  begin
    1.10  
    1.11  text {*
    1.12 @@ -73,6 +73,7 @@
    1.13    Adhoc_Overloading.add_overloaded @{const_name bind}
    1.14    #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Predicate.bind}
    1.15    #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Option.bind}
    1.16 +  #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name More_List.bind}
    1.17  *}
    1.18  
    1.19  end
     2.1 --- a/src/HOL/Library/More_List.thy	Fri Oct 14 11:34:30 2011 +0200
     2.2 +++ b/src/HOL/Library/More_List.thy	Fri Oct 14 22:42:56 2011 +0200
     2.3 @@ -17,6 +17,7 @@
     2.4  declare (in complete_lattice) Inf_set_fold [code_unfold del]
     2.5  declare (in complete_lattice) Sup_set_fold [code_unfold del]
     2.6  
     2.7 +
     2.8  text {* Fold combinator with canonical argument order *}
     2.9  
    2.10  primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
    2.11 @@ -156,6 +157,7 @@
    2.12    "sort xs = fold insort xs []"
    2.13    by (rule sort_key_conv_fold) simp
    2.14  
    2.15 +
    2.16  text {* @{const Finite_Set.fold} and @{const fold} *}
    2.17  
    2.18  lemma (in comp_fun_commute) fold_set_remdups:
    2.19 @@ -268,6 +270,7 @@
    2.20    "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
    2.21    unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map ..
    2.22  
    2.23 +
    2.24  text {* @{text nth_map} *}
    2.25  
    2.26  definition nth_map :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    2.27 @@ -295,4 +298,15 @@
    2.28    "nth_map (Suc n) f (x # xs) = x # nth_map n f xs"
    2.29    by (simp add: nth_map_def)
    2.30  
    2.31 +
    2.32 +text {* monad operation *}
    2.33 +
    2.34 +definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
    2.35 +  "bind xs f = concat (map f xs)"
    2.36 +
    2.37 +lemma bind_simps [simp]:
    2.38 +  "bind [] f = []"
    2.39 +  "bind (x # xs) f = f x @ bind xs f"
    2.40 +  by (simp_all add: bind_def)
    2.41 +
    2.42  end