avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)

--- a/src/HOL/Imperative_HOL/Array.thy	Fri Jul 09 09:48:54 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Fri Jul 09 10:08:10 2010 +0200
@@ -201,7 +201,7 @@
 
 lemma upd_return:
   "upd i x a \<guillemotright> return a = upd i x a"
-  by (rule Heap_eqI) (simp add: bindM_def guard_def upd_def)
+  by (rule Heap_eqI) (simp add: bind_def guard_def upd_def)
 
 lemma array_make:
   "new n x = make n (\<lambda>_. x)"
@@ -265,7 +265,7 @@
      x \<leftarrow> nth a i;
      upd i (f x) a
    done)"
-  by (rule Heap_eqI) (simp add: bindM_def guard_def map_entry_def)
+  by (rule Heap_eqI) (simp add: bind_def guard_def map_entry_def)
 
 lemma [code]:
   "swap i x a = (do
@@ -273,12 +273,12 @@
      upd i x a;
      return y
    done)"
-  by (rule Heap_eqI) (simp add: bindM_def guard_def swap_def)
+  by (rule Heap_eqI) (simp add: bind_def guard_def swap_def)
 
 lemma [code]:
   "freeze a = (do
      n \<leftarrow> len a;
-     mapM (\<lambda>i. nth a i) [0..<n]
+     Heap_Monad.fold_map (\<lambda>i. nth a i) [0..<n]
    done)"
 proof (rule Heap_eqI)
   fix h
@@ -288,20 +288,20 @@
      [0..<length a h] =
        List.map (List.nth (get_array a h)) [0..<length a h]"
     by simp
-  have "Heap_Monad.execute (mapM (Array.nth a) [0..<length a h]) h =
+  have "Heap_Monad.execute (Heap_Monad.fold_map (Array.nth a) [0..<length a h]) h =
     Some (get_array a h, h)"
-    apply (subst execute_mapM_unchanged_heap)
+    apply (subst execute_fold_map_unchanged_heap)
     apply (simp_all add: nth_def guard_def *)
     apply (simp add: length_def map_nth)
     done
   then have "Heap_Monad.execute (do
       n \<leftarrow> len a;
-      mapM (Array.nth a) [0..<n]
+      Heap_Monad.fold_map (Array.nth a) [0..<n]
     done) h = Some (get_array a h, h)"
     by (auto intro: execute_eq_SomeI)
   then show "Heap_Monad.execute (freeze a) h = Heap_Monad.execute (do
       n \<leftarrow> len a;
-      mapM (Array.nth a) [0..<n]
+      Heap_Monad.fold_map (Array.nth a) [0..<n]
     done) h" by simp
 qed
 

--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 09 09:48:54 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 09 10:08:10 2010 +0200
@@ -66,36 +66,36 @@
   "execute (raise s) = (\<lambda>_. None)"
   by (simp add: raise_def)
 
-definition bindM :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where (*FIXME just bind*)
+definition bind :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where
   [code del]: "f >>= g = Heap (\<lambda>h. case execute f h of
                   Some (x, h') \<Rightarrow> execute (g x) h'
                 | None \<Rightarrow> None)"
 
-notation bindM (infixl "\<guillemotright>=" 54)
+notation bind (infixl "\<guillemotright>=" 54)
 
 lemma execute_bind [simp]:
   "execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'"
   "execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None"
-  by (simp_all add: bindM_def)
+  by (simp_all add: bind_def)
 
 lemma execute_bind_heap [simp]:
   "execute (heap f \<guillemotright>= g) h = execute (g (fst (f h))) (snd (f h))"
-  by (simp add: bindM_def split_def)
+  by (simp add: bind_def split_def)
   
 lemma execute_eq_SomeI:
   assumes "Heap_Monad.execute f h = Some (x, h')"
     and "Heap_Monad.execute (g x) h' = Some (y, h'')"
   shows "Heap_Monad.execute (f \<guillemotright>= g) h = Some (y, h'')"
-  using assms by (simp add: bindM_def)
+  using assms by (simp add: bind_def)
 
 lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
   by (rule Heap_eqI) simp
 
 lemma bind_return [simp]: "f \<guillemotright>= return = f"
-  by (rule Heap_eqI) (simp add: bindM_def split: option.splits)
+  by (rule Heap_eqI) (simp add: bind_def split: option.splits)
 
 lemma bind_bind [simp]: "(f \<guillemotright>= g) \<guillemotright>= k = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= k)"
-  by (rule Heap_eqI) (simp add: bindM_def split: option.splits)
+  by (rule Heap_eqI) (simp add: bind_def split: option.splits)
 
 lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
   by (rule Heap_eqI) simp
@@ -149,7 +149,7 @@
         let
           val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
         in (Free (v, dummyT), t) end;
