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