src/HOLCF/Fix.ML
author nipkow
Wed Jan 19 17:35:01 1994 +0100 (1994-01-19)
changeset 243 c22b85994e17
child 271 d773733dfc74
permissions -rw-r--r--
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
in HOL.
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@243
   390
nipkow@243
   391
(* ------------------------------------------------------------------------ *)
nipkow@243
   392
(* better access to definitions                                             *)
nipkow@243
   393
(* ------------------------------------------------------------------------ *)
nipkow@243
   394
nipkow@243
   395
nipkow@243
   396
val Ifix_def2 = prove_goal Fix.thy "Ifix=(%x. lub(range(%i. iterate(i,x,UU))))"
nipkow@243
   397
 (fn prems =>
nipkow@243
   398
	[
nipkow@243
   399
	(rtac ext 1),
nipkow@243
   400
	(rewrite_goals_tac [Ifix_def]),
nipkow@243
   401
	(rtac refl 1)
nipkow@243
   402
	]);
nipkow@243
   403
nipkow@243
   404
(* ------------------------------------------------------------------------ *)
nipkow@243
   405
(* direct connection between fix and iteration without Ifix                 *)
nipkow@243
   406
(* ------------------------------------------------------------------------ *)
nipkow@243
   407
nipkow@243
   408
val fix_def2 = prove_goalw Fix.thy [fix_def]
nipkow@243
   409
 "fix[F] = lub(range(%i. iterate(i,F,UU)))"
nipkow@243
   410
 (fn prems =>
nipkow@243
   411
	[
nipkow@243
   412
	(fold_goals_tac [Ifix_def]),
nipkow@243
   413
	(asm_simp_tac (Cfun_ss addsimps [contX_Ifix]) 1)
nipkow@243
   414
	]);
nipkow@243
   415
nipkow@243
   416
nipkow@243
   417
(* ------------------------------------------------------------------------ *)
nipkow@243
   418
(* Lemmas about admissibility and fixed point induction                     *)
nipkow@243
   419
(* ------------------------------------------------------------------------ *)
nipkow@243
   420
nipkow@243
   421
(* ------------------------------------------------------------------------ *)
nipkow@243
   422
(* access to definitions                                                    *)
nipkow@243
   423
(* ------------------------------------------------------------------------ *)
nipkow@243
   424
nipkow@243
   425
val adm_def2 = prove_goalw Fix.thy [adm_def]
nipkow@243
   426
	"adm(P) = (!Y. is_chain(Y) --> (!i.P(Y(i))) --> P(lub(range(Y))))"
nipkow@243
   427
 (fn prems =>
nipkow@243
   428
	[
nipkow@243
   429
	(rtac refl 1)
nipkow@243
   430
	]);
nipkow@243
   431
nipkow@243
   432
val admw_def2 = prove_goalw Fix.thy [admw_def]
nipkow@243
   433
	"admw(P) = (!F.((!n.P(iterate(n,F,UU)))-->\
nipkow@243
   434
\			 P(lub(range(%i.iterate(i,F,UU))))))"
nipkow@243
   435
 (fn prems =>
nipkow@243
   436
	[
nipkow@243
   437
	(rtac refl 1)
nipkow@243
   438
	]);
nipkow@243
   439
nipkow@243
   440
(* ------------------------------------------------------------------------ *)
nipkow@243
   441
(* an admissible formula is also weak admissible                            *)
nipkow@243
   442
(* ------------------------------------------------------------------------ *)
nipkow@243
   443
nipkow@243
   444
val adm_impl_admw = prove_goalw  Fix.thy [admw_def] "adm(P)==>admw(P)"
nipkow@243
   445
 (fn prems =>
nipkow@243
   446
	[
nipkow@243
   447
	(cut_facts_tac prems 1),
nipkow@243
   448
	(strip_tac 1),
nipkow@243
   449
	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
nipkow@243
   450
	(atac 1),
nipkow@243
   451
	(rtac is_chain_iterate 1),
nipkow@243
   452
	(atac 1)
nipkow@243
   453
	]);
nipkow@243
   454
nipkow@243
   455
(* ------------------------------------------------------------------------ *)
nipkow@243
   456
(* fixed point induction                                                    *)
nipkow@243
   457
(* ------------------------------------------------------------------------ *)
nipkow@243
   458
nipkow@243
   459
val fix_ind = prove_goal  Fix.thy  
nipkow@243
   460
"[| adm(P);P(UU);!!x. P(x) ==> P(F[x])|] ==> P(fix[F])"
nipkow@243
   461
 (fn prems =>
nipkow@243
   462
	[
nipkow@243
   463
	(cut_facts_tac prems 1),
nipkow@243
   464
	(rtac (fix_def2 RS ssubst) 1),
nipkow@243
   465
	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
nipkow@243
   466
	(atac 1),
nipkow@243
   467
	(rtac is_chain_iterate 1),
nipkow@243
   468
	(rtac allI 1),
nipkow@243
   469
	(nat_ind_tac "i" 1),
nipkow@243
   470
	(rtac (iterate_0 RS ssubst) 1),
nipkow@243
   471
	(atac 1),
nipkow@243
   472
	(rtac (iterate_Suc RS ssubst) 1),
nipkow@243
   473
	(resolve_tac prems 1),
nipkow@243
   474
	(atac 1)
nipkow@243
   475
	]);
nipkow@243
   476
nipkow@243
   477
(* ------------------------------------------------------------------------ *)
nipkow@243
   478
(* computational induction for weak admissible formulae                     *)
nipkow@243
   479
(* ------------------------------------------------------------------------ *)
nipkow@243
   480
nipkow@243
   481
val wfix_ind = prove_goal  Fix.thy  
nipkow@243
   482
