src/HOLCF/Cprod.thy
changeset 15576 efb95d0d01f7
child 15577 e16da3068ad6
equal deleted inserted replaced
15575:63babb1ee883 15576:efb95d0d01f7
       
     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 = Cfun:
       
    12 
       
    13 defaultsort cpo
       
    14 
       
    15 instance "*"::(sq_ord,sq_ord)sq_ord ..
       
    16 
       
    17 defs (overloaded)
       
    18 
       
    19   less_cprod_def: "p1 << p2 == (fst p1<<fst p2 & snd p1 << snd p2)"
       
    20 
       
    21 (* ------------------------------------------------------------------------ *)
       
    22 (* less_cprod is a partial order on 'a * 'b                                 *)
       
    23 (* ------------------------------------------------------------------------ *)
       
    24 
       
    25 lemma refl_less_cprod: "(p::'a*'b) << p"
       
    26 apply (unfold less_cprod_def)
       
    27 apply simp
       
    28 done
       
    29 
       
    30 lemma antisym_less_cprod: "[|(p1::'a * 'b) << p2;p2 << p1|] ==> p1=p2"
       
    31 apply (unfold less_cprod_def)
       
    32 apply (rule injective_fst_snd)
       
    33 apply (fast intro: antisym_less)
       
    34 apply (fast intro: antisym_less)
       
    35 done
       
    36 
       
    37 lemma trans_less_cprod: 
       
    38         "[|(p1::'a*'b) << p2;p2 << p3|] ==> p1 << p3"
       
    39 apply (unfold less_cprod_def)
       
    40 apply (rule conjI)
       
    41 apply (fast intro: trans_less)
       
    42 apply (fast intro: trans_less)
       
    43 done
       
    44 
       
    45 (* Class Instance *::(pcpo,pcpo)po *)
       
    46 
       
    47 defaultsort pcpo
       
    48 
       
    49 instance "*"::(cpo,cpo)po
       
    50 apply (intro_classes)
       
    51 apply (rule refl_less_cprod)
       
    52 apply (rule antisym_less_cprod, assumption+)
       
    53 apply (rule trans_less_cprod, assumption+)
       
    54 done
       
    55 
       
    56 (* for compatibility with old HOLCF-Version *)
       
    57 lemma inst_cprod_po: "(op <<)=(%x y. fst x<<fst y & snd x<<snd y)"
       
    58 apply (fold less_cprod_def)
       
    59 apply (rule refl)
       
    60 done
       
    61 
       
    62 lemma less_cprod4c: "(x1,y1) << (x2,y2) ==> x1 << x2 & y1 << y2"
       
    63 apply (simp add: inst_cprod_po)
       
    64 done
       
    65 
       
    66 (* ------------------------------------------------------------------------ *)
       
    67 (* type cprod is pointed                                                    *)
       
    68 (* ------------------------------------------------------------------------ *)
       
    69 
       
    70 lemma minimal_cprod: "(UU,UU)<<p"
       
    71 apply (simp (no_asm) add: inst_cprod_po)
       
    72 done
       
    73 
       
    74 lemmas UU_cprod_def = minimal_cprod [THEN minimal2UU, symmetric, standard]
       
    75 
       
    76 lemma least_cprod: "EX x::'a*'b. ALL y. x<<y"
       
    77 apply (rule_tac x = " (UU,UU) " in exI)
       
    78 apply (rule minimal_cprod [THEN allI])
       
    79 done
       
    80 
       
    81 (* ------------------------------------------------------------------------ *)
       
    82 (* Pair <_,_>  is monotone in both arguments                                *)
       
    83 (* ------------------------------------------------------------------------ *)
       
    84 
       
    85 lemma monofun_pair1: "monofun Pair"
       
    86 
       
    87 apply (unfold monofun)
       
    88 apply (intro strip)
       
    89 apply (rule less_fun [THEN iffD2])
       
    90 apply (intro strip)
       
    91 apply (simp (no_asm_simp) add: inst_cprod_po)
       
    92 done
       
    93 
       
    94 lemma monofun_pair2: "monofun(Pair x)"
       
    95 apply (unfold monofun)
       
    96 apply (simp (no_asm_simp) add: inst_cprod_po)
       
    97 done
       
    98 
       
    99 lemma monofun_pair: "[|x1<<x2; y1<<y2|] ==> (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)"
       
   100 apply (rule trans_less)
       
   101 apply (erule monofun_pair1 [THEN monofunE, THEN spec, THEN spec, THEN mp, THEN less_fun [THEN iffD1, THEN spec]])
       
   102 apply (erule monofun_pair2 [THEN monofunE, THEN spec, THEN spec, THEN mp])
       
   103 done
       
   104 
       
   105 (* ------------------------------------------------------------------------ *)
       
   106 (* fst and snd are monotone                                                 *)
       
   107 (* ------------------------------------------------------------------------ *)
       
   108 
       
   109 lemma monofun_fst: "monofun fst"
       
   110 apply (unfold monofun)
       
   111 apply (intro strip)
       
   112 apply (rule_tac p = "x" in PairE)
       
   113 apply (rule_tac p = "y" in PairE)
       
   114 apply simp
       
   115 apply (erule less_cprod4c [THEN conjunct1])
       
   116 done
       
   117 
       
   118 lemma monofun_snd: "monofun snd"
       
   119 apply (unfold monofun)
       
   120 apply (intro strip)
       
   121 apply (rule_tac p = "x" in PairE)
       
   122 apply (rule_tac p = "y" in PairE)
       
   123 apply simp
       
   124 apply (erule less_cprod4c [THEN conjunct2])
       
   125 done
       
   126 
       
   127 (* ------------------------------------------------------------------------ *)
       
   128 (* the type 'a * 'b is a cpo                                                *)
       
   129 (* ------------------------------------------------------------------------ *)
       
   130 
       
   131 lemma lub_cprod: 
       
   132 "chain S ==> range S<<|(lub(range(%i. fst(S i))),lub(range(%i. snd(S i))))"
       
   133 apply (rule is_lubI)
       
   134 apply (rule ub_rangeI)
       
   135 apply (rule_tac t = "S i" in surjective_pairing [THEN ssubst])
       
   136 apply (rule monofun_pair)
       
   137 apply (rule is_ub_thelub)
       
   138 apply (erule monofun_fst [THEN ch2ch_monofun])
       
   139 apply (rule is_ub_thelub)
       
   140 apply (erule monofun_snd [THEN ch2ch_monofun])
       
   141 apply (rule_tac t = "u" in surjective_pairing [THEN ssubst])
       
   142 apply (rule monofun_pair)
       
   143 apply (rule is_lub_thelub)
       
   144 apply (erule monofun_fst [THEN ch2ch_monofun])
       
   145 apply (erule monofun_fst [THEN ub2ub_monofun])
       
   146 apply (rule is_lub_thelub)
       
   147 apply (erule monofun_snd [THEN ch2ch_monofun])
       
   148 apply (erule monofun_snd [THEN ub2ub_monofun])
       
   149 done
       
   150 
       
   151 lemmas thelub_cprod = lub_cprod [THEN thelubI, standard]
       
   152 (*
       
   153 "chain ?S1 ==>
       
   154  lub (range ?S1) =
       
   155  (lub (range (%i. fst (?S1 i))), lub (range (%i. snd (?S1 i))))" : thm
       
   156 
       
   157 *)
       
   158 
       
   159 lemma cpo_cprod: "chain(S::nat=>'a::cpo*'b::cpo)==>EX x. range S<<| x"
       
   160 apply (rule exI)
       
   161 apply (erule lub_cprod)
       
   162 done
       
   163 
       
   164 (* Class instance of * for class pcpo and cpo. *)
       
   165 
       
   166 instance "*" :: (cpo,cpo)cpo
       
   167 by (intro_classes, rule cpo_cprod)
       
   168 
       
   169 instance "*" :: (pcpo,pcpo)pcpo
       
   170 by (intro_classes, rule least_cprod)
       
   171 
       
   172 consts
       
   173         cpair        :: "'a::cpo -> 'b::cpo -> ('a*'b)" (* continuous pairing *)
       
   174         cfst         :: "('a::cpo*'b::cpo)->'a"
       
   175         csnd         :: "('a::cpo*'b::cpo)->'b"
       
   176         csplit       :: "('a::cpo->'b::cpo->'c::cpo)->('a*'b)->'c"
       
   177 
       
   178 syntax
       
   179         "@ctuple"    :: "['a, args] => 'a * 'b"         ("(1<_,/ _>)")
       
   180 
       
   181 translations
       
   182         "<x, y, z>"   == "<x, <y, z>>"
       
   183         "<x, y>"      == "cpair$x$y"
       
   184 
       
   185 defs
       
   186 cpair_def:       "cpair  == (LAM x y.(x,y))"
       
   187 cfst_def:        "cfst   == (LAM p. fst(p))"
       
   188 csnd_def:        "csnd   == (LAM p. snd(p))"      
       
   189 csplit_def:      "csplit == (LAM f p. f$(cfst$p)$(csnd$p))"
       
   190 
       
   191 
       
   192 
       
   193 (* introduce syntax for
       
   194 
       
   195    Let <x,y> = e1; z = E2 in E3
       
   196 
       
   197    and
       
   198 
       
   199    LAM <x,y,z>.e
       
   200 *)
       
   201 
       
   202 constdefs
       
   203   CLet           :: "'a -> ('a -> 'b) -> 'b"
       
   204   "CLet == LAM s f. f$s"
       
   205 
       
   206 
       
   207 (* syntax for Let *)
       
   208 
       
   209 nonterminals
       
   210   Cletbinds  Cletbind
       
   211 
       
   212 syntax
       
   213   "_Cbind"  :: "[pttrn, 'a] => Cletbind"             ("(2_ =/ _)" 10)
       
   214   ""        :: "Cletbind => Cletbinds"               ("_")
       
   215   "_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds"  ("_;/ _")
       
   216   "_CLet"   :: "[Cletbinds, 'a] => 'a"               ("(Let (_)/ in (_))" 10)
       
   217 
       
   218 translations
       
   219   "_CLet (_Cbinds b bs) e"  == "_CLet b (_CLet bs e)"
       
   220   "Let x = a in e"          == "CLet$a$(LAM x. e)"
       
   221 
       
   222 
       
   223 (* syntax for LAM <x,y,z>.e *)
       
   224 
       
   225 syntax
       
   226   "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3LAM <_>./ _)" [0, 10] 10)
       
   227 
       
   228 translations
       
   229   "LAM <x,y,zs>.b"        == "csplit$(LAM x. LAM <y,zs>.b)"
       
   230   "LAM <x,y>. LAM zs. b"  <= "csplit$(LAM x y zs. b)"
       
   231   "LAM <x,y>.b"           == "csplit$(LAM x y. b)"
       
   232 
       
   233 syntax (xsymbols)
       
   234   "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\\<Lambda>()<_>./ _)" [0, 10] 10)
       
   235 
       
   236 (* for compatibility with old HOLCF-Version *)
       
   237 lemma inst_cprod_pcpo: "UU = (UU,UU)"
       
   238 apply (simp add: UU_cprod_def[folded UU_def])
       
   239 done
       
   240 
       
   241 (* ------------------------------------------------------------------------ *)
       
   242 (* continuity of (_,_) , fst, snd                                           *)
       
   243 (* ------------------------------------------------------------------------ *)
       
   244 
       
   245 lemma Cprod3_lemma1: 
       
   246 "chain(Y::(nat=>'a::cpo)) ==> 
       
   247   (lub(range(Y)),(x::'b::cpo)) = 
       
   248   (lub(range(%i. fst(Y i,x))),lub(range(%i. snd(Y i,x))))"
       
   249 apply (rule_tac f1 = "Pair" in arg_cong [THEN cong])
       
   250 apply (rule lub_equal)
       
   251 apply assumption
       
   252 apply (rule monofun_fst [THEN ch2ch_monofun])
       
   253 apply (rule ch2ch_fun)
       
   254 apply (rule monofun_pair1 [THEN ch2ch_monofun])
       
   255 apply assumption
       
   256 apply (rule allI)
       
   257 apply (simp (no_asm))
       
   258 apply (rule sym)
       
   259 apply (simp (no_asm))
       
   260 apply (rule lub_const [THEN thelubI])
       
   261 done
       
   262 
       
   263 lemma contlub_pair1: "contlub(Pair)"
       
   264 apply (rule contlubI)
       
   265 apply (intro strip)
       
   266 apply (rule expand_fun_eq [THEN iffD2])
       
   267 apply (intro strip)
       
   268 apply (subst lub_fun [THEN thelubI])
       
   269 apply (erule monofun_pair1 [THEN ch2ch_monofun])
       
   270 apply (rule trans)
       
   271 apply (rule_tac [2] thelub_cprod [symmetric])
       
   272 apply (rule_tac [2] ch2ch_fun)
       
   273 apply (erule_tac [2] monofun_pair1 [THEN ch2ch_monofun])
       
   274 apply (erule Cprod3_lemma1)
       
   275 done
       
   276 
       
   277 lemma Cprod3_lemma2: 
       
   278 "chain(Y::(nat=>'a::cpo)) ==> 
       
   279   ((x::'b::cpo),lub(range Y)) = 
       
   280   (lub(range(%i. fst(x,Y i))),lub(range(%i. snd(x, Y i))))"
       
   281 apply (rule_tac f1 = "Pair" in arg_cong [THEN cong])
       
   282 apply (rule sym)
       
   283 apply (simp (no_asm))
       
   284 apply (rule lub_const [THEN thelubI])
       
   285 apply (rule lub_equal)
       
   286 apply assumption
       
   287 apply (rule monofun_snd [THEN ch2ch_monofun])
       
   288 apply (rule monofun_pair2 [THEN ch2ch_monofun])
       
   289 apply assumption
       
   290 apply (rule allI)
       
   291 apply (simp (no_asm))
       
   292 done
       
   293 
       
   294 lemma contlub_pair2: "contlub(Pair(x))"
       
   295 apply (rule contlubI)
       
   296 apply (intro strip)
       
   297 apply (rule trans)
       
   298 apply (rule_tac [2] thelub_cprod [symmetric])
       
   299 apply (erule_tac [2] monofun_pair2 [THEN ch2ch_monofun])
       
   300 apply (erule Cprod3_lemma2)
       
   301 done
       
   302 
       
   303 lemma cont_pair1: "cont(Pair)"
       
   304 apply (rule monocontlub2cont)
       
   305 apply (rule monofun_pair1)
       
   306 apply (rule contlub_pair1)
       
   307 done
       
   308 
       
   309 lemma cont_pair2: "cont(Pair(x))"
       
   310 apply (rule monocontlub2cont)
       
   311 apply (rule monofun_pair2)
       
   312 apply (rule contlub_pair2)
       
   313 done
       
   314 
       
   315 lemma contlub_fst: "contlub(fst)"
       
   316 apply (rule contlubI)
       
   317 apply (intro strip)
       
   318 apply (subst lub_cprod [THEN thelubI])
       
   319 apply assumption
       
   320 apply (simp (no_asm))
       
   321 done
       
   322 
       
   323 lemma contlub_snd: "contlub(snd)"
       
   324 apply (rule contlubI)
       
   325 apply (intro strip)
       
   326 apply (subst lub_cprod [THEN thelubI])
       
   327 apply assumption
       
   328 apply (simp (no_asm))
       
   329 done
       
   330 
       
   331 lemma cont_fst: "cont(fst)"
       
   332 apply (rule monocontlub2cont)
       
   333 apply (rule monofun_fst)
       
   334 apply (rule contlub_fst)
       
   335 done
       
   336 
       
   337 lemma cont_snd: "cont(snd)"
       
   338 apply (rule monocontlub2cont)
       
   339 apply (rule monofun_snd)
       
   340 apply (rule contlub_snd)
       
   341 done
       
   342 
       
   343 (* 
       
   344  -------------------------------------------------------------------------- 
       
   345  more lemmas for Cprod3.thy 
       
   346  
       
   347  -------------------------------------------------------------------------- 
       
   348 *)
       
   349 
       
   350 (* ------------------------------------------------------------------------ *)
       
   351 (* convert all lemmas to the continuous versions                            *)
       
   352 (* ------------------------------------------------------------------------ *)
       
   353 
       
   354 lemma beta_cfun_cprod: 
       
   355         "(LAM x y.(x,y))$a$b = (a,b)"
       
   356 apply (subst beta_cfun)
       
   357 apply (simp (no_asm) add: cont_pair1 cont_pair2 cont2cont_CF1L)
       
   358 apply (subst beta_cfun)
       
   359 apply (rule cont_pair2)
       
   360 apply (rule refl)
       
   361 done
       
   362 
       
   363 lemma inject_cpair: 
       
   364         "<a,b> = <aa,ba>  ==> a=aa & b=ba"
       
   365 apply (unfold cpair_def)
       
   366 apply (drule beta_cfun_cprod [THEN subst])
       
   367 apply (drule beta_cfun_cprod [THEN subst])
       
   368 apply (erule Pair_inject)
       
   369 apply fast
       
   370 done
       
   371 
       
   372 lemma inst_cprod_pcpo2: "UU = <UU,UU>"
       
   373 apply (unfold cpair_def)
       
   374 apply (rule sym)
       
   375 apply (rule trans)
       
   376 apply (rule beta_cfun_cprod)
       
   377 apply (rule sym)
       
   378 apply (rule inst_cprod_pcpo)
       
   379 done
       
   380 
       
   381 lemma defined_cpair_rev: 
       
   382  "<a,b> = UU ==> a = UU & b = UU"
       
   383 apply (drule inst_cprod_pcpo2 [THEN subst])
       
   384 apply (erule inject_cpair)
       
   385 done
       
   386 
       
   387 lemma Exh_Cprod2:
       
   388         "? a b. z=<a,b>"
       
   389 apply (unfold cpair_def)
       
   390 apply (rule PairE)
       
   391 apply (rule exI)
       
   392 apply (rule exI)
       
   393 apply (erule beta_cfun_cprod [THEN ssubst])
       
   394 done
       
   395 
       
   396 lemma cprodE:
       
   397 assumes prems: "!!x y. [| p = <x,y> |] ==> Q"
       
   398 shows "Q"
       
   399 apply (rule PairE)
       
   400 apply (rule prems)
       
   401 apply (unfold cpair_def)
       
   402 apply (erule beta_cfun_cprod [THEN ssubst])
       
   403 done
       
   404 
       
   405 lemma cfst2: 
       
   406         "cfst$<x,y> = x"
       
   407 apply (unfold cfst_def cpair_def)
       
   408 apply (subst beta_cfun_cprod)
       
   409 apply (subst beta_cfun)
       
   410 apply (rule cont_fst)
       
   411 apply (simp (no_asm))
       
   412 done
       
   413 
       
   414 lemma csnd2: 
       
   415         "csnd$<x,y> = y"
       
   416 apply (unfold csnd_def cpair_def)
       
   417 apply (subst beta_cfun_cprod)
       
   418 apply (subst beta_cfun)
       
   419 apply (rule cont_snd)
       
   420 apply (simp (no_asm))
       
   421 done
       
   422 
       
   423 lemma cfst_strict: "cfst$UU = UU"
       
   424 apply (simp add: inst_cprod_pcpo2 cfst2)
       
   425 done
       
   426 
       
   427 lemma csnd_strict: "csnd$UU = UU"
       
   428 apply (simp add: inst_cprod_pcpo2 csnd2)
       
   429 done
       
   430 
       
   431 lemma surjective_pairing_Cprod2: "<cfst$p , csnd$p> = p"
       
   432 apply (unfold cfst_def csnd_def cpair_def)
       
   433 apply (subst beta_cfun_cprod)
       
   434 apply (simplesubst beta_cfun)
       
   435 apply (rule cont_snd)
       
   436 apply (subst beta_cfun)
       
   437 apply (rule cont_fst)
       
   438 apply (rule surjective_pairing [symmetric])
       
   439 done
       
   440 
       
   441 lemma less_cprod5c: 
       
   442  "<xa,ya> << <x,y> ==> xa<<x & ya << y"
       
   443 apply (unfold cfst_def csnd_def cpair_def)
       
   444 apply (rule less_cprod4c)
       
   445 apply (drule beta_cfun_cprod [THEN subst])
       
   446 apply (drule beta_cfun_cprod [THEN subst])
       
   447 apply assumption
       
   448 done
       
   449 
       
   450 lemma lub_cprod2: 
       
   451 "[|chain(S)|] ==> range(S) <<|  
       
   452   <(lub(range(%i. cfst$(S i)))) , lub(range(%i. csnd$(S i)))>"
       
   453 apply (unfold cfst_def csnd_def cpair_def)
       
   454 apply (subst beta_cfun_cprod)
       
   455 apply (simplesubst beta_cfun [THEN ext])
       
   456 apply (rule cont_snd)
       
   457 apply (subst beta_cfun [THEN ext])
       
   458 apply (rule cont_fst)
       
   459 apply (rule lub_cprod)
       
   460 apply assumption
       
   461 done
       
   462 
       
   463 lemmas thelub_cprod2 = lub_cprod2 [THEN thelubI, standard]
       
   464 (*
       
   465 chain ?S1 ==>
       
   466  lub (range ?S1) =
       
   467  <lub (range (%i. cfst$(?S1 i))), lub (range (%i. csnd$(?S1 i)))>" 
       
   468 *)
       
   469 lemma csplit2: 
       
   470         "csplit$f$<x,y> = f$x$y"
       
   471 apply (unfold csplit_def)
       
   472 apply (subst beta_cfun)
       
   473 apply (simp (no_asm))
       
   474 apply (simp (no_asm) add: cfst2 csnd2)
       
   475 done
       
   476 
       
   477 lemma csplit3: 
       
   478   "csplit$cpair$z=z"
       
   479 apply (unfold csplit_def)
       
   480 apply (subst beta_cfun)
       
   481 apply (simp (no_asm))
       
   482 apply (simp (no_asm) add: surjective_pairing_Cprod2)
       
   483 done
       
   484 
       
   485 (* ------------------------------------------------------------------------ *)
       
   486 (* install simplifier for Cprod                                             *)
       
   487 (* ------------------------------------------------------------------------ *)
       
   488 
       
   489 declare cfst2 [simp] csnd2 [simp] csplit2 [simp]
       
   490 
       
   491 lemmas Cprod_rews = cfst2 csnd2 csplit2
       
   492 
       
   493 end