src/HOLCF/Up3.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 5291 5706f0ef1d43
child 8161 bde1391fd0a5
permissions -rw-r--r--
made tutorial first;
oheimb@2278
     1
(*  Title:      HOLCF/Up3.ML
oheimb@2278
     2
    ID:         $Id$
oheimb@2278
     3
    Author:     Franz Regensburger
oheimb@2278
     4
    Copyright   1993 Technische Universitaet Muenchen
oheimb@2278
     5
oheimb@2278
     6
Lemmas for Up3.thy
oheimb@2278
     7
*)
oheimb@2278
     8
oheimb@2278
     9
open Up3;
oheimb@2278
    10
slotosch@2640
    11
(* for compatibility with old HOLCF-Version *)
slotosch@2640
    12
qed_goal "inst_up_pcpo" thy "UU = Abs_Up(Inl ())"
slotosch@2640
    13
 (fn prems => 
slotosch@2640
    14
        [
slotosch@2640
    15
        (simp_tac (HOL_ss addsimps [UU_def,UU_up_def]) 1)
slotosch@2640
    16
        ]);
slotosch@2640
    17
oheimb@2278
    18
(* -------------------------------------------------------------------------*)
oheimb@2278
    19
(* some lemmas restated for class pcpo                                      *)
oheimb@2278
    20
(* ------------------------------------------------------------------------ *)
oheimb@2278
    21
slotosch@2640
    22
qed_goal "less_up3b" thy "~ Iup(x) << UU"
oheimb@2278
    23
 (fn prems =>
oheimb@2278
    24
        [
oheimb@2278
    25
        (stac inst_up_pcpo 1),
oheimb@2278
    26
        (rtac less_up2b 1)
oheimb@2278
    27
        ]);
oheimb@2278
    28
slotosch@2640
    29
qed_goal "defined_Iup2" thy "Iup(x) ~= UU"
oheimb@2278
    30
 (fn prems =>
oheimb@2278
    31
        [
oheimb@2278
    32
        (stac inst_up_pcpo 1),
oheimb@2278
    33
        (rtac defined_Iup 1)
oheimb@2278
    34
        ]);
oheimb@2278
    35
oheimb@2278
    36
(* ------------------------------------------------------------------------ *)
oheimb@2278
    37
(* continuity for Iup                                                       *)
oheimb@2278
    38
(* ------------------------------------------------------------------------ *)
oheimb@2278
    39
slotosch@2640
    40
qed_goal "contlub_Iup" thy "contlub(Iup)"
oheimb@2278
    41
 (fn prems =>
oheimb@2278
    42
        [
oheimb@2278
    43
        (rtac contlubI 1),
oheimb@2278
    44
        (strip_tac 1),
oheimb@2278
    45
        (rtac trans 1),
oheimb@2278
    46
        (rtac (thelub_up1a RS sym) 2),
oheimb@2278
    47
        (fast_tac HOL_cs 3),
oheimb@2278
    48
        (etac (monofun_Iup RS ch2ch_monofun) 2),
oheimb@2278
    49
        (res_inst_tac [("f","Iup")] arg_cong  1),
oheimb@2278
    50
        (rtac lub_equal 1),
oheimb@2278
    51
        (atac 1),
oheimb@2278
    52
        (rtac (monofun_Ifup2 RS ch2ch_monofun) 1),
oheimb@2278
    53
        (etac (monofun_Iup RS ch2ch_monofun) 1),
oheimb@2278
    54
        (asm_simp_tac Up0_ss 1)
oheimb@2278
    55
        ]);
oheimb@2278
    56
slotosch@2640
    57
qed_goal "cont_Iup" thy "cont(Iup)"
oheimb@2278
    58
 (fn prems =>
oheimb@2278
    59
        [
oheimb@2278
    60
        (rtac monocontlub2cont 1),
oheimb@2278
    61
        (rtac monofun_Iup 1),
oheimb@2278
    62
        (rtac contlub_Iup 1)
oheimb@2278
    63
        ]);
oheimb@2278
    64
oheimb@2278
    65
oheimb@2278
    66
(* ------------------------------------------------------------------------ *)
oheimb@2278
    67
(* continuity for Ifup                                                     *)
oheimb@2278
    68
(* ------------------------------------------------------------------------ *)
oheimb@2278
    69
