src/HOLCF/Cfun3.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 5291 5706f0ef1d43
child 8820 a1297de19ec7
permissions -rw-r--r--
made tutorial first;
clasohm@1461
     1
(*  Title:      HOLCF/cfun3.ML
nipkow@243
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Franz Regensburger
nipkow@243
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@243
     5
*)
nipkow@243
     6
nipkow@243
     7
open Cfun3;
nipkow@243
     8
slotosch@2640
     9
(* for compatibility with old HOLCF-Version *)
slotosch@5291
    10
qed_goal "inst_cfun_pcpo" thy "UU = Abs_CFun(%x. UU)"
slotosch@2640
    11
 (fn prems => 
slotosch@2640
    12
        [
slotosch@2640
    13
        (simp_tac (HOL_ss addsimps [UU_def,UU_cfun_def]) 1)
slotosch@2640
    14
        ]);
slotosch@2640
    15
nipkow@243
    16
(* ------------------------------------------------------------------------ *)
slotosch@5291
    17
(* the contlub property for Rep_CFun its 'first' argument                       *)
nipkow@243
    18
(* ------------------------------------------------------------------------ *)
nipkow@243
    19
slotosch@5291
    20
qed_goal "contlub_Rep_CFun1" thy "contlub(Rep_CFun)"
nipkow@243
    21
(fn prems =>
clasohm@1461
    22
        [
clasohm@1461
    23
        (rtac contlubI 1),
clasohm@1461
    24
        (strip_tac 1),
clasohm@1461
    25
        (rtac (expand_fun_eq RS iffD2) 1),
clasohm@1461
    26
        (strip_tac 1),
paulson@2033
    27
        (stac thelub_cfun 1),
clasohm@1461
    28
        (atac 1),
paulson@2033
    29
        (stac Cfunapp2 1),
clasohm@1461
    30
        (etac cont_lubcfun 1),
paulson@2033
    31
        (stac thelub_fun 1),
slotosch@5291
    32
        (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1),
clasohm@1461
    33
        (rtac refl 1)
clasohm@1461
    34
        ]);
nipkow@243
    35
nipkow@243
    36
nipkow@243
    37
(* ------------------------------------------------------------------------ *)
slotosch@5291
    38
(* the cont property for Rep_CFun in its first argument                        *)
nipkow@243
    39
(* ------------------------------------------------------------------------ *)
nipkow@243
    40
slotosch@5291
    41
qed_goal "cont_Rep_CFun1" thy "cont(Rep_CFun)"
nipkow@243
    42
(fn prems =>
clasohm@1461
    43
        [
clasohm@1461
    44
        (rtac monocontlub2cont 1),
slotosch@5291
    45
        (rtac monofun_Rep_CFun1 1),
slotosch@5291
    46
        (rtac contlub_Rep_CFun1 1)
clasohm@1461
    47
        ]);
nipkow@243
    48
nipkow@243
    49
nipkow@243
    50
(* ------------------------------------------------------------------------ *)
slotosch@5291
    51
(* contlub, cont properties of Rep_CFun in its first argument in mixfix _[_]   *)
nipkow@243
    52
(* ------------------------------------------------------------------------ *)
nipkow@243
    53
slotosch@2640
    54
qed_goal "contlub_cfun_fun" thy 
oheimb@4721
    55
"chain(FY) ==>\
wenzelm@3842
    56
\ lub(range FY)`x = lub(range (%i. FY(i)`x))"
nipkow@243
    57
(fn prems =>
clasohm@1461
    58
        [
clasohm@1461
    59
        (cut_facts_tac prems 1),
clasohm@1461
    60
        (rtac trans 1),
slotosch@5291
    61
        (etac (contlub_Rep_CFun1 RS contlubE RS spec RS mp RS fun_cong) 1),
paulson@2033
    62
        (stac thelub_fun 1),
slotosch@5291
    63
        (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1),
clasohm@1461
    64
        (rtac refl 1)
clasohm@1461
    65
        ]);
nipkow@243
    66
nipkow@243
    67
slotosch@2640
    68
qed_goal "cont_cfun_fun" thy 
oheimb@4721
    69
"chain(FY) ==>\
wenzelm@3842
    70
\ range(%i. FY(i)`x) <<| lub(range FY)`x"
nipkow@243
    71
(fn prems =>
clasohm@1461
    72
        [
clasohm@1461
    73
        (cut_facts_tac prems 1),
clasohm@1461
    74
        (rtac thelubE 1),
slotosch@5291
    75
        (etac ch2ch_Rep_CFunL 1),
clasohm@1461
    76
        (etac (contlub_cfun_fun RS sym) 1)
clasohm@1461
    77
        ]);
nipkow@243
    78
nipkow@243
    79
nipkow@243
    80
(* ------------------------------------------------------------------------ *)
slotosch@5291
    81
(* contlub, cont  properties of Rep_CFun in both argument in mixfix _[_]       *)
nipkow@243
    82
(* ------------------------------------------------------------------------ *)
nipkow@243
    83
slotosch@2640
    84
qed_goal "contlub_cfun" thy 
oheimb@4721
    85
"[|chain(FY);chain(TY)|] ==>\
wenzelm@3842
    86
\ (lub(range FY))`(lub(range TY)) = lub(range(%i. FY(i)`(TY i)))"
nipkow@243
    87
