src/HOL/HOLCF/Cprod.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 62175 8ffc4d0e652d
child 67312 0d25e02759b7
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      HOL/HOLCF/Cprod.thy
     2     Author:     Franz Regensburger
     3 *)
     4 
     5 section \<open>The cpo of cartesian products\<close>
     6 
     7 theory Cprod
     8 imports Cfun
     9 begin
    10 
    11 default_sort cpo
    12 
    13 subsection \<open>Continuous case function for unit type\<close>
    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 \<open>Continuous version of split function\<close>
    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 \<open>Convert all lemmas to the continuous versions\<close>
    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