completely remove constants cpair, cfst, csnd
authorhuffman
Mon Mar 22 23:34:23 2010 -0700 (2010-03-22)
changeset 35926e6aec5d665f0
parent 35925 3da8db225c93
child 35927 343d5b0df29a
completely remove constants cpair, cfst, csnd
src/HOLCF/Cprod.thy
src/HOLCF/Fixrec.thy
src/HOLCF/HOLCF.thy
     1.1 --- a/src/HOLCF/Cprod.thy	Mon Mar 22 23:33:23 2010 -0700
     1.2 +++ b/src/HOLCF/Cprod.thy	Mon Mar 22 23:34:23 2010 -0700
     1.3 @@ -22,150 +22,22 @@
     1.4  lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a"
     1.5  by (simp add: unit_when_def)
     1.6  
     1.7 -subsection {* Continuous versions of constants *}
     1.8 -
     1.9 -definition
    1.10 -  cpair :: "'a \<rightarrow> 'b \<rightarrow> ('a * 'b)"  -- {* continuous pairing *}  where
    1.11 -  "cpair = (\<Lambda> x y. (x, y))"
    1.12 -
    1.13 -definition
    1.14 -  cfst :: "('a * 'b) \<rightarrow> 'a" where
    1.15 -  "cfst = (\<Lambda> p. fst p)"
    1.16 -
    1.17 -definition
    1.18 -  csnd :: "('a * 'b) \<rightarrow> 'b" where
    1.19 -  "csnd = (\<Lambda> p. snd p)"
    1.20 +subsection {* Continuous version of split function *}
    1.21  
    1.22  definition
    1.23    csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c" where
    1.24    "csplit = (\<Lambda> f p. f\<cdot>(fst p)\<cdot>(snd p))"
    1.25  
    1.26 -syntax
    1.27 -  "_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(1<_,/ _>)")
    1.28 -
    1.29 -syntax (xsymbols)
    1.30 -  "_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(1\<langle>_,/ _\<rangle>)")
    1.31 -
    1.32  translations
    1.33 -  "\<langle>x, y, z\<rangle>" == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
    1.34 -  "\<langle>x, y\<rangle>"    == "CONST cpair\<cdot>x\<cdot>y"
    1.35 -
    1.36 -translations
    1.37 -  "\<Lambda>(CONST cpair\<cdot>x\<cdot>y). t" == "CONST csplit\<cdot>(\<Lambda> x y. t)"
    1.38 -  "\<Lambda>(CONST Pair x y). t" => "CONST csplit\<cdot>(\<Lambda> x y. t)"
    1.39 +  "\<Lambda>(CONST Pair x y). t" == "CONST csplit\<cdot>(\<Lambda> x y. t)"
    1.40  
    1.41  
    1.42  subsection {* Convert all lemmas to the continuous versions *}
    1.43  
    1.44 -lemma cpair_eq_pair: "<x, y> = (x, y)"
    1.45 -by (simp add: cpair_def cont_pair1 cont_pair2)
    1.46 -
    1.47 -lemma pair_eq_cpair: "(x, y) = <x, y>"
    1.48 -by (simp add: cpair_def cont_pair1 cont_pair2)
    1.49 -
    1.50 -lemma inject_cpair: "<a,b> = <aa,ba> \<Longrightarrow> a = aa \<and> b = ba"
    1.51 -by (simp add: cpair_eq_pair)
    1.52 -
    1.53 -lemma cpair_eq [iff]: "(<a, b> = <a', b'>) = (a = a' \<and> b = b')"
    1.54 -by (simp add: cpair_eq_pair)
    1.55 -
    1.56 -lemma cpair_below [iff]: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')"
    1.57 -by (simp add: cpair_eq_pair)
    1.58 -
    1.59 -lemma cpair_defined_iff [iff]: "(<x, y> = \<bottom>) = (x = \<bottom> \<and> y = \<bottom>)"
    1.60 -by (simp add: cpair_eq_pair)
    1.61 -
    1.62 -lemma cpair_strict [simp]: "\<langle>\<bottom>, \<bottom>\<rangle> = \<bottom>"
    1.63 -by simp
    1.64 -
    1.65 -lemma inst_cprod_pcpo2: "\<bottom> = <\<bottom>, \<bottom>>"
    1.66 -by (rule cpair_strict [symmetric])
    1.67 -
    1.68 -lemma defined_cpair_rev: 
    1.69 - "<a,b> = \<bottom> \<Longrightarrow> a = \<bottom> \<and> b = \<bottom>"
    1.70 -by simp
    1.71 -
    1.72 -lemma Exh_Cprod2: "\<exists>a b. z = <a, b>"
    1.73 -by (simp add: cpair_eq_pair)
    1.74 -
    1.75 -lemma cprodE: "\<lbrakk>\<And>x y. p = <x, y> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    1.76 -by (cut_tac Exh_Cprod2, auto)
    1.77 -
    1.78 -lemma cfst_cpair [simp]: "cfst\<cdot><x, y> = x"
    1.79 -by (simp add: cpair_eq_pair cfst_def)
    1.80 -
    1.81 -lemma csnd_cpair [simp]: "csnd\<cdot><x, y> = y"
    1.82 -by (simp add: cpair_eq_pair csnd_def)
    1.83 -
    1.84 -lemma cfst_strict [simp]: "cfst\<cdot>\<bottom> = \<bottom>"
    1.85 -by (simp add: cfst_def)
    1.86 -
    1.87 -lemma csnd_strict [simp]: "csnd\<cdot>\<bottom> = \<bottom>"
    1.88 -by (simp add: csnd_def)
    1.89 -
    1.90 -lemma cpair_cfst_csnd: "\<langle>cfst\<cdot>p, csnd\<cdot>p\<rangle> = p"
    1.91 -by (cases p rule: cprodE, simp)
    1.92 -
    1.93 -lemmas surjective_pairing_Cprod2 = cpair_cfst_csnd
    1.94 -
    1.95 -lemma below_cprod: "x \<sqsubseteq> y = (cfst\<cdot>x \<sqsubseteq> cfst\<cdot>y \<and> csnd\<cdot>x \<sqsubseteq> csnd\<cdot>y)"
    1.96 -by (simp add: below_prod_def cfst_def csnd_def)
    1.97 -
    1.98 -lemma eq_cprod: "(x = y) = (cfst\<cdot>x = cfst\<cdot>y \<and> csnd\<cdot>x = csnd\<cdot>y)"
    1.99 -by (auto simp add: po_eq_conv below_cprod)
   1.100 -
   1.101 -lemma cfst_below_iff: "cfst\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> <y, csnd\<cdot>x>"
   1.102 -by (simp add: below_cprod)
   1.103 -
   1.104 -lemma csnd_below_iff: "csnd\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> <cfst\<cdot>x, y>"
   1.105 -by (simp add: below_cprod)
   1.106 -
   1.107 -lemma compact_cfst: "compact x \<Longrightarrow> compact (cfst\<cdot>x)"
   1.108 -by (rule compactI, simp add: cfst_below_iff)
   1.109 -
   1.110 -lemma compact_csnd: "compact x \<Longrightarrow> compact (csnd\<cdot>x)"
   1.111 -by (rule compactI, simp add: csnd_below_iff)
   1.112 -
   1.113 -lemma compact_cpair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact <x, y>"
   1.114 -by (simp add: cpair_eq_pair)
   1.115 -
   1.116 -lemma compact_cpair_iff [simp]: "compact <x, y> = (compact x \<and> compact y)"
   1.117 -by (simp add: cpair_eq_pair)
   1.118 -
   1.119 -lemma lub_cprod2: 
   1.120 -  "chain S \<Longrightarrow> range S <<| <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
   1.121 -apply (simp add: cpair_eq_pair cfst_def csnd_def)
   1.122 -apply (erule lub_cprod)
   1.123 -done
   1.124 -
   1.125 -lemma thelub_cprod2:
   1.126 -  "chain S \<Longrightarrow> (\<Squnion>i. S i) = <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
   1.127 -by (rule lub_cprod2 [THEN thelubI])
   1.128 -
   1.129  lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>"
   1.130  by (simp add: csplit_def)
   1.131  
   1.132 -lemma csplit2 [simp]: "csplit\<cdot>f\<cdot><x,y> = f\<cdot>x\<cdot>y"
   1.133 -by (simp add: csplit_def cpair_def)
   1.134 -
   1.135 -lemma csplit3 [simp]: "csplit\<cdot>cpair\<cdot>z = z"
   1.136 -by (simp add: csplit_def cpair_def)
   1.137 -
   1.138  lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y"
   1.139  by (simp add: csplit_def)
   1.140  
   1.141 -lemmas Cprod_rews = cfst_cpair csnd_cpair csplit2
   1.142 -
   1.143 -subsection {* Product type is a bifinite domain *}
   1.144 -
   1.145 -lemma approx_cpair [simp]:
   1.146 -  "approx i\<cdot>\<langle>x, y\<rangle> = \<langle>approx i\<cdot>x, approx i\<cdot>y\<rangle>"
   1.147 -by (simp add: cpair_eq_pair)
   1.148 -
   1.149 -lemma cfst_approx: "cfst\<cdot>(approx i\<cdot>p) = approx i\<cdot>(cfst\<cdot>p)"
   1.150 -by (cases p rule: cprodE, simp)
   1.151 -
   1.152 -lemma csnd_approx: "csnd\<cdot>(approx i\<cdot>p) = approx i\<cdot>(csnd\<cdot>p)"
   1.153 -by (cases p rule: cprodE, simp)
   1.154 -
   1.155  end
     2.1 --- a/src/HOLCF/Fixrec.thy	Mon Mar 22 23:33:23 2010 -0700
     2.2 +++ b/src/HOLCF/Fixrec.thy	Mon Mar 22 23:34:23 2010 -0700
     2.3 @@ -276,13 +276,13 @@
     2.4  
     2.5  definition
     2.6    cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat" where
     2.7 -  "cpair_pat p1 p2 = (\<Lambda>\<langle>x, y\<rangle>.
     2.8 -    bind\<cdot>(p1\<cdot>x)\<cdot>(\<Lambda> a. bind\<cdot>(p2\<cdot>y)\<cdot>(\<Lambda> b. return\<cdot>\<langle>a, b\<rangle>)))"
     2.9 +  "cpair_pat p1 p2 = (\<Lambda>(x, y).
    2.10 +    bind\<cdot>(p1\<cdot>x)\<cdot>(\<Lambda> a. bind\<cdot>(p2\<cdot>y)\<cdot>(\<Lambda> b. return\<cdot>(a, b))))"
    2.11  
    2.12  definition
    2.13    spair_pat ::
    2.14    "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a::pcpo \<otimes> 'b::pcpo, 'c \<times> 'd) pat" where
    2.15 -  "spair_pat p1 p2 = (\<Lambda>(:x, y:). cpair_pat p1 p2\<cdot>\<langle>x, y\<rangle>)"
    2.16 +  "spair_pat p1 p2 = (\<Lambda>(:x, y:). cpair_pat p1 p2\<cdot>(x, y))"
    2.17  
    2.18  definition
    2.19    sinl_pat :: "('a, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat" where
    2.20 @@ -310,7 +310,7 @@
    2.21  
    2.22  text {* Parse translations (patterns) *}
    2.23  translations
    2.24 -  "_pat (XCONST cpair\<cdot>x\<cdot>y)" => "CONST cpair_pat (_pat x) (_pat y)"
    2.25 +  "_pat (XCONST Pair x y)" => "CONST cpair_pat (_pat x) (_pat y)"
    2.26    "_pat (XCONST spair\<cdot>x\<cdot>y)" => "CONST spair_pat (_pat x) (_pat y)"
    2.27    "_pat (XCONST sinl\<cdot>x)" => "CONST sinl_pat (_pat x)"
    2.28    "_pat (XCONST sinr\<cdot>x)" => "CONST sinr_pat (_pat x)"
    2.29 @@ -321,12 +321,12 @@
    2.30  
    2.31  text {* CONST version is also needed for constructors with special syntax *}
    2.32  translations
    2.33 -  "_pat (CONST cpair\<cdot>x\<cdot>y)" => "CONST cpair_pat (_pat x) (_pat y)"
    2.34 +  "_pat (CONST Pair x y)" => "CONST cpair_pat (_pat x) (_pat y)"
    2.35    "_pat (CONST spair\<cdot>x\<cdot>y)" => "CONST spair_pat (_pat x) (_pat y)"
    2.36  
    2.37  text {* Parse translations (variables) *}
    2.38  translations
    2.39 -  "_variable (XCONST cpair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
    2.40 +  "_variable (XCONST Pair x y) r" => "_variable (_args x y) r"
    2.41    "_variable (XCONST spair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
    2.42    "_variable (XCONST sinl\<cdot>x) r" => "_variable x r"
    2.43    "_variable (XCONST sinr\<cdot>x) r" => "_variable x r"
    2.44 @@ -336,12 +336,12 @@
    2.45    "_variable (XCONST ONE) r" => "_variable _noargs r"
    2.46  
    2.47  translations
    2.48 -  "_variable (CONST cpair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
    2.49 +  "_variable (CONST Pair x y) r" => "_variable (_args x y) r"
    2.50    "_variable (CONST spair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
    2.51  
    2.52  text {* Print translations *}
    2.53  translations
    2.54 -  "CONST cpair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
    2.55 +  "CONST Pair (_match p1 v1) (_match p2 v2)"
    2.56        <= "_match (CONST cpair_pat p1 p2) (_args v1 v2)"
    2.57    "CONST spair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
    2.58        <= "_match (CONST spair_pat p1 p2) (_args v1 v2)"
    2.59 @@ -353,20 +353,20 @@
    2.60    "CONST ONE" <= "_match (CONST ONE_pat) _noargs"
    2.61  
    2.62  lemma cpair_pat1:
    2.63 -  "branch p\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = \<bottom>"
    2.64 +  "branch p\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>(x, y) = \<bottom>"
    2.65  apply (simp add: branch_def cpair_pat_def)
    2.66  apply (rule_tac p="p\<cdot>x" in maybeE, simp_all)
    2.67  done
    2.68  
    2.69  lemma cpair_pat2:
    2.70 -  "branch p\<cdot>r\<cdot>x = fail \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = fail"
    2.71 +  "branch p\<cdot>r\<cdot>x = fail \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>(x, y) = fail"
    2.72  apply (simp add: branch_def cpair_pat_def)
    2.73  apply (rule_tac p="p\<cdot>x" in maybeE, simp_all)
    2.74  done
    2.75  
    2.76  lemma cpair_pat3:
    2.77    "branch p\<cdot>r\<cdot>x = return\<cdot>s \<Longrightarrow>
    2.78 -   branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = branch q\<cdot>s\<cdot>y"
    2.79 +   branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>(x, y) = branch q\<cdot>s\<cdot>y"
    2.80  apply (simp add: branch_def cpair_pat_def)
    2.81  apply (rule_tac p="p\<cdot>x" in maybeE, simp_all)
    2.82  apply (rule_tac p="q\<cdot>y" in maybeE, simp_all)
    2.83 @@ -379,7 +379,7 @@
    2.84    "branch (spair_pat p1 p2)\<cdot>r\<cdot>\<bottom> = \<bottom>"
    2.85    "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk>
    2.86       \<Longrightarrow> branch (spair_pat p1 p2)\<cdot>r\<cdot>(:x, y:) =
    2.87 -         branch (cpair_pat p1 p2)\<cdot>r\<cdot>\<langle>x, y\<rangle>"
    2.88 +         branch (cpair_pat p1 p2)\<cdot>r\<cdot>(x, y)"
    2.89  by (simp_all add: branch_def spair_pat_def)
    2.90  
    2.91  lemma sinl_pat [simp]:
    2.92 @@ -425,7 +425,7 @@
    2.93  
    2.94  definition
    2.95    as_pat :: "('a \<rightarrow> 'b maybe) \<Rightarrow> 'a \<rightarrow> ('a \<times> 'b) maybe" where
    2.96 -  "as_pat p = (\<Lambda> x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> a. return\<cdot>\<langle>x, a\<rangle>))"
    2.97 +  "as_pat p = (\<Lambda> x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> a. return\<cdot>(x, a)))"
    2.98  
    2.99  definition
   2.100    lazy_pat :: "('a \<rightarrow> 'b::pcpo maybe) \<Rightarrow> ('a \<rightarrow> 'b maybe)" where
   2.101 @@ -516,7 +516,6 @@
   2.102  by (simp_all add: match_UU_def)
   2.103  
   2.104  lemma match_cpair_simps [simp]:
   2.105 -  "match_cpair\<cdot>\<langle>x, y\<rangle>\<cdot>k = k\<cdot>x\<cdot>y"
   2.106    "match_cpair\<cdot>(x, y)\<cdot>k = k\<cdot>x\<cdot>y"
   2.107  by (simp_all add: match_cpair_def)
   2.108  
   2.109 @@ -602,7 +601,6 @@
   2.110        (@{const_name sinl}, @{const_name match_sinl}),
   2.111        (@{const_name sinr}, @{const_name match_sinr}),
   2.112        (@{const_name spair}, @{const_name match_spair}),
   2.113 -      (@{const_name cpair}, @{const_name match_cpair}),
   2.114        (@{const_name Pair}, @{const_name match_cpair}),
   2.115        (@{const_name ONE}, @{const_name match_ONE}),
   2.116        (@{const_name TT}, @{const_name match_TT}),
     3.1 --- a/src/HOLCF/HOLCF.thy	Mon Mar 22 23:33:23 2010 -0700
     3.2 +++ b/src/HOLCF/HOLCF.thy	Mon Mar 22 23:34:23 2010 -0700
     3.3 @@ -50,10 +50,6 @@
     3.4  lemmas not_Iup_less = not_Iup_below
     3.5  lemmas Iup_less = Iup_below
     3.6  lemmas up_less = up_below
     3.7 -lemmas cpair_less = cpair_below
     3.8 -lemmas less_cprod = below_cprod
     3.9 -lemmas cfst_less_iff = cfst_below_iff
    3.10 -lemmas csnd_less_iff = csnd_below_iff
    3.11  lemmas Def_inject_less_eq = Def_below_Def
    3.12  lemmas Def_less_is_eq = Def_below_iff
    3.13  lemmas spair_less_iff = spair_below_iff