29531

1 
(* Title: HOLCF/Product_Cpo.thy


2 
Author: Franz Regensburger


3 
*)


4 


5 
header {* The cpo of cartesian products *}


6 


7 
theory Product_Cpo


8 
imports Ffun


9 
begin


10 


11 
defaultsort cpo


12 


13 
subsection {* Type @{typ unit} is a pcpo *}


14 


15 
instantiation unit :: sq_ord


16 
begin


17 


18 
definition


19 
less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True"


20 


21 
instance ..


22 
end


23 


24 
instance unit :: discrete_cpo


25 
by intro_classes simp


26 


27 
instance unit :: finite_po ..


28 


29 
instance unit :: pcpo


30 
by intro_classes simp


31 


32 


33 
subsection {* Product type is a partial order *}


34 


35 
instantiation "*" :: (sq_ord, sq_ord) sq_ord


36 
begin


37 


38 
definition


39 
less_cprod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"


40 


41 
instance ..


42 
end


43 


44 
instance "*" :: (po, po) po


45 
proof


46 
fix x :: "'a \<times> 'b"


47 
show "x \<sqsubseteq> x"


48 
unfolding less_cprod_def by simp


49 
next


50 
fix x y :: "'a \<times> 'b"


51 
assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"


52 
unfolding less_cprod_def Pair_fst_snd_eq


53 
by (fast intro: antisym_less)


54 
next


55 
fix x y z :: "'a \<times> 'b"


56 
assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"


57 
unfolding less_cprod_def


58 
by (fast intro: trans_less)


59 
qed


60 


61 
subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}


62 


63 
lemma prod_lessI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"


64 
unfolding less_cprod_def by simp


65 


66 
lemma Pair_less_iff [simp]: "(a, b) \<sqsubseteq> (c, d) = (a \<sqsubseteq> c \<and> b \<sqsubseteq> d)"


67 
unfolding less_cprod_def by simp


68 


69 
text {* Pair @{text "(_,_)"} is monotone in both arguments *}


70 


71 
lemma monofun_pair1: "monofun (\<lambda>x. (x, y))"


72 
by (simp add: monofun_def)


73 


74 
lemma monofun_pair2: "monofun (\<lambda>y. (x, y))"


75 
by (simp add: monofun_def)


76 


77 
lemma monofun_pair:


78 
"\<lbrakk>x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2\<rbrakk> \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)"


79 
by simp


80 


81 
text {* @{term fst} and @{term snd} are monotone *}


82 


83 
lemma monofun_fst: "monofun fst"


84 
by (simp add: monofun_def less_cprod_def)


85 


86 
lemma monofun_snd: "monofun snd"


87 
by (simp add: monofun_def less_cprod_def)


88 


89 
subsection {* Product type is a cpo *}


90 


91 
lemma is_lub_Pair:


92 
"\<lbrakk>range X << x; range Y << y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (X i, Y i)) << (x, y)"


93 
apply (rule is_lubI [OF ub_rangeI])


94 
apply (simp add: less_cprod_def is_ub_lub)


95 
apply (frule ub2ub_monofun [OF monofun_fst])


96 
apply (drule ub2ub_monofun [OF monofun_snd])


97 
apply (simp add: less_cprod_def is_lub_lub)


98 
done


99 


100 
lemma lub_cprod:


101 
fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)"


102 
assumes S: "chain S"


103 
shows "range S << (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"


104 
proof 


105 
have "chain (\<lambda>i. fst (S i))"


106 
using monofun_fst S by (rule ch2ch_monofun)


107 
hence 1: "range (\<lambda>i. fst (S i)) << (\<Squnion>i. fst (S i))"


108 
by (rule cpo_lubI)


109 
have "chain (\<lambda>i. snd (S i))"


110 
using monofun_snd S by (rule ch2ch_monofun)


111 
hence 2: "range (\<lambda>i. snd (S i)) << (\<Squnion>i. snd (S i))"


112 
by (rule cpo_lubI)


113 
show "range S << (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"


114 
using is_lub_Pair [OF 1 2] by simp


115 
qed


116 


117 
lemma thelub_cprod:


118 
"chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)


119 
\<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"


120 
by (rule lub_cprod [THEN thelubI])


121 


122 
instance "*" :: (cpo, cpo) cpo


123 
proof


124 
fix S :: "nat \<Rightarrow> ('a \<times> 'b)"


125 
assume "chain S"


126 
hence "range S << (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"


127 
by (rule lub_cprod)


128 
thus "\<exists>x. range S << x" ..


129 
qed


130 


131 
instance "*" :: (finite_po, finite_po) finite_po ..


132 


133 
instance "*" :: (discrete_cpo, discrete_cpo) discrete_cpo


134 
proof


135 
fix x y :: "'a \<times> 'b"


136 
show "x \<sqsubseteq> y \<longleftrightarrow> x = y"


137 
unfolding less_cprod_def Pair_fst_snd_eq


138 
by simp


139 
qed


140 


141 
subsection {* Product type is pointed *}


142 


143 
lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"


144 
by (simp add: less_cprod_def)


145 


146 
instance "*" :: (pcpo, pcpo) pcpo


147 
by intro_classes (fast intro: minimal_cprod)


148 


149 
lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"


150 
by (rule minimal_cprod [THEN UU_I, symmetric])


151 


152 


153 
subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}


154 


155 
lemma cont_pair1: "cont (\<lambda>x. (x, y))"


156 
apply (rule contI)


157 
apply (rule is_lub_Pair)


158 
apply (erule cpo_lubI)


159 
apply (rule lub_const)


160 
done


161 


162 
lemma cont_pair2: "cont (\<lambda>y. (x, y))"


163 
apply (rule contI)


164 
apply (rule is_lub_Pair)


165 
apply (rule lub_const)


166 
apply (erule cpo_lubI)


167 
done


168 


169 
lemma contlub_fst: "contlub fst"


170 
apply (rule contlubI)


171 
apply (simp add: thelub_cprod)


172 
done


173 


174 
lemma contlub_snd: "contlub snd"


175 
apply (rule contlubI)


176 
apply (simp add: thelub_cprod)


177 
done


178 


179 
lemma cont_fst: "cont fst"


180 
apply (rule monocontlub2cont)


181 
apply (rule monofun_fst)


182 
apply (rule contlub_fst)


183 
done


184 


185 
lemma cont_snd: "cont snd"


186 
apply (rule monocontlub2cont)


187 
apply (rule monofun_snd)


188 
apply (rule contlub_snd)


189 
done


190 


191 
lemma cont2cont_Pair [cont2cont]:


192 
assumes f: "cont (\<lambda>x. f x)"


193 
assumes g: "cont (\<lambda>x. g x)"


194 
shows "cont (\<lambda>x. (f x, g x))"


195 
apply (rule cont2cont_app2 [OF cont2cont_lambda cont_pair2 g])


196 
apply (rule cont2cont_app2 [OF cont_const cont_pair1 f])


197 
done


198 


199 
lemmas cont2cont_fst [cont2cont] = cont2cont_app3 [OF cont_fst]


200 


201 
lemmas cont2cont_snd [cont2cont] = cont2cont_app3 [OF cont_snd]


202 


203 
end
