reimplement Case expression pattern matching to support lazy patterns
authorhuffman
Wed Nov 30 01:01:15 2005 +0100 (2005-11-30)
changeset 182934eaa654c92f2
parent 18292 9ca223aedb1e
child 18294 bbfd64cc91ab
reimplement Case expression pattern matching to support lazy patterns
src/HOLCF/Fixrec.thy
src/HOLCF/document/root.tex
src/HOLCF/domain/axioms.ML
src/HOLCF/domain/library.ML
src/HOLCF/domain/syntax.ML
src/HOLCF/domain/theorems.ML
     1.1 --- a/src/HOLCF/Fixrec.thy	Wed Nov 30 00:59:04 2005 +0100
     1.2 +++ b/src/HOLCF/Fixrec.thy	Wed Nov 30 01:01:15 2005 +0100
     1.3 @@ -31,6 +31,20 @@
     1.4  apply (rule_tac p=y in upE, simp, simp)
     1.5  done
     1.6  
     1.7 +lemma return_defined [simp]: "return\<cdot>x \<noteq> \<bottom>"
     1.8 +by (simp add: return_def)
     1.9 +
    1.10 +lemma fail_defined [simp]: "fail \<noteq> \<bottom>"
    1.11 +by (simp add: fail_def)
    1.12 +
    1.13 +lemma return_eq [simp]: "(return\<cdot>x = return\<cdot>y) = (x = y)"
    1.14 +by (simp add: return_def)
    1.15 +
    1.16 +lemma return_neq_fail [simp]:
    1.17 +  "return\<cdot>x \<noteq> fail" "fail \<noteq> return\<cdot>x"
    1.18 +by (simp_all add: return_def fail_def)
    1.19 +
    1.20 +
    1.21  subsubsection {* Monadic bind operator *}
    1.22  
    1.23  constdefs
    1.24 @@ -149,22 +163,21 @@
    1.25  
    1.26  lemmas run_fatbar_simps [simp] = run_fatbar1 run_fatbar2 run_fatbar3
    1.27  
    1.28 -subsection {* Pattern combinators *}
    1.29 -
    1.30 -types ('a,'b,'c) pat = "'b \<rightarrow> 'a \<rightarrow> 'c maybe"
    1.31 +subsection {* Case branch combinator *}
    1.32  
    1.33  constdefs
    1.34 -  wild_pat :: "('a, 'b, 'b) pat"
    1.35 -  "wild_pat \<equiv> \<Lambda> r a. return\<cdot>r"
    1.36 -
    1.37 -  var_pat :: "('a, 'a \<rightarrow> 'b, 'b) pat"
    1.38 -  "var_pat \<equiv> \<Lambda> r a. return\<cdot>(r\<cdot>a)"
    1.39 +  branch :: "('a \<rightarrow> 'b maybe) \<Rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'c maybe)"
    1.40 +  "branch p \<equiv> \<Lambda> r x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> y. return\<cdot>(r\<cdot>y))"
    1.41  
    1.42 -lemma wild_pat [simp]: "wild_pat\<cdot>r\<cdot>a = return\<cdot>r"
    1.43 -by (simp add: wild_pat_def)
    1.44 +lemma branch_rews:
    1.45 +  "p\<cdot>x = \<bottom> \<Longrightarrow> branch p\<cdot>r\<cdot>x = \<bottom>"
    1.46 +  "p\<cdot>x = fail \<Longrightarrow> branch p\<cdot>r\<cdot>x = fail"
    1.47 +  "p\<cdot>x = return\<cdot>y \<Longrightarrow> branch p\<cdot>r\<cdot>x = return\<cdot>(r\<cdot>y)"
    1.48 +by (simp_all add: branch_def)
    1.49  
    1.50 -lemma var_pat [simp]: "var_pat\<cdot>r\<cdot>a = return\<cdot>(r\<cdot>a)"
    1.51 -by (simp add: var_pat_def)
    1.52 +lemma branch_return [simp]: "branch return\<cdot>r\<cdot>x = return\<cdot>(r\<cdot>x)"
    1.53 +by (simp add: branch_def)
    1.54 +
    1.55  
    1.56  subsection {* Case syntax *}
    1.57  
    1.58 @@ -180,198 +193,242 @@
    1.59  syntax (xsymbols)
    1.60    "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
    1.61  
    1.62 -text {* Intermediate tags for parsing/printing *}
    1.63 -syntax
    1.64 -  "_pat" :: "'a"
    1.65 -  "_var" :: "'a"
    1.66 -  "_match" :: "'a"
    1.67 +translations
    1.68 +  "_Case_syntax x ms" == "run\<cdot>(ms\<cdot>x)"
    1.69 +  "_Case2 m ms" == "m \<parallel> ms"
    1.70  
    1.71  text {* Parsing Case expressions *}
    1.72  
    1.73 +syntax
    1.74 +  "_pat" :: "'a"
    1.75 +  "_var" :: "'a"
    1.76 +
    1.77  translations
    1.78 -  "_Case_syntax x cs" => "run\<cdot>(cs\<cdot>x)"
    1.79 -  "_Case2 c cs" => "fatbar\<cdot>c\<cdot>cs"
    1.80 -  "_Case1 p r" => "_match (_var p) r"
    1.81 -  "_var _" => "wild_pat"
    1.82 +  "_Case1 p r" => "branch (_pat p)\<cdot>(_var p r)"
    1.83 +  "_var (_args x y) r" => "csplit\<cdot>(_var x (_var y r))"
    1.84 +  "_var () r" => "unit_when\<cdot>r"
    1.85  
    1.86  parse_translation {*
    1.87 -  let
    1.88 -    fun capp (t,u) = Syntax.const "Rep_CFun" $ t $ u;
    1.89 -    fun cabs (x,t) = (snd (mk_binder_tr ("_cabs", "Abs_CFun"))) [x,t];
    1.90 -
    1.91 -    fun get_vars (Const ("_var",_) $ x) = [x]
    1.92 -    |   get_vars (t $ u) = get_vars t @ get_vars u
    1.93 -    |   get_vars t = [];
    1.94 -
    1.95 -    fun rem_vars (Const ("_var",_) $ x) = Syntax.const "var_pat"
    1.96 -    |   rem_vars (t $ u) = rem_vars t $ rem_vars u
    1.97 -    |   rem_vars t = t;
    1.98 -
    1.99 -    fun match_tr [pat, rhs] =
   1.100 -          capp (rem_vars pat, foldr cabs rhs (get_vars pat))
   1.101 -    |   match_tr ts = raise TERM ("match_tr", ts);
   1.102 -
   1.103 -  in [("_match", match_tr)] end;
   1.104 +(* rewrites (_pat x) => (return) *)
   1.105 +(* rewrites (_var x t) => (Abs_CFun (%x. t)) *)
   1.106 +  [("_pat", K (Syntax.const "return")),
   1.107 +   mk_binder_tr ("_var", "Abs_CFun")];
   1.108  *}
   1.109  
   1.110  text {* Printing Case expressions *}
   1.111  
   1.112 -translations
   1.113 -  "_" <= "_pat wild_pat"
   1.114 -  "x" <= "_pat (_var x)"
   1.115 +syntax
   1.116 +  "_match" :: "'a"
   1.117  
   1.118  print_translation {*
   1.119    let
   1.120 -    fun dest_cabs (Const ("Abs_CFun",_) $ t) =
   1.121 -          let val abs = case t of Abs abs => abs
   1.122 -                  | _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0);
   1.123 -          in atomic_abs_tr' abs end
   1.124 -    |   dest_cabs _ = raise Match; (* too few vars: abort translation *)
   1.125 -
   1.126 -    fun put_vars (Const ("var_pat",_), rhs) =
   1.127 -          let val (x, rhs') = dest_cabs rhs;
   1.128 -          in (Syntax.const "_var" $ x, rhs') end
   1.129 -    |   put_vars (t $ u, rhs) =
   1.130 +    fun dest_LAM (Const ("Rep_CFun",_) $ Const ("unit_when",_) $ t) =
   1.131 +          (Syntax.const "Unity", t)
   1.132 +    |   dest_LAM (Const ("Rep_CFun",_) $ Const ("csplit",_) $ t) =
   1.133 +          let
   1.134 +            val (v1, t1) = dest_LAM t;
   1.135 +            val (v2, t2) = dest_LAM t1;
   1.136 +          in (Syntax.const "_args" $ v1 $ v2, t2) end 
   1.137 +    |   dest_LAM (Const ("Abs_CFun",_) $ t) =
   1.138            let
   1.139 -            val (t', rhs') = put_vars (t,rhs);
   1.140 -            val (u', rhs'') = put_vars (u,rhs');
   1.141 -          in (t' $ u', rhs'') end
   1.142 -    |   put_vars (t, rhs) = (t, rhs);
   1.143 -
   1.144 -    fun Case1_tr' (_ $ pat $ rhs) = let
   1.145 -          val (pat', rhs') = put_vars (pat, rhs);
   1.146 -        in Syntax.const "_Case1" $ (Syntax.const "_pat" $ pat') $ rhs' end;
   1.147 +            val abs = case t of Abs abs => abs
   1.148 +                | _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0);
   1.149 +            val (x, t') = atomic_abs_tr' abs;
   1.150 +          in (Syntax.const "_var" $ x, t') end
   1.151 +    |   dest_LAM _ = raise Match; (* too few vars: abort translation *)
   1.152  
   1.153 -    fun Case2_tr' (_ $ (_ $ Const ("fatbar",_) $ m) $ ms) =
   1.154 -          Syntax.const "_Case2" $ Case1_tr' m $ Case2_tr' ms
   1.155 -    |   Case2_tr' t = Case1_tr' t;
   1.156 +    fun Case1_tr' [Const("branch",_) $ p, r] =
   1.157 +          let val (v, t) = dest_LAM r;
   1.158 +          in Syntax.const "_Case1" $ (Syntax.const "_match" $ p $ v) $ t end;
   1.159  
   1.160 -    fun Case_syntax_tr' [Const ("run",_), _ $ ms $ x] =
   1.161 -          Syntax.const "_Case_syntax" $ x $ Case2_tr' ms;
   1.162 -
   1.163 -  in [("Rep_CFun", Case_syntax_tr')] end;
   1.164 +  in [("Rep_CFun", Case1_tr')] end;
   1.165  *}
   1.166  
   1.167 -subsection {* Pattern combinators for built-in types *}
   1.168 +translations
   1.169 +  "x" <= "_match return (_var x)"
   1.170 +
   1.171 +
   1.172 +subsection {* Pattern combinators for data constructors *}
   1.173 +
   1.174 +types ('a, 'b) pat = "'a \<rightarrow> 'b maybe"
   1.175  
   1.176  constdefs
   1.177 -  cpair_pat :: "('a, _, _) pat \<Rightarrow> ('b, _, _) pat \<Rightarrow> ('a \<times> 'b, _, _) pat"
   1.178 -  "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)"
   1.179 +  cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat"
   1.180 +  "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>"
   1.181  
   1.182 -  spair_pat :: "(_, _, _) pat \<Rightarrow> (_, _, _) pat \<Rightarrow> (_, _, _) pat"
   1.183 -  "spair_pat p1 p2 \<equiv> \<Lambda> r (:x,y:). cpair_pat p1 p2\<cdot>r\<cdot>\<langle>x,y\<rangle>"
   1.184 +  spair_pat ::
   1.185 +  "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a::pcpo \<otimes> 'b::pcpo, 'c \<times> 'd) pat"
   1.186 +  "spair_pat p1 p2 \<equiv> \<Lambda>(:x, y:). cpair_pat p1 p2\<cdot>\<langle>x, y\<rangle>"
   1.187  
   1.188 -  sinl_pat :: "(_, _, _) pat \<Rightarrow> (_, _, _) pat"
   1.189 -  "sinl_pat p \<equiv> \<Lambda> r a. case a of sinl\<cdot>x \<Rightarrow> p\<cdot>r\<cdot>x | sinr\<cdot>y \<Rightarrow> fail"
   1.190 +  sinl_pat :: "('a, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat"
   1.191 +  "sinl_pat p \<equiv> sscase\<cdot>p\<cdot>(\<Lambda> x. fail)"
   1.192  
   1.193 -  sinr_pat :: "(_, _, _) pat \<Rightarrow> (_, _, _) pat"
   1.194 -  "sinr_pat p \<equiv> \<Lambda> r a. case a of sinl\<cdot>x \<Rightarrow> fail | sinr\<cdot>y \<Rightarrow> p\<cdot>r\<cdot>y"
   1.195 +  sinr_pat :: "('b, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat"
   1.196 +  "sinr_pat p \<equiv> sscase\<cdot>(\<Lambda> x. fail)\<cdot>p"
   1.197 +
   1.198 +  up_pat :: "('a, 'b) pat \<Rightarrow> ('a u, 'b) pat"
   1.199 +  "up_pat p \<equiv> fup\<cdot>p"
   1.200  
   1.201 -  up_pat :: "('a, _, _) pat \<Rightarrow> ('a u, _, _) pat"
   1.202 -  "up_pat p \<equiv> \<Lambda> r a. case a of up\<cdot>x \<Rightarrow> p\<cdot>r\<cdot>x"
   1.203 +  TT_pat :: "(tr, unit) pat"
   1.204 +  "TT_pat \<equiv> \<Lambda> b. If b then return\<cdot>() else fail fi"
   1.205  
   1.206 -  Def_pat :: "'a::type \<Rightarrow> ('a lift, _, _) pat"
   1.207 -  "Def_pat x \<equiv> \<Lambda> r. FLIFT y. if x = y then return\<cdot>r else fail"
   1.208 +  FF_pat :: "(tr, unit) pat"
   1.209 +  "FF_pat \<equiv> \<Lambda> b. If b then fail else return\<cdot>() fi"
   1.210  
   1.211 -  ONE_pat :: "(one, _, _) pat"
   1.212 -  "ONE_pat \<equiv> \<Lambda> r ONE. return\<cdot>r"
   1.213 -
   1.214 -  TT_pat :: "(tr, _, _) pat"
   1.215 -  "TT_pat \<equiv> \<Lambda> r b. If b then return\<cdot>r else fail fi"
   1.216 -
   1.217 -  FF_pat :: "(tr, _, _) pat"
   1.218 -  "FF_pat \<equiv> \<Lambda> r b. If b then fail else return\<cdot>r fi"
   1.219 +  ONE_pat :: "(one, unit) pat"
   1.220 +  "ONE_pat \<equiv> \<Lambda> ONE. return\<cdot>()"
   1.221  
   1.222 -text {* Parse translations *}
   1.223 +text {* Parse translations (patterns) *}
   1.224  translations
   1.225 -  "_var (cpair\<cdot>p1\<cdot>p2)" => "cpair_pat (_var p1) (_var p2)"
   1.226 -  "_var (spair\<cdot>p1\<cdot>p2)" => "spair_pat (_var p1) (_var p2)"
   1.227 -  "_var (sinl\<cdot>p1)"     => "sinl_pat (_var p1)"
   1.228 -  "_var (sinr\<cdot>p1)"     => "sinr_pat (_var p1)"
   1.229 -  "_var (up\<cdot>p1)"       => "up_pat (_var p1)"
   1.230 -  "_var (Def x)"       => "Def_pat x"
   1.231 -  "_var ONE"           => "ONE_pat"
   1.232 -  "_var TT"            => "TT_pat"
   1.233 -  "_var FF"            => "FF_pat"
   1.234 +  "_pat (cpair\<cdot>x\<cdot>y)" => "cpair_pat (_pat x) (_pat y)"
   1.235 +  "_pat (spair\<cdot>x\<cdot>y)" => "spair_pat (_pat x) (_pat y)"
   1.236 +  "_pat (sinl\<cdot>x)" => "sinl_pat (_pat x)"
   1.237 +  "_pat (sinr\<cdot>x)" => "sinr_pat (_pat x)"
   1.238 +  "_pat (up\<cdot>x)" => "up_pat (_pat x)"
   1.239 +  "_pat TT" => "TT_pat"
   1.240 +  "_pat FF" => "FF_pat"
   1.241 +  "_pat ONE" => "ONE_pat"
   1.242 +
   1.243 +text {* Parse translations (variables) *}
   1.244 +translations
   1.245 +  "_var (cpair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
   1.246 +  "_var (spair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
   1.247 +  "_var (sinl\<cdot>x) r" => "_var x r"
   1.248 +  "_var (sinr\<cdot>x) r" => "_var x r"
   1.249 +  "_var (up\<cdot>x) r" => "_var x r"
   1.250 +  "_var TT r" => "_var () r"
   1.251 +  "_var FF r" => "_var () r"
   1.252 +  "_var ONE r" => "_var () r"
   1.253  
   1.254  text {* Print translations *}
   1.255  translations
   1.256 -  "cpair\<cdot>(_pat p1)\<cdot>(_pat p2)" <= "_pat (cpair_pat p1 p2)"
   1.257 -  "spair\<cdot>(_pat p1)\<cdot>(_pat p2)" <= "_pat (spair_pat p1 p2)"
   1.258 -  "sinl\<cdot>(_pat p1)"            <= "_pat (sinl_pat p1)"
   1.259 -  "sinr\<cdot>(_pat p1)"            <= "_pat (sinr_pat p1)"
   1.260 -  "up\<cdot>(_pat p1)"              <= "_pat (up_pat p1)"
   1.261 -  "Def x"                     <= "_pat (Def_pat x)"
   1.262 -  "TT"                        <= "_pat (TT_pat)"
   1.263 -  "FF"                        <= "_pat (FF_pat)"
   1.264 +  "cpair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
   1.265 +      <= "_match (cpair_pat p1 p2) (_args v1 v2)"
   1.266 +  "spair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
   1.267 +      <= "_match (spair_pat p1 p2) (_args v1 v2)"
   1.268 +  "sinl\<cdot>(_match p1 v1)" <= "_match (sinl_pat p1) v1"
   1.269 +  "sinr\<cdot>(_match p1 v1)" <= "_match (sinr_pat p1) v1"
   1.270 +  "up\<cdot>(_match p1 v1)" <= "_match (up_pat p1) v1"
   1.271 +  "TT" <= "_match TT_pat ()"
   1.272 +  "FF" <= "_match FF_pat ()"
   1.273 +  "ONE" <= "_match ONE_pat ()"
   1.274 +
   1.275 +lemma cpair_pat1:
   1.276 +  "branch p\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = \<bottom>"
   1.277 +apply (simp add: branch_def cpair_pat_def)
   1.278 +apply (rule_tac p="p\<cdot>x" in maybeE, simp_all)
   1.279 +done
   1.280  
   1.281 -lemma cpair_pat_simps [simp]:
   1.282 -  "p1\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> cpair_pat p1 p2\<cdot>r\<cdot><x,y> = \<bottom>"
   1.283 -  "p1\<cdot>r\<cdot>x = fail \<Longrightarrow> cpair_pat p1 p2\<cdot>r\<cdot><x,y> = fail"
   1.284 -  "p1\<cdot>r\<cdot>x = return\<cdot>r' \<Longrightarrow> cpair_pat p1 p2\<cdot>r\<cdot><x,y> = p2\<cdot>r'\<cdot>y"
   1.285 -by (simp_all add: cpair_pat_def)
   1.286 +lemma cpair_pat2:
   1.287 +  "branch p\<cdot>r\<cdot>x = fail \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = fail"
   1.288 +apply (simp add: branch_def cpair_pat_def)
   1.289 +apply (rule_tac p="p\<cdot>x" in maybeE, simp_all)
   1.290 +done
   1.291  
   1.292 -lemma spair_pat_simps [simp]:
   1.293 -  "spair_pat p1 p2\<cdot>r\<cdot>\<bottom> = \<bottom>"
   1.294 -  "\<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>"
   1.295 -by (simp_all add: spair_pat_def)
   1.296 +lemma cpair_pat3:
   1.297 +  "branch p\<cdot>r\<cdot>x = return\<cdot>s \<Longrightarrow>
   1.298 +   branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = branch q\<cdot>s\<cdot>y"
   1.299 +apply (simp add: branch_def cpair_pat_def)
   1.300 +apply (rule_tac p="p\<cdot>x" in maybeE, simp_all)
   1.301 +apply (rule_tac p="q\<cdot>y" in maybeE, simp_all)
   1.302 +done
   1.303  
   1.304 -lemma sinl_pat_simps [simp]:
   1.305 -  "sinl_pat p\<cdot>r\<cdot>\<bottom> = \<bottom>"
   1.306 -  "x \<noteq> \<bottom> \<Longrightarrow> sinl_pat p\<cdot>r\<cdot>(sinl\<cdot>x) = p\<cdot>r\<cdot>x"
   1.307 -  "x \<noteq> \<bottom> \<Longrightarrow> sinl_pat p\<cdot>r\<cdot>(sinr\<cdot>x) = fail"
   1.308 -by (simp_all add: sinl_pat_def)
   1.309 +lemmas cpair_pat [simp] =
   1.310 +  cpair_pat1 cpair_pat2 cpair_pat3
   1.311  
   1.312 -lemma sinr_pat_simps [simp]:
   1.313 -  "sinr_pat p\<cdot>r\<cdot>\<bottom> = \<bottom>"
   1.314 -  "x \<noteq> \<bottom> \<Longrightarrow> sinr_pat p\<cdot>r\<cdot>(sinl\<cdot>x) = fail"
   1.315 -  "x \<noteq> \<bottom> \<Longrightarrow> sinr_pat p\<cdot>r\<cdot>(sinr\<cdot>x) = p\<cdot>r\<cdot>x"
   1.316 -by (simp_all add: sinr_pat_def)
   1.317 +lemma spair_pat [simp]:
   1.318 +  "branch (spair_pat p1 p2)\<cdot>r\<cdot>\<bottom> = \<bottom>"
   1.319 +  "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk>
   1.320 +     \<Longrightarrow> branch (spair_pat p1 p2)\<cdot>r\<cdot>(:x, y:) =
   1.321 +         branch (cpair_pat p1 p2)\<cdot>r\<cdot>\<langle>x, y\<rangle>"
   1.322 +by (simp_all add: branch_def spair_pat_def)
   1.323  
   1.324 -lemma up_pat_simps [simp]:
   1.325 -  "up_pat p\<cdot>r\<cdot>\<bottom> = \<bottom>"
   1.326 -  "up_pat p\<cdot>r\<cdot>(up\<cdot>x) = p\<cdot>r\<cdot>x"
   1.327 -by (simp_all add: up_pat_def)
   1.328 +lemma sinl_pat [simp]:
   1.329 +  "branch (sinl_pat p)\<cdot>r\<cdot>\<bottom> = \<bottom>"
   1.330 +  "x \<noteq> \<bottom> \<Longrightarrow> branch (sinl_pat p)\<cdot>r\<cdot>(sinl\<cdot>x) = branch p\<cdot>r\<cdot>x"
   1.331 +  "y \<noteq> \<bottom> \<Longrightarrow> branch (sinl_pat p)\<cdot>r\<cdot>(sinr\<cdot>y) = fail"
   1.332 +by (simp_all add: branch_def sinl_pat_def)
   1.333  
   1.334 -lemma Def_pat_simps [simp]:
   1.335 -  "Def_pat x\<cdot>r\<cdot>\<bottom> = \<bottom>"
   1.336 -  "Def_pat x\<cdot>r\<cdot>(Def x) = return\<cdot>r"
   1.337 -  "x \<noteq> y \<Longrightarrow> Def_pat x\<cdot>r\<cdot>(Def y) = fail"
   1.338 -by (simp_all add: Def_pat_def)
   1.339 +lemma sinr_pat [simp]:
   1.340 +  "branch (sinr_pat p)\<cdot>r\<cdot>\<bottom> = \<bottom>"
   1.341 +  "x \<noteq> \<bottom> \<Longrightarrow> branch (sinr_pat p)\<cdot>r\<cdot>(sinl\<cdot>x) = fail"
   1.342 +  "y \<noteq> \<bottom> \<Longrightarrow> branch (sinr_pat p)\<cdot>r\<cdot>(sinr\<cdot>y) = branch p\<cdot>r\<cdot>y"
   1.343 +by (simp_all add: branch_def sinr_pat_def)
   1.344  
   1.345 -lemma ONE_pat_simps [simp]:
   1.346 -  "ONE_pat\<cdot>r\<cdot>\<bottom> = \<bottom>"
   1.347 -  "ONE_pat\<cdot>r\<cdot>ONE = return\<cdot>r"
   1.348 -by (simp_all add: ONE_pat_def)
   1.349 +lemma up_pat [simp]:
   1.350 +  "branch (up_pat p)\<cdot>r\<cdot>\<bottom> = \<bottom>"
   1.351 +  "branch (up_pat p)\<cdot>r\<cdot>(up\<cdot>x) = branch p\<cdot>r\<cdot>x"
   1.352 +by (simp_all add: branch_def up_pat_def)
   1.353 +
   1.354 +lemma TT_pat [simp]:
   1.355 +  "branch TT_pat\<cdot>(unit_when\<cdot>r)\<cdot>\<bottom> = \<bottom>"
   1.356 +  "branch TT_pat\<cdot>(unit_when\<cdot>r)\<cdot>TT = return\<cdot>r"
   1.357 +  "branch TT_pat\<cdot>(unit_when\<cdot>r)\<cdot>FF = fail"
   1.358 +by (simp_all add: branch_def TT_pat_def)
   1.359  
   1.360 -lemma TT_pat_simps [simp]:
   1.361 -  "TT_pat\<cdot>r\<cdot>\<bottom> = \<bottom>"
   1.362 -  "TT_pat\<cdot>r\<cdot>TT = return\<cdot>r"
   1.363 -  "TT_pat\<cdot>r\<cdot>FF = fail"
   1.364 -by (simp_all add: TT_pat_def)
   1.365 +lemma FF_pat [simp]:
   1.366 +  "branch FF_pat\<cdot>(unit_when\<cdot>r)\<cdot>\<bottom> = \<bottom>"
   1.367 +  "branch FF_pat\<cdot>(unit_when\<cdot>r)\<cdot>TT = fail"
   1.368 +  "branch FF_pat\<cdot>(unit_when\<cdot>r)\<cdot>FF = return\<cdot>r"
   1.369 +by (simp_all add: branch_def FF_pat_def)
   1.370  
   1.371 -lemma FF_pat_simps [simp]:
   1.372 -  "FF_pat\<cdot>r\<cdot>\<bottom> = \<bottom>"
   1.373 -  "FF_pat\<cdot>r\<cdot>TT = fail"
   1.374 -  "FF_pat\<cdot>r\<cdot>FF = return\<cdot>r"
   1.375 -by (simp_all add: FF_pat_def)
   1.376 +lemma ONE_pat [simp]:
   1.377 +  "branch ONE_pat\<cdot>(unit_when\<cdot>r)\<cdot>\<bottom> = \<bottom>"
   1.378 +  "branch ONE_pat\<cdot>(unit_when\<cdot>r)\<cdot>ONE = return\<cdot>r"
   1.379 +by (simp_all add: branch_def ONE_pat_def)
   1.380  
   1.381 -subsection {* As-patterns *}
   1.382 +
   1.383 +subsection {* Wildcards, as-patterns, and lazy patterns *}
   1.384  
   1.385  syntax
   1.386 -  "_as_pattern" :: "['a, 'a] \<Rightarrow> 'a" (* infixr "as" 10 *)
   1.387 -  (* TODO: choose a non-ambiguous syntax for as-patterns *)
   1.388 +  "_as_pat" :: "[idt, 'a] \<Rightarrow> 'a" (infixr "\<as>" 10)
   1.389 +  "_lazy_pat" :: "'a \<Rightarrow> 'a" ("\<lazy> _" [1000] 1000)
   1.390  
   1.391  constdefs
   1.392 -  as_pat :: "('a,'b,'c) pat \<Rightarrow> ('a,'c,'d) pat \<Rightarrow> ('a,'b,'d) pat"
   1.393 -  "as_pat p1 p2 \<equiv> \<Lambda> r a. cpair_pat p1 p2\<cdot>r\<cdot>\<langle>a, a\<rangle>"
   1.394 +  wild_pat :: "'a \<rightarrow> unit maybe"
   1.395 +  "wild_pat \<equiv> \<Lambda> x. return\<cdot>()"
   1.396 +
   1.397 +  as_pat :: "('a \<rightarrow> 'b maybe) \<Rightarrow> 'a \<rightarrow> ('a \<times> 'b) maybe"
   1.398 +  "as_pat p \<equiv> \<Lambda> x. do a <- p\<cdot>x; return\<cdot>\<langle>x, a\<rangle>"
   1.399  
   1.400 +  lazy_pat :: "('a \<rightarrow> 'b::pcpo maybe) \<Rightarrow> ('a \<rightarrow> 'b maybe)"
   1.401 +  "lazy_pat p \<equiv> \<Lambda> x. return\<cdot>(run\<cdot>(p\<cdot>x))"
   1.402 +
   1.403 +text {* Parse translations (patterns) *}
   1.404 +translations
   1.405 +  "_pat _" => "wild_pat"
   1.406 +  "_pat (_as_pat x y)" => "as_pat (_pat y)"
   1.407 +  "_pat (_lazy_pat x)" => "lazy_pat (_pat x)"
   1.408 +
   1.409 +text {* Parse translations (variables) *}
   1.410  translations
   1.411 -  "_var (_as_pattern p1 p2)" => "as_pat (_var p1) (_var p2)"
   1.412 -  "_as_pattern (_pat p1) (_pat p2)" <= "_pat (as_pat p1 p2)"
   1.413 +  "_var _ r" => "_var () r"
   1.414 +  "_var (_as_pat x y) r" => "_var (_args x y) r"
   1.415 +  "_var (_lazy_pat x) r" => "_var x r"
   1.416 +
   1.417 +text {* Print translations *}
   1.418 +translations
   1.419 +  "_" <= "_match wild_pat ()"
   1.420 +  "_as_pat x (_match p v)" <= "_match (as_pat p) (_args (_var x) v)"
   1.421 +  "_lazy_pat (_match p v)" <= "_match (lazy_pat p) v"
   1.422 +
   1.423 +lemma wild_pat [simp]: "branch wild_pat\<cdot>(unit_when\<cdot>r)\<cdot>x = return\<cdot>r"
   1.424 +by (simp add: branch_def wild_pat_def)
   1.425  
   1.426 -lemma as_pat [simp]: "as_pat p1 p2\<cdot>r\<cdot>a = cpair_pat p1 p2\<cdot>r\<cdot>\<langle>a, a\<rangle>"
   1.427 -by (simp add: as_pat_def)
   1.428 +lemma as_pat [simp]:
   1.429 +  "branch (as_pat p)\<cdot>(csplit\<cdot>r)\<cdot>x = branch p\<cdot>(r\<cdot>x)\<cdot>x"
   1.430 +apply (simp add: branch_def as_pat_def)
   1.431 +apply (rule_tac p="p\<cdot>x" in maybeE, simp_all)
   1.432 +done
   1.433 +
   1.434 +lemma lazy_pat [simp]:
   1.435 +  "branch p\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> branch (lazy_pat p)\<cdot>r\<cdot>x = return\<cdot>(r\<cdot>\<bottom>)"
   1.436 +  "branch p\<cdot>r\<cdot>x = fail \<Longrightarrow> branch (lazy_pat p)\<cdot>r\<cdot>x = return\<cdot>(r\<cdot>\<bottom>)"
   1.437 +  "branch p\<cdot>r\<cdot>x = return\<cdot>s \<Longrightarrow> branch (lazy_pat p)\<cdot>r\<cdot>x = return\<cdot>s"
   1.438 +apply (simp_all add: branch_def lazy_pat_def)
   1.439 +apply (rule_tac [!] p="p\<cdot>x" in maybeE, simp_all)
   1.440 +done
   1.441 +
   1.442  
   1.443  subsection {* Match functions for built-in types *}
   1.444  
   1.445 @@ -478,6 +535,7 @@
   1.446  val cpair_eqD1 = thm "cpair_eqD1";
   1.447  val cpair_eqD2 = thm "cpair_eqD2";
   1.448  val ssubst_lhs = thm "ssubst_lhs";
   1.449 +val branch_def = thm "branch_def";
   1.450  *}
   1.451  
   1.452  subsection {* Initializing the fixrec package *}
     2.1 --- a/src/HOLCF/document/root.tex	Wed Nov 30 00:59:04 2005 +0100
     2.2 +++ b/src/HOLCF/document/root.tex	Wed Nov 30 01:01:15 2005 +0100
     2.3 @@ -10,6 +10,8 @@
     2.4  \urlstyle{rm}
     2.5  \isabellestyle{it}
     2.6  \pagestyle{myheadings}
     2.7 +\newcommand{\isasymas}{\textsf{as}}
     2.8 +\newcommand{\isasymlazy}{\isamath{\sim}}
     2.9  
    2.10  \begin{document}
    2.11  
     3.1 --- a/src/HOLCF/domain/axioms.ML	Wed Nov 30 00:59:04 2005 +0100
     3.2 +++ b/src/HOLCF/domain/axioms.ML	Wed Nov 30 01:01:15 2005 +0100
     3.3 @@ -79,14 +79,14 @@
     3.4            val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
     3.5            val xs = map (bound_arg args) args;
     3.6            val r = Bound (length args);
     3.7 -          val rhs = case args of [] => %%:returnN ` r
     3.8 -                                | _ => foldr1 cpair_pat ps ` r ` mk_ctuple xs;
     3.9 +          val rhs = case args of [] => %%:returnN ` HOLogic.unit
    3.10 +                                | _ => foldr1 cpair_pat ps ` mk_ctuple xs;
    3.11            fun one_con (con',args') = foldr /\# (if con'=con then rhs else %%:failN) args';
    3.12          in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) == 
    3.13 -               /\ "r" (list_ccomb(%%:(dname^"_when"), map one_con cons)))
    3.14 +               list_ccomb(%%:(dname^"_when"), map one_con cons))
    3.15          end
    3.16      in map pdef cons end;
    3.17 -  
    3.18 +
    3.19    val sel_defs = let
    3.20  	fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == 
    3.21  		 list_ccomb(%%:(dname^"_when"),map 
     4.1 --- a/src/HOLCF/domain/library.ML	Wed Nov 30 00:59:04 2005 +0100
     4.2 +++ b/src/HOLCF/domain/library.ML	Wed Nov 30 01:01:15 2005 +0100
     4.3 @@ -130,6 +130,7 @@
     4.4  val returnN    = "Fixrec.return";
     4.5  val failN      = "Fixrec.fail";
     4.6  val cpair_patN = "Fixrec.cpair_pat";
     4.7 +val branchN    = "Fixrec.branch";
     4.8  
     4.9  val pcpoN      = "Pcpo.pcpo"
    4.10  val pcpoS      = [pcpoN];
     5.1 --- a/src/HOLCF/domain/syntax.ML	Wed Nov 30 00:59:04 2005 +0100
     5.2 +++ b/src/HOLCF/domain/syntax.ML	Wed Nov 30 01:01:15 2005 +0100
     5.3 @@ -53,10 +53,10 @@
     5.4    fun sel (_   ,_,args) = List.mapPartial sel1 args;
     5.5    fun freetvar s n      = let val tvar = mk_TFree (s ^ string_of_int n) in
     5.6  			  if tvar mem typevars then freetvar ("t"^s) n else tvar end;
     5.7 -  fun mk_patT (a,b,c)   = b ->> a ->> mk_ssumT(oneT, mk_uT c);
     5.8 -  fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n, freetvar "t" (n+1));
     5.9 +  fun mk_patT (a,b)     = a ->> mk_ssumT (oneT, mk_uT b);
    5.10 +  fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n);
    5.11    fun pat (con ,s,args) = (pat_name_ con, (mapn pat_arg_typ 1 args) --->
    5.12 -			   mk_patT (dtype, freetvar "t" 1, freetvar "t" (length args + 1)),
    5.13 +			   mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))),
    5.14  			   Mixfix(escape (con ^ "_pat"), [], Syntax.max_pri));
    5.15  
    5.16  in
    5.17 @@ -80,16 +80,19 @@
    5.18      fun expvar n     = Variable ("e"^(string_of_int n));
    5.19      fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
    5.20  				     (string_of_int m));
    5.21 -    fun app s (l,r)   = mk_appl (Constant s) [l,r];
    5.22 +    fun argvars n args = mapn (argvar n) 1 args;
    5.23 +    fun app s (l,r)  = mk_appl (Constant s) [l,r];
    5.24      val cabs = app "_cabs";
    5.25      val capp = app "Rep_CFun";
    5.26 -    fun con1 n (con,mx,args) = Library.foldl capp (c_ast con mx, mapn (argvar n) 1 args);
    5.27 +    fun con1 n (con,mx,args) = Library.foldl capp (c_ast con mx, argvars n args);
    5.28      fun case1 n (con,mx,args) = app "_case1" (con1 n (con,mx,args), expvar n);
    5.29 -    fun arg1 n (con,_,args) = foldr cabs (expvar n) (mapn (argvar n) 1 args);
    5.30 +    fun arg1 n (con,_,args) = foldr cabs (expvar n) (argvars n args);
    5.31      fun when1 n m = if n = m then arg1 n else K (Constant "UU");
    5.32  
    5.33 -    fun app_var x = mk_appl (Constant "_var") [x];
    5.34 +    fun app_var x = mk_appl (Constant "_var") [x, Variable "rhs"];
    5.35      fun app_pat x = mk_appl (Constant "_pat") [x];
    5.36 +    fun args_list [] = Constant "Unity"
    5.37 +    |   args_list xs = foldr1 (app "_args") xs;
    5.38    in
    5.39      val case_trans = ParsePrintRule
    5.40          (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn case1 1 cons')),
    5.41 @@ -99,20 +102,29 @@
    5.42          (cabs (con1 n (con,mx,args), expvar n),
    5.43           Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons'))) 1 cons';
    5.44      
    5.45 -    val pattern_trans = mapn (fn n => fn (con,mx,args) => ParseRule
    5.46 -          (app_var (Library.foldl capp (c_ast con mx, mapn (argvar n) 1 args)),
    5.47 -           mk_appl (Constant (pat_name_ con)) (map app_var (mapn (argvar n) 1 args)))) 1 cons';
    5.48 -    
    5.49 -    val pattern_trans' = mapn (fn n => fn (con,mx,args) => PrintRule
    5.50 -          (Library.foldl capp (c_ast con mx, map app_pat (mapn (argvar n) 1 args)),
    5.51 -           app_pat (mk_appl (Constant (pat_name_ con)) (mapn (argvar n) 1 args)))) 1 cons';
    5.52 +    val Case_trans = List.concat (map (fn (con,mx,args) =>
    5.53 +      let
    5.54 +        val cname = c_ast con mx;
    5.55 +        val pname = Constant (pat_name_ con);
    5.56 +        val ns = 1 upto length args;
    5.57 +        val xs = map (fn n => Variable ("x"^(string_of_int n))) ns;
    5.58 +        val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
    5.59 +        val vs = map (fn n => Variable ("v"^(string_of_int n))) ns;
    5.60 +      in
    5.61 +        [ParseRule (app_pat (Library.foldl capp (cname, xs)),
    5.62 +                    mk_appl pname (map app_pat xs)),
    5.63 +         ParseRule (app_var (Library.foldl capp (cname, xs)),
    5.64 +                    app_var (args_list xs)),
    5.65 +         PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)),
    5.66 +                    app "_match" (mk_appl pname ps, args_list vs))]
    5.67 +      end) cons');
    5.68    end;
    5.69  end;
    5.70  
    5.71  in ([const_rep, const_abs, const_when, const_copy] @ 
    5.72       consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @
    5.73      [const_take, const_finite],
    5.74 -    (case_trans::(abscon_trans @ pattern_trans @ pattern_trans')))
    5.75 +    (case_trans::(abscon_trans @ Case_trans)))
    5.76  end; (* let *)
    5.77  
    5.78  (* ----- putting all the syntax stuff together ------------------------------ *)
     6.1 --- a/src/HOLCF/domain/theorems.ML	Wed Nov 30 00:59:04 2005 +0100
     6.2 +++ b/src/HOLCF/domain/theorems.ML	Wed Nov 30 01:01:15 2005 +0100
     6.3 @@ -209,18 +209,19 @@
     6.4  
     6.5  val pat_rews = let
     6.6    fun ps args = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
     6.7 -  fun pat_lhs (con,args) = list_comb (%%:(pat_name con), ps args);
     6.8 -  fun pat_rhs (con,[]) = %%:returnN ` (%:"rhs")
     6.9 -  |   pat_rhs (con,args) = (foldr1 cpair_pat (ps args))`(%:"rhs")`(mk_ctuple (map %# args));
    6.10 -  val pat_stricts = map (fn (con,args) => pg axs_pat_def (mk_trp(
    6.11 -                             strict(pat_lhs (con,args)`(%:"rhs"))))
    6.12 -                   [simp_tac (HOLCF_ss addsimps [when_strict]) 1]) cons;
    6.13 -  val pat_apps = let fun one_pat c (con,args)= pg axs_pat_def
    6.14 +  fun pat_lhs (con,args) = %%:branchN $ list_comb (%%:(pat_name con), ps args);
    6.15 +  fun pat_rhs (con,[]) = %%:returnN ` ((%:"rhs") ` HOLogic.unit)
    6.16 +  |   pat_rhs (con,args) =
    6.17 +        (%%:branchN $ foldr1 cpair_pat (ps args))`(%:"rhs")`(mk_ctuple (map %# args));
    6.18 +  val pat_stricts = map (fn (con,args) => pg (branch_def::axs_pat_def)
    6.19 +                      (mk_trp(strict(pat_lhs (con,args)`(%:"rhs"))))
    6.20 +                      [simp_tac (HOLCF_ss addsimps [when_strict]) 1]) cons;
    6.21 +  val pat_apps = let fun one_pat c (con,args) = pg (branch_def::axs_pat_def)
    6.22                     (lift_defined %: (nonlazy args,
    6.23                          (mk_trp((pat_lhs c)`(%:"rhs")`(con_app con args) ===
    6.24                                (if con = fst c then pat_rhs c else %%:failN)))))
    6.25                     [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
    6.26 -        in List.concat(map (fn c => map (one_pat c) cons) cons) end;
    6.27 +        in List.concat (map (fn c => map (one_pat c) cons) cons) end;
    6.28  in pat_stricts @ pat_apps end;
    6.29  
    6.30  val con_stricts = List.concat(map (fn (con,args) => map (fn vn =>
    6.31 @@ -369,7 +370,7 @@
    6.32  		("copy_rews", copy_rews)])))
    6.33         |> (#1 o PureThy.add_thmss [(("match_rews", mat_rews), [Simplifier.simp_add_global])])
    6.34         |> Theory.parent_path |> rpair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
    6.35 -                 dist_les @ dist_eqs @ copy_rews)
    6.36 +                 pat_rews @ dist_les @ dist_eqs @ copy_rews)
    6.37  end; (* let *)
    6.38  
    6.39  fun comp_theorems (comp_dnam, eqs: eq list) thy =