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