slotosch@2640
    70
qed_goal "contlub_Ifup1" thy "contlub(Ifup)"
oheimb@2278
    71
 (fn prems =>
oheimb@2278
    72
        [
oheimb@2278
    73
        (rtac contlubI 1),
oheimb@2278
    74
        (strip_tac 1),
oheimb@2278
    75
        (rtac trans 1),
oheimb@2278
    76
        (rtac (thelub_fun RS sym) 2),
oheimb@2278
    77
        (etac (monofun_Ifup1 RS ch2ch_monofun) 2),
oheimb@2278
    78
        (rtac ext 1),
oheimb@2278
    79
        (res_inst_tac [("p","x")] upE 1),
oheimb@2278
    80
        (asm_simp_tac Up0_ss 1),
oheimb@2278
    81
        (rtac (lub_const RS thelubI RS sym) 1),
oheimb@2278
    82
        (asm_simp_tac Up0_ss 1),
oheimb@2278
    83
        (etac contlub_cfun_fun 1)
oheimb@2278
    84
        ]);
oheimb@2278
    85
oheimb@2278
    86
slotosch@2640
    87
qed_goal "contlub_Ifup2" thy "contlub(Ifup(f))"
oheimb@2278
    88
 (fn prems =>
oheimb@2278
    89
        [
oheimb@2278
    90
        (rtac contlubI 1),
oheimb@2278
    91
        (strip_tac 1),
oheimb@2278
    92
        (rtac disjE 1),
oheimb@2278
    93
        (stac thelub_up1a 2),
oheimb@2278
    94
        (atac 2),
oheimb@2278
    95
        (atac 2),
oheimb@2278
    96
        (asm_simp_tac Up0_ss 2),
oheimb@2278
    97
        (stac thelub_up1b 3),
oheimb@2278
    98
        (atac 3),
oheimb@2278
    99
        (atac 3),
oheimb@2278
   100
        (fast_tac HOL_cs 1),
oheimb@2278
   101
        (asm_simp_tac Up0_ss 2),
oheimb@2278
   102
        (rtac (chain_UU_I_inverse RS sym) 2),
oheimb@2278
   103
        (rtac allI 2),
oheimb@2278
   104
        (res_inst_tac [("p","Y(i)")] upE 2),
oheimb@2278
   105
        (asm_simp_tac Up0_ss 2),
oheimb@2278
   106
        (rtac notE 2),
oheimb@2278
   107
        (dtac spec 2),
oheimb@2278
   108
        (etac spec 2),
oheimb@2278
   109
        (atac 2),
oheimb@2278
   110
        (stac contlub_cfun_arg 1),
oheimb@2278
   111
        (etac (monofun_Ifup2 RS ch2ch_monofun) 1),
oheimb@2278
   112
        (rtac lub_equal2 1),
slotosch@5291
   113
        (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 2),
oheimb@2278
   114
        (etac (monofun_Ifup2 RS ch2ch_monofun) 2),
oheimb@2278
   115
        (etac (monofun_Ifup2 RS ch2ch_monofun) 2),
oheimb@2278
   116
        (rtac (chain_mono2 RS exE) 1),
oheimb@2278
   117
        (atac 2),
oheimb@2278
   118
        (etac exE 1),
oheimb@2278
   119
        (etac exE 1),
oheimb@2278
   120
        (rtac exI 1),
oheimb@2278
   121
        (res_inst_tac [("s","Iup(x)"),("t","Y(i)")] ssubst 1),
oheimb@2278
   122
        (atac 1),
oheimb@2278
   123
        (rtac defined_Iup2 1),
oheimb@2278
   124
        (rtac exI 1),
oheimb@2278
   125
        (strip_tac 1),
oheimb@2278
   126
        (res_inst_tac [("p","Y(i)")] upE 1),
oheimb@2278
   127
        (asm_simp_tac Up0_ss 2),
oheimb@2278
   128
        (res_inst_tac [("P","Y(i) = UU")] notE 1),
oheimb@2278
   129
        (fast_tac HOL_cs 1),
oheimb@2278
   130
        (stac inst_up_pcpo 1),
oheimb@2278
   131
        (atac 1)
oheimb@2278
   132
        ]);
oheimb@2278
   133
slotosch@2640
   134
