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
+