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