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