src/HOLCF/fix.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 300 3fb8c0256bec
permissions -rw-r--r--
made tutorial first;
nipkow@243
     1
(*  Title: 	HOLCF/fix.ML
nipkow@243
     2
    ID:         $Id$
nipkow@243
     3
    Author: 	Franz Regensburger
nipkow@243
     4
    Copyright   1993  Technische Universitaet Muenchen
nipkow@243
     5
nipkow@243
     6
Lemmas for fix.thy 
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
open Fix;
nipkow@243
    10
nipkow@243
    11
(* ------------------------------------------------------------------------ *)
nipkow@243
    12
(* derive inductive properties of iterate from primitive recursion          *)
nipkow@243
    13
(* ------------------------------------------------------------------------ *)
nipkow@243
    14
nipkow@243
    15
val iterate_0 = prove_goal Fix.thy "iterate(0,F,x) = x"
nipkow@243
    16
 (fn prems =>
nipkow@243
    17
	[
nipkow@243
    18
	(resolve_tac (nat_recs iterate_def) 1)
nipkow@243
    19
	]);
nipkow@243
    20
nipkow@243
    21
val iterate_Suc = prove_goal Fix.thy "iterate(Suc(n),F,x) = F[iterate(n,F,x)]"
nipkow@243
    22
 (fn prems =>
nipkow@243
    23
	[
nipkow@243
    24
	(resolve_tac (nat_recs iterate_def) 1)
nipkow@243
    25
	]);
nipkow@243
    26
nipkow@243
    27
val iterate_ss = Cfun_ss addsimps [iterate_0,iterate_Suc];
nipkow@243
    28
nipkow@243
    29
val iterate_Suc2 = prove_goal Fix.thy "iterate(Suc(n),F,x) = iterate(n,F,F[x])"
nipkow@243
    30
 (fn prems =>
nipkow@243
    31
	[
nipkow@243
    32
	(nat_ind_tac "n" 1),
nipkow@243
    33
	(simp_tac iterate_ss 1),
nipkow@243
    34
	(asm_simp_tac iterate_ss 1)
nipkow@243
    35
	]);
nipkow@243
    36
nipkow@243
    37
(* ------------------------------------------------------------------------ *)
nipkow@243
    38
(* the sequence of function itertaions is a chain                           *)
nipkow@243
    39
(* This property is essential since monotonicity of iterate makes no sense  *)
nipkow@243
    40
(* ------------------------------------------------------------------------ *)
nipkow@243
    41
nipkow@243
    42
val is_chain_iterate2 = prove_goalw Fix.thy [is_chain] 
nipkow@243
    43
	" x << F[x] ==> is_chain(%i.iterate(i,F,x))"
nipkow@243
    44
 (fn prems =>
nipkow@243
    45
	[
nipkow@243
    46
	(cut_facts_tac prems 1),
nipkow@243
    47
	(strip_tac 1),
nipkow@243
    48
	(simp_tac iterate_ss 1),
nipkow@243
    49
	(nat_ind_tac "i" 1),
nipkow@243
    50
	(asm_simp_tac iterate_ss 1),
nipkow@243
    51
	(asm_simp_tac iterate_ss 1),
nipkow@243
    52
	(etac monofun_cfun_arg 1)
nipkow@243
    53
	]);
nipkow@243
    54
nipkow@243
    55
nipkow@243
    56
val is_chain_iterate = prove_goal Fix.thy  
nipkow@243
    57
	"is_chain(%i.iterate(i,F,UU))"
nipkow@243
    58
 (fn prems =>
nipkow@243
    59
	[
nipkow@243
    60
	(rtac is_chain_iterate2 1),
nipkow@243
    61
	(rtac minimal 1)
nipkow@243
    62
	]);
nipkow@243
    63
nipkow@243
    64
nipkow@243
    65
(* ------------------------------------------------------------------------ *)
nipkow@243
    66
(* Kleene's fixed point theorems for continuous functions in pointed        *)
nipkow@243
    67
(* omega cpo's                                                              *)
nipkow@243
    68
(* ------------------------------------------------------------------------ *)
nipkow@243
    69
nipkow@243
    70
nipkow@243
    71
val Ifix_eq = prove_goalw Fix.thy  [Ifix_def] "Ifix(F)=F[Ifix(F)]"
nipkow@243
    72
 (fn prems =>
nipkow@243
    73
	[
nipkow@243
    74
	(rtac (contlub_cfun_arg RS ssubst) 1),
nipkow@243
    75
	(rtac is_chain_iterate 1),
nipkow@243
    76
	(rtac antisym_less 1),
nipkow@243
    77
	(rtac lub_mono 1),
nipkow@243
    78
	(rtac is_chain_iterate 1),
nipkow@243
    79
	(rtac ch2ch_fappR 1),
nipkow@243
    80
	(rtac is_chain_iterate 1),
nipkow@243
    81
	(rtac allI 1),
nipkow@243
    82
	(rtac (iterate_Suc RS subst) 1),
nipkow@243
    83
	(rtac (is_chain_iterate RS is_chainE RS spec) 1),
nipkow@243
    84
	(rtac is_lub_thelub 1),
nipkow@243
    85
	(rtac ch2ch_fappR 1),
nipkow@243
    86
	(rtac is_chain_iterate 1),
nipkow@243
    87
	(rtac ub_rangeI 1),
nipkow@243
    88
	(rtac allI 1),
nipkow@243
    89
	(rtac (iterate_Suc RS subst) 1),
nipkow@243
    90
	(rtac is_ub_thelub 1),
nipkow@243
    91
	(rtac is_chain_iterate 1)
nipkow@243
    92
	]);
nipkow@243
    93
nipkow@243
    94
nipkow@243
    95
val Ifix_least = prove_goalw Fix.thy [Ifix_def] "F[x]=x ==> Ifix(F) << x"
nipkow@243
    96
 (fn prems =>
nipkow@243
    97
	[
nipkow@243
    98
	(cut_facts_tac prems 1),
nipkow@243
    99
	(rtac is_lub_thelub 1),
nipkow@243
   100
	(rtac is_chain_iterate 1),
nipkow@243
   101
	(rtac ub_rangeI 1),
nipkow@243
   102
	(strip_tac 1),
nipkow@243
   103
	(nat_ind_tac "i" 1),
nipkow@243
   104
	(asm_simp_tac iterate_ss 1),
nipkow@243
   105
	(asm_simp_tac iterate_ss 1),
nipkow@243
   106
	(res_inst_tac [("t","x")] subst 1),
nipkow@243
   107
	(atac 1),
nipkow@243
   108
	(etac monofun_cfun_arg 1)
nipkow@243
   109
	]);
nipkow@243
   110
nipkow@243
   111
nipkow@243
   112
(* ------------------------------------------------------------------------ *)
nipkow@243
   113
(* monotonicity and continuity of iterate                                   *)
nipkow@243
   114
(* ------------------------------------------------------------------------ *)
nipkow@243
   115
nipkow@243
   116
val monofun_iterate = prove_goalw Fix.thy  [monofun] "monofun(iterate(i))"
nipkow@243
   117
 (fn prems =>
nipkow@243
   118
	[
nipkow@243
   119
	(strip_tac 1),
nipkow@243
   120
	(nat_ind_tac "i" 1),
nipkow@243
   121
	(asm_simp_tac iterate_ss 1),
nipkow@243
   122
	(asm_simp_tac iterate_ss 1),
nipkow@243
   123
	(rtac (less_fun RS iffD2) 1),
nipkow@243
   124
	(rtac allI 1),
nipkow@243
   125
	(rtac monofun_cfun 1),
nipkow@243
   126
	(atac 1),
nipkow@243
   127
	(rtac (less_fun RS iffD1 RS spec) 1),
nipkow@243
   128
	(atac 1)
nipkow@243
   129
	]);
nipkow@243
   130
nipkow@243
   131
(* ------------------------------------------------------------------------ *)
nipkow@243
   132
(* the following lemma uses contlub_cfun which itself is based on a         *)
nipkow@243
   133
(* diagonalisation lemma for continuous functions with two arguments.       *)
nipkow@243
   134
(* In this special case it is the application function fapp                 *)
nipkow@243
   135
(* ------------------------------------------------------------------------ *)
nipkow@243
   136
nipkow@243
   137
val contlub_iterate = prove_goalw Fix.thy  [contlub] "contlub(iterate(i))"
nipkow@243
   138
 (fn prems =>
nipkow@243
   139
	[
nipkow@243
   140
	(strip_tac 1),
nipkow@243
   141
	(nat_ind_tac "i" 1),
nipkow@243
   142
	(asm_simp_tac iterate_ss 1),
nipkow@243
   143
	(rtac (lub_const RS thelubI RS sym) 1),
nipkow@243
   144
	(asm_simp_tac iterate_ss 1),
nipkow@243
   145
	(rtac ext 1),
nipkow@243
   146
	(rtac (thelub_fun RS ssubst) 1),
nipkow@243
   147
	(rtac is_chainI 1),
nipkow@243
   148
	(rtac allI 1),
nipkow@243
   149
	(rtac (less_fun RS iffD2) 1),
nipkow@243
   150
	(rtac allI 1),
nipkow@243
   151
	(rtac (is_chainE RS spec) 1),
nipkow@243
   152
	(rtac (monofun_fapp1 RS ch2ch_MF2LR) 1),
nipkow@243
   153
	(rtac allI 1),
nipkow@243
   154
	(rtac monofun_fapp2 1),
nipkow@243
   155
	(atac 1),
nipkow@243
   156
	(rtac ch2ch_fun 1),
nipkow@243
   157
	(rtac (monofun_iterate RS ch2ch_monofun) 1),
nipkow@243
   158
	(atac 1),
nipkow@243
   159
	(rtac (thelub_fun RS ssubst) 1),
nipkow@243
   160
	(rtac (monofun_iterate RS ch2ch_monofun) 1),
nipkow@243
   161
	(atac 1),
nipkow@243
   162
	(rtac contlub_cfun  1),
nipkow@243
   163
	(atac 1),
nipkow@243
   164
	(etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun) 1)
nipkow@243
   165
	]);
nipkow@243
   166
nipkow@243
   167
nipkow@243
   168
val contX_iterate = prove_goal Fix.thy "contX(iterate(i))"
nipkow@243
   169
 (fn prems =>
nipkow@243
   170
	[
nipkow@243
   171
	(rtac monocontlub2contX 1),
nipkow@243
   172
	(rtac monofun_iterate 1),
nipkow@243
   173
	(rtac contlub_iterate 1)
nipkow@243
   174
	]);
nipkow@243
   175
nipkow@243
   176
(* ------------------------------------------------------------------------ *)
nipkow@243
   177
(* a lemma about continuity of iterate in its third argument                *)
nipkow@243
   178
(* ------------------------------------------------------------------------ *)
nipkow@243
   179
nipkow@243
   180
val monofun_iterate2 = prove_goal Fix.thy "monofun(iterate(n,F))"
nipkow@243
   181
 (fn prems =>
nipkow@243
   182
	[
nipkow@243
   183
	(rtac monofunI 1),
nipkow@243
   184
	(strip_tac 1),
nipkow@243
   185
	(nat_ind_tac "n" 1),
nipkow@243
   186
	(asm_simp_tac iterate_ss 1),
nipkow@243
   187
	(asm_simp_tac iterate_ss 1),
nipkow@243
   188
	(etac monofun_cfun_arg 1)
nipkow@243
   189
	]);
nipkow@243
   190
nipkow@243
   191
val contlub_iterate2 = prove_goal Fix.thy "contlub(iterate(n,F))"
nipkow@243
   192
 (fn prems =>
nipkow@243
   193
	[
nipkow@243
   194
	(rtac contlubI 1),
nipkow@243
   195
	(strip_tac 1),
nipkow@243
   196
	(nat_ind_tac "n" 1),
nipkow@243
   197
	(simp_tac iterate_ss 1),
nipkow@243
   198
	(simp_tac iterate_ss 1),
nipkow@243
   199
	(res_inst_tac [("t","iterate(n1, F, lub(range(%u. Y(u))))"),
nipkow@243
   200
	("s","lub(range(%i. iterate(n1, F, Y(i))))")] ssubst 1),
nipkow@243
   201
	(atac 1),
nipkow@243
   202
	(rtac contlub_cfun_arg 1),
nipkow@243
   203
	(etac (monofun_iterate2 RS ch2ch_monofun) 1)
nipkow@243
   204
	]);
nipkow@243
   205
nipkow@243
   206
val contX_iterate2 = prove_goal Fix.thy "contX(iterate(n,F))"
nipkow@243
   207
 (fn prems =>
nipkow@243
   208
	[
nipkow@243
   209
	(rtac monocontlub2contX 1),
nipkow@243
   210
	(rtac monofun_iterate2 1),
nipkow@243
   211
	(rtac contlub_iterate2 1)
nipkow@243
   212
	]);
nipkow@243
   213
nipkow@243
   214
(* ------------------------------------------------------------------------ *)
nipkow@243
   215
(* monotonicity and continuity of Ifix                                      *)
nipkow@243
   216
(* ------------------------------------------------------------------------ *)
nipkow@243
   217
nipkow@243
   218
val monofun_Ifix = prove_goalw Fix.thy  [monofun,Ifix_def] "monofun(Ifix)"
nipkow@243
   219
 (fn prems =>
nipkow@243
   220
	[
nipkow@243
   221
	(strip_tac 1),
nipkow@243
   222
	(rtac lub_mono 1),
nipkow@243
   223
	(rtac is_chain_iterate 1),
nipkow@243
   224
	(rtac is_chain_iterate 1),
nipkow@243
   225
	(rtac allI 1),
nipkow@243
   226
	(rtac (less_fun RS iffD1 RS spec) 1),
nipkow@243
   227
	(etac (monofun_iterate RS monofunE RS spec RS spec RS mp) 1)
nipkow@243
   228
	]);
nipkow@243
   229
nipkow@243
   230
nipkow@243
   231
(* ------------------------------------------------------------------------ *)
nipkow@243
   232
(* since iterate is not monotone in its first argument, special lemmas must *)
nipkow@243
   233
(* be derived for lubs in this argument                                     *)
nipkow@243
   234
(* ------------------------------------------------------------------------ *)
nipkow@243
   235
nipkow@243
   236
val is_chain_iterate_lub = prove_goal Fix.thy   
nipkow@243
   237
"is_chain(Y) ==> is_chain(%i. lub(range(%ia. iterate(ia,Y(i),UU))))"
nipkow@243
   238
 (fn prems =>
nipkow@243
   239
	[
nipkow@243
   240
	(cut_facts_tac prems 1),
nipkow@243
   241
	(rtac is_chainI 1),
nipkow@243
   242
	(strip_tac 1),
nipkow@243
   243
	(rtac lub_mono 1),
nipkow@243
   244
	(rtac is_chain_iterate 1),
nipkow@243
   245
	(rtac is_chain_iterate 1),
nipkow@243
   246
	(strip_tac 1),
nipkow@243
   247
	(etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun RS is_chainE 
nipkow@243
   248
         RS spec) 1)
nipkow@243
   249
	]);
nipkow@243
   250
nipkow@243
   251
(* ------------------------------------------------------------------------ *)
nipkow@243
   252
(* this exchange lemma is analog to the one for monotone functions          *)
nipkow@243
   253
(* observe that monotonicity is not really needed. The propagation of       *)
nipkow@243
   254
(* chains is the essential argument which is usually derived from monot.    *)
nipkow@243
   255
(* ------------------------------------------------------------------------ *)
nipkow@243
   256
nipkow@243
   257
val contlub_Ifix_lemma1 = prove_goal Fix.thy 
nipkow@243
   258
"is_chain(Y) ==> iterate(n,lub(range(Y)),y) = lub(range(%i. iterate(n,Y(i),y)))"
nipkow@243
   259
 (fn prems =>
nipkow@243
   260
	[
nipkow@243
   261
	(cut_facts_tac prems 1),
nipkow@243
   262
	(rtac (thelub_fun RS subst) 1),
nipkow@243
   263
	(rtac (monofun_iterate RS ch2ch_monofun) 1),
nipkow@243
   264
	(atac 1),
nipkow@243
   265
	(rtac fun_cong 1),
nipkow@243
   266
	(rtac (contlub_iterate RS contlubE RS spec RS mp RS ssubst) 1),
nipkow@243
   267
	(atac 1),
nipkow@243
   268
	(rtac refl 1)
nipkow@243
   269
	]);
nipkow@243
   270
nipkow@243
   271
nipkow@243
   272
val ex_lub_iterate = prove_goal Fix.thy  "is_chain(Y) ==>\
nipkow@243
   273
\         lub(range(%i. lub(range(%ia. iterate(i,Y(ia),UU))))) =\
nipkow@243
   274
\         lub(range(%i. lub(range(%ia. iterate(ia,Y(i),UU)))))"
nipkow@243
   275
 (fn prems =>
nipkow@243
   276
	[
nipkow@243
   277
	(cut_facts_tac prems 1),
nipkow@243
   278
	(rtac antisym_less 1),
nipkow@243
   279
	(rtac is_lub_thelub 1),
nipkow@243
   280
	(rtac (contlub_Ifix_lemma1 RS ext RS subst) 1),
nipkow@243
   281
	(atac 1),
nipkow@243
   282
	(rtac is_chain_iterate 1),
nipkow@243
   283
	(rtac ub_rangeI 1),
nipkow@243
   284
	(strip_tac 1),
nipkow@243
   285
	(rtac lub_mono 1),
nipkow@243
   286
	(etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun) 1),
nipkow@243
   287
	(etac is_chain_iterate_lub 1),
nipkow@243
   288
	(strip_tac 1),
nipkow@243
   289
	(rtac is_ub_thelub 1),
nipkow@243
   290
	(rtac is_chain_iterate 1),
nipkow@243
   291
	(rtac is_lub_thelub 1),
nipkow@243
   292
	(etac is_chain_iterate_lub 1),
nipkow@243
   293
	(rtac ub_rangeI 1),
nipkow@243
   294
	(strip_tac 1),
nipkow@243
   295
	(rtac lub_mono 1),
nipkow@243
   296
	(rtac is_chain_iterate 1),
nipkow@243
   297
	(rtac (contlub_Ifix_lemma1 RS ext RS subst) 1),
nipkow@243
   298
	(atac 1),
nipkow@243
   299
	(rtac is_chain_iterate 1),
nipkow@243
   300
	(strip_tac 1),
nipkow@243
   301
	(rtac is_ub_thelub 1),
nipkow@243
   302
	(etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun) 1)
nipkow@243
   303
	]);
