src/HOLCF/Cprod.thy
author huffman
Thu Jan 03 22:10:52 2008 +0100 (2008-01-03)
changeset 25815 c7b1e7b7087b
parent 25784 71157f7e671e
child 25827 c2adeb1bae5c
permissions -rw-r--r--
instance unit :: finite_po
     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 subsection {* Product type is pointed *}
   165 
   166 lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
   167 by (simp add: less_cprod_def)
   168 
   169 lemma least_cprod: "EX x::'a::pcpo * 'b::pcpo. ALL y. x \<sqsubseteq> y"
   170 apply (rule_tac x = "(\<bottom>, \<bottom>)" in exI)
   171 apply (rule minimal_cprod [THEN allI])
   172 done
   173 
   174 instance "*" :: (pcpo, pcpo) pcpo
   175 by intro_classes (rule least_cprod)
   176 
   177 text {* for compatibility with old HOLCF-Version *}
   178 lemma inst_cprod_pcpo: "UU = (UU,UU)"
   179 by (rule minimal_cprod [THEN UU_I, symmetric])
   180 
   181 
   182 subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
   183 
   184 lemma contlub_pair1: "contlub (\<lambda>x. (x, y))"
   185 apply (rule contlubI)
   186 apply (subst thelub_cprod)
   187 apply (erule monofun_pair1 [THEN ch2ch_monofun])
   188 apply simp
   189 done
   190 
   191 lemma contlub_pair2: "contlub (\<lambda>y. (x, y))"
   192 apply (rule contlubI)
   193 apply (subst thelub_cprod)
   194 apply (erule monofun_pair2 [THEN ch2ch_monofun])
   195 apply simp
   196 done
   197 
   198 lemma cont_pair1: "cont (\<lambda>x. (x, y))"
   199 apply (rule monocontlub2cont)
   200 apply (rule monofun_pair1)
   201 apply (rule contlub_pair1)
   202 done
   203 
   204 lemma cont_pair2: "cont (\<lambda>y. (x, y))"
   205 apply (rule monocontlub2cont)
   206 apply (rule monofun_pair2)
   207 apply (rule contlub_pair2)
   208 done
   209 
   210 lemma contlub_fst: "contlub fst"
   211 apply (rule contlubI)
   212 apply (simp add: thelub_cprod)
   213 done
   214 
   215 lemma contlub_snd: "contlub snd"
   216 apply (rule contlubI)
   217 apply (simp add: thelub_cprod)
   218 done
   219 
   220 lemma cont_fst: "cont fst"
   221 apply (rule monocontlub2cont)
   222 apply (rule monofun_fst)
   223 apply (rule contlub_fst)
   224 done
   225 
   226 lemma cont_snd: "cont snd"
   227 apply (rule monocontlub2cont)
   228 apply (rule monofun_snd)
   229 apply (rule contlub_snd)
   230 done
   231 
   232 subsection {* Continuous versions of constants *}
   233 
   234 definition
   235   cpair :: "'a \<rightarrow> 'b \<rightarrow> ('a * 'b)"  -- {* continuous pairing *}  where
   236   "cpair = (\<Lambda> x y. (x, y))"
   237 
   238 definition
   239   cfst :: "('a * 'b) \<rightarrow> 'a" where
   240   "cfst = (\<Lambda> p. fst p)"
   241 
   242 definition
   243   csnd :: "('a * 'b) \<rightarrow> 'b" where
   244   "csnd = (\<Lambda> p. snd p)"      
   245 
   246 definition
   247   csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c" where
   248   "csplit = (\<Lambda> f p. f\<cdot>(cfst\<cdot>p)\<cdot>(csnd\<cdot>p))"
   249 
   250 syntax
   251   "_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(1<_,/ _>)")
   252 
   253 syntax (xsymbols)
   254   "_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(1\<langle>_,/ _\<rangle>)")
   255 
   256 translations
   257   "\<langle>x, y, z\<rangle>" == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
   258   "\<langle>x, y\<rangle>"    == "CONST cpair\<cdot>x\<cdot>y"
   259 
   260 translations
   261   "\<Lambda>(CONST cpair\<cdot>x\<cdot>y). t" == "CONST csplit\<cdot>(\<Lambda> x y. t)"
   262 
   263 
   264 subsection {* Convert all lemmas to the continuous versions *}
   265 
   266 lemma cpair_eq_pair: "<x, y> = (x, y)"
   267 by (simp add: cpair_def cont_pair1 cont_pair2)
   268 
   269 lemma inject_cpair: "<a,b> = <aa,ba> \<Longrightarrow> a = aa \<and> b = ba"
   270 by (simp add: cpair_eq_pair)
   271 
   272 lemma cpair_eq [iff]: "(<a, b> = <a', b'>) = (a = a' \<and> b = b')"
   273 by (simp add: cpair_eq_pair)
   274 
   275 lemma cpair_less [iff]: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')"
   276 by (simp add: cpair_eq_pair less_cprod_def)
   277 
   278 lemma cpair_defined_iff [iff]: "(<x, y> = \<bottom>) = (x = \<bottom> \<and> y = \<bottom>)"
   279 by (simp add: inst_cprod_pcpo cpair_eq_pair)
   280 
   281 lemma cpair_strict: "<\<bottom>, \<bottom>> = \<bottom>"
   282 by simp
   283 
   284 lemma inst_cprod_pcpo2: "\<bottom> = <\<bottom>, \<bottom>>"
   285 by (rule cpair_strict [symmetric])
   286 
   287 lemma defined_cpair_rev: 
   288  "<a,b> = \<bottom> \<Longrightarrow> a = \<bottom> \<and> b = \<bottom>"
   289 by simp
   290 
   291 lemma Exh_Cprod2: "\<exists>a b. z = <a, b>"
   292 by (simp add: cpair_eq_pair)
   293 
   294 lemma cprodE: "\<lbrakk>\<And>x y. p = <x, y> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
   295 by (cut_tac Exh_Cprod2, auto)
   296 
   297 lemma cfst_cpair [simp]: "cfst\<cdot><x, y> = x"
   298 by (simp add: cpair_eq_pair cfst_def cont_fst)
   299 
   300 lemma csnd_cpair [simp]: "csnd\<cdot><x, y> = y"
   301 by (simp add: cpair_eq_pair csnd_def cont_snd)
   302 
   303 lemma cfst_strict [simp]: "cfst\<cdot>\<bottom> = \<bottom>"
   304 by (simp add: inst_cprod_pcpo2)
   305 
   306 lemma csnd_strict [simp]: "csnd\<cdot>\<bottom> = \<bottom>"
   307 by (simp add: inst_cprod_pcpo2)
   308 
   309 lemma surjective_pairing_Cprod2: "<cfst\<cdot>p, csnd\<cdot>p> = p"
   310 apply (unfold cfst_def csnd_def)
   311 apply (simp add: cont_fst cont_snd cpair_eq_pair)
   312 done
   313 
   314 lemma less_cprod: "x \<sqsubseteq> y = (cfst\<cdot>x \<sqsubseteq> cfst\<cdot>y \<and> csnd\<cdot>x \<sqsubseteq> csnd\<cdot>y)"
   315 by (simp add: less_cprod_def cfst_def csnd_def cont_fst cont_snd)
   316 
   317 lemma eq_cprod: "(x = y) = (cfst\<cdot>x = cfst\<cdot>y \<and> csnd\<cdot>x = csnd\<cdot>y)"
   318 by (auto simp add: po_eq_conv less_cprod)
   319 
   320 lemma compact_cpair [simp]: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact <x, y>"
   321 by (rule compactI, simp add: less_cprod)
   322 
   323 lemma lub_cprod2: 
   324   "chain S \<Longrightarrow> range S <<| <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
   325 apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd)
   326 apply (erule lub_cprod)
   327 done
   328 
   329 lemma thelub_cprod2:
   330   "chain S \<Longrightarrow> lub (range S) = <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
   331 by (rule lub_cprod2 [THEN thelubI])
   332 
   333 lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>"
   334 by (simp add: csplit_def)
   335 
   336 lemma csplit2 [simp]: "csplit\<cdot>f\<cdot><x,y> = f\<cdot>x\<cdot>y"
   337 by (simp add: csplit_def)
   338 
   339 lemma csplit3 [simp]: "csplit\<cdot>cpair\<cdot>z = z"
   340 by (simp add: csplit_def surjective_pairing_Cprod2)
   341 
   342 lemmas Cprod_rews = cfst_cpair csnd_cpair csplit2
   343 
   344 end