1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 09 09:48:54 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 09 10:08:10 2010 +0200
     1.3 @@ -66,36 +66,36 @@
     1.4    "execute (raise s) = (\<lambda>_. None)"
     1.5    by (simp add: raise_def)
     1.6  
     1.7 -definition bindM :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where (*FIXME just bind*)
     1.8 +definition bind :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where
     1.9    [code del]: "f >>= g = Heap (\<lambda>h. case execute f h of
    1.10                    Some (x, h') \<Rightarrow> execute (g x) h'
    1.11                  | None \<Rightarrow> None)"
    1.12  
    1.13 -notation bindM (infixl "\<guillemotright>=" 54)
    1.14 +notation bind (infixl "\<guillemotright>=" 54)
    1.15  
    1.16  lemma execute_bind [simp]:
    1.17    "execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'"
    1.18    "execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None"
    1.19 -  by (simp_all add: bindM_def)
    1.20 +  by (simp_all add: bind_def)
    1.21  
    1.22  lemma execute_bind_heap [simp]:
    1.23    "execute (heap f \<guillemotright>= g) h = execute (g (fst (f h))) (snd (f h))"
    1.24 -  by (simp add: bindM_def split_def)
    1.25 +  by (simp add: bind_def split_def)
    1.26    
    1.27  lemma execute_eq_SomeI:
    1.28    assumes "Heap_Monad.execute f h = Some (x, h')"
    1.29      and "Heap_Monad.execute (g x) h' = Some (y, h'')"
    1.30    shows "Heap_Monad.execute (f \<guillemotright>= g) h = Some (y, h'')"
    1.31 -  using assms by (simp add: bindM_def)
    1.32 +  using assms by (simp add: bind_def)
    1.33  
    1.34  lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
    1.35    by (rule Heap_eqI) simp
    1.36  
    1.37  lemma bind_return [simp]: "f \<guillemotright>= return = f"
    1.38 -  by (rule Heap_eqI) (simp add: bindM_def split: option.splits)
    1.39 +  by (rule Heap_eqI) (simp add: bind_def split: option.splits)
    1.40  
    1.41  lemma bind_bind [simp]: "(f \<guillemotright>= g) \<guillemotright>= k = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= k)"
    1.42 -  by (rule Heap_eqI) (simp add: bindM_def split: option.splits)
    1.43 +  by (rule Heap_eqI) (simp add: bind_def split: option.splits)
    1.44  
    1.45  lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
    1.46    by (rule Heap_eqI) simp
    1.47 @@ -149,7 +149,7 @@
    1.48          let
    1.49            val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
    1.50          in (Free (v, dummyT), t) end;
    1.51 -  fun unfold_monad (Const (@{const_syntax bindM}, _) $ f $ g) =
    1.52 +  fun unfold_monad (Const (@{const_syntax bind}, _) $ f $ g) =
    1.53          let
    1.54            val (v, g') = dest_abs_eta g;
    1.55            val vs = fold_aterms (fn Free (v, _) => insert (op =) v | _ => I) v [];
    1.56 @@ -169,19 +169,19 @@
    1.57      | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
    1.58          Const (@{const_syntax return}, dummyT) $ f
    1.59      | unfold_monad f = f;
    1.60 -  fun contains_bind (Const (@{const_syntax bindM}, _) $ _ $ _) = true
    1.61 +  fun contains_bind (Const (@{const_syntax bind}, _) $ _ $ _) = true
    1.62      | contains_bind (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
    1.63          contains_bind t;
    1.64 -  fun bindM_monad_tr' (f::g::ts) = list_comb
    1.65 +  fun bind_monad_tr' (f::g::ts) = list_comb
    1.66      (Const (@{syntax_const "_do"}, dummyT) $
    1.67 -      unfold_monad (Const (@{const_syntax bindM}, dummyT) $ f $ g), ts);
    1.68 +      unfold_monad (Const (@{const_syntax bind}, dummyT) $ f $ g), ts);
    1.69    fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) =
    1.70      if contains_bind g' then list_comb
    1.71        (Const (@{syntax_const "_do"}, dummyT) $
    1.72          unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
    1.73      else raise Match;
    1.74  in
    1.75 - [(@{const_syntax bindM}, bindM_monad_tr'),
    1.76 + [(@{const_syntax bind}, bind_monad_tr'),
    1.77    (@{const_syntax Let}, Let_monad_tr')]
    1.78  end;
    1.79  *}
    1.80 @@ -216,21 +216,21 @@
    1.81    "(f \<guillemotright>= lift g) = (f \<guillemotright>= (\<lambda>x. return (g x)))"
    1.82    by (simp add: lift_def comp_def)
    1.83  
    1.84 -primrec mapM :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where (*FIXME just map?*)
    1.85 -  "mapM f [] = return []"
    1.86 -| "mapM f (x # xs) = do
    1.87 +primrec fold_map :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where
    1.88 +  "fold_map f [] = return []"
    1.89 +| "fold_map f (x # xs) = do
    1.90       y \<leftarrow> f x;
    1.91 -     ys \<leftarrow> mapM f xs;
    1.92 +     ys \<leftarrow> fold_map f xs;
    1.93       return (y # ys)
    1.94     done"
    1.95  
    1.96 -lemma mapM_append:
    1.97 -  "mapM f (xs @ ys) = mapM f xs \<guillemotright>= (\<lambda>xs. mapM f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
    1.98 +lemma fold_map_append:
    1.99 +  "fold_map f (xs @ ys) = fold_map f xs \<guillemotright>= (\<lambda>xs. fold_map f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
   1.100    by (induct xs) simp_all
   1.101  
   1.102 -lemma execute_mapM_unchanged_heap:
   1.103 +lemma execute_fold_map_unchanged_heap:
   1.104    assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<exists>y. execute (f x) h = Some (y, h)"
   1.105 -  shows "execute (mapM f xs) h =
   1.106 +  shows "execute (fold_map f xs) h =
   1.107      Some (List.map (\<lambda>x. fst (the (execute (f x) h))) xs, h)"
   1.108  using assms proof (induct xs)
   1.109    case Nil show ?case by simp
   1.110 @@ -238,7 +238,7 @@
   1.111    case (Cons x xs)
   1.112    from Cons.prems obtain y
   1.113      where y: "execute (f x) h = Some (y, h)" by auto
   1.114 -  moreover from Cons.prems Cons.hyps have "execute (mapM f xs) h =
   1.115 +  moreover from Cons.prems Cons.hyps have "execute (fold_map f xs) h =
   1.116      Some (map (\<lambda>x. fst (the (execute (f x) h))) xs, h)" by auto
   1.117    ultimately show ?case by (simp, simp only: execute_bind(1), simp)
   1.118  qed
   1.119 @@ -314,7 +314,7 @@
   1.120                     g x s z
   1.121                  done) done)"
   1.122    unfolding MREC_def
   1.123 -  unfolding bindM_def return_def
   1.124 +  unfolding bind_def return_def
   1.125    apply simp
   1.126    apply (rule ext)
   1.127    apply (unfold mrec_rule[of x])
   1.128 @@ -426,7 +426,7 @@
   1.129      fun is_const c = case lookup_const naming c
   1.130       of SOME c' => (fn c'' => c' = c'')
   1.131        | NONE => K false;
   1.132 -    val is_bind = is_const @{const_name bindM};
   1.133 +    val is_bind = is_const @{const_name bind};
   1.134      val is_return = is_const @{const_name return};
   1.135      val dummy_name = "";
   1.136      val dummy_type = ITyVar dummy_name;
   1.137 @@ -527,6 +527,6 @@
   1.138  code_const return (Haskell "return")
   1.139  code_const Heap_Monad.raise' (Haskell "error/ _")
   1.140  
   1.141 -hide_const (open) Heap heap guard execute raise'
   1.142 +hide_const (open) Heap heap guard execute raise' fold_map
   1.143  
   1.144  end