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
huffman@15600
     1
(*  Title:      HOLCF/Cprod.thy
huffman@15576
     2
    Author:     Franz Regensburger
huffman@15576
     3
*)
huffman@15576
     4
huffman@15576
     5
header {* The cpo of cartesian products *}
huffman@15576
     6
huffman@15577
     7
theory Cprod
huffman@40502
     8
imports Cfun
huffman@15577
     9
begin
huffman@15576
    10
wenzelm@36452
    11
default_sort cpo
huffman@15576
    12
huffman@35900
    13
subsection {* Continuous case function for unit type *}
huffman@16008
    14
wenzelm@25131
    15
definition
wenzelm@25131
    16
  unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a" where
wenzelm@25131
    17
  "unit_when = (\<Lambda> a _. a)"
huffman@16008
    18
huffman@18289
    19
translations
wenzelm@25131
    20
  "\<Lambda>(). t" == "CONST unit_when\<cdot>t"
huffman@18289
    21
huffman@18289
    22
lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a"
huffman@18289
    23
by (simp add: unit_when_def)
huffman@18289
    24
huffman@35926
    25
subsection {* Continuous version of split function *}
huffman@17834
    26
wenzelm@25131
    27
definition
wenzelm@25131
    28
  csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c" where
huffman@35922
    29
  "csplit = (\<Lambda> f p. f\<cdot>(fst p)\<cdot>(snd p))"
huffman@15576
    30
huffman@15576
    31
translations
huffman@35926
    32
  "\<Lambda>(CONST Pair x y). t" == "CONST csplit\<cdot>(\<Lambda> x y. t)"
huffman@17816
    33
huffman@15576
    34
huffman@15593
    35
subsection {* Convert all lemmas to the continuous versions *}
huffman@15576
    36
huffman@18077
    37
lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>"
huffman@18077
    38
by (simp add: csplit_def)
huffman@18077
    39
huffman@33399
    40
lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y"
huffman@35922
    41
by (simp add: csplit_def)
huffman@33399
    42
huffman@15576
    43
end