src/HOL/Library/State_Monad.thy
changeset 21418 4bc2882f80af
parent 21404 eb85850d3eb7
child 21601 6588b947d631
     1.1 --- a/src/HOL/Library/State_Monad.thy	Sat Nov 18 00:20:26 2006 +0100
     1.2 +++ b/src/HOL/Library/State_Monad.thy	Sat Nov 18 00:20:27 2006 +0100
     1.3 @@ -144,7 +144,6 @@
     1.4    "\<And>f. run f = f \<longleftrightarrow> True"
     1.5    unfolding run_def by rule+
     1.6  
     1.7 -
     1.8  subsection {* Monad laws *}
     1.9  
    1.10  text {*
    1.11 @@ -161,6 +160,14 @@
    1.12    unfolding mbind_def by (simp add: expand_fun_eq split_Pair)
    1.13  
    1.14  lemma
    1.15 +  id_fcomp [simp]: "id \<guillemotright> f = f"
    1.16 +  unfolding fcomp_def by simp
    1.17 +
    1.18 +lemma
    1.19 +  fcomp_id [simp]: "f \<guillemotright> id = f"
    1.20 +  unfolding fcomp_def by simp
    1.21 +
    1.22 +lemma
    1.23    mbind_mbind [simp]: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)"
    1.24    unfolding mbind_def by (simp add: split_def expand_fun_eq)
    1.25  
    1.26 @@ -176,7 +183,7 @@
    1.27    fcomp_fcomp [simp]: "(f \<guillemotright> g) \<guillemotright> h = f \<guillemotright> (g \<guillemotright> h)"
    1.28    unfolding fcomp_def o_assoc ..
    1.29  
    1.30 -lemmas monad_simp = run_simp return_mbind mbind_return
    1.31 +lemmas monad_simp = run_simp return_mbind mbind_return id_fcomp fcomp_id
    1.32    mbind_mbind mbind_fcomp fcomp_mbind fcomp_fcomp
    1.33  
    1.34  text {*
    1.35 @@ -246,6 +253,61 @@
    1.36  ] end;
    1.37  *}
    1.38  
    1.39 +subsection {* Combinators *}
    1.40 +
    1.41 +definition
    1.42 +  lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> 'b \<times> 'c"
    1.43 +  "lift f x = return (f x)"
    1.44 +
    1.45 +fun
    1.46 +  list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
    1.47 +  "list f [] = id"
    1.48 +  "list f (x#xs) = (do f x; list f xs done)"
    1.49 +lemmas [code] = list.simps
    1.50 +
    1.51 +fun list_yield :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<times> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'c list \<times> 'b" where
    1.52 +  "list_yield f [] = return []"
    1.53 +  "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"
    1.54 +lemmas [code] = list_yield.simps
    1.55 +  
    1.56 +text {* combinator properties *}
    1.57 +
    1.58 +lemma list_append [simp]:
    1.59 +  "list f (xs @ ys) = list f xs \<guillemotright> list f ys"
    1.60 +  by (induct xs) (simp_all del: id_apply) (*FIXME*)
    1.61 +
    1.62 +lemma list_cong [fundef_cong, recdef_cong]:
    1.63 +  "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
    1.64 +    \<Longrightarrow> list f xs = list g ys"
    1.65 +proof (induct f xs arbitrary: g ys rule: list.induct)
    1.66 +  case 1 then show ?case by simp
    1.67 +next
    1.68 +  case (2 f x xs g)
    1.69 +  from 2 have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
    1.70 +  then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto
    1.71 +  with 2 have "list f xs = list g xs" by auto
    1.72 +  with 2 have "list f (x # xs) = list g (x # xs)" by auto
    1.73 +  with 2 show "list f (x # xs) = list g ys" by auto
    1.74 +qed
    1.75 +
    1.76 +lemma list_yield_cong [fundef_cong, recdef_cong]:
    1.77 +  "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
    1.78 +    \<Longrightarrow> list_yield f xs = list_yield g ys"
    1.79 +proof (induct f xs arbitrary: g ys rule: list_yield.induct)
    1.80 +  case 1 then show ?case by simp
    1.81 +next
    1.82 +  case (2 f x xs g)
    1.83 +  from 2 have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
    1.84 +  then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto
    1.85 +  with 2 have "list_yield f xs = list_yield g xs" by auto
    1.86 +  with 2 have "list_yield f (x # xs) = list_yield g (x # xs)" by auto
    1.87 +  with 2 show "list_yield f (x # xs) = list_yield g ys" by auto
    1.88 +qed
    1.89 +
    1.90 +text {*
    1.91 +  still waiting for extensions@{text "\<dots>"}
    1.92 +*}
    1.93 +
    1.94  text {*
    1.95    For an example, see HOL/ex/CodeRandom.thy (more examples coming soon).
    1.96  *}