make maybe into a real type constructor; remove monad syntax

--- a/src/HOLCF/Fixrec.thy	Thu Feb 16 23:40:32 2006 +0100
+++ b/src/HOLCF/Fixrec.thy	Fri Feb 17 01:46:38 2006 +0100
@@ -14,84 +14,81 @@
 
 defaultsort cpo
 
-types 'a maybe = "one ++ 'a u"
+pcpodef (open) 'a maybe = "UNIV::(one ++ 'a u) set"
+by simp
 
 constdefs
   fail :: "'a maybe"
-  "fail \<equiv> sinl\<cdot>ONE"
+  "fail \<equiv> Abs_maybe (sinl\<cdot>ONE)"
 
   return :: "'a \<rightarrow> 'a maybe"
-  "return \<equiv> sinr oo up"
+  "return \<equiv> \<Lambda> x. Abs_maybe (sinr\<cdot>(up\<cdot>x))"
+
+  maybe_when :: "'b \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a maybe \<rightarrow> 'b::pcpo"
+  "maybe_when \<equiv> \<Lambda> f r m. sscase\<cdot>(\<Lambda> x. f)\<cdot>(fup\<cdot>r)\<cdot>(Rep_maybe m)"
 
 lemma maybeE:
   "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = fail \<Longrightarrow> Q; \<And>x. p = return\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
 apply (unfold fail_def return_def)
-apply (rule_tac p=p in ssumE, simp)
+apply (cases p, rename_tac r)
+apply (rule_tac p=r in ssumE, simp add: Abs_maybe_strict)
 apply (rule_tac p=x in oneE, simp, simp)
-apply (rule_tac p=y in upE, simp, simp)
+apply (rule_tac p=y in upE, simp, simp add: cont_Abs_maybe)
 done
 
 lemma return_defined [simp]: "return\<cdot>x \<noteq> \<bottom>"
-by (simp add: return_def)
+by (simp add: return_def cont_Abs_maybe Abs_maybe_defined)
 
 lemma fail_defined [simp]: "fail \<noteq> \<bottom>"
-by (simp add: fail_def)
+by (simp add: fail_def Abs_maybe_defined)
 
 lemma return_eq [simp]: "(return\<cdot>x = return\<cdot>y) = (x = y)"
-by (simp add: return_def)
+by (simp add: return_def cont_Abs_maybe Abs_maybe_inject)
 
 lemma return_neq_fail [simp]:
   "return\<cdot>x \<noteq> fail" "fail \<noteq> return\<cdot>x"
-by (simp_all add: return_def fail_def)
+by (simp_all add: return_def fail_def cont_Abs_maybe Abs_maybe_inject)
+
+lemma maybe_when_rews [simp]:
+  "maybe_when\<cdot>f\<cdot>r\<cdot>\<bottom> = \<bottom>"
+  "maybe_when\<cdot>f\<cdot>r\<cdot>fail = f"
+  "maybe_when\<cdot>f\<cdot>r\<cdot>(return\<cdot>x) = r\<cdot>x"
+by (simp_all add: return_def fail_def maybe_when_def cont_Rep_maybe
+                  cont_Abs_maybe Abs_maybe_inverse Rep_maybe_strict)
+
+translations
+  "case m of fail \<Rightarrow> t1 | return\<cdot>x \<Rightarrow> t2" == "maybe_when\<cdot>t1\<cdot>(\<Lambda> x. t2)\<cdot>m"
 
 
 subsubsection {* Monadic bind operator *}
 
 constdefs
   bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe"
