# HG changeset patch
# User haftmann
# Date 1220702556 -7200
# Node ID af3923ed478619e03bf4213402289eb3f4080a0b
# Parent  2c27248bf2670cc526ec90f61ca74e53f494d2a9
dropped "run" marker in monad syntax

diff -r 2c27248bf267 -r af3923ed4786 doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML	Fri Sep 05 11:50:35 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-structure Nat = 
-struct
-
-datatype nat = Suc of nat | Zero_nat;
-
-val one_nat : nat = Suc Zero_nat;
-
-fun nat_case f1 f2 Zero_nat = f1
-  | nat_case f1 f2 (Suc nat) = f2 nat;
-
-fun plus_nat (Suc m) n = plus_nat m (Suc n)
-  | plus_nat Zero_nat n = n;
-
-fun times_nat (Suc m) n = plus_nat n (times_nat m n)
-  | times_nat Zero_nat n = Zero_nat;
-
-end; (*struct Nat*)
-
-structure Codegen = 
-struct
-
-fun fac n =
-  (case n of Nat.Zero_nat => Nat.one_nat
-     | Nat.Suc m => Nat.times_nat n (fac m));
-
-end; (*struct Codegen*)
diff -r 2c27248bf267 -r af3923ed4786 doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML	Fri Sep 05 11:50:35 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-structure Nat = 
-struct
-
-datatype nat = Suc of nat | Zero_nat;
-
-fun less_nat m (Suc n) = less_eq_nat m n
-  | less_nat n Zero_nat = false
-and less_eq_nat (Suc m) n = less_nat m n
-  | less_eq_nat Zero_nat n = true;
-
-fun minus_nat (Suc m) (Suc n) = minus_nat m n
-  | minus_nat Zero_nat n = Zero_nat
-  | minus_nat m Zero_nat = m;
-
-end; (*struct Nat*)
-
-structure Codegen = 
-struct
-
-fun pick ((k, v) :: xs) n =
-  (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k));
-
-end; (*struct Codegen*)
diff -r 2c27248bf267 -r af3923ed4786 src/HOL/Library/Array.thy
--- a/src/HOL/Library/Array.thy	Fri Sep 05 11:50:35 2008 +0200
+++ b/src/HOL/Library/Array.thy	Sat Sep 06 14:02:36 2008 +0200
@@ -57,7 +57,7 @@
   obtain len h' where "Heap_Monad.execute (Array.length a) h = (len, h')"
     by (cases "Heap_Monad.execute (Array.length a) h")
   then show "Heap_Monad.execute (upd i x a \<guillemotright> return a) h = Heap_Monad.execute (upd i x a) h"
-    by (auto simp add: upd_def bindM_def run_drop split: sum.split)
+    by (auto simp add: upd_def bindM_def split: sum.split)
 qed
 
 
diff -r 2c27248bf267 -r af3923ed4786 src/HOL/Library/Heap_Monad.thy
--- a/src/HOL/Library/Heap_Monad.thy	Fri Sep 05 11:50:35 2008 +0200
+++ b/src/HOL/Library/Heap_Monad.thy	Sat Sep 06 14:02:36 2008 +0200
@@ -56,10 +56,6 @@
   by (simp add: heap_def)
 
 definition
