src/HOLCF/Cprod.thy
author huffman
Wed Nov 10 17:56:08 2010 -0800 (2010-11-10)
changeset 40502 8e92772bc0e8
parent 40002 c5b5f7a3a3b1
permissions -rw-r--r--
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
     1 (*  Title:      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 
    35 subsection {* Convert all lemmas to the continuous versions *}
    36 
    37 lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>"
    38 by (simp add: csplit_def)
    39 
    40 lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y"
    41 by (simp add: csplit_def)
    42 
    43 end