nipkow@243
   304
nipkow@243
   305
nipkow@243
   306
val contlub_Ifix = prove_goalw Fix.thy  [contlub,Ifix_def] "contlub(Ifix)"
nipkow@243
   307
 (fn prems =>
nipkow@243
   308
	[
nipkow@243
   309
	(strip_tac 1),
nipkow@243
   310
	(rtac (contlub_Ifix_lemma1 RS ext RS ssubst) 1),
nipkow@243
   311
	(atac 1),
nipkow@243
   312
	(etac ex_lub_iterate 1)
nipkow@243
   313
	]);
nipkow@243
   314
nipkow@243
   315
nipkow@243
   316
val contX_Ifix = prove_goal Fix.thy "contX(Ifix)"
nipkow@243
   317
 (fn prems =>
nipkow@243
   318
	[
nipkow@243
   319
	(rtac monocontlub2contX 1),
nipkow@243
   320
	(rtac monofun_Ifix 1),
nipkow@243
   321
	(rtac contlub_Ifix 1)
nipkow@243
   322
	]);
nipkow@243
   323
nipkow@243
   324
(* ------------------------------------------------------------------------ *)
nipkow@243
   325
(* propagate properties of Ifix to its continuous counterpart               *)
nipkow@243
   326
(* ------------------------------------------------------------------------ *)
nipkow@243
   327