qed_goal "cont_Ifup1" thy "cont(Ifup)"
oheimb@2278
   135
 (fn prems =>
oheimb@2278
   136
        [
oheimb@2278
   137
        (rtac monocontlub2cont 1),
oheimb@2278
   138
        (rtac monofun_Ifup1 1),
oheimb@2278
   139
        (rtac contlub_Ifup1 1)
oheimb@2278
   140
        ]);
oheimb@2278
   141
slotosch@2640
   142
qed_goal "cont_Ifup2" thy "cont(Ifup(f))"
oheimb@2278
   143
 (fn prems =>
oheimb@2278
   144
        [
oheimb@2278
   145
        (rtac monocontlub2cont 1),
oheimb@2278
   146
        (rtac monofun_Ifup2 1),
oheimb@2278
   147
        (rtac contlub_Ifup2 1)
oheimb@2278
   148
        ]);
oheimb@2278
   149
oheimb@2278
   150
oheimb@2278
   151
(* ------------------------------------------------------------------------ *)
oheimb@2278
   152
(* continuous versions of lemmas for ('a)u                                  *)
oheimb@2278
   153
(* ------------------------------------------------------------------------ *)
oheimb@2278
   154
slotosch@2640
   155
qed_goalw "Exh_Up1" thy [up_def] "z = UU | (? x. z = up`x)"
oheimb@2278
   156
 (fn prems =>
oheimb@2278
   157
        [
oheimb@2278
   158
        (simp_tac (Up0_ss addsimps [cont_Iup]) 1),
oheimb@2278
   159
        (stac inst_up_pcpo 1),
oheimb@2278
   160
        (rtac Exh_Up 1)
oheimb@2278
   161
        ]);
oheimb@2278
   162
slotosch@2640
   163
qed_goalw "inject_up" thy [up_def] "up`x=up`y ==> x=y"
oheimb@2278
   164
 (fn prems =>
oheimb@2278
   165
        [
oheimb@2278
   166
        (cut_facts_tac prems 1),
oheimb@2278
   167
        (rtac inject_Iup 1),
oheimb@2278
   168
        (etac box_equals 1),
oheimb@2278
   169
        (simp_tac (Up0_ss addsimps [cont_Iup]) 1),
oheimb@2278
   170
        (simp_tac (Up0_ss addsimps [cont_Iup]) 1)
oheimb@2278
   171
        ]);
oheimb@2278
   172
slotosch@2640
   173
qed_goalw "defined_up" thy [up_def] " up`x ~= UU"
oheimb@2278
   174
 (fn prems =>
oheimb@2278
   175
        [
oheimb@2278
   176
        (simp_tac (Up0_ss addsimps [cont_Iup]) 1),
oheimb@2278
   177
        (rtac defined_Iup2 1)
oheimb@2278
   178
        ]);
oheimb@2278
   179
slotosch@2640
   180
qed_goalw "upE1" thy [up_def] 
oheimb@2278
   181
        "[| p=UU ==> Q; !!x. p=up`x==>Q|] ==>Q"
oheimb@2278
   182
 (fn prems =>
oheimb@2278
   183
        [
oheimb@2278
   184
        (rtac upE 1),
oheimb@2278
   185
        (resolve_tac prems 1),
oheimb@2278
   186
        (etac (inst_up_pcpo RS ssubst) 1),
oheimb@2278
   187
        (resolve_tac (tl prems) 1),
oheimb@2278
   188
        (asm_simp_tac (Up0_ss addsimps [cont_Iup]) 1)
oheimb@2278
   189
        ]);
oheimb@2278
   190
wenzelm@4098
   191
val tac = (simp_tac (simpset() addsimps [cont_Iup,cont_Ifup1,
oheimb@2566
   192
                cont_Ifup2,cont2cont_CF1L]) 1);
oheimb@2278
   193
slotosch@2640
   194
qed_goalw "fup1" thy [up_def,fup_def] "fup`f`UU=UU"
oheimb@2278
   195
 (fn prems =>
oheimb@2278
   196
        [
oheimb@2278
   197
        (stac inst_up_pcpo 1),
oheimb@2278
   198
        (stac beta_cfun 1),
oheimb@2566
   199
	tac,
oheimb@2278
   200
        (stac beta_cfun 1),
oheimb@2566
   201
	tac,
oheimb@2278
   202
        (simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1)
oheimb@2278
   203
        ]);
oheimb@2278
   204
slotosch@2640
   205
qed_goalw "fup2" thy [up_def,fup_def] "fup`f`(up`x)=f`x"
oheimb@2278
   206
 (fn prems =>
oheimb@2278
   207
        [
oheimb@2278
   208
        (stac beta_cfun 1),
oheimb@2278
   209
        (rtac cont_Iup 1),
oheimb@2278
   210
        (stac beta_cfun 1),
oheimb@2566
   211
	tac,
oheimb@2278
   212
        (stac beta_cfun 1),
oheimb@2278
   213
        (rtac cont_Ifup2 1),
oheimb@2278
   214
        (simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1)
oheimb@2278
   215
        ]);
oheimb@2278
   216
slotosch@2640
   217
qed_goalw "less_up4b" thy [up_def,fup_def] "~ up`x << UU"
oheimb@2278
   218
 (fn prems =>
oheimb@2278
   219
        [
oheimb@2278
   220
        (simp_tac (Up0_ss addsimps [cont_Iup]) 1),
oheimb@2278
   221
        (rtac less_up3b 1)
oheimb@2278
   222
        ]);
oheimb@2278
   223
slotosch@2640
   224
qed_goalw "less_up4c" thy [up_def,fup_def]
oheimb@2278
   225
         "(up`x << up`y) = (x<<y)"
oheimb@2278
   226
 (fn prems =>
oheimb@2278
   227
        [
oheimb@2278
   228
        (simp_tac (Up0_ss addsimps [cont_Iup]) 1),
oheimb@2278
   229
        (rtac less_up2c 1)
oheimb@2278
   230
        ]);
oheimb@2278
   231
slotosch@2640
   232
qed_goalw "thelub_up2a" thy [up_def,fup_def] 
oheimb@4721
   233
"[| chain(Y); ? i x. Y(i) = up`x |] ==>\
oheimb@2278
   234
\      lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))"
oheimb@2278
   235
 (fn prems =>
oheimb@2278
   236
        [
oheimb@2278
   237
        (cut_facts_tac prems 1),
oheimb@2278
   238
        (stac beta_cfun 1),
oheimb@2566
   239
	tac,
oheimb@2278
   240
        (stac beta_cfun 1),
oheimb@2566
   241
	tac,
oheimb@2278
   242
        (stac (beta_cfun RS ext) 1),
oheimb@2566
   243
	tac,
oheimb@2278
   244
        (rtac thelub_up1a 1),
oheimb@2278
   245
        (atac 1),
oheimb@2278
   246
        (etac exE 1),
oheimb@2278
   247
        (etac exE 1),
oheimb@2278
   248
        (rtac exI 1),
oheimb@2278
   249
        (rtac exI 1),
oheimb@2278
   250
        (etac box_equals 1),
oheimb@2278
   251
        (rtac refl 1),
oheimb@2278
   252
        (simp_tac (Up0_ss addsimps [cont_Iup]) 1)
oheimb@2278
   253
        ]);