(fn prems =>
clasohm@1461
    88
        [
clasohm@1461
    89
        (cut_facts_tac prems 1),
clasohm@1461
    90
        (rtac contlub_CF2 1),
slotosch@5291
    91
        (rtac cont_Rep_CFun1 1),
clasohm@1461
    92
        (rtac allI 1),
slotosch@5291
    93
        (rtac cont_Rep_CFun2 1),
clasohm@1461
    94
        (atac 1),
clasohm@1461
    95
        (atac 1)
clasohm@1461
    96
        ]);
nipkow@243
    97
slotosch@2640
    98
qed_goal "cont_cfun" thy 
oheimb@4721
    99
"[|chain(FY);chain(TY)|] ==>\
regensbu@1168
   100
\ range(%i.(FY i)`(TY i)) <<| (lub (range FY))`(lub(range TY))"
nipkow@243
   101
(fn prems =>
clasohm@1461
   102
        [
clasohm@1461
   103
        (cut_facts_tac prems 1),
clasohm@1461
   104
        (rtac thelubE 1),
slotosch@5291
   105
        (rtac (monofun_Rep_CFun1 RS ch2ch_MF2LR) 1),
clasohm@1461
   106
        (rtac allI 1),
slotosch@5291
   107
        (rtac monofun_Rep_CFun2 1),
clasohm@1461
   108
        (atac 1),
clasohm@1461
   109
        (atac 1),
clasohm@1461
   110
        (etac (contlub_cfun RS sym) 1),
clasohm@1461
   111
        (atac 1)
clasohm@1461
   112
        ]);
nipkow@243
   113
nipkow@243
   114
nipkow@243
   115
(* ------------------------------------------------------------------------ *)
slotosch@5291
   116
(* cont2cont lemma for Rep_CFun                                               *)
nipkow@243
   117
(* ------------------------------------------------------------------------ *)
nipkow@243
   118
slotosch@5291
   119
qed_goal "cont2cont_Rep_CFun" thy 
wenzelm@3842
   120
        "[|cont(%x. ft x);cont(%x. tt x)|] ==> cont(%x. (ft x)`(tt x))"
nipkow@243
   121
 (fn prems =>
clasohm@1461
   122
        [
clasohm@1461
   123
        (cut_facts_tac prems 1),
clasohm@1461
   124
        (rtac cont2cont_app2 1),
clasohm@1461
   125
        (rtac cont2cont_app2 1),
clasohm@1461
   126
        (rtac cont_const 1),
slotosch@5291
   127
        (rtac cont_Rep_CFun1 1),
clasohm@1461
   128
        (atac 1),
slotosch@5291
   129
        (rtac cont_Rep_CFun2 1),
clasohm@1461
   130
        (atac 1)
clasohm@1461
   131
        ]);
nipkow@243
   132
nipkow@243
   133
nipkow@243
   134
nipkow@243
   135
(* ------------------------------------------------------------------------ *)
regensbu@1168
   136
(* cont2mono Lemma for %x. LAM y. c1(x)(y)                                  *)
nipkow@243
   137
(* ------------------------------------------------------------------------ *)
nipkow@243
   138
slotosch@2640
   139
qed_goal "cont2mono_LAM" thy 
wenzelm@3842
   140
 "[| !!x. cont(c1 x); !!y. monofun(%x. c1 x y)|] ==> monofun(%x. LAM y. c1 x y)"
nipkow@2842
   141
(fn [p1,p2] =>
clasohm@1461
   142
        [
clasohm@1461
   143
        (rtac monofunI 1),
clasohm@1461
   144
        (strip_tac 1),
paulson@2033
   145
        (stac less_cfun 1),
paulson@2033
   146
        (stac less_fun 1),
clasohm@1461
   147
        (rtac allI 1),
paulson@2033
   148
        (stac beta_cfun 1),
nipkow@2842
   149
	(rtac p1 1),
paulson@2033
   150
        (stac beta_cfun 1),
nipkow@2842
   151
	(rtac p1 1),
nipkow@2842
   152
        (etac (p2 RS monofunE RS spec RS spec RS mp) 1)
clasohm@1461
   153
        ]);
nipkow@243
   154
nipkow@243
   155
(* ------------------------------------------------------------------------ *)
regensbu@1168
   156
(* cont2cont Lemma for %x. LAM y. c1 x y)                                 *)
nipkow@243
   157
