src/HOLCF/Cprod.thy
author huffman
Thu Jan 10 05:15:43 2008 +0100 (2008-01-10)
changeset 25879 98b93782c3b1
parent 25827 c2adeb1bae5c
child 25905 098469c6c351
permissions -rw-r--r--
new compactness lemmas
     1 (*  Title:      HOLCF/Cprod.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4 
     5 Partial ordering for cartesian product of HOL products.
     6 *)
     7 
     8 header {* The cpo of cartesian products *}
     9 
    10 theory Cprod
    11 imports Cfun
    12 begin
    13 
    14 defaultsort cpo
    15 
    16 subsection {* Type @{typ unit} is a pcpo *}
    17 
    18 instantiation unit :: sq_ord
    19 begin
    20 
    21 definition
    22   less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True"
    23 
    24 instance ..
    25 end
    26 
    27 instance unit :: po
    28 by intro_classes simp_all
    29 
    30 instance unit :: finite_po ..
    31 
    32 instance unit :: pcpo
    33 by intro_classes simp
    34 
    35 definition
    36   unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a" where
    37   "unit_when = (\<Lambda> a _. a)"
    38 
    39 translations
    40   "\<Lambda>(). t" == "CONST unit_when\<cdot>t"
    41 
    42 lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a"
    43 by (simp add: unit_when_def)
    44 
    45 
    46 subsection {* Product type is a partial order *}
    47 
    48 instantiation "*" :: (sq_ord, sq_ord) sq_ord
    49 begin
    50 
    51 definition
    52   less_cprod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
    53 
    54 instance ..
    55 end
    56 
    57 instance "*" :: (po, po) po
    58 proof
    59   fix x :: "'a \<times> 'b"
    60   show "x \<sqsubseteq> x"
    61     unfolding less_cprod_def by simp
    62 next
    63   fix x y :: "'a \<times> 'b"
    64   assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
    65     unfolding less_cprod_def Pair_fst_snd_eq
    66     by (fast intro: antisym_less)
    67 next
    68   fix x y z :: "'a \<times> 'b"
    69   assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
    70     unfolding less_cprod_def
    71     by (fast intro: trans_less)
    72 qed
    73 
    74 
    75 subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
    76 
    77 text {* Pair @{text "(_,_)"}  is monotone in both arguments *}
    78 
    79 lemma monofun_pair1: "monofun (\<lambda>x. (x, y))"
    80 by (simp add: monofun_def less_cprod_def)
    81 
    82 lemma monofun_pair2: "monofun (\<lambda>y. (x, y))"
    83 by (simp add: monofun_def less_cprod_def)
    84 
    85 lemma monofun_pair:
    86   "\<lbrakk>x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2\<rbrakk> \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)"
    87 by (simp add: less_cprod_def)
    88 
    89 text {* @{term fst} and @{term snd} are monotone *}
    90 
    91 lemma monofun_fst: "monofun fst"
    92 by (simp add: monofun_def less_cprod_def)
    93 
    94 lemma monofun_snd: "monofun snd"
    95 by (simp add: monofun_def less_cprod_def)
    96 
    97 subsection {* Product type is a cpo *}
    98 
    99 lemma lub_cprod:
   100   fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)"
   101   assumes S: "chain S"
   102   shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   103 apply (rule is_lubI)
   104 apply (rule ub_rangeI)
   105 apply (rule_tac t = "S i" in surjective_pairing [THEN ssubst])
   106 apply (rule monofun_pair)
   107 apply (rule is_ub_thelub)
   108 apply (rule ch2ch_monofun [OF monofun_fst S])
   109 apply (rule is_ub_thelub)
   110 apply (rule ch2ch_monofun [OF monofun_snd S])
   111 apply (rule_tac t = "u" in surjective_pairing [THEN ssubst])
   112 apply (rule monofun_pair)
   113 apply (rule is_lub_thelub)
   114 apply (rule ch2ch_monofun [OF monofun_fst S])
   115 apply (erule monofun_fst [THEN ub2ub_monofun])
   116 apply (rule is_lub_thelub)
   117 apply (rule ch2ch_monofun [OF monofun_snd S])
   118 apply (erule monofun_snd [THEN ub2ub_monofun])
   119 done
   120 
   121 lemma directed_lub_cprod:
   122   fixes S :: "('a::dcpo \<times> 'b::dcpo) set"
   123   assumes S: "directed S"
   124   shows "S <<| (\<Squnion>x\<in>S. fst x, \<Squnion>x\<in>S. snd x)"
   125 apply (rule is_lubI)
   126 apply (rule is_ubI)
   127 apply (rule_tac t=x in surjective_pairing [THEN ssubst])
   128 apply (rule monofun_pair)
   129 apply (erule is_ub_thelub' [OF dir2dir_monofun [OF monofun_fst S] imageI])
   130 apply (erule is_ub_thelub' [OF dir2dir_monofun [OF monofun_snd S] imageI])
   131 apply (rule_tac t=u in surjective_pairing [THEN ssubst])
   132 apply (rule monofun_pair)
   133 apply (rule is_lub_thelub')
   134 apply (rule dir2dir_monofun [OF monofun_fst S])
   135 apply (erule ub2ub_monofun' [OF monofun_fst])
   136 apply (rule is_lub_thelub')
   137 apply (rule dir2dir_monofun [OF monofun_snd S])
   138 apply (erule ub2ub_monofun' [OF monofun_snd])
   139 done
   140 
   141 lemma thelub_cprod:
   142   "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
   143     \<Longrightarrow> lub (range S) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   144 by (rule lub_cprod [THEN thelubI])
   145 
   146 instance "*" :: (cpo, cpo) cpo
   147 proof
   148   fix S :: "nat \<Rightarrow> ('a \<times> 'b)"
   149   assume "chain S"
   150   hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   151     by (rule lub_cprod)
   152   thus "\<exists>x. range S <<| x" ..
   153 qed
   154 
   155 instance "*" :: (dcpo, dcpo) dcpo
   156 proof
   157   fix S :: "('a \<times> 'b) set"
   158   assume "directed S"
   159   hence "S <<| (\<Squnion>x\<in>S. fst x, \<Squnion>x\<in>S. snd x)"
   160     by (rule directed_lub_cprod)
   161   thus "\<exists>x. S <<| x" ..
   162 qed
   163 
   164 instance "*" :: (finite_po, finite_po) finite_po ..
   165 
   166 instance "*" :: (chfin, chfin) chfin
   167 proof (intro_classes, clarify)
   168   fix Y :: "nat \<Rightarrow> 'a \<times> 'b"
   169   assume Y: "chain Y"
   170   from Y have "chain (\<lambda>i. fst (Y i))"
   171     by (rule ch2ch_monofun [OF monofun_fst])
   172   hence "\<exists>m. max_in_chain m (\<lambda>i. fst (Y i))"
   173     by (rule chfin [rule_format])
   174   then obtain m where m: "max_in_chain m (\<lambda>i. fst (Y i))" ..
   175   from Y have "chain (\<lambda>i. snd (Y i))"
   176     by (rule ch2ch_monofun [OF monofun_snd])
   177   hence "\<exists>n. max_in_chain n (\<lambda>i. snd (Y i))"
   178     by (rule chfin [rule_format])
   179   then obtain n where n: "max_in_chain n (\<lambda>i. snd (Y i))" ..
   180   from m have m': "max_in_chain (max m n) (\<lambda>i. fst (Y i))"
   181     by (rule maxinch_mono [OF _ le_maxI1])
   182   from n have n': "max_in_chain (max m n) (\<lambda>i. snd (Y i))"
   183     by (rule maxinch_mono [OF _ le_maxI2])
   184   from m' n' have "max_in_chain (max m n) Y"
   185     unfolding max_in_chain_def Pair_fst_snd_eq by fast
   186   thus "\<exists>n. max_in_chain n Y" ..
   187 qed
   188 
   189 subsection {* Product type is pointed *}
   190 
   191 lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
   192 by (simp add: less_cprod_def)
   193 
   194 lemma least_cprod: "EX x::'a::pcpo * 'b::pcpo. ALL y. x \<sqsubseteq> y"
   195 apply (rule_tac x = "(\<bottom>, \<bottom>)" in exI)
   196 apply (rule minimal_cprod [THEN allI])
   197 done
   198 
   199 instance "*" :: (pcpo, pcpo) pcpo
   200 by intro_classes (rule least_cprod)
   201 
   202 text {* for compatibility with old HOLCF-Version *}
   203 lemma inst_cprod_pcpo: "UU = (UU,UU)"
   204 by (rule minimal_cprod [THEN UU_I, symmetric])
   205 
   206 
   207 subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
   208 
   209 lemma contlub_pair1: "contlub (\<lambda>x. (x, y))"
   210 apply (rule contlubI)
   211 apply (subst thelub_cprod)
   212 apply (erule monofun_pair1 [THEN ch2ch_monofun])
   213 apply simp
   214 done
   215 
   216 lemma contlub_pair2: "contlub (\<lambda>y. (x, y))"
   217 apply (rule contlubI)
   218 apply (subst thelub_cprod)
   219 apply (erule monofun_pair2 [THEN ch2ch_monofun])
   220 apply simp
   221 done
   222 
   223 lemma cont_pair1: "cont (\<lambda>x. (x, y))"
   224 apply (rule monocontlub2cont)
   225 apply (rule monofun_pair1)
   226 apply (rule contlub_pair1)
   227 done
   228 
   229 lemma cont_pair2: "cont (\<lambda>y. (x, y))"
   230 apply (rule monocontlub2cont)
   231 apply (rule monofun_pair2)
   232 apply (rule contlub_pair2)
   233 done
   234 
   235 lemma contlub_fst: "contlub fst"
   236 apply (rule contlubI)
   237 apply (simp add: thelub_cprod)
   238 done
   239 
   240 lemma contlub_snd: "contlub snd"
   241 apply (rule contlubI)
   242 apply (simp add: thelub_cprod)
   243 done
   244 
   245 lemma cont_fst: "cont fst"
   246 apply (rule monocontlub2cont)
   247 apply (rule monofun_fst)
   248 apply (rule contlub_fst)
   249 done
   250 
   251 lemma cont_snd: "cont snd"
   252 apply (rule monocontlub2cont)
   253 apply (rule monofun_snd)
   254 apply (rule contlub_snd)
   255 done
   256 
   257 subsection {* Continuous versions of constants *}
   258 
   259 definition
   260   cpair :: "'a \<rightarrow> 'b \<rightarrow> ('a * 'b)"  -- {* continuous pairing *}  where
   261   "cpair = (\<Lambda> x y. (x, y))"
   262 
   263 definition
   264   cfst :: "('a * 'b) \<rightarrow> 'a" where
   265   "cfst = (\<Lambda> p. fst p)"
   266 
   267 definition
   268   csnd :: "('a * 'b) \<rightarrow> 'b" where
   269   "csnd = (\<Lambda> p. snd p)"      
   270 
   271 definition
   272   csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c" where
   273   "csplit = (\<Lambda> f p. f\<cdot>(cfst\<cdot>p)\<cdot>(csnd\<cdot>p))"
   274 
   275 syntax
   276   "_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(1<_,/ _>)")
   277 
   278 syntax (xsymbols)
   279   "_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(1\<langle>_,/ _\<rangle>)")
   280 
   281 translations
   282   "\<langle>x, y, z\<rangle>" == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
   283   "\<langle>x, y\<rangle>"    == "CONST cpair\<cdot>x\<cdot>y"
   284 
   285 translations
   286   "\<Lambda>(CONST cpair\<cdot>x\<cdot>y). t" == "CONST csplit\<cdot>(\<Lambda> x y. t)"
   287 
   288 
   289 subsection {* Convert all lemmas to the continuous versions *}
   290 
   291 lemma cpair_eq_pair: "<x, y> = (x, y)"
   292 by (simp add: cpair_def cont_pair1 cont_pair2)
   293 
   294 lemma inject_cpair: "<a,b> = <aa,ba> \<Longrightarrow> a = aa \<and> b = ba"
   295 by (simp add: cpair_eq_pair)
   296 
   297 lemma cpair_eq [iff]: "(<a, b> = <a', b'>) = (a = a' \<and> b = b')"
   298 by (simp add: cpair_eq_pair)
   299 
   300 lemma cpair_less [iff]: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')"
   301 by (simp add: cpair_eq_pair less_cprod_def)
   302 
   303 lemma cpair_defined_iff [iff]: "(<x, y> = \<bottom>) = (x = \<bottom> \<and> y = \<bottom>)"
   304 by (simp add: inst_cprod_pcpo cpair_eq_pair)
   305 
   306 lemma cpair_strict: "<\<bottom>, \<bottom>> = \<bottom>"
   307 by simp
   308 
   309 lemma inst_cprod_pcpo2: "\<bottom> = <\<bottom>, \<bottom>>"
   310 by (rule cpair_strict [symmetric])
   311 
   312 lemma defined_cpair_rev: 
   313  "<a,b> = \<bottom> \<Longrightarrow> a = \<bottom> \<and> b = \<bottom>"
   314 by simp
   315 
   316 lemma Exh_Cprod2: "\<exists>a b. z = <a, b>"
   317 by (simp add: cpair_eq_pair)
   318 
   319 lemma cprodE: "\<lbrakk>\<And>x y. p = <x, y> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
   320 by (cut_tac Exh_Cprod2, auto)
   321 
   322 lemma cfst_cpair [simp]: "cfst\<cdot><x, y> = x"
   323 by (simp add: cpair_eq_pair cfst_def cont_fst)
   324 
   325 lemma csnd_cpair [simp]: "csnd\<cdot><x, y> = y"
   326 by (simp add: cpair_eq_pair csnd_def cont_snd)
   327 
   328 lemma cfst_strict [simp]: "cfst\<cdot>\<bottom> = \<bottom>"
   329 by (simp add: inst_cprod_pcpo2)
   330 
   331 lemma csnd_strict [simp]: "csnd\<cdot>\<bottom> = \<bottom>"
   332 by (simp add: inst_cprod_pcpo2)
   333 
   334 lemma surjective_pairing_Cprod2: "<cfst\<cdot>p, csnd\<cdot>p> = p"
   335 apply (unfold cfst_def csnd_def)
   336 apply (simp add: cont_fst cont_snd cpair_eq_pair)
   337 done
   338 
   339 lemma less_cprod: "x \<sqsubseteq> y = (cfst\<cdot>x \<sqsubseteq> cfst\<cdot>y \<and> csnd\<cdot>x \<sqsubseteq> csnd\<cdot>y)"
   340 by (simp add: less_cprod_def cfst_def csnd_def cont_fst cont_snd)
   341 
   342 lemma eq_cprod: "(x = y) = (cfst\<cdot>x = cfst\<cdot>y \<and> csnd\<cdot>x = csnd\<cdot>y)"
   343 by (auto simp add: po_eq_conv less_cprod)
   344 
   345 lemma cfst_less_iff: "cfst\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> <y, csnd\<cdot>x>"
   346 by (simp add: less_cprod)
   347 
   348 lemma csnd_less_iff: "csnd\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> <cfst\<cdot>x, y>"
   349 by (simp add: less_cprod)
   350 
   351 lemma compact_cfst: "compact x \<Longrightarrow> compact (cfst\<cdot>x)"
   352 by (rule compactI, simp add: cfst_less_iff)
   353 
   354 lemma compact_csnd: "compact x \<Longrightarrow> compact (csnd\<cdot>x)"
   355 by (rule compactI, simp add: csnd_less_iff)
   356 
   357 lemma compact_cpair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact <x, y>"
   358 by (rule compactI, simp add: less_cprod)
   359 
   360 lemma compact_cpair_iff [simp]: "compact <x, y> = (compact x \<and> compact y)"
   361 apply (safe intro!: compact_cpair)
   362 apply (drule compact_cfst, simp)
   363 apply (drule compact_csnd, simp)
   364 done
   365 
   366 lemma lub_cprod2: 
   367   "chain S \<Longrightarrow> range S <<| <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
   368 apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd)
   369 apply (erule lub_cprod)
   370 done
   371 
   372 lemma thelub_cprod2:
   373   "chain S \<Longrightarrow> lub (range S) = <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
   374 by (rule lub_cprod2 [THEN thelubI])
   375 
   376 lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>"
   377 by (simp add: csplit_def)
   378 
   379 lemma csplit2 [simp]: "csplit\<cdot>f\<cdot><x,y> = f\<cdot>x\<cdot>y"
   380 by (simp add: csplit_def)
   381 
   382 lemma csplit3 [simp]: "csplit\<cdot>cpair\<cdot>z = z"
   383 by (simp add: csplit_def surjective_pairing_Cprod2)
   384 
   385 lemmas Cprod_rews = cfst_cpair csnd_cpair csplit2
   386 
   387 end