-  "bind \<equiv> \<Lambda> m f. sscase\<cdot>sinl\<cdot>(fup\<cdot>f)\<cdot>m"
-
-syntax ">>=" :: "['a maybe, 'a \<rightarrow> 'b maybe] \<Rightarrow> 'b maybe" (infixl ">>=" 50)
-translations "m >>= f" == "bind\<cdot>m\<cdot>f"
-
-nonterminals
-  maybebind maybebinds
-
-syntax 
-  "_MBIND"  :: "pttrn \<Rightarrow> 'a maybe \<Rightarrow> maybebind"         ("(2_ <-/ _)" 10)
-  ""        :: "maybebind \<Rightarrow> maybebinds"                ("_")
-
-  "_MBINDS" :: "[maybebind, maybebinds] \<Rightarrow> maybebinds"  ("_;/ _")
-  "_MDO"    :: "[maybebinds, 'a maybe] \<Rightarrow> 'a maybe"     ("(do _;/ (_))" 10)
-
-translations
-  "_MDO (_MBINDS b bs) e" == "_MDO b (_MDO bs e)"
-  "do (x,y) <- m; e" == "m >>= (LAM <x,y>. e)" 
-  "do x <- m; e"            == "m >>= (LAM x. e)"
+  "bind \<equiv> \<Lambda> m f. case m of fail \<Rightarrow> fail | return\<cdot>x \<Rightarrow> f\<cdot>x"
 
 text {* monad laws *}
 
-lemma bind_strict [simp]: "UU >>= f = UU"
+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 bind_fail [simp]: "fail >>= f = fail"
-by (simp add: bind_def fail_def)
+lemma left_unit [simp]: "bind\<cdot>(return\<cdot>a)\<cdot>k = k\<cdot>a"
+by (simp add: bind_def)
 
-lemma left_unit [simp]: "(return\<cdot>a) >>= k = k\<cdot>a"
-by (simp add: bind_def return_def)
-
-lemma right_unit [simp]: "m >>= return = m"
+lemma right_unit [simp]: "bind\<cdot>m\<cdot>return = m"
 by (rule_tac p=m in maybeE, simp_all)
 
-lemma bind_assoc [simp]:
- "(do b <- (do a <- m; k\<cdot>a); h\<cdot>b) = (do a <- m; b <- k\<cdot>a; h\<cdot>b)"
+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 *}
 
 constdefs
-  run:: "'a::pcpo maybe \<rightarrow> 'a"
-  "run \<equiv> sscase\<cdot>\<bottom>\<cdot>(fup\<cdot>ID)"
+  run:: "'a maybe \<rightarrow> 'a::pcpo"
+  "run \<equiv> maybe_when\<cdot>\<bottom>\<cdot>ID"
 
 text {* rewrite rules for run *}
 
@@ -99,16 +96,16 @@
 by (simp add: run_def)
 
 lemma run_fail [simp]: "run\<cdot>fail = \<bottom>"
-by (simp add: run_def fail_def)
+by (simp add: run_def)
 
 lemma run_return [simp]: "run\<cdot>(return\<cdot>x) = x"
-by (simp add: run_def return_def)
+by (simp add: run_def)
 
 subsubsection {* Monad plus operator *}
 
 constdefs
   mplus :: "'a maybe \<rightarrow> 'a maybe \<rightarrow> 'a maybe"
-  "mplus \<equiv> \<Lambda> m1 m2. sscase\<cdot>(\<Lambda> x. m2)\<cdot>(fup\<cdot>return)\<cdot>m1"
+  "mplus \<equiv> \<Lambda> m1 m2. case m1 of fail \<Rightarrow> m2 | return\<cdot>x \<Rightarrow> m1"
 
 syntax "+++" :: "['a maybe, 'a maybe] \<Rightarrow> 'a maybe" (infixr "+++" 65)
 translations "m1 +++ m2" == "mplus\<cdot>m1\<cdot>m2"
@@ -119,10 +116,10 @@
 by (simp add: mplus_def)
 
 lemma mplus_fail [simp]: "fail +++ m = m"
-by (simp add: mplus_def fail_def)
+by (simp add: mplus_def)
 
 lemma mplus_return [simp]: "return\<cdot>x +++ m = return\<cdot>x"