(* ------------------------------------------------------------------------ *)
nipkow@243
   158
slotosch@2640
   159
qed_goal "cont2cont_LAM" thy 
wenzelm@3842
   160
 "[| !!x. cont(c1 x); !!y. cont(%x. c1 x y) |] ==> cont(%x. LAM y. c1 x y)"
nipkow@2842
   161
(fn [p1,p2] =>
clasohm@1461
   162
        [
clasohm@1461
   163
        (rtac monocontlub2cont 1),
nipkow@2842
   164
        (rtac (p1 RS cont2mono_LAM) 1),
nipkow@2842
   165
        (rtac (p2 RS cont2mono) 1),
clasohm@1461
   166
        (rtac contlubI 1),
clasohm@1461
   167
        (strip_tac 1),
paulson@2033
   168
        (stac thelub_cfun 1),
nipkow@2842
   169
        (rtac (p1 RS cont2mono_LAM RS ch2ch_monofun) 1),
nipkow@2842
   170
        (rtac (p2 RS cont2mono) 1),
clasohm@1461
   171
        (atac 1),
slotosch@5291
   172
        (res_inst_tac [("f","Abs_CFun")] arg_cong 1),
clasohm@1461
   173
        (rtac ext 1),
nipkow@2842
   174
        (stac (p1 RS beta_cfun RS ext) 1),
nipkow@2842
   175
        (etac (p2 RS cont2contlub RS contlubE RS spec RS mp) 1)
clasohm@1461
   176
        ]);
nipkow@243
   177
nipkow@243
   178
(* ------------------------------------------------------------------------ *)
regensbu@1168
   179
(* cont2cont tactic                                                       *)
nipkow@243
   180
(* ------------------------------------------------------------------------ *)
nipkow@243
   181
slotosch@5291
   182
val cont_lemmas1 = [cont_const, cont_id, cont_Rep_CFun2,
slotosch@5291
   183
                    cont2cont_Rep_CFun,cont2cont_LAM];
oheimb@2566
   184
oheimb@2566
   185
Addsimps cont_lemmas1;
nipkow@243
   186
oheimb@4004
   187
(* HINT: cont_tac is now installed in simplifier in Lift.ML ! *)
nipkow@243
   188
oheimb@2566
   189
(*val cont_tac = (fn i => (resolve_tac cont_lemmas i));*)
oheimb@2566
   190
(*val cont_tacR = (fn i => (REPEAT (cont_tac i)));*)
nipkow@243
   191
nipkow@243
   192
(* ------------------------------------------------------------------------ *)
nipkow@243
   193
(* function application _[_]  is strict in its first arguments              *)
nipkow@243
   194
(* ------------------------------------------------------------------------ *)
nipkow@243
   195
slotosch@5291
   196
qed_goal "strict_Rep_CFun1" thy "(UU::'a::cpo->'b)`x = (UU::'b)"
nipkow@243
   197
 (fn prems =>
clasohm@1461
   198
        [
paulson@2033
   199
        (stac inst_cfun_pcpo 1),
paulson@2033
   200
        (stac beta_cfun 1),
oheimb@2566
   201
        (Simp_tac 1),
clasohm@1461
   202
        (rtac refl 1)
clasohm@1461
   203
        ]);
nipkow@243
   204
nipkow@243
   205
nipkow@243
   206
(* ------------------------------------------------------------------------ *)
nipkow@243
   207
(* results about strictify                                                  *)
nipkow@243
   208
(* ------------------------------------------------------------------------ *)
nipkow@243
   209
slotosch@2640
   210
qed_goalw "Istrictify1" thy [Istrictify_def]
clasohm@1461
   211
        "Istrictify(f)(UU)= (UU)"
nipkow@243
   212
 (fn prems =>
clasohm@1461
   213
        [
clasohm@1461
   214
        (Simp_tac 1)
clasohm@1461
   215
        ]);
nipkow@243
   216
slotosch@2640
   217
qed_goalw "Istrictify2" thy [Istrictify_def]
clasohm@1461
   218
        "~x=UU ==> Istrictify(f)(x)=f`x"
nipkow@243
   219
 (fn prems =>
clasohm@1461
   220
        [
clasohm@1461
   221
        (cut_facts_tac prems 1),
clasohm@1461
   222
        (Asm_simp_tac 1)
clasohm@1461
   223
        ]);
nipkow@243
   224
slotosch@2640
   225
