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