-by (simp add: mplus_def return_def)
+by (simp add: mplus_def)
 
 lemma mplus_fail2 [simp]: "m +++ fail = m"
 by (rule_tac p=m in maybeE, simp_all)
@@ -254,7 +251,8 @@
 
 constdefs
   cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat"
-  "cpair_pat p1 p2 \<equiv> \<Lambda>\<langle>x, y\<rangle>. do a <- p1\<cdot>x; b <- p2\<cdot>y; return\<cdot>\<langle>a, b\<rangle>"
+  "cpair_pat p1 p2 \<equiv> \<Lambda>\<langle>x, y\<rangle>.
+    bind\<cdot>(p1\<cdot>x)\<cdot>(\<Lambda> a. bind\<cdot>(p2\<cdot>y)\<cdot>(\<Lambda> b. return\<cdot>\<langle>a, b\<rangle>))"
 
   spair_pat ::
   "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a::pcpo \<otimes> 'b::pcpo, 'c \<times> 'd) pat"
@@ -389,7 +387,7 @@
   "wild_pat \<equiv> \<Lambda> x. return\<cdot>()"
 
   as_pat :: "('a \<rightarrow> 'b maybe) \<Rightarrow> 'a \<rightarrow> ('a \<times> 'b) maybe"
-  "as_pat p \<equiv> \<Lambda> x. do a <- p\<cdot>x; return\<cdot>\<langle>x, a\<rangle>"
+  "as_pat p \<equiv> \<Lambda> x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> a. return\<cdot>\<langle>x, a\<rangle>)"
 
   lazy_pat :: "('a \<rightarrow> 'b::pcpo maybe) \<Rightarrow> ('a \<rightarrow> 'b maybe)"
   "lazy_pat p \<equiv> \<Lambda> x. return\<cdot>(run\<cdot>(p\<cdot>x))"

--- a/src/HOLCF/domain/library.ML	Thu Feb 16 23:40:32 2006 +0100
+++ b/src/HOLCF/domain/library.ML	Fri Feb 17 01:46:38 2006 +0100
@@ -207,6 +207,7 @@
 |   mk_stuple ts = foldr1 spair ts;
 fun mk_ctupleT [] = HOLogic.unitT   (* used in match_defs *)
 |   mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts;
+fun mk_maybeT T = Type ("Fixrec.maybe",[T]);
 fun cpair_pat (p1,p2) = %%:cpair_patN $ p1 $ p2;
 fun lift_defined f = lift (fn x => defined (f x));
 fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);

--- a/src/HOLCF/domain/syntax.ML	Thu Feb 16 23:40:32 2006 +0100
+++ b/src/HOLCF/domain/syntax.ML	Fri Feb 17 01:46:38 2006 +0100
@@ -47,13 +47,13 @@
 			(* strictly speaking, these constants have one argument,
 			   but the mixfix (without arguments) is introduced only
 			   to generate parse rules for non-alphanumeric names*)
-  fun mat (con ,s,args) = (mat_name_ con, dtype->>mk_ssumT(oneT,mk_uT(mk_ctupleT(map third args))),
+  fun mat (con ,s,args) = (mat_name_ con, dtype->>mk_maybeT(mk_ctupleT(map third args)),
 			   Mixfix(escape ("match_" ^ con), [], Syntax.max_pri));
   fun sel1 (_,sel,typ)  = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel;
   fun sel (_   ,_,args) = List.mapPartial sel1 args;
   fun freetvar s n      = let val tvar = mk_TFree (s ^ string_of_int n) in
 			  if tvar mem typevars then freetvar ("t"^s) n else tvar end;
-  fun mk_patT (a,b)     = a ->> mk_ssumT (oneT, mk_uT b);
+  fun mk_patT (a,b)     = a ->> mk_maybeT b;
   fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n);
   fun pat (con ,s,args) = (pat_name_ con, (mapn pat_arg_typ 1 args) --->
 			   mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))),