qed_goal "monofun_Istrictify1" thy "monofun(Istrictify)"
nipkow@243
   226
 (fn prems =>
clasohm@1461
   227
        [
clasohm@1461
   228
        (rtac monofunI 1),
clasohm@1461
   229
        (strip_tac 1),
clasohm@1461
   230
        (rtac (less_fun RS iffD2) 1),
clasohm@1461
   231
        (strip_tac 1),
clasohm@1461
   232
        (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1),
paulson@2033
   233
        (stac Istrictify2 1),
clasohm@1461
   234
        (atac 1),
paulson@2033
   235
        (stac Istrictify2 1),
clasohm@1461
   236
        (atac 1),
clasohm@1461
   237
        (rtac monofun_cfun_fun 1),
clasohm@1461
   238
        (atac 1),
clasohm@1461
   239
        (hyp_subst_tac 1),
paulson@2033
   240
        (stac Istrictify1 1),
paulson@2033
   241
        (stac Istrictify1 1),
clasohm@1461
   242
        (rtac refl_less 1)
clasohm@1461
   243
        ]);
nipkow@243
   244
slotosch@2640
   245
qed_goal "monofun_Istrictify2" thy "monofun(Istrictify(f))"
nipkow@243
   246
 (fn prems =>
clasohm@1461
   247
        [
clasohm@1461
   248
        (rtac monofunI 1),
clasohm@1461
   249
        (strip_tac 1),
clasohm@1461
   250
        (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
paulson@2033
   251
        (stac Istrictify2 1),
clasohm@1461
   252
        (etac notUU_I 1),
clasohm@1461
   253
        (atac 1),
paulson@2033
   254
        (stac Istrictify2 1),
clasohm@1461
   255
        (atac 1),
clasohm@1461
   256
        (rtac monofun_cfun_arg 1),
clasohm@1461
   257
        (atac 1),
clasohm@1461
   258
        (hyp_subst_tac 1),
paulson@2033
   259
        (stac Istrictify1 1),
clasohm@1461
   260
        (rtac minimal 1)
clasohm@1461
   261
        ]);
nipkow@243
   262
nipkow@243
   263
slotosch@2640
   264
qed_goal "contlub_Istrictify1" thy "contlub(Istrictify)"
nipkow@243
   265
 (fn prems =>
clasohm@1461
   266
        [
clasohm@1461
   267
        (rtac contlubI 1),
clasohm@1461
   268
        (strip_tac 1),
clasohm@1461
   269
        (rtac (expand_fun_eq RS iffD2) 1),
clasohm@1461
   270
        (strip_tac 1),
paulson@2033
   271
        (stac thelub_fun 1),
clasohm@1461
   272
        (etac (monofun_Istrictify1 RS ch2ch_monofun) 1),
clasohm@1461
   273
        (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
paulson@2033
   274
        (stac Istrictify2 1),
clasohm@1461
   275
        (atac 1),
paulson@2033
   276
        (stac (Istrictify2 RS ext) 1),
clasohm@1461
   277
        (atac 1),
paulson@2033
   278
        (stac thelub_cfun 1),
clasohm@1461
   279
        (atac 1),
paulson@2033
   280
        (stac beta_cfun 1),
clasohm@1461
   281
        (rtac cont_lubcfun 1),
clasohm@1461
   282
        (atac 1),
clasohm@1461
   283
        (rtac refl 1),
clasohm@1461
   284
        (hyp_subst_tac 1),
paulson@2033
   285
        (stac Istrictify1 1),
paulson@2033
   286
        (stac (Istrictify1 RS ext) 1),
clasohm@1461
   287
        (rtac (chain_UU_I_inverse RS sym) 1),
clasohm@1461
   288
        (rtac (refl RS allI) 1)
clasohm@1461
   289
        ]);
nipkow@243
   290
slotosch@2640
   291
qed_goal "contlub_Istrictify2" thy "contlub(Istrictify(f::'a -> 'b))"
nipkow@243
   292
 (fn prems =>
clasohm@1461
   293
        [
clasohm@1461
   294
        (rtac contlubI 1),
clasohm@1461
   295
        (strip_tac 1),
oheimb@1675
   296
        (case_tac "lub(range(Y))=(UU::'a)" 1),
clasohm@1461
   297
        (res_inst_tac [("t","lub(range(Y))")] subst 1),
clasohm@1461
   298
        (rtac sym 1),
clasohm@1461
   299
        (atac 1),
paulson@2033
   300
        (stac Istrictify1 1),
clasohm@1461
   301
        (rtac sym 1),
clasohm@1461
   302
        (rtac chain_UU_I_inverse 1),
clasohm@1461
   303
        (strip_tac 1),
clasohm@1461
   304
        (res_inst_tac [("t","Y(i)"),("s","UU::'a")] subst 1),
clasohm@1461
   305
        (rtac sym 1),
clasohm@1461
   306
        (rtac (chain_UU_I RS spec) 1),
clasohm@1461
   307
        (atac 1),
clasohm@1461
   308
        (atac 1),
clasohm@1461
   309
        (rtac Istrictify1 1),
paulson@2033
   310
        (stac Istrictify2 1),
clasohm@1461
   311
        (atac 1),
clasohm@1461
   312
        (res_inst_tac [("s","lub(range(%i. f`(Y i)))")] trans 1),
clasohm@1461
   313
        (rtac contlub_cfun_arg 1),
clasohm@1461
   314
        (atac 1),
clasohm@1461
   315
        (rtac lub_equal2 1),
clasohm@1461
   316
        (rtac (chain_mono2 RS exE) 1),
clasohm@1461
   317
        (atac 2),
clasohm@1461
   318
        (rtac chain_UU_I_inverse2 1),
clasohm@1461
   319
        (atac 1),
clasohm@1461
   320
        (rtac exI 1),
clasohm@1461
   321
        (strip_tac 1),
clasohm@1461
   322
        (rtac (Istrictify2 RS sym) 1),
clasohm@1461
   323
        (fast_tac HOL_cs 1),
clasohm@1461
   324
        (rtac ch2ch_monofun 1),
slotosch@5291
   325
        (rtac monofun_Rep_CFun2 1),
clasohm@1461
   326
        (atac 1),
clasohm@1461
   327
        (rtac ch2ch_monofun 1),
clasohm@1461
   328
        (rtac monofun_Istrictify2 1),
clasohm@1461
   329
        (atac 1)
clasohm@1461
   330
        ]);
nipkow@243
   331
nipkow@243
   332
oheimb@1779
   333
bind_thm ("cont_Istrictify1", contlub_Istrictify1 RS 
clasohm@1461
   334
        (monofun_Istrictify1 RS monocontlub2cont)); 
nipkow@243
   335
oheimb@1779
   336
bind_thm ("cont_Istrictify2", contlub_Istrictify2 RS 
clasohm@1461
   337
        (monofun_Istrictify2 RS monocontlub2cont)); 
nipkow@243
   338
nipkow@243
   339
slotosch@2640
   340
qed_goalw "strictify1" thy [strictify_def] "strictify`f`UU=UU" (fn _ => [
paulson@2033
   341
        (stac beta_cfun 1),
wenzelm@4098
   342
         (simp_tac (simpset() addsimps [cont_Istrictify2,cont_Istrictify1,
oheimb@2566
   343
					cont2cont_CF1L]) 1),
paulson@2033
   344
        (stac beta_cfun 1),
clasohm@1461
   345
        (rtac cont_Istrictify2 1),
clasohm@1461
   346
        (rtac Istrictify1 1)
clasohm@1461
   347
        ]);
nipkow@243
   348
slotosch@2640
   349
qed_goalw "strictify2" thy [strictify_def]
oheimb@2566
   350
        "~x=UU ==> strictify`f`x=f`x"  (fn prems => [
paulson@2033
   351
        (stac beta_cfun 1),
wenzelm@4098
   352
         (simp_tac (simpset() addsimps [cont_Istrictify2,cont_Istrictify1,
oheimb@2566
   353
					cont2cont_CF1L]) 1),
paulson@2033
   354
        (stac beta_cfun 1),
clasohm@1461
   355
        (rtac cont_Istrictify2 1),
clasohm@1461
   356
        (rtac Istrictify2 1),
clasohm@1461
   357
        (resolve_tac prems 1)
clasohm@1461
   358
        ]);
nipkow@243
   359
nipkow@243
   360
nipkow@243
   361
(* ------------------------------------------------------------------------ *)
nipkow@243
   362
(* Instantiate the simplifier                                               *)
nipkow@243
   363
(* ------------------------------------------------------------------------ *)
nipkow@243
   364
slotosch@5291
   365
Addsimps [minimal,refl_less,beta_cfun,strict_Rep_CFun1,strictify1, strictify2];
clasohm@1267
   366
nipkow@243
   367
nipkow@243
   368
(* ------------------------------------------------------------------------ *)
regensbu@1168
   369
(* use cont_tac as autotac.                                                *)
nipkow@243
   370
(* ------------------------------------------------------------------------ *)
nipkow@243
   371
oheimb@4004
   372
(* HINT: cont_tac is now installed in simplifier in Lift.ML ! *)
wenzelm@4098
   373
(*simpset_ref() := simpset() addsolver (K (DEPTH_SOLVE_1 o cont_tac));*)
slotosch@3326
   374
slotosch@3326
   375
(* ------------------------------------------------------------------------ *)
oheimb@4721
   376
(* some lemmata for functions with flat/chfin domain/range types	    *)
slotosch@3326
   377
(* ------------------------------------------------------------------------ *)
slotosch@3326
   378
slotosch@5291
   379
qed_goal "chfin_Rep_CFunR" thy 
oheimb@4721
   380
    "chain (Y::nat => 'a::cpo->'b::chfin)==> !s. ? n. lub(range(Y))`s = Y n`s" 
slotosch@3326
   381
(fn prems => 
slotosch@3326
   382
	[
slotosch@3326
   383
	cut_facts_tac prems 1,
slotosch@3326
   384
	rtac allI 1,
wenzelm@4423
   385
	stac contlub_cfun_fun 1,
slotosch@3326
   386
	 atac 1,
slotosch@5291
   387
	fast_tac (HOL_cs addSIs [thelubI,chfin,lub_finch2,chfin2finch,ch2ch_Rep_CFunL])1
slotosch@3326
   388
	]);
slotosch@3326
   389
slotosch@3326
   390
(* ------------------------------------------------------------------------ *)
slotosch@3326
   391
(* continuous isomorphisms are strict                                       *)
slotosch@3326
   392
(* a prove for embedding projection pairs is similar                        *)
slotosch@3326
   393
(* ------------------------------------------------------------------------ *)
slotosch@3326
   394
slotosch@3326
   395
qed_goal "iso_strict"  thy  
wenzelm@3842
   396
"!!f g.[|!y. f`(g`y)=(y::'b) ; !x. g`(f`x)=(x::'a) |] \
slotosch@3326
   397
\ ==> f`UU=UU & g`UU=UU"
slotosch@3326
   398
 (fn prems =>
slotosch@3326
   399
        [
slotosch@3326
   400
        (rtac conjI 1),
slotosch@3326
   401
        (rtac UU_I 1),
slotosch@3326
   402
        (res_inst_tac [("s","f`(g`(UU::'b))"),("t","UU::'b")] subst 1),
slotosch@3326
   403
        (etac spec 1),
slotosch@3326
   404
        (rtac (minimal RS monofun_cfun_arg) 1),
slotosch@3326
   405
        (rtac UU_I 1),
slotosch@3326
   406
        (res_inst_tac [("s","g`(f`(UU::'a))"),("t","UU::'a")] subst 1),
slotosch@3326
   407
        (etac spec 1),
slotosch@3326
   408
        (rtac (minimal RS monofun_cfun_arg) 1)
slotosch@3326
   409
        ]);
slotosch@3326
   410
slotosch@3326
   411
slotosch@3326
   412
qed_goal "isorep_defined" thy 
wenzelm@3842
   413
        "[|!x. rep`(abs`x)=x;!y. abs`(rep`y)=y; z~=UU|] ==> rep`z ~= UU"
slotosch@3326
   414
 (fn prems =>
slotosch@3326
   415
        [
slotosch@3326
   416
        (cut_facts_tac prems 1),
slotosch@3326
   417
        (etac swap 1),
slotosch@3326
   418
        (dtac notnotD 1),
slotosch@3326
   419
        (dres_inst_tac [("f","abs")] cfun_arg_cong 1),
slotosch@3326
   420
        (etac box_equals 1),
slotosch@3326
   421
        (fast_tac HOL_cs 1),
slotosch@3326
   422
        (etac (iso_strict RS conjunct1) 1),
slotosch@3326
   423
        (atac 1)
slotosch@3326
   424
        ]);
slotosch@3326
   425
slotosch@3326
   426
qed_goal "isoabs_defined" thy 
wenzelm@3842
   427
        "[|!x. rep`(abs`x) = x;!y. abs`(rep`y)=y ; z~=UU|] ==> abs`z ~= UU"
slotosch@3326
   428
 (fn prems =>
slotosch@3326
   429
        [
slotosch@3326
   430
        (cut_facts_tac prems 1),
slotosch@3326
   431
        (etac swap 1),
slotosch@3326
   432
        (dtac notnotD 1),
slotosch@3326
   433
        (dres_inst_tac [("f","rep")] cfun_arg_cong 1),
slotosch@3326
   434
        (etac box_equals 1),
slotosch@3326
   435
        (fast_tac HOL_cs 1),
slotosch@3326
   436
        (etac (iso_strict RS conjunct2) 1),
slotosch@3326
   437
        (atac 1)
slotosch@3326
   438
        ]);
slotosch@3326
   439
slotosch@3326
   440
(* ------------------------------------------------------------------------ *)
slotosch@3326
   441
(* propagation of flatness and chainfiniteness by continuous isomorphisms   *)
slotosch@3326
   442
(* ------------------------------------------------------------------------ *)
slotosch@3326
   443
oheimb@4721
   444
qed_goal "chfin2chfin" thy "!!f g.[|! Y::nat=>'a. chain Y --> (? n. max_in_chain n Y); \
wenzelm@3842
   445
\ !y. f`(g`y)=(y::'b) ; !x. g`(f`x)=(x::'a::chfin) |] \
oheimb@4721
   446
