# HG changeset patch
# User huffman
# Date 1274310521 25200
# Node ID 9316a18ec9319ec6b461e881838a2b3c2109a139
# Parent  ca3172dbde8bcb92f3947719453ae191350d8d10
remove unnecessary constant Fixrec.bind

diff -r ca3172dbde8b -r 9316a18ec931 src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Wed May 19 14:38:25 2010 -0700
+++ b/src/HOLCF/Fixrec.thy	Wed May 19 16:08:41 2010 -0700
@@ -65,30 +65,6 @@
     == "CONST maybe_when\<cdot>t1\<cdot>(\<Lambda> x. t2)\<cdot>m"
 
 
-subsubsection {* Monadic bind operator *}
-
-definition
-  bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe" where
-  "bind = (\<Lambda> m f. case m of fail \<Rightarrow> fail | return\<cdot>x \<Rightarrow> f\<cdot>x)"
-
-text {* monad laws *}
-
-lemma bind_strict [simp]: "bind\<cdot>\<bottom>\<cdot>f = \<bottom>"
-by (simp add: bind_def)
-
-lemma bind_fail [simp]: "bind\<cdot>fail\<cdot>f = fail"
-by (simp add: bind_def)
-
-lemma left_unit [simp]: "bind\<cdot>(return\<cdot>a)\<cdot>k = k\<cdot>a"
-by (simp add: bind_def)
-
-lemma right_unit [simp]: "bind\<cdot>m\<cdot>return = m"
-by (rule_tac p=m in maybeE, simp_all)
-
-lemma bind_assoc:
- "bind\<cdot>(bind\<cdot>m\<cdot>k)\<cdot>h = bind\<cdot>m\<cdot>(\<Lambda> a. bind\<cdot>(k\<cdot>a)\<cdot>h)"
-by (rule_tac p=m in maybeE, simp_all)
-
 subsubsection {* Run operator *}
 
 definition
@@ -169,7 +145,7 @@
 
 definition
   branch :: "('a \<rightarrow> 'b maybe) \<Rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'c maybe)" where
-  "branch p \<equiv> \<Lambda> r x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> y. return\<cdot>(r\<cdot>y))"
+  "branch p \<equiv> \<Lambda> r x. maybe_when\<cdot>fail\<cdot>(\<Lambda> y. return\<cdot>(r\<cdot>y))\<cdot>(p\<cdot>x)"
 
 lemma branch_rews:
   "p\<cdot>x = \<bottom> \<Longrightarrow> branch p\<cdot>r\<cdot>x = \<bottom>"
@@ -277,7 +253,7 @@
 definition
   cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat" where
   "cpair_pat p1 p2 = (\<Lambda>(x, y).
-    bind\<cdot>(p1\<cdot>x)\<cdot>(\<Lambda> a. bind\<cdot>(p2\<cdot>y)\<cdot>(\<Lambda> b. return\<cdot>(a, b))))"
+    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))"
 
 definition
   spair_pat ::
@@ -425,7 +401,7 @@
 
 definition
   as_pat :: "('a \<rightarrow> 'b maybe) \<Rightarrow> 'a \<rightarrow> ('a \<times> 'b) maybe" where
-  "as_pat p = (\<Lambda> x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> a. return\<cdot>(x, a)))"
+  "as_pat p = (\<Lambda> x. maybe_when\<cdot>fail\<cdot>(\<Lambda> a. return\<cdot>(x, a))\<cdot>(p\<cdot>x))"
 
 definition
   lazy_pat :: "('a \<rightarrow> 'b::pcpo maybe) \<Rightarrow> ('a \<rightarrow> 'b maybe)" where
@@ -608,7 +584,7 @@
       (@{const_name UU}, @{const_name match_UU}) ]
 *}
 
-hide_const (open) return bind fail run cases
+hide_const (open) return fail run cases
 
 lemmas [fixrec_simp] =
   run_strict run_fail run_return
diff -r ca3172dbde8b -r 9316a18ec931 src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Wed May 19 14:38:25 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Wed May 19 16:08:41 2010 -0700
@@ -952,7 +952,7 @@
           val (fun1, fun2, taken) = pat_lhs (pat, args);
           val defs = @{thm branch_def} :: pat_defs;
           val goal = mk_trp (mk_strict fun1);
-          val rules = @{thm Fixrec.bind_strict} :: case_rews;
+          val rules = @{thms maybe_when_rews} @ case_rews;
           val tacs = [simp_tac (beta_ss addsimps rules) 1];
         in prove thy defs goal (K tacs) end;
       fun pat_apps (i, (pat, (con, args))) =
@@ -967,7 +967,7 @@
               val concl = mk_trp (mk_eq (fun1 ` con_app, rhs));
               val goal = Logic.list_implies (assms, concl);
               val defs = @{thm branch_def} :: pat_defs;
-              val rules = @{thms bind_fail left_unit} @ case_rews;
+              val rules = @{thms maybe_when_rews} @ case_rews;
               val tacs = [asm_simp_tac (beta_ss addsimps rules) 1];
             in prove thy defs goal (K tacs) end;
         in map_index pat_app spec end;