nipkow@243
   328
val fix_eq = prove_goalw Fix.thy  [fix_def] "fix[F]=F[fix[F]]"
nipkow@243
   329
 (fn prems =>
nipkow@243
   330
	[
nipkow@243
   331
	(asm_simp_tac (Cfun_ss addsimps [contX_Ifix]) 1),
nipkow@243
   332
	(rtac Ifix_eq 1)
nipkow@243
   333
	]);
nipkow@243
   334
nipkow@243
   335
val fix_least = prove_goalw Fix.thy [fix_def] "F[x]=x ==> fix[F] << x"
nipkow@243
   336
 (fn prems =>
nipkow@243
   337
	[
nipkow@243
   338
	(cut_facts_tac prems 1),
nipkow@243
   339
	(asm_simp_tac (Cfun_ss addsimps [contX_Ifix]) 1),
nipkow@243
   340
	(etac Ifix_least 1)
nipkow@243
   341
	]);
nipkow@243
   342
nipkow@243
   343
nipkow@243
   344
val fix_eq2 = prove_goal Fix.thy "f == fix[F] ==> f = F[f]"
nipkow@243
   345
 (fn prems =>
nipkow@243
   346
	[
nipkow@243
   347
	(rewrite_goals_tac prems),
nipkow@243
   348
	(rtac fix_eq 1)
nipkow@243
   349
	]);
nipkow@243
   350
nipkow@243
   351
val fix_eq3 = prove_goal Fix.thy "f == fix[F] ==> f[x] = F[f][x]"
nipkow@243
   352
 (fn prems =>
nipkow@243
   353
	[
nipkow@243
   354
	(rtac trans 1),
nipkow@243
   355
	(rtac ((hd prems) RS fix_eq2 RS cfun_fun_cong) 1),
nipkow@243
   356
	(rtac refl 1)
nipkow@243
   357
	]);
nipkow@243
   358
nipkow@243
   359
fun fix_tac3 thm i  = ((rtac trans i) THEN (rtac (thm RS fix_eq3) i)); 
nipkow@243
   360
nipkow@243
   361
val fix_eq4 = prove_goal Fix.thy "f = fix[F] ==> f = F[f]"
nipkow@243
   362
 (fn prems =>
nipkow@243
   363
	[
nipkow@243
   364
	(cut_facts_tac prems 1),
nipkow@243
   365
	(hyp_subst_tac 1),
nipkow@243
   366
	(rtac fix_eq 1)
nipkow@243
   367
	]);
nipkow@243
   368
nipkow@243
   369
val fix_eq5 = prove_goal Fix.thy "f = fix[F] ==> f[x] = F[f][x]"
nipkow@243
   370
 (fn prems =>
nipkow@243
   371
	[
nipkow@243
   372
	(rtac trans 1),
nipkow@243
   373
	(rtac ((hd prems) RS fix_eq4 RS cfun_fun_cong) 1),
nipkow@243
   374
	(rtac refl 1)
nipkow@243
   375
	]);
nipkow@243
   376
nipkow@243
   377
fun fix_tac5 thm i  = ((rtac trans i) THEN (rtac (thm RS fix_eq5) i)); 
nipkow@243
   378
nipkow@243
   379
fun fix_prover thy fixdef thm = prove_goal thy thm
nipkow@243
   380
 (fn prems =>
nipkow@243
   381
        [
nipkow@243
   382
        (rtac trans 1),
nipkow@243
   383
        (rtac (fixdef RS fix_eq4) 1),
nipkow@243
   384
        (rtac trans 1),
nipkow@243
   385
        (rtac beta_cfun 1),
nipkow@243
   386
        (contX_tacR 1),
nipkow@243
   387
        (rtac refl 1)
nipkow@243
   388
        ]);
nipkow@243
   389
nipkow@297
   390
(* ------------------------------------------------------------------------ 
nipkow@297
   391
nipkow@297
   392
given the definition
nipkow@297
   393
nipkow@297
   394
smap_def
nipkow@297
   395
  "smap = fix[LAM h f s. stream_when[LAM x l.scons[f[x]][h[f][l]]][s]]"
nipkow@297
   396
nipkow@297
   397
use fix_prover for 
nipkow@297
   398
nipkow@297
   399
val smap_def2 = fix_prover Stream2.thy smap_def 
nipkow@297
   400
        "smap = (LAM f s. stream_when[LAM x l.scons[f[x]][smap[f][l]]][s])";
nipkow@297
   401
nipkow@297
   402
   ------------------------------------------------------------------------ *)
nipkow@243
   403
nipkow@243
   404
(* ------------------------------------------------------------------------ *)
nipkow@243
   405
(* better access to definitions                                             *)
nipkow@243
   406
(* ------------------------------------------------------------------------ *)
nipkow@243
   407
nipkow@243
   408
nipkow@243
   409
val Ifix_def2 = prove_goal Fix.thy "Ifix=(%x. lub(range(%i. iterate(i,x,UU))))"
nipkow@243
   410
 (fn prems =>
nipkow@243
   411
	[
nipkow@243
   412
	(rtac ext 1),
nipkow@243
   413
	(rewrite_goals_tac [Ifix_def]),
nipkow@243
   414
	(rtac refl 1)
nipkow@243
   415
	]);
nipkow@243
   416
nipkow@243
   417
(* ------------------------------------------------------------------------ *)
nipkow@243
   418
(* direct connection between fix and iteration without Ifix                 *)
nipkow@243
   419
(* ------------------------------------------------------------------------ *)
nipkow@243
   420
nipkow@243
   421
val fix_def2 = prove_goalw Fix.thy [fix_def]
nipkow@243
   422
 "fix[F] = lub(range(%i. iterate(i,F,UU)))"
nipkow@243
   423
 (fn prems =>
nipkow@243
   424
	[
nipkow@243
   425
	(fold_goals_tac [Ifix_def]),
nipkow@243
   426
	(asm_simp_tac (Cfun_ss addsimps [contX_Ifix]) 1)
nipkow@243
   427
	]);
nipkow@243
   428
nipkow@243
   429
nipkow@243
   430
(* ------------------------------------------------------------------------ *)
nipkow@243
   431
(* Lemmas about admissibility and fixed point induction                     *)
nipkow@243
   432
(* ------------------------------------------------------------------------ *)
nipkow@243
   433
nipkow@243
   434
(* ------------------------------------------------------------------------ *)
nipkow@243
   435
(* access to definitions                                                    *)
nipkow@243
   436
