src/HOLCF/Product_Cpo.thy
author haftmann
Fri Jun 19 21:08:07 2009 +0200 (2009-06-19)
changeset 31726 ffd2dc631d88
parent 31112 4dcda8ca5d59
child 33506 afb577487b15
permissions -rw-r--r--
merged
     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 Adm
     9 begin
    10 
    11 defaultsort cpo
    12 
    13 subsection {* Type @{typ unit} is a pcpo *}
    14 
    15 instantiation unit :: below
    16 begin
    17 
    18 definition
    19   below_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<longleftrightarrow> 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 "*" :: (below, below) below
    36 begin
    37 
    38 definition
    39   below_prod_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 below_prod_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 below_prod_def Pair_fst_snd_eq
    53     by (fast intro: below_antisym)
    54 next
    55   fix x y z :: "'a \<times> 'b"
    56   assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
    57     unfolding below_prod_def
    58     by (fast intro: below_trans)
    59 qed
    60 
    61 subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
    62 
    63 lemma prod_belowI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"
    64 unfolding below_prod_def by simp
    65 
    66 lemma Pair_below_iff [simp]: "(a, b) \<sqsubseteq> (c, d) \<longleftrightarrow> a \<sqsubseteq> c \<and> b \<sqsubseteq> d"
    67 unfolding below_prod_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 lemma ch2ch_Pair [simp]:
    82   "chain X \<Longrightarrow> chain Y \<Longrightarrow> chain (\<lambda>i. (X i, Y i))"
    83 by (rule chainI, simp add: chainE)
    84 
    85 text {* @{term fst} and @{term snd} are monotone *}
    86 
    87 lemma monofun_fst: "monofun fst"
    88 by (simp add: monofun_def below_prod_def)
    89 
    90 lemma monofun_snd: "monofun snd"
    91 by (simp add: monofun_def below_prod_def)
    92 
    93 lemmas ch2ch_fst [simp] = ch2ch_monofun [OF monofun_fst]
    94 
    95 lemmas ch2ch_snd [simp] = ch2ch_monofun [OF monofun_snd]
    96 
    97 lemma prod_chain_cases:
    98   assumes "chain Y"
    99   obtains A B
   100   where "chain A" and "chain B" and "Y = (\<lambda>i. (A i, B i))"
   101 proof
   102   from `chain Y` show "chain (\<lambda>i. fst (Y i))" by (rule ch2ch_fst)
   103   from `chain Y` show "chain (\<lambda>i. snd (Y i))" by (rule ch2ch_snd)
   104   show "Y = (\<lambda>i. (fst (Y i), snd (Y i)))" by simp
   105 qed
   106 
   107 subsection {* Product type is a cpo *}
   108 
   109 lemma is_lub_Pair:
   110   "\<lbrakk>range A <<| x; range B <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (A i, B i)) <<| (x, y)"
   111 apply (rule is_lubI [OF ub_rangeI])
   112 apply (simp add: is_ub_lub)
   113 apply (frule ub2ub_monofun [OF monofun_fst])
   114 apply (drule ub2ub_monofun [OF monofun_snd])
   115 apply (simp add: below_prod_def is_lub_lub)
   116 done
   117 
   118 lemma thelub_Pair:
   119   "\<lbrakk>chain (A::nat \<Rightarrow> 'a::cpo); chain (B::nat \<Rightarrow> 'b::cpo)\<rbrakk>
   120     \<Longrightarrow> (\<Squnion>i. (A i, B i)) = (\<Squnion>i. A i, \<Squnion>i. B i)"
   121 by (fast intro: thelubI is_lub_Pair elim: thelubE)
   122 
   123 lemma lub_cprod:
   124   fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)"
   125   assumes S: "chain S"
   126   shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   127 proof -
   128   from `chain S` have "chain (\<lambda>i. fst (S i))"
   129     by (rule ch2ch_fst)
   130   hence 1: "range (\<lambda>i. fst (S i)) <<| (\<Squnion>i. fst (S i))"
   131     by (rule cpo_lubI)
   132   from `chain S` have "chain (\<lambda>i. snd (S i))"
   133     by (rule ch2ch_snd)
   134   hence 2: "range (\<lambda>i. snd (S i)) <<| (\<Squnion>i. snd (S i))"
   135     by (rule cpo_lubI)
   136   show "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   137     using is_lub_Pair [OF 1 2] by simp
   138 qed
   139 
   140 lemma thelub_cprod:
   141   "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
   142     \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   143 by (rule lub_cprod [THEN thelubI])
   144 
   145 instance "*" :: (cpo, cpo) cpo
   146 proof
   147   fix S :: "nat \<Rightarrow> ('a \<times> 'b)"
   148   assume "chain S"
   149   hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   150     by (rule lub_cprod)
   151   thus "\<exists>x. range S <<| x" ..
   152 qed
   153 
   154 instance "*" :: (finite_po, finite_po) finite_po ..
   155 
   156 instance "*" :: (discrete_cpo, discrete_cpo) discrete_cpo
   157 proof
   158   fix x y :: "'a \<times> 'b"
   159   show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
   160     unfolding below_prod_def Pair_fst_snd_eq
   161     by simp
   162 qed
   163 
   164 subsection {* Product type is pointed *}
   165 
   166 lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
   167 by (simp add: below_prod_def)
   168 
   169 instance "*" :: (pcpo, pcpo) pcpo
   170 by intro_classes (fast intro: minimal_cprod)
   171 
   172 lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
   173 by (rule minimal_cprod [THEN UU_I, symmetric])
   174 
   175 lemma Pair_defined_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
   176 unfolding inst_cprod_pcpo by simp
   177 
   178 lemma fst_strict [simp]: "fst \<bottom> = \<bottom>"
   179 unfolding inst_cprod_pcpo by (rule fst_conv)
   180 
   181 lemma csnd_strict [simp]: "snd \<bottom> = \<bottom>"
   182 unfolding inst_cprod_pcpo by (rule snd_conv)
   183 
   184 lemma Pair_strict [simp]: "(\<bottom>, \<bottom>) = \<bottom>"
   185 by simp
   186 
   187 lemma split_strict [simp]: "split f \<bottom> = f \<bottom> \<bottom>"
   188 unfolding split_def by simp
   189 
   190 subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
   191 
   192 lemma cont_pair1: "cont (\<lambda>x. (x, y))"
   193 apply (rule contI)
   194 apply (rule is_lub_Pair)
   195 apply (erule cpo_lubI)
   196 apply (rule lub_const)
   197 done
   198 
   199 lemma cont_pair2: "cont (\<lambda>y. (x, y))"
   200 apply (rule contI)
   201 apply (rule is_lub_Pair)
   202 apply (rule lub_const)
   203 apply (erule cpo_lubI)
   204 done
   205 
   206 lemma contlub_fst: "contlub fst"
   207 apply (rule contlubI)
   208 apply (simp add: thelub_cprod)
   209 done
   210 
   211 lemma contlub_snd: "contlub snd"
   212 apply (rule contlubI)
   213 apply (simp add: thelub_cprod)
   214 done
   215 
   216 lemma cont_fst: "cont fst"
   217 apply (rule monocontlub2cont)
   218 apply (rule monofun_fst)
   219 apply (rule contlub_fst)
   220 done
   221 
   222 lemma cont_snd: "cont snd"
   223 apply (rule monocontlub2cont)
   224 apply (rule monofun_snd)
   225 apply (rule contlub_snd)
   226 done
   227 
   228 lemma cont2cont_Pair [cont2cont]:
   229   assumes f: "cont (\<lambda>x. f x)"
   230   assumes g: "cont (\<lambda>x. g x)"
   231   shows "cont (\<lambda>x. (f x, g x))"
   232 apply (rule cont_apply [OF f cont_pair1])
   233 apply (rule cont_apply [OF g cont_pair2])
   234 apply (rule cont_const)
   235 done
   236 
   237 lemmas cont2cont_fst [cont2cont] = cont_compose [OF cont_fst]
   238 
   239 lemmas cont2cont_snd [cont2cont] = cont_compose [OF cont_snd]
   240 
   241 lemma cont2cont_split:
   242   assumes f1: "\<And>a b. cont (\<lambda>x. f x a b)"
   243   assumes f2: "\<And>x b. cont (\<lambda>a. f x a b)"
   244   assumes f3: "\<And>x a. cont (\<lambda>b. f x a b)"
   245   assumes g: "cont (\<lambda>x. g x)"
   246   shows "cont (\<lambda>x. split (\<lambda>a b. f x a b) (g x))"
   247 unfolding split_def
   248 apply (rule cont_apply [OF g])
   249 apply (rule cont_apply [OF cont_fst f2])
   250 apply (rule cont_apply [OF cont_snd f3])
   251 apply (rule cont_const)
   252 apply (rule f1)
   253 done
   254 
   255 lemma cont_fst_snd_D1:
   256   "cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>x. f x y)"
   257 by (drule cont_compose [OF _ cont_pair1], simp)
   258 
   259 lemma cont_fst_snd_D2:
   260   "cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>y. f x y)"
   261 by (drule cont_compose [OF _ cont_pair2], simp)
   262 
   263 lemma cont2cont_split' [cont2cont]:
   264   assumes f: "cont (\<lambda>p. f (fst p) (fst (snd p)) (snd (snd p)))"
   265   assumes g: "cont (\<lambda>x. g x)"
   266   shows "cont (\<lambda>x. split (f x) (g x))"
   267 proof -
   268   note f1 = f [THEN cont_fst_snd_D1]
   269   note f2 = f [THEN cont_fst_snd_D2, THEN cont_fst_snd_D1]
   270   note f3 = f [THEN cont_fst_snd_D2, THEN cont_fst_snd_D2]
   271   show ?thesis
   272     unfolding split_def
   273     apply (rule cont_apply [OF g])
   274     apply (rule cont_apply [OF cont_fst f2])
   275     apply (rule cont_apply [OF cont_snd f3])
   276     apply (rule cont_const)
   277     apply (rule f1)
   278     done
   279 qed
   280 
   281 subsection {* Compactness and chain-finiteness *}
   282 
   283 lemma fst_below_iff: "fst (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)"
   284 unfolding below_prod_def by simp
   285 
   286 lemma snd_below_iff: "snd (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (fst x, y)"
   287 unfolding below_prod_def by simp
   288 
   289 lemma compact_fst: "compact x \<Longrightarrow> compact (fst x)"
   290 by (rule compactI, simp add: fst_below_iff)
   291 
   292 lemma compact_snd: "compact x \<Longrightarrow> compact (snd x)"
   293 by (rule compactI, simp add: snd_below_iff)
   294 
   295 lemma compact_Pair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (x, y)"
   296 by (rule compactI, simp add: below_prod_def)
   297 
   298 lemma compact_Pair_iff [simp]: "compact (x, y) \<longleftrightarrow> compact x \<and> compact y"
   299 apply (safe intro!: compact_Pair)
   300 apply (drule compact_fst, simp)
   301 apply (drule compact_snd, simp)
   302 done
   303 
   304 instance "*" :: (chfin, chfin) chfin
   305 apply intro_classes
   306 apply (erule compact_imp_max_in_chain)
   307 apply (case_tac "\<Squnion>i. Y i", simp)
   308 done
   309 
   310 end