src/HOL/HOLCF/Product_Cpo.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 62175 8ffc4d0e652d
child 67312 0d25e02759b7
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      HOL/HOLCF/Product_Cpo.thy
     2     Author:     Franz Regensburger
     3 *)
     4 
     5 section \<open>The cpo of cartesian products\<close>
     6 
     7 theory Product_Cpo
     8 imports Adm
     9 begin
    10 
    11 default_sort cpo
    12 
    13 subsection \<open>Unit type is a pcpo\<close>
    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 \<open>Product type is a partial order\<close>
    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 prod_eq_iff
    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 \<open>Monotonicity of \emph{Pair}, \emph{fst}, \emph{snd}\<close>
    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 \<open>Pair \<open>(_,_)\<close>  is monotone in both arguments\<close>
    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 \<open>@{term fst} and @{term snd} are monotone\<close>
    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 \<open>chain Y\<close> show "chain (\<lambda>i. fst (Y i))" by (rule ch2ch_fst)
   106   from \<open>chain Y\<close> 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 \<open>Product type is a cpo\<close>
   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 unfolding is_lub_def is_ub_def ball_simps below_prod_def by simp
   115 
   116 lemma lub_Pair:
   117   "\<lbrakk>chain (A::nat \<Rightarrow> 'a::cpo); chain (B::nat \<Rightarrow> 'b::cpo)\<rbrakk>
   118     \<Longrightarrow> (\<Squnion>i. (A i, B i)) = (\<Squnion>i. A i, \<Squnion>i. B i)"
   119 by (fast intro: lub_eqI is_lub_Pair elim: thelubE)
   120 
   121 lemma is_lub_prod:
   122   fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)"
   123   assumes S: "chain S"
   124   shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   125 using S by (auto elim: prod_chain_cases simp add: is_lub_Pair cpo_lubI)
   126 
   127 lemma lub_prod:
   128   "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
   129     \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   130 by (rule is_lub_prod [THEN lub_eqI])
   131 
   132 instance prod :: (cpo, cpo) cpo
   133 proof
   134   fix S :: "nat \<Rightarrow> ('a \<times> 'b)"
   135   assume "chain S"
   136   hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   137     by (rule is_lub_prod)
   138   thus "\<exists>x. range S <<| x" ..
   139 qed
   140 
   141 instance prod :: (discrete_cpo, discrete_cpo) discrete_cpo
   142 proof
   143   fix x y :: "'a \<times> 'b"
   144   show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
   145     unfolding below_prod_def prod_eq_iff
   146     by simp
   147 qed
   148 
   149 subsection \<open>Product type is pointed\<close>
   150 
   151 lemma minimal_prod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
   152 by (simp add: below_prod_def)
   153 
   154 instance prod :: (pcpo, pcpo) pcpo
   155 by intro_classes (fast intro: minimal_prod)
   156 
   157 lemma inst_prod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
   158 by (rule minimal_prod [THEN bottomI, symmetric])
   159 
   160 lemma Pair_bottom_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
   161 unfolding inst_prod_pcpo by simp
   162 
   163 lemma fst_strict [simp]: "fst \<bottom> = \<bottom>"
   164 unfolding inst_prod_pcpo by (rule fst_conv)
   165 
   166 lemma snd_strict [simp]: "snd \<bottom> = \<bottom>"
   167 unfolding inst_prod_pcpo by (rule snd_conv)
   168 
   169 lemma Pair_strict [simp]: "(\<bottom>, \<bottom>) = \<bottom>"
   170 by simp
   171 
   172 lemma split_strict [simp]: "case_prod f \<bottom> = f \<bottom> \<bottom>"
   173 unfolding split_def by simp
   174 
   175 subsection \<open>Continuity of \emph{Pair}, \emph{fst}, \emph{snd}\<close>
   176 
   177 lemma cont_pair1: "cont (\<lambda>x. (x, y))"
   178 apply (rule contI)
   179 apply (rule is_lub_Pair)
   180 apply (erule cpo_lubI)
   181 apply (rule is_lub_const)
   182 done
   183 
   184 lemma cont_pair2: "cont (\<lambda>y. (x, y))"
   185 apply (rule contI)
   186 apply (rule is_lub_Pair)
   187 apply (rule is_lub_const)
   188 apply (erule cpo_lubI)
   189 done
   190 
   191 lemma cont_fst: "cont fst"
   192 apply (rule contI)
   193 apply (simp add: lub_prod)
   194 apply (erule cpo_lubI [OF ch2ch_fst])
   195 done
   196 
   197 lemma cont_snd: "cont snd"
   198 apply (rule contI)
   199 apply (simp add: lub_prod)
   200 apply (erule cpo_lubI [OF ch2ch_snd])
   201 done
   202 
   203 lemma cont2cont_Pair [simp, cont2cont]:
   204   assumes f: "cont (\<lambda>x. f x)"
   205   assumes g: "cont (\<lambda>x. g x)"
   206   shows "cont (\<lambda>x. (f x, g x))"
   207 apply (rule cont_apply [OF f cont_pair1])
   208 apply (rule cont_apply [OF g cont_pair2])
   209 apply (rule cont_const)
   210 done
   211 
   212 lemmas cont2cont_fst [simp, cont2cont] = cont_compose [OF cont_fst]
   213 
   214 lemmas cont2cont_snd [simp, cont2cont] = cont_compose [OF cont_snd]
   215 
   216 lemma cont2cont_case_prod:
   217   assumes f1: "\<And>a b. cont (\<lambda>x. f x a b)"
   218   assumes f2: "\<And>x b. cont (\<lambda>a. f x a b)"
   219   assumes f3: "\<And>x a. cont (\<lambda>b. f x a b)"
   220   assumes g: "cont (\<lambda>x. g x)"
   221   shows "cont (\<lambda>x. case g x of (a, b) \<Rightarrow> f x a b)"
   222 unfolding split_def
   223 apply (rule cont_apply [OF g])
   224 apply (rule cont_apply [OF cont_fst f2])
   225 apply (rule cont_apply [OF cont_snd f3])
   226 apply (rule cont_const)
   227 apply (rule f1)
   228 done
   229 
   230 lemma prod_contI:
   231   assumes f1: "\<And>y. cont (\<lambda>x. f (x, y))"
   232   assumes f2: "\<And>x. cont (\<lambda>y. f (x, y))"
   233   shows "cont f"
   234 proof -
   235   have "cont (\<lambda>(x, y). f (x, y))"
   236     by (intro cont2cont_case_prod f1 f2 cont2cont)
   237   thus "cont f"
   238     by (simp only: case_prod_eta)
   239 qed
   240 
   241 lemma prod_cont_iff:
   242   "cont f \<longleftrightarrow> (\<forall>y. cont (\<lambda>x. f (x, y))) \<and> (\<forall>x. cont (\<lambda>y. f (x, y)))"
   243 apply safe
   244 apply (erule cont_compose [OF _ cont_pair1])
   245 apply (erule cont_compose [OF _ cont_pair2])
   246 apply (simp only: prod_contI)
   247 done
   248 
   249 lemma cont2cont_case_prod' [simp, cont2cont]:
   250   assumes f: "cont (\<lambda>p. f (fst p) (fst (snd p)) (snd (snd p)))"
   251   assumes g: "cont (\<lambda>x. g x)"
   252   shows "cont (\<lambda>x. case_prod (f x) (g x))"
   253 using assms by (simp add: cont2cont_case_prod prod_cont_iff)
   254 
   255 text \<open>The simple version (due to Joachim Breitner) is needed if
   256   either element type of the pair is not a cpo.\<close>
   257 
   258 lemma cont2cont_split_simple [simp, cont2cont]:
   259  assumes "\<And>a b. cont (\<lambda>x. f x a b)"
   260  shows "cont (\<lambda>x. case p of (a, b) \<Rightarrow> f x a b)"
   261 using assms by (cases p) auto
   262 
   263 text \<open>Admissibility of predicates on product types.\<close>
   264 
   265 lemma adm_case_prod [simp]:
   266   assumes "adm (\<lambda>x. P x (fst (f x)) (snd (f x)))"
   267   shows "adm (\<lambda>x. case f x of (a, b) \<Rightarrow> P x a b)"
   268 unfolding case_prod_beta using assms .
   269 
   270 subsection \<open>Compactness and chain-finiteness\<close>
   271 
   272 lemma fst_below_iff: "fst (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)"
   273 unfolding below_prod_def by simp
   274 
   275 lemma snd_below_iff: "snd (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (fst x, y)"
   276 unfolding below_prod_def by simp
   277 
   278 lemma compact_fst: "compact x \<Longrightarrow> compact (fst x)"
   279 by (rule compactI, simp add: fst_below_iff)
   280 
   281 lemma compact_snd: "compact x \<Longrightarrow> compact (snd x)"
   282 by (rule compactI, simp add: snd_below_iff)
   283 
   284 lemma compact_Pair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (x, y)"
   285 by (rule compactI, simp add: below_prod_def)
   286 
   287 lemma compact_Pair_iff [simp]: "compact (x, y) \<longleftrightarrow> compact x \<and> compact y"
   288 apply (safe intro!: compact_Pair)
   289 apply (drule compact_fst, simp)
   290 apply (drule compact_snd, simp)
   291 done
   292 
   293 instance prod :: (chfin, chfin) chfin
   294 apply intro_classes
   295 apply (erule compact_imp_max_in_chain)
   296 apply (case_tac "\<Squnion>i. Y i", simp)
   297 done
   298 
   299 end