(* ------------------------------------------------------------------------ *)
nipkow@243
   437
nipkow@243
   438
val adm_def2 = prove_goalw Fix.thy [adm_def]
nipkow@243
   439
	"adm(P) = (!Y. is_chain(Y) --> (!i.P(Y(i))) --> P(lub(range(Y))))"
nipkow@243
   440
 (fn prems =>
nipkow@243
   441
	[
nipkow@243
   442
	(rtac refl 1)
nipkow@243
   443
	]);
nipkow@243
   444
nipkow@243
   445
val admw_def2 = prove_goalw Fix.thy [admw_def]
nipkow@243
   446
	"admw(P) = (!F.((!n.P(iterate(n,F,UU)))-->\
nipkow@243
   447
\			 P(lub(range(%i.iterate(i,F,UU))))))"
nipkow@243
   448
 (fn prems =>
nipkow@243
   449
	[
nipkow@243
   450
	(rtac refl 1)
nipkow@243
   451
	]);
nipkow@243
   452
nipkow@243
   453
(* ------------------------------------------------------------------------ *)
nipkow@243
   454
(* an admissible formula is also weak admissible                            *)
nipkow@243
   455
(* ------------------------------------------------------------------------ *)
nipkow@243
   456
nipkow@243
   457
val adm_impl_admw = prove_goalw  Fix.thy [admw_def] "adm(P)==>admw(P)"
nipkow@243
   458
 (fn prems =>
nipkow@243
   459
	[
nipkow@243
   460
	(cut_facts_tac prems 1),
nipkow@243
   461
	(strip_tac 1),
nipkow@243
   462
	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
nipkow@243
   463
	(atac 1),
nipkow@243
   464
	(rtac is_chain_iterate 1),
nipkow@243
   465
	(atac 1)
nipkow@243
   466
	]);
nipkow@243
   467
nipkow@243
   468
(* ------------------------------------------------------------------------ *)
nipkow@243
   469
(* fixed point induction                                                    *)
nipkow@243
   470
(* ------------------------------------------------------------------------ *)
nipkow@243
   471
nipkow@243
   472
val fix_ind = prove_goal  Fix.thy  
nipkow@243
   473
"[| adm(P);P(UU);!!x. P(x) ==> P(F[x])|] ==> P(fix[F])"
nipkow@243
   474
 (fn prems =>
nipkow@243
   475
	[
nipkow@243
   476
	(cut_facts_tac prems 1),
nipkow@243
   477
	(rtac (fix_def2 RS ssubst) 1),
nipkow@243
   478
	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
nipkow@243
   479
	(atac 1),
nipkow@243
   480
	(rtac is_chain_iterate 1),
nipkow@243
   481
	(rtac allI 1),
nipkow@243
   482
	(nat_ind_tac "i" 1),
nipkow@243
   483
	(rtac (iterate_0 RS ssubst) 1),
nipkow@243
   484
	(atac 1),
nipkow@243
   485
	(rtac (iterate_Suc RS ssubst) 1),
nipkow@243
   486
	(resolve_tac prems 1),
nipkow@243
   487
	(atac 1)
nipkow@243
   488
	]);
nipkow@243
   489
nipkow@243
   490
(* ------------------------------------------------------------------------ *)
nipkow@243
   491
(* computational induction for weak admissible formulae                     *)
nipkow@243
   492
(* ------------------------------------------------------------------------ *)
nipkow@243
   493
nipkow@243
   494
val wfix_ind = prove_goal  Fix.thy  
nipkow@243
   495
"[| admw(P); !n. P(iterate(n,F,UU))|] ==> P(fix[F])"
nipkow@243
   496
 (fn prems =>
nipkow@243
   497
	[
nipkow@243
   498
	(cut_facts_tac prems 1),
nipkow@243
   499
	(rtac (fix_def2 RS ssubst) 1),
nipkow@243
   500
	(rtac (admw_def2 RS iffD1 RS spec RS mp) 1),
nipkow@243
   501
	(atac 1),
nipkow@243
   502
	(rtac allI 1),
nipkow@243
   503
	(etac spec 1)
nipkow@243
   504
	]);
nipkow@243
   505
nipkow@243
   506
(* ------------------------------------------------------------------------ *)
nipkow@243
   507
(* for chain-finite (easy) types every formula is admissible                *)
nipkow@243
   508
(* ------------------------------------------------------------------------ *)
nipkow@243
   509
nipkow@243
   510
val adm_max_in_chain = prove_goalw  Fix.thy  [adm_def]
nipkow@243
   511
"!Y. is_chain(Y::nat=>'a) --> (? n.max_in_chain(n,Y)) ==> adm(P::'a=>bool)"
nipkow@243
   512
 (fn prems =>
nipkow@243
   513
	[
nipkow@243
   514
	(cut_facts_tac prems 1),
nipkow@243
   515
	(strip_tac 1),
nipkow@243
   516
	(rtac exE 1),
nipkow@243
   517
	(rtac mp 1),
nipkow@243
   518
	(etac spec 1),
nipkow@243
   519
	(atac 1),
nipkow@243
   520
	(rtac (lub_finch1 RS thelubI RS ssubst) 1),
nipkow@243
   521
	(atac 1),
nipkow@243
   522
	(atac 1),
nipkow@243
   523
	(etac spec 1)
nipkow@243
   524
	]);
nipkow@243
   525
nipkow@243
   526
nipkow@243
   527
val adm_chain_finite = prove_goalw  Fix.thy  [chain_finite_def]
nipkow@243
   528
	"chain_finite(x::'a) ==> adm(P::'a=>bool)"
nipkow@243
   529
 (fn prems =>
nipkow@243
   530
	[
nipkow@243
   531
	(cut_facts_tac prems 1),
nipkow@243
   532
	(etac adm_max_in_chain 1)
nipkow@243
   533
	]);
nipkow@243
   534
nipkow@243
   535
(* ------------------------------------------------------------------------ *)
nipkow@243
   536
(* flat types are chain_finite                                              *)
nipkow@243
   537
(* ------------------------------------------------------------------------ *)
nipkow@243
   538
nipkow@243
   539
val flat_imp_chain_finite = prove_goalw  Fix.thy  [flat_def,chain_finite_def]
nipkow@243
   540
	"flat(x::'a)==>chain_finite(x::'a)"
nipkow@243
   541
 (fn prems =>
nipkow@243
   542
	[
nipkow@243
   543
	(rewrite_goals_tac [max_in_chain_def]),
nipkow@243
   544
	(cut_facts_tac prems 1),
nipkow@243
   545
	(strip_tac 1),
nipkow@243
   546
	(res_inst_tac [("Q","!i.Y(i)=UU")] classical2 1),
nipkow@243
   547
	(res_inst_tac [("x","0")] exI 1),
nipkow@243
   548
	(strip_tac 1),
nipkow@243
   549
	(rtac trans 1),
nipkow@243
   550
	(etac spec 1),
nipkow@243
   551
	(rtac sym 1),
nipkow@243
   552
	(etac spec 1),
nipkow@243
   553
	(rtac (chain_mono2 RS exE) 1),
nipkow@243
   554
	(fast_tac HOL_cs 1),
nipkow@243
   555
	(atac 1),
nipkow@243
   556
	(res_inst_tac [("x","Suc(x)")] exI 1),
nipkow@243
   557
	(strip_tac 1),
nipkow@243
   558
	(rtac disjE 1),
nipkow@243
   559
	(atac 3),
nipkow@243
   560
	(rtac mp 1),
nipkow@243
   561
	(dtac spec 1),
nipkow@243
   562
	(etac spec 1),
nipkow@243
   563
	(etac (le_imp_less_or_eq RS disjE) 1),
nipkow@243
   564
	(etac (chain_mono RS mp) 1),
nipkow@243
   565
	(atac 1),
nipkow@243
   566
	(hyp_subst_tac 1),
nipkow@243
   567
	(rtac refl_less 1),
nipkow@243
   568
	(res_inst_tac [("P","Y(Suc(x)) = UU")] notE 1),
nipkow@243
   569
	(atac 2),
nipkow@243
   570
	(rtac mp 1),
nipkow@243
   571
	(etac spec 1),
nipkow@243
   572
	(asm_simp_tac nat_ss 1)
nipkow@243
   573
	]);
nipkow@243
   574
nipkow@243
   575
nipkow@243
   576
val adm_flat = flat_imp_chain_finite RS adm_chain_finite;
nipkow@243
   577
(* flat(?x::?'a) ==> adm(?P::?'a => bool) *)
nipkow@243
   578
nipkow@243
   579
val flat_void = prove_goalw Fix.thy [flat_def] "flat(UU::void)"
nipkow@243
   580
 (fn prems =>
nipkow@243
   581
	[
nipkow@243
   582
	(strip_tac 1),
nipkow@243
   583
	(rtac disjI1 1),
nipkow@243
   584
	(rtac unique_void2 1)
nipkow@243
   585
	]);