\ ==> ! Y::nat=>'b. chain Y --> (? n. max_in_chain n Y)"
slotosch@3326
   447
 (fn prems =>
slotosch@3326
   448
        [
slotosch@3326
   449
        (rewtac max_in_chain_def),
slotosch@3326
   450
        (strip_tac 1),
slotosch@3326
   451
        (rtac exE 1),
oheimb@4721
   452
        (res_inst_tac [("P","chain(%i. g`(Y i))")] mp 1),
slotosch@3326
   453
        (etac spec 1),
slotosch@5291
   454
        (etac ch2ch_Rep_CFunR 1),
slotosch@3326
   455
        (rtac exI 1),
slotosch@3326
   456
        (strip_tac 1),
slotosch@3326
   457
        (res_inst_tac [("s","f`(g`(Y x))"),("t","Y(x)")] subst 1),
slotosch@3326
   458
        (etac spec 1),
slotosch@3326
   459
        (res_inst_tac [("s","f`(g`(Y j))"),("t","Y(j)")] subst 1),
slotosch@3326
   460
        (etac spec 1),
slotosch@3326
   461
        (rtac cfun_arg_cong 1),
slotosch@3326
   462
        (rtac mp 1),
slotosch@3326
   463
        (etac spec 1),
slotosch@3326
   464
        (atac 1)
slotosch@3326
   465
        ]);