-  fun unfold_monad (Const (@{const_syntax bindM}, _) $ f $ g) =
+  fun unfold_monad (Const (@{const_syntax bind}, _) $ f $ g) =
         let
           val (v, g') = dest_abs_eta g;
           val vs = fold_aterms (fn Free (v, _) => insert (op =) v | _ => I) v [];
@@ -169,19 +169,19 @@
     | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
         Const (@{const_syntax return}, dummyT) $ f
     | unfold_monad f = f;
-  fun contains_bind (Const (@{const_syntax bindM}, _) $ _ $ _) = true
+  fun contains_bind (Const (@{const_syntax bind}, _) $ _ $ _) = true
     | contains_bind (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
         contains_bind t;
-  fun bindM_monad_tr' (f::g::ts) = list_comb
+  fun bind_monad_tr' (f::g::ts) = list_comb
     (Const (@{syntax_const "_do"}, dummyT) $
-      unfold_monad (Const (@{const_syntax bindM}, dummyT) $ f $ g), ts);
+      unfold_monad (Const (@{const_syntax bind}, dummyT) $ f $ g), ts);
   fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) =
     if contains_bind g' then list_comb
       (Const (@{syntax_const "_do"}, dummyT) $
         unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
     else raise Match;
 in
- [(@{const_syntax bindM}, bindM_monad_tr'),
+ [(@{const_syntax bind}, bind_monad_tr'),
   (@{const_syntax Let}, Let_monad_tr')]
 end;
 *}
@@ -216,21 +216,21 @@
   "(f \<guillemotright>= lift g) = (f \<guillemotright>= (\<lambda>x. return (g x)))"
   by (simp add: lift_def comp_def)
 
-primrec mapM :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where (*FIXME just map?*)
-  "mapM f [] = return []"
-| "mapM f (x # xs) = do
+primrec fold_map :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where
+  "fold_map f [] = return []"
+| "fold_map f (x # xs) = do
      y \<leftarrow> f x;
-     ys \<leftarrow> mapM f xs;
+     ys \<leftarrow> fold_map f xs;
      return (y # ys)
    done"
 
-lemma mapM_append:
-  "mapM f (xs @ ys) = mapM f xs \<guillemotright>= (\<lambda>xs. mapM f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
+lemma fold_map_append:
+  "fold_map f (xs @ ys) = fold_map f xs \<guillemotright>= (\<lambda>xs. fold_map f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
   by (induct xs) simp_all
 
-lemma execute_mapM_unchanged_heap:
+lemma execute_fold_map_unchanged_heap:
   assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<exists>y. execute (f x) h = Some (y, h)"
-  shows "execute (mapM f xs) h =
+  shows "execute (fold_map f xs) h =
     Some (List.map (\<lambda>x. fst (the (execute (f x) h))) xs, h)"
 using assms proof (induct xs)
   case Nil show ?case by simp
@@ -238,7 +238,7 @@
   case (Cons x xs)
   from Cons.prems obtain y
     where y: "execute (f x) h = Some (y, h)" by auto
-  moreover from Cons.prems Cons.hyps have "execute (mapM f xs) h =
+  moreover from Cons.prems Cons.hyps have "execute (fold_map f xs) h =
     Some (map (\<lambda>x. fst (the (execute (f x) h))) xs, h)" by auto
   ultimately show ?case by (simp, simp only: execute_bind(1), simp)
 qed
@@ -314,7 +314,7 @@
                    g x s z
                 done) done)"
   unfolding MREC_def
-  unfolding bindM_def return_def
+  unfolding bind_def return_def
   apply simp
   apply (rule ext)
   apply (unfold mrec_rule[of x])
@@ -426,7 +426,7 @@
     fun is_const c = case lookup_const naming c
      of SOME c' => (fn c'' => c' = c'')
       | NONE => K false;
-    val is_bind = is_const @{const_name bindM};
+    val is_bind = is_const @{const_name bind};
     val is_return = is_const @{const_name return};
     val dummy_name = "";
     val dummy_type = ITyVar dummy_name;
@@ -527,6 +527,6 @@
 code_const return (Haskell "return")
 code_const Heap_Monad.raise' (Haskell "error/ _")
 
-hide_const (open) Heap heap guard execute raise'
+hide_const (open) Heap heap guard execute raise' fold_map
 
 end

--- a/src/HOL/Imperative_HOL/Relational.thy	Fri Jul 09 09:48:54 2010 +0200
+++ b/src/HOL/Imperative_HOL/Relational.thy	Fri Jul 09 10:08:10 2010 +0200
@@ -39,7 +39,7 @@
 lemma crelE[consumes 1]:
   assumes "crel (f >>= g) h h'' r'"
   obtains h' r where "crel f h h' r" "crel (g r) h' h'' r'"
-  using assms by (auto simp add: crel_def bindM_def split: option.split_asm)
+  using assms by (auto simp add: crel_def bind_def split: option.split_asm)
 
 lemma crelE'[consumes 1]:
   assumes "crel (f >> g) h h'' r'"
@@ -73,10 +73,10 @@
   using assms
   unfolding crel_def by auto
 
-lemma crel_mapM:
-  assumes "crel (mapM f xs) h h' r"
+lemma crel_fold_map:
+  assumes "crel (Heap_Monad.fold_map f xs) h h' r"
   assumes "\<And>h h'. P f [] h h' []"
-  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)"
+  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)"
   shows "P f xs h h' r"
 using assms(1)
 proof (induct xs arbitrary: h h' r)
@@ -85,11 +85,11 @@
 next
   case (Cons x xs)
   from Cons(2) obtain h1 y ys where crel_f: "crel (f x) h h1 y"
-    and crel_mapM: "crel (mapM f xs) h1 h' ys"
+    and crel_fold_map: "crel (Heap_Monad.fold_map f xs) h1 h' ys"
     and r_def: "r = y#ys"
-    unfolding mapM.simps
+    unfolding fold_map.simps
     by (auto elim!: crelE crel_return)
-  from Cons(1)[OF crel_mapM] crel_mapM crel_f assms(3) r_def
+  from Cons(1)[OF crel_fold_map] crel_fold_map crel_f assms(3) r_def
   show ?case by auto
 qed
 
@@ -156,9 +156,9 @@
   with l show ?thesis by (simp add: upt_conv_Cons)
 qed
 
-lemma crel_mapM_nth:
+lemma crel_fold_map_nth:
   assumes
-  "crel (mapM (Array.nth a) [Array.length a h - n..<Array.length a h]) h h' xs"
+  "crel (Heap_Monad.fold_map (Array.nth a) [Array.length a h - n..<Array.length a h]) h h' xs"
   assumes "n \<le> Array.length a h"
   shows "h = h' \<and> xs = drop (Array.length a h - n) (get_array a h)"
 using assms
@@ -170,12 +170,12 @@
   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]"
     by (simp add: upt_conv_Cons')
   with Suc(2) obtain r where
-    crel_mapM: "crel (mapM (Array.nth a) [Array.length a h - n..<Array.length a h]) h h' r"
+    crel_fold_map: "crel (Heap_Monad.fold_map (Array.nth a) [Array.length a h - n..<Array.length a h]) h h' r"
     and xs_def: "xs = get_array a h ! (Array.length a h - Suc n) # r"
     by (auto elim!: crelE crel_nth crel_return)
   from Suc(3) have "Array.length a h - n = Suc (Array.length a h - Suc n)" 
     by arith
-  with Suc.hyps[OF crel_mapM] xs_def show ?case
+  with Suc.hyps[OF crel_fold_map] xs_def show ?case
     unfolding Array.length_def
     by (auto simp add: nth_drop')
 qed
@@ -186,8 +186,8 @@
   using assms unfolding freeze_def
   by (elim crel_heap) simp
 
-lemma crel_mapM_map_entry_remains:
-  assumes "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
+lemma crel_fold_map_map_entry_remains:
+  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"
   assumes "i < Array.length a h - n"
   shows "get_array a h ! i = get_array a h' ! i"
 using assms
@@ -201,16 +201,16 @@
   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]"
     by (simp add: upt_conv_Cons')
   from Suc(2) this obtain r where
-    crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
+    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"
     by (auto simp add: elim!: crelE crel_map_entry crel_return)
   have length_remains: "Array.length a ?h1 = Array.length a h" by simp
-  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"
+  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"
     by simp
   from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
 qed
 
-lemma crel_mapM_map_entry_changes:
-  assumes "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
+lemma crel_fold_map_map_entry_changes:
+  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"
   assumes "n \<le> Array.length a h"  
   assumes "i \<ge> Array.length a h - n"
   assumes "i < Array.length a h"
@@ -226,22 +226,22 @@
   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]"
     by (simp add: upt_conv_Cons')
   from Suc(2) this obtain r where
-    crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
+    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"
     by (auto simp add: elim!: crelE crel_map_entry crel_return)
   have length_remains: "Array.length a ?h1 = Array.length a h" by simp
   from Suc(3) have less: "Array.length a h - Suc n < Array.length a h - n" by arith
   from Suc(3) have less2: "Array.length a h - Suc n < Array.length a h" by arith
   from Suc(4) length_remains have cases: "i = Array.length a ?h1 - Suc n \<or> i \<ge> Array.length a ?h1 - n" by arith
-  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"
+  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"
     by simp
   from Suc(1)[OF this] cases Suc(3) Suc(5) length_remains
-    crel_mapM_map_entry_remains[OF this, of "Array.length a h - Suc n", symmetric] less less2
+    crel_fold_map_map_entry_remains[OF this, of "Array.length a h - Suc n", symmetric] less less2
   show ?case
     by (auto simp add: nth_list_update_eq Array.length_def)
 qed
 
-lemma crel_mapM_map_entry_length:
-  assumes "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
+lemma crel_fold_map_map_entry_length:
+  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"
   assumes "n \<le> Array.length a h"
   shows "Array.length a h' = Array.length a h"
 using assms
@@ -254,21 +254,21 @@
   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]"
     by (simp add: upt_conv_Cons')
   from Suc(2) this obtain r where 
-    crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
+    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"
     by (auto elim!: crelE crel_map_entry crel_return)
   have length_remains: "Array.length a ?h1 = Array.length a h" by simp
-  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"
+  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"
     by simp
   from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
 qed
 
-lemma crel_mapM_map_entry:
-assumes "crel (mapM (\<lambda>n. map_entry n f a) [0..<Array.length a h]) h h' r"
+lemma crel_fold_map_map_entry:
+assumes "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [0..<Array.length a h]) h h' r"
   shows "get_array a h' = List.map f (get_array a h)"
 proof -
-  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
-  from crel_mapM_map_entry_length[OF this]
-  crel_mapM_map_entry_changes[OF this] show ?thesis
+  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
+  from crel_fold_map_map_entry_length[OF this]
+  crel_fold_map_map_entry_changes[OF this] show ?thesis
     unfolding Array.length_def
     by (auto intro: nth_equalityI)
 qed
@@ -342,7 +342,7 @@
   by (elim crel_if crel_return crel_raise) auto
 
 lemma crel_assert_eq: "(\<And>h h' r. crel f h h' r \<Longrightarrow> P r) \<Longrightarrow> f \<guillemotright>= assert P = f"
-unfolding crel_def bindM_def Let_def assert_def
+unfolding crel_def bind_def Let_def assert_def
   raise_def return_def prod_case_beta
 apply (cases f)
 apply simp
@@ -359,7 +359,7 @@
 lemma crelI:
   assumes "crel f h h' r" "crel (g r) h' h'' r'"
   shows "crel (f >>= g) h h'' r'"
-  using assms by (simp add: crel_def' bindM_def)
+  using assms by (simp add: crel_def' bind_def)
 
 lemma crelI':
   assumes "crel f h h' r" "crel g h' h'' r'"
@@ -513,19 +513,19 @@
   assumes "\<And>h' r. crel f h h' r \<Longrightarrow> noError (g r) h'"
   shows "noError (f \<guillemotright>= g) h"
   using assms
-  by (auto simp add: noError_def' crel_def' bindM_def)
+  by (auto simp add: noError_def' crel_def' bind_def)
 
 lemma noErrorI':
   assumes "noError f h"
   assumes "\<And>h' r. crel f h h' r \<Longrightarrow> noError g h'"
   shows "noError (f \<guillemotright> g) h"
   using assms
-  by (auto simp add: noError_def' crel_def' bindM_def)
+  by (auto simp add: noError_def' crel_def' bind_def)
 
 lemma noErrorI2:
 "\<lbrakk>crel f h h' r ; noError f h; noError (g r) h'\<rbrakk>
 \<Longrightarrow> noError (f \<guillemotright>= g) h"
-by (auto simp add: noError_def' crel_def' bindM_def)
+by (auto simp add: noError_def' crel_def' bind_def)
 
 lemma noError_return: 
   shows "noError (return x) h"
@@ -546,18 +546,18 @@
 using assms
 by (auto split: option.split)
 
-lemma noError_mapM: 
+lemma noError_fold_map: 
 assumes "\<forall>x \<in> set xs. noError (f x) h \<and> crel (f x) h h (r x)" 
-shows "noError (mapM f xs) h"
+shows "noError (Heap_Monad.fold_map f xs) h"
 using assms
 proof (induct xs)
   case Nil
   thus ?case
-    unfolding mapM.simps by (intro noError_return)
+    unfolding fold_map.simps by (intro noError_return)
 next
   case (Cons x xs)
   thus ?case
-    unfolding mapM.simps
+    unfolding fold_map.simps
     by (auto intro: noErrorI2[of "f x"] noErrorI noError_return)
 qed
 
@@ -611,9 +611,9 @@
   "noError (freeze a) h"
   by (simp add: freeze_def)
 
-lemma noError_mapM_map_entry:
+lemma noError_fold_map_map_entry:
   assumes "n \<le> Array.length a h"
-  shows "noError (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h"
+  shows "noError (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h"
 using assms
 proof (induct n arbitrary: h)
   case 0