nipkow@243
   586
nipkow@243
   587
(* ------------------------------------------------------------------------ *)
nipkow@243
   588
(* continuous isomorphisms are strict                                       *)
nipkow@243
   589
(* a prove for embedding projection pairs is similar                        *)
nipkow@243
   590
(* ------------------------------------------------------------------------ *)
nipkow@243
   591
nipkow@243
   592
val iso_strict = prove_goal  Fix.thy  
nipkow@243
   593
"!!f g.[|!y.f[g[y]]=(y::'b) ; !x.g[f[x]]=(x::'a) |] \
nipkow@243
   594
\ ==> f[UU]=UU & g[UU]=UU"
nipkow@243
   595
 (fn prems =>
nipkow@243
   596
	[
nipkow@243
   597
	(rtac conjI 1),
nipkow@243
   598
	(rtac UU_I 1),
nipkow@243
   599
	(res_inst_tac [("s","f[g[UU::'b]]"),("t","UU::'b")] subst 1),
nipkow@243
   600
	(etac spec 1),
nipkow@243
   601
	(rtac (minimal RS monofun_cfun_arg) 1),
nipkow@243
   602
	(rtac UU_I 1),
nipkow@243
   603
	(res_inst_tac [("s","g[f[UU::'a]]"),("t","UU::'a")] subst 1),
nipkow@243
   604
	(etac spec 1),
nipkow@243
   605
	(rtac (minimal RS monofun_cfun_arg) 1)
nipkow@243
   606
	]);
nipkow@243
   607
nipkow@243
   608
nipkow@243
   609
val isorep_defined = prove_goal Fix.thy 
nipkow@243
   610
	"[|!x.rep[abs[x]]=x;!y.abs[rep[y]]=y;z~=UU|] ==> rep[z]~=UU"
nipkow@243
   611
 (fn prems =>
nipkow@243
   612
	[
nipkow@243
   613
	(cut_facts_tac prems 1),
nipkow@243
   614
	(etac swap 1),
nipkow@243
   615
	(dtac notnotD 1),
nipkow@243
   616
	(dres_inst_tac [("f","abs")] cfun_arg_cong 1),
nipkow@243
   617
	(etac box_equals 1),
nipkow@243
   618
	(fast_tac HOL_cs 1),
nipkow@243
   619
	(etac (iso_strict RS conjunct1) 1),
nipkow@243
   620
	(atac 1)
nipkow@243
   621
	]);
nipkow@243
   622
nipkow@243
   623
val isoabs_defined = prove_goal Fix.thy 
nipkow@243
   624
	"[|!x.rep[abs[x]]=x;!y.abs[rep[y]]=y;z~=UU|] ==> abs[z]~=UU"
nipkow@243
   625
 (fn prems =>
nipkow@243
   626
	[
nipkow@243
   627
	(cut_facts_tac prems 1),
nipkow@243
   628
	(etac swap 1),
nipkow@243
   629
	(dtac notnotD 1),
nipkow@243
   630
	(dres_inst_tac [("f","rep")] cfun_arg_cong 1),
nipkow@243
   631
	(etac box_equals 1),
nipkow@243
   632
	(fast_tac HOL_cs 1),
nipkow@243
   633
	(etac (iso_strict RS conjunct2) 1),
nipkow@243
   634
	(atac 1)
nipkow@243
   635
	]);
nipkow@243
   636
nipkow@243
   637
(* ------------------------------------------------------------------------ *)
nipkow@243
   638
(* propagation of flatness and chainfiniteness by continuous isomorphisms   *)
nipkow@243
   639
(* ------------------------------------------------------------------------ *)
nipkow@243
   640
nipkow@243
   641
val chfin2chfin = prove_goalw  Fix.thy  [chain_finite_def]
nipkow@243
   642
"!!f g.[|chain_finite(x::'a); !y.f[g[y]]=(y::'b) ; !x.g[f[x]]=(x::'a) |] \
nipkow@243
   643
