avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
authorhaftmann
Fri Jul 09 10:08:10 2010 +0200 (2010-07-09)
changeset 3775659caa6180fff
parent 37755 7086b7feaaa5
child 37757 dc78d2d9e90a
child 37758 bf86a65403a8
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
src/HOL/Imperative_HOL/Array.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Imperative_HOL/Relational.thy
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Fri Jul 09 09:48:54 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Fri Jul 09 10:08:10 2010 +0200
     1.3 @@ -201,7 +201,7 @@
     1.4  
     1.5  lemma upd_return:
     1.6    "upd i x a \<guillemotright> return a = upd i x a"
     1.7 -  by (rule Heap_eqI) (simp add: bindM_def guard_def upd_def)
     1.8 +  by (rule Heap_eqI) (simp add: bind_def guard_def upd_def)
     1.9  
    1.10  lemma array_make:
    1.11    "new n x = make n (\<lambda>_. x)"
    1.12 @@ -265,7 +265,7 @@
    1.13       x \<leftarrow> nth a i;
    1.14       upd i (f x) a
    1.15     done)"
    1.16 -  by (rule Heap_eqI) (simp add: bindM_def guard_def map_entry_def)
    1.17 +  by (rule Heap_eqI) (simp add: bind_def guard_def map_entry_def)
    1.18  
    1.19  lemma [code]:
    1.20    "swap i x a = (do
    1.21 @@ -273,12 +273,12 @@
    1.22       upd i x a;
    1.23       return y
    1.24     done)"
    1.25 -  by (rule Heap_eqI) (simp add: bindM_def guard_def swap_def)
    1.26 +  by (rule Heap_eqI) (simp add: bind_def guard_def swap_def)
    1.27  
    1.28  lemma [code]:
    1.29    "freeze a = (do
    1.30       n \<leftarrow> len a;
    1.31 -     mapM (\<lambda>i. nth a i) [0..<n]
    1.32 +     Heap_Monad.fold_map (\<lambda>i. nth a i) [0..<n]
    1.33     done)"
    1.34  proof (rule Heap_eqI)
    1.35    fix h
    1.36 @@ -288,20 +288,20 @@
    1.37       [0..<length a h] =
    1.38         List.map (List.nth (get_array a h)) [0..<length a h]"
    1.39      by simp
    1.40 -  have "Heap_Monad.execute (mapM (Array.nth a) [0..<length a h]) h =
    1.41 +  have "Heap_Monad.execute (Heap_Monad.fold_map (Array.nth a) [0..<length a h]) h =
    1.42      Some (get_array a h, h)"
    1.43 -    apply (subst execute_mapM_unchanged_heap)
    1.44 +    apply (subst execute_fold_map_unchanged_heap)
    1.45      apply (simp_all add: nth_def guard_def *)
    1.46      apply (simp add: length_def map_nth)
    1.47      done
    1.48    then have "Heap_Monad.execute (do
    1.49        n \<leftarrow> len a;
    1.50 -      mapM (Array.nth a) [0..<n]
    1.51 +      Heap_Monad.fold_map (Array.nth a) [0..<n]
    1.52      done) h = Some (get_array a h, h)"
    1.53      by (auto intro: execute_eq_SomeI)
    1.54    then show "Heap_Monad.execute (freeze a) h = Heap_Monad.execute (do
    1.55        n \<leftarrow> len a;
    1.56 -      mapM (Array.nth a) [0..<n]
    1.57 +      Heap_Monad.fold_map (Array.nth a) [0..<n]
    1.58      done) h" by simp
    1.59  qed
    1.60  
     2.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 09 09:48:54 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 09 10:08:10 2010 +0200
     2.3 @@ -66,36 +66,36 @@
     2.4    "execute (raise s) = (\<lambda>_. None)"
     2.5    by (simp add: raise_def)
     2.6  
     2.7 -definition bindM :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where (*FIXME just bind*)
     2.8 +definition bind :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where
     2.9    [code del]: "f >>= g = Heap (\<lambda>h. case execute f h of
    2.10                    Some (x, h') \<Rightarrow> execute (g x) h'
    2.11                  | None \<Rightarrow> None)"
    2.12  
    2.13 -notation bindM (infixl "\<guillemotright>=" 54)
    2.14 +notation bind (infixl "\<guillemotright>=" 54)
    2.15  
    2.16  lemma execute_bind [simp]:
    2.17    "execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'"
    2.18    "execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None"
    2.19 -  by (simp_all add: bindM_def)
    2.20 +  by (simp_all add: bind_def)
    2.21  
    2.22  lemma execute_bind_heap [simp]:
    2.23    "execute (heap f \<guillemotright>= g) h = execute (g (fst (f h))) (snd (f h))"
    2.24 -  by (simp add: bindM_def split_def)
    2.25 +  by (simp add: bind_def split_def)
    2.26    
    2.27  lemma execute_eq_SomeI:
    2.28    assumes "Heap_Monad.execute f h = Some (x, h')"
    2.29      and "Heap_Monad.execute (g x) h' = Some (y, h'')"
    2.30    shows "Heap_Monad.execute (f \<guillemotright>= g) h = Some (y, h'')"
    2.31 -  using assms by (simp add: bindM_def)
    2.32 +  using assms by (simp add: bind_def)
    2.33  
    2.34  lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
    2.35    by (rule Heap_eqI) simp
    2.36  
    2.37  lemma bind_return [simp]: "f \<guillemotright>= return = f"
    2.38 -  by (rule Heap_eqI) (simp add: bindM_def split: option.splits)
    2.39 +  by (rule Heap_eqI) (simp add: bind_def split: option.splits)
    2.40  
    2.41  lemma bind_bind [simp]: "(f \<guillemotright>= g) \<guillemotright>= k = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= k)"
    2.42 -  by (rule Heap_eqI) (simp add: bindM_def split: option.splits)
    2.43 +  by (rule Heap_eqI) (simp add: bind_def split: option.splits)
    2.44  
    2.45  lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
    2.46    by (rule Heap_eqI) simp
    2.47 @@ -149,7 +149,7 @@
    2.48          let
    2.49            val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
    2.50          in (Free (v, dummyT), t) end;
    2.51 -  fun unfold_monad (Const (@{const_syntax bindM}, _) $ f $ g) =
    2.52 +  fun unfold_monad (Const (@{const_syntax bind}, _) $ f $ g) =
    2.53          let
    2.54            val (v, g') = dest_abs_eta g;
    2.55            val vs = fold_aterms (fn Free (v, _) => insert (op =) v | _ => I) v [];
    2.56 @@ -169,19 +169,19 @@
    2.57      | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
    2.58          Const (@{const_syntax return}, dummyT) $ f
    2.59      | unfold_monad f = f;
    2.60 -  fun contains_bind (Const (@{const_syntax bindM}, _) $ _ $ _) = true
    2.61 +  fun contains_bind (Const (@{const_syntax bind}, _) $ _ $ _) = true
    2.62      | contains_bind (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
    2.63          contains_bind t;
    2.64 -  fun bindM_monad_tr' (f::g::ts) = list_comb
    2.65 +  fun bind_monad_tr' (f::g::ts) = list_comb
    2.66      (Const (@{syntax_const "_do"}, dummyT) $
    2.67 -      unfold_monad (Const (@{const_syntax bindM}, dummyT) $ f $ g), ts);
    2.68 +      unfold_monad (Const (@{const_syntax bind}, dummyT) $ f $ g), ts);
    2.69    fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) =
    2.70      if contains_bind g' then list_comb
    2.71        (Const (@{syntax_const "_do"}, dummyT) $
    2.72          unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
    2.73      else raise Match;
    2.74  in
    2.75 - [(@{const_syntax bindM}, bindM_monad_tr'),
    2.76 + [(@{const_syntax bind}, bind_monad_tr'),
    2.77    (@{const_syntax Let}, Let_monad_tr')]
    2.78  end;
    2.79  *}
    2.80 @@ -216,21 +216,21 @@
    2.81    "(f \<guillemotright>= lift g) = (f \<guillemotright>= (\<lambda>x. return (g x)))"
    2.82    by (simp add: lift_def comp_def)
    2.83  
    2.84 -primrec mapM :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where (*FIXME just map?*)
    2.85 -  "mapM f [] = return []"
    2.86 -| "mapM f (x # xs) = do
    2.87 +primrec fold_map :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where
    2.88 +  "fold_map f [] = return []"
    2.89 +| "fold_map f (x # xs) = do
    2.90       y \<leftarrow> f x;
    2.91 -     ys \<leftarrow> mapM f xs;
    2.92 +     ys \<leftarrow> fold_map f xs;
    2.93       return (y # ys)
    2.94     done"
    2.95  
    2.96 -lemma mapM_append:
    2.97 -  "mapM f (xs @ ys) = mapM f xs \<guillemotright>= (\<lambda>xs. mapM f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
    2.98 +lemma fold_map_append:
    2.99 +  "fold_map f (xs @ ys) = fold_map f xs \<guillemotright>= (\<lambda>xs. fold_map f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
   2.100    by (induct xs) simp_all
   2.101  
   2.102 -lemma execute_mapM_unchanged_heap:
   2.103 +lemma execute_fold_map_unchanged_heap:
   2.104    assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<exists>y. execute (f x) h = Some (y, h)"
   2.105 -  shows "execute (mapM f xs) h =
   2.106 +  shows "execute (fold_map f xs) h =
   2.107      Some (List.map (\<lambda>x. fst (the (execute (f x) h))) xs, h)"
   2.108  using assms proof (induct xs)
   2.109    case Nil show ?case by simp
   2.110 @@ -238,7 +238,7 @@
   2.111    case (Cons x xs)
   2.112    from Cons.prems obtain y
   2.113      where y: "execute (f x) h = Some (y, h)" by auto
   2.114 -  moreover from Cons.prems Cons.hyps have "execute (mapM f xs) h =
   2.115 +  moreover from Cons.prems Cons.hyps have "execute (fold_map f xs) h =
   2.116      Some (map (\<lambda>x. fst (the (execute (f x) h))) xs, h)" by auto
   2.117    ultimately show ?case by (simp, simp only: execute_bind(1), simp)
   2.118  qed
   2.119 @@ -314,7 +314,7 @@
   2.120                     g x s z
   2.121                  done) done)"
   2.122    unfolding MREC_def
   2.123 -  unfolding bindM_def return_def
   2.124 +  unfolding bind_def return_def
   2.125    apply simp
   2.126    apply (rule ext)
   2.127    apply (unfold mrec_rule[of x])
   2.128 @@ -426,7 +426,7 @@
   2.129      fun is_const c = case lookup_const naming c
   2.130       of SOME c' => (fn c'' => c' = c'')
   2.131        | NONE => K false;
   2.132 -    val is_bind = is_const @{const_name bindM};
   2.133 +    val is_bind = is_const @{const_name bind};
   2.134      val is_return = is_const @{const_name return};
   2.135      val dummy_name = "";
   2.136      val dummy_type = ITyVar dummy_name;
   2.137 @@ -527,6 +527,6 @@
   2.138  code_const return (Haskell "return")
   2.139  code_const Heap_Monad.raise' (Haskell "error/ _")
   2.140  
   2.141 -hide_const (open) Heap heap guard execute raise'
   2.142 +hide_const (open) Heap heap guard execute raise' fold_map
   2.143  
   2.144  end
     3.1 --- a/src/HOL/Imperative_HOL/Relational.thy	Fri Jul 09 09:48:54 2010 +0200
     3.2 +++ b/src/HOL/Imperative_HOL/Relational.thy	Fri Jul 09 10:08:10 2010 +0200
     3.3 @@ -39,7 +39,7 @@
     3.4  lemma crelE[consumes 1]:
     3.5    assumes "crel (f >>= g) h h'' r'"
     3.6    obtains h' r where "crel f h h' r" "crel (g r) h' h'' r'"
     3.7 -  using assms by (auto simp add: crel_def bindM_def split: option.split_asm)
     3.8 +  using assms by (auto simp add: crel_def bind_def split: option.split_asm)
     3.9  
    3.10  lemma crelE'[consumes 1]:
    3.11    assumes "crel (f >> g) h h'' r'"
    3.12 @@ -73,10 +73,10 @@
    3.13    using assms
    3.14    unfolding crel_def by auto
    3.15  
    3.16 -lemma crel_mapM:
    3.17 -  assumes "crel (mapM f xs) h h' r"
    3.18 +lemma crel_fold_map:
    3.19 +  assumes "crel (Heap_Monad.fold_map f xs) h h' r"
    3.20    assumes "\<And>h h'. P f [] h h' []"
    3.21 -  assumes "\<And>h h1 h' x xs y ys. \<lbrakk> crel (f x) h h1 y; crel (mapM f xs) h1 h' ys; P f xs h1 h' ys \<rbrakk> \<Longrightarrow> P f (x#xs) h h' (y#ys)"
    3.22 +  assumes "\<And>h h1 h' x xs y ys. \<lbrakk> crel (f x) h h1 y; crel (Heap_Monad.fold_map f xs) h1 h' ys; P f xs h1 h' ys \<rbrakk> \<Longrightarrow> P f (x#xs) h h' (y#ys)"
    3.23    shows "P f xs h h' r"
    3.24  using assms(1)
    3.25  proof (induct xs arbitrary: h h' r)
    3.26 @@ -85,11 +85,11 @@
    3.27  next
    3.28    case (Cons x xs)
    3.29    from Cons(2) obtain h1 y ys where crel_f: "crel (f x) h h1 y"
    3.30 -    and crel_mapM: "crel (mapM f xs) h1 h' ys"
    3.31 +    and crel_fold_map: "crel (Heap_Monad.fold_map f xs) h1 h' ys"
    3.32      and r_def: "r = y#ys"
    3.33 -    unfolding mapM.simps
    3.34 +    unfolding fold_map.simps
    3.35      by (auto elim!: crelE crel_return)
    3.36 -  from Cons(1)[OF crel_mapM] crel_mapM crel_f assms(3) r_def
    3.37 +  from Cons(1)[OF crel_fold_map] crel_fold_map crel_f assms(3) r_def
    3.38    show ?case by auto
    3.39  qed
    3.40  
    3.41 @@ -156,9 +156,9 @@
    3.42    with l show ?thesis by (simp add: upt_conv_Cons)
    3.43  qed
    3.44  
    3.45 -lemma crel_mapM_nth:
    3.46 +lemma crel_fold_map_nth:
    3.47    assumes
    3.48 -  "crel (mapM (Array.nth a) [Array.length a h - n..<Array.length a h]) h h' xs"
    3.49 +  "crel (Heap_Monad.fold_map (Array.nth a) [Array.length a h - n..<Array.length a h]) h h' xs"
    3.50    assumes "n \<le> Array.length a h"
    3.51    shows "h = h' \<and> xs = drop (Array.length a h - n) (get_array a h)"
    3.52  using assms
    3.53 @@ -170,12 +170,12 @@
    3.54    from Suc(3) have "[Array.length a h - Suc n..<Array.length a h] = (Array.length a h - Suc n)#[Array.length a h - n..<Array.length a h]"
    3.55      by (simp add: upt_conv_Cons')
    3.56    with Suc(2) obtain r where
    3.57 -    crel_mapM: "crel (mapM (Array.nth a) [Array.length a h - n..<Array.length a h]) h h' r"
    3.58 +    crel_fold_map: "crel (Heap_Monad.fold_map (Array.nth a) [Array.length a h - n..<Array.length a h]) h h' r"
    3.59      and xs_def: "xs = get_array a h ! (Array.length a h - Suc n) # r"
    3.60      by (auto elim!: crelE crel_nth crel_return)
    3.61    from Suc(3) have "Array.length a h - n = Suc (Array.length a h - Suc n)" 
    3.62      by arith
    3.63 -  with Suc.hyps[OF crel_mapM] xs_def show ?case
    3.64 +  with Suc.hyps[OF crel_fold_map] xs_def show ?case
    3.65      unfolding Array.length_def
    3.66      by (auto simp add: nth_drop')
    3.67  qed
    3.68 @@ -186,8 +186,8 @@
    3.69    using assms unfolding freeze_def
    3.70    by (elim crel_heap) simp
    3.71  
    3.72 -lemma crel_mapM_map_entry_remains:
    3.73 -  assumes "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
    3.74 +lemma crel_fold_map_map_entry_remains:
    3.75 +  assumes "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
    3.76    assumes "i < Array.length a h - n"
    3.77    shows "get_array a h ! i = get_array a h' ! i"
    3.78  using assms
    3.79 @@ -201,16 +201,16 @@
    3.80    from Suc(3) have "[Array.length a h - Suc n..<Array.length a h] = (Array.length a h - Suc n)#[Array.length a h - n..<Array.length a h]"
    3.81      by (simp add: upt_conv_Cons')
    3.82    from Suc(2) this obtain r where
    3.83 -    crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
    3.84 +    crel_fold_map: "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
    3.85      by (auto simp add: elim!: crelE crel_map_entry crel_return)
    3.86    have length_remains: "Array.length a ?h1 = Array.length a h" by simp
    3.87 -  from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a ?h1 - n..<Array.length a ?h1]) ?h1 h' r"
    3.88 +  from crel_fold_map have crel_fold_map': "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a ?h1 - n..<Array.length a ?h1]) ?h1 h' r"
    3.89      by simp
    3.90    from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
    3.91  qed
    3.92  
    3.93 -lemma crel_mapM_map_entry_changes:
    3.94 -  assumes "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
    3.95 +lemma crel_fold_map_map_entry_changes:
    3.96 +  assumes "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
    3.97    assumes "n \<le> Array.length a h"  
    3.98    assumes "i \<ge> Array.length a h - n"
    3.99    assumes "i < Array.length a h"
   3.100 @@ -226,22 +226,22 @@
   3.101    from Suc(3) have "[Array.length a h - Suc n..<Array.length a h] = (Array.length a h - Suc n)#[Array.length a h - n..<Array.length a h]"
   3.102      by (simp add: upt_conv_Cons')
   3.103    from Suc(2) this obtain r where
   3.104 -    crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
   3.105 +    crel_fold_map: "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
   3.106      by (auto simp add: elim!: crelE crel_map_entry crel_return)
   3.107    have length_remains: "Array.length a ?h1 = Array.length a h" by simp
   3.108    from Suc(3) have less: "Array.length a h - Suc n < Array.length a h - n" by arith
   3.109    from Suc(3) have less2: "Array.length a h - Suc n < Array.length a h" by arith
   3.110    from Suc(4) length_remains have cases: "i = Array.length a ?h1 - Suc n \<or> i \<ge> Array.length a ?h1 - n" by arith
   3.111 -  from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a ?h1 - n..<Array.length a ?h1]) ?h1 h' r"
   3.112 +  from crel_fold_map have crel_fold_map': "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a ?h1 - n..<Array.length a ?h1]) ?h1 h' r"
   3.113      by simp
   3.114    from Suc(1)[OF this] cases Suc(3) Suc(5) length_remains
   3.115 -    crel_mapM_map_entry_remains[OF this, of "Array.length a h - Suc n", symmetric] less less2
   3.116 +    crel_fold_map_map_entry_remains[OF this, of "Array.length a h - Suc n", symmetric] less less2
   3.117    show ?case
   3.118      by (auto simp add: nth_list_update_eq Array.length_def)
   3.119  qed
   3.120  
   3.121 -lemma crel_mapM_map_entry_length:
   3.122 -  assumes "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
   3.123 +lemma crel_fold_map_map_entry_length:
   3.124 +  assumes "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
   3.125    assumes "n \<le> Array.length a h"
   3.126    shows "Array.length a h' = Array.length a h"
   3.127  using assms
   3.128 @@ -254,21 +254,21 @@
   3.129    from Suc(3) have "[Array.length a h - Suc n..<Array.length a h] = (Array.length a h - Suc n)#[Array.length a h - n..<Array.length a h]"
   3.130      by (simp add: upt_conv_Cons')
   3.131    from Suc(2) this obtain r where 
   3.132 -    crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
   3.133 +    crel_fold_map: "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
   3.134      by (auto elim!: crelE crel_map_entry crel_return)
   3.135    have length_remains: "Array.length a ?h1 = Array.length a h" by simp
   3.136 -  from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a ?h1 - n..<Array.length a ?h1]) ?h1 h' r"
   3.137 +  from crel_fold_map have crel_fold_map': "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a ?h1 - n..<Array.length a ?h1]) ?h1 h' r"
   3.138      by simp
   3.139    from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
   3.140  qed
   3.141  
   3.142 -lemma crel_mapM_map_entry:
   3.143 -assumes "crel (mapM (\<lambda>n. map_entry n f a) [0..<Array.length a h]) h h' r"
   3.144 +lemma crel_fold_map_map_entry:
   3.145 +assumes "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [0..<Array.length a h]) h h' r"
   3.146    shows "get_array a h' = List.map f (get_array a h)"
   3.147  proof -
   3.148 -  from assms have "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - Array.length a h..<Array.length a h]) h h' r" by simp
   3.149 -  from crel_mapM_map_entry_length[OF this]
   3.150 -  crel_mapM_map_entry_changes[OF this] show ?thesis
   3.151 +  from assms have "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - Array.length a h..<Array.length a h]) h h' r" by simp
   3.152 +  from crel_fold_map_map_entry_length[OF this]
   3.153 +  crel_fold_map_map_entry_changes[OF this] show ?thesis
   3.154      unfolding Array.length_def
   3.155      by (auto intro: nth_equalityI)
   3.156  qed
   3.157 @@ -342,7 +342,7 @@
   3.158    by (elim crel_if crel_return crel_raise) auto
   3.159  
   3.160  lemma crel_assert_eq: "(\<And>h h' r. crel f h h' r \<Longrightarrow> P r) \<Longrightarrow> f \<guillemotright>= assert P = f"
   3.161 -unfolding crel_def bindM_def Let_def assert_def
   3.162 +unfolding crel_def bind_def Let_def assert_def
   3.163    raise_def return_def prod_case_beta
   3.164  apply (cases f)
   3.165  apply simp
   3.166 @@ -359,7 +359,7 @@
   3.167  lemma crelI:
   3.168    assumes "crel f h h' r" "crel (g r) h' h'' r'"
   3.169    shows "crel (f >>= g) h h'' r'"
   3.170 -  using assms by (simp add: crel_def' bindM_def)
   3.171 +  using assms by (simp add: crel_def' bind_def)
   3.172  
   3.173  lemma crelI':
   3.174    assumes "crel f h h' r" "crel g h' h'' r'"
   3.175 @@ -513,19 +513,19 @@
   3.176    assumes "\<And>h' r. crel f h h' r \<Longrightarrow> noError (g r) h'"
   3.177    shows "noError (f \<guillemotright>= g) h"
   3.178    using assms
   3.179 -  by (auto simp add: noError_def' crel_def' bindM_def)
   3.180 +  by (auto simp add: noError_def' crel_def' bind_def)
   3.181  
   3.182  lemma noErrorI':
   3.183    assumes "noError f h"
   3.184    assumes "\<And>h' r. crel f h h' r \<Longrightarrow> noError g h'"
   3.185    shows "noError (f \<guillemotright> g) h"
   3.186    using assms
   3.187 -  by (auto simp add: noError_def' crel_def' bindM_def)
   3.188 +  by (auto simp add: noError_def' crel_def' bind_def)
   3.189  
   3.190  lemma noErrorI2:
   3.191  "\<lbrakk>crel f h h' r ; noError f h; noError (g r) h'\<rbrakk>
   3.192  \<Longrightarrow> noError (f \<guillemotright>= g) h"
   3.193 -by (auto simp add: noError_def' crel_def' bindM_def)
   3.194 +by (auto simp add: noError_def' crel_def' bind_def)
   3.195  
   3.196  lemma noError_return: 
   3.197    shows "noError (return x) h"
   3.198 @@ -546,18 +546,18 @@
   3.199  using assms
   3.200  by (auto split: option.split)
   3.201  
   3.202 -lemma noError_mapM: 
   3.203 +lemma noError_fold_map: 
   3.204  assumes "\<forall>x \<in> set xs. noError (f x) h \<and> crel (f x) h h (r x)" 
   3.205 -shows "noError (mapM f xs) h"
   3.206 +shows "noError (Heap_Monad.fold_map f xs) h"
   3.207  using assms
   3.208  proof (induct xs)
   3.209    case Nil
   3.210    thus ?case
   3.211 -    unfolding mapM.simps by (intro noError_return)
   3.212 +    unfolding fold_map.simps by (intro noError_return)
   3.213  next
   3.214    case (Cons x xs)
   3.215    thus ?case
   3.216 -    unfolding mapM.simps
   3.217 +    unfolding fold_map.simps
   3.218      by (auto intro: noErrorI2[of "f x"] noErrorI noError_return)
   3.219  qed
   3.220  
   3.221 @@ -611,9 +611,9 @@
   3.222    "noError (freeze a) h"
   3.223    by (simp add: freeze_def)
   3.224  
   3.225 -lemma noError_mapM_map_entry:
   3.226 +lemma noError_fold_map_map_entry:
   3.227    assumes "n \<le> Array.length a h"
   3.228 -  shows "noError (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h"
   3.229 +  shows "noError (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h"
   3.230  using assms
   3.231  proof (induct n arbitrary: h)
   3.232    case 0