--- a/src/HOLCF/Fixrec.thy Sun Nov 06 00:35:24 2005 +0100
+++ b/src/HOLCF/Fixrec.thy Sun Nov 06 01:21:37 2005 +0100
@@ -31,12 +31,14 @@
apply (rule_tac p=y in upE, simp, simp)
done
-subsection {* Monadic bind operator *}
+subsubsection {* Monadic bind operator *}
-consts
- bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe" (infixl ">>=" 50)
-defs
- bind_def: "bind \<equiv> \<Lambda> m f. sscase\<cdot>sinl\<cdot>(fup\<cdot>f)\<cdot>m"
+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
@@ -71,7 +73,7 @@
"(do b <- (do a <- m; k\<cdot>a); h\<cdot>b) = (do a <- m; b <- k\<cdot>a; h\<cdot>b)"
by (rule_tac p=m in maybeE, simp_all)
-subsection {* Run operator *}
+subsubsection {* Run operator *}
constdefs
run:: "'a::pcpo maybe \<rightarrow> 'a"
@@ -88,12 +90,14 @@
lemma run_return [simp]: "run\<cdot>(return\<cdot>x) = x"
by (simp add: run_def return_def)
-subsection {* Monad plus operator *}
+subsubsection {* Monad plus operator *}
-consts
- mplus :: "'a maybe \<rightarrow> 'a maybe \<rightarrow> 'a maybe" (infixr "+++" 65)
-defs
- mplus_def: "mplus \<equiv> \<Lambda> m1 m2. sscase\<cdot>(\<Lambda> x. m2)\<cdot>(fup\<cdot>return)\<cdot>m1"
+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"
+
+syntax "+++" :: "['a maybe, 'a maybe] \<Rightarrow> 'a maybe" (infixr "+++" 65)
+translations "m1 +++ m2" == "mplus\<cdot>m1\<cdot>m2"
text {* rewrite rules for mplus *}
@@ -112,6 +116,193 @@
lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)"
by (rule_tac p=x in maybeE, simp_all)
+subsubsection {* Fatbar combinator *}
+
+constdefs
+ fatbar :: "('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe)"
+ "fatbar \<equiv> \<Lambda> a b x. a\<cdot>x +++ b\<cdot>x"
+
+syntax
+ "\<parallel>" :: "['a \<rightarrow> 'b maybe, 'a \<rightarrow> 'b maybe] \<Rightarrow> 'a \<rightarrow> 'b maybe" (infixr "\<parallel>" 60)
+translations
+ "m1 \<parallel> m2" == "fatbar\<cdot>m1\<cdot>m2"
+
+lemma fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> (m \<parallel> ms)\<cdot>x = \<bottom>"
+by (simp add: fatbar_def)
+
+lemma fatbar2: "m\<cdot>x = fail \<Longrightarrow> (m \<parallel> ms)\<cdot>x = ms\<cdot>x"
+by (simp add: fatbar_def)
+
+lemma fatbar3: "m\<cdot>x = return\<cdot>y \<Longrightarrow> (m \<parallel> ms)\<cdot>x = return\<cdot>y"
+by (simp add: fatbar_def)
+
+lemmas fatbar_simps = fatbar1 fatbar2 fatbar3
+
+subsection {* Pattern combinators *}
+
+types ('a,'b,'c) pattern = "'b \<rightarrow> 'a \<rightarrow> 'c maybe"
+
+constdefs
+ wild_pat :: "('a, 'b, 'b) pattern"
+ "wild_pat \<equiv> \<Lambda> r a. return\<cdot>r"
+
+ var_pat :: "('a, 'a \<rightarrow> 'b, 'b) pattern"
+ "var_pat \<equiv> \<Lambda> r a. return\<cdot>(r\<cdot>a)"
+
+ as_pat :: "('a, 'b, 'c) pattern \<Rightarrow> ('a, 'a \<rightarrow> 'b, 'c) pattern"
+ "as_pat p \<equiv> \<Lambda> r a. p\<cdot>(r\<cdot>a)\<cdot>a"
+
+lemma wild_pat [simp]: "wild_pat\<cdot>r\<cdot>a = return\<cdot>r"
+by (simp add: wild_pat_def)
+
+lemma var_pat [simp]: "var_pat\<cdot>r\<cdot>a = return\<cdot>(r\<cdot>a)"
+by (simp add: var_pat_def)
+
+lemma as_pat [simp]: "as_pat p\<cdot>r\<cdot>a = p\<cdot>(r\<cdot>a)\<cdot>a"
+by (simp add: as_pat_def)
+
+subsection {* Case syntax *}
+
+nonterminals
+ Case_syn Cases_syn
+
+syntax
+ "_Case_syntax":: "['a, Cases_syn] => 'b" ("(Case _ of/ _)" 10)
+ "_Case1" :: "['a, 'b] => Case_syn" ("(2_ =>/ _)" 10)
+ "" :: "Case_syn => Cases_syn" ("_")
+ "_Case2" :: "[Case_syn, Cases_syn] => Cases_syn" ("_/ | _")
+ "_as_pattern" :: "[idt, 'a] \<Rightarrow> 'a" (infixr "as" 10)
+
+syntax (xsymbols)
+ "_Case1" :: "['a, 'b] => Case_syn" ("(2_ \<Rightarrow>/ _)" 10)
+
+syntax
+ "_match" :: "'a \<Rightarrow> Case_syn" (* or Cases_syn *)
+ "_as" :: "[pttrn, Case_syn] \<Rightarrow> Case_syn"
+ "_matches" :: "['a, Case_syn, 'a list] \<Rightarrow> Case_syn"
+ "_cons" :: "['a, 'a list] \<Rightarrow> 'a list"
+ "_nil" :: "'a list"
+
+translations
+ "_Case_syntax x (_match m)" == "run\<cdot>(m\<cdot>x)"
+ "_Case2 (_match c) (_match cs)" == "_match (c \<parallel> cs)"
+ "_Case1 dummy_pattern r" == "_match (wild_pat\<cdot>r)"
+ "_as x (_match (p\<cdot>t))" == "_match ((as_pat p)\<cdot>(\<Lambda> x. t))"
+ "_Case1 (_as_pattern x e) r" == "_as x (_Case1 e r)"
+ "_Case1 x t" == "_match (var_pat\<cdot>(\<Lambda> x. t))"
+ "_Case1 (f\<cdot>e) r" == "_matches f (_Case1 e r) _nil"
+ "_matches (f\<cdot>e) (_match (p\<cdot>r)) ps" == "_matches f (_Case1 e r) (_cons p ps)"
+
+lemma run_fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = \<bottom>"
+by (simp add: fatbar_def)
+
+lemma run_fatbar2: "m\<cdot>x = fail \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = run\<cdot>(ms\<cdot>x)"
+by (simp add: fatbar_def)
+
+lemma run_fatbar3: "m\<cdot>x = return\<cdot>y \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = y"
+by (simp add: fatbar_def)
+
+lemmas run_fatbar_simps [simp] = run_fatbar1 run_fatbar2 run_fatbar3
+
+subsection {* Pattern combinators for built-in types *}
+
+constdefs
+ cpair_pat :: "_"
+ "cpair_pat p1 p2 \<equiv> \<Lambda> r1 \<langle>x1,x2\<rangle>. bind\<cdot>(p1\<cdot>r1\<cdot>x1)\<cdot>(\<Lambda> r2. p2\<cdot>r2\<cdot>x2)"
+
+ spair_pat :: "_"
+ "spair_pat p1 p2 \<equiv> \<Lambda> r (:x,y:). cpair_pat p1 p2\<cdot>r\<cdot>\<langle>x,y\<rangle>"
+
+ sinl_pat :: "_"
+ "sinl_pat p \<equiv> \<Lambda> r a. case a of sinl\<cdot>x \<Rightarrow> p\<cdot>r\<cdot>x | sinr\<cdot>y \<Rightarrow> fail"
+
+ sinr_pat :: "_"
+ "sinr_pat p \<equiv> \<Lambda> r a. case a of sinl\<cdot>x \<Rightarrow> fail | sinr\<cdot>y \<Rightarrow> p\<cdot>r\<cdot>y"
+
+ up_pat :: "_"
+ "up_pat p \<equiv> \<Lambda> r a. case a of up\<cdot>x \<Rightarrow> p\<cdot>r\<cdot>x"
+
+ Def_pat :: "'a::type \<Rightarrow> ('a lift, 'b, 'b) pattern"
+ "Def_pat x \<equiv> \<Lambda> r. FLIFT y. if x = y then return\<cdot>r else fail"
+
+ ONE_pat :: "_"
+ "ONE_pat \<equiv> \<Lambda> r ONE. return\<cdot>r"
+
+ TT_pat :: "(tr, _, _) pattern"
+ "TT_pat \<equiv> \<Lambda> r b. If b then return\<cdot>r else fail fi"
+
+ FF_pat :: "(tr, _, _) pattern"
+ "FF_pat \<equiv> \<Lambda> r b. If b then fail else return\<cdot>r fi"
+
+translations
+ "_matches cpair (_match (p1\<cdot>r)) (_cons p2 _nil)"
+ == "_match ((cpair_pat p1 p2)\<cdot>r)"
+
+ "_matches spair (_match (p1\<cdot>r)) (_cons p2 _nil)"
+ == "_match ((spair_pat p1 p2)\<cdot>r)"
+
+translations
+ "_matches sinl (_match (p1\<cdot>r)) _nil" == "_match ((sinl_pat p1)\<cdot>r)"
+ "_matches sinr (_match (p1\<cdot>r)) _nil" == "_match ((sinr_pat p1)\<cdot>r)"
+ "_matches up (_match (p1\<cdot>r)) _nil" == "_match ((up_pat p1)\<cdot>r)"
+
+translations
+ "_Case1 (Def x) r" == "_match (Def_pat x\<cdot>r)"
+ "_Case1 ONE r" == "_match (ONE_pat\<cdot>r)"
+ "_Case1 TT r" == "_match (TT_pat\<cdot>r)"
+ "_Case1 FF r" == "_match (FF_pat\<cdot>r)"
+
+lemma cpair_pat_simps [simp]:
+ "p1\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> cpair_pat p1 p2\<cdot>r\<cdot><x,y> = \<bottom>"
+ "p1\<cdot>r\<cdot>x = fail \<Longrightarrow> cpair_pat p1 p2\<cdot>r\<cdot><x,y> = fail"
+ "p1\<cdot>r\<cdot>x = return\<cdot>r' \<Longrightarrow> cpair_pat p1 p2\<cdot>r\<cdot><x,y> = p2\<cdot>r'\<cdot>y"
+by (simp_all add: cpair_pat_def)
+
+lemma spair_pat_simps [simp]:
+ "spair_pat p1 p2\<cdot>r\<cdot>\<bottom> = \<bottom>"
+ "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> spair_pat p1 p2\<cdot>r\<cdot>(:x, y:) = cpair_pat p1 p2\<cdot>r\<cdot>\<langle>x, y\<rangle>"
+by (simp_all add: spair_pat_def)
+
+lemma sinl_pat_simps [simp]:
+ "sinl_pat p\<cdot>r\<cdot>\<bottom> = \<bottom>"
+ "x \<noteq> \<bottom> \<Longrightarrow> sinl_pat p\<cdot>r\<cdot>(sinl\<cdot>x) = p\<cdot>r\<cdot>x"
+ "x \<noteq> \<bottom> \<Longrightarrow> sinl_pat p\<cdot>r\<cdot>(sinr\<cdot>x) = fail"
+by (simp_all add: sinl_pat_def)
+
+lemma sinr_pat_simps [simp]:
+ "sinr_pat p\<cdot>r\<cdot>\<bottom> = \<bottom>"
+ "x \<noteq> \<bottom> \<Longrightarrow> sinr_pat p\<cdot>r\<cdot>(sinl\<cdot>x) = fail"
+ "x \<noteq> \<bottom> \<Longrightarrow> sinr_pat p\<cdot>r\<cdot>(sinr\<cdot>x) = p\<cdot>r\<cdot>x"
+by (simp_all add: sinr_pat_def)
+
+lemma up_pat_simps [simp]:
+ "up_pat p\<cdot>r\<cdot>\<bottom> = \<bottom>"
+ "up_pat p\<cdot>r\<cdot>(up\<cdot>x) = p\<cdot>r\<cdot>x"
+by (simp_all add: up_pat_def)
+
+lemma Def_pat_simps [simp]:
+ "Def_pat x\<cdot>r\<cdot>\<bottom> = \<bottom>"
+ "Def_pat x\<cdot>r\<cdot>(Def x) = return\<cdot>r"
+ "x \<noteq> y \<Longrightarrow> Def_pat x\<cdot>r\<cdot>(Def y) = fail"
+by (simp_all add: Def_pat_def)
+
+lemma ONE_pat_simps [simp]:
+ "ONE_pat\<cdot>r\<cdot>\<bottom> = \<bottom>"
+ "ONE_pat\<cdot>r\<cdot>ONE = return\<cdot>r"
+by (simp_all add: ONE_pat_def)
+
+lemma TT_pat_simps [simp]:
+ "TT_pat\<cdot>r\<cdot>\<bottom> = \<bottom>"
+ "TT_pat\<cdot>r\<cdot>TT = return\<cdot>r"
+ "TT_pat\<cdot>r\<cdot>FF = fail"
+by (simp_all add: TT_pat_def)
+
+lemma FF_pat_simps [simp]:
+ "FF_pat\<cdot>r\<cdot>\<bottom> = \<bottom>"
+ "FF_pat\<cdot>r\<cdot>TT = fail"
+ "FF_pat\<cdot>r\<cdot>FF = return\<cdot>r"
+by (simp_all add: FF_pat_def)
+
subsection {* Match functions for built-in types *}
defaultsort pcpo