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.102  by (simp_all add: match_UU_def)
   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"
   1.107  by (simp_all add: match_cpair_def)
   1.108  
   1.109 @@ -602,7 +601,6 @@
   1.110        (@{const_name sinl}, @{const_name match_sinl}),
   1.111        (@{const_name sinr}, @{const_name match_sinr}),
   1.112        (@{const_name spair}, @{const_name match_spair}),
   1.113 -      (@{const_name cpair}, @{const_name match_cpair}),
   1.114        (@{const_name Pair}, @{const_name match_cpair}),
   1.115        (@{const_name ONE}, @{const_name match_ONE}),
   1.116        (@{const_name TT}, @{const_name match_TT}),