src/HOLCF/Cprod.thy
author huffman
Tue Mar 08 00:32:10 2005 +0100 (2005-03-08)
changeset 15593 24d770bbc44a
parent 15577 e16da3068ad6
child 15600 a59f07556a8d
permissions -rw-r--r--
reordered and arranged for document generation, cleaned up some proofs
     1 (*  Title:      HOLCF/Cprod1.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Partial ordering for cartesian product of HOL theory prod.thy
     7 *)
     8 
     9 header {* The cpo of cartesian products *}
    10 
    11 theory Cprod
    12 imports Cfun
    13 begin
    14 
    15 defaultsort cpo
    16 
    17 subsection {* Ordering on @{typ "'a * 'b"} *}
    18 
    19 instance "*" :: (sq_ord, sq_ord) sq_ord ..
    20 
    21 defs (overloaded)
    22   less_cprod_def: "p1 << p2 == (fst p1<<fst p2 & snd p1 << snd p2)"
    23 
    24 subsection {* Type @{typ "'a * 'b"} is a partial order *}
    25 
    26 lemma refl_less_cprod: "(p::'a*'b) << p"
    27 apply (unfold less_cprod_def)
    28 apply simp
    29 done
    30 
    31 lemma antisym_less_cprod: "[|(p1::'a * 'b) << p2;p2 << p1|] ==> p1=p2"
    32 apply (unfold less_cprod_def)
    33 apply (rule injective_fst_snd)
    34 apply (fast intro: antisym_less)
    35 apply (fast intro: antisym_less)
    36 done
    37 
    38 lemma trans_less_cprod: 
    39         "[|(p1::'a*'b) << p2;p2 << p3|] ==> p1 << p3"
    40 apply (unfold less_cprod_def)
    41 apply (rule conjI)
    42 apply (fast intro: trans_less)
    43 apply (fast intro: trans_less)
    44 done
    45 
    46 defaultsort pcpo
    47 
    48 instance "*" :: (cpo, cpo) po
    49 by intro_classes
    50   (assumption | rule refl_less_cprod antisym_less_cprod trans_less_cprod)+
    51 
    52 text {* for compatibility with old HOLCF-Version *}
    53 lemma inst_cprod_po: "(op <<)=(%x y. fst x<<fst y & snd x<<snd y)"
    54 apply (fold less_cprod_def)
    55 apply (rule refl)
    56 done
    57 
    58 lemma less_cprod4c: "(x1,y1) << (x2,y2) ==> x1 << x2 & y1 << y2"
    59 apply (simp add: inst_cprod_po)
    60 done
    61 
    62 subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
    63 
    64 text {* Pair @{text "(_,_)"}  is monotone in both arguments *}
    65 
    66 lemma monofun_pair1: "monofun Pair"
    67 by (simp add: monofun less_fun inst_cprod_po)
    68 
    69 lemma monofun_pair2: "monofun(Pair x)"
    70 by (simp add: monofun inst_cprod_po)
    71 
    72 lemma monofun_pair: "[|x1<<x2; y1<<y2|] ==> (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)"
    73 by (simp add: inst_cprod_po)
    74 
    75 text {* @{term fst} and @{term snd} are monotone *}
    76 
    77 lemma monofun_fst: "monofun fst"
    78 by (simp add: monofun inst_cprod_po)
    79 
    80 lemma monofun_snd: "monofun snd"
    81 by (simp add: monofun inst_cprod_po)
    82 
    83 subsection {* Type @{typ "'a * 'b"} is a cpo *}
    84 
    85 lemma lub_cprod: 
    86 "chain S ==> range S<<|(lub(range(%i. fst(S i))),lub(range(%i. snd(S i))))"
    87 apply (rule is_lubI)
    88 apply (rule ub_rangeI)
    89 apply (rule_tac t = "S i" in surjective_pairing [THEN ssubst])
    90 apply (rule monofun_pair)
    91 apply (rule is_ub_thelub)
    92 apply (erule monofun_fst [THEN ch2ch_monofun])
    93 apply (rule is_ub_thelub)
    94 apply (erule monofun_snd [THEN ch2ch_monofun])
    95 apply (rule_tac t = "u" in surjective_pairing [THEN ssubst])
    96 apply (rule monofun_pair)
    97 apply (rule is_lub_thelub)
    98 apply (erule monofun_fst [THEN ch2ch_monofun])
    99 apply (erule monofun_fst [THEN ub2ub_monofun])
   100 apply (rule is_lub_thelub)
   101 apply (erule monofun_snd [THEN ch2ch_monofun])
   102 apply (erule monofun_snd [THEN ub2ub_monofun])
   103 done
   104 
   105 lemmas thelub_cprod = lub_cprod [THEN thelubI, standard]
   106 (*
   107 "chain ?S1 ==>
   108  lub (range ?S1) =
   109  (lub (range (%i. fst (?S1 i))), lub (range (%i. snd (?S1 i))))" : thm
   110 
   111 *)
   112 
   113 lemma cpo_cprod: "chain(S::nat=>'a::cpo*'b::cpo)==>EX x. range S<<| x"
   114 by (rule exI, erule lub_cprod)
   115 
   116 instance "*" :: (cpo,cpo)cpo
   117 by intro_classes (rule cpo_cprod)
   118 
   119 subsection {* Type @{typ "'a * 'b"} is pointed *}
   120 
   121 lemma minimal_cprod: "(UU,UU)<<p"
   122 by (simp add: inst_cprod_po)
   123 
   124 lemmas UU_cprod_def = minimal_cprod [THEN minimal2UU, symmetric, standard]
   125 
   126 lemma least_cprod: "EX x::'a*'b. ALL y. x<<y"
   127 apply (rule_tac x = " (UU,UU) " in exI)
   128 apply (rule minimal_cprod [THEN allI])
   129 done
   130 
   131 instance "*" :: (pcpo,pcpo)pcpo
   132 by intro_classes (rule least_cprod)
   133 
   134 text {* for compatibility with old HOLCF-Version *}
   135 lemma inst_cprod_pcpo: "UU = (UU,UU)"
   136 apply (simp add: UU_cprod_def[folded UU_def])
   137 done
   138 
   139 subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
   140 
   141 lemma contlub_pair1: "contlub(Pair)"
   142 apply (rule contlubI [rule_format])
   143 apply (rule ext)
   144 apply (subst lub_fun [THEN thelubI])
   145 apply (erule monofun_pair1 [THEN ch2ch_monofun])
   146 apply (subst thelub_cprod)
   147 apply (rule ch2ch_fun)
   148 apply (erule monofun_pair1 [THEN ch2ch_monofun])
   149 apply (simp add: lub_const [THEN thelubI])
   150 done
   151 
   152 lemma contlub_pair2: "contlub(Pair(x))"
   153 apply (rule contlubI [rule_format])
   154 apply (subst thelub_cprod)
   155 apply (erule monofun_pair2 [THEN ch2ch_monofun])
   156 apply (simp add: lub_const [THEN thelubI])
   157 done
   158 
   159 lemma cont_pair1: "cont(Pair)"
   160 apply (rule monocontlub2cont)
   161 apply (rule monofun_pair1)
   162 apply (rule contlub_pair1)
   163 done
   164 
   165 lemma cont_pair2: "cont(Pair(x))"
   166 apply (rule monocontlub2cont)
   167 apply (rule monofun_pair2)
   168 apply (rule contlub_pair2)
   169 done
   170 
   171 lemma contlub_fst: "contlub(fst)"
   172 apply (rule contlubI [rule_format])
   173 apply (simp add: lub_cprod [THEN thelubI])
   174 done
   175 
   176 lemma contlub_snd: "contlub(snd)"
   177 apply (rule contlubI [rule_format])
   178 apply (simp add: lub_cprod [THEN thelubI])
   179 done
   180 
   181 lemma cont_fst: "cont(fst)"
   182 apply (rule monocontlub2cont)
   183 apply (rule monofun_fst)
   184 apply (rule contlub_fst)
   185 done
   186 
   187 lemma cont_snd: "cont(snd)"
   188 apply (rule monocontlub2cont)
   189 apply (rule monofun_snd)
   190 apply (rule contlub_snd)
   191 done
   192 
   193 subsection {* Continuous versions of constants *}
   194 
   195 consts
   196         cpair        :: "'a::cpo -> 'b::cpo -> ('a*'b)" (* continuous pairing *)
   197         cfst         :: "('a::cpo*'b::cpo)->'a"
   198         csnd         :: "('a::cpo*'b::cpo)->'b"
   199         csplit       :: "('a::cpo->'b::cpo->'c::cpo)->('a*'b)->'c"
   200 
   201 syntax
   202         "@ctuple"    :: "['a, args] => 'a * 'b"         ("(1<_,/ _>)")
   203 
   204 translations
   205         "<x, y, z>"   == "<x, <y, z>>"
   206         "<x, y>"      == "cpair$x$y"
   207 
   208 defs
   209 cpair_def:       "cpair  == (LAM x y.(x,y))"
   210 cfst_def:        "cfst   == (LAM p. fst(p))"
   211 csnd_def:        "csnd   == (LAM p. snd(p))"      
   212 csplit_def:      "csplit == (LAM f p. f$(cfst$p)$(csnd$p))"
   213 
   214 
   215 
   216 (* introduce syntax for
   217 
   218    Let <x,y> = e1; z = E2 in E3
   219 
   220    and
   221 
   222    LAM <x,y,z>.e
   223 *)
   224 
   225 constdefs
   226   CLet           :: "'a -> ('a -> 'b) -> 'b"
   227   "CLet == LAM s f. f$s"
   228 
   229 
   230 (* syntax for Let *)
   231 
   232 nonterminals
   233   Cletbinds  Cletbind
   234 
   235 syntax
   236   "_Cbind"  :: "[pttrn, 'a] => Cletbind"             ("(2_ =/ _)" 10)
   237   ""        :: "Cletbind => Cletbinds"               ("_")
   238   "_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds"  ("_;/ _")
   239   "_CLet"   :: "[Cletbinds, 'a] => 'a"               ("(Let (_)/ in (_))" 10)
   240 
   241 translations
   242   "_CLet (_Cbinds b bs) e"  == "_CLet b (_CLet bs e)"
   243   "Let x = a in e"          == "CLet$a$(LAM x. e)"
   244 
   245 
   246 (* syntax for LAM <x,y,z>.e *)
   247 
   248 syntax
   249   "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3LAM <_>./ _)" [0, 10] 10)
   250 
   251 translations
   252   "LAM <x,y,zs>.b"        == "csplit$(LAM x. LAM <y,zs>.b)"
   253   "LAM <x,y>. LAM zs. b"  <= "csplit$(LAM x y zs. b)"
   254   "LAM <x,y>.b"           == "csplit$(LAM x y. b)"
   255 
   256 syntax (xsymbols)
   257   "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\<Lambda>()<_>./ _)" [0, 10] 10)
   258 
   259 subsection {* Convert all lemmas to the continuous versions *}
   260 
   261 lemma beta_cfun_cprod: 
   262         "(LAM x y.(x,y))$a$b = (a,b)"
   263 apply (subst beta_cfun)
   264 apply (simp add: cont_pair1 cont_pair2 cont2cont_CF1L)
   265 apply (subst beta_cfun)
   266 apply (rule cont_pair2)
   267 apply (rule refl)
   268 done
   269 
   270 lemma inject_cpair: 
   271         "<a,b> = <aa,ba>  ==> a=aa & b=ba"
   272 by (simp add: cpair_def beta_cfun_cprod)
   273 
   274 lemma inst_cprod_pcpo2: "UU = <UU,UU>"
   275 by (simp add: cpair_def beta_cfun_cprod inst_cprod_pcpo)
   276 
   277 lemma defined_cpair_rev: 
   278  "<a,b> = UU ==> a = UU & b = UU"
   279 apply (drule inst_cprod_pcpo2 [THEN subst])
   280 apply (erule inject_cpair)
   281 done
   282 
   283 lemma Exh_Cprod2: "? a b. z=<a,b>"
   284 apply (unfold cpair_def)
   285 apply (rule PairE)
   286 apply (rule exI)
   287 apply (rule exI)
   288 apply (erule beta_cfun_cprod [THEN ssubst])
   289 done
   290 
   291 lemma cprodE:
   292 assumes prems: "!!x y. [| p = <x,y> |] ==> Q"
   293 shows "Q"
   294 apply (rule PairE)
   295 apply (rule prems)
   296 apply (simp add: cpair_def beta_cfun_cprod)
   297 done
   298 
   299 lemma cfst2 [simp]: "cfst$<x,y> = x"
   300 by (simp add: cpair_def cfst_def beta_cfun_cprod cont_fst)
   301 
   302 lemma csnd2 [simp]: "csnd$<x,y> = y"
   303 by (simp add: cpair_def csnd_def beta_cfun_cprod cont_snd)
   304 
   305 lemma cfst_strict: "cfst$UU = UU"
   306 by (simp add: inst_cprod_pcpo2)
   307 
   308 lemma csnd_strict: "csnd$UU = UU"
   309 by (simp add: inst_cprod_pcpo2)
   310 
   311 lemma surjective_pairing_Cprod2: "<cfst$p, csnd$p> = p"
   312 apply (unfold cfst_def csnd_def cpair_def)
   313 apply (simp add: cont_fst cont_snd beta_cfun_cprod)
   314 done
   315 
   316 lemma less_cprod5c: 
   317  "<xa,ya> << <x,y> ==> xa<<x & ya << y"
   318 by (simp add: cpair_def beta_cfun_cprod inst_cprod_po)
   319 
   320 lemma lub_cprod2: 
   321 "[|chain(S)|] ==> range(S) <<|  
   322   <(lub(range(%i. cfst$(S i)))) , lub(range(%i. csnd$(S i)))>"
   323 apply (simp add: cpair_def beta_cfun_cprod)
   324 apply (simp add: cfst_def csnd_def cont_fst cont_snd)
   325 apply (erule lub_cprod)
   326 done
   327 
   328 lemmas thelub_cprod2 = lub_cprod2 [THEN thelubI, standard]
   329 (*
   330 chain ?S1 ==>
   331  lub (range ?S1) =
   332  <lub (range (%i. cfst$(?S1 i))), lub (range (%i. csnd$(?S1 i)))>" 
   333 *)
   334 
   335 lemma csplit2 [simp]: "csplit$f$<x,y> = f$x$y"
   336 by (simp add: csplit_def)
   337 
   338 lemma csplit3: "csplit$cpair$z=z"
   339 by (simp add: csplit_def surjective_pairing_Cprod2)
   340 
   341 lemmas Cprod_rews = cfst2 csnd2 csplit2
   342 
   343 end