src/HOL/HOLCF/Cprod.thy
changeset 45786 3f07a7a91180
parent 42151 4da4fc77664b
child 58880 0baae4311a9f
equal deleted inserted replaced
45785:192243fd94a5 45786:3f07a7a91180
    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 
    31 translations
    31 translations
    32   "\<Lambda>(CONST Pair x y). t" == "CONST csplit\<cdot>(\<Lambda> x y. t)"
    32   "\<Lambda>(CONST Pair x y). t" == "CONST csplit\<cdot>(\<Lambda> x y. t)"
    33 
    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"
    34 
    41 
    35 subsection {* Convert all lemmas to the continuous versions *}
    42 subsection {* Convert all lemmas to the continuous versions *}
    36 
    43 
    37 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>"
    38 by (simp add: csplit_def)
    45 by (simp add: csplit_def)