src/HOL/HOLCF/Cprod.thy
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 62175 8ffc4d0e652d
child 67312 0d25e02759b7
permissions -rw-r--r--
tuned;
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/Cprod.thy
huffman@15576
     2
    Author:     Franz Regensburger
huffman@15576
     3
*)
huffman@15576
     4
wenzelm@62175
     5
section \<open>The cpo of cartesian products\<close>
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
wenzelm@62175
    13
subsection \<open>Continuous case function for unit type\<close>
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
wenzelm@62175
    25
subsection \<open>Continuous version of split function\<close>
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@45786
    34
abbreviation
huffman@45786
    35
  cfst :: "'a \<times> 'b \<rightarrow> 'a" where
huffman@45786
    36
  "cfst \<equiv> Abs_cfun fst"
huffman@45786
    37
huffman@45786
    38
abbreviation
huffman@45786
    39
  csnd :: "'a \<times> 'b \<rightarrow> 'b" where
huffman@45786
    40
  "csnd \<equiv> Abs_cfun snd"
huffman@15576
    41
wenzelm@62175
    42
subsection \<open>Convert all lemmas to the continuous versions\<close>
huffman@15576
    43
huffman@18077
    44
lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>"
huffman@18077
    45
by (simp add: csplit_def)
huffman@18077
    46
huffman@33399
    47
lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y"
huffman@35922
    48
by (simp add: csplit_def)
huffman@33399
    49
huffman@15576
    50
end