src/HOLCF/Cprod.thy
author huffman
Mon Jan 14 20:45:10 2008 +0100 (2008-01-14)
changeset 25908 d8ce142f7e6e
parent 25907 695a9d88d697
child 25910 25533eb2b914
permissions -rw-r--r--
cleaned up instance proofs
     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 :: po
    19 begin
    20 
    21 definition
    22   less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True"
    23 
    24 instance
    25 by intro_classes simp_all
    26 
    27 end
    28 
    29 instance unit :: finite_po ..
    30 
    31 instance unit :: pcpo
    32 by intro_classes simp
    33 
    34 definition
    35   unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a" where
    36   "unit_when = (\<Lambda> a _. a)"
    37 
    38 translations
    39   "\<Lambda>(). t" == "CONST unit_when\<cdot>t"
    40 
    41 lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a"
    42 by (simp add: unit_when_def)
    43 
    44 
    45 subsection {* Product type is a partial order *}
    46 
    47 instantiation "*" :: (po, po) po
    48 begin
    49 
    50 definition
    51   less_cprod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
    52 
    53 instance
    54 proof
    55   fix x :: "'a \<times> 'b"
    56   show "x \<sqsubseteq> x"
    57     unfolding less_cprod_def by simp
    58 next
    59   fix x y :: "'a \<times> 'b"
    60   assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
    61     unfolding less_cprod_def Pair_fst_snd_eq
    62     by (fast intro: antisym_less)
    63 next
    64   fix x y z :: "'a \<times> 'b"
    65   assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
    66     unfolding less_cprod_def
    67     by (fast intro: trans_less)
    68 qed
    69 
    70 end
    71 
    72 subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
    73 
    74 text {* Pair @{text "(_,_)"}  is monotone in both arguments *}
    75 
    76 lemma monofun_pair1: "monofun (\<lambda>x. (x, y))"
    77 by (simp add: monofun_def less_cprod_def)
    78 
    79 lemma monofun_pair2: "monofun (\<lambda>y. (x, y))"
    80 by (simp add: monofun_def less_cprod_def)
    81 
    82 lemma monofun_pair:
    83   "\<lbrakk>x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2\<rbrakk> \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)"
    84 by (simp add: less_cprod_def)
    85 
    86 text {* @{term fst} and @{term snd} are monotone *}
    87 
    88 lemma monofun_fst: "monofun fst"
    89 by (simp add: monofun_def less_cprod_def)
    90 
    91 lemma monofun_snd: "monofun snd"
    92 by (simp add: monofun_def less_cprod_def)
    93 
    94 subsection {* Product type is a cpo *}
    95 
    96 lemma lub_cprod:
    97   fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)"
    98   assumes S: "chain S"
    99   shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   100 apply (rule is_lubI)
   101 apply (rule ub_rangeI)
   102 apply (rule_tac t = "S i" in surjective_pairing [THEN ssubst])
   103 apply (rule monofun_pair)
   104 apply (rule is_ub_thelub)
   105 apply (rule ch2ch_monofun [OF monofun_fst S])
   106 apply (rule is_ub_thelub)
   107 apply (rule ch2ch_monofun [OF monofun_snd S])
   108 apply (rule_tac t = "u" in surjective_pairing [THEN ssubst])
   109 apply (rule monofun_pair)
   110 apply (rule is_lub_thelub)
   111 apply (rule ch2ch_monofun [OF monofun_fst S])
   112 apply (erule monofun_fst [THEN ub2ub_monofun])
   113 apply (rule is_lub_thelub)
   114 apply (rule ch2ch_monofun [OF monofun_snd S])
   115 apply (erule monofun_snd [THEN ub2ub_monofun])
   116 done
   117 
   118 lemma thelub_cprod:
   119   "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
   120     \<Longrightarrow> lub (range S) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   121 by (rule lub_cprod [THEN thelubI])
   122 
   123 instance "*" :: (cpo, cpo) cpo
   124 proof
   125   fix S :: "nat \<Rightarrow> ('a \<times> 'b)"
   126   assume "chain S"
   127   hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   128     by (rule lub_cprod)
   129   thus "\<exists>x. range S <<| x" ..
   130 qed
   131 
   132 instance "*" :: (finite_po, finite_po) finite_po ..
   133 
   134 subsection {* Product type is pointed *}
   135 
   136 lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
   137 by (simp add: less_cprod_def)
   138 
   139 instance "*" :: (pcpo, pcpo) pcpo
   140 by intro_classes (fast intro: minimal_cprod)
   141 
   142 lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
   143 by (rule minimal_cprod [THEN UU_I, symmetric])
   144 
   145 
   146 subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
   147 
   148 lemma contlub_pair1: "contlub (\<lambda>x. (x, y))"
   149 apply (rule contlubI)
   150 apply (subst thelub_cprod)
   151 apply (erule monofun_pair1 [THEN ch2ch_monofun])
   152 apply simp
   153 done
   154 
   155 lemma contlub_pair2: "contlub (\<lambda>y. (x, y))"
   156 apply (rule contlubI)
   157 apply (subst thelub_cprod)
   158 apply (erule monofun_pair2 [THEN ch2ch_monofun])
   159 apply simp
   160 done
   161 
   162 lemma cont_pair1: "cont (\<lambda>x. (x, y))"
   163 apply (rule monocontlub2cont)
   164 apply (rule monofun_pair1)
   165 apply (rule contlub_pair1)
   166 done
   167 
   168 lemma cont_pair2: "cont (\<lambda>y. (x, y))"
   169 apply (rule monocontlub2cont)
   170 apply (rule monofun_pair2)
   171 apply (rule contlub_pair2)
   172 done
   173 
   174 lemma contlub_fst: "contlub fst"
   175 apply (rule contlubI)
   176 apply (simp add: thelub_cprod)
   177 done
   178 
   179 lemma contlub_snd: "contlub snd"
   180 apply (rule contlubI)
   181 apply (simp add: thelub_cprod)
   182 done
   183 
   184 lemma cont_fst: "cont fst"
   185 apply (rule monocontlub2cont)
   186 apply (rule monofun_fst)
   187 apply (rule contlub_fst)
   188 done
   189 
   190 lemma cont_snd: "cont snd"
   191 apply (rule monocontlub2cont)
   192 apply (rule monofun_snd)
   193 apply (rule contlub_snd)
   194 done
   195 
   196 subsection {* Continuous versions of constants *}
   197 
   198 definition
   199   cpair :: "'a \<rightarrow> 'b \<rightarrow> ('a * 'b)"  -- {* continuous pairing *}  where
   200   "cpair = (\<Lambda> x y. (x, y))"
   201 
   202 definition
   203   cfst :: "('a * 'b) \<rightarrow> 'a" where
   204   "cfst = (\<Lambda> p. fst p)"
   205 
   206 definition
   207   csnd :: "('a * 'b) \<rightarrow> 'b" where
   208   "csnd = (\<Lambda> p. snd p)"      
   209 
   210 definition
   211   csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c" where
   212   "csplit = (\<Lambda> f p. f\<cdot>(cfst\<cdot>p)\<cdot>(csnd\<cdot>p))"
   213 
   214 syntax
   215   "_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(1<_,/ _>)")
   216 
   217 syntax (xsymbols)
   218   "_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(1\<langle>_,/ _\<rangle>)")
   219 
   220 translations
   221   "\<langle>x, y, z\<rangle>" == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
   222   "\<langle>x, y\<rangle>"    == "CONST cpair\<cdot>x\<cdot>y"
   223 
   224 translations
   225   "\<Lambda>(CONST cpair\<cdot>x\<cdot>y). t" == "CONST csplit\<cdot>(\<Lambda> x y. t)"
   226 
   227 
   228 subsection {* Convert all lemmas to the continuous versions *}
   229 
   230 lemma cpair_eq_pair: "<x, y> = (x, y)"
   231 by (simp add: cpair_def cont_pair1 cont_pair2)
   232 
   233 lemma inject_cpair: "<a,b> = <aa,ba> \<Longrightarrow> a = aa \<and> b = ba"
   234 by (simp add: cpair_eq_pair)
   235 
   236 lemma cpair_eq [iff]: "(<a, b> = <a', b'>) = (a = a' \<and> b = b')"
   237 by (simp add: cpair_eq_pair)
   238 
   239 lemma cpair_less [iff]: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')"
   240 by (simp add: cpair_eq_pair less_cprod_def)
   241 
   242 lemma cpair_defined_iff [iff]: "(<x, y> = \<bottom>) = (x = \<bottom> \<and> y = \<bottom>)"
   243 by (simp add: inst_cprod_pcpo cpair_eq_pair)
   244 
   245 lemma cpair_strict: "<\<bottom>, \<bottom>> = \<bottom>"
   246 by simp
   247 
   248 lemma inst_cprod_pcpo2: "\<bottom> = <\<bottom>, \<bottom>>"
   249 by (rule cpair_strict [symmetric])
   250 
   251 lemma defined_cpair_rev: 
   252  "<a,b> = \<bottom> \<Longrightarrow> a = \<bottom> \<and> b = \<bottom>"
   253 by simp
   254 
   255 lemma Exh_Cprod2: "\<exists>a b. z = <a, b>"
   256 by (simp add: cpair_eq_pair)
   257 
   258 lemma cprodE: "\<lbrakk>\<And>x y. p = <x, y> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
   259 by (cut_tac Exh_Cprod2, auto)
   260 
   261 lemma cfst_cpair [simp]: "cfst\<cdot><x, y> = x"
   262 by (simp add: cpair_eq_pair cfst_def cont_fst)
   263 
   264 lemma csnd_cpair [simp]: "csnd\<cdot><x, y> = y"
   265 by (simp add: cpair_eq_pair csnd_def cont_snd)
   266 
   267 lemma cfst_strict [simp]: "cfst\<cdot>\<bottom> = \<bottom>"
   268 by (simp add: inst_cprod_pcpo2)
   269 
   270 lemma csnd_strict [simp]: "csnd\<cdot>\<bottom> = \<bottom>"
   271 by (simp add: inst_cprod_pcpo2)
   272 
   273 lemma surjective_pairing_Cprod2: "<cfst\<cdot>p, csnd\<cdot>p> = p"
   274 apply (unfold cfst_def csnd_def)
   275 apply (simp add: cont_fst cont_snd cpair_eq_pair)
   276 done
   277 
   278 lemma less_cprod: "x \<sqsubseteq> y = (cfst\<cdot>x \<sqsubseteq> cfst\<cdot>y \<and> csnd\<cdot>x \<sqsubseteq> csnd\<cdot>y)"
   279 by (simp add: less_cprod_def cfst_def csnd_def cont_fst cont_snd)
   280 
   281 lemma eq_cprod: "(x = y) = (cfst\<cdot>x = cfst\<cdot>y \<and> csnd\<cdot>x = csnd\<cdot>y)"
   282 by (auto simp add: po_eq_conv less_cprod)
   283 
   284 lemma cfst_less_iff: "cfst\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> <y, csnd\<cdot>x>"
   285 by (simp add: less_cprod)
   286 
   287 lemma csnd_less_iff: "csnd\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> <cfst\<cdot>x, y>"
   288 by (simp add: less_cprod)
   289 
   290 lemma compact_cfst: "compact x \<Longrightarrow> compact (cfst\<cdot>x)"
   291 by (rule compactI, simp add: cfst_less_iff)
   292 
   293 lemma compact_csnd: "compact x \<Longrightarrow> compact (csnd\<cdot>x)"
   294 by (rule compactI, simp add: csnd_less_iff)
   295 
   296 lemma compact_cpair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact <x, y>"
   297 by (rule compactI, simp add: less_cprod)
   298 
   299 lemma compact_cpair_iff [simp]: "compact <x, y> = (compact x \<and> compact y)"
   300 apply (safe intro!: compact_cpair)
   301 apply (drule compact_cfst, simp)
   302 apply (drule compact_csnd, simp)
   303 done
   304 
   305 instance "*" :: (chfin, chfin) chfin
   306 apply (intro_classes, clarify)
   307 apply (erule compact_imp_max_in_chain)
   308 apply (rule_tac p="\<Squnion>i. Y i" in cprodE, simp)
   309 done
   310 
   311 lemma lub_cprod2: 
   312   "chain S \<Longrightarrow> range S <<| <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
   313 apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd)
   314 apply (erule lub_cprod)
   315 done
   316 
   317 lemma thelub_cprod2:
   318   "chain S \<Longrightarrow> lub (range S) = <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
   319 by (rule lub_cprod2 [THEN thelubI])
   320 
   321 lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>"
   322 by (simp add: csplit_def)
   323 
   324 lemma csplit2 [simp]: "csplit\<cdot>f\<cdot><x,y> = f\<cdot>x\<cdot>y"
   325 by (simp add: csplit_def)
   326 
   327 lemma csplit3 [simp]: "csplit\<cdot>cpair\<cdot>z = z"
   328 by (simp add: csplit_def surjective_pairing_Cprod2)
   329 
   330 lemmas Cprod_rews = cfst_cpair csnd_cpair csplit2
   331 
   332 end