# HG changeset patch
# User huffman
# Date 1133308875 -3600
# Node ID 4eaa654c92f2e9ac5034ab25d2a2c24b9e275efa
# Parent  9ca223aedb1e661405416c78fb0d1fe88156b435
reimplement Case expression pattern matching to support lazy patterns

diff -r 9ca223aedb1e -r 4eaa654c92f2 src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Wed Nov 30 00:59:04 2005 +0100
+++ b/src/HOLCF/Fixrec.thy	Wed Nov 30 01:01:15 2005 +0100
@@ -31,6 +31,20 @@
 apply (rule_tac p=y in upE, simp, simp)
 done
 
+lemma return_defined [simp]: "return\<cdot>x \<noteq> \<bottom>"
+by (simp add: return_def)
+
+lemma fail_defined [simp]: "fail \<noteq> \<bottom>"
+by (simp add: fail_def)
+
+lemma return_eq [simp]: "(return\<cdot>x = return\<cdot>y) = (x = y)"
+by (simp add: return_def)
+
+lemma return_neq_fail [simp]:
+  "return\<cdot>x \<noteq> fail" "fail \<noteq> return\<cdot>x"
+by (simp_all add: return_def fail_def)
+
+
 subsubsection {* Monadic bind operator *}
 
 constdefs
@@ -149,22 +163,21 @@
 
 lemmas run_fatbar_simps [simp] = run_fatbar1 run_fatbar2 run_fatbar3
 
