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