"[| admw(P); !n. P(iterate(n,F,UU))|] ==> P(fix[F])"
nipkow@243
   483
 (fn prems =>
nipkow@243
   484
	[
nipkow@243
   485
	(cut_facts_tac prems 1),
nipkow@243
   486
	(rtac (fix_def2 RS ssubst) 1),
nipkow@243
   487
	(rtac (admw_def2 RS iffD1 RS spec RS mp) 1),
nipkow@243
   488
	(atac 1),
nipkow@243
   489
	(rtac allI 1),
nipkow@243
   490
	(etac spec 1)
nipkow@243
   491
	]);
nipkow@243
   492
nipkow@243
   493
(* ------------------------------------------------------------------------ *)
nipkow@243
   494
(* for chain-finite (easy) types every formula is admissible                *)
nipkow@243
   495
(* ------------------------------------------------------------------------ *)
nipkow@243
   496
nipkow@243
   497
val adm_max_in_chain = prove_goalw  Fix.thy  [adm_def]
nipkow@243
   498
"!Y. is_chain(Y::nat=>'a) --> (? n.max_in_chain(n,Y)) ==> adm(P::'a=>bool)"
nipkow@243
   499
 (fn prems =>
nipkow@243
   500
	[
nipkow@243
   501
	(cut_facts_tac prems 1),
nipkow@243
   502
	(strip_tac 1),
nipkow@243
   503
	(rtac exE 1),
nipkow@243
   504
	(rtac mp 1),
nipkow@243
   505
	(etac spec 1),
nipkow@243
   506
	(atac 1),
nipkow@243
   507
	(rtac (lub_finch1 RS thelubI RS ssubst) 1),
nipkow@243
   508
	(atac 1),
nipkow@243
   509
	(atac 1),
nipkow@243
   510
	(etac spec 1)
nipkow@243
   511
	]);
nipkow@243
   512
nipkow@243
   513
nipkow@243
   514
val adm_chain_finite = prove_goalw  Fix.thy  [chain_finite_def]
nipkow@243
   515
	"chain_finite(x::'a) ==> adm(P::'a=>bool)"
nipkow@243
   516
 (fn prems =>
nipkow@243
   517
	[
nipkow@243
   518
	(cut_facts_tac prems 1),
nipkow@243
   519
	(etac adm_max_in_chain 1)
nipkow@243
   520
	]);
nipkow@243
   521
nipkow@243
   522
(* ------------------------------------------------------------------------ *)
nipkow@243
   523
(* flat types are chain_finite                                              *)
nipkow@243
   524
(* ------------------------------------------------------------------------ *)
nipkow@243
   525
nipkow@243
   526
val flat_imp_chain_finite = prove_goalw  Fix.thy  [flat_def,chain_finite_def]
nipkow@243
   527
	"flat(x::'a)==>chain_finite(x::'a)"
nipkow@243
   528
 (fn prems =>
nipkow@243
   529
	[
nipkow@243
   530
	(rewrite_goals_tac [max_in_chain_def]),
nipkow@243
   531
	(cut_facts_tac prems 1),
nipkow@243
   532
	(strip_tac 1),
nipkow@243
   533
	(res_inst_tac [("Q","!i.Y(i)=UU")] classical2 1),
nipkow@243
   534
	(res_inst_tac [("x","0")] exI 1),
nipkow@243
   535
	(strip_tac 1),
nipkow@243
   536
	(rtac trans 1),
nipkow@243
   537
	(etac spec 1),
nipkow@243
   538
	(rtac sym 1),
nipkow@243
   539
	(etac spec 1),
nipkow@243
   540
	(rtac (chain_mono2 RS exE) 1),
nipkow@243
   541
	(fast_tac HOL_cs 1),
nipkow@243
   542
	(atac 1),
nipkow@243
   543
	(res_inst_tac [("x","Suc(x)")] exI 1),
nipkow@243
   544
	(strip_tac 1),
nipkow@243
   545
	(rtac disjE 1),
nipkow@243
   546
	(atac 3),
nipkow@243
   547
	(rtac mp 1),
nipkow@243
   548
	(dtac spec 1),
nipkow@243
   549
	(etac spec 1),
nipkow@243
   550
	(etac (le_imp_less_or_eq RS disjE) 1),
nipkow@243
   551
	(etac (chain_mono RS mp) 1),
nipkow@243
   552
	(atac 1),
nipkow@243
   553
	(hyp_subst_tac 1),
nipkow@243
   554
	(rtac refl_less 1),
nipkow@243
   555
	(res_inst_tac [("P","Y(Suc(x)) = UU")] notE 1),
nipkow@243
   556
	(atac 2),
nipkow@243
   557
	(rtac mp 1),
nipkow@243
   558
	(etac spec 1),
nipkow@243
   559
	(asm_simp_tac nat_ss 1)
nipkow@243
   560
	]);
nipkow@243
   561
nipkow@243
   562
nipkow@243
   563
val adm_flat = flat_imp_chain_finite RS adm_chain_finite;
nipkow@243
   564
(* flat(?x::?'a) ==> adm(?P::?'a => bool) *)
nipkow@243
   565
nipkow@243
   566
val flat_void = prove_goalw Fix.thy [flat_def] "flat(UU::void)"
nipkow@243
   567
 (fn prems =>
nipkow@243
   568
	[
nipkow@243
   569
	(strip_tac 1),
nipkow@243
   570
	(rtac disjI1 1),
nipkow@243
   571
	(rtac unique_void2 1)
nipkow@243
   572
	]);
nipkow@243
   573
nipkow@243
   574
(* ------------------------------------------------------------------------ *)
nipkow@243
   575
(* continuous isomorphisms are strict                                       *)
nipkow@243
   576
(* a prove for embedding projection pairs is similar                        *)
nipkow@243
   577
(* ------------------------------------------------------------------------ *)
nipkow@243
   578
nipkow@243
   579
val iso_strict = prove_goal  Fix.thy  
nipkow@243
   580
