1(*  Title:      HOL/HOLCF/Cprod.thy
2    Author:     Franz Regensburger
3*)
4
5section \<open>The cpo of cartesian products\<close>
6
7theory Cprod
8  imports Cfun
9begin
10
11default_sort cpo
12
13
14subsection \<open>Continuous case function for unit type\<close>
15
16definition unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a"
17  where "unit_when = (\<Lambda> a _. a)"
18
19translations
20  "\<Lambda>(). t" \<rightleftharpoons> "CONST unit_when\<cdot>t"
21
22lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a"
23  by (simp add: unit_when_def)
24
25
26subsection \<open>Continuous version of split function\<close>
27
28definition csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a \<times> 'b) \<rightarrow> 'c"
29  where "csplit = (\<Lambda> f p. f\<cdot>(fst p)\<cdot>(snd p))"
30
31translations
32  "\<Lambda>(CONST Pair x y). t" \<rightleftharpoons> "CONST csplit\<cdot>(\<Lambda> x y. t)"
33
34abbreviation cfst :: "'a \<times> 'b \<rightarrow> 'a"
35  where "cfst \<equiv> Abs_cfun fst"
36
37abbreviation csnd :: "'a \<times> 'b \<rightarrow> 'b"
38  where "csnd \<equiv> Abs_cfun snd"
39
40
41subsection \<open>Convert all lemmas to the continuous versions\<close>
42
43lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>"
44  by (simp add: csplit_def)
45
46lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y"
47  by (simp add: csplit_def)
48
49end
50