-subsection {* Pattern combinators *}
-
-types ('a,'b,'c) pat = "'b \<rightarrow> 'a \<rightarrow> 'c maybe"
+subsection {* Case branch combinator *}
 
 constdefs
-  wild_pat :: "('a, 'b, 'b) pat"
-  "wild_pat \<equiv> \<Lambda> r a. return\<cdot>r"
-
-  var_pat :: "('a, 'a \<rightarrow> 'b, 'b) pat"
-  "var_pat \<equiv> \<Lambda> r a. return\<cdot>(r\<cdot>a)"
+  branch :: "('a \<rightarrow> 'b maybe) \<Rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'c maybe)"
+  "branch p \<equiv> \<Lambda> r x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> y. return\<cdot>(r\<cdot>y))"
 
-lemma wild_pat [simp]: "wild_pat\<cdot>r\<cdot>a = return\<cdot>r"
-by (simp add: wild_pat_def)
+lemma branch_rews:
+  "p\<cdot>x = \<bottom> \<Longrightarrow> branch p\<cdot>r\<cdot>x = \<bottom>"
+  "p\<cdot>x = fail \<Longrightarrow> branch p\<cdot>r\<cdot>x = fail"
+  "p\<cdot>x = return\<cdot>y \<Longrightarrow> branch p\<cdot>r\<cdot>x = return\<cdot>(r\<cdot>y)"
+by (simp_all add: branch_def)
 
-lemma var_pat [simp]: "var_pat\<cdot>r\<cdot>a = return\<cdot>(r\<cdot>a)"
-by (simp add: var_pat_def)
+lemma branch_return [simp]: "branch return\<cdot>r\<cdot>x = return\<cdot>(r\<cdot>x)"
+by (simp add: branch_def)
+
 
 subsection {* Case syntax *}
 
@@ -180,198 +193,242 @@
 syntax (xsymbols)
   "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
 
-text {* Intermediate tags for parsing/printing *}
-syntax
-  "_pat" :: "'a"
-  "_var" :: "'a"
-  "_match" :: "'a"
+translations
+  "_Case_syntax x ms" == "run\<cdot>(ms\<cdot>x)"
+  "_Case2 m ms" == "m \<parallel> ms"
 
 text {* Parsing Case expressions *}
 
+syntax
+  "_pat" :: "'a"
+  "_var" :: "'a"
+
 translations
-  "_Case_syntax x cs" => "run\<cdot>(cs\<cdot>x)"
-  "_Case2 c cs" => "fatbar\<cdot>c\<cdot>cs"
-  "_Case1 p r" => "_match (_var p) r"
-  "_var _" => "wild_pat"
+  "_Case1 p r" => "branch (_pat p)\<cdot>(_var p r)"
+  "_var (_args x y) r" => "csplit\<cdot>(_var x (_var y r))"
+  "_var () r" => "unit_when\<cdot>r"
 
 parse_translation {*
-  let
-    fun capp (t,u) = Syntax.const "Rep_CFun" $ t $ u;
-    fun cabs (x,t) = (snd (mk_binder_tr ("_cabs", "Abs_CFun"))) [x,t];
-
-    fun get_vars (Const ("_var",_) $ x) = [x]
-    |   get_vars (t $ u) = get_vars t @ get_vars u
-    |   get_vars t = [];
-
-    fun rem_vars (Const ("_var",_) $ x) = Syntax.const "var_pat"
-    |   rem_vars (t $ u) = rem_vars t $ rem_vars u
-    |   rem_vars t = t;
-
-    fun match_tr [pat, rhs] =
-          capp (rem_vars pat, foldr cabs rhs (get_vars pat))
-    |   match_tr ts = raise TERM ("match_tr", ts);
-
-  in [("_match", match_tr)] end;
+(* rewrites (_pat x) => (return) *)
+(* rewrites (_var x t) => (Abs_CFun (%x. t)) *)
+  [("_pat", K (Syntax.const "return")),
+   mk_binder_tr ("_var", "Abs_CFun")];
 *}
 
 text {* Printing Case expressions *}
 
-translations
-  "_" <= "_pat wild_pat"
-  "x" <= "_pat (_var x)"
+syntax
+  "_match" :: "'a"
 
 print_translation {*
   let
-    fun dest_cabs (Const ("Abs_CFun",_) $ t) =
-          let val abs = case t of Abs abs => abs
-                  | _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0);
-          in atomic_abs_tr' abs end
-    |   dest_cabs _ = raise Match; (* too few vars: abort translation *)
-
-    fun put_vars (Const ("var_pat",_), rhs) =
-          let val (x, rhs') = dest_cabs rhs;
-          in (Syntax.const "_var" $ x, rhs') end
-    |   put_vars (t $ u, rhs) =
+    fun dest_LAM (Const ("Rep_CFun",_) $ Const ("unit_when",_) $ t) =
+          (Syntax.const "Unity", t)
+    |   dest_LAM (Const ("Rep_CFun",_) $ Const ("csplit",_) $ t) =
+          let
+            val (v1, t1) = dest_LAM t;
+            val (v2, t2) = dest_LAM t1;
+          in (Syntax.const "_args" $ v1 $ v2, t2) end 
+    |   dest_LAM (Const ("Abs_CFun",_) $ t) =
           let
-            val (t', rhs') = put_vars (t,rhs);
-            val (u', rhs'') = put_vars (u,rhs');
-          in (t' $ u', rhs'') end
-    |   put_vars (t, rhs) = (t, rhs);
-
-    fun Case1_tr' (_ $ pat $ rhs) = let
-          val (pat', rhs') = put_vars (pat, rhs);
-        in Syntax.const "_Case1" $ (Syntax.const "_pat" $ pat') $ rhs' end;
+            val abs = case t of Abs abs => abs
+                | _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0);
+            val (x, t') = atomic_abs_tr' abs;
+          in (Syntax.const "_var" $ x, t') end
+    |   dest_LAM _ = raise Match; (* too few vars: abort translation *)
 
-    fun Case2_tr' (_ $ (_ $ Const ("fatbar",_) $ m) $ ms) =
-          Syntax.const "_Case2" $ Case1_tr' m $ Case2_tr' ms
-    |   Case2_tr' t = Case1_tr' t;
+    fun Case1_tr' [Const("branch",_) $ p, r] =
+          let val (v, t) = dest_LAM r;
+          in Syntax.const "_Case1" $ (Syntax.const "_match" $ p $ v) $ t end;
 
-    fun Case_syntax_tr' [Const ("run",_), _ $ ms $ x] =
-          Syntax.const "_Case_syntax" $ x $ Case2_tr' ms;
-
-  in [("Rep_CFun", Case_syntax_tr')] end;
+  in [("Rep_CFun", Case1_tr')] end;
 *}
 
-subsection {* Pattern combinators for built-in types *}
+translations
+  "x" <= "_match return (_var x)"
+
+
+subsection {* Pattern combinators for data constructors *}
+
+types ('a, 'b) pat = "'a \<rightarrow> 'b maybe"
 
 constdefs
-  cpair_pat :: "('a, _, _) pat \<Rightarrow> ('b, _, _) pat \<Rightarrow> ('a \<times> 'b, _, _) 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)"
+  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>"
 
-  spair_pat :: "(_, _, _) pat \<Rightarrow> (_, _, _) pat \<Rightarrow> (_, _, _) pat"
-  "spair_pat p1 p2 \<equiv> \<Lambda> r (:x,y:). cpair_pat p1 p2\<cdot>r\<cdot>\<langle>x,y\<rangle>"
+  spair_pat ::
+  "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a::pcpo \<otimes> 'b::pcpo, 'c \<times> 'd) pat"
+  "spair_pat p1 p2 \<equiv> \<Lambda>(:x, y:). cpair_pat p1 p2\<cdot>\<langle>x, y\<rangle>"
 
-  sinl_pat :: "(_, _, _) pat \<Rightarrow> (_, _, _) 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"
+  sinl_pat :: "('a, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat"
+  "sinl_pat p \<equiv> sscase\<cdot>p\<cdot>(\<Lambda> x. fail)"
 
-  sinr_pat :: "(_, _, _) pat \<Rightarrow> (_, _, _) 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"
+  sinr_pat :: "('b, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat"
+  "sinr_pat p \<equiv> sscase\<cdot>(\<Lambda> x. fail)\<cdot>p"
+
+  up_pat :: "('a, 'b) pat \<Rightarrow> ('a u, 'b) pat"
+  "up_pat p \<equiv> fup\<cdot>p"
 
-  up_pat :: "('a, _, _) pat \<Rightarrow> ('a u, _, _) pat"
-  "up_pat p \<equiv> \<Lambda> r a. case a of up\<cdot>x \<Rightarrow> p\<cdot>r\<cdot>x"
+  TT_pat :: "(tr, unit) pat"
+  "TT_pat \<equiv> \<Lambda> b. If b then return\<cdot>() else fail fi"
 
-  Def_pat :: "'a::type \<Rightarrow> ('a lift, _, _) pat"
-  "Def_pat x \<equiv> \<Lambda> r. FLIFT y. if x = y then return\<cdot>r else fail"
+  FF_pat :: "(tr, unit) pat"
+  "FF_pat \<equiv> \<Lambda> b. If b then fail else return\<cdot>() fi"
 
-  ONE_pat :: "(one, _, _) pat"
-  "ONE_pat \<equiv> \<Lambda> r ONE. return\<cdot>r"
-
-  TT_pat :: "(tr, _, _) pat"
-  "TT_pat \<equiv> \<Lambda> r b. If b then return\<cdot>r else fail fi"
-
-  FF_pat :: "(tr, _, _) pat"
-  "FF_pat \<equiv> \<Lambda> r b. If b then fail else return\<cdot>r fi"
+  ONE_pat :: "(one, unit) pat"
+  "ONE_pat \<equiv> \<Lambda> ONE. return\<cdot>()"
 
-text {* Parse translations *}
+text {* Parse translations (patterns) *}
 translations
-  "_var (cpair\<cdot>p1\<cdot>p2)" => "cpair_pat (_var p1) (_var p2)"
-  "_var (spair\<cdot>p1\<cdot>p2)" => "spair_pat (_var p1) (_var p2)"
-  "_var (sinl\<cdot>p1)"     => "sinl_pat (_var p1)"
-  "_var (sinr\<cdot>p1)"     => "sinr_pat (_var p1)"
-  "_var (up\<cdot>p1)"       => "up_pat (_var p1)"
-  "_var (Def x)"       => "Def_pat x"
-  "_var ONE"           => "ONE_pat"
-  "_var TT"            => "TT_pat"
-  "_var FF"            => "FF_pat"
+  "_pat (cpair\<cdot>x\<cdot>y)" => "cpair_pat (_pat x) (_pat y)"
+  "_pat (spair\<cdot>x\<cdot>y)" => "spair_pat (_pat x) (_pat y)"
+  "_pat (sinl\<cdot>x)" => "sinl_pat (_pat x)"
+  "_pat (sinr\<cdot>x)" => "sinr_pat (_pat x)"
+  "_pat (up\<cdot>x)" => "up_pat (_pat x)"
+  "_pat TT" => "TT_pat"
+  "_pat FF" => "FF_pat"
+  "_pat ONE" => "ONE_pat"
+
+text {* Parse translations (variables) *}
+translations
+  "_var (cpair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
+  "_var (spair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
+  "_var (sinl\<cdot>x) r" => "_var x r"
+  "_var (sinr\<cdot>x) r" => "_var x r"
+  "_var (up\<cdot>x) r" => "_var x r"
+  "_var TT r" => "_var () r"
+  "_var FF r" => "_var () r"
+  "_var ONE r" => "_var () r"
 
 text {* Print translations *}
 translations
-  "cpair\<cdot>(_pat p1)\<cdot>(_pat p2)" <= "_pat (cpair_pat p1 p2)"
-  "spair\<cdot>(_pat p1)\<cdot>(_pat p2)" <= "_pat (spair_pat p1 p2)"
-  "sinl\<cdot>(_pat p1)"            <= "_pat (sinl_pat p1)"
-  "sinr\<cdot>(_pat p1)"            <= "_pat (sinr_pat p1)"
-  "up\<cdot>(_pat p1)"              <= "_pat (up_pat p1)"
-  "Def x"                     <= "_pat (Def_pat x)"
-  "TT"                        <= "_pat (TT_pat)"
-  "FF"                        <= "_pat (FF_pat)"
+  "cpair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
+      <= "_match (cpair_pat p1 p2) (_args v1 v2)"
+  "spair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
+      <= "_match (spair_pat p1 p2) (_args v1 v2)"
+  "sinl\<cdot>(_match p1 v1)" <= "_match (sinl_pat p1) v1"
+  "sinr\<cdot>(_match p1 v1)" <= "_match (sinr_pat p1) v1"
+  "up\<cdot>(_match p1 v1)" <= "_match (up_pat p1) v1"
+  "TT" <= "_match TT_pat ()"
+  "FF" <= "_match FF_pat ()"
+  "ONE" <= "_match ONE_pat ()"
+
+lemma cpair_pat1:
+  "branch p\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = \<bottom>"
+apply (simp add: branch_def cpair_pat_def)
+apply (rule_tac p="p\<cdot>x" in maybeE, simp_all)
+done
 
-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 cpair_pat2:
+  "branch p\<cdot>r\<cdot>x = fail \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = fail"
+apply (simp add: branch_def cpair_pat_def)
+apply (rule_tac p="p\<cdot>x" in maybeE, simp_all)
+done
 
-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 cpair_pat3:
+  "branch p\<cdot>r\<cdot>x = return\<cdot>s \<Longrightarrow>
+   branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = branch q\<cdot>s\<cdot>y"
+apply (simp add: branch_def cpair_pat_def)
+apply (rule_tac p="p\<cdot>x" in maybeE, simp_all)
+apply (rule_tac p="q\<cdot>y" in maybeE, simp_all)
+done
 
-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)
+lemmas cpair_pat [simp] =
+  cpair_pat1 cpair_pat2 cpair_pat3
 
-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 spair_pat [simp]:
+  "branch (spair_pat p1 p2)\<cdot>r\<cdot>\<bottom> = \<bottom>"
+  "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk>
+     \<Longrightarrow> branch (spair_pat p1 p2)\<cdot>r\<cdot>(:x, y:) =
+         branch (cpair_pat p1 p2)\<cdot>r\<cdot>\<langle>x, y\<rangle>"
+by (simp_all add: branch_def spair_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 sinl_pat [simp]:
+  "branch (sinl_pat p)\<cdot>r\<cdot>\<bottom> = \<bottom>"
+  "x \<noteq> \<bottom> \<Longrightarrow> branch (sinl_pat p)\<cdot>r\<cdot>(sinl\<cdot>x) = branch p\<cdot>r\<cdot>x"
+  "y \<noteq> \<bottom> \<Longrightarrow> branch (sinl_pat p)\<cdot>r\<cdot>(sinr\<cdot>y) = fail"
+by (simp_all add: branch_def sinl_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 sinr_pat [simp]:
+  "branch (sinr_pat p)\<cdot>r\<cdot>\<bottom> = \<bottom>"
+  "x \<noteq> \<bottom> \<Longrightarrow> branch (sinr_pat p)\<cdot>r\<cdot>(sinl\<cdot>x) = fail"
+  "y \<noteq> \<bottom> \<Longrightarrow> branch (sinr_pat p)\<cdot>r\<cdot>(sinr\<cdot>y) = branch p\<cdot>r\<cdot>y"
+by (simp_all add: branch_def sinr_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 up_pat [simp]:
+  "branch (up_pat p)\<cdot>r\<cdot>\<bottom> = \<bottom>"
+  "branch (up_pat p)\<cdot>r\<cdot>(up\<cdot>x) = branch p\<cdot>r\<cdot>x"
+by (simp_all add: branch_def up_pat_def)
+
+lemma TT_pat [simp]:
+  "branch TT_pat\<cdot>(unit_when\<cdot>r)\<cdot>\<bottom> = \<bottom>"
+  "branch TT_pat\<cdot>(unit_when\<cdot>r)\<cdot>TT = return\<cdot>r"
+  "branch TT_pat\<cdot>(unit_when\<cdot>r)\<cdot>FF = fail"
+by (simp_all add: branch_def TT_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 [simp]:
+  "branch FF_pat\<cdot>(unit_when\<cdot>r)\<cdot>\<bottom> = \<bottom>"
+  "branch FF_pat\<cdot>(unit_when\<cdot>r)\<cdot>TT = fail"
+  "branch FF_pat\<cdot>(unit_when\<cdot>r)\<cdot>FF = return\<cdot>r"
+by (simp_all add: branch_def FF_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)
+lemma ONE_pat [simp]:
+  "branch ONE_pat\<cdot>(unit_when\<cdot>r)\<cdot>\<bottom> = \<bottom>"
+  "branch ONE_pat\<cdot>(unit_when\<cdot>r)\<cdot>ONE = return\<cdot>r"
+by (simp_all add: branch_def ONE_pat_def)
 
-subsection {* As-patterns *}
+
+subsection {* Wildcards, as-patterns, and lazy patterns *}
 
 syntax
-  "_as_pattern" :: "['a, 'a] \<Rightarrow> 'a" (* infixr "as" 10 *)
-  (* TODO: choose a non-ambiguous syntax for as-patterns *)
+  "_as_pat" :: "[idt, 'a] \<Rightarrow> 'a" (infixr "\<as>" 10)
+  "_lazy_pat" :: "'a \<Rightarrow> 'a" ("\<lazy> _" [1000] 1000)
 
 constdefs
-  as_pat :: "('a,'b,'c) pat \<Rightarrow> ('a,'c,'d) pat \<Rightarrow> ('a,'b,'d) pat"
-  "as_pat p1 p2 \<equiv> \<Lambda> r a. cpair_pat p1 p2\<cdot>r\<cdot>\<langle>a, a\<rangle>"
+  wild_pat :: "'a \<rightarrow> unit maybe"
+  "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>"
 
+  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))"
+
+text {* Parse translations (patterns) *}
+translations
+  "_pat _" => "wild_pat"
+  "_pat (_as_pat x y)" => "as_pat (_pat y)"
+  "_pat (_lazy_pat x)" => "lazy_pat (_pat x)"
+
+text {* Parse translations (variables) *}
 translations
-  "_var (_as_pattern p1 p2)" => "as_pat (_var p1) (_var p2)"
-  "_as_pattern (_pat p1) (_pat p2)" <= "_pat (as_pat p1 p2)"
+  "_var _ r" => "_var () r"
+  "_var (_as_pat x y) r" => "_var (_args x y) r"
+  "_var (_lazy_pat x) r" => "_var x r"
+
+text {* Print translations *}
+translations
+  "_" <= "_match wild_pat ()"
+  "_as_pat x (_match p v)" <= "_match (as_pat p) (_args (_var x) v)"
+  "_lazy_pat (_match p v)" <= "_match (lazy_pat p) v"
+
+lemma wild_pat [simp]: "branch wild_pat\<cdot>(unit_when\<cdot>r)\<cdot>x = return\<cdot>r"
+by (simp add: branch_def wild_pat_def)
 
-lemma as_pat [simp]: "as_pat p1 p2\<cdot>r\<cdot>a = cpair_pat p1 p2\<cdot>r\<cdot>\<langle>a, a\<rangle>"
-by (simp add: as_pat_def)
+lemma as_pat [simp]:
+  "branch (as_pat p)\<cdot>(csplit\<cdot>r)\<cdot>x = branch p\<cdot>(r\<cdot>x)\<cdot>x"
+apply (simp add: branch_def as_pat_def)
+apply (rule_tac p="p\<cdot>x" in maybeE, simp_all)
+done
+
+lemma lazy_pat [simp]:
+  "branch p\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> branch (lazy_pat p)\<cdot>r\<cdot>x = return\<cdot>(r\<cdot>\<bottom>)"
+  "branch p\<cdot>r\<cdot>x = fail \<Longrightarrow> branch (lazy_pat p)\<cdot>r\<cdot>x = return\<cdot>(r\<cdot>\<bottom>)"
+  "branch p\<cdot>r\<cdot>x = return\<cdot>s \<Longrightarrow> branch (lazy_pat p)\<cdot>r\<cdot>x = return\<cdot>s"
+apply (simp_all add: branch_def lazy_pat_def)
+apply (rule_tac [!] p="p\<cdot>x" in maybeE, simp_all)
+done
+
 
 subsection {* Match functions for built-in types *}
 
@@ -478,6 +535,7 @@
 val cpair_eqD1 = thm "cpair_eqD1";
 val cpair_eqD2 = thm "cpair_eqD2";
 val ssubst_lhs = thm "ssubst_lhs";
+val branch_def = thm "branch_def";
 *}
 
 subsection {* Initializing the fixrec package *}
diff -r 9ca223aedb1e -r 4eaa654c92f2 src/HOLCF/document/root.tex
--- a/src/HOLCF/document/root.tex	Wed Nov 30 00:59:04 2005 +0100
+++ b/src/HOLCF/document/root.tex	Wed Nov 30 01:01:15 2005 +0100
@@ -10,6 +10,8 @@
 \urlstyle{rm}
 \isabellestyle{it}
 \pagestyle{myheadings}
+\newcommand{\isasymas}{\textsf{as}}
+\newcommand{\isasymlazy}{\isamath{\sim}}
 
 \begin{document}
 
diff -r 9ca223aedb1e -r 4eaa654c92f2 src/HOLCF/domain/axioms.ML
--- a/src/HOLCF/domain/axioms.ML	Wed Nov 30 00:59:04 2005 +0100
+++ b/src/HOLCF/domain/axioms.ML	Wed Nov 30 01:01:15 2005 +0100
@@ -79,14 +79,14 @@
           val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
           val xs = map (bound_arg args) args;
           val r = Bound (length args);
-          val rhs = case args of [] => %%:returnN ` r
-                                | _ => foldr1 cpair_pat ps ` r ` mk_ctuple xs;
+          val rhs = case args of [] => %%:returnN ` HOLogic.unit
+                                | _ => foldr1 cpair_pat ps ` mk_ctuple xs;
           fun one_con (con',args') = foldr /\# (if con'=con then rhs else %%:failN) args';
         in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) == 
-               /\ "r" (list_ccomb(%%:(dname^"_when"), map one_con cons)))
+               list_ccomb(%%:(dname^"_when"), map one_con cons))
         end
     in map pdef cons end;
-  
+
   val sel_defs = let
 	fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == 
 		 list_ccomb(%%:(dname^"_when"),map 
diff -r 9ca223aedb1e -r 4eaa654c92f2 src/HOLCF/domain/library.ML
--- a/src/HOLCF/domain/library.ML	Wed Nov 30 00:59:04 2005 +0100
+++ b/src/HOLCF/domain/library.ML	Wed Nov 30 01:01:15 2005 +0100
@@ -130,6 +130,7 @@
 val returnN    = "Fixrec.return";
 val failN      = "Fixrec.fail";
 val cpair_patN = "Fixrec.cpair_pat";
+val branchN    = "Fixrec.branch";
 
 val pcpoN      = "Pcpo.pcpo"
 val pcpoS      = [pcpoN];
diff -r 9ca223aedb1e -r 4eaa654c92f2 src/HOLCF/domain/syntax.ML
--- a/src/HOLCF/domain/syntax.ML	Wed Nov 30 00:59:04 2005 +0100
+++ b/src/HOLCF/domain/syntax.ML	Wed Nov 30 01:01:15 2005 +0100
@@ -53,10 +53,10 @@
   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,c)   = b ->> a ->> mk_ssumT(oneT, mk_uT c);
-  fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n, freetvar "t" (n+1));
+  fun mk_patT (a,b)     = a ->> mk_ssumT (oneT, mk_uT 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, freetvar "t" 1, freetvar "t" (length args + 1)),
+			   mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))),
 			   Mixfix(escape (con ^ "_pat"), [], Syntax.max_pri));
 
 in
@@ -80,16 +80,19 @@
     fun expvar n     = Variable ("e"^(string_of_int n));
     fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
 				     (string_of_int m));
-    fun app s (l,r)   = mk_appl (Constant s) [l,r];
+    fun argvars n args = mapn (argvar n) 1 args;
+    fun app s (l,r)  = mk_appl (Constant s) [l,r];
     val cabs = app "_cabs";
     val capp = app "Rep_CFun";
-    fun con1 n (con,mx,args) = Library.foldl capp (c_ast con mx, mapn (argvar n) 1 args);
+    fun con1 n (con,mx,args) = Library.foldl capp (c_ast con mx, argvars n args);
     fun case1 n (con,mx,args) = app "_case1" (con1 n (con,mx,args), expvar n);
-    fun arg1 n (con,_,args) = foldr cabs (expvar n) (mapn (argvar n) 1 args);
+    fun arg1 n (con,_,args) = foldr cabs (expvar n) (argvars n args);
     fun when1 n m = if n = m then arg1 n else K (Constant "UU");
 
-    fun app_var x = mk_appl (Constant "_var") [x];
+    fun app_var x = mk_appl (Constant "_var") [x, Variable "rhs"];
     fun app_pat x = mk_appl (Constant "_pat") [x];
+    fun args_list [] = Constant "Unity"
+    |   args_list xs = foldr1 (app "_args") xs;
   in
     val case_trans = ParsePrintRule
         (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn case1 1 cons')),
@@ -99,20 +102,29 @@
         (cabs (con1 n (con,mx,args), expvar n),
          Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons'))) 1 cons';
     
-    val pattern_trans = mapn (fn n => fn (con,mx,args) => ParseRule
-          (app_var (Library.foldl capp (c_ast con mx, mapn (argvar n) 1 args)),
-           mk_appl (Constant (pat_name_ con)) (map app_var (mapn (argvar n) 1 args)))) 1 cons';
-    
-    val pattern_trans' = mapn (fn n => fn (con,mx,args) => PrintRule
-          (Library.foldl capp (c_ast con mx, map app_pat (mapn (argvar n) 1 args)),
-           app_pat (mk_appl (Constant (pat_name_ con)) (mapn (argvar n) 1 args)))) 1 cons';
+    val Case_trans = List.concat (map (fn (con,mx,args) =>
+      let
+        val cname = c_ast con mx;
+        val pname = Constant (pat_name_ con);
+        val ns = 1 upto length args;
+        val xs = map (fn n => Variable ("x"^(string_of_int n))) ns;
+        val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
+        val vs = map (fn n => Variable ("v"^(string_of_int n))) ns;
+      in
+        [ParseRule (app_pat (Library.foldl capp (cname, xs)),
+                    mk_appl pname (map app_pat xs)),
+         ParseRule (app_var (Library.foldl capp (cname, xs)),
+                    app_var (args_list xs)),
+         PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)),
+                    app "_match" (mk_appl pname ps, args_list vs))]
+      end) cons');
   end;
 end;
 
 in ([const_rep, const_abs, const_when, const_copy] @ 
      consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @
     [const_take, const_finite],
-    (case_trans::(abscon_trans @ pattern_trans @ pattern_trans')))
+    (case_trans::(abscon_trans @ Case_trans)))
 end; (* let *)
 
 (* ----- putting all the syntax stuff together ------------------------------ *)
diff -r 9ca223aedb1e -r 4eaa654c92f2 src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Wed Nov 30 00:59:04 2005 +0100
+++ b/src/HOLCF/domain/theorems.ML	Wed Nov 30 01:01:15 2005 +0100
@@ -209,18 +209,19 @@
 
 val pat_rews = let
   fun ps args = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
-  fun pat_lhs (con,args) = list_comb (%%:(pat_name con), ps args);
-  fun pat_rhs (con,[]) = %%:returnN ` (%:"rhs")
-  |   pat_rhs (con,args) = (foldr1 cpair_pat (ps args))`(%:"rhs")`(mk_ctuple (map %# args));
-  val pat_stricts = map (fn (con,args) => pg axs_pat_def (mk_trp(
-                             strict(pat_lhs (con,args)`(%:"rhs"))))
-                   [simp_tac (HOLCF_ss addsimps [when_strict]) 1]) cons;
-  val pat_apps = let fun one_pat c (con,args)= pg axs_pat_def
+  fun pat_lhs (con,args) = %%:branchN $ list_comb (%%:(pat_name con), ps args);
+  fun pat_rhs (con,[]) = %%:returnN ` ((%:"rhs") ` HOLogic.unit)
+  |   pat_rhs (con,args) =
+        (%%:branchN $ foldr1 cpair_pat (ps args))`(%:"rhs")`(mk_ctuple (map %# args));
+  val pat_stricts = map (fn (con,args) => pg (branch_def::axs_pat_def)
+                      (mk_trp(strict(pat_lhs (con,args)`(%:"rhs"))))
+                      [simp_tac (HOLCF_ss addsimps [when_strict]) 1]) cons;
+  val pat_apps = let fun one_pat c (con,args) = pg (branch_def::axs_pat_def)
                    (lift_defined %: (nonlazy args,
                         (mk_trp((pat_lhs c)`(%:"rhs")`(con_app con args) ===
                               (if con = fst c then pat_rhs c else %%:failN)))))
                    [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
-        in List.concat(map (fn c => map (one_pat c) cons) cons) end;
+        in List.concat (map (fn c => map (one_pat c) cons) cons) end;
 in pat_stricts @ pat_apps end;
 
 val con_stricts = List.concat(map (fn (con,args) => map (fn vn =>
@@ -369,7 +370,7 @@
 		("copy_rews", copy_rews)])))
        |> (#1 o PureThy.add_thmss [(("match_rews", mat_rews), [Simplifier.simp_add_global])])
        |> Theory.parent_path |> rpair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
-                 dist_les @ dist_eqs @ copy_rews)
+                 pat_rews @ dist_les @ dist_eqs @ copy_rews)
 end; (* let *)
 
 fun comp_theorems (comp_dnam, eqs: eq list) thy =