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