src/HOLCF/Cprod.thy
changeset 25131 2c8caac48ade
parent 18289 56ddf617d6e8
child 25784 71157f7e671e
equal deleted inserted replaced
25130:d91391a8705b 25131:2c8caac48ade
    27 by intro_classes (simp add: is_lub_def is_ub_def)
    27 by intro_classes (simp add: is_lub_def is_ub_def)
    28 
    28 
    29 instance unit :: pcpo
    29 instance unit :: pcpo
    30 by intro_classes simp
    30 by intro_classes simp
    31 
    31 
    32 constdefs
    32 definition
    33   unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a"
    33   unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a" where
    34   "unit_when \<equiv> \<Lambda> a _. a"
    34   "unit_when = (\<Lambda> a _. a)"
    35 
    35 
    36 translations
    36 translations
    37   "\<Lambda>(). t" == "unit_when\<cdot>t"
    37   "\<Lambda>(). t" == "CONST unit_when\<cdot>t"
    38 
    38 
    39 lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a"
    39 lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a"
    40 by (simp add: unit_when_def)
    40 by (simp add: unit_when_def)
    41 
    41 
    42 
    42 
   190 apply (rule contlub_snd)
   190 apply (rule contlub_snd)
   191 done
   191 done
   192 
   192 
   193 subsection {* Continuous versions of constants *}
   193 subsection {* Continuous versions of constants *}
   194 
   194 
   195 constdefs
   195 definition
   196   cpair :: "'a \<rightarrow> 'b \<rightarrow> ('a * 'b)" (* continuous pairing *)
   196   cpair :: "'a \<rightarrow> 'b \<rightarrow> ('a * 'b)"  -- {* continuous pairing *}  where
   197   "cpair \<equiv> (\<Lambda> x y. (x, y))"
   197   "cpair = (\<Lambda> x y. (x, y))"
   198 
   198 
   199   cfst :: "('a * 'b) \<rightarrow> 'a"
   199 definition
   200   "cfst \<equiv> (\<Lambda> p. fst p)"
   200   cfst :: "('a * 'b) \<rightarrow> 'a" where
   201 
   201   "cfst = (\<Lambda> p. fst p)"
   202   csnd :: "('a * 'b) \<rightarrow> 'b"
   202 
   203   "csnd \<equiv> (\<Lambda> p. snd p)"      
   203 definition
   204 
   204   csnd :: "('a * 'b) \<rightarrow> 'b" where
   205   csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c"
   205   "csnd = (\<Lambda> p. snd p)"      
   206   "csplit \<equiv> (\<Lambda> f p. f\<cdot>(cfst\<cdot>p)\<cdot>(csnd\<cdot>p))"
   206 
       
   207 definition
       
   208   csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c" where
       
   209   "csplit = (\<Lambda> f p. f\<cdot>(cfst\<cdot>p)\<cdot>(csnd\<cdot>p))"
   207 
   210 
   208 syntax
   211 syntax
   209   "_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(1<_,/ _>)")
   212   "_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(1<_,/ _>)")
   210 
   213 
   211 syntax (xsymbols)
   214 syntax (xsymbols)
   212   "_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(1\<langle>_,/ _\<rangle>)")
   215   "_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(1\<langle>_,/ _\<rangle>)")
   213 
   216 
   214 translations
   217 translations
   215   "\<langle>x, y, z\<rangle>" == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
   218   "\<langle>x, y, z\<rangle>" == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
   216   "\<langle>x, y\<rangle>"    == "cpair\<cdot>x\<cdot>y"
   219   "\<langle>x, y\<rangle>"    == "CONST cpair\<cdot>x\<cdot>y"
   217 
   220 
   218 translations
   221 translations
   219   "\<Lambda>(cpair\<cdot>x\<cdot>y). t" == "csplit\<cdot>(\<Lambda> x y. t)"
   222   "\<Lambda>(CONST cpair\<cdot>x\<cdot>y). t" == "CONST csplit\<cdot>(\<Lambda> x y. t)"
   220 
   223 
   221 
   224 
   222 subsection {* Convert all lemmas to the continuous versions *}
   225 subsection {* Convert all lemmas to the continuous versions *}
   223 
   226 
   224 lemma cpair_eq_pair: "<x, y> = (x, y)"
   227 lemma cpair_eq_pair: "<x, y> = (x, y)"