oheimb@2278
   254
oheimb@2278
   255
oheimb@2278
   256
slotosch@2640
   257
qed_goalw "thelub_up2b" thy [up_def,fup_def] 
oheimb@4721
   258
"[| chain(Y); ! i x. Y(i) ~= up`x |] ==> lub(range(Y)) = UU"
oheimb@2278
   259
 (fn prems =>
oheimb@2278
   260
        [
oheimb@2278
   261
        (cut_facts_tac prems 1),
oheimb@2278
   262
        (stac inst_up_pcpo 1),
oheimb@2278
   263
        (rtac thelub_up1b 1),
oheimb@2278
   264
        (atac 1),
oheimb@2278
   265
        (strip_tac 1),
oheimb@2278
   266
        (dtac spec 1),
oheimb@2278
   267
        (dtac spec 1),
oheimb@2278
   268
        (rtac swap 1),
oheimb@2278
   269
        (atac 1),
oheimb@2278
   270
        (dtac notnotD 1),
oheimb@2278
   271
        (etac box_equals 1),
oheimb@2278
   272
        (rtac refl 1),
oheimb@2278
   273
        (simp_tac (Up0_ss addsimps [cont_Iup]) 1)
oheimb@2278
   274
        ]);
oheimb@2278
   275
oheimb@2278
   276
