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