src/HOL/HOLCF/Cprod.thy
changeset 62175 8ffc4d0e652d
parent 58880 0baae4311a9f
child 67312 0d25e02759b7
equal deleted inserted replaced
62174:fae6233c5f37 62175:8ffc4d0e652d
     1 (*  Title:      HOL/HOLCF/Cprod.thy
     1 (*  Title:      HOL/HOLCF/Cprod.thy
     2     Author:     Franz Regensburger
     2     Author:     Franz Regensburger
     3 *)
     3 *)
     4 
     4 
     5 section {* The cpo of cartesian products *}
     5 section \<open>The cpo of cartesian products\<close>
     6 
     6 
     7 theory Cprod
     7 theory Cprod
     8 imports Cfun
     8 imports Cfun
     9 begin
     9 begin
    10 
    10 
    11 default_sort cpo
    11 default_sort cpo
    12 
    12 
    13 subsection {* Continuous case function for unit type *}
    13 subsection \<open>Continuous case function for unit type\<close>
    14 
    14 
    15 definition
    15 definition
    16   unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a" where
    16   unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a" where
    17   "unit_when = (\<Lambda> a _. a)"
    17   "unit_when = (\<Lambda> a _. a)"
    18 
    18 
    20   "\<Lambda>(). t" == "CONST unit_when\<cdot>t"
    20   "\<Lambda>(). t" == "CONST unit_when\<cdot>t"
    21 
    21 
    22 lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a"
    22 lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a"
    23 by (simp add: unit_when_def)
    23 by (simp add: unit_when_def)
    24 
    24 
    25 subsection {* Continuous version of split function *}
    25 subsection \<open>Continuous version of split function\<close>
    26 
    26 
    27 definition
    27 definition
    28   csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c" where
    28   csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c" where
    29   "csplit = (\<Lambda> f p. f\<cdot>(fst p)\<cdot>(snd p))"
    29   "csplit = (\<Lambda> f p. f\<cdot>(fst p)\<cdot>(snd p))"
    30 
    30 
    37 
    37 
    38 abbreviation
    38 abbreviation
    39   csnd :: "'a \<times> 'b \<rightarrow> 'b" where
    39   csnd :: "'a \<times> 'b \<rightarrow> 'b" where
    40   "csnd \<equiv> Abs_cfun snd"
    40   "csnd \<equiv> Abs_cfun snd"
    41 
    41 
    42 subsection {* Convert all lemmas to the continuous versions *}
    42 subsection \<open>Convert all lemmas to the continuous versions\<close>
    43 
    43 
    44 lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>"
    44 lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>"
    45 by (simp add: csplit_def)
    45 by (simp add: csplit_def)
    46 
    46 
    47 lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y"
    47 lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y"