slotosch@3326
   466
slotosch@3326
   467
wenzelm@3842
   468
qed_goal "flat2flat" thy "!!f g.[|!x y::'a. x<<y --> x=UU | x=y; \
wenzelm@3842
   469
\ !y. f`(g`y)=(y::'b); !x. g`(f`x)=(x::'a)|] ==> !x y::'b. x<<y --> x=UU | x=y"
slotosch@3326
   470
 (fn prems =>
slotosch@3326
   471
        [
slotosch@3326
   472
        (strip_tac 1),
slotosch@3326
   473
        (rtac disjE 1),
slotosch@3326
   474
        (res_inst_tac [("P","g`x<<g`y")] mp 1),
slotosch@3326
   475
        (etac monofun_cfun_arg 2),
slotosch@3326
   476
        (dtac spec 1),
slotosch@3326
   477
        (etac spec 1),
slotosch@3326
   478
        (rtac disjI1 1),
slotosch@3326
   479
        (rtac trans 1),
slotosch@3326
   480
        (res_inst_tac [("s","f`(g`x)"),("t","x")] subst 1),
slotosch@3326
   481
        (etac spec 1),
slotosch@3326
   482
        (etac cfun_arg_cong 1),
slotosch@3326
   483
        (rtac (iso_strict RS conjunct1) 1),
slotosch@3326
   484
        (atac 1),
slotosch@3326
   485
        (atac 1),
slotosch@3326
   486
        (rtac disjI2 1),
slotosch@3326
   487
        (res_inst_tac [("s","f`(g`x)"),("t","x")] subst 1),
slotosch@3326
   488
        (etac spec 1),
slotosch@3326
   489
        (res_inst_tac [("s","f`(g`y)"),("t","y")] subst 1),
slotosch@3326
   490
        (etac spec 1),
slotosch@3326
   491
        (etac cfun_arg_cong 1)
slotosch@3326
   492
        ]);
