src/HOLCF/Product_Cpo.thy
author huffman
Wed May 06 00:57:29 2009 -0700 (2009-05-06)
changeset 31041 85b4843d9939
parent 29535 08824fad8879
child 31076 99fe356cbbc2
permissions -rw-r--r--
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
     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 :: 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) \<longleftrightarrow> 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 lemma Pair_defined_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
   153 unfolding inst_cprod_pcpo by simp
   154 
   155 lemma fst_strict [simp]: "fst \<bottom> = \<bottom>"
   156 unfolding inst_cprod_pcpo by (rule fst_conv)
   157 
   158 lemma csnd_strict [simp]: "snd \<bottom> = \<bottom>"
   159 unfolding inst_cprod_pcpo by (rule snd_conv)
   160 
   161 lemma Pair_strict [simp]: "(\<bottom>, \<bottom>) = \<bottom>"
   162 by simp
   163 
   164 lemma split_strict [simp]: "split f \<bottom> = f \<bottom> \<bottom>"
   165 unfolding split_def by simp
   166 
   167 subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
   168 
   169 lemma cont_pair1: "cont (\<lambda>x. (x, y))"
   170 apply (rule contI)
   171 apply (rule is_lub_Pair)
   172 apply (erule cpo_lubI)
   173 apply (rule lub_const)
   174 done
   175 
   176 lemma cont_pair2: "cont (\<lambda>y. (x, y))"
   177 apply (rule contI)
   178 apply (rule is_lub_Pair)
   179 apply (rule lub_const)
   180 apply (erule cpo_lubI)
   181 done
   182 
   183 lemma contlub_fst: "contlub fst"
   184 apply (rule contlubI)
   185 apply (simp add: thelub_cprod)
   186 done
   187 
   188 lemma contlub_snd: "contlub snd"
   189 apply (rule contlubI)
   190 apply (simp add: thelub_cprod)
   191 done
   192 
   193 lemma cont_fst: "cont fst"
   194 apply (rule monocontlub2cont)
   195 apply (rule monofun_fst)
   196 apply (rule contlub_fst)
   197 done
   198 
   199 lemma cont_snd: "cont snd"
   200 apply (rule monocontlub2cont)
   201 apply (rule monofun_snd)
   202 apply (rule contlub_snd)
   203 done
   204 
   205 lemma cont2cont_Pair [cont2cont]:
   206   assumes f: "cont (\<lambda>x. f x)"
   207   assumes g: "cont (\<lambda>x. g x)"
   208   shows "cont (\<lambda>x. (f x, g x))"
   209 apply (rule cont_apply [OF f cont_pair1])
   210 apply (rule cont_apply [OF g cont_pair2])
   211 apply (rule cont_const)
   212 done
   213 
   214 lemmas cont2cont_fst [cont2cont] = cont_compose [OF cont_fst]
   215 
   216 lemmas cont2cont_snd [cont2cont] = cont_compose [OF cont_snd]
   217 
   218 lemma cont2cont_split:
   219   assumes f1: "\<And>a b. cont (\<lambda>x. f x a b)"
   220   assumes f2: "\<And>x b. cont (\<lambda>a. f x a b)"
   221   assumes f3: "\<And>x a. cont (\<lambda>b. f x a b)"
   222   assumes g: "cont (\<lambda>x. g x)"
   223   shows "cont (\<lambda>x. split (\<lambda>a b. f x a b) (g x))"
   224 unfolding split_def
   225 apply (rule cont_apply [OF g])
   226 apply (rule cont_apply [OF cont_fst f2])
   227 apply (rule cont_apply [OF cont_snd f3])
   228 apply (rule cont_const)
   229 apply (rule f1)
   230 done
   231 
   232 lemma cont_fst_snd_D1:
   233   "cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>x. f x y)"
   234 by (drule cont_compose [OF _ cont_pair1], simp)
   235 
   236 lemma cont_fst_snd_D2:
   237   "cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>y. f x y)"
   238 by (drule cont_compose [OF _ cont_pair2], simp)
   239 
   240 lemma cont2cont_split' [cont2cont]:
   241   assumes f: "cont (\<lambda>p. f (fst p) (fst (snd p)) (snd (snd p)))"
   242   assumes g: "cont (\<lambda>x. g x)"
   243   shows "cont (\<lambda>x. split (f x) (g x))"
   244 proof -
   245   note f1 = f [THEN cont_fst_snd_D1]
   246   note f2 = f [THEN cont_fst_snd_D2, THEN cont_fst_snd_D1]
   247   note f3 = f [THEN cont_fst_snd_D2, THEN cont_fst_snd_D2]
   248   show ?thesis
   249     unfolding split_def
   250     apply (rule cont_apply [OF g])
   251     apply (rule cont_apply [OF cont_fst f2])
   252     apply (rule cont_apply [OF cont_snd f3])
   253     apply (rule cont_const)
   254     apply (rule f1)
   255     done
   256 qed
   257 
   258 subsection {* Compactness and chain-finiteness *}
   259 
   260 lemma fst_less_iff: "fst (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)"
   261 unfolding less_cprod_def by simp
   262 
   263 lemma snd_less_iff: "snd (x::'a \<times> 'b) \<sqsubseteq> y = x \<sqsubseteq> (fst x, y)"
   264 unfolding less_cprod_def by simp
   265 
   266 lemma compact_fst: "compact x \<Longrightarrow> compact (fst x)"
   267 by (rule compactI, simp add: fst_less_iff)
   268 
   269 lemma compact_snd: "compact x \<Longrightarrow> compact (snd x)"
   270 by (rule compactI, simp add: snd_less_iff)
   271 
   272 lemma compact_Pair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (x, y)"
   273 by (rule compactI, simp add: less_cprod_def)
   274 
   275 lemma compact_Pair_iff [simp]: "compact (x, y) \<longleftrightarrow> compact x \<and> compact y"
   276 apply (safe intro!: compact_Pair)
   277 apply (drule compact_fst, simp)
   278 apply (drule compact_snd, simp)
   279 done
   280 
   281 instance "*" :: (chfin, chfin) chfin
   282 apply intro_classes
   283 apply (erule compact_imp_max_in_chain)
   284 apply (case_tac "\<Squnion>i. Y i", simp)
   285 done
   286 
   287 end