"!!f g.[|!y.f[g[y]]=(y::'b) ; !x.g[f[x]]=(x::'a) |] \
nipkow@243
   581
\ ==> f[UU]=UU & g[UU]=UU"
nipkow@243
   582
 (fn prems =>
nipkow@243
   583
	[
nipkow@243
   584
	(rtac conjI 1),
nipkow@243
   585
	(rtac UU_I 1),
nipkow@243
   586
	(res_inst_tac [("s","f[g[UU::'b]]"),("t","UU::'b")] subst 1),
nipkow@243
   587
	(etac spec 1),
nipkow@243
   588
	(rtac (minimal RS monofun_cfun_arg) 1),
nipkow@243
   589
	(rtac UU_I 1),
nipkow@243
   590
	(res_inst_tac [("s","g[f[UU::'a]]"),("t","UU::'a")] subst 1),
nipkow@243
   591
	(etac spec 1),
nipkow@243
   592
	(rtac (minimal RS monofun_cfun_arg) 1)
nipkow@243
   593
	]);
nipkow@243
   594
nipkow@243
   595
nipkow@243
   596
val isorep_defined = prove_goal Fix.thy 
nipkow@243
   597
	"[|!x.rep[abs[x]]=x;!y.abs[rep[y]]=y;z~=UU|] ==> rep[z]~=UU"
nipkow@243
   598
 (fn prems =>
nipkow@243
   599
	[
nipkow@243
   600
	(cut_facts_tac prems 1),
nipkow@243
   601
	(etac swap 1),
nipkow@243
   602
	(dtac notnotD 1),
nipkow@243
   603
	(dres_inst_tac [("f","abs")] cfun_arg_cong 1),
nipkow@243
   604
	(etac box_equals 1),
nipkow@243
   605
	(fast_tac HOL_cs 1),
nipkow@243
   606
	(etac (iso_strict RS conjunct1) 1),
nipkow@243
   607
	(atac 1)
nipkow@243
   608
	]);
nipkow@243
   609
nipkow@243
   610
val isoabs_defined = prove_goal Fix.thy 
nipkow@243
   611
	"[|!x.rep[abs[x]]=x;!y.abs[rep[y]]=y;z~=UU|] ==> abs[z]~=UU"
nipkow@243
   612
 (fn prems =>
nipkow@243
   613
	[
nipkow@243
   614
	(cut_facts_tac prems 1),
nipkow@243
   615
	(etac swap 1),
nipkow@243
   616
	(dtac notnotD 1),
nipkow@243
   617
	(dres_inst_tac [("f","rep")] cfun_arg_cong 1),
nipkow@243
   618
	(etac box_equals 1),
nipkow@243
   619
	(fast_tac HOL_cs 1),
nipkow@243
   620
	(etac (iso_strict RS conjunct2) 1),
nipkow@243
   621
	(atac 1)
nipkow@243
   622
	]);
nipkow@243
   623
nipkow@243
   624
(* ------------------------------------------------------------------------ *)
nipkow@243
   625
(* propagation of flatness and chainfiniteness by continuous isomorphisms   *)
nipkow@243
   626
(* ------------------------------------------------------------------------ *)
nipkow@243
   627
nipkow@243
   628
val chfin2chfin = prove_goalw  Fix.thy  [chain_finite_def]
nipkow@243
   629
"!!f g.[|chain_finite(x::'a); !y.f[g[y]]=(y::'b) ; !x.g[f[x]]=(x::'a) |] \
nipkow@243
   630
