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