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