renamed mbind to scomp
authorhaftmann
Wed Apr 09 17:46:17 2008 +0200 (2008-04-09)
changeset 2658943cb72871897
parent 26588 d83271bfaba5
child 26590 9114b5fe533a
renamed mbind to scomp
src/HOL/ex/Quickcheck.thy
src/HOL/ex/Random.thy
     1.1 --- a/src/HOL/ex/Quickcheck.thy	Wed Apr 09 08:10:11 2008 +0200
     1.2 +++ b/src/HOL/ex/Quickcheck.thy	Wed Apr 09 17:46:17 2008 +0200
     1.3 @@ -42,8 +42,8 @@
     1.4    fun term_ty ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
     1.5    fun mk_split thy ty ty' = Sign.mk_const thy
     1.6      (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, StateMonad.liftT (term_ty ty') @{typ seed}]);
     1.7 -  fun mk_mbind_split thy ty ty' t t' =
     1.8 -    StateMonad.mbind (term_ty ty) (term_ty ty') @{typ seed} t
     1.9 +  fun mk_scomp_split thy ty ty' t t' =
    1.10 +    StateMonad.scomp (term_ty ty) (term_ty ty') @{typ seed} t
    1.11        (mk_split thy ty ty' $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')))
    1.12    fun mk_cons thy this_ty (c, args) =
    1.13      let
    1.14 @@ -59,7 +59,7 @@
    1.15        val return = StateMonad.return (term_ty this_ty) @{typ seed}
    1.16          (HOLogic.mk_prod (c_t, t_t));
    1.17        val t = fold_rev (fn ((ty, _), random) =>
    1.18 -        mk_mbind_split thy ty this_ty random)
    1.19 +        mk_scomp_split thy ty this_ty random)
    1.20            args return;
    1.21        val is_rec = exists (snd o fst) args;
    1.22      in (is_rec, StateMonad.run (term_ty this_ty) @{typ seed} t) end;
    1.23 @@ -268,10 +268,10 @@
    1.24      fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
    1.25      fun mk_split ty = Sign.mk_const thy
    1.26        (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, StateMonad.liftT @{typ "term list option"} @{typ seed}]);
    1.27 -    fun mk_mbind_split ty t t' =
    1.28 -      StateMonad.mbind (mk_termtyp ty) @{typ "term list option"} @{typ seed} t (*FIXME*)
    1.29 +    fun mk_scomp_split ty t t' =
    1.30 +      StateMonad.scomp (mk_termtyp ty) @{typ "term list option"} @{typ seed} t (*FIXME*)
    1.31          (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')));
    1.32 -    fun mk_bindclause (_, _, i, ty) = mk_mbind_split ty
    1.33 +    fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
    1.34        (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i)
    1.35      val t = fold_rev mk_bindclause bounds (return $ check);
    1.36    in Abs ("n", @{typ index}, t) end;
     2.1 --- a/src/HOL/ex/Random.thy	Wed Apr 09 08:10:11 2008 +0200
     2.2 +++ b/src/HOL/ex/Random.thy	Wed Apr 09 17:46:17 2008 +0200
     2.3 @@ -114,7 +114,7 @@
     2.4      "range_aux (log 2147483561 k) 1 s = (v, w)"
     2.5      by (cases "range_aux (log 2147483561 k) 1 s")
     2.6    with assms show ?thesis
     2.7 -    by (simp add: range_def run_def mbind_def split_def del: range_aux.simps log.simps)
     2.8 +    by (simp add: range_def run_def scomp_def split_def del: range_aux.simps log.simps)
     2.9  qed
    2.10  
    2.11  definition
    2.12 @@ -135,7 +135,7 @@
    2.13    then have
    2.14      "nat_of_index (fst (range (index_of_nat (length xs)) s)) < length xs" by simp
    2.15    then show ?thesis
    2.16 -    by (auto simp add: select_def run_def mbind_def split_def)
    2.17 +    by (auto simp add: select_def run_def scomp_def split_def)
    2.18  qed
    2.19  
    2.20  definition
    2.21 @@ -148,7 +148,7 @@
    2.22  
    2.23  lemma select_default_zero:
    2.24    "fst (select_default 0 x y s) = y"
    2.25 -  by (simp add: run_def mbind_def split_def select_default_def)
    2.26 +  by (simp add: run_def scomp_def split_def select_default_def)
    2.27  
    2.28  lemma select_default_code [code]:
    2.29    "select_default k x y = (if k = 0 then do
    2.30 @@ -162,7 +162,7 @@
    2.31    case False then show ?thesis by (simp add: select_default_def)
    2.32  next
    2.33    case True then show ?thesis
    2.34 -    by (simp add: run_def mbind_def split_def select_default_def expand_fun_eq range_def)
    2.35 +    by (simp add: run_def scomp_def split_def select_default_def expand_fun_eq range_def)
    2.36  qed
    2.37  
    2.38