src/HOL/HOLCF/Cprod.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 45786 3f07a7a91180
child 58880 0baae4311a9f
permissions -rw-r--r--
Quotient_Info stores only relation maps
     1 (*  Title:      HOL/HOLCF/Cprod.thy
     2     Author:     Franz Regensburger
     3 *)
     4 
     5 header {* The cpo of cartesian products *}
     6 
     7 theory Cprod
     8 imports Cfun
     9 begin
    10 
    11 default_sort cpo
    12 
    13 subsection {* Continuous case function for unit type *}
    14 
    15 definition
    16   unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a" where
    17   "unit_when = (\<Lambda> a _. a)"
    18 
    19 translations
    20   "\<Lambda>(). t" == "CONST unit_when\<cdot>t"
    21 
    22 lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a"
    23 by (simp add: unit_when_def)
    24 
    25 subsection {* Continuous version of split function *}
    26 
    27 definition
    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))"
    30 
    31 translations
    32   "\<Lambda>(CONST Pair x y). t" == "CONST csplit\<cdot>(\<Lambda> x y. t)"
    33 
    34 abbreviation
    35   cfst :: "'a \<times> 'b \<rightarrow> 'a" where
    36   "cfst \<equiv> Abs_cfun fst"
    37 
    38 abbreviation
    39   csnd :: "'a \<times> 'b \<rightarrow> 'b" where
    40   "csnd \<equiv> Abs_cfun snd"
    41 
    42 subsection {* Convert all lemmas to the continuous versions *}
    43 
    44 lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>"
    45 by (simp add: csplit_def)
    46 
    47 lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y"
    48 by (simp add: csplit_def)
    49 
    50 end