1.1 --- a/src/HOLCF/Fixrec.thy	Wed May 19 14:38:25 2010 -0700
     1.2 +++ b/src/HOLCF/Fixrec.thy	Wed May 19 16:08:41 2010 -0700
     1.3 @@ -65,30 +65,6 @@
     1.4      == "CONST maybe_when\<cdot>t1\<cdot>(\<Lambda> x. t2)\<cdot>m"
     1.5  
     1.6  
     1.7 -subsubsection {* Monadic bind operator *}
     1.8 -
     1.9 -definition
    1.10 -  bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe" where
    1.11 -  "bind = (\<Lambda> m f. case m of fail \<Rightarrow> fail | return\<cdot>x \<Rightarrow> f\<cdot>x)"
    1.12 -
    1.13 -text {* monad laws *}
    1.14 -
    1.15 -lemma bind_strict [simp]: "bind\<cdot>\<bottom>\<cdot>f = \<bottom>"
    1.16 -by (simp add: bind_def)
    1.17 -
    1.18 -lemma bind_fail [simp]: "bind\<cdot>fail\<cdot>f = fail"
    1.19 -by (simp add: bind_def)
    1.20 -
    1.21 -lemma left_unit [simp]: "bind\<cdot>(return\<cdot>a)\<cdot>k = k\<cdot>a"
    1.22 -by (simp add: bind_def)
    1.23 -
    1.24 -lemma right_unit [simp]: "bind\<cdot>m\<cdot>return = m"
    1.25 -by (rule_tac p=m in maybeE, simp_all)
    1.26 -
    1.27 -lemma bind_assoc:
    1.28 - "bind\<cdot>(bind\<cdot>m\<cdot>k)\<cdot>h = bind\<cdot>m\<cdot>(\<Lambda> a. bind\<cdot>(k\<cdot>a)\<cdot>h)"
    1.29 -by (rule_tac p=m in maybeE, simp_all)
    1.30 -
    1.31  subsubsection {* Run operator *}
    1.32  
    1.33  definition
    1.34 @@ -169,7 +145,7 @@
    1.35  
    1.36  definition
    1.37    branch :: "('a \<rightarrow> 'b maybe) \<Rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'c maybe)" where
    1.38 -  "branch p \<equiv> \<Lambda> r x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> y. return\<cdot>(r\<cdot>y))"
    1.39 +  "branch p \<equiv> \<Lambda> r x. maybe_when\<cdot>fail\<cdot>(\<Lambda> y. return\<cdot>(r\<cdot>y))\<cdot>(p\<cdot>x)"
    1.40  
    1.41  lemma branch_rews:
    1.42    "p\<cdot>x = \<bottom> \<Longrightarrow> branch p\<cdot>r\<cdot>x = \<bottom>"
    1.43 @@ -277,7 +253,7 @@
    1.44  definition
    1.45    cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat" where
    1.46    "cpair_pat p1 p2 = (\<Lambda>(x, y).
    1.47 -    bind\<cdot>(p1\<cdot>x)\<cdot>(\<Lambda> a. bind\<cdot>(p2\<cdot>y)\<cdot>(\<Lambda> b. return\<cdot>(a, b))))"
    1.48 +    maybe_when\<cdot>fail\<cdot>(\<Lambda> a. maybe_when\<cdot>fail\<cdot>(\<Lambda> b. return\<cdot>(a, b))\<cdot>(p2\<cdot>y))\<cdot>(p1\<cdot>x))"
    1.49  
    1.50  definition
    1.51    spair_pat ::
    1.52 @@ -425,7 +401,7 @@
    1.53  
    1.54  definition
    1.55    as_pat :: "('a \<rightarrow> 'b maybe) \<Rightarrow> 'a \<rightarrow> ('a \<times> 'b) maybe" where
    1.56 -  "as_pat p = (\<Lambda> x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> a. return\<cdot>(x, a)))"
    1.57 +  "as_pat p = (\<Lambda> x. maybe_when\<cdot>fail\<cdot>(\<Lambda> a. return\<cdot>(x, a))\<cdot>(p\<cdot>x))"
    1.58  
    1.59  definition
    1.60    lazy_pat :: "('a \<rightarrow> 'b::pcpo maybe) \<Rightarrow> ('a \<rightarrow> 'b maybe)" where
    1.61 @@ -608,7 +584,7 @@
    1.62        (@{const_name UU}, @{const_name match_UU}) ]
    1.63  *}
    1.64  
    1.65 -hide_const (open) return bind fail run cases
    1.66 +hide_const (open) return fail run cases
    1.67  
    1.68  lemmas [fixrec_simp] =
    1.69    run_strict run_fail run_return

     2.1 --- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Wed May 19 14:38:25 2010 -0700
     2.2 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Wed May 19 16:08:41 2010 -0700
     2.3 @@ -952,7 +952,7 @@
     2.4            val (fun1, fun2, taken) = pat_lhs (pat, args);
     2.5            val defs = @{thm branch_def} :: pat_defs;
     2.6            val goal = mk_trp (mk_strict fun1);
     2.7 -          val rules = @{thm Fixrec.bind_strict} :: case_rews;
     2.8 +          val rules = @{thms maybe_when_rews} @ case_rews;
     2.9            val tacs = [simp_tac (beta_ss addsimps rules) 1];
    2.10          in prove thy defs goal (K tacs) end;
    2.11        fun pat_apps (i, (pat, (con, args))) =
    2.12 @@ -967,7 +967,7 @@
    2.13                val concl = mk_trp (mk_eq (fun1 ` con_app, rhs));
    2.14                val goal = Logic.list_implies (assms, concl);
    2.15                val defs = @{thm branch_def} :: pat_defs;
    2.16 -              val rules = @{thms bind_fail left_unit} @ case_rews;
    2.17 +              val rules = @{thms maybe_when_rews} @ case_rews;
    2.18                val tacs = [asm_simp_tac (beta_ss addsimps rules) 1];
    2.19              in prove thy defs goal (K tacs) end;
    2.20          in map_index pat_app spec end;