wenzelm@3842
   277
qed_goal "up_lemma2" thy  " (? x. z = up`x) = (z~=UU)"
oheimb@2278
   278
 (fn prems =>
oheimb@2278
   279
        [
oheimb@2278
   280
        (rtac iffI 1),
oheimb@2278
   281
        (etac exE 1),
oheimb@2278
   282
        (hyp_subst_tac 1),
oheimb@2278
   283
        (rtac defined_up 1),
oheimb@2278
   284
        (res_inst_tac [("p","z")] upE1 1),
oheimb@2278
   285
        (etac notE 1),
oheimb@2278
   286
        (atac 1),
oheimb@2278
   287
        (etac exI 1)
oheimb@2278
   288
        ]);
oheimb@2278
   289
oheimb@2278
   290
slotosch@2640
   291
qed_goal "thelub_up2a_rev" thy  
oheimb@4721
   292
"[| chain(Y); lub(range(Y)) = up`x |] ==> ? i x. Y(i) = up`x"
oheimb@2278
   293
 (fn prems =>
oheimb@2278
   294
        [
oheimb@2278
   295
        (cut_facts_tac prems 1),
oheimb@2278
   296
        (rtac exE 1),
oheimb@2278
   297
        (rtac chain_UU_I_inverse2 1),
oheimb@2278
   298
        (rtac (up_lemma2 RS iffD1) 1),
oheimb@2278
   299
        (etac exI 1),
oheimb@2278
   300
        (rtac exI 1),
oheimb@2278
   301
        (rtac (up_lemma2 RS iffD2) 1),
oheimb@2278
   302
        (atac 1)
oheimb@2278
   303
        ]);
oheimb@2278
   304
slotosch@2640
   305
qed_goal "thelub_up2b_rev" thy  
oheimb@4721
   306
"[| chain(Y); lub(range(Y)) = UU |] ==> ! i x.  Y(i) ~= up`x"
oheimb@2278
   307
 (fn prems =>
oheimb@2278
   308
        [
oheimb@2278
   309
        (cut_facts_tac prems 1),
oheimb@2278
   310
        (rtac allI 1),
oheimb@2278
   311
        (rtac (not_ex RS iffD1) 1),
oheimb@2278
   312
        (rtac contrapos 1),
oheimb@2278
   313
        (etac (up_lemma2 RS iffD1) 2),
oheimb@2278
   314
        (fast_tac (HOL_cs addSDs [chain_UU_I RS spec]) 1)
oheimb@2278
   315
        ]);
oheimb@2278
   316
oheimb@2278
   317
slotosch@2640
   318
qed_goal "thelub_up3" thy  
oheimb@4721
   319
"chain(Y) ==> lub(range(Y)) = UU |\
wenzelm@3842
   320
\                lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))"
oheimb@2278
   321
 (fn prems =>
oheimb@2278
   322
        [
oheimb@2278
   323
        (cut_facts_tac prems 1),
oheimb@2278
   324
        (rtac disjE 1),
oheimb@2278
   325
        (rtac disjI1 2),
oheimb@2278
   326
        (rtac thelub_up2b 2),
oheimb@2278
   327
        (atac 2),
oheimb@2278
   328
        (atac 2),
oheimb@2278
   329
        (rtac disjI2 2),
oheimb@2278
   330
        (rtac thelub_up2a 2),
oheimb@2278
   331
        (atac 2),
oheimb@2278
   332
        (atac 2),
oheimb@2278
   333
        (fast_tac HOL_cs 1)
oheimb@2278
   334
        ]);
oheimb@2278
   335
slotosch@2640
   336
qed_goal "fup3" thy "fup`up`x=x"
oheimb@2278
   337
 (fn prems =>
oheimb@2278
   338
        [
oheimb@2278
   339
        (res_inst_tac [("p","x")] upE1 1),
wenzelm@4098
   340
        (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1),
wenzelm@4098
   341
        (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1)
oheimb@2278
   342
        ]);
oheimb@2278
   343
oheimb@2278
   344
(* ------------------------------------------------------------------------ *)
oheimb@2278
   345
(* install simplifier for ('a)u                                             *)
oheimb@2278
   346
(* ------------------------------------------------------------------------ *)
oheimb@2278
   347
slotosch@3327
   348
Addsimps [fup1,fup2,defined_up];