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