move unused pattern match syntax stuff into HOLCF/ex
authorhuffman
Mon May 24 11:29:49 2010 -0700 (2010-05-24)
changeset 37109e67760c1b851
parent 37108 00f13d3ad474
child 37110 7ffdbc24b27f
child 37112 67934c40a5f7
move unused pattern match syntax stuff into HOLCF/ex
src/HOLCF/Fixrec.thy
src/HOLCF/IsaMakefile
src/HOLCF/Tools/Domain/domain_constructors.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
src/HOLCF/Tutorial/Domain_ex.thy
src/HOLCF/ex/Pattern_Match.thy
src/HOLCF/ex/ROOT.ML
     1.1 --- a/src/HOLCF/Fixrec.thy	Mon May 24 09:32:52 2010 -0700
     1.2 +++ b/src/HOLCF/Fixrec.thy	Mon May 24 11:29:49 2010 -0700
     1.3 @@ -64,7 +64,6 @@
     1.4    "case m of XCONST fail \<Rightarrow> t1 | XCONST succeed\<cdot>x \<Rightarrow> t2"
     1.5      == "CONST match_case\<cdot>t1\<cdot>(\<Lambda> x. t2)\<cdot>m"
     1.6  
     1.7 -
     1.8  subsubsection {* Run operator *}
     1.9  
    1.10  definition
    1.11 @@ -109,334 +108,6 @@
    1.12  lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)"
    1.13  by (cases x, simp_all)
    1.14  
    1.15 -subsubsection {* Fatbar combinator *}
    1.16 -
    1.17 -definition
    1.18 -  fatbar :: "('a \<rightarrow> 'b match) \<rightarrow> ('a \<rightarrow> 'b match) \<rightarrow> ('a \<rightarrow> 'b match)" where
    1.19 -  "fatbar = (\<Lambda> a b x. a\<cdot>x +++ b\<cdot>x)"
    1.20 -
    1.21 -abbreviation
    1.22 -  fatbar_syn :: "['a \<rightarrow> 'b match, 'a \<rightarrow> 'b match] \<Rightarrow> 'a \<rightarrow> 'b match" (infixr "\<parallel>" 60)  where
    1.23 -  "m1 \<parallel> m2 == fatbar\<cdot>m1\<cdot>m2"
    1.24 -
    1.25 -lemma fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> (m \<parallel> ms)\<cdot>x = \<bottom>"
    1.26 -by (simp add: fatbar_def)
    1.27 -
    1.28 -lemma fatbar2: "m\<cdot>x = fail \<Longrightarrow> (m \<parallel> ms)\<cdot>x = ms\<cdot>x"
    1.29 -by (simp add: fatbar_def)
    1.30 -
    1.31 -lemma fatbar3: "m\<cdot>x = succeed\<cdot>y \<Longrightarrow> (m \<parallel> ms)\<cdot>x = succeed\<cdot>y"
    1.32 -by (simp add: fatbar_def)
    1.33 -
    1.34 -lemmas fatbar_simps = fatbar1 fatbar2 fatbar3
    1.35 -
    1.36 -lemma run_fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = \<bottom>"
    1.37 -by (simp add: fatbar_def)
    1.38 -
    1.39 -lemma run_fatbar2: "m\<cdot>x = fail \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = run\<cdot>(ms\<cdot>x)"
    1.40 -by (simp add: fatbar_def)
    1.41 -
    1.42 -lemma run_fatbar3: "m\<cdot>x = succeed\<cdot>y \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = y"
    1.43 -by (simp add: fatbar_def)
    1.44 -
    1.45 -lemmas run_fatbar_simps [simp] = run_fatbar1 run_fatbar2 run_fatbar3
    1.46 -
    1.47 -subsection {* Case branch combinator *}
    1.48 -
    1.49 -definition
    1.50 -  branch :: "('a \<rightarrow> 'b match) \<Rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'c match)" where
    1.51 -  "branch p \<equiv> \<Lambda> r x. match_case\<cdot>fail\<cdot>(\<Lambda> y. succeed\<cdot>(r\<cdot>y))\<cdot>(p\<cdot>x)"
    1.52 -
    1.53 -lemma branch_simps:
    1.54 -  "p\<cdot>x = \<bottom> \<Longrightarrow> branch p\<cdot>r\<cdot>x = \<bottom>"
    1.55 -  "p\<cdot>x = fail \<Longrightarrow> branch p\<cdot>r\<cdot>x = fail"
    1.56 -  "p\<cdot>x = succeed\<cdot>y \<Longrightarrow> branch p\<cdot>r\<cdot>x = succeed\<cdot>(r\<cdot>y)"
    1.57 -by (simp_all add: branch_def)
    1.58 -
    1.59 -lemma branch_succeed [simp]: "branch succeed\<cdot>r\<cdot>x = succeed\<cdot>(r\<cdot>x)"
    1.60 -by (simp add: branch_def)
    1.61 -
    1.62 -subsubsection {* Cases operator *}
    1.63 -
    1.64 -definition
    1.65 -  cases :: "'a match \<rightarrow> 'a::pcpo" where
    1.66 -  "cases = match_case\<cdot>\<bottom>\<cdot>ID"
    1.67 -
    1.68 -text {* rewrite rules for cases *}
    1.69 -
    1.70 -lemma cases_strict [simp]: "cases\<cdot>\<bottom> = \<bottom>"
    1.71 -by (simp add: cases_def)
    1.72 -
    1.73 -lemma cases_fail [simp]: "cases\<cdot>fail = \<bottom>"
    1.74 -by (simp add: cases_def)
    1.75 -
    1.76 -lemma cases_succeed [simp]: "cases\<cdot>(succeed\<cdot>x) = x"
    1.77 -by (simp add: cases_def)
    1.78 -
    1.79 -subsection {* Case syntax *}
    1.80 -
    1.81 -nonterminals
    1.82 -  Case_syn  Cases_syn
    1.83 -
    1.84 -syntax
    1.85 -  "_Case_syntax":: "['a, Cases_syn] => 'b"               ("(Case _ of/ _)" 10)
    1.86 -  "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ =>/ _)" 10)
    1.87 -  ""            :: "Case_syn => Cases_syn"               ("_")
    1.88 -  "_Case2"      :: "[Case_syn, Cases_syn] => Cases_syn"  ("_/ | _")
    1.89 -
    1.90 -syntax (xsymbols)
    1.91 -  "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
    1.92 -
    1.93 -translations
    1.94 -  "_Case_syntax x ms" == "CONST Fixrec.cases\<cdot>(ms\<cdot>x)"
    1.95 -  "_Case2 m ms" == "m \<parallel> ms"
    1.96 -
    1.97 -text {* Parsing Case expressions *}
    1.98 -
    1.99 -syntax
   1.100 -  "_pat" :: "'a"
   1.101 -  "_variable" :: "'a"
   1.102 -  "_noargs" :: "'a"
   1.103 -
   1.104 -translations
   1.105 -  "_Case1 p r" => "CONST branch (_pat p)\<cdot>(_variable p r)"
   1.106 -  "_variable (_args x y) r" => "CONST csplit\<cdot>(_variable x (_variable y r))"
   1.107 -  "_variable _noargs r" => "CONST unit_when\<cdot>r"
   1.108 -
   1.109 -parse_translation {*
   1.110 -(* rewrite (_pat x) => (succeed) *)
   1.111 -(* rewrite (_variable x t) => (Abs_CFun (%x. t)) *)
   1.112 - [(@{syntax_const "_pat"}, fn _ => Syntax.const @{const_syntax Fixrec.succeed}),
   1.113 -  mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_CFun})];
   1.114 -*}
   1.115 -
   1.116 -text {* Printing Case expressions *}
   1.117 -
   1.118 -syntax
   1.119 -  "_match" :: "'a"
   1.120 -
   1.121 -print_translation {*
   1.122 -  let
   1.123 -    fun dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax unit_when},_) $ t) =
   1.124 -          (Syntax.const @{syntax_const "_noargs"}, t)
   1.125 -    |   dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax csplit},_) $ t) =
   1.126 -          let
   1.127 -            val (v1, t1) = dest_LAM t;
   1.128 -            val (v2, t2) = dest_LAM t1;
   1.129 -          in (Syntax.const @{syntax_const "_args"} $ v1 $ v2, t2) end
   1.130 -    |   dest_LAM (Const (@{const_syntax Abs_CFun},_) $ t) =
   1.131 -          let
   1.132 -            val abs =
   1.133 -              case t of Abs abs => abs
   1.134 -                | _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0);
   1.135 -            val (x, t') = atomic_abs_tr' abs;
   1.136 -          in (Syntax.const @{syntax_const "_variable"} $ x, t') end
   1.137 -    |   dest_LAM _ = raise Match; (* too few vars: abort translation *)
   1.138 -
   1.139 -    fun Case1_tr' [Const(@{const_syntax branch},_) $ p, r] =
   1.140 -          let val (v, t) = dest_LAM r in
   1.141 -            Syntax.const @{syntax_const "_Case1"} $
   1.142 -              (Syntax.const @{syntax_const "_match"} $ p $ v) $ t
   1.143 -          end;
   1.144 -
   1.145 -  in [(@{const_syntax Rep_CFun}, Case1_tr')] end;
   1.146 -*}
   1.147 -
   1.148 -translations
   1.149 -  "x" <= "_match (CONST Fixrec.succeed) (_variable x)"
   1.150 -
   1.151 -
   1.152 -subsection {* Pattern combinators for data constructors *}
   1.153 -
   1.154 -types ('a, 'b) pat = "'a \<rightarrow> 'b match"
   1.155 -
   1.156 -definition
   1.157 -  cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat" where
   1.158 -  "cpair_pat p1 p2 = (\<Lambda>(x, y).
   1.159 -    match_case\<cdot>fail\<cdot>(\<Lambda> a. match_case\<cdot>fail\<cdot>(\<Lambda> b. succeed\<cdot>(a, b))\<cdot>(p2\<cdot>y))\<cdot>(p1\<cdot>x))"
   1.160 -
   1.161 -definition
   1.162 -  spair_pat ::
   1.163 -  "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a::pcpo \<otimes> 'b::pcpo, 'c \<times> 'd) pat" where
   1.164 -  "spair_pat p1 p2 = (\<Lambda>(:x, y:). cpair_pat p1 p2\<cdot>(x, y))"
   1.165 -
   1.166 -definition
   1.167 -  sinl_pat :: "('a, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat" where
   1.168 -  "sinl_pat p = sscase\<cdot>p\<cdot>(\<Lambda> x. fail)"
   1.169 -
   1.170 -definition
   1.171 -  sinr_pat :: "('b, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat" where
   1.172 -  "sinr_pat p = sscase\<cdot>(\<Lambda> x. fail)\<cdot>p"
   1.173 -
   1.174 -definition
   1.175 -  up_pat :: "('a, 'b) pat \<Rightarrow> ('a u, 'b) pat" where
   1.176 -  "up_pat p = fup\<cdot>p"
   1.177 -
   1.178 -definition
   1.179 -  TT_pat :: "(tr, unit) pat" where
   1.180 -  "TT_pat = (\<Lambda> b. If b then succeed\<cdot>() else fail fi)"
   1.181 -
   1.182 -definition
   1.183 -  FF_pat :: "(tr, unit) pat" where
   1.184 -  "FF_pat = (\<Lambda> b. If b then fail else succeed\<cdot>() fi)"
   1.185 -
   1.186 -definition
   1.187 -  ONE_pat :: "(one, unit) pat" where
   1.188 -  "ONE_pat = (\<Lambda> ONE. succeed\<cdot>())"
   1.189 -
   1.190 -text {* Parse translations (patterns) *}
   1.191 -translations
   1.192 -  "_pat (XCONST Pair x y)" => "CONST cpair_pat (_pat x) (_pat y)"
   1.193 -  "_pat (XCONST spair\<cdot>x\<cdot>y)" => "CONST spair_pat (_pat x) (_pat y)"
   1.194 -  "_pat (XCONST sinl\<cdot>x)" => "CONST sinl_pat (_pat x)"
   1.195 -  "_pat (XCONST sinr\<cdot>x)" => "CONST sinr_pat (_pat x)"
   1.196 -  "_pat (XCONST up\<cdot>x)" => "CONST up_pat (_pat x)"
   1.197 -  "_pat (XCONST TT)" => "CONST TT_pat"
   1.198 -  "_pat (XCONST FF)" => "CONST FF_pat"
   1.199 -  "_pat (XCONST ONE)" => "CONST ONE_pat"
   1.200 -
   1.201 -text {* CONST version is also needed for constructors with special syntax *}
   1.202 -translations
   1.203 -  "_pat (CONST Pair x y)" => "CONST cpair_pat (_pat x) (_pat y)"
   1.204 -  "_pat (CONST spair\<cdot>x\<cdot>y)" => "CONST spair_pat (_pat x) (_pat y)"
   1.205 -
   1.206 -text {* Parse translations (variables) *}
   1.207 -translations
   1.208 -  "_variable (XCONST Pair x y) r" => "_variable (_args x y) r"
   1.209 -  "_variable (XCONST spair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
   1.210 -  "_variable (XCONST sinl\<cdot>x) r" => "_variable x r"
   1.211 -  "_variable (XCONST sinr\<cdot>x) r" => "_variable x r"
   1.212 -  "_variable (XCONST up\<cdot>x) r" => "_variable x r"
   1.213 -  "_variable (XCONST TT) r" => "_variable _noargs r"
   1.214 -  "_variable (XCONST FF) r" => "_variable _noargs r"
   1.215 -  "_variable (XCONST ONE) r" => "_variable _noargs r"
   1.216 -
   1.217 -translations
   1.218 -  "_variable (CONST Pair x y) r" => "_variable (_args x y) r"
   1.219 -  "_variable (CONST spair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
   1.220 -
   1.221 -text {* Print translations *}
   1.222 -translations
   1.223 -  "CONST Pair (_match p1 v1) (_match p2 v2)"
   1.224 -      <= "_match (CONST cpair_pat p1 p2) (_args v1 v2)"
   1.225 -  "CONST spair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
   1.226 -      <= "_match (CONST spair_pat p1 p2) (_args v1 v2)"
   1.227 -  "CONST sinl\<cdot>(_match p1 v1)" <= "_match (CONST sinl_pat p1) v1"
   1.228 -  "CONST sinr\<cdot>(_match p1 v1)" <= "_match (CONST sinr_pat p1) v1"
   1.229 -  "CONST up\<cdot>(_match p1 v1)" <= "_match (CONST up_pat p1) v1"
   1.230 -  "CONST TT" <= "_match (CONST TT_pat) _noargs"
   1.231 -  "CONST FF" <= "_match (CONST FF_pat) _noargs"
   1.232 -  "CONST ONE" <= "_match (CONST ONE_pat) _noargs"
   1.233 -
   1.234 -lemma cpair_pat1:
   1.235 -  "branch p\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>(x, y) = \<bottom>"
   1.236 -apply (simp add: branch_def cpair_pat_def)
   1.237 -apply (cases "p\<cdot>x", simp_all)
   1.238 -done
   1.239 -
   1.240 -lemma cpair_pat2:
   1.241 -  "branch p\<cdot>r\<cdot>x = fail \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>(x, y) = fail"
   1.242 -apply (simp add: branch_def cpair_pat_def)
   1.243 -apply (cases "p\<cdot>x", simp_all)
   1.244 -done
   1.245 -
   1.246 -lemma cpair_pat3:
   1.247 -  "branch p\<cdot>r\<cdot>x = succeed\<cdot>s \<Longrightarrow>
   1.248 -   branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>(x, y) = branch q\<cdot>s\<cdot>y"
   1.249 -apply (simp add: branch_def cpair_pat_def)
   1.250 -apply (cases "p\<cdot>x", simp_all)
   1.251 -apply (cases "q\<cdot>y", simp_all)
   1.252 -done
   1.253 -
   1.254 -lemmas cpair_pat [simp] =
   1.255 -  cpair_pat1 cpair_pat2 cpair_pat3
   1.256 -
   1.257 -lemma spair_pat [simp]:
   1.258 -  "branch (spair_pat p1 p2)\<cdot>r\<cdot>\<bottom> = \<bottom>"
   1.259 -  "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk>
   1.260 -     \<Longrightarrow> branch (spair_pat p1 p2)\<cdot>r\<cdot>(:x, y:) =
   1.261 -         branch (cpair_pat p1 p2)\<cdot>r\<cdot>(x, y)"
   1.262 -by (simp_all add: branch_def spair_pat_def)
   1.263 -
   1.264 -lemma sinl_pat [simp]:
   1.265 -  "branch (sinl_pat p)\<cdot>r\<cdot>\<bottom> = \<bottom>"
   1.266 -  "x \<noteq> \<bottom> \<Longrightarrow> branch (sinl_pat p)\<cdot>r\<cdot>(sinl\<cdot>x) = branch p\<cdot>r\<cdot>x"
   1.267 -  "y \<noteq> \<bottom> \<Longrightarrow> branch (sinl_pat p)\<cdot>r\<cdot>(sinr\<cdot>y) = fail"
   1.268 -by (simp_all add: branch_def sinl_pat_def)
   1.269 -
   1.270 -lemma sinr_pat [simp]:
   1.271 -  "branch (sinr_pat p)\<cdot>r\<cdot>\<bottom> = \<bottom>"
   1.272 -  "x \<noteq> \<bottom> \<Longrightarrow> branch (sinr_pat p)\<cdot>r\<cdot>(sinl\<cdot>x) = fail"
   1.273 -  "y \<noteq> \<bottom> \<Longrightarrow> branch (sinr_pat p)\<cdot>r\<cdot>(sinr\<cdot>y) = branch p\<cdot>r\<cdot>y"
   1.274 -by (simp_all add: branch_def sinr_pat_def)
   1.275 -
   1.276 -lemma up_pat [simp]:
   1.277 -  "branch (up_pat p)\<cdot>r\<cdot>\<bottom> = \<bottom>"
   1.278 -  "branch (up_pat p)\<cdot>r\<cdot>(up\<cdot>x) = branch p\<cdot>r\<cdot>x"
   1.279 -by (simp_all add: branch_def up_pat_def)
   1.280 -
   1.281 -lemma TT_pat [simp]:
   1.282 -  "branch TT_pat\<cdot>(unit_when\<cdot>r)\<cdot>\<bottom> = \<bottom>"
   1.283 -  "branch TT_pat\<cdot>(unit_when\<cdot>r)\<cdot>TT = succeed\<cdot>r"
   1.284 -  "branch TT_pat\<cdot>(unit_when\<cdot>r)\<cdot>FF = fail"
   1.285 -by (simp_all add: branch_def TT_pat_def)
   1.286 -
   1.287 -lemma FF_pat [simp]:
   1.288 -  "branch FF_pat\<cdot>(unit_when\<cdot>r)\<cdot>\<bottom> = \<bottom>"
   1.289 -  "branch FF_pat\<cdot>(unit_when\<cdot>r)\<cdot>TT = fail"
   1.290 -  "branch FF_pat\<cdot>(unit_when\<cdot>r)\<cdot>FF = succeed\<cdot>r"
   1.291 -by (simp_all add: branch_def FF_pat_def)
   1.292 -
   1.293 -lemma ONE_pat [simp]:
   1.294 -  "branch ONE_pat\<cdot>(unit_when\<cdot>r)\<cdot>\<bottom> = \<bottom>"
   1.295 -  "branch ONE_pat\<cdot>(unit_when\<cdot>r)\<cdot>ONE = succeed\<cdot>r"
   1.296 -by (simp_all add: branch_def ONE_pat_def)
   1.297 -
   1.298 -
   1.299 -subsection {* Wildcards, as-patterns, and lazy patterns *}
   1.300 -
   1.301 -definition
   1.302 -  wild_pat :: "'a \<rightarrow> unit match" where
   1.303 -  "wild_pat = (\<Lambda> x. succeed\<cdot>())"
   1.304 -
   1.305 -definition
   1.306 -  as_pat :: "('a \<rightarrow> 'b match) \<Rightarrow> 'a \<rightarrow> ('a \<times> 'b) match" where
   1.307 -  "as_pat p = (\<Lambda> x. match_case\<cdot>fail\<cdot>(\<Lambda> a. succeed\<cdot>(x, a))\<cdot>(p\<cdot>x))"
   1.308 -
   1.309 -definition
   1.310 -  lazy_pat :: "('a \<rightarrow> 'b::pcpo match) \<Rightarrow> ('a \<rightarrow> 'b match)" where
   1.311 -  "lazy_pat p = (\<Lambda> x. succeed\<cdot>(cases\<cdot>(p\<cdot>x)))"
   1.312 -
   1.313 -text {* Parse translations (patterns) *}
   1.314 -translations
   1.315 -  "_pat _" => "CONST wild_pat"
   1.316 -
   1.317 -text {* Parse translations (variables) *}
   1.318 -translations
   1.319 -  "_variable _ r" => "_variable _noargs r"
   1.320 -
   1.321 -text {* Print translations *}
   1.322 -translations
   1.323 -  "_" <= "_match (CONST wild_pat) _noargs"
   1.324 -
   1.325 -lemma wild_pat [simp]: "branch wild_pat\<cdot>(unit_when\<cdot>r)\<cdot>x = succeed\<cdot>r"
   1.326 -by (simp add: branch_def wild_pat_def)
   1.327 -
   1.328 -lemma as_pat [simp]:
   1.329 -  "branch (as_pat p)\<cdot>(csplit\<cdot>r)\<cdot>x = branch p\<cdot>(r\<cdot>x)\<cdot>x"
   1.330 -apply (simp add: branch_def as_pat_def)
   1.331 -apply (cases "p\<cdot>x", simp_all)
   1.332 -done
   1.333 -
   1.334 -lemma lazy_pat [simp]:
   1.335 -  "branch p\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> branch (lazy_pat p)\<cdot>r\<cdot>x = succeed\<cdot>(r\<cdot>\<bottom>)"
   1.336 -  "branch p\<cdot>r\<cdot>x = fail \<Longrightarrow> branch (lazy_pat p)\<cdot>r\<cdot>x = succeed\<cdot>(r\<cdot>\<bottom>)"
   1.337 -  "branch p\<cdot>r\<cdot>x = succeed\<cdot>s \<Longrightarrow> branch (lazy_pat p)\<cdot>r\<cdot>x = succeed\<cdot>s"
   1.338 -apply (simp_all add: branch_def lazy_pat_def)
   1.339 -apply (cases "p\<cdot>x", simp_all)+
   1.340 -done
   1.341 -
   1.342 -
   1.343  subsection {* Match functions for built-in types *}
   1.344  
   1.345  default_sort pcpo
   1.346 @@ -584,6 +255,6 @@
   1.347        (@{const_name UU}, @{const_name match_UU}) ]
   1.348  *}
   1.349  
   1.350 -hide_const (open) succeed fail run cases
   1.351 +hide_const (open) succeed fail run
   1.352  
   1.353  end
     2.1 --- a/src/HOLCF/IsaMakefile	Mon May 24 09:32:52 2010 -0700
     2.2 +++ b/src/HOLCF/IsaMakefile	Mon May 24 11:29:49 2010 -0700
     2.3 @@ -115,6 +115,7 @@
     2.4    ex/Hoare.thy \
     2.5    ex/Letrec.thy \
     2.6    ex/Loop.thy \
     2.7 +  ex/Pattern_Match.thy \
     2.8    ex/Powerdomain_ex.thy \
     2.9    ex/Stream.thy \
    2.10    ex/Strict_Fun.thy \
     3.1 --- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Mon May 24 09:32:52 2010 -0700
     3.2 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Mon May 24 11:29:49 2010 -0700
     3.3 @@ -25,8 +25,7 @@
     3.4             cases : thm list,
     3.5             sel_rews : thm list,
     3.6             dis_rews : thm list,
     3.7 -           match_rews : thm list,
     3.8 -           pat_rews : thm list
     3.9 +           match_rews : thm list
    3.10           } * theory;
    3.11  end;
    3.12  
    3.13 @@ -824,162 +823,6 @@
    3.14    end;
    3.15  
    3.16  (******************************************************************************)
    3.17 -(************** definitions and theorems for pattern combinators **************)
    3.18 -(******************************************************************************)
    3.19 -
    3.20 -fun add_pattern_combinators
    3.21 -    (bindings : binding list)
    3.22 -    (spec : (term * (bool * typ) list) list)
    3.23 -    (lhsT : typ)
    3.24 -    (exhaust : thm)
    3.25 -    (case_const : typ -> term)
    3.26 -    (case_rews : thm list)
    3.27 -    (thy : theory) =
    3.28 -  let
    3.29 -
    3.30 -    (* utility functions *)
    3.31 -    fun mk_pair_pat (p1, p2) =
    3.32 -      let
    3.33 -        val T1 = fastype_of p1;
    3.34 -        val T2 = fastype_of p2;
    3.35 -        val (U1, V1) = apsnd dest_matchT (dest_cfunT T1);
    3.36 -        val (U2, V2) = apsnd dest_matchT (dest_cfunT T2);
    3.37 -        val pat_typ = [T1, T2] --->
    3.38 -            (mk_prodT (U1, U2) ->> mk_matchT (mk_prodT (V1, V2)));
    3.39 -        val pat_const = Const (@{const_name cpair_pat}, pat_typ);
    3.40 -      in
    3.41 -        pat_const $ p1 $ p2
    3.42 -      end;
    3.43 -    fun mk_tuple_pat [] = succeed_const HOLogic.unitT
    3.44 -      | mk_tuple_pat ps = foldr1 mk_pair_pat ps;
    3.45 -    fun branch_const (T,U,V) = 
    3.46 -      Const (@{const_name branch},
    3.47 -        (T ->> mk_matchT U) --> (U ->> V) ->> T ->> mk_matchT V);
    3.48 -
    3.49 -    (* define pattern combinators *)
    3.50 -    local
    3.51 -      val tns = map (fst o dest_TFree) (snd (dest_Type lhsT));
    3.52 -
    3.53 -      fun pat_eqn (i, (bind, (con, args))) : binding * term * mixfix =
    3.54 -        let
    3.55 -          val pat_bind = Binding.suffix_name "_pat" bind;
    3.56 -          val Ts = map snd args;
    3.57 -          val Vs =
    3.58 -              (map (K "'t") args)
    3.59 -              |> Datatype_Prop.indexify_names
    3.60 -              |> Name.variant_list tns
    3.61 -              |> map (fn t => TFree (t, @{sort pcpo}));
    3.62 -          val patNs = Datatype_Prop.indexify_names (map (K "pat") args);
    3.63 -          val patTs = map2 (fn T => fn V => T ->> mk_matchT V) Ts Vs;
    3.64 -          val pats = map Free (patNs ~~ patTs);
    3.65 -          val fail = mk_fail (mk_tupleT Vs);
    3.66 -          val (vs, nonlazy) = get_vars_avoiding patNs args;
    3.67 -          val rhs = big_lambdas vs (mk_tuple_pat pats ` mk_tuple vs);
    3.68 -          fun one_fun (j, (_, args')) =
    3.69 -            let
    3.70 -              val (vs', nonlazy) = get_vars_avoiding patNs args';
    3.71 -            in if i = j then rhs else big_lambdas vs' fail end;
    3.72 -          val funs = map_index one_fun spec;
    3.73 -          val body = list_ccomb (case_const (mk_matchT (mk_tupleT Vs)), funs);
    3.74 -        in
    3.75 -          (pat_bind, lambdas pats body, NoSyn)
    3.76 -        end;
    3.77 -    in
    3.78 -      val ((pat_consts, pat_defs), thy) =
    3.79 -          define_consts (map_index pat_eqn (bindings ~~ spec)) thy
    3.80 -    end;
    3.81 -
    3.82 -    (* syntax translations for pattern combinators *)
    3.83 -    local
    3.84 -      open Syntax
    3.85 -      fun syntax c = Syntax.mark_const (fst (dest_Const c));
    3.86 -      fun app s (l, r) = Syntax.mk_appl (Constant s) [l, r];
    3.87 -      val capp = app @{const_syntax Rep_CFun};
    3.88 -      val capps = Library.foldl capp
    3.89 -
    3.90 -      fun app_var x = Syntax.mk_appl (Constant "_variable") [x, Variable "rhs"];
    3.91 -      fun app_pat x = Syntax.mk_appl (Constant "_pat") [x];
    3.92 -      fun args_list [] = Constant "_noargs"
    3.93 -        | args_list xs = foldr1 (app "_args") xs;
    3.94 -      fun one_case_trans (pat, (con, args)) =
    3.95 -        let
    3.96 -          val cname = Constant (syntax con);
    3.97 -          val pname = Constant (syntax pat);
    3.98 -          val ns = 1 upto length args;
    3.99 -          val xs = map (fn n => Variable ("x"^(string_of_int n))) ns;
   3.100 -          val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
   3.101 -          val vs = map (fn n => Variable ("v"^(string_of_int n))) ns;
   3.102 -        in
   3.103 -          [ParseRule (app_pat (capps (cname, xs)),
   3.104 -                      mk_appl pname (map app_pat xs)),
   3.105 -           ParseRule (app_var (capps (cname, xs)),
   3.106 -                      app_var (args_list xs)),
   3.107 -           PrintRule (capps (cname, ListPair.map (app "_match") (ps,vs)),
   3.108 -                      app "_match" (mk_appl pname ps, args_list vs))]
   3.109 -        end;
   3.110 -      val trans_rules : Syntax.ast Syntax.trrule list =
   3.111 -          maps one_case_trans (pat_consts ~~ spec);
   3.112 -    in
   3.113 -      val thy = Sign.add_trrules_i trans_rules thy;
   3.114 -    end;
   3.115 -
   3.116 -    (* prove strictness and reduction rules of pattern combinators *)
   3.117 -    local
   3.118 -      val tns = map (fst o dest_TFree) (snd (dest_Type lhsT));
   3.119 -      val rn = Name.variant tns "'r";
   3.120 -      val R = TFree (rn, @{sort pcpo});
   3.121 -      fun pat_lhs (pat, args) =
   3.122 -        let
   3.123 -          val Ts = map snd args;
   3.124 -          val Vs =
   3.125 -              (map (K "'t") args)
   3.126 -              |> Datatype_Prop.indexify_names
   3.127 -              |> Name.variant_list (rn::tns)
   3.128 -              |> map (fn t => TFree (t, @{sort pcpo}));
   3.129 -          val patNs = Datatype_Prop.indexify_names (map (K "pat") args);
   3.130 -          val patTs = map2 (fn T => fn V => T ->> mk_matchT V) Ts Vs;
   3.131 -          val pats = map Free (patNs ~~ patTs);
   3.132 -          val k = Free ("rhs", mk_tupleT Vs ->> R);
   3.133 -          val branch1 = branch_const (lhsT, mk_tupleT Vs, R);
   3.134 -          val fun1 = (branch1 $ list_comb (pat, pats)) ` k;
   3.135 -          val branch2 = branch_const (mk_tupleT Ts, mk_tupleT Vs, R);
   3.136 -          val fun2 = (branch2 $ mk_tuple_pat pats) ` k;
   3.137 -          val taken = "rhs" :: patNs;
   3.138 -        in (fun1, fun2, taken) end;
   3.139 -      fun pat_strict (pat, (con, args)) =
   3.140 -        let
   3.141 -          val (fun1, fun2, taken) = pat_lhs (pat, args);
   3.142 -          val defs = @{thm branch_def} :: pat_defs;
   3.143 -          val goal = mk_trp (mk_strict fun1);
   3.144 -          val rules = @{thms match_case_simps} @ case_rews;
   3.145 -          val tacs = [simp_tac (beta_ss addsimps rules) 1];
   3.146 -        in prove thy defs goal (K tacs) end;
   3.147 -      fun pat_apps (i, (pat, (con, args))) =
   3.148 -        let
   3.149 -          val (fun1, fun2, taken) = pat_lhs (pat, args);
   3.150 -          fun pat_app (j, (con', args')) =
   3.151 -            let
   3.152 -              val (vs, nonlazy) = get_vars_avoiding taken args';
   3.153 -              val con_app = list_ccomb (con', vs);
   3.154 -              val assms = map (mk_trp o mk_defined) nonlazy;
   3.155 -              val rhs = if i = j then fun2 ` mk_tuple vs else mk_fail R;
   3.156 -              val concl = mk_trp (mk_eq (fun1 ` con_app, rhs));
   3.157 -              val goal = Logic.list_implies (assms, concl);
   3.158 -              val defs = @{thm branch_def} :: pat_defs;
   3.159 -              val rules = @{thms match_case_simps} @ case_rews;
   3.160 -              val tacs = [asm_simp_tac (beta_ss addsimps rules) 1];
   3.161 -            in prove thy defs goal (K tacs) end;
   3.162 -        in map_index pat_app spec end;
   3.163 -    in
   3.164 -      val pat_stricts = map pat_strict (pat_consts ~~ spec);
   3.165 -      val pat_apps = flat (map_index pat_apps (pat_consts ~~ spec));
   3.166 -    end;
   3.167 -
   3.168 -  in
   3.169 -    (pat_stricts @ pat_apps, thy)
   3.170 -  end
   3.171 -
   3.172 -(******************************************************************************)
   3.173  (******************************* main function ********************************)
   3.174  (******************************************************************************)
   3.175  
   3.176 @@ -1061,18 +904,6 @@
   3.177            exhaust case_const cases thy
   3.178        end
   3.179  
   3.180 -    (* define and prove theorems for pattern combinators *)
   3.181 -    val (pat_thms : thm list, thy : theory) =
   3.182 -      let
   3.183 -        val bindings = map #1 spec;
   3.184 -        fun prep_arg (lazy, sel, T) = (lazy, T);
   3.185 -        fun prep_con c (b, args, mx) = (c, map prep_arg args);
   3.186 -        val pat_spec = map2 prep_con con_consts spec;
   3.187 -      in
   3.188 -        add_pattern_combinators bindings pat_spec lhsT
   3.189 -          exhaust case_const cases thy
   3.190 -      end
   3.191 -
   3.192      (* restore original signature path *)
   3.193      val thy = Sign.parent_path thy;
   3.194  
   3.195 @@ -1090,8 +921,7 @@
   3.196          cases = cases,
   3.197          sel_rews = sel_thms,
   3.198          dis_rews = dis_thms,
   3.199 -        match_rews = match_thms,
   3.200 -        pat_rews = pat_thms };
   3.201 +        match_rews = match_thms };
   3.202    in
   3.203      (result, thy)
   3.204    end;
     4.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon May 24 09:32:52 2010 -0700
     4.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon May 24 11:29:49 2010 -0700
     4.3 @@ -145,7 +145,6 @@
     4.4  val when_strict = hd when_rews;
     4.5  val dis_rews = #dis_rews result;
     4.6  val mat_rews = #match_rews result;
     4.7 -val pat_rews = #pat_rews result;
     4.8  
     4.9  (* ----- theorems concerning the isomorphism -------------------------------- *)
    4.10  
    4.11 @@ -211,7 +210,6 @@
    4.12       ((qualified "con_rews"  , con_rews    ), [simp]),
    4.13       ((qualified "sel_rews"  , sel_rews    ), [simp]),
    4.14       ((qualified "dis_rews"  , dis_rews    ), [simp]),
    4.15 -     ((qualified "pat_rews"  , pat_rews    ), [simp]),
    4.16       ((qualified "dist_les"  , dist_les    ), [simp]),
    4.17       ((qualified "dist_eqs"  , dist_eqs    ), [simp]),
    4.18       ((qualified "inverts"   , inverts     ), [simp]),
    4.19 @@ -220,7 +218,7 @@
    4.20       ((qualified "match_rews", mat_rews    ), [simp])]
    4.21    |> snd
    4.22    |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
    4.23 -      pat_rews @ dist_les @ dist_eqs)
    4.24 +      dist_les @ dist_eqs)
    4.25  end; (* let *)
    4.26  
    4.27  (******************************************************************************)
     5.1 --- a/src/HOLCF/Tutorial/Domain_ex.thy	Mon May 24 09:32:52 2010 -0700
     5.2 +++ b/src/HOLCF/Tutorial/Domain_ex.thy	Mon May 24 11:29:49 2010 -0700
     5.3 @@ -154,11 +154,6 @@
     5.4  term is_Node
     5.5  thm tree.dis_rews
     5.6  
     5.7 -text {* Rules about pattern match combinators *}
     5.8 -term Leaf_pat
     5.9 -term Node_pat
    5.10 -thm tree.pat_rews
    5.11 -
    5.12  text {* Rules about monadic pattern match combinators *}
    5.13  term match_Leaf
    5.14  term match_Node
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOLCF/ex/Pattern_Match.thy	Mon May 24 11:29:49 2010 -0700
     6.3 @@ -0,0 +1,591 @@
     6.4 +(*  Title:      HOLCF/ex/Pattern_Match.thy
     6.5 +    Author:     Brian Huffman
     6.6 +*)
     6.7 +
     6.8 +header {* An experimental pattern-matching notation *}
     6.9 +
    6.10 +theory Pattern_Match
    6.11 +imports HOLCF
    6.12 +begin
    6.13 +
    6.14 +text {* FIXME: Find a proper way to un-hide constants. *}
    6.15 +
    6.16 +abbreviation fail :: "'a match"
    6.17 +where "fail \<equiv> Fixrec.fail"
    6.18 +
    6.19 +abbreviation succeed :: "'a \<rightarrow> 'a match"
    6.20 +where "succeed \<equiv> Fixrec.succeed"
    6.21 +
    6.22 +abbreviation run :: "'a match \<rightarrow> 'a"
    6.23 +where "run \<equiv> Fixrec.run"
    6.24 +
    6.25 +subsection {* Fatbar combinator *}
    6.26 +
    6.27 +definition
    6.28 +  fatbar :: "('a \<rightarrow> 'b match) \<rightarrow> ('a \<rightarrow> 'b match) \<rightarrow> ('a \<rightarrow> 'b match)" where
    6.29 +  "fatbar = (\<Lambda> a b x. a\<cdot>x +++ b\<cdot>x)"
    6.30 +
    6.31 +abbreviation
    6.32 +  fatbar_syn :: "['a \<rightarrow> 'b match, 'a \<rightarrow> 'b match] \<Rightarrow> 'a \<rightarrow> 'b match" (infixr "\<parallel>" 60)  where
    6.33 +  "m1 \<parallel> m2 == fatbar\<cdot>m1\<cdot>m2"
    6.34 +
    6.35 +lemma fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> (m \<parallel> ms)\<cdot>x = \<bottom>"
    6.36 +by (simp add: fatbar_def)
    6.37 +
    6.38 +lemma fatbar2: "m\<cdot>x = fail \<Longrightarrow> (m \<parallel> ms)\<cdot>x = ms\<cdot>x"
    6.39 +by (simp add: fatbar_def)
    6.40 +
    6.41 +lemma fatbar3: "m\<cdot>x = succeed\<cdot>y \<Longrightarrow> (m \<parallel> ms)\<cdot>x = succeed\<cdot>y"
    6.42 +by (simp add: fatbar_def)
    6.43 +
    6.44 +lemmas fatbar_simps = fatbar1 fatbar2 fatbar3
    6.45 +
    6.46 +lemma run_fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = \<bottom>"
    6.47 +by (simp add: fatbar_def)
    6.48 +
    6.49 +lemma run_fatbar2: "m\<cdot>x = fail \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = run\<cdot>(ms\<cdot>x)"
    6.50 +by (simp add: fatbar_def)
    6.51 +
    6.52 +lemma run_fatbar3: "m\<cdot>x = succeed\<cdot>y \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = y"
    6.53 +by (simp add: fatbar_def)
    6.54 +
    6.55 +lemmas run_fatbar_simps [simp] = run_fatbar1 run_fatbar2 run_fatbar3
    6.56 +
    6.57 +subsection {* Case branch combinator *}
    6.58 +
    6.59 +definition
    6.60 +  branch :: "('a \<rightarrow> 'b match) \<Rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'c match)" where
    6.61 +  "branch p \<equiv> \<Lambda> r x. match_case\<cdot>fail\<cdot>(\<Lambda> y. succeed\<cdot>(r\<cdot>y))\<cdot>(p\<cdot>x)"
    6.62 +
    6.63 +lemma branch_simps:
    6.64 +  "p\<cdot>x = \<bottom> \<Longrightarrow> branch p\<cdot>r\<cdot>x = \<bottom>"
    6.65 +  "p\<cdot>x = fail \<Longrightarrow> branch p\<cdot>r\<cdot>x = fail"
    6.66 +  "p\<cdot>x = succeed\<cdot>y \<Longrightarrow> branch p\<cdot>r\<cdot>x = succeed\<cdot>(r\<cdot>y)"
    6.67 +by (simp_all add: branch_def)
    6.68 +
    6.69 +lemma branch_succeed [simp]: "branch succeed\<cdot>r\<cdot>x = succeed\<cdot>(r\<cdot>x)"
    6.70 +by (simp add: branch_def)
    6.71 +
    6.72 +subsection {* Cases operator *}
    6.73 +
    6.74 +definition
    6.75 +  cases :: "'a match \<rightarrow> 'a::pcpo" where
    6.76 +  "cases = match_case\<cdot>\<bottom>\<cdot>ID"
    6.77 +
    6.78 +text {* rewrite rules for cases *}
    6.79 +
    6.80 +lemma cases_strict [simp]: "cases\<cdot>\<bottom> = \<bottom>"
    6.81 +by (simp add: cases_def)
    6.82 +
    6.83 +lemma cases_fail [simp]: "cases\<cdot>fail = \<bottom>"
    6.84 +by (simp add: cases_def)
    6.85 +
    6.86 +lemma cases_succeed [simp]: "cases\<cdot>(succeed\<cdot>x) = x"
    6.87 +by (simp add: cases_def)
    6.88 +
    6.89 +subsection {* Case syntax *}
    6.90 +
    6.91 +nonterminals
    6.92 +  Case_syn  Cases_syn
    6.93 +
    6.94 +syntax
    6.95 +  "_Case_syntax":: "['a, Cases_syn] => 'b"               ("(Case _ of/ _)" 10)
    6.96 +  "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ =>/ _)" 10)
    6.97 +  ""            :: "Case_syn => Cases_syn"               ("_")
    6.98 +  "_Case2"      :: "[Case_syn, Cases_syn] => Cases_syn"  ("_/ | _")
    6.99 +
   6.100 +syntax (xsymbols)
   6.101 +  "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
   6.102 +
   6.103 +translations
   6.104 +  "_Case_syntax x ms" == "CONST cases\<cdot>(ms\<cdot>x)"
   6.105 +  "_Case2 m ms" == "m \<parallel> ms"
   6.106 +
   6.107 +text {* Parsing Case expressions *}
   6.108 +
   6.109 +syntax
   6.110 +  "_pat" :: "'a"
   6.111 +  "_variable" :: "'a"
   6.112 +  "_noargs" :: "'a"
   6.113 +
   6.114 +translations
   6.115 +  "_Case1 p r" => "CONST branch (_pat p)\<cdot>(_variable p r)"
   6.116 +  "_variable (_args x y) r" => "CONST csplit\<cdot>(_variable x (_variable y r))"
   6.117 +  "_variable _noargs r" => "CONST unit_when\<cdot>r"
   6.118 +
   6.119 +parse_translation {*
   6.120 +(* rewrite (_pat x) => (succeed) *)
   6.121 +(* rewrite (_variable x t) => (Abs_CFun (%x. t)) *)
   6.122 + [(@{syntax_const "_pat"}, fn _ => Syntax.const @{const_syntax Fixrec.succeed}),
   6.123 +  mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_CFun})];
   6.124 +*}
   6.125 +
   6.126 +text {* Printing Case expressions *}
   6.127 +
   6.128 +syntax
   6.129 +  "_match" :: "'a"
   6.130 +
   6.131 +print_translation {*
   6.132 +  let
   6.133 +    fun dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax unit_when},_) $ t) =
   6.134 +          (Syntax.const @{syntax_const "_noargs"}, t)
   6.135 +    |   dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax csplit},_) $ t) =
   6.136 +          let
   6.137 +            val (v1, t1) = dest_LAM t;
   6.138 +            val (v2, t2) = dest_LAM t1;
   6.139 +          in (Syntax.const @{syntax_const "_args"} $ v1 $ v2, t2) end
   6.140 +    |   dest_LAM (Const (@{const_syntax Abs_CFun},_) $ t) =
   6.141 +          let
   6.142 +            val abs =
   6.143 +              case t of Abs abs => abs
   6.144 +                | _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0);
   6.145 +            val (x, t') = atomic_abs_tr' abs;
   6.146 +          in (Syntax.const @{syntax_const "_variable"} $ x, t') end
   6.147 +    |   dest_LAM _ = raise Match; (* too few vars: abort translation *)
   6.148 +
   6.149 +    fun Case1_tr' [Const(@{const_syntax branch},_) $ p, r] =
   6.150 +          let val (v, t) = dest_LAM r in
   6.151 +            Syntax.const @{syntax_const "_Case1"} $
   6.152 +              (Syntax.const @{syntax_const "_match"} $ p $ v) $ t
   6.153 +          end;
   6.154 +
   6.155 +  in [(@{const_syntax Rep_CFun}, Case1_tr')] end;
   6.156 +*}
   6.157 +
   6.158 +translations
   6.159 +  "x" <= "_match (CONST succeed) (_variable x)"
   6.160 +
   6.161 +
   6.162 +subsection {* Pattern combinators for data constructors *}
   6.163 +
   6.164 +types ('a, 'b) pat = "'a \<rightarrow> 'b match"
   6.165 +
   6.166 +definition
   6.167 +  cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat" where
   6.168 +  "cpair_pat p1 p2 = (\<Lambda>(x, y).
   6.169 +    match_case\<cdot>fail\<cdot>(\<Lambda> a. match_case\<cdot>fail\<cdot>(\<Lambda> b. succeed\<cdot>(a, b))\<cdot>(p2\<cdot>y))\<cdot>(p1\<cdot>x))"
   6.170 +
   6.171 +definition
   6.172 +  spair_pat ::
   6.173 +  "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a::pcpo \<otimes> 'b::pcpo, 'c \<times> 'd) pat" where
   6.174 +  "spair_pat p1 p2 = (\<Lambda>(:x, y:). cpair_pat p1 p2\<cdot>(x, y))"
   6.175 +
   6.176 +definition
   6.177 +  sinl_pat :: "('a, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat" where
   6.178 +  "sinl_pat p = sscase\<cdot>p\<cdot>(\<Lambda> x. fail)"
   6.179 +
   6.180 +definition
   6.181 +  sinr_pat :: "('b, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat" where
   6.182 +  "sinr_pat p = sscase\<cdot>(\<Lambda> x. fail)\<cdot>p"
   6.183 +
   6.184 +definition
   6.185 +  up_pat :: "('a, 'b) pat \<Rightarrow> ('a u, 'b) pat" where
   6.186 +  "up_pat p = fup\<cdot>p"
   6.187 +
   6.188 +definition
   6.189 +  TT_pat :: "(tr, unit) pat" where
   6.190 +  "TT_pat = (\<Lambda> b. If b then succeed\<cdot>() else fail fi)"
   6.191 +
   6.192 +definition
   6.193 +  FF_pat :: "(tr, unit) pat" where
   6.194 +  "FF_pat = (\<Lambda> b. If b then fail else succeed\<cdot>() fi)"
   6.195 +
   6.196 +definition
   6.197 +  ONE_pat :: "(one, unit) pat" where
   6.198 +  "ONE_pat = (\<Lambda> ONE. succeed\<cdot>())"
   6.199 +
   6.200 +text {* Parse translations (patterns) *}
   6.201 +translations
   6.202 +  "_pat (XCONST Pair x y)" => "CONST cpair_pat (_pat x) (_pat y)"
   6.203 +  "_pat (XCONST spair\<cdot>x\<cdot>y)" => "CONST spair_pat (_pat x) (_pat y)"
   6.204 +  "_pat (XCONST sinl\<cdot>x)" => "CONST sinl_pat (_pat x)"
   6.205 +  "_pat (XCONST sinr\<cdot>x)" => "CONST sinr_pat (_pat x)"
   6.206 +  "_pat (XCONST up\<cdot>x)" => "CONST up_pat (_pat x)"
   6.207 +  "_pat (XCONST TT)" => "CONST TT_pat"
   6.208 +  "_pat (XCONST FF)" => "CONST FF_pat"
   6.209 +  "_pat (XCONST ONE)" => "CONST ONE_pat"
   6.210 +
   6.211 +text {* CONST version is also needed for constructors with special syntax *}
   6.212 +translations
   6.213 +  "_pat (CONST Pair x y)" => "CONST cpair_pat (_pat x) (_pat y)"
   6.214 +  "_pat (CONST spair\<cdot>x\<cdot>y)" => "CONST spair_pat (_pat x) (_pat y)"
   6.215 +
   6.216 +text {* Parse translations (variables) *}
   6.217 +translations
   6.218 +  "_variable (XCONST Pair x y) r" => "_variable (_args x y) r"
   6.219 +  "_variable (XCONST spair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
   6.220 +  "_variable (XCONST sinl\<cdot>x) r" => "_variable x r"
   6.221 +  "_variable (XCONST sinr\<cdot>x) r" => "_variable x r"
   6.222 +  "_variable (XCONST up\<cdot>x) r" => "_variable x r"
   6.223 +  "_variable (XCONST TT) r" => "_variable _noargs r"
   6.224 +  "_variable (XCONST FF) r" => "_variable _noargs r"
   6.225 +  "_variable (XCONST ONE) r" => "_variable _noargs r"
   6.226 +
   6.227 +translations
   6.228 +  "_variable (CONST Pair x y) r" => "_variable (_args x y) r"
   6.229 +  "_variable (CONST spair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
   6.230 +
   6.231 +text {* Print translations *}
   6.232 +translations
   6.233 +  "CONST Pair (_match p1 v1) (_match p2 v2)"
   6.234 +      <= "_match (CONST cpair_pat p1 p2) (_args v1 v2)"
   6.235 +  "CONST spair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
   6.236 +      <= "_match (CONST spair_pat p1 p2) (_args v1 v2)"
   6.237 +  "CONST sinl\<cdot>(_match p1 v1)" <= "_match (CONST sinl_pat p1) v1"
   6.238 +  "CONST sinr\<cdot>(_match p1 v1)" <= "_match (CONST sinr_pat p1) v1"
   6.239 +  "CONST up\<cdot>(_match p1 v1)" <= "_match (CONST up_pat p1) v1"
   6.240 +  "CONST TT" <= "_match (CONST TT_pat) _noargs"
   6.241 +  "CONST FF" <= "_match (CONST FF_pat) _noargs"
   6.242 +  "CONST ONE" <= "_match (CONST ONE_pat) _noargs"
   6.243 +
   6.244 +lemma cpair_pat1:
   6.245 +  "branch p\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>(x, y) = \<bottom>"
   6.246 +apply (simp add: branch_def cpair_pat_def)
   6.247 +apply (cases "p\<cdot>x", simp_all)
   6.248 +done
   6.249 +
   6.250 +lemma cpair_pat2:
   6.251 +  "branch p\<cdot>r\<cdot>x = fail \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>(x, y) = fail"
   6.252 +apply (simp add: branch_def cpair_pat_def)
   6.253 +apply (cases "p\<cdot>x", simp_all)
   6.254 +done
   6.255 +
   6.256 +lemma cpair_pat3:
   6.257 +  "branch p\<cdot>r\<cdot>x = succeed\<cdot>s \<Longrightarrow>
   6.258 +   branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>(x, y) = branch q\<cdot>s\<cdot>y"
   6.259 +apply (simp add: branch_def cpair_pat_def)
   6.260 +apply (cases "p\<cdot>x", simp_all)
   6.261 +apply (cases "q\<cdot>y", simp_all)
   6.262 +done
   6.263 +
   6.264 +lemmas cpair_pat [simp] =
   6.265 +  cpair_pat1 cpair_pat2 cpair_pat3
   6.266 +
   6.267 +lemma spair_pat [simp]:
   6.268 +  "branch (spair_pat p1 p2)\<cdot>r\<cdot>\<bottom> = \<bottom>"
   6.269 +  "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk>
   6.270 +     \<Longrightarrow> branch (spair_pat p1 p2)\<cdot>r\<cdot>(:x, y:) =
   6.271 +         branch (cpair_pat p1 p2)\<cdot>r\<cdot>(x, y)"
   6.272 +by (simp_all add: branch_def spair_pat_def)
   6.273 +
   6.274 +lemma sinl_pat [simp]:
   6.275 +  "branch (sinl_pat p)\<cdot>r\<cdot>\<bottom> = \<bottom>"
   6.276 +  "x \<noteq> \<bottom> \<Longrightarrow> branch (sinl_pat p)\<cdot>r\<cdot>(sinl\<cdot>x) = branch p\<cdot>r\<cdot>x"
   6.277 +  "y \<noteq> \<bottom> \<Longrightarrow> branch (sinl_pat p)\<cdot>r\<cdot>(sinr\<cdot>y) = fail"
   6.278 +by (simp_all add: branch_def sinl_pat_def)
   6.279 +
   6.280 +lemma sinr_pat [simp]:
   6.281 +  "branch (sinr_pat p)\<cdot>r\<cdot>\<bottom> = \<bottom>"
   6.282 +  "x \<noteq> \<bottom> \<Longrightarrow> branch (sinr_pat p)\<cdot>r\<cdot>(sinl\<cdot>x) = fail"
   6.283 +  "y \<noteq> \<bottom> \<Longrightarrow> branch (sinr_pat p)\<cdot>r\<cdot>(sinr\<cdot>y) = branch p\<cdot>r\<cdot>y"
   6.284 +by (simp_all add: branch_def sinr_pat_def)
   6.285 +
   6.286 +lemma up_pat [simp]:
   6.287 +  "branch (up_pat p)\<cdot>r\<cdot>\<bottom> = \<bottom>"
   6.288 +  "branch (up_pat p)\<cdot>r\<cdot>(up\<cdot>x) = branch p\<cdot>r\<cdot>x"
   6.289 +by (simp_all add: branch_def up_pat_def)
   6.290 +
   6.291 +lemma TT_pat [simp]:
   6.292 +  "branch TT_pat\<cdot>(unit_when\<cdot>r)\<cdot>\<bottom> = \<bottom>"
   6.293 +  "branch TT_pat\<cdot>(unit_when\<cdot>r)\<cdot>TT = succeed\<cdot>r"
   6.294 +  "branch TT_pat\<cdot>(unit_when\<cdot>r)\<cdot>FF = fail"
   6.295 +by (simp_all add: branch_def TT_pat_def)
   6.296 +
   6.297 +lemma FF_pat [simp]:
   6.298 +  "branch FF_pat\<cdot>(unit_when\<cdot>r)\<cdot>\<bottom> = \<bottom>"
   6.299 +  "branch FF_pat\<cdot>(unit_when\<cdot>r)\<cdot>TT = fail"
   6.300 +  "branch FF_pat\<cdot>(unit_when\<cdot>r)\<cdot>FF = succeed\<cdot>r"
   6.301 +by (simp_all add: branch_def FF_pat_def)
   6.302 +
   6.303 +lemma ONE_pat [simp]:
   6.304 +  "branch ONE_pat\<cdot>(unit_when\<cdot>r)\<cdot>\<bottom> = \<bottom>"
   6.305 +  "branch ONE_pat\<cdot>(unit_when\<cdot>r)\<cdot>ONE = succeed\<cdot>r"
   6.306 +by (simp_all add: branch_def ONE_pat_def)
   6.307 +
   6.308 +
   6.309 +subsection {* Wildcards, as-patterns, and lazy patterns *}
   6.310 +
   6.311 +definition
   6.312 +  wild_pat :: "'a \<rightarrow> unit match" where
   6.313 +  "wild_pat = (\<Lambda> x. succeed\<cdot>())"
   6.314 +
   6.315 +definition
   6.316 +  as_pat :: "('a \<rightarrow> 'b match) \<Rightarrow> 'a \<rightarrow> ('a \<times> 'b) match" where
   6.317 +  "as_pat p = (\<Lambda> x. match_case\<cdot>fail\<cdot>(\<Lambda> a. succeed\<cdot>(x, a))\<cdot>(p\<cdot>x))"
   6.318 +
   6.319 +definition
   6.320 +  lazy_pat :: "('a \<rightarrow> 'b::pcpo match) \<Rightarrow> ('a \<rightarrow> 'b match)" where
   6.321 +  "lazy_pat p = (\<Lambda> x. succeed\<cdot>(cases\<cdot>(p\<cdot>x)))"
   6.322 +
   6.323 +text {* Parse translations (patterns) *}
   6.324 +translations
   6.325 +  "_pat _" => "CONST wild_pat"
   6.326 +
   6.327 +text {* Parse translations (variables) *}
   6.328 +translations
   6.329 +  "_variable _ r" => "_variable _noargs r"
   6.330 +
   6.331 +text {* Print translations *}
   6.332 +translations
   6.333 +  "_" <= "_match (CONST wild_pat) _noargs"
   6.334 +
   6.335 +lemma wild_pat [simp]: "branch wild_pat\<cdot>(unit_when\<cdot>r)\<cdot>x = succeed\<cdot>r"
   6.336 +by (simp add: branch_def wild_pat_def)
   6.337 +
   6.338 +lemma as_pat [simp]:
   6.339 +  "branch (as_pat p)\<cdot>(csplit\<cdot>r)\<cdot>x = branch p\<cdot>(r\<cdot>x)\<cdot>x"
   6.340 +apply (simp add: branch_def as_pat_def)
   6.341 +apply (cases "p\<cdot>x", simp_all)
   6.342 +done
   6.343 +
   6.344 +lemma lazy_pat [simp]:
   6.345 +  "branch p\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> branch (lazy_pat p)\<cdot>r\<cdot>x = succeed\<cdot>(r\<cdot>\<bottom>)"
   6.346 +  "branch p\<cdot>r\<cdot>x = fail \<Longrightarrow> branch (lazy_pat p)\<cdot>r\<cdot>x = succeed\<cdot>(r\<cdot>\<bottom>)"
   6.347 +  "branch p\<cdot>r\<cdot>x = succeed\<cdot>s \<Longrightarrow> branch (lazy_pat p)\<cdot>r\<cdot>x = succeed\<cdot>s"
   6.348 +apply (simp_all add: branch_def lazy_pat_def)
   6.349 +apply (cases "p\<cdot>x", simp_all)+
   6.350 +done
   6.351 +
   6.352 +subsection {* Examples *}
   6.353 +
   6.354 +term "Case t of (:up\<cdot>(sinl\<cdot>x), sinr\<cdot>y:) \<Rightarrow> (x, y)"
   6.355 +
   6.356 +term "\<Lambda> t. Case t of up\<cdot>(sinl\<cdot>a) \<Rightarrow> a | up\<cdot>(sinr\<cdot>b) \<Rightarrow> b"
   6.357 +
   6.358 +term "\<Lambda> t. Case t of (:up\<cdot>(sinl\<cdot>_), sinr\<cdot>x:) \<Rightarrow> x"
   6.359 +
   6.360 +subsection {* ML code for generating definitions *}
   6.361 +
   6.362 +ML {*
   6.363 +local open HOLCF_Library in
   6.364 +
   6.365 +val beta_rules =
   6.366 +  @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @
   6.367 +  @{thms cont2cont_fst cont2cont_snd cont2cont_Pair};
   6.368 +
   6.369 +val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);
   6.370 +
   6.371 +fun define_consts
   6.372 +    (specs : (binding * term * mixfix) list)
   6.373 +    (thy : theory)
   6.374 +    : (term list * thm list) * theory =
   6.375 +  let
   6.376 +    fun mk_decl (b, t, mx) = (b, fastype_of t, mx);
   6.377 +    val decls = map mk_decl specs;
   6.378 +    val thy = Cont_Consts.add_consts decls thy;
   6.379 +    fun mk_const (b, T, mx) = Const (Sign.full_name thy b, T);
   6.380 +    val consts = map mk_const decls;
   6.381 +    fun mk_def c (b, t, mx) =
   6.382 +      (Binding.suffix_name "_def" b, Logic.mk_equals (c, t));
   6.383 +    val defs = map2 mk_def consts specs;
   6.384 +    val (def_thms, thy) =
   6.385 +      PureThy.add_defs false (map Thm.no_attributes defs) thy;
   6.386 +  in
   6.387 +    ((consts, def_thms), thy)
   6.388 +  end;
   6.389 +
   6.390 +fun prove
   6.391 +    (thy : theory)
   6.392 +    (defs : thm list)
   6.393 +    (goal : term)
   6.394 +    (tacs : {prems: thm list, context: Proof.context} -> tactic list)
   6.395 +    : thm =
   6.396 +  let
   6.397 +    fun tac {prems, context} =
   6.398 +      rewrite_goals_tac defs THEN
   6.399 +      EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context})
   6.400 +  in
   6.401 +    Goal.prove_global thy [] [] goal tac
   6.402 +  end;
   6.403 +
   6.404 +fun get_vars_avoiding
   6.405 +    (taken : string list)
   6.406 +    (args : (bool * typ) list)
   6.407 +    : (term list * term list) =
   6.408 +  let
   6.409 +    val Ts = map snd args;
   6.410 +    val ns = Name.variant_list taken (Datatype_Prop.make_tnames Ts);
   6.411 +    val vs = map Free (ns ~~ Ts);
   6.412 +    val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs));
   6.413 +  in
   6.414 +    (vs, nonlazy)
   6.415 +  end;
   6.416 +
   6.417 +(******************************************************************************)
   6.418 +(************** definitions and theorems for pattern combinators **************)
   6.419 +(******************************************************************************)
   6.420 +
   6.421 +fun add_pattern_combinators
   6.422 +    (bindings : binding list)
   6.423 +    (spec : (term * (bool * typ) list) list)
   6.424 +    (lhsT : typ)
   6.425 +    (exhaust : thm)
   6.426 +    (case_const : typ -> term)
   6.427 +    (case_rews : thm list)
   6.428 +    (thy : theory) =
   6.429 +  let
   6.430 +
   6.431 +    (* utility functions *)
   6.432 +    fun mk_pair_pat (p1, p2) =
   6.433 +      let
   6.434 +        val T1 = fastype_of p1;
   6.435 +        val T2 = fastype_of p2;
   6.436 +        val (U1, V1) = apsnd dest_matchT (dest_cfunT T1);
   6.437 +        val (U2, V2) = apsnd dest_matchT (dest_cfunT T2);
   6.438 +        val pat_typ = [T1, T2] --->
   6.439 +            (mk_prodT (U1, U2) ->> mk_matchT (mk_prodT (V1, V2)));
   6.440 +        val pat_const = Const (@{const_name cpair_pat}, pat_typ);
   6.441 +      in
   6.442 +        pat_const $ p1 $ p2
   6.443 +      end;
   6.444 +    fun mk_tuple_pat [] = succeed_const HOLogic.unitT
   6.445 +      | mk_tuple_pat ps = foldr1 mk_pair_pat ps;
   6.446 +    fun branch_const (T,U,V) = 
   6.447 +      Const (@{const_name branch},
   6.448 +        (T ->> mk_matchT U) --> (U ->> V) ->> T ->> mk_matchT V);
   6.449 +
   6.450 +    (* define pattern combinators *)
   6.451 +    local
   6.452 +      val tns = map (fst o dest_TFree) (snd (dest_Type lhsT));
   6.453 +
   6.454 +      fun pat_eqn (i, (bind, (con, args))) : binding * term * mixfix =
   6.455 +        let
   6.456 +          val pat_bind = Binding.suffix_name "_pat" bind;
   6.457 +          val Ts = map snd args;
   6.458 +          val Vs =
   6.459 +              (map (K "'t") args)
   6.460 +              |> Datatype_Prop.indexify_names
   6.461 +              |> Name.variant_list tns
   6.462 +              |> map (fn t => TFree (t, @{sort pcpo}));
   6.463 +          val patNs = Datatype_Prop.indexify_names (map (K "pat") args);
   6.464 +          val patTs = map2 (fn T => fn V => T ->> mk_matchT V) Ts Vs;
   6.465 +          val pats = map Free (patNs ~~ patTs);
   6.466 +          val fail = mk_fail (mk_tupleT Vs);
   6.467 +          val (vs, nonlazy) = get_vars_avoiding patNs args;
   6.468 +          val rhs = big_lambdas vs (mk_tuple_pat pats ` mk_tuple vs);
   6.469 +          fun one_fun (j, (_, args')) =
   6.470 +            let
   6.471 +              val (vs', nonlazy) = get_vars_avoiding patNs args';
   6.472 +            in if i = j then rhs else big_lambdas vs' fail end;
   6.473 +          val funs = map_index one_fun spec;
   6.474 +          val body = list_ccomb (case_const (mk_matchT (mk_tupleT Vs)), funs);
   6.475 +        in
   6.476 +          (pat_bind, lambdas pats body, NoSyn)
   6.477 +        end;
   6.478 +    in
   6.479 +      val ((pat_consts, pat_defs), thy) =
   6.480 +          define_consts (map_index pat_eqn (bindings ~~ spec)) thy
   6.481 +    end;
   6.482 +
   6.483 +    (* syntax translations for pattern combinators *)
   6.484 +    local
   6.485 +      open Syntax
   6.486 +      fun syntax c = Syntax.mark_const (fst (dest_Const c));
   6.487 +      fun app s (l, r) = Syntax.mk_appl (Constant s) [l, r];
   6.488 +      val capp = app @{const_syntax Rep_CFun};
   6.489 +      val capps = Library.foldl capp
   6.490 +
   6.491 +      fun app_var x = Syntax.mk_appl (Constant "_variable") [x, Variable "rhs"];
   6.492 +      fun app_pat x = Syntax.mk_appl (Constant "_pat") [x];
   6.493 +      fun args_list [] = Constant "_noargs"
   6.494 +        | args_list xs = foldr1 (app "_args") xs;
   6.495 +      fun one_case_trans (pat, (con, args)) =
   6.496 +        let
   6.497 +          val cname = Constant (syntax con);
   6.498 +          val pname = Constant (syntax pat);
   6.499 +          val ns = 1 upto length args;
   6.500 +          val xs = map (fn n => Variable ("x"^(string_of_int n))) ns;
   6.501 +          val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
   6.502 +          val vs = map (fn n => Variable ("v"^(string_of_int n))) ns;
   6.503 +        in
   6.504 +          [ParseRule (app_pat (capps (cname, xs)),
   6.505 +                      mk_appl pname (map app_pat xs)),
   6.506 +           ParseRule (app_var (capps (cname, xs)),
   6.507 +                      app_var (args_list xs)),
   6.508 +           PrintRule (capps (cname, ListPair.map (app "_match") (ps,vs)),
   6.509 +                      app "_match" (mk_appl pname ps, args_list vs))]
   6.510 +        end;
   6.511 +      val trans_rules : Syntax.ast Syntax.trrule list =
   6.512 +          maps one_case_trans (pat_consts ~~ spec);
   6.513 +    in
   6.514 +      val thy = Sign.add_trrules_i trans_rules thy;
   6.515 +    end;
   6.516 +
   6.517 +    (* prove strictness and reduction rules of pattern combinators *)
   6.518 +    local
   6.519 +      val tns = map (fst o dest_TFree) (snd (dest_Type lhsT));
   6.520 +      val rn = Name.variant tns "'r";
   6.521 +      val R = TFree (rn, @{sort pcpo});
   6.522 +      fun pat_lhs (pat, args) =
   6.523 +        let
   6.524 +          val Ts = map snd args;
   6.525 +          val Vs =
   6.526 +              (map (K "'t") args)
   6.527 +              |> Datatype_Prop.indexify_names
   6.528 +              |> Name.variant_list (rn::tns)
   6.529 +              |> map (fn t => TFree (t, @{sort pcpo}));
   6.530 +          val patNs = Datatype_Prop.indexify_names (map (K "pat") args);
   6.531 +          val patTs = map2 (fn T => fn V => T ->> mk_matchT V) Ts Vs;
   6.532 +          val pats = map Free (patNs ~~ patTs);
   6.533 +          val k = Free ("rhs", mk_tupleT Vs ->> R);
   6.534 +          val branch1 = branch_const (lhsT, mk_tupleT Vs, R);
   6.535 +          val fun1 = (branch1 $ list_comb (pat, pats)) ` k;
   6.536 +          val branch2 = branch_const (mk_tupleT Ts, mk_tupleT Vs, R);
   6.537 +          val fun2 = (branch2 $ mk_tuple_pat pats) ` k;
   6.538 +          val taken = "rhs" :: patNs;
   6.539 +        in (fun1, fun2, taken) end;
   6.540 +      fun pat_strict (pat, (con, args)) =
   6.541 +        let
   6.542 +          val (fun1, fun2, taken) = pat_lhs (pat, args);
   6.543 +          val defs = @{thm branch_def} :: pat_defs;
   6.544 +          val goal = mk_trp (mk_strict fun1);
   6.545 +          val rules = @{thms match_case_simps} @ case_rews;
   6.546 +          val tacs = [simp_tac (beta_ss addsimps rules) 1];
   6.547 +        in prove thy defs goal (K tacs) end;
   6.548 +      fun pat_apps (i, (pat, (con, args))) =
   6.549 +        let
   6.550 +          val (fun1, fun2, taken) = pat_lhs (pat, args);
   6.551 +          fun pat_app (j, (con', args')) =
   6.552 +            let
   6.553 +              val (vs, nonlazy) = get_vars_avoiding taken args';
   6.554 +              val con_app = list_ccomb (con', vs);
   6.555 +              val assms = map (mk_trp o mk_defined) nonlazy;
   6.556 +              val rhs = if i = j then fun2 ` mk_tuple vs else mk_fail R;
   6.557 +              val concl = mk_trp (mk_eq (fun1 ` con_app, rhs));
   6.558 +              val goal = Logic.list_implies (assms, concl);
   6.559 +              val defs = @{thm branch_def} :: pat_defs;
   6.560 +              val rules = @{thms match_case_simps} @ case_rews;
   6.561 +              val tacs = [asm_simp_tac (beta_ss addsimps rules) 1];
   6.562 +            in prove thy defs goal (K tacs) end;
   6.563 +        in map_index pat_app spec end;
   6.564 +    in
   6.565 +      val pat_stricts = map pat_strict (pat_consts ~~ spec);
   6.566 +      val pat_apps = flat (map_index pat_apps (pat_consts ~~ spec));
   6.567 +    end;
   6.568 +
   6.569 +  in
   6.570 +    (pat_stricts @ pat_apps, thy)
   6.571 +  end
   6.572 +
   6.573 +end
   6.574 +*}
   6.575 +
   6.576 +(*
   6.577 +Cut from HOLCF/Tools/domain_constructors.ML
   6.578 +in function add_domain_constructors:
   6.579 +
   6.580 +    ( * define and prove theorems for pattern combinators * )
   6.581 +    val (pat_thms : thm list, thy : theory) =
   6.582 +      let
   6.583 +        val bindings = map #1 spec;
   6.584 +        fun prep_arg (lazy, sel, T) = (lazy, T);
   6.585 +        fun prep_con c (b, args, mx) = (c, map prep_arg args);
   6.586 +        val pat_spec = map2 prep_con con_consts spec;
   6.587 +      in
   6.588 +        add_pattern_combinators bindings pat_spec lhsT
   6.589 +          exhaust case_const cases thy
   6.590 +      end
   6.591 +
   6.592 +*)
   6.593 +
   6.594 +end
     7.1 --- a/src/HOLCF/ex/ROOT.ML	Mon May 24 09:32:52 2010 -0700
     7.2 +++ b/src/HOLCF/ex/ROOT.ML	Mon May 24 11:29:49 2010 -0700
     7.3 @@ -6,4 +6,5 @@
     7.4  use_thys ["Dnat", "Stream", "Dagstuhl", "Focus_ex", "Fix2", "Hoare",
     7.5    "Loop", "Powerdomain_ex", "Domain_Proofs",
     7.6    "Letrec",
     7.7 +  "Pattern_Match",
     7.8    "Strict_Fun"];