src/HOLCF/Fixrec.thy
changeset 37109 e67760c1b851
parent 37108 00f13d3ad474
child 39807 19ddbededdd3
     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