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