\ ==> chain_finite(y::'b)"
nipkow@243
   631
 (fn prems =>
nipkow@243
   632
	[
nipkow@243
   633
	(rewrite_goals_tac [max_in_chain_def]),
nipkow@243
   634
	(strip_tac 1),
nipkow@243
   635
	(rtac exE 1),
nipkow@243
   636
	(res_inst_tac [("P","is_chain(%i.g[Y(i)])")] mp 1),
nipkow@243
   637
	(etac spec 1),
nipkow@243
   638
	(etac ch2ch_fappR 1),
nipkow@243
   639
	(rtac exI 1),
nipkow@243
   640
	(strip_tac 1),
nipkow@243
   641
	(res_inst_tac [("s","f[g[Y(x)]]"),("t","Y(x)")] subst 1),
nipkow@243
   642
	(etac spec 1),
nipkow@243
   643
	(res_inst_tac [("s","f[g[Y(j)]]"),("t","Y(j)")] subst 1),
nipkow@243
   644
	(etac spec 1),
nipkow@243
   645
	(rtac cfun_arg_cong 1),
nipkow@243
   646
	(rtac mp 1),
nipkow@243
   647
	(etac spec 1),
nipkow@243
   648
	(atac 1)
nipkow@243
   649
	]);
nipkow@243
   650
nipkow@243
   651
val flat2flat = prove_goalw  Fix.thy  [flat_def]
nipkow@243
   652
"!!f g.[|flat(x::'a); !y.f[g[y]]=(y::'b) ; !x.g[f[x]]=(x::'a) |] \
nipkow@243
   653
\ ==> flat(y::'b)"
nipkow@243
   654
 (fn prems =>
nipkow@243
   655
	[
nipkow@243
   656
	(strip_tac 1),
nipkow@243
   657
	(rtac disjE 1),
nipkow@243
   658
	(res_inst_tac [("P","g[x]<<g[y]")] mp 1),
nipkow@243
   659
	(etac monofun_cfun_arg 2),
nipkow@243
   660
	(dtac spec 1),
nipkow@243
   661
	(etac spec 1),
nipkow@243
   662
	(rtac disjI1 1),
nipkow@243
   663
	(rtac trans 1),
nipkow@243
   664
	(res_inst_tac [("s","f[g[x]]"),("t","x")] subst 1),
nipkow@243
   665
	(etac spec 1),
nipkow@243
   666
	(etac cfun_arg_cong 1),
nipkow@243
   667
	(rtac (iso_strict RS conjunct1) 1),
nipkow@243
   668
	(atac 1),
nipkow@243
   669
	(atac 1),
nipkow@243
   670
	(rtac disjI2 1),
nipkow@243
   671
	(res_inst_tac [("s","f[g[x]]"),("t","x")] subst 1),
nipkow@243
   672
	(etac spec 1),
nipkow@243
   673
	(res_inst_tac [("s","f[g[y]]"),("t","y")] subst 1),
nipkow@243
   674
	(etac spec 1),
nipkow@243
   675
	(etac cfun_arg_cong 1)
nipkow@243
   676
	]);
nipkow@243
   677
nipkow@243
   678
(* ------------------------------------------------------------------------ *)
nipkow@243
   679
(* admissibility of special formulae and propagation                        *)
nipkow@243
   680
(* ------------------------------------------------------------------------ *)
nipkow@243
   681
nipkow@243
   682
val adm_less = prove_goalw  Fix.thy [adm_def]
nipkow@243
   683
	"[|contX(u);contX(v)|]==> adm(%x.u(x)<<v(x))"
nipkow@243
   684
 (fn prems =>
nipkow@243
   685
	[
nipkow@243
   686
	(cut_facts_tac prems 1),
nipkow@243
   687
	(strip_tac 1),
nipkow@243
   688
	(etac (contX2contlub RS contlubE RS spec RS mp RS ssubst) 1),
nipkow@243
   689
	(atac 1),
nipkow@243
   690
	(etac (contX2contlub RS contlubE RS spec RS mp RS ssubst) 1),
nipkow@243
   691
	(atac 1),
nipkow@243
   692
	(rtac lub_mono 1),
nipkow@243
   693
	(cut_facts_tac prems 1),
nipkow@243
   694
	(etac (contX2mono RS ch2ch_monofun) 1),
nipkow@243
   695
	(atac 1),
nipkow@243
   696
	(cut_facts_tac prems 1),
nipkow@243
   697
	(etac (contX2mono RS ch2ch_monofun) 1),
nipkow@243
   698
	(atac 1),
nipkow@243
   699
	(atac 1)
nipkow@243
   700
	]);
nipkow@243
   701
nipkow@243
   702
val adm_conj = prove_goal  Fix.thy  
nipkow@243
   703
	"[| adm(P); adm(Q) |] ==> adm(%x.P(x)&Q(x))"
nipkow@243
   704
 (fn prems =>
nipkow@243
   705
	[
nipkow@243
   706
	(cut_facts_tac prems 1),
nipkow@243
   707
	(rtac (adm_def2 RS iffD2) 1),
nipkow@243
   708
	(strip_tac 1),
nipkow@243
   709
	(rtac conjI 1),
nipkow@243
   710
	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
nipkow@243
   711
	(atac 1),
nipkow@243
   712
	(atac 1),
nipkow@243
   713
	(fast_tac HOL_cs 1),
nipkow@243
   714
	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
nipkow@243
   715
	(atac 1),
nipkow@243
   716
	(atac 1),
nipkow@243
   717
	(fast_tac HOL_cs 1)
nipkow@243
   718
	]);
nipkow@243
   719
nipkow@243
   720
val adm_cong = prove_goal  Fix.thy  
nipkow@243
   721
	"(!x. P(x) = Q(x)) ==> adm(P)=adm(Q)"
nipkow@243
   722
 (fn prems =>
nipkow@243
   723
	[
nipkow@243
   724
	(cut_facts_tac prems 1),
nipkow@243
   725
	(res_inst_tac [("s","P"),("t","Q")] subst 1),
nipkow@243
   726
	(rtac refl 2),
nipkow@243
   727
	(rtac ext 1),
nipkow@243
   728
	(etac spec 1)
nipkow@243
   729
	]);
nipkow@243
   730
nipkow@243
   731
val adm_not_free = prove_goalw  Fix.thy [adm_def] "adm(%x.t)"
nipkow@243
   732
 (fn prems =>
nipkow@243
   733
	[
nipkow@243
   734
	(fast_tac HOL_cs 1)
nipkow@243
   735
	]);
nipkow@243
   736
nipkow@243
   737
val adm_not_less = prove_goalw  Fix.thy [adm_def]
nipkow@243
   738
	"contX(t) ==> adm(%x.~ t(x) << u)"
nipkow@243
   739
 (fn prems =>
nipkow@243
   740
	[
nipkow@243
   741
	(cut_facts_tac prems 1),
nipkow@243
   742
	(strip_tac 1),
nipkow@243
   743
	(rtac contrapos 1),
nipkow@243
   744
	(etac spec 1),
nipkow@243
   745
	(rtac trans_less 1),
nipkow@243
   746
	(atac 2),
nipkow@243
   747
	(etac (contX2mono RS monofun_fun_arg) 1),
nipkow@243
   748
	(rtac is_ub_thelub 1),
nipkow@243
   749
	(atac 1)
nipkow@243
   750
	]);
nipkow@243
   751
nipkow@243
   752
val adm_all = prove_goal  Fix.thy  
nipkow@243
   753
	" !y.adm(P(y)) ==> adm(%x.!y.P(y,x))"
nipkow@243
   754
 (fn prems =>
nipkow@243
   755
	[
nipkow@243
   756
	(cut_facts_tac prems 1),
nipkow@243
   757
	(rtac (adm_def2 RS iffD2) 1),
nipkow@243
   758
	(strip_tac 1),
nipkow@243
   759
	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
nipkow@243
   760
	(etac spec 1),
nipkow@243
   761
	(atac 1),
nipkow@243
   762
	(rtac allI 1),
nipkow@243
   763
	(dtac spec 1),
nipkow@243
   764
	(etac spec 1)
nipkow@243
   765
	]);
nipkow@243
   766
nipkow@243
   767
val adm_subst = prove_goal  Fix.thy  
nipkow@243
   768
	"[|contX(t); adm(P)|] ==> adm(%x.P(t(x)))"
nipkow@243
   769
 (fn prems =>
nipkow@243
   770
	[
nipkow@243
   771
	(cut_facts_tac prems 1),
nipkow@243
   772
	(rtac (adm_def2 RS iffD2) 1),
nipkow@243
   773
	(strip_tac 1),
nipkow@243
   774
	(rtac (contX2contlub RS contlubE RS spec RS mp RS ssubst) 1),
nipkow@243
   775
	(atac 1),
nipkow@243
   776
	(atac 1),
nipkow@243
   777
	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
nipkow@243
   778
	(atac 1),
nipkow@243
   779
	(rtac (contX2mono RS ch2ch_monofun) 1),
nipkow@243
   780
	(atac 1),
nipkow@243
   781
	(atac 1),
nipkow@243
   782
	(atac 1)
nipkow@243
   783
	]);
nipkow@243
   784
nipkow@243
   785
val adm_UU_not_less = prove_goal  Fix.thy "adm(%x.~ UU << t(x))"
nipkow@243
   786
 (fn prems =>
nipkow@243
   787
	[
nipkow@243
   788
	(res_inst_tac [("P2","%x.False")] (adm_cong RS iffD1) 1),
nipkow@243
   789
	(asm_simp_tac Cfun_ss 1),
nipkow@243
   790
	(rtac adm_not_free 1)
nipkow@243
   791
	]);
nipkow@243
   792
nipkow@243
   793
val adm_not_UU = prove_goalw  Fix.thy [adm_def] 
nipkow@243
   794
	"contX(t)==> adm(%x.~ t(x) = UU)"
nipkow@243
   795
 (fn prems =>
nipkow@243
   796
	[
nipkow@243
   797
	(cut_facts_tac prems 1),
nipkow@243
   798
	(strip_tac 1),
nipkow@243
   799
	(rtac contrapos 1),
nipkow@243
   800
	(etac spec 1),
nipkow@243
   801
	(rtac (chain_UU_I RS spec) 1),
nipkow@243
   802
	(rtac (contX2mono RS ch2ch_monofun) 1),
nipkow@243
   803
	(atac 1),
nipkow@243
   804
	(atac 1),
nipkow@243
   805
	(rtac (contX2contlub RS contlubE RS spec RS mp RS subst) 1),
nipkow@243
   806
	(atac 1),
nipkow@243
   807
	(atac 1),
nipkow@243
   808
	(atac 1)
nipkow@243
   809
	]);
nipkow@243
   810
nipkow@243
   811
val adm_eq = prove_goal  Fix.thy 
nipkow@243
   812
	"[|contX(u);contX(v)|]==> adm(%x.u(x)= v(x))"
nipkow@243
   813
 (fn prems =>
nipkow@243
   814
	[
nipkow@243
   815
	(rtac (adm_cong RS iffD1) 1),
nipkow@243
   816
	(rtac allI 1),
nipkow@243
   817
	(rtac iffI 1),
nipkow@243
   818
	(rtac antisym_less 1),
nipkow@243
   819
	(rtac antisym_less_inverse 3),
nipkow@243
   820
	(atac 3),
nipkow@243
   821
	(etac conjunct1 1),
nipkow@243
   822
	(etac conjunct2 1),
nipkow@243
   823
	(rtac adm_conj 1),
nipkow@243
   824
	(rtac adm_less 1),
nipkow@243
   825
	(resolve_tac prems 1),
nipkow@243
   826
	(resolve_tac prems 1),
nipkow@243
   827
	(rtac adm_less 1),
nipkow@243
   828
	(resolve_tac prems 1),
nipkow@243
   829
	(resolve_tac prems 1)
nipkow@243
   830
	]);
nipkow@243
   831
nipkow@243
   832
nipkow@243
   833
(* ------------------------------------------------------------------------ *)
nipkow@243
   834
(* admissibility for disjunction is hard to prove. It takes 10 Lemmas       *)
nipkow@243
   835
(* ------------------------------------------------------------------------ *)
nipkow@243
   836
nipkow@243
   837
val adm_disj_lemma1 = prove_goal  Pcpo.thy 
nipkow@243
   838
"[| is_chain(Y); !n.P(Y(n))|Q(Y(n))|]\
nipkow@243
   839
\ ==> (? i.!j. i<j --> Q(Y(j))) | (!i.? j.i<j & P(Y(j)))"
nipkow@243
   840
 (fn prems =>
nipkow@243
   841
	[
nipkow@243
   842
	(cut_facts_tac prems 1),
nipkow@243
   843
	(fast_tac HOL_cs 1)
nipkow@243
   844
	]);
nipkow@243
   845
nipkow@243
   846
val adm_disj_lemma2 = prove_goal  Fix.thy  
nipkow@243
   847
"[| adm(Q); ? X.is_chain(X) & (!n.Q(X(n))) &\
nipkow@243
   848
\   lub(range(Y))=lub(range(X))|] ==> Q(lub(range(Y)))"
nipkow@243
   849
 (fn prems =>
nipkow@243
   850
	[
nipkow@243
   851
	(cut_facts_tac prems 1),
nipkow@243
   852
	(etac exE 1),
nipkow@243
   853
	(etac conjE 1),
nipkow@243
   854
	(etac conjE 1),
nipkow@243
   855
	(res_inst_tac [("s","lub(range(X))"),("t","lub(range(Y))")] ssubst 1),
nipkow@243
   856
	(atac 1),
nipkow@243
   857
	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
nipkow@243
   858
	(atac 1),
nipkow@243
   859
	(atac 1),
nipkow@243
   860
	(atac 1)
nipkow@243
   861
	]);
nipkow@243
   862
nipkow@243
   863
val adm_disj_lemma3 = prove_goal  Fix.thy
nipkow@243
   864
"[| is_chain(Y); ! j. i < j --> Q(Y(j)) |] ==>\
nipkow@243
   865
\         is_chain(%m. if(m < Suc(i),Y(Suc(i)),Y(m)))"
nipkow@243
   866
 (fn prems =>
nipkow@243
   867
	[
nipkow@243
   868
	(cut_facts_tac prems 1),
nipkow@243
   869
	(rtac is_chainI 1),
nipkow@243
   870
	(rtac allI 1),
nipkow@243
   871
	(res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1),
nipkow@243
   872
	(res_inst_tac [("s","False"),("t","ia < Suc(i)")] ssubst 1),
nipkow@243
   873
	(rtac iffI 1),
nipkow@243
   874
	(etac FalseE 2),
nipkow@243
   875
	(rtac notE 1),
nipkow@243
   876
	(rtac (not_less_eq RS iffD2) 1),
nipkow@243
   877
	(atac 1),
nipkow@243
   878
	(atac 1),
nipkow@243
   879
	(res_inst_tac [("s","False"),("t","Suc(ia) < Suc(i)")] ssubst 1),
nipkow@243
   880
	(asm_simp_tac nat_ss  1),
nipkow@243
   881
	(rtac iffI 1),
nipkow@243
   882
	(etac FalseE 2),
nipkow@243
   883
	(rtac notE 1),
nipkow@243
   884
	(etac (less_not_sym RS mp) 1),	
nipkow@243
   885
	(atac 1),
nipkow@243
   886
	(asm_simp_tac Cfun_ss  1),
nipkow@243
   887
	(etac (is_chainE RS spec) 1),
nipkow@243
   888
	(hyp_subst_tac 1),
nipkow@243
   889
	(asm_simp_tac nat_ss 1),
nipkow@243
   890
	(rtac refl_less 1),
nipkow@243
   891
	(asm_simp_tac nat_ss 1),
nipkow@243
   892
	(rtac refl_less 1)
nipkow@243
   893
	]);
nipkow@243
   894
nipkow@243
   895
val adm_disj_lemma4 = prove_goal  Fix.thy
nipkow@243
   896
"[| ! j. i < j --> Q(Y(j)) |] ==>\
nipkow@243
   897
\	 ! n. Q(if(n < Suc(i),Y(Suc(i)),Y(n)))"
nipkow@243
   898
 (fn prems =>
nipkow@243
   899
	[
nipkow@243
   900
	(cut_facts_tac prems 1),
nipkow@243
   901
	(rtac allI 1),
nipkow@243
   902
	(res_inst_tac [("m","n"),("n","Suc(i)")] nat_less_cases 1),
nipkow@243
   903
	(res_inst_tac[("s","Y(Suc(i))"),("t","if(n<Suc(i),Y(Suc(i)),Y(n))")]
nipkow@243
   904
		ssubst 1),
nipkow@243
   905
	(asm_simp_tac nat_ss 1),
nipkow@243
   906
	(etac allE 1),
nipkow@243
   907
	(rtac mp 1),
nipkow@243
   908
	(atac 1),
nipkow@243
   909
	(asm_simp_tac nat_ss 1),
nipkow@243
   910
	(res_inst_tac[("s","Y(n)"),("t","if(n<Suc(i),Y(Suc(i)),Y(n))")] 
nipkow@243
   911
		ssubst 1),
nipkow@243
   912
	(asm_simp_tac nat_ss 1),
nipkow@243
   913
	(hyp_subst_tac 1),
nipkow@243
   914
	(dtac spec 1),
nipkow@243
   915
	(rtac mp 1),
nipkow@243
   916
	(atac 1),
nipkow@243
   917
	(asm_simp_tac nat_ss 1),
nipkow@243
   918
	(res_inst_tac [("s","Y(n)"),("t","if(n < Suc(i),Y(Suc(i)),Y(n))")] 
nipkow@243
   919
		ssubst 1),
nipkow@243
   920
	(res_inst_tac [("s","False"),("t","n < Suc(i)")] ssubst 1),
nipkow@243
   921
	(rtac iffI 1),
nipkow@243
   922
	(etac FalseE 2),
nipkow@243
   923
	(rtac notE 1),
nipkow@243
   924
	(etac (less_not_sym RS mp) 1),	
nipkow@243
   925
	(atac 1),
nipkow@243
   926
	(asm_simp_tac nat_ss 1),
nipkow@243
   927
	(dtac spec 1),
nipkow@243
   928
	(rtac mp 1),
nipkow@243
   929
	(atac 1),
nipkow@243
   930
	(etac Suc_lessD 1)
nipkow@243
   931
	]);
nipkow@243
   932
nipkow@243
   933
val adm_disj_lemma5 = prove_goal  Fix.thy
nipkow@243
   934
"[| is_chain(Y::nat=>'a); ! j. i < j --> Q(Y(j)) |] ==>\
nipkow@243
   935
\         lub(range(Y)) = lub(range(%m. if(m < Suc(i),Y(Suc(i)),Y(m))))"
nipkow@243
   936
 (fn prems =>
nipkow@243
   937
	[
nipkow@243
   938
	(cut_facts_tac prems 1),
nipkow@243
   939
	(rtac lub_equal2 1),
nipkow@243
   940
	(atac 2),
nipkow@243
   941
	(rtac adm_disj_lemma3 2),
nipkow@243
   942
	(atac 2),
nipkow@243
   943
	(atac 2),
nipkow@243
   944
	(res_inst_tac [("x","i")] exI 1),
nipkow@243
   945
	(strip_tac 1),
nipkow@243
   946
	(res_inst_tac [("s","False"),("t","ia < Suc(i)")] ssubst 1),
nipkow@243
   947
	(rtac iffI 1),
nipkow@243
   948
	(etac FalseE 2),
nipkow@243
   949
	(rtac notE 1),
nipkow@243
   950
	(rtac (not_less_eq RS iffD2) 1),
nipkow@243
   951
	(atac 1),
nipkow@243
   952
	(atac 1),
nipkow@243
   953
	(rtac (if_False RS ssubst) 1),
nipkow@243
   954
	(rtac refl 1)
nipkow@243
   955
	]);
nipkow@243
   956
nipkow@243
   957
val adm_disj_lemma6 = prove_goal  Fix.thy
nipkow@243
   958
"[| is_chain(Y::nat=>'a); ? i. ! j. i < j --> Q(Y(j)) |] ==>\
nipkow@243
   959
\         ? X. is_chain(X) & (! n. Q(X(n))) & lub(range(Y)) = lub(range(X))"
nipkow@243
   960
 (fn prems =>
nipkow@243
   961
	[
nipkow@243
   962
	(cut_facts_tac prems 1),
nipkow@243
   963
	(etac exE 1),
nipkow@243
   964
	(res_inst_tac [("x","%m.if(m< Suc(i),Y(Suc(i)),Y(m))")] exI 1),
nipkow@243
   965
	(rtac conjI 1),
nipkow@243
   966
	(rtac adm_disj_lemma3 1),
nipkow@243
   967
	(atac 1),
nipkow@243
   968
	(atac 1),
nipkow@243
   969
	(rtac conjI 1),
nipkow@243
   970
	(rtac adm_disj_lemma4 1),
nipkow@243
   971
	(atac 1),
nipkow@243
   972
	(rtac adm_disj_lemma5 1),
nipkow@243
   973
	(atac 1),
nipkow@243
   974
	(atac 1)
nipkow@243
   975
	]);
nipkow@243
   976
nipkow@243
   977
nipkow@243
   978
val adm_disj_lemma7 = prove_goal  Fix.thy 
nipkow@243
   979
"[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j))  |] ==>\
nipkow@243
   980
\         is_chain(%m. Y(theleast(%j. m<j & P(Y(j)))))"
nipkow@243
   981
 (fn prems =>
nipkow@243
   982
	[
nipkow@243
   983
	(cut_facts_tac prems 1),
nipkow@243
   984
	(rtac is_chainI 1),
nipkow@243
   985
	(rtac allI 1),
nipkow@243
   986
	(rtac chain_mono3 1),
nipkow@243
   987
	(atac 1),
nipkow@243
   988
	(rtac theleast2 1),
nipkow@243
   989
	(rtac conjI 1),
nipkow@243
   990
	(rtac Suc_lessD 1),
nipkow@243
   991
	(etac allE 1),
nipkow@243
   992
	(etac exE 1),
nipkow@243
   993
	(rtac (theleast1 RS conjunct1) 1),
nipkow@243
   994
	(atac 1),
nipkow@243
   995
	(etac allE 1),
nipkow@243
   996
	(etac exE 1),
nipkow@243
   997
	(rtac (theleast1 RS conjunct2) 1),
nipkow@243
   998
	(atac 1)
nipkow@243
   999
	]);
nipkow@243
  1000
nipkow@243
  1001
val adm_disj_lemma8 = prove_goal  Fix.thy 
nipkow@243
  1002
"[| ! i. ? j. i < j & P(Y(j)) |] ==> ! m. P(Y(theleast(%j. m<j & P(Y(j)))))"
nipkow@243
  1003
 (fn prems =>
nipkow@243
  1004
	[
nipkow@243
  1005
	(cut_facts_tac prems 1),
nipkow@243
  1006
	(strip_tac 1),
nipkow@243
  1007
	(etac allE 1),
nipkow@243
  1008
	(etac exE 1),
nipkow@243
  1009
	(etac (theleast1 RS conjunct2) 1)
nipkow@243
  1010
	]);
nipkow@243
  1011
nipkow@243
  1012
val adm_disj_lemma9 = prove_goal  Fix.thy
nipkow@243
  1013
"[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
nipkow@243
  1014
\         lub(range(Y)) = lub(range(%m. Y(theleast(%j. m<j & P(Y(j))))))"
nipkow@243
  1015
 (fn prems =>
nipkow@243
  1016
	[
nipkow@243
  1017
	(cut_facts_tac prems 1),
nipkow@243
  1018
	(rtac antisym_less 1),
nipkow@243
  1019
	(rtac lub_mono 1),
nipkow@243
  1020
	(atac 1),
nipkow@243
  1021
	(rtac adm_disj_lemma7 1),
nipkow@243
  1022
	(atac 1),
nipkow@243
  1023
	(atac 1),
nipkow@243
  1024
	(strip_tac 1),
nipkow@243
  1025
	(rtac (chain_mono RS mp) 1),
nipkow@243
  1026
	(atac 1),
nipkow@243
  1027
	(etac allE 1),
nipkow@243
  1028
	(etac exE 1),
nipkow@243
  1029
	(rtac (theleast1 RS conjunct1) 1),
nipkow@243
  1030
	(atac 1),
nipkow@243
  1031
	(rtac lub_mono3 1),
nipkow@243
  1032
	(rtac adm_disj_lemma7 1),
nipkow@243
  1033
	(atac 1),
nipkow@243
  1034
	(atac 1),
nipkow@243
  1035
	(atac 1),
nipkow@243
  1036
	(strip_tac 1),
nipkow@243
  1037
	(rtac exI 1),
nipkow@243
  1038
	(rtac (chain_mono RS mp) 1),
nipkow@243
  1039
	(atac 1),
nipkow@243
  1040
	(rtac lessI 1)
nipkow@243
  1041
	]);
nipkow@243
  1042
nipkow@243
  1043
val adm_disj_lemma10 = prove_goal  Fix.thy
nipkow@243
  1044
"[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
nipkow@243
  1045
\         ? X. is_chain(X) & (! n. P(X(n))) & lub(range(Y)) = lub(range(X))"
nipkow@243
  1046
 (fn prems =>
nipkow@243
  1047
	[
nipkow@243
  1048
	(cut_facts_tac prems 1),
nipkow@243
  1049
	(res_inst_tac [("x","%m. Y(theleast(%j. m<j & P(Y(j))))")] exI 1),
nipkow@243
  1050
	(rtac conjI 1),
nipkow@243
  1051
	(rtac adm_disj_lemma7 1),
nipkow@243
  1052
	(atac 1),
nipkow@243
  1053
	(atac 1),
nipkow@243
  1054
	(rtac conjI 1),
nipkow@243
  1055
	(rtac adm_disj_lemma8 1),
nipkow@243
  1056
	(atac 1),
nipkow@243
  1057
	(rtac adm_disj_lemma9 1),
nipkow@243
  1058
	(atac 1),
nipkow@243
  1059
	(atac 1)
nipkow@243
  1060
	]);
nipkow@243
  1061
nipkow@243
  1062
val adm_disj = prove_goal  Fix.thy  
nipkow@243
  1063
	"[| adm(P); adm(Q) |] ==> adm(%x.P(x)|Q(x))"
nipkow@243
  1064
 (fn prems =>
nipkow@243
  1065
	[
nipkow@243
  1066
	(cut_facts_tac prems 1),
nipkow@243
  1067
	(rtac (adm_def2 RS iffD2) 1),
nipkow@243
  1068
	(strip_tac 1),
nipkow@243
  1069
	(rtac (adm_disj_lemma1 RS disjE) 1),
nipkow@243
  1070
	(atac 1),
nipkow@243
  1071
	(atac 1),
nipkow@243
  1072
	(rtac disjI2 1),
nipkow@243
  1073
	(rtac adm_disj_lemma2 1),
nipkow@243
  1074
	(atac 1),
nipkow@243
  1075
	(rtac adm_disj_lemma6 1),
nipkow@243
  1076
	(atac 1),
nipkow@243
  1077
	(atac 1),
nipkow@243
  1078
	(rtac disjI1 1),
nipkow@243
  1079
	(rtac adm_disj_lemma2 1),
nipkow@243
  1080
	(atac 1),
nipkow@243
  1081
	(rtac adm_disj_lemma10 1),
nipkow@243
  1082
	(atac 1),
nipkow@243
  1083
	(atac 1)
nipkow@243
  1084
	]);
nipkow@243
  1085
nipkow@243
  1086
val adm_impl = prove_goal  Fix.thy  
nipkow@243
  1087
	"[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x.P(x)-->Q(x))"
nipkow@243
  1088
 (fn prems =>
nipkow@243
  1089
	[
nipkow@243
  1090
	(cut_facts_tac prems 1),
nipkow@243
  1091
	(res_inst_tac [("P2","%x.~P(x)|Q(x)")] (adm_cong RS iffD1) 1),
nipkow@243
  1092
	(fast_tac HOL_cs 1),
nipkow@243
  1093
	(rtac adm_disj 1),
nipkow@243
  1094
	(atac 1),
nipkow@243
  1095
	(atac 1)
nipkow@243
  1096
	]);
nipkow@243
  1097
nipkow@243
  1098
nipkow@243
  1099
val adm_all2 = (allI RS adm_all);
nipkow@243
  1100
nipkow@243
  1101
val adm_thms = [adm_impl,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
nipkow@243
  1102
	adm_all2,adm_not_less,adm_not_free,adm_conj,adm_less
nipkow@243
  1103
	];
nipkow@243
  1104
nipkow@243
  1105
(* ------------------------------------------------------------------------- *)
nipkow@243
  1106
(* a result about functions with flat codomain                               *)
nipkow@243
  1107
(* ------------------------------------------------------------------------- *)
nipkow@243
  1108
nipkow@243
  1109
val flat_codom = prove_goalw Fix.thy [flat_def]
nipkow@243
  1110
"[|flat(y::'b);f[x::'a]=(c::'b)|] ==> f[UU::'a]=UU::'b | (!z.f[z::'a]=c)"
nipkow@243
  1111
 (fn prems =>
nipkow@243
  1112
	[
nipkow@243
  1113
	(cut_facts_tac prems 1),
nipkow@243
  1114
	(res_inst_tac [("Q","f[x::'a]=UU::'b")] classical2 1),
nipkow@243
  1115
	(rtac disjI1 1),
nipkow@243
  1116
	(rtac UU_I 1),
nipkow@243
  1117
	(res_inst_tac [("s","f[x]"),("t","UU::'b")] subst 1),
nipkow@243
  1118
	(atac 1),
nipkow@243
  1119
	(rtac (minimal RS monofun_cfun_arg) 1),
nipkow@243
  1120
	(res_inst_tac [("Q","f[UU::'a]=UU::'b")] classical2 1),
nipkow@243
  1121
	(etac disjI1 1),
nipkow@243
  1122
	(rtac disjI2 1),
nipkow@243
  1123
	(rtac allI 1),
nipkow@243
  1124
	(res_inst_tac [("s","f[x]"),("t","c")] subst 1),
nipkow@243
  1125
	(atac 1),
nipkow@243
  1126
	(res_inst_tac [("a","f[UU::'a]")] (refl RS box_equals) 1),
nipkow@243
  1127
	(etac allE 1),(etac allE 1),
nipkow@243
  1128
	(dtac mp 1),
nipkow@243
  1129
	(res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
nipkow@243
  1130
	(etac disjE 1),
nipkow@243
  1131
	(contr_tac 1),
nipkow@243
  1132
	(atac 1),
nipkow@243
  1133
	(etac allE 1),
nipkow@243
  1134
	(etac allE 1),
nipkow@243
  1135
	(dtac mp 1),
nipkow@243
  1136
	(res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
nipkow@243
  1137
	(etac disjE 1),
nipkow@243
  1138
	(contr_tac 1),
nipkow@243
  1139
	(atac 1)
nipkow@243
  1140
	]);