src/HOLCF/Product_Cpo.thy
author huffman
Wed Nov 10 17:56:08 2010 -0800 (2010-11-10)
changeset 40502 8e92772bc0e8
parent 40321 d065b195ec89
child 40619 84edf7177d73
permissions -rw-r--r--
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
     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 default_sort cpo
    12 
    13 subsection {* Unit type is a pcpo *}
    14 
    15 instantiation unit :: discrete_cpo
    16 begin
    17 
    18 definition
    19   below_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<longleftrightarrow> True"
    20 
    21 instance proof
    22 qed simp
    23 
    24 end
    25 
    26 instance unit :: pcpo
    27 by intro_classes simp
    28 
    29 
    30 subsection {* Product type is a partial order *}
    31 
    32 instantiation prod :: (below, below) below
    33 begin
    34 
    35 definition
    36   below_prod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
    37 
    38 instance ..
    39 end
    40 
    41 instance prod :: (po, po) po
    42 proof
    43   fix x :: "'a \<times> 'b"
    44   show "x \<sqsubseteq> x"
    45     unfolding below_prod_def by simp
    46 next
    47   fix x y :: "'a \<times> 'b"
    48   assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
    49     unfolding below_prod_def Pair_fst_snd_eq
    50     by (fast intro: below_antisym)
    51 next
    52   fix x y z :: "'a \<times> 'b"
    53   assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
    54     unfolding below_prod_def
    55     by (fast intro: below_trans)
    56 qed
    57 
    58 subsection {* Monotonicity of \emph{Pair}, \emph{fst}, \emph{snd} *}
    59 
    60 lemma prod_belowI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"
    61 unfolding below_prod_def by simp
    62 
    63 lemma Pair_below_iff [simp]: "(a, b) \<sqsubseteq> (c, d) \<longleftrightarrow> a \<sqsubseteq> c \<and> b \<sqsubseteq> d"
    64 unfolding below_prod_def by simp
    65 
    66 text {* Pair @{text "(_,_)"}  is monotone in both arguments *}
    67 
    68 lemma monofun_pair1: "monofun (\<lambda>x. (x, y))"
    69 by (simp add: monofun_def)
    70 
    71 lemma monofun_pair2: "monofun (\<lambda>y. (x, y))"
    72 by (simp add: monofun_def)
    73 
    74 lemma monofun_pair:
    75   "\<lbrakk>x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2\<rbrakk> \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)"
    76 by simp
    77 
    78 lemma ch2ch_Pair [simp]:
    79   "chain X \<Longrightarrow> chain Y \<Longrightarrow> chain (\<lambda>i. (X i, Y i))"
    80 by (rule chainI, simp add: chainE)
    81 
    82 text {* @{term fst} and @{term snd} are monotone *}
    83 
    84 lemma fst_monofun: "x \<sqsubseteq> y \<Longrightarrow> fst x \<sqsubseteq> fst y"
    85 unfolding below_prod_def by simp
    86 
    87 lemma snd_monofun: "x \<sqsubseteq> y \<Longrightarrow> snd x \<sqsubseteq> snd y"
    88 unfolding below_prod_def by simp
    89 
    90 lemma monofun_fst: "monofun fst"
    91 by (simp add: monofun_def below_prod_def)
    92 
    93 lemma monofun_snd: "monofun snd"
    94 by (simp add: monofun_def below_prod_def)
    95 
    96 lemmas ch2ch_fst [simp] = ch2ch_monofun [OF monofun_fst]
    97 
    98 lemmas ch2ch_snd [simp] = ch2ch_monofun [OF monofun_snd]
    99 
   100 lemma prod_chain_cases:
   101   assumes "chain Y"
   102   obtains A B
   103   where "chain A" and "chain B" and "Y = (\<lambda>i. (A i, B i))"
   104 proof
   105   from `chain Y` show "chain (\<lambda>i. fst (Y i))" by (rule ch2ch_fst)
   106   from `chain Y` show "chain (\<lambda>i. snd (Y i))" by (rule ch2ch_snd)
   107   show "Y = (\<lambda>i. (fst (Y i), snd (Y i)))" by simp
   108 qed
   109 
   110 subsection {* Product type is a cpo *}
   111 
   112 lemma is_lub_Pair:
   113   "\<lbrakk>range A <<| x; range B <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (A i, B i)) <<| (x, y)"
   114 apply (rule is_lubI [OF ub_rangeI])
   115 apply (simp add: is_ub_lub)
   116 apply (frule ub2ub_monofun [OF monofun_fst])
   117 apply (drule ub2ub_monofun [OF monofun_snd])
   118 apply (simp add: below_prod_def is_lub_lub)
   119 done
   120 
   121 lemma thelub_Pair:
   122   "\<lbrakk>chain (A::nat \<Rightarrow> 'a::cpo); chain (B::nat \<Rightarrow> 'b::cpo)\<rbrakk>
   123     \<Longrightarrow> (\<Squnion>i. (A i, B i)) = (\<Squnion>i. A i, \<Squnion>i. B i)"
   124 by (fast intro: thelubI is_lub_Pair elim: thelubE)
   125 
   126 lemma lub_cprod:
   127   fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)"
   128   assumes S: "chain S"
   129   shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   130 proof -
   131   from `chain S` have "chain (\<lambda>i. fst (S i))"
   132     by (rule ch2ch_fst)
   133   hence 1: "range (\<lambda>i. fst (S i)) <<| (\<Squnion>i. fst (S i))"
   134     by (rule cpo_lubI)
   135   from `chain S` have "chain (\<lambda>i. snd (S i))"
   136     by (rule ch2ch_snd)
   137   hence 2: "range (\<lambda>i. snd (S i)) <<| (\<Squnion>i. snd (S i))"
   138     by (rule cpo_lubI)
   139   show "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   140     using is_lub_Pair [OF 1 2] by simp
   141 qed
   142 
   143 lemma thelub_cprod:
   144   "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
   145     \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   146 by (rule lub_cprod [THEN thelubI])
   147 
   148 instance prod :: (cpo, cpo) cpo
   149 proof
   150   fix S :: "nat \<Rightarrow> ('a \<times> 'b)"
   151   assume "chain S"
   152   hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   153     by (rule lub_cprod)
   154   thus "\<exists>x. range S <<| x" ..
   155 qed
   156 
   157 instance prod :: (discrete_cpo, discrete_cpo) discrete_cpo
   158 proof
   159   fix x y :: "'a \<times> 'b"
   160   show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
   161     unfolding below_prod_def Pair_fst_snd_eq
   162     by simp
   163 qed
   164 
   165 subsection {* Product type is pointed *}
   166 
   167 lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
   168 by (simp add: below_prod_def)
   169 
   170 instance prod :: (pcpo, pcpo) pcpo
   171 by intro_classes (fast intro: minimal_cprod)
   172 
   173 lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
   174 by (rule minimal_cprod [THEN UU_I, symmetric])
   175 
   176 lemma Pair_bottom_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
   177 unfolding inst_cprod_pcpo by simp
   178 
   179 lemma fst_strict [simp]: "fst \<bottom> = \<bottom>"
   180 unfolding inst_cprod_pcpo by (rule fst_conv)
   181 
   182 lemma snd_strict [simp]: "snd \<bottom> = \<bottom>"
   183 unfolding inst_cprod_pcpo by (rule snd_conv)
   184 
   185 lemma Pair_strict [simp]: "(\<bottom>, \<bottom>) = \<bottom>"
   186 by simp
   187 
   188 lemma split_strict [simp]: "split f \<bottom> = f \<bottom> \<bottom>"
   189 unfolding split_def by simp
   190 
   191 subsection {* Continuity of \emph{Pair}, \emph{fst}, \emph{snd} *}
   192 
   193 lemma cont_pair1: "cont (\<lambda>x. (x, y))"
   194 apply (rule contI)
   195 apply (rule is_lub_Pair)
   196 apply (erule cpo_lubI)
   197 apply (rule lub_const)
   198 done
   199 
   200 lemma cont_pair2: "cont (\<lambda>y. (x, y))"
   201 apply (rule contI)
   202 apply (rule is_lub_Pair)
   203 apply (rule lub_const)
   204 apply (erule cpo_lubI)
   205 done
   206 
   207 lemma cont_fst: "cont fst"
   208 apply (rule contI)
   209 apply (simp add: thelub_cprod)
   210 apply (erule cpo_lubI [OF ch2ch_fst])
   211 done
   212 
   213 lemma cont_snd: "cont snd"
   214 apply (rule contI)
   215 apply (simp add: thelub_cprod)
   216 apply (erule cpo_lubI [OF ch2ch_snd])
   217 done
   218 
   219 lemma cont2cont_Pair [simp, cont2cont]:
   220   assumes f: "cont (\<lambda>x. f x)"
   221   assumes g: "cont (\<lambda>x. g x)"
   222   shows "cont (\<lambda>x. (f x, g x))"
   223 apply (rule cont_apply [OF f cont_pair1])
   224 apply (rule cont_apply [OF g cont_pair2])
   225 apply (rule cont_const)
   226 done
   227 
   228 lemmas cont2cont_fst [simp, cont2cont] = cont_compose [OF cont_fst]
   229 
   230 lemmas cont2cont_snd [simp, cont2cont] = cont_compose [OF cont_snd]
   231 
   232 lemma cont2cont_prod_case:
   233   assumes f1: "\<And>a b. cont (\<lambda>x. f x a b)"
   234   assumes f2: "\<And>x b. cont (\<lambda>a. f x a b)"
   235   assumes f3: "\<And>x a. cont (\<lambda>b. f x a b)"
   236   assumes g: "cont (\<lambda>x. g x)"
   237   shows "cont (\<lambda>x. case g x of (a, b) \<Rightarrow> f x a b)"
   238 unfolding split_def
   239 apply (rule cont_apply [OF g])
   240 apply (rule cont_apply [OF cont_fst f2])
   241 apply (rule cont_apply [OF cont_snd f3])
   242 apply (rule cont_const)
   243 apply (rule f1)
   244 done
   245 
   246 lemma prod_contI:
   247   assumes f1: "\<And>y. cont (\<lambda>x. f (x, y))"
   248   assumes f2: "\<And>x. cont (\<lambda>y. f (x, y))"
   249   shows "cont f"
   250 proof -
   251   have "cont (\<lambda>(x, y). f (x, y))"
   252     by (intro cont2cont_prod_case f1 f2 cont2cont)
   253   thus "cont f"
   254     by (simp only: split_eta)
   255 qed
   256 
   257 lemma prod_cont_iff:
   258   "cont f \<longleftrightarrow> (\<forall>y. cont (\<lambda>x. f (x, y))) \<and> (\<forall>x. cont (\<lambda>y. f (x, y)))"
   259 apply safe
   260 apply (erule cont_compose [OF _ cont_pair1])
   261 apply (erule cont_compose [OF _ cont_pair2])
   262 apply (simp only: prod_contI)
   263 done
   264 
   265 lemma cont2cont_prod_case' [simp, cont2cont]:
   266   assumes f: "cont (\<lambda>p. f (fst p) (fst (snd p)) (snd (snd p)))"
   267   assumes g: "cont (\<lambda>x. g x)"
   268   shows "cont (\<lambda>x. prod_case (f x) (g x))"
   269 using assms by (simp add: cont2cont_prod_case prod_cont_iff)
   270 
   271 text {* The simple version (due to Joachim Breitner) is needed if
   272   either element type of the pair is not a cpo. *}
   273 
   274 lemma cont2cont_split_simple [simp, cont2cont]:
   275  assumes "\<And>a b. cont (\<lambda>x. f x a b)"
   276  shows "cont (\<lambda>x. case p of (a, b) \<Rightarrow> f x a b)"
   277 using assms by (cases p) auto
   278 
   279 subsection {* Compactness and chain-finiteness *}
   280 
   281 lemma fst_below_iff: "fst (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)"
   282 unfolding below_prod_def by simp
   283 
   284 lemma snd_below_iff: "snd (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (fst x, y)"
   285 unfolding below_prod_def by simp
   286 
   287 lemma compact_fst: "compact x \<Longrightarrow> compact (fst x)"
   288 by (rule compactI, simp add: fst_below_iff)
   289 
   290 lemma compact_snd: "compact x \<Longrightarrow> compact (snd x)"
   291 by (rule compactI, simp add: snd_below_iff)
   292 
   293 lemma compact_Pair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (x, y)"
   294 by (rule compactI, simp add: below_prod_def)
   295 
   296 lemma compact_Pair_iff [simp]: "compact (x, y) \<longleftrightarrow> compact x \<and> compact y"
   297 apply (safe intro!: compact_Pair)
   298 apply (drule compact_fst, simp)
   299 apply (drule compact_snd, simp)
   300 done
   301 
   302 instance prod :: (chfin, chfin) chfin
   303 apply intro_classes
   304 apply (erule compact_imp_max_in_chain)
   305 apply (case_tac "\<Squnion>i. Y i", simp)
   306 done
   307 
   308 end