slotosch@3326
   493
slotosch@3326
   494
(* ------------------------------------------------------------------------- *)
slotosch@3326
   495
(* a result about functions with flat codomain                               *)
slotosch@3326
   496
(* ------------------------------------------------------------------------- *)
slotosch@3326
   497
slotosch@3326
   498
qed_goal "flat_codom" thy 
wenzelm@3842
   499
"f`(x::'a)=(c::'b::flat) ==> f`(UU::'a)=(UU::'b) | (!z. f`(z::'a)=c)"
slotosch@3326
   500
 (fn prems =>
slotosch@3326
   501
        [
slotosch@3326
   502
        (cut_facts_tac prems 1),
slotosch@3326
   503
        (case_tac "f`(x::'a)=(UU::'b)" 1),
slotosch@3326
   504
        (rtac disjI1 1),
slotosch@3326
   505
        (rtac UU_I 1),
slotosch@3326
   506
        (res_inst_tac [("s","f`(x)"),("t","UU::'b")] subst 1),
slotosch@3326
   507
        (atac 1),
slotosch@3326
   508
        (rtac (minimal RS monofun_cfun_arg) 1),
slotosch@3326
   509
        (case_tac "f`(UU::'a)=(UU::'b)" 1),
slotosch@3326
   510
        (etac disjI1 1),
slotosch@3326
   511
        (rtac disjI2 1),
slotosch@3326
   512
        (rtac allI 1),
slotosch@3326
   513
        (hyp_subst_tac 1),
slotosch@3326
   514
        (res_inst_tac [("a","f`(UU::'a)")] (refl RS box_equals) 1),
slotosch@3326
   515
        (res_inst_tac [("fo5","f")] ((minimal RS monofun_cfun_arg) RS 
slotosch@3326
   516
		(ax_flat RS spec RS spec RS mp) RS disjE) 1),
slotosch@3326
   517
	(contr_tac 1),(atac 1),
slotosch@3326
   518
        (res_inst_tac [("fo5","f")] ((minimal RS monofun_cfun_arg) RS 
slotosch@3326
   519
		(ax_flat RS spec RS spec RS mp) RS disjE) 1),
slotosch@3326
   520
	(contr_tac 1),(atac 1)
slotosch@3326
   521
]);
slotosch@3326
   522
