src/HOLCF/Product_Cpo.thy
author huffman
Wed Jan 14 18:18:48 2009 -0800 (2009-01-14)
changeset 29533 7f4a32134447
parent 29531 2eb29775b0b6
child 29535 08824fad8879
permissions -rw-r--r--
minimize dependencies
     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 Cont
     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_apply [OF _ cont_pair1 f])
   196 apply (rule cont2cont_apply [OF _ cont_pair2 g])
   197 apply (rule cont_const)
   198 done
   199 
   200 lemmas cont2cont_fst [cont2cont] = cont2cont_compose [OF cont_fst]
   201 
   202 lemmas cont2cont_snd [cont2cont] = cont2cont_compose [OF cont_snd]
   203 
   204 end