\ ==> chain_finite(y::'b)"
nipkow@243
   644
 (fn prems =>
nipkow@243
   645
	[
nipkow@243
   646
	(rewrite_goals_tac [max_in_chain_def]),
nipkow@243
   647
	(strip_tac 1),
nipkow@243
   648
	(rtac exE 1),
nipkow@243
   649
	(res_inst_tac [("P","is_chain(%i.g[Y(i)])")] mp 1),
nipkow@243
   650
	(etac spec 1),
nipkow@243
   651
	(etac ch2ch_fappR 1),
nipkow@243
   652
	(rtac exI 1),
nipkow@243
   653
	(strip_tac 1),
nipkow@243
   654
	(res_inst_tac [("s","f[g[Y(x)]]"),("t","Y(x)")] subst 1),
nipkow@243
   655
	(etac spec 1),
nipkow@243
   656
	(res_inst_tac [("s","f[g[Y(j)]]"),("t","Y(j)")] subst 1),
nipkow@243
   657
	(etac spec 1),
nipkow@243
   658
	(rtac cfun_arg_cong 1),
nipkow@243
   659
	(rtac mp 1),
nipkow@243
   660
	(etac spec 1),
nipkow@243
   661
	(atac 1)
nipkow@243
   662
	]);
nipkow@243
   663
nipkow@243
   664
val flat2flat = prove_goalw  Fix.thy  [flat_def]
nipkow@243
   665
"!!f g.[|flat(x::'a); !y.f[g[y]]=(y::'b) ; !x.g[f[x]]=(x::'a) |] \
nipkow@243
   666
\ ==> flat(y::'b)"
nipkow@243
   667
 (fn prems =>
nipkow@243
   668
	[
nipkow@243
   669
	(strip_tac 1),
nipkow@243
   670
	(rtac disjE 1),
nipkow@243
   671
	(res_inst_tac [("P","g[x]<<g[y]")] mp 1),
nipkow@243
   672
	(etac monofun_cfun_arg 2),
nipkow@243
   673
	(dtac spec 1),
nipkow@243
   674
	(etac spec 1),
nipkow@243
   675
	(rtac disjI1 1),
nipkow@243
   676
	(rtac trans 1),
nipkow@243
   677
	(res_inst_tac [("s","f[g[x]]"),("t","x")] subst 1),
nipkow@243
   678
	(etac spec 1),
nipkow@243
   679
	(etac cfun_arg_cong 1),
nipkow@243
   680
	(rtac (iso_strict RS conjunct1) 1),
nipkow@243
   681
	(atac 1),
nipkow@243
   682
	(atac 1),
nipkow@243
   683
	(rtac disjI2 1),
nipkow@243
   684
	(res_inst_tac [("s","f[g[x]]"),("t","x")] subst 1),
nipkow@243
   685
	(etac spec 1),
nipkow@243
   686
	(res_inst_tac [("s","f[g[y]]"),("t","y")] subst 1),
nipkow@243
   687
	(etac spec 1),
nipkow@243
   688
	(etac cfun_arg_cong 1)
nipkow@243
   689
	]);
nipkow@243
   690
nipkow@243
   691
(* ------------------------------------------------------------------------ *)
nipkow@243
   692
(* admissibility of special formulae and propagation                        *)
nipkow@243
   693
(* ------------------------------------------------------------------------ *)
nipkow@243
   694
nipkow@243
   695
val adm_less = prove_goalw  Fix.thy [adm_def]
nipkow@243
   696
	"[|contX(u);contX(v)|]==> adm(%x.u(x)<<v(x))"
nipkow@243
   697
 (fn prems =>
nipkow@243
   698
	[
nipkow@243
   699
	(cut_facts_tac prems 1),
nipkow@243
   700
	(strip_tac 1),
nipkow@243
   701
	(etac (contX2contlub RS contlubE RS spec RS mp RS ssubst) 1),
nipkow@243
   702
	(atac 1),
nipkow@243
   703
	(etac (contX2contlub RS contlubE RS spec RS mp RS ssubst) 1),
nipkow@243
   704
	(atac 1),
nipkow@243
   705
	(rtac lub_mono 1),
nipkow@243
   706
	(cut_facts_tac prems 1),
nipkow@243
   707
	(etac (contX2mono RS ch2ch_monofun) 1),
nipkow@243
   708
	(atac 1),
nipkow@243
   709
	(cut_facts_tac prems 1),
nipkow@243
   710
	(etac (contX2mono RS ch2ch_monofun) 1),
nipkow@243
   711
	(atac 1),
nipkow@243
   712
	(atac 1)
nipkow@243
   713
	]);
nipkow@243
   714
nipkow@243
   715
val adm_conj = prove_goal  Fix.thy  
nipkow@243
   716
	"[| adm(P); adm(Q) |] ==> adm(%x.P(x)&Q(x))"
nipkow@243
   717
 (fn prems =>
nipkow@243
   718
	[
nipkow@243
   719
	(cut_facts_tac prems 1),
nipkow@243
   720
	(rtac (adm_def2 RS iffD2) 1),
nipkow@243
   721
	(strip_tac 1),
nipkow@243
   722
	(rtac conjI 1),
nipkow@243
   723
	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
nipkow@243
   724
	(atac 1),
nipkow@243
   725
	(atac 1),
nipkow@243
   726
	(fast_tac HOL_cs 1),
nipkow@243
   727
	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
nipkow@243
   728
	(atac 1),
nipkow@243
   729
	(atac 1),
nipkow@243
   730
	(fast_tac HOL_cs 1)
nipkow@243
   731
	]);
nipkow@243
   732
nipkow@243
   733
val adm_cong = prove_goal  Fix.thy  
nipkow@243
   734
	"(!x. P(x) = Q(x)) ==> adm(P)=adm(Q)"
nipkow@243
   735
 (fn prems =>
nipkow@243
   736
	[
nipkow@243
   737
	(cut_facts_tac prems 1),
nipkow@243
   738
	(res_inst_tac [("s","P"),("t","Q")] subst 1),
nipkow@243
   739
	(rtac refl 2),
nipkow@243
   740
	(rtac ext 1),
nipkow@243
   741
	(etac spec 1)
nipkow@243
   742
	]);
nipkow@243
   743
nipkow@243
   744
val adm_not_free = prove_goalw  Fix.thy [adm_def] "adm(%x.t)"
nipkow@243
   745
 (fn prems =>
nipkow@243
   746
	[
nipkow@243
   747
	(fast_tac HOL_cs 1)
nipkow@243
   748
	]);
nipkow@243
   749
nipkow@243
   750
val adm_not_less = prove_goalw  Fix.thy [adm_def]
nipkow@243
   751
	"contX(t) ==> adm(%x.~ t(x) << u)"
nipkow@243
   752
 (fn prems =>
nipkow@243
   753
	[
nipkow@243
   754
	(cut_facts_tac prems 1),
nipkow@243
   755
	(strip_tac 1),
nipkow@243
   756
	(rtac contrapos 1),
nipkow@243
   757
	(etac spec 1),
nipkow@243
   758
	(rtac trans_less 1),
nipkow@243
   759
	(atac 2),
nipkow@243
   760
	(etac (contX2mono RS monofun_fun_arg) 1),
nipkow@243
   761
	(rtac is_ub_thelub 1),
nipkow@243
   762
	(atac 1)
nipkow@243
   763
	]);
nipkow@243
   764
nipkow@243
   765
val adm_all = prove_goal  Fix.thy  
nipkow@243
   766
	" !y.adm(P(y)) ==> adm(%x.!y.P(y,x))"
nipkow@243
   767
 (fn prems =>
nipkow@243
   768
	[
nipkow@243
   769
	(cut_facts_tac prems 1),
nipkow@243
   770
	(rtac (adm_def2 RS iffD2) 1),
nipkow@243
   771
	(strip_tac 1),
nipkow@243
   772
	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
nipkow@243
   773
	(etac spec 1),
nipkow@243
   774
	(atac 1),
nipkow@243
   775
	(rtac allI 1),
nipkow@243
   776
	(dtac spec 1),
nipkow@243
   777
	(etac spec 1)
nipkow@243
   778
	]);
nipkow@243
   779
nipkow@243
   780
val adm_subst = prove_goal  Fix.thy  
nipkow@243
   781
	"[|contX(t); adm(P)|] ==> adm(%x.P(t(x)))"
nipkow@243
   782
 (fn prems =>
nipkow@243
   783
	[
nipkow@243
   784
	(cut_facts_tac prems 1),
nipkow@243
   785
	(rtac (adm_def2 RS iffD2) 1),
nipkow@243
   786
	(strip_tac 1),
nipkow@243
   787
	(rtac (contX2contlub RS contlubE RS spec RS mp RS ssubst) 1),
nipkow@243
   788
	(atac 1),
nipkow@243
   789
	(atac 1),
nipkow@243
   790
	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
nipkow@243
   791
	(atac 1),
nipkow@243
   792
	(rtac (contX2mono RS ch2ch_monofun) 1),
nipkow@243
   793
	(atac 1),
nipkow@243
   794
	(atac 1),
nipkow@243
   795
	(atac 1)
nipkow@243
   796
	]);
nipkow@243
   797
nipkow@243
   798
val adm_UU_not_less = prove_goal  Fix.thy "adm(%x.~ UU << t(x))"
nipkow@243
   799
 (fn prems =>
nipkow@243
   800
	[
nipkow@243
   801
	(res_inst_tac [("P2","%x.False")] (adm_cong RS iffD1) 1),
nipkow@243
   802
	(asm_simp_tac Cfun_ss 1),
nipkow@243
   803
	(rtac adm_not_free 1)
nipkow@243
   804
	]);
nipkow@243
   805
nipkow@243
   806
val adm_not_UU = prove_goalw  Fix.thy [adm_def] 
nipkow@243
   807
	"contX(t)==> adm(%x.~ t(x) = UU)"
nipkow@243
   808
 (fn prems =>
nipkow@243
   809
	[
nipkow@243
   810
	(cut_facts_tac prems 1),
nipkow@243
   811
	(strip_tac 1),
nipkow@243
   812
	(rtac contrapos 1),
nipkow@243
   813
	(etac spec 1),
nipkow@243
   814
	(rtac (chain_UU_I RS spec) 1),
nipkow@243
   815
	(rtac (contX2mono RS ch2ch_monofun) 1),
nipkow@243
   816
	(atac 1),
nipkow@243
   817
	(atac 1),
nipkow@243
   818
	(rtac (contX2contlub RS contlubE RS spec RS mp RS subst) 1),
nipkow@243
   819
	(atac 1),
nipkow@243
   820
	(atac 1),
nipkow@243
   821
	(atac 1)
nipkow@243
   822
	]);
nipkow@243
   823
nipkow@243
   824
val adm_eq = prove_goal  Fix.thy 
nipkow@243
   825
	"[|contX(u);contX(v)|]==> adm(%x.u(x)= v(x))"
nipkow@243
   826
 (fn prems =>
nipkow@243
   827
	[
nipkow@243
   828
	(rtac (adm_cong RS iffD1) 1),
nipkow@243
   829
	(rtac allI 1),
nipkow@243
   830
	(rtac iffI 1),
nipkow@243
   831
	(rtac antisym_less 1),
nipkow@243
   832
	(rtac antisym_less_inverse 3),
nipkow@243
   833
	(atac 3),
nipkow@243
   834
	(etac conjunct1 1),
nipkow@243
   835
	(etac conjunct2 1),
nipkow@243
   836
	(rtac adm_conj 1),
nipkow@243
   837
	(rtac adm_less 1),
nipkow@243
   838
	(resolve_tac prems 1),
nipkow@243
   839
	(resolve_tac prems 1),
nipkow@243
   840
	(rtac adm_less 1),
nipkow@243
   841
	(resolve_tac prems 1),
nipkow@243
   842
	(resolve_tac prems 1)
nipkow@243
   843
	]);
nipkow@243
   844
nipkow@243
   845
nipkow@243
   846
(* ------------------------------------------------------------------------ *)
nipkow@243
   847
(* admissibility for disjunction is hard to prove. It takes 10 Lemmas       *)
nipkow@243
   848
(* ------------------------------------------------------------------------ *)
nipkow@243
   849
nipkow@243
   850
val adm_disj_lemma1 = prove_goal  Pcpo.thy 
nipkow@243
   851
"[| is_chain(Y); !n.P(Y(n))|Q(Y(n))|]\
nipkow@243
   852
\ ==> (? i.!j. i<j --> Q(Y(j))) | (!i.? j.i<j & P(Y(j)))"
nipkow@243
   853
 (fn prems =>
nipkow@243
   854
	[
nipkow@243
   855
	(cut_facts_tac prems 1),
nipkow@243
   856
	(fast_tac HOL_cs 1)
nipkow@243
   857
	]);
nipkow@243
   858
nipkow@243
   859
val adm_disj_lemma2 = prove_goal  Fix.thy  
nipkow@243
   860
"[| adm(Q); ? X.is_chain(X) & (!n.Q(X(n))) &\
nipkow@243
   861
\   lub(range(Y))=lub(range(X))|] ==> Q(lub(range(Y)))"
nipkow@243
   862
 (fn prems =>
nipkow@243
   863
	[
nipkow@243
   864
	(cut_facts_tac prems 1),
nipkow@243
   865
	(etac exE 1),
nipkow@243
   866
	(etac conjE 1),
nipkow@243
   867
	(etac conjE 1),
nipkow@243
   868
	(res_inst_tac [("s","lub(range(X))"),("t","lub(range(Y))")] ssubst 1),
nipkow@243
   869
	(atac 1),
nipkow@243
   870
	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
nipkow@243
   871
	(atac 1),
nipkow@243
   872
	(atac 1),
nipkow@243
   873
	(atac 1)
nipkow@243
   874
	]);
nipkow@243
   875
nipkow@243
   876
val adm_disj_lemma3 = prove_goal  Fix.thy
nipkow@243
   877
"[| is_chain(Y); ! j. i < j --> Q(Y(j)) |] ==>\
nipkow@243
   878
\         is_chain(%m. if(m < Suc(i),Y(Suc(i)),Y(m)))"
nipkow@243
   879
 (fn prems =>
nipkow@243
   880
	[
nipkow@243
   881
	(cut_facts_tac prems 1),
nipkow@243
   882
	(rtac is_chainI 1),
nipkow@243
   883
	(rtac allI 1),
nipkow@243
   884
	(res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1),
nipkow@243
   885
	(res_inst_tac [("s","False"),("t","ia < Suc(i)")] ssubst 1),
nipkow@243
   886
	(rtac iffI 1),
nipkow@243
   887
	(etac FalseE 2),
nipkow@243
   888
	(rtac notE 1),
nipkow@243
   889
	(rtac (not_less_eq RS iffD2) 1),
nipkow@243
   890
	(atac 1),
nipkow@243
   891
	(atac 1),
nipkow@243
   892
	(res_inst_tac [("s","False"),("t","Suc(ia) < Suc(i)")] ssubst 1),
nipkow@243
   893
	(asm_simp_tac nat_ss  1),
nipkow@243
   894
	(rtac iffI 1),
nipkow@243
   895
	(etac FalseE 2),
nipkow@243
   896
	(rtac notE 1),
nipkow@300
   897
	(etac less_not_sym 1),	
nipkow@243
   898
	(atac 1),
nipkow@243
   899
	(asm_simp_tac Cfun_ss  1),
nipkow@243
   900
	(etac (is_chainE RS spec) 1),
nipkow@243
   901
	(hyp_subst_tac 1),
nipkow@243
   902
	(asm_simp_tac nat_ss 1),
nipkow@243
   903
	(rtac refl_less 1),
nipkow@243
   904
	(asm_simp_tac nat_ss 1),
nipkow@243
   905
	(rtac refl_less 1)
nipkow@243
   906
	]);
nipkow@243
   907
nipkow@243
   908
val adm_disj_lemma4 = prove_goal  Fix.thy
nipkow@243
   909
"[| ! j. i < j --> Q(Y(j)) |] ==>\
nipkow@243
   910
\	 ! n. Q(if(n < Suc(i),Y(Suc(i)),Y(n)))"
nipkow@243
   911
 (fn prems =>
nipkow@243
   912
	[
nipkow@243
   913
	(cut_facts_tac prems 1),
nipkow@243
   914
	(rtac allI 1),
nipkow@243
   915
	(res_inst_tac [("m","n"),("n","Suc(i)")] nat_less_cases 1),
nipkow@243
   916
	(res_inst_tac[("s","Y(Suc(i))"),("t","if(n<Suc(i),Y(Suc(i)),Y(n))")]
nipkow@243
   917
		ssubst 1),
nipkow@243
   918
	(asm_simp_tac nat_ss 1),
nipkow@243
   919
	(etac allE 1),
nipkow@243
   920
	(rtac mp 1),
nipkow@243
   921
	(atac 1),
nipkow@243
   922
	(asm_simp_tac nat_ss 1),
nipkow@243
   923
	(res_inst_tac[("s","Y(n)"),("t","if(n<Suc(i),Y(Suc(i)),Y(n))")] 
nipkow@243
   924
		ssubst 1),
nipkow@243
   925
	(asm_simp_tac nat_ss 1),
nipkow@243
   926
	(hyp_subst_tac 1),
nipkow@243
   927
	(dtac spec 1),
nipkow@243
   928
	(rtac mp 1),
nipkow@243
   929
	(atac 1),
nipkow@243
   930
	(asm_simp_tac nat_ss 1),
nipkow@243
   931
	(res_inst_tac [("s","Y(n)"),("t","if(n < Suc(i),Y(Suc(i)),Y(n))")] 
nipkow@243
   932
		ssubst 1),
nipkow@243
   933
	(res_inst_tac [("s","False"),("t","n < Suc(i)")] ssubst 1),
nipkow@243
   934
	(rtac iffI 1),
nipkow@243
   935
	(etac FalseE 2),
nipkow@243
   936
	(rtac notE 1),
nipkow@300
   937
	(etac less_not_sym 1),	
nipkow@243
   938
	(atac 1),
nipkow@243
   939
	(asm_simp_tac nat_ss 1),
nipkow@243
   940
	(dtac spec 1),
nipkow@243
   941
	(rtac mp 1),
nipkow@243
   942
	(atac 1),
nipkow@243
   943
	(etac Suc_lessD 1)
nipkow@243
   944
	]);
nipkow@243
   945
nipkow@243
   946
val adm_disj_lemma5 = prove_goal  Fix.thy
nipkow@243
   947
"[| is_chain(Y::nat=>'a); ! j. i < j --> Q(Y(j)) |] ==>\
nipkow@243
   948
\         lub(range(Y)) = lub(range(%m. if(m < Suc(i),Y(Suc(i)),Y(m))))"
nipkow@243
   949
 (fn prems =>
nipkow@243
   950
	[
nipkow@243
   951
	(cut_facts_tac prems 1),
nipkow@243
   952
	(rtac lub_equal2 1),
nipkow@243
   953
	(atac 2),
nipkow@243
   954
	(rtac adm_disj_lemma3 2),
nipkow@243
   955
	(atac 2),
nipkow@243
   956
	(atac 2),
nipkow@243
   957
	(res_inst_tac [("x","i")] exI 1),
nipkow@243
   958
	(strip_tac 1),
nipkow@243
   959
	(res_inst_tac [("s","False"),("t","ia < Suc(i)")] ssubst 1),
nipkow@243
   960
	(rtac iffI 1),
nipkow@243
   961
	(etac FalseE 2),
nipkow@243
   962
	(rtac notE 1),
nipkow@243
   963
	(rtac (not_less_eq RS iffD2) 1),
nipkow@243
   964
	(atac 1),
nipkow@243
   965
	(atac 1),
nipkow@243
   966
	(rtac (if_False RS ssubst) 1),
nipkow@243
   967
	(rtac refl 1)
nipkow@243
   968
	]);
nipkow@243
   969
nipkow@243
   970
val adm_disj_lemma6 = prove_goal  Fix.thy
nipkow@243
   971
"[| is_chain(Y::nat=>'a); ? i. ! j. i < j --> Q(Y(j)) |] ==>\
nipkow@243
   972
\         ? X. is_chain(X) & (! n. Q(X(n))) & lub(range(Y)) = lub(range(X))"
nipkow@243
   973
 (fn prems =>
nipkow@243
   974
	[
nipkow@243
   975
	(cut_facts_tac prems 1),
nipkow@243
   976
	(etac exE 1),
nipkow@243
   977
	(res_inst_tac [("x","%m.if(m< Suc(i),Y(Suc(i)),Y(m))")] exI 1),
nipkow@243
   978
	(rtac conjI 1),
nipkow@243
   979
	(rtac adm_disj_lemma3 1),
nipkow@243
   980
	(atac 1),
nipkow@243
   981
	(atac 1),
nipkow@243
   982
	(rtac conjI 1),
nipkow@243
   983
	(rtac adm_disj_lemma4 1),
nipkow@243
   984
	(atac 1),
nipkow@243
   985
	(rtac adm_disj_lemma5 1),
nipkow@243
   986
	(atac 1),
nipkow@243
   987
	(atac 1)
nipkow@243
   988
	]);
nipkow@243
   989
nipkow@243
   990
nipkow@243
   991
val adm_disj_lemma7 = prove_goal  Fix.thy 
nipkow@243
   992
"[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j))  |] ==>\
nipkow@243
   993
\         is_chain(%m. Y(theleast(%j. m<j & P(Y(j)))))"
nipkow@243
   994
 (fn prems =>
nipkow@243
   995
	[
nipkow@243
   996
	(cut_facts_tac prems 1),
nipkow@243
   997
	(rtac is_chainI 1),
nipkow@243
   998
	(rtac allI 1),
nipkow@243
   999
	(rtac chain_mono3 1),
nipkow@243
  1000
	(atac 1),
nipkow@243
  1001
	(rtac theleast2 1),
nipkow@243
  1002
	(rtac conjI 1),
nipkow@243
  1003
	(rtac Suc_lessD 1),
nipkow@243
  1004
	(etac allE 1),
nipkow@243
  1005
	(etac exE 1),
nipkow@243
  1006
	(rtac (theleast1 RS conjunct1) 1),
nipkow@243
  1007
	(atac 1),
nipkow@243
  1008
	(etac allE 1),
nipkow@243
  1009
	(etac exE 1),
nipkow@243
  1010
	(rtac (theleast1 RS conjunct2) 1),
nipkow@243
  1011
	(atac 1)
nipkow@243
  1012
	]);
nipkow@243
  1013
nipkow@243
  1014
val adm_disj_lemma8 = prove_goal  Fix.thy 
nipkow@243
  1015
"[| ! i. ? j. i < j & P(Y(j)) |] ==> ! m. P(Y(theleast(%j. m<j & P(Y(j)))))"
nipkow@243
  1016
 (fn prems =>
nipkow@243
  1017
	[
nipkow@243
  1018
	(cut_facts_tac prems 1),
nipkow@243
  1019
	(strip_tac 1),
nipkow@243
  1020
	(etac allE 1),
nipkow@243
  1021
	(etac exE 1),
nipkow@243
  1022
	(etac (theleast1 RS conjunct2) 1)
nipkow@243
  1023
	]);
nipkow@243
  1024
nipkow@243
  1025
val adm_disj_lemma9 = prove_goal  Fix.thy
nipkow@243
  1026
"[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
nipkow@243
  1027
\         lub(range(Y)) = lub(range(%m. Y(theleast(%j. m<j & P(Y(j))))))"
nipkow@243
  1028
 (fn prems =>
nipkow@243
  1029
	[
nipkow@243
  1030
	(cut_facts_tac prems 1),
nipkow@243
  1031
	(rtac antisym_less 1),
nipkow@243
  1032
	(rtac lub_mono 1),
nipkow@243
  1033
	(atac 1),
nipkow@243
  1034
	(rtac adm_disj_lemma7 1),
nipkow@243
  1035
	(atac 1),
nipkow@243
  1036
	(atac 1),
nipkow@243
  1037
	(strip_tac 1),
nipkow@243
  1038
	(rtac (chain_mono RS mp) 1),
nipkow@243
  1039
	(atac 1),
nipkow@243
  1040
	(etac allE 1),
nipkow@243
  1041
	(etac exE 1),
nipkow@243
  1042
	(rtac (theleast1 RS conjunct1) 1),
nipkow@243
  1043
	(atac 1),
nipkow@243
  1044
	(rtac lub_mono3 1),
nipkow@243
  1045
	(rtac adm_disj_lemma7 1),
nipkow@243
  1046
	(atac 1),
nipkow@243
  1047
	(atac 1),
nipkow@243
  1048
	(atac 1),
nipkow@243
  1049
	(strip_tac 1),
nipkow@243
  1050
	(rtac exI 1),
nipkow@243
  1051
	(rtac (chain_mono RS mp) 1),
nipkow@243
  1052
	(atac 1),
nipkow@243
  1053
	(rtac lessI 1)
nipkow@243
  1054
	]);
nipkow@243
  1055
nipkow@243
  1056
val adm_disj_lemma10 = prove_goal  Fix.thy
nipkow@243
  1057
"[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
nipkow@243
  1058
\         ? X. is_chain(X) & (! n. P(X(n))) & lub(range(Y)) = lub(range(X))"
nipkow@243
  1059
 (fn prems =>
nipkow@243
  1060
	[
nipkow@243
  1061
	(cut_facts_tac prems 1),
nipkow@243
  1062
	(res_inst_tac [("x","%m. Y(theleast(%j. m<j & P(Y(j))))")] exI 1),
nipkow@243
  1063
	(rtac conjI 1),
nipkow@243
  1064
	(rtac adm_disj_lemma7 1),
nipkow@243
  1065
	(atac 1),
nipkow@243
  1066
	(atac 1),
nipkow@243
  1067
	(rtac conjI 1),
nipkow@243
  1068
	(rtac adm_disj_lemma8 1),
nipkow@243
  1069
	(atac 1),
nipkow@243
  1070
	(rtac adm_disj_lemma9 1),
nipkow@243
  1071
	(atac 1),
nipkow@243
  1072
	(atac 1)
nipkow@243
  1073
	]);
nipkow@243
  1074
nipkow@243
  1075
val adm_disj = prove_goal  Fix.thy  
nipkow@243
  1076
	"[| adm(P); adm(Q) |] ==> adm(%x.P(x)|Q(x))"
nipkow@243
  1077
 (fn prems =>
nipkow@243
  1078
	[
nipkow@243
  1079
	(cut_facts_tac prems 1),
nipkow@243
  1080
	(rtac (adm_def2 RS iffD2) 1),
nipkow@243
  1081
	(strip_tac 1),
nipkow@243
  1082
	(rtac (adm_disj_lemma1 RS disjE) 1),
nipkow@243
  1083
	(atac 1),
nipkow@243
  1084
	(atac 1),
nipkow@243
  1085
	(rtac disjI2 1),
nipkow@243
  1086
	(rtac adm_disj_lemma2 1),
nipkow@243
  1087
	(atac 1),
nipkow@243
  1088
	(rtac adm_disj_lemma6 1),
nipkow@243
  1089
	(atac 1),
nipkow@243
  1090
	(atac 1),
nipkow@243
  1091
	(rtac disjI1 1),
nipkow@243
  1092
	(rtac adm_disj_lemma2 1),
nipkow@243
  1093
	(atac 1),
nipkow@243
  1094
	(rtac adm_disj_lemma10 1),
nipkow@243
  1095
	(atac 1),
nipkow@243
  1096
	(atac 1)
nipkow@243
  1097
	]);
nipkow@243
  1098
nipkow@243
  1099
val adm_impl = prove_goal  Fix.thy  
nipkow@243
  1100
	"[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x.P(x)-->Q(x))"
nipkow@243
  1101
 (fn prems =>
nipkow@243
  1102
	[
nipkow@243
  1103
	(cut_facts_tac prems 1),
nipkow@243
  1104
	(res_inst_tac [("P2","%x.~P(x)|Q(x)")] (adm_cong RS iffD1) 1),
nipkow@243
  1105
	(fast_tac HOL_cs 1),
nipkow@243
  1106
	(rtac adm_disj 1),
nipkow@243
  1107
	(atac 1),
nipkow@243
  1108
	(atac 1)
nipkow@243
  1109
	]);
nipkow@243
  1110
nipkow@243
  1111
nipkow@243
  1112
val adm_all2 = (allI RS adm_all);
nipkow@243
  1113
nipkow@243
  1114
val adm_thms = [adm_impl,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
nipkow@243
  1115
	adm_all2,adm_not_less,adm_not_free,adm_conj,adm_less
nipkow@243
  1116
	];
nipkow@243
  1117
nipkow@243
  1118
(* ------------------------------------------------------------------------- *)
nipkow@243
  1119
(* a result about functions with flat codomain                               *)
nipkow@243
  1120
(* ------------------------------------------------------------------------- *)
nipkow@243
  1121
nipkow@243
  1122
val flat_codom = prove_goalw Fix.thy [flat_def]
nipkow@243
  1123
"[|flat(y::'b);f[x::'a]=(c::'b)|] ==> f[UU::'a]=UU::'b | (!z.f[z::'a]=c)"
nipkow@243
  1124
 (fn prems =>
nipkow@243
  1125
	[
nipkow@243
  1126
	(cut_facts_tac prems 1),
nipkow@243
  1127
	(res_inst_tac [("Q","f[x::'a]=UU::'b")] classical2 1),
nipkow@243
  1128
	(rtac disjI1 1),
nipkow@243
  1129
	(rtac UU_I 1),
nipkow@243
  1130
	(res_inst_tac [("s","f[x]"),("t","UU::'b")] subst 1),
nipkow@243
  1131
	(atac 1),
nipkow@243
  1132
	(rtac (minimal RS monofun_cfun_arg) 1),
nipkow@243
  1133
	(res_inst_tac [("Q","f[UU::'a]=UU::'b")] classical2 1),
nipkow@243
  1134
	(etac disjI1 1),
nipkow@243
  1135
	(rtac disjI2 1),
nipkow@243
  1136
	(rtac allI 1),
nipkow@243
  1137
	(res_inst_tac [("s","f[x]"),("t","c")] subst 1),
nipkow@243
  1138
	(atac 1),
nipkow@243
  1139
	(res_inst_tac [("a","f[UU::'a]")] (refl RS box_equals) 1),
nipkow@243
  1140
	(etac allE 1),(etac allE 1),
nipkow@243
  1141
	(dtac mp 1),
nipkow@243
  1142
	(res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
nipkow@243
  1143
	(etac disjE 1),
nipkow@243
  1144
	(contr_tac 1),
nipkow@243
  1145
	(atac 1),
nipkow@243
  1146
	(etac allE 1),
nipkow@243
  1147
	(etac allE 1),
nipkow@243
  1148
	(dtac mp 1),
nipkow@243
  1149
	(res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
nipkow@243
  1150
	(etac disjE 1),
nipkow@243
  1151
	(contr_tac 1),
nipkow@243
  1152
	(atac 1)
nipkow@243
  1153
	]);