src/HOLCF/Fixrec.thy
 changeset 35926 e6aec5d665f0 parent 35920 9ef9a20cfba1 child 35939 db69a6a1fbb5
```     1.1 --- a/src/HOLCF/Fixrec.thy	Mon Mar 22 23:33:23 2010 -0700
1.2 +++ b/src/HOLCF/Fixrec.thy	Mon Mar 22 23:34:23 2010 -0700
1.3 @@ -276,13 +276,13 @@
1.4
1.5  definition
1.6    cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat" where
1.7 -  "cpair_pat p1 p2 = (\<Lambda>\<langle>x, y\<rangle>.
1.8 -    bind\<cdot>(p1\<cdot>x)\<cdot>(\<Lambda> a. bind\<cdot>(p2\<cdot>y)\<cdot>(\<Lambda> b. return\<cdot>\<langle>a, b\<rangle>)))"
1.9 +  "cpair_pat p1 p2 = (\<Lambda>(x, y).
1.10 +    bind\<cdot>(p1\<cdot>x)\<cdot>(\<Lambda> a. bind\<cdot>(p2\<cdot>y)\<cdot>(\<Lambda> b. return\<cdot>(a, b))))"
1.11
1.12  definition
1.13    spair_pat ::
1.14    "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a::pcpo \<otimes> 'b::pcpo, 'c \<times> 'd) pat" where
1.15 -  "spair_pat p1 p2 = (\<Lambda>(:x, y:). cpair_pat p1 p2\<cdot>\<langle>x, y\<rangle>)"
1.16 +  "spair_pat p1 p2 = (\<Lambda>(:x, y:). cpair_pat p1 p2\<cdot>(x, y))"
1.17
1.18  definition
1.19    sinl_pat :: "('a, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat" where
1.20 @@ -310,7 +310,7 @@
1.21
1.22  text {* Parse translations (patterns) *}
1.23  translations
1.24 -  "_pat (XCONST cpair\<cdot>x\<cdot>y)" => "CONST cpair_pat (_pat x) (_pat y)"
1.25 +  "_pat (XCONST Pair x y)" => "CONST cpair_pat (_pat x) (_pat y)"
1.26    "_pat (XCONST spair\<cdot>x\<cdot>y)" => "CONST spair_pat (_pat x) (_pat y)"
1.27    "_pat (XCONST sinl\<cdot>x)" => "CONST sinl_pat (_pat x)"
1.28    "_pat (XCONST sinr\<cdot>x)" => "CONST sinr_pat (_pat x)"
1.29 @@ -321,12 +321,12 @@
1.30
1.31  text {* CONST version is also needed for constructors with special syntax *}
1.32  translations
1.33 -  "_pat (CONST cpair\<cdot>x\<cdot>y)" => "CONST cpair_pat (_pat x) (_pat y)"
1.34 +  "_pat (CONST Pair x y)" => "CONST cpair_pat (_pat x) (_pat y)"
1.35    "_pat (CONST spair\<cdot>x\<cdot>y)" => "CONST spair_pat (_pat x) (_pat y)"
1.36
1.37  text {* Parse translations (variables) *}
1.38  translations
1.39 -  "_variable (XCONST cpair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
1.40 +  "_variable (XCONST Pair x y) r" => "_variable (_args x y) r"
1.41    "_variable (XCONST spair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
1.42    "_variable (XCONST sinl\<cdot>x) r" => "_variable x r"
1.43    "_variable (XCONST sinr\<cdot>x) r" => "_variable x r"
1.44 @@ -336,12 +336,12 @@
1.45    "_variable (XCONST ONE) r" => "_variable _noargs r"
1.46
1.47  translations
1.48 -  "_variable (CONST cpair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
1.49 +  "_variable (CONST Pair x y) r" => "_variable (_args x y) r"
1.50    "_variable (CONST spair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
1.51
1.52  text {* Print translations *}
1.53  translations
1.54 -  "CONST cpair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
1.55 +  "CONST Pair (_match p1 v1) (_match p2 v2)"
1.56        <= "_match (CONST cpair_pat p1 p2) (_args v1 v2)"
1.57    "CONST spair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
1.58        <= "_match (CONST spair_pat p1 p2) (_args v1 v2)"
1.59 @@ -353,20 +353,20 @@
1.60    "CONST ONE" <= "_match (CONST ONE_pat) _noargs"
1.61
1.62  lemma cpair_pat1:
1.63 -  "branch p\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = \<bottom>"
1.64 +  "branch p\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>(x, y) = \<bottom>"
1.65  apply (simp add: branch_def cpair_pat_def)
1.66  apply (rule_tac p="p\<cdot>x" in maybeE, simp_all)
1.67  done
1.68
1.69  lemma cpair_pat2:
1.70 -  "branch p\<cdot>r\<cdot>x = fail \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = fail"
1.71 +  "branch p\<cdot>r\<cdot>x = fail \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>(x, y) = fail"
1.72  apply (simp add: branch_def cpair_pat_def)
1.73  apply (rule_tac p="p\<cdot>x" in maybeE, simp_all)
1.74  done
1.75
1.76  lemma cpair_pat3:
1.77    "branch p\<cdot>r\<cdot>x = return\<cdot>s \<Longrightarrow>
1.78 -   branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = branch q\<cdot>s\<cdot>y"
1.79 +   branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>(x, y) = branch q\<cdot>s\<cdot>y"
1.80  apply (simp add: branch_def cpair_pat_def)
1.81  apply (rule_tac p="p\<cdot>x" in maybeE, simp_all)
1.82  apply (rule_tac p="q\<cdot>y" in maybeE, simp_all)
1.83 @@ -379,7 +379,7 @@
1.84    "branch (spair_pat p1 p2)\<cdot>r\<cdot>\<bottom> = \<bottom>"
1.85    "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk>
1.86       \<Longrightarrow> branch (spair_pat p1 p2)\<cdot>r\<cdot>(:x, y:) =
1.87 -         branch (cpair_pat p1 p2)\<cdot>r\<cdot>\<langle>x, y\<rangle>"
1.88 +         branch (cpair_pat p1 p2)\<cdot>r\<cdot>(x, y)"
1.89  by (simp_all add: branch_def spair_pat_def)
1.90
1.91  lemma sinl_pat [simp]:
1.92 @@ -425,7 +425,7 @@
1.93
1.94  definition
1.95    as_pat :: "('a \<rightarrow> 'b maybe) \<Rightarrow> 'a \<rightarrow> ('a \<times> 'b) maybe" where
1.96 -  "as_pat p = (\<Lambda> x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> a. return\<cdot>\<langle>x, a\<rangle>))"
1.97 +  "as_pat p = (\<Lambda> x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> a. return\<cdot>(x, a)))"
1.98
1.99  definition
1.100    lazy_pat :: "('a \<rightarrow> 'b::pcpo maybe) \<Rightarrow> ('a \<rightarrow> 'b maybe)" where
1.101 @@ -516,7 +516,6 @@
1.103
1.104  lemma match_cpair_simps [simp]:
1.105 -  "match_cpair\<cdot>\<langle>x, y\<rangle>\<cdot>k = k\<cdot>x\<cdot>y"
1.106    "match_cpair\<cdot>(x, y)\<cdot>k = k\<cdot>x\<cdot>y"