src/HOLCF/Up.thy
author huffman
Fri Mar 04 23:12:36 2005 +0100 (2005-03-04)
changeset 15576 efb95d0d01f7
child 15577 e16da3068ad6
permissions -rw-r--r--
converted to new-style theories, and combined numbered files
     1 (*  Title:      HOLCF/Up1.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Lifting.
     7 *)
     8 
     9 header {* The type of lifted values *}
    10 
    11 theory Up = Cfun + Sum_Type + Datatype:
    12 
    13 (* new type for lifting *)
    14 
    15 typedef (Up) ('a) "u" = "{x::(unit + 'a).True}"
    16 by auto
    17 
    18 instance u :: (sq_ord)sq_ord ..
    19 
    20 consts
    21   Iup         :: "'a => ('a)u"
    22   Ifup        :: "('a->'b)=>('a)u => 'b"
    23 
    24 defs
    25   Iup_def:     "Iup x == Abs_Up(Inr(x))"
    26   Ifup_def:    "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f$z"
    27 
    28 defs (overloaded)
    29   less_up_def: "(op <<) == (%x1 x2. case Rep_Up(x1) of                 
    30                Inl(y1) => True          
    31              | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False       
    32                                             | Inr(z2) => y2<<z2))"
    33 
    34 lemma Abs_Up_inverse2: "Rep_Up (Abs_Up y) = y"
    35 apply (simp (no_asm) add: Up_def Abs_Up_inverse)
    36 done
    37 
    38 lemma Exh_Up: "z = Abs_Up(Inl ()) | (? x. z = Iup x)"
    39 apply (unfold Iup_def)
    40 apply (rule Rep_Up_inverse [THEN subst])
    41 apply (rule_tac s = "Rep_Up z" in sumE)
    42 apply (rule disjI1)
    43 apply (rule_tac f = "Abs_Up" in arg_cong)
    44 apply (rule unit_eq [THEN subst])
    45 apply assumption
    46 apply (rule disjI2)
    47 apply (rule exI)
    48 apply (rule_tac f = "Abs_Up" in arg_cong)
    49 apply assumption
    50 done
    51 
    52 lemma inj_Abs_Up: "inj(Abs_Up)"
    53 apply (rule inj_on_inverseI)
    54 apply (rule Abs_Up_inverse2)
    55 done
    56 
    57 lemma inj_Rep_Up: "inj(Rep_Up)"
    58 apply (rule inj_on_inverseI)
    59 apply (rule Rep_Up_inverse)
    60 done
    61 
    62 lemma inject_Iup: "Iup x=Iup y ==> x=y"
    63 apply (unfold Iup_def)
    64 apply (rule inj_Inr [THEN injD])
    65 apply (rule inj_Abs_Up [THEN injD])
    66 apply assumption
    67 done
    68 
    69 declare inject_Iup [dest!]
    70 
    71 lemma defined_Iup: "Iup x~=Abs_Up(Inl ())"
    72 apply (unfold Iup_def)
    73 apply (rule notI)
    74 apply (rule notE)
    75 apply (rule Inl_not_Inr)
    76 apply (rule sym)
    77 apply (erule inj_Abs_Up [THEN injD])
    78 done
    79 
    80 
    81 lemma upE: "[| p=Abs_Up(Inl ()) ==> Q; !!x. p=Iup(x)==>Q|] ==>Q"
    82 apply (rule Exh_Up [THEN disjE])
    83 apply fast
    84 apply (erule exE)
    85 apply fast
    86 done
    87 
    88 lemma Ifup1: "Ifup(f)(Abs_Up(Inl ()))=UU"
    89 apply (unfold Ifup_def)
    90 apply (subst Abs_Up_inverse2)
    91 apply (subst sum_case_Inl)
    92 apply (rule refl)
    93 done
    94 
    95 lemma Ifup2: 
    96         "Ifup(f)(Iup(x))=f$x"
    97 apply (unfold Ifup_def Iup_def)
    98 apply (subst Abs_Up_inverse2)
    99 apply (subst sum_case_Inr)
   100 apply (rule refl)
   101 done
   102 
   103 lemmas Up0_ss = Ifup1 Ifup2
   104 
   105 declare Ifup1 [simp] Ifup2 [simp]
   106 
   107 lemma less_up1a: 
   108         "Abs_Up(Inl ())<< z"
   109 apply (unfold less_up_def)
   110 apply (subst Abs_Up_inverse2)
   111 apply (subst sum_case_Inl)
   112 apply (rule TrueI)
   113 done
   114 
   115 lemma less_up1b: 
   116         "~(Iup x) << (Abs_Up(Inl ()))"
   117 apply (unfold Iup_def less_up_def)
   118 apply (rule notI)
   119 apply (rule iffD1)
   120 prefer 2 apply (assumption)
   121 apply (subst Abs_Up_inverse2)
   122 apply (subst Abs_Up_inverse2)
   123 apply (subst sum_case_Inr)
   124 apply (subst sum_case_Inl)
   125 apply (rule refl)
   126 done
   127 
   128 lemma less_up1c: 
   129         "(Iup x) << (Iup y)=(x<<y)"
   130 apply (unfold Iup_def less_up_def)
   131 apply (subst Abs_Up_inverse2)
   132 apply (subst Abs_Up_inverse2)
   133 apply (subst sum_case_Inr)
   134 apply (subst sum_case_Inr)
   135 apply (rule refl)
   136 done
   137 
   138 declare less_up1a [iff] less_up1b [iff] less_up1c [iff]
   139 
   140 lemma refl_less_up: "(p::'a u) << p"
   141 apply (rule_tac p = "p" in upE)
   142 apply auto
   143 done
   144 
   145 lemma antisym_less_up: "[|(p1::'a u) << p2;p2 << p1|] ==> p1=p2"
   146 apply (rule_tac p = "p1" in upE)
   147 apply simp
   148 apply (rule_tac p = "p2" in upE)
   149 apply (erule sym)
   150 apply simp
   151 apply (rule_tac p = "p2" in upE)
   152 apply simp
   153 apply simp
   154 apply (drule antisym_less, assumption)
   155 apply simp
   156 done
   157 
   158 lemma trans_less_up: "[|(p1::'a u) << p2;p2 << p3|] ==> p1 << p3"
   159 apply (rule_tac p = "p1" in upE)
   160 apply simp
   161 apply (rule_tac p = "p2" in upE)
   162 apply simp
   163 apply (rule_tac p = "p3" in upE)
   164 apply auto
   165 apply (blast intro: trans_less)
   166 done
   167 
   168 (* Class Instance u::(pcpo)po *)
   169 
   170 instance u :: (pcpo)po
   171 apply (intro_classes)
   172 apply (rule refl_less_up)
   173 apply (rule antisym_less_up, assumption+)
   174 apply (rule trans_less_up, assumption+)
   175 done
   176 
   177 (* for compatibility with old HOLCF-Version *)
   178 lemma inst_up_po: "(op <<)=(%x1 x2. case Rep_Up(x1) of                 
   179                 Inl(y1) => True  
   180               | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False  
   181                                              | Inr(z2) => y2<<z2))"
   182 apply (fold less_up_def)
   183 apply (rule refl)
   184 done
   185 
   186 (* -------------------------------------------------------------------------*)
   187 (* type ('a)u is pointed                                                    *)
   188 (* ------------------------------------------------------------------------ *)
   189 
   190 lemma minimal_up: "Abs_Up(Inl ()) << z"
   191 apply (simp (no_asm) add: less_up1a)
   192 done
   193 
   194 lemmas UU_up_def = minimal_up [THEN minimal2UU, symmetric, standard]
   195 
   196 lemma least_up: "EX x::'a u. ALL y. x<<y"
   197 apply (rule_tac x = "Abs_Up (Inl ())" in exI)
   198 apply (rule minimal_up [THEN allI])
   199 done
   200 
   201 (* -------------------------------------------------------------------------*)
   202 (* access to less_up in class po                                          *)
   203 (* ------------------------------------------------------------------------ *)
   204 
   205 lemma less_up2b: "~ Iup(x) << Abs_Up(Inl ())"
   206 apply (simp (no_asm) add: less_up1b)
   207 done
   208 
   209 lemma less_up2c: "(Iup(x)<<Iup(y)) = (x<<y)"
   210 apply (simp (no_asm) add: less_up1c)
   211 done
   212 
   213 (* ------------------------------------------------------------------------ *)
   214 (* Iup and Ifup are monotone                                               *)
   215 (* ------------------------------------------------------------------------ *)
   216 
   217 lemma monofun_Iup: "monofun(Iup)"
   218 
   219 apply (unfold monofun)
   220 apply (intro strip)
   221 apply (erule less_up2c [THEN iffD2])
   222 done
   223 
   224 lemma monofun_Ifup1: "monofun(Ifup)"
   225 apply (unfold monofun)
   226 apply (intro strip)
   227 apply (rule less_fun [THEN iffD2])
   228 apply (intro strip)
   229 apply (rule_tac p = "xa" in upE)
   230 apply simp
   231 apply simp
   232 apply (erule monofun_cfun_fun)
   233 done
   234 
   235 lemma monofun_Ifup2: "monofun(Ifup(f))"
   236 apply (unfold monofun)
   237 apply (intro strip)
   238 apply (rule_tac p = "x" in upE)
   239 apply simp
   240 apply simp
   241 apply (rule_tac p = "y" in upE)
   242 apply simp
   243 apply simp
   244 apply (erule monofun_cfun_arg)
   245 done
   246 
   247 (* ------------------------------------------------------------------------ *)
   248 (* Some kind of surjectivity lemma                                          *)
   249 (* ------------------------------------------------------------------------ *)
   250 
   251 lemma up_lemma1: "z=Iup(x) ==> Iup(Ifup(LAM x. x)(z)) = z"
   252 apply simp
   253 done
   254 
   255 (* ------------------------------------------------------------------------ *)
   256 (* ('a)u is a cpo                                                           *)
   257 (* ------------------------------------------------------------------------ *)
   258 
   259 lemma lub_up1a: "[|chain(Y);EX i x. Y(i)=Iup(x)|]  
   260       ==> range(Y) <<| Iup(lub(range(%i.(Ifup (LAM x. x) (Y(i))))))"
   261 apply (rule is_lubI)
   262 apply (rule ub_rangeI)
   263 apply (rule_tac p = "Y (i) " in upE)
   264 apply (rule_tac s = "Abs_Up (Inl ())" and t = "Y (i) " in subst)
   265 apply (erule sym)
   266 apply (rule minimal_up)
   267 apply (rule_tac t = "Y (i) " in up_lemma1 [THEN subst])
   268 apply assumption
   269 apply (rule less_up2c [THEN iffD2])
   270 apply (rule is_ub_thelub)
   271 apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
   272 apply (rule_tac p = "u" in upE)
   273 apply (erule exE)
   274 apply (erule exE)
   275 apply (rule_tac P = "Y (i) <<Abs_Up (Inl ())" in notE)
   276 apply (rule_tac s = "Iup (x) " and t = "Y (i) " in ssubst)
   277 apply assumption
   278 apply (rule less_up2b)
   279 apply (erule subst)
   280 apply (erule ub_rangeD)
   281 apply (rule_tac t = "u" in up_lemma1 [THEN subst])
   282 apply assumption
   283 apply (rule less_up2c [THEN iffD2])
   284 apply (rule is_lub_thelub)
   285 apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
   286 apply (erule monofun_Ifup2 [THEN ub2ub_monofun])
   287 done
   288 
   289 lemma lub_up1b: "[|chain(Y); ALL i x. Y(i)~=Iup(x)|] ==> range(Y) <<| Abs_Up (Inl ())"
   290 apply (rule is_lubI)
   291 apply (rule ub_rangeI)
   292 apply (rule_tac p = "Y (i) " in upE)
   293 apply (rule_tac s = "Abs_Up (Inl ())" and t = "Y (i) " in ssubst)
   294 apply assumption
   295 apply (rule refl_less)
   296 apply (rule notE)
   297 apply (drule spec)
   298 apply (drule spec)
   299 apply assumption
   300 apply assumption
   301 apply (rule minimal_up)
   302 done
   303 
   304 lemmas thelub_up1a = lub_up1a [THEN thelubI, standard]
   305 (*
   306 [| chain ?Y1; EX i x. ?Y1 i = Iup x |] ==>
   307  lub (range ?Y1) = Iup (lub (range (%i. Iup (LAM x. x) (?Y1 i))))
   308 *)
   309 
   310 lemmas thelub_up1b = lub_up1b [THEN thelubI, standard]
   311 (*
   312 [| chain ?Y1; ! i x. ?Y1 i ~= Iup x |] ==>
   313  lub (range ?Y1) = UU_up
   314 *)
   315 
   316 lemma cpo_up: "chain(Y::nat=>('a)u) ==> EX x. range(Y) <<|x"
   317 apply (rule disjE)
   318 apply (rule_tac [2] exI)
   319 apply (erule_tac [2] lub_up1a)
   320 prefer 2 apply (assumption)
   321 apply (rule_tac [2] exI)
   322 apply (erule_tac [2] lub_up1b)
   323 prefer 2 apply (assumption)
   324 apply fast
   325 done
   326 
   327 (* Class instance of  ('a)u for class pcpo *)
   328 
   329 instance u :: (pcpo)pcpo
   330 apply (intro_classes)
   331 apply (erule cpo_up)
   332 apply (rule least_up)
   333 done
   334 
   335 constdefs  
   336         up  :: "'a -> ('a)u"
   337        "up  == (LAM x. Iup(x))"
   338         fup :: "('a->'c)-> ('a)u -> 'c"
   339        "fup == (LAM f p. Ifup(f)(p))"
   340 
   341 translations
   342 "case l of up$x => t1" == "fup$(LAM x. t1)$l"
   343 
   344 (* for compatibility with old HOLCF-Version *)
   345 lemma inst_up_pcpo: "UU = Abs_Up(Inl ())"
   346 apply (simp add: UU_def UU_up_def)
   347 done
   348 
   349 (* -------------------------------------------------------------------------*)
   350 (* some lemmas restated for class pcpo                                      *)
   351 (* ------------------------------------------------------------------------ *)
   352 
   353 lemma less_up3b: "~ Iup(x) << UU"
   354 apply (subst inst_up_pcpo)
   355 apply (rule less_up2b)
   356 done
   357 
   358 lemma defined_Iup2: "Iup(x) ~= UU"
   359 apply (subst inst_up_pcpo)
   360 apply (rule defined_Iup)
   361 done
   362 declare defined_Iup2 [iff]
   363 
   364 (* ------------------------------------------------------------------------ *)
   365 (* continuity for Iup                                                       *)
   366 (* ------------------------------------------------------------------------ *)
   367 
   368 lemma contlub_Iup: "contlub(Iup)"
   369 apply (rule contlubI)
   370 apply (intro strip)
   371 apply (rule trans)
   372 apply (rule_tac [2] thelub_up1a [symmetric])
   373 prefer 3 apply fast
   374 apply (erule_tac [2] monofun_Iup [THEN ch2ch_monofun])
   375 apply (rule_tac f = "Iup" in arg_cong)
   376 apply (rule lub_equal)
   377 apply assumption
   378 apply (rule monofun_Ifup2 [THEN ch2ch_monofun])
   379 apply (erule monofun_Iup [THEN ch2ch_monofun])
   380 apply simp
   381 done
   382 
   383 lemma cont_Iup: "cont(Iup)"
   384 apply (rule monocontlub2cont)
   385 apply (rule monofun_Iup)
   386 apply (rule contlub_Iup)
   387 done
   388 declare cont_Iup [iff]
   389 
   390 (* ------------------------------------------------------------------------ *)
   391 (* continuity for Ifup                                                     *)
   392 (* ------------------------------------------------------------------------ *)
   393 
   394 lemma contlub_Ifup1: "contlub(Ifup)"
   395 apply (rule contlubI)
   396 apply (intro strip)
   397 apply (rule trans)
   398 apply (rule_tac [2] thelub_fun [symmetric])
   399 apply (erule_tac [2] monofun_Ifup1 [THEN ch2ch_monofun])
   400 apply (rule ext)
   401 apply (rule_tac p = "x" in upE)
   402 apply simp
   403 apply (rule lub_const [THEN thelubI, symmetric])
   404 apply simp
   405 apply (erule contlub_cfun_fun)
   406 done
   407 
   408 
   409 lemma contlub_Ifup2: "contlub(Ifup(f))"
   410 apply (rule contlubI)
   411 apply (intro strip)
   412 apply (rule disjE)
   413 defer 1
   414 apply (subst thelub_up1a)
   415 apply assumption
   416 apply assumption
   417 apply simp
   418 prefer 2
   419 apply (subst thelub_up1b)
   420 apply assumption
   421 apply assumption
   422 apply simp
   423 apply (rule chain_UU_I_inverse [symmetric])
   424 apply (rule allI)
   425 apply (rule_tac p = "Y(i)" in upE)
   426 apply simp
   427 apply simp
   428 apply (subst contlub_cfun_arg)
   429 apply  (erule monofun_Ifup2 [THEN ch2ch_monofun])
   430 apply (rule lub_equal2)
   431 apply   (rule_tac [2] monofun_Rep_CFun2 [THEN ch2ch_monofun])
   432 apply   (erule_tac [2] monofun_Ifup2 [THEN ch2ch_monofun])
   433 apply  (erule_tac [2] monofun_Ifup2 [THEN ch2ch_monofun])
   434 apply (rule chain_mono2 [THEN exE])
   435 prefer 2 apply   (assumption)
   436 apply  (erule exE)
   437 apply  (erule exE)
   438 apply  (rule exI)
   439 apply  (rule_tac s = "Iup (x) " and t = "Y (i) " in ssubst)
   440 apply   assumption
   441 apply  (rule defined_Iup2)
   442 apply (rule exI)
   443 apply (intro strip)
   444 apply (rule_tac p = "Y (i) " in upE)
   445 prefer 2 apply simp
   446 apply (rule_tac P = "Y (i) = UU" in notE)
   447 apply  fast
   448 apply (subst inst_up_pcpo)
   449 apply assumption
   450 apply fast
   451 done
   452 
   453 lemma cont_Ifup1: "cont(Ifup)"
   454 apply (rule monocontlub2cont)
   455 apply (rule monofun_Ifup1)
   456 apply (rule contlub_Ifup1)
   457 done
   458 
   459 lemma cont_Ifup2: "cont(Ifup(f))"
   460 apply (rule monocontlub2cont)
   461 apply (rule monofun_Ifup2)
   462 apply (rule contlub_Ifup2)
   463 done
   464 
   465 
   466 (* ------------------------------------------------------------------------ *)
   467 (* continuous versions of lemmas for ('a)u                                  *)
   468 (* ------------------------------------------------------------------------ *)
   469 
   470 lemma Exh_Up1: "z = UU | (EX x. z = up$x)"
   471 
   472 apply (unfold up_def)
   473 apply simp
   474 apply (subst inst_up_pcpo)
   475 apply (rule Exh_Up)
   476 done
   477 
   478 lemma inject_up: "up$x=up$y ==> x=y"
   479 apply (unfold up_def)
   480 apply (rule inject_Iup)
   481 apply auto
   482 done
   483 
   484 lemma defined_up: " up$x ~= UU"
   485 apply (unfold up_def)
   486 apply auto
   487 done
   488 
   489 lemma upE1: 
   490         "[| p=UU ==> Q; !!x. p=up$x==>Q|] ==>Q"
   491 apply (unfold up_def)
   492 apply (rule upE)
   493 apply (simp only: inst_up_pcpo)
   494 apply fast
   495 apply simp
   496 done
   497 
   498 lemmas up_conts = cont_lemmas1 cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_CF1L
   499 
   500 lemma fup1: "fup$f$UU=UU"
   501 apply (unfold up_def fup_def)
   502 apply (subst inst_up_pcpo)
   503 apply (subst beta_cfun)
   504 apply (intro up_conts)
   505 apply (subst beta_cfun)
   506 apply (rule cont_Ifup2)
   507 apply simp
   508 done
   509 
   510 lemma fup2: "fup$f$(up$x)=f$x"
   511 apply (unfold up_def fup_def)
   512 apply (simplesubst beta_cfun)
   513 apply (rule cont_Iup)
   514 apply (subst beta_cfun)
   515 apply (intro up_conts)
   516 apply (subst beta_cfun)
   517 apply (rule cont_Ifup2)
   518 apply simp
   519 done
   520 
   521 lemma less_up4b: "~ up$x << UU"
   522 apply (unfold up_def fup_def)
   523 apply simp
   524 apply (rule less_up3b)
   525 done
   526 
   527 lemma less_up4c: 
   528          "(up$x << up$y) = (x<<y)"
   529 apply (unfold up_def fup_def)
   530 apply simp
   531 done
   532 
   533 lemma thelub_up2a: 
   534 "[| chain(Y); EX i x. Y(i) = up$x |] ==> 
   535        lub(range(Y)) = up$(lub(range(%i. fup$(LAM x. x)$(Y i))))"
   536 apply (unfold up_def fup_def)
   537 apply (subst beta_cfun)
   538 apply (rule cont_Iup)
   539 apply (subst beta_cfun)
   540 apply (intro up_conts)
   541 apply (subst beta_cfun [THEN ext])
   542 apply (rule cont_Ifup2)
   543 apply (rule thelub_up1a)
   544 apply assumption
   545 apply (erule exE)
   546 apply (erule exE)
   547 apply (rule exI)
   548 apply (rule exI)
   549 apply (erule box_equals)
   550 apply (rule refl)
   551 apply simp
   552 done
   553 
   554 
   555 
   556 lemma thelub_up2b: 
   557 "[| chain(Y); ! i x. Y(i) ~= up$x |] ==> lub(range(Y)) = UU"
   558 apply (unfold up_def fup_def)
   559 apply (subst inst_up_pcpo)
   560 apply (rule thelub_up1b)
   561 apply assumption
   562 apply (intro strip)
   563 apply (drule spec)
   564 apply (drule spec)
   565 apply simp
   566 done
   567 
   568 
   569 lemma up_lemma2: "(EX x. z = up$x) = (z~=UU)"
   570 apply (rule iffI)
   571 apply (erule exE)
   572 apply simp
   573 apply (rule defined_up)
   574 apply (rule_tac p = "z" in upE1)
   575 apply (erule notE)
   576 apply assumption
   577 apply (erule exI)
   578 done
   579 
   580 
   581 lemma thelub_up2a_rev: "[| chain(Y); lub(range(Y)) = up$x |] ==> EX i x. Y(i) = up$x"
   582 apply (rule exE)
   583 apply (rule chain_UU_I_inverse2)
   584 apply (rule up_lemma2 [THEN iffD1])
   585 apply (erule exI)
   586 apply (rule exI)
   587 apply (rule up_lemma2 [THEN iffD2])
   588 apply assumption
   589 done
   590 
   591 lemma thelub_up2b_rev: "[| chain(Y); lub(range(Y)) = UU |] ==> ! i x.  Y(i) ~= up$x"
   592 apply (blast dest!: chain_UU_I [THEN spec] exI [THEN up_lemma2 [THEN iffD1]])
   593 done
   594 
   595 
   596 lemma thelub_up3: "chain(Y) ==> lub(range(Y)) = UU |  
   597                    lub(range(Y)) = up$(lub(range(%i. fup$(LAM x. x)$(Y i))))"
   598 apply (rule disjE)
   599 apply (rule_tac [2] disjI1)
   600 apply (rule_tac [2] thelub_up2b)
   601 prefer 2 apply (assumption)
   602 prefer 2 apply (assumption)
   603 apply (rule_tac [2] disjI2)
   604 apply (rule_tac [2] thelub_up2a)
   605 prefer 2 apply (assumption)
   606 prefer 2 apply (assumption)
   607 apply fast
   608 done
   609 
   610 lemma fup3: "fup$up$x=x"
   611 apply (rule_tac p = "x" in upE1)
   612 apply (simp add: fup1 fup2)
   613 apply (simp add: fup1 fup2)
   614 done
   615 
   616 (* ------------------------------------------------------------------------ *)
   617 (* install simplifier for ('a)u                                             *)
   618 (* ------------------------------------------------------------------------ *)
   619 
   620 declare fup1 [simp] fup2 [simp] defined_up [simp]
   621 
   622 end
   623 
   624 
   625