-  run :: "'a Heap \<Rightarrow> 'a Heap" where
-  run_drop [code del]: "run f = f"
-
-definition
   bindM :: "'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
                   (Inl x, h') \<Rightarrow> execute (g x) h'
@@ -129,7 +125,7 @@
   "return" ("\<^raw:{\textsf{return}}>")
 
 translations
-  "_do f" => "CONST run f"
+  "_do f" => "f"
   "_bindM x f g" => "f \<guillemotright>= (\<lambda>x. g)"
   "_chainM f g" => "f \<guillemotright> g"
   "_let x t f" => "CONST Let t (\<lambda>x. f)"
@@ -140,18 +136,19 @@
   fun dest_abs_eta (Abs (abs as (_, ty, _))) =
         let
           val (v, t) = Syntax.variant_abs abs;
-        in ((v, ty), t) end
+        in (Free (v, ty), t) end
     | dest_abs_eta t =
         let
           val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
-        in ((v, dummyT), t) end
+        in (Free (v, dummyT), t) end;
   fun unfold_monad (Const (@{const_syntax bindM}, _) $ f $ g) =
         let
-          val ((v, ty), g') = dest_abs_eta g;
+          val (v, g') = dest_abs_eta g;
+          val vs = fold_aterms (fn Free (v, _) => insert (op =) v | _ => I) v [];
           val v_used = fold_aterms
-            (fn Free (w, _) => (fn s => s orelse v = w) | _ => I) g' false;
+            (fn Free (w, _) => (fn s => s orelse member (op =) vs w) | _ => I) g' false;
         in if v_used then
-          Const ("_bindM", dummyT) $ Free (v, ty) $ f $ unfold_monad g'
+          Const ("_bindM", dummyT) $ v $ f $ unfold_monad g'
         else
           Const ("_chainM", dummyT) $ f $ unfold_monad g'
         end
@@ -159,33 +156,28 @@
         Const ("_chainM", dummyT) $ f $ unfold_monad g
     | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
         let
-          val ((v, ty), g') = dest_abs_eta g;
-        in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
+          val (v, g') = dest_abs_eta g;
+        in Const ("_let", dummyT) $ v $ f $ unfold_monad g' end
     | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
-        Const ("return", dummyT) $ f
+        Const (@{const_syntax return}, dummyT) $ f
     | unfold_monad f = f;
-  fun tr' (f::ts) =
-    list_comb (Const ("_do", dummyT) $ unfold_monad f, ts)
-in [(@{const_syntax "run"}, tr')] end;
+  fun contains_bindM (Const (@{const_syntax bindM}, _) $ _ $ _) = true
+    | contains_bindM (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
+        contains_bindM t;
+  fun bindM_monad_tr' (f::g::ts) = list_comb
+    (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax bindM}, dummyT) $ f $ g), ts);
+  fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) = if contains_bindM g' then list_comb
+      (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 Let}, Let_monad_tr')
+] end;
 *}
 
 
 subsection {* Monad properties *}
 
-subsubsection {* Superfluous runs *}
-
-text {* @{term run} is just a doodle *}
-
-lemma run_simp [simp]:
-  "\<And>f. run (run f) = run f"
-  "\<And>f g. run f \<guillemotright>= g = f \<guillemotright>= g"
-  "\<And>f g. run f \<guillemotright> g = f \<guillemotright> g"
-  "\<And>f g. f \<guillemotright>= (\<lambda>x. run g) = f \<guillemotright>= (\<lambda>x. g)"
-  "\<And>f g. f \<guillemotright> run g = f \<guillemotright> g"
-  "\<And>f. f = run g \<longleftrightarrow> f = g"
-  "\<And>f. run f = g \<longleftrightarrow> f = g"
-  unfolding run_drop by rule+
-
 subsubsection {* Monad laws *}
 
 lemma return_bind: "return x \<guillemotright>= f = f x"
@@ -293,7 +285,6 @@
 code_type Heap (SML "unit/ ->/ _")
 code_const Heap (SML "raise/ (Fail/ \"bare Heap\")")
 code_const "op \<guillemotright>=" (SML "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())")
-code_const run (SML "_")
 code_const return (SML "!(fn/ ()/ =>/ _)")
 code_const "Heap_Monad.Fail" (SML "Fail")
 code_const "Heap_Monad.raise_exc" (SML "!(fn/ ()/ =>/ raise/ _)")
@@ -301,7 +292,6 @@
 code_type Heap (OCaml "_")
 code_const Heap (OCaml "failwith/ \"bare Heap\"")
 code_const "op \<guillemotright>=" (OCaml "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())")
-code_const run (OCaml "_")
 code_const return (OCaml "!(fun/ ()/ ->/ _)")
 code_const "Heap_Monad.Fail" (OCaml "Failure")
 code_const "Heap_Monad.raise_exc" (OCaml "!(fun/ ()/ ->/ raise/ _)")
@@ -416,7 +406,7 @@
 
 code_type Heap (Haskell "ST/ RealWorld/ _")
 code_const Heap (Haskell "error/ \"bare Heap\"")
-code_monad run "op \<guillemotright>=" Haskell
+code_monad "op \<guillemotright>=" Haskell
 code_const return (Haskell "return")
 code_const "Heap_Monad.Fail" (Haskell "_")
 code_const "Heap_Monad.raise_exc" (Haskell "error")
diff -r 2c27248bf267 -r af3923ed4786 src/HOL/Library/Relational.thy
--- a/src/HOL/Library/Relational.thy	Fri Sep 05 11:50:35 2008 +0200
+++ b/src/HOL/Library/Relational.thy	Sat Sep 06 14:02:36 2008 +0200
@@ -77,7 +77,7 @@
   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 r_def: "r = y#ys"
-    unfolding mapM.simps run_drop
+    unfolding mapM.simps
     by (auto elim!: crelE crel_return)
   from Cons(1)[OF crel_mapM] crel_mapM crel_f assms(3) r_def
   show ?case by auto
@@ -109,14 +109,14 @@
   assumes "crel (nth a i) h h' r"
   obtains "r = (get_array a h) ! i" "h = h'" "i < Heap.length a h"
   using assms
-  unfolding nth_def run_drop
+  unfolding nth_def
   by (auto elim!: crelE crel_if crel_raise crel_length crel_heap)
 
 lemma crel_upd[consumes 1]:
   assumes "crel (upd i v a) h h' r"
   obtains "r = a" "h' = Heap.upd a i v h"
   using assms
-  unfolding upd_def run_drop
+  unfolding upd_def
   by (elim crelE crel_if crel_return crel_raise
     crel_length crel_heap) auto
 
@@ -132,14 +132,14 @@
   assumes "crel (Array.map_entry i f a) h h' r"
   obtains "r = a" "h' = Heap.upd a i (f (get_array a h ! i)) h"
   using assms
-  unfolding Array.map_entry_def run_drop
+  unfolding Array.map_entry_def
   by (elim crelE crel_upd crel_nth) auto
 
 lemma crel_swap:
   assumes "crel (Array.swap i x a) h h' r"
   obtains "r = get_array a h ! i" "h' = Heap.upd a i x h"
   using assms
-  unfolding Array.swap_def run_drop
+  unfolding Array.swap_def
   by (elim crelE crel_upd crel_nth crel_return) auto
 
 (* Strong version of the lemma for this operation is missing *)
@@ -175,7 +175,7 @@
   with Suc(2) obtain r where
     crel_mapM: "crel (mapM (Array.nth a) [Heap.length a h - n..<Heap.length a h]) h h' r"
     and xs_def: "xs = get_array a h ! (Heap.length a h - Suc n) # r"
-    by (auto simp add: run_drop elim!: crelE crel_nth crel_return)
+    by (auto elim!: crelE crel_nth crel_return)
   from Suc(3) have "Heap.length a h - n = Suc (Heap.length a h - Suc n)" 
     by arith
   with Suc.hyps[OF crel_mapM] xs_def show ?case
@@ -188,7 +188,7 @@
   obtains "h = h'" "xs = get_array a h"
 proof 
   from assms have "crel (mapM (Array.nth a) [0..<Heap.length a h]) h h' xs"
-    unfolding freeze_def run_drop
+    unfolding freeze_def
     by (auto elim: crelE crel_length)
   hence "crel (mapM (Array.nth a) [(Heap.length a h - Heap.length a h)..<Heap.length a h]) h h' xs"
     by simp
@@ -211,7 +211,7 @@
     by (simp add: upt_conv_Cons')
   from Suc(2) this obtain r where
     crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
-    by (auto simp add: run_drop elim!: crelE crel_map_entry crel_return)
+    by (auto simp add: elim!: crelE crel_map_entry crel_return)
   have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
   from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
     by simp
@@ -236,7 +236,7 @@
     by (simp add: upt_conv_Cons')
   from Suc(2) this obtain r where
     crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
-    by (auto simp add: run_drop elim!: crelE crel_map_entry crel_return)
+    by (auto simp add: elim!: crelE crel_map_entry crel_return)
   have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
   from Suc(3) have less: "Heap.length a h - Suc n < Heap.length a h - n" by arith
   from Suc(3) have less2: "Heap.length a h - Suc n < Heap.length a h" by arith
@@ -264,7 +264,7 @@
     by (simp add: upt_conv_Cons')
   from Suc(2) this obtain r where 
     crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
-    by (auto simp add: run_drop elim!: crelE crel_map_entry crel_return)
+    by (auto elim!: crelE crel_map_entry crel_return)
   have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
   from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
     by simp
@@ -287,10 +287,10 @@
   obtains "r = a" "get_array a h' = List.map f (get_array a h)"
 proof
   from assms crel_mapM_map_entry show  "get_array a h' = List.map f (get_array a h)"
-    unfolding Array.map_def run_drop
+    unfolding Array.map_def
     by (fastsimp elim!: crelE crel_length crel_return)
   from assms show "r = a"
-    unfolding Array.map_def run_drop
+    unfolding Array.map_def
     by (elim crelE crel_return)
 qed
 
@@ -351,7 +351,7 @@
   assumes "crel (Ref.change f ref) h h' r"
   obtains "h' = set_ref ref (f (get_ref ref h)) h" "r = f (get_ref ref h)"
 using assms
-unfolding Ref.change_def run_drop Let_def
+unfolding Ref.change_def Let_def
 by (auto elim!: crelE crel_lookup crel_update crel_return)
 
 subsection {* Elimination rules for the assert command *}
@@ -446,14 +446,14 @@
   assumes "i < Heap.length a h"
   shows "crel (nth a i) h h ((get_array a h) ! i)"
   using assms
-  unfolding nth_def run_drop
+  unfolding nth_def
   by (auto intro!: crelI crel_ifI crel_raiseI crel_lengthI crel_heapI')
 
 lemma crel_updI:
   assumes "i < Heap.length a h"
   shows "crel (upd i v a) h (Heap.upd a i v h) a"
   using assms
-  unfolding upd_def run_drop
+  unfolding upd_def
   by (auto intro!: crelI crel_ifI crel_returnI crel_raiseI
     crel_lengthI crel_heapI')
 
@@ -481,7 +481,7 @@
 
 lemma crel_changeI: 
   shows "crel (Ref.change f ref) h (set_ref ref (f (get_ref ref h)) h) (f (get_ref ref h))"
-unfolding change_def Let_def run_drop by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
+unfolding change_def Let_def by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
 
 subsection {* Introduction rules for the assert command *}
 
@@ -562,7 +562,7 @@
 next
   case (Cons x xs)
   thus ?case
-    unfolding mapM.simps run_drop
+    unfolding mapM.simps
     by (auto intro: noErrorI2[of "f x"] noErrorI noError_return)
 qed
 
@@ -585,14 +585,14 @@
   assumes "i < Heap.length a h"
   shows "noError (Array.upd i v a) h"
   using assms
-  unfolding upd_def run_drop
+  unfolding upd_def
   by (auto intro!: noErrorI noError_if noError_return noError_length noError_heap) (auto elim: crel_length)
 
 lemma noError_nth:
 assumes "i < Heap.length a h"
   shows "noError (Array.nth a i) h"
   using assms
-  unfolding nth_def run_drop
+  unfolding nth_def
   by (auto intro!: noErrorI noError_if noError_return noError_length noError_heap) (auto elim: crel_length)
 
 lemma noError_of_list:
@@ -603,14 +603,14 @@
   assumes "i < Heap.length a h"
   shows "noError (map_entry i f a) h"
   using assms
-  unfolding map_entry_def run_drop
+  unfolding map_entry_def
   by (auto elim: crel_nth intro!: noErrorI noError_nth noError_upd)
 
 lemma noError_swap:
   assumes "i < Heap.length a h"
   shows "noError (swap i x a) h"
   using assms
-  unfolding swap_def run_drop
+  unfolding swap_def
   by (auto elim: crel_nth intro!: noErrorI noError_return noError_nth noError_upd)
 
 lemma noError_make:
@@ -625,7 +625,7 @@
 
 lemma noError_freeze:
   shows "noError (freeze a) h"
-unfolding freeze_def run_drop
+unfolding freeze_def
 by (auto intro!: noErrorI noError_length noError_mapM[of _ _ _ "\<lambda>x. get_array a h ! x"]
   noError_nth crel_nthI elim: crel_length)
 
@@ -641,13 +641,13 @@
   from Suc.prems have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
     by (simp add: upt_conv_Cons')
   with Suc.hyps[of "(Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h)"] Suc.prems show ?case
-    by (auto simp add: run_drop intro!: noErrorI noError_return noError_map_entry elim: crel_map_entry)
+    by (auto simp add: intro!: noErrorI noError_return noError_map_entry elim: crel_map_entry)
 qed
 
 lemma noError_map:
   shows "noError (Array.map f a) h"
 using noError_mapM_map_entry[of "Heap.length a h" a h]
-unfolding Array.map_def run_drop
+unfolding Array.map_def
 by (auto intro: noErrorI noError_length noError_return elim!: crel_length)
 
 subsection {* Introduction rules for the reference commands *}
@@ -666,7 +666,7 @@
 
 lemma noError_change:
   shows "noError (Ref.change f ref) h"
-  unfolding Ref.change_def run_drop Let_def by (intro noErrorI noError_lookup noError_update noError_return)
+  unfolding Ref.change_def Let_def by (intro noErrorI noError_lookup noError_update noError_return)
 
 subsection {* Introduction rules for the assert command *}
 
diff -r 2c27248bf267 -r af3923ed4786 src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Fri Sep 05 11:50:35 2008 +0200
+++ b/src/HOL/Library/State_Monad.thy	Sat Sep 06 14:02:36 2008 +0200
@@ -56,31 +56,23 @@
   we use a set of monad combinators:
 *}
 
-notation fcomp (infixl ">>" 60)
-notation (xsymbols) fcomp (infixl "\<guillemotright>" 60)
-notation scomp (infixl ">>=" 60)
-notation (xsymbols) scomp (infixl "\<guillemotright>=" 60)
+notation fcomp (infixl "o>" 60)
+notation (xsymbols) fcomp (infixl "o>" 60)
+notation scomp (infixl "o->" 60)
+notation (xsymbols) scomp (infixl "o\<rightarrow>" 60)
 
 abbreviation (input)
   "return \<equiv> Pair"
 
-definition
-  run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
-  "run f = f"
-
-print_ast_translation {*
-  [(@{const_syntax "run"}, fn (f::ts) => Syntax.mk_appl f ts)]
-*}
-
 text {*
   Given two transformations @{term f} and @{term g}, they
-  may be directly composed using the @{term "op \<guillemotright>"} combinator,
-  forming a forward composition: @{prop "(f \<guillemotright> g) s = f (g s)"}.
+  may be directly composed using the @{term "op o>"} combinator,
+  forming a forward composition: @{prop "(f o> g) s = f (g s)"}.
 
   After any yielding transformation, we bind the side result
   immediately using a lambda abstraction.  This 
-  is the purpose of the @{term "op \<guillemotright>="} combinator:
-  @{prop "(f \<guillemotright>= (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
+  is the purpose of the @{term "op o\<rightarrow>"} combinator:
+  @{prop "(f o\<rightarrow> (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
 
   For queries, the existing @{term "Let"} is appropriate.
 
@@ -88,8 +80,6 @@
   it to the state from the left;  we introduce the
   suggestive abbreviation @{term return} for this purpose.
 
-  The @{const run} ist just a marker.
-
   The most crucial distinction to Haskell is that we do
   not need to introduce distinguished type constructors
   for different kinds of state.  This has two consequences:
@@ -107,22 +97,6 @@
 *}
 
 
-subsection {* Obsolete runs *}
-
-text {*
-  @{term run} is just a doodle and should not occur nested:
-*}
-
-lemma run_simp [simp]:
-  "\<And>f. run (run f) = run f"
-  "\<And>f g. run f \<guillemotright>= g = f \<guillemotright>= g"
-  "\<And>f g. run f \<guillemotright> g = f \<guillemotright> g"
-  "\<And>f g. f \<guillemotright>= (\<lambda>x. run g) = f \<guillemotright>= (\<lambda>x. g)"
-  "\<And>f g. f \<guillemotright> run g = f \<guillemotright> g"
-  "\<And>f. f = run f \<longleftrightarrow> True"
-  "\<And>f. run f = f \<longleftrightarrow> True"
-  unfolding run_def by rule+
-
 subsection {* Monad laws *}
 
 text {*
@@ -130,66 +104,14 @@
   as normalization rules for monadic expressions:
 *}
 
-lemma
-  return_scomp [simp]: "return x \<guillemotright>= f = f x"
-  unfolding scomp_def by (simp add: expand_fun_eq)
-
-lemma
-  scomp_return [simp]: "x \<guillemotright>= return = x"
-  unfolding scomp_def by (simp add: expand_fun_eq split_Pair)
-
-lemma
-  id_fcomp [simp]: "id \<guillemotright> f = f"
-  unfolding fcomp_def by simp
-
-lemma
-  fcomp_id [simp]: "f \<guillemotright> id = f"
-  unfolding fcomp_def by simp
-
-lemma
-  scomp_scomp [simp]: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)"
-  unfolding scomp_def by (simp add: split_def expand_fun_eq)
-
-lemma
-  scomp_fcomp [simp]: "(f \<guillemotright>= g) \<guillemotright> h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright> h)"
-  unfolding scomp_def fcomp_def by (simp add: split_def expand_fun_eq)
-
-lemma
-  fcomp_scomp [simp]: "(f \<guillemotright> g) \<guillemotright>= h = f \<guillemotright> (g \<guillemotright>= h)"
-  unfolding scomp_def fcomp_def by (simp add: split_def expand_fun_eq)
-
-lemma
-  fcomp_fcomp [simp]: "(f \<guillemotright> g) \<guillemotright> h = f \<guillemotright> (g \<guillemotright> h)"
-  unfolding fcomp_def o_assoc ..
-
-lemmas monad_simp = run_simp return_scomp scomp_return id_fcomp fcomp_id
-  scomp_scomp scomp_fcomp fcomp_scomp fcomp_fcomp
+lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id
+  scomp_scomp scomp_fcomp fcomp_scomp fcomp_assoc
 
 text {*
   Evaluation of monadic expressions by force:
 *}
 
-lemmas monad_collapse = monad_simp o_apply o_assoc split_Pair split_comp
-  scomp_def fcomp_def run_def
-
-subsection {* ML abstract operations *}
-
-ML {*
-structure StateMonad =
-struct
-
-fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
-fun liftT' sT = sT --> sT;
-
-fun return T sT x = Const (@{const_name return}, T --> liftT T sT) $ x;
-
-fun scomp T1 T2 sT f g = Const (@{const_name scomp},
-  liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
-
-fun run T sT f = Const (@{const_name run}, liftT' (liftT T sT)) $ f;
-
-end;
-*}
+lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta
 
 
 subsection {* Syntax *}
@@ -211,7 +133,7 @@
     ("_;// _" [13, 12] 12)
   "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
     ("let _ = _;// _" [1000, 13, 12] 12)
-  "_nil" :: "'a \<Rightarrow> do_expr"
+  "_done" :: "'a \<Rightarrow> do_expr"
     ("_" [12] 12)
 
 syntax (xsymbols)
@@ -219,95 +141,55 @@
     ("_ \<leftarrow> _;// _" [1000, 13, 12] 12)
 
 translations
-  "_do f" => "CONST run f"
-  "_scomp x f g" => "f \<guillemotright>= (\<lambda>x. g)"
-  "_fcomp f g" => "f \<guillemotright> g"
+  "_do f" => "f"
+  "_scomp x f g" => "f o\<rightarrow> (\<lambda>x. g)"
+  "_fcomp f g" => "f o> g"
   "_let x t f" => "CONST Let t (\<lambda>x. f)"
-  "_nil f" => "f"
+  "_done f" => "f"
 
 print_translation {*
 let
   fun dest_abs_eta (Abs (abs as (_, ty, _))) =
         let
           val (v, t) = Syntax.variant_abs abs;
-        in ((v, ty), t) end
+        in (Free (v, ty), t) end
     | dest_abs_eta t =
         let
           val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
-        in ((v, dummyT), t) end
+        in (Free (v, dummyT), t) end;
   fun unfold_monad (Const (@{const_syntax scomp}, _) $ f $ g) =
         let
-          val ((v, ty), g') = dest_abs_eta g;
-        in Const ("_scomp", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
+          val (v, g') = dest_abs_eta g;
+        in Const ("_scomp", dummyT) $ v $ f $ unfold_monad g' end
     | unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) =
         Const ("_fcomp", dummyT) $ f $ unfold_monad g
     | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
         let
-          val ((v, ty), g') = dest_abs_eta g;
-        in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
+          val (v, g') = dest_abs_eta g;
+        in Const ("_let", dummyT) $ v $ f $ unfold_monad g' end
     | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
         Const ("return", dummyT) $ f
     | unfold_monad f = f;
-  fun tr' (f::ts) =
-    list_comb (Const ("_do", dummyT) $ unfold_monad f, ts)
-in [(@{const_syntax "run"}, tr')] end;
+  fun contains_scomp (Const (@{const_syntax scomp}, _) $ _ $ _) = true
+    | contains_scomp (Const (@{const_syntax fcomp}, _) $ _ $ t) =
+        contains_scomp t
+    | contains_scomp (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
+        contains_scomp t;
+  fun scomp_monad_tr' (f::g::ts) = list_comb
+    (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax scomp}, dummyT) $ f $ g), ts);
+  fun fcomp_monad_tr' (f::g::ts) = if contains_scomp g then list_comb
+      (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax fcomp}, dummyT) $ f $ g), ts)
+    else raise Match;
+  fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) = if contains_scomp g' then list_comb
+      (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
+    else raise Match;
+in [
+  (@{const_syntax scomp}, scomp_monad_tr'),
+  (@{const_syntax fcomp}, fcomp_monad_tr'),
+  (@{const_syntax Let}, Let_monad_tr')
+] end;
 *}
 
-
-subsection {* Combinators *}
-
-definition
-  lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> 'b \<times> 'c" where
-  "lift f x = return (f x)"
-
-primrec
-  list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
-  "list f [] = id"
-| "list f (x#xs) = (do f x; list f xs done)"
-
-primrec
-  list_yield :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<times> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'c list \<times> 'b" where
-  "list_yield f [] = return []"
-| "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"
-
-definition
-  collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
-  "collapse f = (do g \<leftarrow> f; g done)"
-
-text {* combinator properties *}
-
-lemma list_append [simp]:
-  "list f (xs @ ys) = list f xs \<guillemotright> list f ys"
-  by (induct xs) (simp_all del: id_apply)
-
-lemma list_cong [fundef_cong, recdef_cong]:
-  "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
-    \<Longrightarrow> list f xs = list g ys"
-proof (induct xs arbitrary: ys)
-  case Nil then show ?case by simp
-next
-  case (Cons x xs)
-  from Cons have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
-  then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto
-  with Cons have "list f xs = list g xs" by auto
-  with Cons have "list f (x # xs) = list g (x # xs)" by auto
-  with Cons show "list f (x # xs) = list g ys" by auto
-qed
-
-lemma list_yield_cong [fundef_cong, recdef_cong]:
-  "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
-    \<Longrightarrow> list_yield f xs = list_yield g ys"
-proof (induct xs arbitrary: ys)
-  case Nil then show ?case by simp
-next
-  case (Cons x xs)
-  from Cons have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
-  then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto
-  with Cons have "list_yield f xs = list_yield g xs" by auto
-  with Cons have "list_yield f (x # xs) = list_yield g (x # xs)" by auto
-  with Cons show "list_yield f (x # xs) = list_yield g ys" by auto
-qed
-
 text {*
   For an example, see HOL/ex/Random.thy.
 *}
diff -r 2c27248bf267 -r af3923ed4786 src/HOL/ex/ImperativeQuicksort.thy
--- a/src/HOL/ex/ImperativeQuicksort.thy	Fri Sep 05 11:50:35 2008 +0200
+++ b/src/HOL/ex/ImperativeQuicksort.thy	Sat Sep 06 14:02:36 2008 +0200
@@ -4,7 +4,6 @@
 
 text {* We prove QuickSort correct in the Relational Calculus. *}
 
-
 definition swap :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
 where
   "swap arr i j = (
@@ -21,7 +20,7 @@
   shows "multiset_of (get_array a h') 
   = multiset_of (get_array a h)"
   using assms
-  unfolding swap_def run_drop
+  unfolding swap_def
   by (auto simp add: Heap.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crelE crel_nth crel_return crel_upd)
 
 function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
@@ -49,7 +48,7 @@
 proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   case (1 a l r p h h' rs)
   thus ?case
-    unfolding part1.simps [of a l r p] run_drop
+    unfolding part1.simps [of a l r p]
     by (elim crelE crel_if crel_return crel_nth) (auto simp add: swap_permutes)
 qed
 
@@ -65,7 +64,7 @@
   proof (cases "r \<le> l")
     case True (* Terminating case *)
     with cr `l \<le> r` show ?thesis
-      unfolding part1.simps[of a l r p] run_drop
+      unfolding part1.simps[of a l r p]
       by (elim crelE crel_if crel_return crel_nth) auto
   next
     case False (* recursive case *)
@@ -76,7 +75,7 @@
       case True
       with cr False
       have rec1: "crel (part1 a (l + 1) r p) h h' rs"
-        unfolding part1.simps[of a l r p] run_drop
+        unfolding part1.simps[of a l r p]
         by (elim crelE crel_nth crel_if crel_return) auto
       from rec_condition have "l + 1 \<le> r" by arith
       from 1(1)[OF rec_condition True rec1 `l + 1 \<le> r`]
@@ -86,7 +85,7 @@
       with rec_condition cr
       obtain h1 where swp: "crel (swap a l r) h h1 ()"
         and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
-        unfolding part1.simps[of a l r p] run_drop
+        unfolding part1.simps[of a l r p]
         by (elim crelE crel_nth crel_if crel_return) auto
       from rec_condition have "l \<le> r - 1" by arith
       from 1(2) [OF rec_condition False rec2 `l \<le> r - 1`] show ?thesis by fastsimp
@@ -106,12 +105,12 @@
   proof (cases "r \<le> l")
     case True (* Terminating case *)
     with cr show ?thesis
-      unfolding part1.simps[of a l r p] run_drop
+      unfolding part1.simps[of a l r p]
       by (elim crelE crel_if crel_return crel_nth) auto
   next
     case False (* recursive case *)
     with cr 1 show ?thesis
-      unfolding part1.simps [of a l r p] swap_def run_drop
+      unfolding part1.simps [of a l r p] swap_def
       by (auto elim!: crelE crel_if crel_nth crel_return crel_upd) fastsimp
   qed
 qed
@@ -128,7 +127,7 @@
   proof (cases "r \<le> l")
     case True (* Terminating case *)
     with cr show ?thesis
-      unfolding part1.simps[of a l r p] run_drop
+      unfolding part1.simps[of a l r p]
       by (elim crelE crel_if crel_return crel_nth) auto
   next
     case False (* recursive case *)
@@ -139,7 +138,7 @@
       case True
       with cr False
       have rec1: "crel (part1 a (l + 1) r p) h h' rs"
-        unfolding part1.simps[of a l r p] run_drop
+        unfolding part1.simps[of a l r p]
         by (elim crelE crel_nth crel_if crel_return) auto
       from 1(1)[OF rec_condition True rec1]
       show ?thesis by fastsimp
@@ -148,11 +147,11 @@
       with rec_condition cr
       obtain h1 where swp: "crel (swap a l r) h h1 ()"
         and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
-        unfolding part1.simps[of a l r p] run_drop
+        unfolding part1.simps[of a l r p]
         by (elim crelE crel_nth crel_if crel_return) auto
       from swp rec_condition have
         "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array a h ! i = get_array a h1 ! i"
-	unfolding swap_def run_drop
+	unfolding swap_def
 	by (elim crelE crel_nth crel_upd crel_return) auto
       with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp
     qed
@@ -173,7 +172,7 @@
   proof (cases "r \<le> l")
     case True (* Terminating case *)
     with cr have "rs = r"
-      unfolding part1.simps[of a l r p] run_drop
+      unfolding part1.simps[of a l r p]
       by (elim crelE crel_if crel_return crel_nth) auto
     with True
     show ?thesis by auto
@@ -186,7 +185,7 @@
       case True
       with lr cr
       have rec1: "crel (part1 a (l + 1) r p) h h' rs"
-        unfolding part1.simps[of a l r p] run_drop
+        unfolding part1.simps[of a l r p]
         by (elim crelE crel_nth crel_if crel_return) auto
       from True part_outer_remains[OF rec1] have a_l: "get_array a h' ! l \<le> p"
 	by fastsimp
@@ -198,10 +197,10 @@
       with lr cr
       obtain h1 where swp: "crel (swap a l r) h h1 ()"
         and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
-        unfolding part1.simps[of a l r p] run_drop
+        unfolding part1.simps[of a l r p]
         by (elim crelE crel_nth crel_if crel_return) auto
       from swp False have "get_array a h1 ! r \<ge> p"
-	unfolding swap_def run_drop
+	unfolding swap_def
 	by (auto simp add: Heap.length_def elim!: crelE crel_nth crel_upd crel_return)
       with part_outer_remains [OF rec2] lr have a_r: "get_array a h' ! r \<ge> p"
 	by fastsimp
@@ -232,7 +231,7 @@
   = multiset_of (get_array a h)"
 proof -
     from assms part_permutes swap_permutes show ?thesis
-      unfolding partition.simps run_drop
+      unfolding partition.simps
       by (elim crelE crel_return crel_nth crel_if crel_upd) auto
 qed
 
@@ -241,7 +240,7 @@
   shows "Heap.length a h = Heap.length a h'"
 proof -
   from assms part_length_remains show ?thesis
-    unfolding partition.simps run_drop swap_def
+    unfolding partition.simps swap_def
     by (elim crelE crel_return crel_nth crel_if crel_upd) auto
 qed
 
@@ -251,7 +250,7 @@
   shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
 proof -
   from assms part_outer_remains part_returns_index_in_bounds show ?thesis
-    unfolding partition.simps swap_def run_drop
+    unfolding partition.simps swap_def
     by (elim crelE crel_return crel_nth crel_if crel_upd) fastsimp
 qed
 
@@ -263,7 +262,7 @@
   from crel obtain middle h'' p where part: "crel (part1 a l (r - 1) p) h h'' middle"
     and rs_equals: "rs = (if get_array a h'' ! middle \<le> get_array a h ! r then middle + 1
          else middle)"
-    unfolding partition.simps run_drop
+    unfolding partition.simps
     by (elim crelE crel_return crel_nth crel_if crel_upd) simp
   from `l < r` have "l \<le> r - 1" by arith
   from part_returns_index_in_bounds[OF part this] rs_equals `l < r` show ?thesis by auto
@@ -280,17 +279,17 @@
     and swap: "crel (swap a rs r) h1 h' ()"
     and rs_equals: "rs = (if get_array a h1 ! middle \<le> ?pivot then middle + 1
          else middle)"
-    unfolding partition.simps run_drop
+    unfolding partition.simps
     by (elim crelE crel_return crel_nth crel_if crel_upd) simp
   from swap have h'_def: "h' = Heap.upd a r (get_array a h1 ! rs)
     (Heap.upd a rs (get_array a h1 ! r) h1)"
-    unfolding swap_def run_drop
+    unfolding swap_def
     by (elim crelE crel_return crel_nth crel_upd) simp
   from swap have in_bounds: "r < Heap.length a h1 \<and> rs < Heap.length a h1"
-    unfolding swap_def run_drop
+    unfolding swap_def
     by (elim crelE crel_return crel_nth crel_upd) simp
   from swap have swap_length_remains: "Heap.length a h1 = Heap.length a h'"
-    unfolding swap_def run_drop by (elim crelE crel_return crel_nth crel_upd) auto
+    unfolding swap_def by (elim crelE crel_return crel_nth crel_upd) auto
   from `l < r` have "l \<le> r - 1" by simp 
   note middle_in_bounds = part_returns_index_in_bounds[OF part this]
   from part_outer_remains[OF part] `l < r`
@@ -298,7 +297,7 @@
     by fastsimp
   with swap
   have right_remains: "get_array a h ! r = get_array a h' ! rs"
-    unfolding swap_def run_drop
+    unfolding swap_def
     by (auto simp add: Heap.length_def elim!: crelE crel_return crel_nth crel_upd) (cases "r = rs", auto)
   from part_partitions [OF part]
   show ?thesis
@@ -414,7 +413,7 @@
 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   case (1 a l r h h' rs)
   with partition_permutes show ?case
-    unfolding quicksort.simps [of a l r] run_drop
+    unfolding quicksort.simps [of a l r]
     by (elim crel_if crelE crel_assert crel_return) auto
 qed
 
@@ -425,7 +424,7 @@
 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   case (1 a l r h h' rs)
   with partition_length_remains show ?case
-    unfolding quicksort.simps [of a l r] run_drop
+    unfolding quicksort.simps [of a l r]
     by (elim crel_if crelE crel_assert crel_return) auto
 qed
 
@@ -463,7 +462,7 @@
       ultimately have "get_array a h ! i= get_array a h' ! i" by simp
     }
     with cr show ?thesis
-      unfolding quicksort.simps [of a l r] run_drop
+      unfolding quicksort.simps [of a l r]
       by (elim crel_if crelE crel_assert crel_return) auto
   qed
 qed
@@ -472,7 +471,7 @@
   assumes "crel (quicksort a l r) h h' rs"
   shows "r \<le> l \<longrightarrow> h = h'"
   using assms
-  unfolding quicksort.simps [of a l r] run_drop
+  unfolding quicksort.simps [of a l r]
   by (elim crel_if crel_return) auto
  
 lemma quicksort_sorts:
@@ -544,7 +543,7 @@
 	by (auto simp add: set_sublist' dest: le_trans [of _ "get_array a h' ! p"])
     }
     with True cr show ?thesis
-      unfolding quicksort.simps [of a l r] run_drop
+      unfolding quicksort.simps [of a l r]
       by (elim crel_if crel_return crelE crel_assert) auto
   qed
 qed
@@ -577,7 +576,7 @@
 proof (induct a l r p arbitrary: h rule: part1.induct)
   case (1 a l r p)
   thus ?case
-    unfolding part1.simps [of a l r] swap_def run_drop
+    unfolding part1.simps [of a l r] swap_def
     by (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd elim!: crelE crel_upd crel_nth crel_return)
 qed
 
@@ -585,7 +584,7 @@
   assumes "l < r" "l < Heap.length a h" "r < Heap.length a h"
   shows "noError (partition a l r) h"
 using assms
-unfolding partition.simps swap_def run_drop
+unfolding partition.simps swap_def
 apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_part1 elim!: crelE crel_upd crel_nth crel_return)
 apply (frule part_length_remains)
 apply (frule part_returns_index_in_bounds)
@@ -604,7 +603,7 @@
 proof (induct a l r arbitrary: h rule: quicksort.induct)
   case (1 a l ri h)
   thus ?case
-    unfolding quicksort.simps [of a l ri] run_drop
+    unfolding quicksort.simps [of a l ri]
     apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_assert noError_partition)
     apply (frule partition_returns_index_in_bounds)
     apply auto
@@ -614,7 +613,7 @@
     apply (subgoal_tac "Suc r \<le> ri \<or> r = ri") 
     apply (erule disjE)
     apply auto
-    unfolding quicksort.simps [of a "Suc ri" ri] run_drop
+    unfolding quicksort.simps [of a "Suc ri" ri]
     apply (auto intro!: noError_if noError_return)
     done
 qed
diff -r 2c27248bf267 -r af3923ed4786 src/HOL/ex/Quickcheck.thy
--- a/src/HOL/ex/Quickcheck.thy	Fri Sep 05 11:50:35 2008 +0200
+++ b/src/HOL/ex/Quickcheck.thy	Sat Sep 06 14:02:36 2008 +0200
@@ -27,6 +27,25 @@
 
 text {* Datatypes *}
 
+definition
+  collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
+  "collapse f = (do g \<leftarrow> f; g done)"
+
+ML {*
+structure StateMonad =
+struct
+
+fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
+fun liftT' sT = sT --> sT;
+
+fun return T sT x = Const (@{const_name return}, T --> liftT T sT) $ x;
+
+fun scomp T1 T2 sT f g = Const (@{const_name scomp},
+  liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
+
+end;
+*}
+
 lemma random'_if:
   fixes random' :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed"
   assumes "random' 0 j = undefined"
@@ -62,7 +81,7 @@
         mk_scomp_split thy ty this_ty random)
           args return;
       val is_rec = exists (snd o fst) args;
-    in (is_rec, StateMonad.run (term_ty this_ty) @{typ seed} t) end;
+    in (is_rec, t) end;
   fun mk_conss thy ty [] = NONE
     | mk_conss thy ty [(_, t)] = SOME t
     | mk_conss thy ty ts = SOME (mk_collapse thy (term_ty ty) $
diff -r 2c27248bf267 -r af3923ed4786 src/HOL/ex/Random.thy
--- a/src/HOL/ex/Random.thy	Fri Sep 05 11:50:35 2008 +0200
+++ b/src/HOL/ex/Random.thy	Sat Sep 06 14:02:36 2008 +0200
@@ -55,18 +55,6 @@
   "(if b then f x else f y) = f (if b then x else y)"
   by (cases b) simp_all
 
-(*lemma seed_invariant:
-  assumes "seed_invariant (index_of_nat v, index_of_nat w)"
-    and "(index_of_nat z, (index_of_nat v', index_of_nat w')) = next (index_of_nat v, index_of_nat w)"
-  shows "seed_invariant (index_of_nat v', index_of_nat w')"
-using assms
-apply (auto simp add: seed_invariant_def)
-apply (auto simp add: minus_shift_def Let_def)
-apply (simp_all add: if_same cong del: if_cong)
-apply safe
-unfolding not_less
-oops*)
-
 definition
   split_seed :: "seed \<Rightarrow> seed \<times> seed"
 where
@@ -109,7 +97,7 @@
     "range_aux (log 2147483561 k) 1 s = (v, w)"
     by (cases "range_aux (log 2147483561 k) 1 s")
   with assms show ?thesis
-    by (simp add: range_def run_def scomp_def split_def del: range_aux.simps log.simps)
+    by (simp add: monad_collapse range_def del: range_aux.simps log.simps)
 qed
 
 definition
@@ -130,7 +118,7 @@
   then have
     "nat_of_index (fst (range (index_of_nat (length xs)) s)) < length xs" by simp
   then show ?thesis
-    by (auto simp add: select_def run_def scomp_def split_def)
+    by (auto simp add: monad_collapse select_def)
 qed
 
 definition
@@ -143,7 +131,7 @@
 
 lemma select_default_zero:
   "fst (select_default 0 x y s) = y"
-  by (simp add: run_def scomp_def split_def select_default_def)
+  by (simp add: monad_collapse select_default_def)
 
 lemma select_default_code [code]:
   "select_default k x y = (if k = 0 then do
@@ -157,7 +145,7 @@
   case False then show ?thesis by (simp add: select_default_def)
 next
   case True then show ?thesis
-    by (simp add: run_def scomp_def split_def select_default_def expand_fun_eq range_def)
+    by (simp add: monad_collapse select_default_def range_def)
 qed
 
 
@@ -192,3 +180,4 @@
 *}
 
 end
+
diff -r 2c27248bf267 -r af3923ed4786 src/Tools/code/code_haskell.ML
--- a/src/Tools/code/code_haskell.ML	Fri Sep 05 11:50:35 2008 +0200
+++ b/src/Tools/code/code_haskell.ML	Sat Sep 06 14:02:36 2008 +0200
@@ -425,50 +425,45 @@
 
 (** optional monad syntax **)
 
-fun implode_monad c_bind t =
-  let
-    fun dest_monad (IConst (c, _) `$ t1 `$ t2) =
-          if c = c_bind
-            then case Code_Thingol.split_abs t2
-             of SOME (((v, pat), ty), t') =>
-                  SOME ((SOME (((SOME v, pat), ty), true), t1), t')
-              | NONE => NONE
-            else NONE
-      | dest_monad t = case Code_Thingol.split_let t
-           of SOME (((pat, ty), tbind), t') =>
-                SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')
-            | NONE => NONE;
-  in Code_Thingol.unfoldr dest_monad t end;
-
 fun pretty_haskell_monad c_bind =
   let
-    fun pretty pr thm pat vars fxy [(t, _)] =
-      let
-        val pr_bind = pr_haskell_bind (K (K pr)) thm;
-        fun pr_monad (NONE, t) vars =
-              (semicolon [pr vars NOBR t], vars)
-          | pr_monad (SOME (bind, true), t) vars = vars
-              |> pr_bind NOBR bind
-              |>> (fn p => semicolon [p, str "<-", pr vars NOBR t])
-          | pr_monad (SOME (bind, false), t) vars = vars
-              |> pr_bind NOBR bind
-              |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
-        val (binds, t) = implode_monad c_bind t;
-        val (ps, vars') = fold_map pr_monad binds vars;
-      in (brackify fxy o single o Pretty.enclose "do {" "}") (ps @| pr vars' NOBR t) end;
-  in (1, pretty) end;
+    fun dest_bind t1 t2 = case Code_Thingol.split_abs t2
+     of SOME (((v, pat), ty), t') =>
+          SOME ((SOME (((SOME v, pat), ty), true), t1), t')
+      | NONE => NONE;
+    fun dest_monad (IConst (c, _) `$ t1 `$ t2) =
+          if c = c_bind then dest_bind t1 t2
+          else NONE
+      | dest_monad t = case Code_Thingol.split_let t
+         of SOME (((pat, ty), tbind), t') =>
+              SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')
+          | NONE => NONE;
+    val implode_monad = Code_Thingol.unfoldr dest_monad;
+    fun pr_monad pr_bind pr (NONE, t) vars =
+          (semicolon [pr vars NOBR t], vars)
+      | pr_monad pr_bind pr (SOME (bind, true), t) vars = vars
+          |> pr_bind NOBR bind
+          |>> (fn p => semicolon [p, str "<-", pr vars NOBR t])
+      | pr_monad pr_bind pr (SOME (bind, false), t) vars = vars
+          |> pr_bind NOBR bind
+          |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
+    fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
+     of SOME (bind, t') => let
+          val (binds, t'') = implode_monad t'
+          val (ps, vars') = fold_map (pr_monad (pr_haskell_bind (K (K pr)) thm) pr) (bind :: binds) vars;
+        in (brackify fxy o single o Pretty.enclose "do {" "}" o Pretty.breaks) (ps @| pr vars' NOBR t'') end
+      | NONE => brackify_infix (1, L) fxy
+          [pr vars (INFX (1, L)) t1, str ">>=", pr vars (INFX (1, X)) t2]
+  in (2, pretty) end;
 
-fun add_monad target' raw_c_run raw_c_bind thy =
+fun add_monad target' raw_c_bind thy =
   let
-    val c_run = Code_Unit.read_const thy raw_c_run;
     val c_bind = Code_Unit.read_const thy raw_c_bind;
     val c_bind' = Code_Name.const thy c_bind;
   in if target = target' then
     thy
-    |> Code_Target.add_syntax_const target c_run
+    |> Code_Target.add_syntax_const target c_bind
         (SOME (pretty_haskell_monad c_bind'))
-    |> Code_Target.add_syntax_const target c_bind
-        (Code_Printer.simple_const_syntax (SOME (Code_Printer.parse_infix fst (L, 1) ">>=")))
   else error "Only Haskell target allows for monad syntax" end;
 
 
@@ -482,9 +477,8 @@
 
 val _ =
   OuterSyntax.command "code_monad" "define code syntax for monads" OuterKeyword.thy_decl (
-    OuterParse.term_group -- OuterParse.term_group -- OuterParse.name
-    >> (fn ((raw_run, raw_bind), target) => Toplevel.theory 
-          (add_monad target raw_run raw_bind))
+    OuterParse.term_group -- OuterParse.name >> (fn (raw_bind, target) =>
+      Toplevel.theory  (add_monad target raw_bind))
   );
 
 val setup =