slotosch@3327
   523
slotosch@3327
   524
(* ------------------------------------------------------------------------ *)
slotosch@3327
   525
(* Access to definitions                                                    *)
slotosch@3327
   526
(* ------------------------------------------------------------------------ *)
slotosch@3327
   527
slotosch@3327
   528
slotosch@3327
   529
qed_goalw "ID1" thy [ID_def] "ID`x=x"
slotosch@3327
   530
 (fn prems =>
slotosch@3327
   531
        [
slotosch@3327
   532
        (stac beta_cfun 1),
slotosch@3327
   533
        (rtac cont_id 1),
slotosch@3327
   534
        (rtac refl 1)
slotosch@3327
   535
        ]);
slotosch@3327
   536
wenzelm@3842
   537
qed_goalw "cfcomp1" thy [oo_def] "(f oo g)=(LAM x. f`(g`x))" (fn _ => [
slotosch@3327
   538
        (stac beta_cfun 1),
slotosch@3327
   539
        (Simp_tac 1),
slotosch@3327
   540
        (stac beta_cfun 1),
slotosch@3327
   541
        (Simp_tac 1),
slotosch@3327
   542
	(rtac refl 1)
slotosch@3327
   543
        ]);
slotosch@3327
   544
slotosch@3327
   545
qed_goal "cfcomp2" thy  "(f oo g)`x=f`(g`x)" (fn _ => [
slotosch@3327
   546
        (stac cfcomp1 1),
slotosch@3327
   547
        (stac beta_cfun 1),
slotosch@3327
   548
        (Simp_tac 1),
slotosch@3327
   549
	(rtac refl 1)
slotosch@3327
   550
        ]);
slotosch@3327
   551
slotosch@3327
   552
slotosch@3327
   553
(* ------------------------------------------------------------------------ *)
slotosch@3327
   554
(* Show that interpretation of (pcpo,_->_) is a category                    *)
slotosch@3327
   555
(* The class of objects is interpretation of syntactical class pcpo         *)
slotosch@3327
   556
(* The class of arrows  between objects 'a and 'b is interpret. of 'a -> 'b *)
slotosch@3327
   557
(* The identity arrow is interpretation of ID                               *)
slotosch@3327
   558
(* The composition of f and g is interpretation of oo                       *)
slotosch@3327
   559
(* ------------------------------------------------------------------------ *)
slotosch@3327
   560
slotosch@3327
   561
slotosch@3327
   562
qed_goal "ID2" thy "f oo ID = f "
slotosch@3327
   563
 (fn prems =>
slotosch@3327
   564
        [
slotosch@3327
   565
        (rtac ext_cfun 1),
slotosch@3327
   566
        (stac cfcomp2 1),
slotosch@3327
   567
        (stac ID1 1),
slotosch@3327
   568
        (rtac refl 1)
slotosch@3327
   569
        ]);
slotosch@3327
   570
slotosch@3327
   571
qed_goal "ID3" thy "ID oo f = f "
slotosch@3327
   572
 (fn prems =>
slotosch@3327
   573
        [
slotosch@3327
   574
        (rtac ext_cfun 1),
slotosch@3327
   575
        (stac cfcomp2 1),
slotosch@3327
   576
        (stac ID1 1),
slotosch@3327
   577
        (rtac refl 1)
slotosch@3327
   578
        ]);
slotosch@3327
   579
slotosch@3327
   580
slotosch@3327
   581
qed_goal "assoc_oo" thy "f oo (g oo h) = (f oo g) oo h"
slotosch@3327
   582
 (fn prems =>
slotosch@3327
   583
        [
slotosch@3327
   584
        (rtac ext_cfun 1),
slotosch@3327
   585
        (res_inst_tac [("s","f`(g`(h`x))")] trans  1),
slotosch@3327
   586
        (stac cfcomp2 1),
slotosch@3327
   587
        (stac cfcomp2 1),
slotosch@3327
   588
        (rtac refl 1),
slotosch@3327
   589
        (stac cfcomp2 1),
slotosch@3327
   590
        (stac cfcomp2 1),
slotosch@3327
   591
        (rtac refl 1)
slotosch@3327
   592
        ]);
slotosch@3327
   593
slotosch@3327
   594
(* ------------------------------------------------------------------------ *)
slotosch@3327
   595
(* Merge the different rewrite rules for the simplifier                     *)
slotosch@3327
   596
(* ------------------------------------------------------------------------ *)
slotosch@3327
   597
slotosch@3327
   598
Addsimps ([ID1,ID2,ID3,cfcomp2]);
slotosch@3327
   599
slotosch@3327
   600