src/HOLCF/Fix.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 5291 5706f0ef1d43
child 5656 f8389824189b
permissions -rw-r--r--
made tutorial first;
slotosch@2640
     1
(*  Title:      HOLCF/Fix.ML
nipkow@243
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Franz Regensburger
nipkow@243
     4
    Copyright   1993  Technische Universitaet Muenchen
nipkow@243
     5
slotosch@2640
     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
slotosch@2640
    15
qed_goal "iterate_Suc2" thy "iterate (Suc n) F x = iterate n F (F`x)"
nipkow@243
    16
 (fn prems =>
clasohm@1461
    17
        [
berghofe@5192
    18
        (induct_tac "n" 1),
clasohm@1461
    19
        (Simp_tac 1),
paulson@2033
    20
        (stac iterate_Suc 1),
paulson@2033
    21
        (stac iterate_Suc 1),
paulson@2033
    22
        (etac ssubst 1),
paulson@2033
    23
        (rtac refl 1)
clasohm@1461
    24
        ]);
nipkow@243
    25
nipkow@243
    26
(* ------------------------------------------------------------------------ *)
nipkow@243
    27
(* the sequence of function itertaions is a chain                           *)
nipkow@243
    28
(* This property is essential since monotonicity of iterate makes no sense  *)
nipkow@243
    29
(* ------------------------------------------------------------------------ *)
nipkow@243
    30
oheimb@4720
    31
qed_goalw "chain_iterate2" thy [chain] 
oheimb@4720
    32
        " x << F`x ==> chain (%i. iterate i F x)"
nipkow@243
    33
 (fn prems =>
clasohm@1461
    34
        [
clasohm@1461
    35
        (cut_facts_tac prems 1),
clasohm@1461
    36
        (strip_tac 1),
clasohm@1461
    37
        (Simp_tac 1),
berghofe@5192
    38
        (induct_tac "i" 1),
clasohm@1461
    39
        (Asm_simp_tac 1),
clasohm@1461
    40
        (Asm_simp_tac 1),
clasohm@1461
    41
        (etac monofun_cfun_arg 1)
clasohm@1461
    42
        ]);
nipkow@243
    43
nipkow@243
    44
oheimb@4720
    45
qed_goal "chain_iterate" thy  
oheimb@4720
    46
        "chain (%i. iterate i F UU)"
nipkow@243
    47
 (fn prems =>
clasohm@1461
    48
        [
oheimb@4720
    49
        (rtac chain_iterate2 1),
clasohm@1461
    50
        (rtac minimal 1)
clasohm@1461
    51
        ]);
nipkow@243
    52
nipkow@243
    53
nipkow@243
    54
(* ------------------------------------------------------------------------ *)
nipkow@243
    55
(* Kleene's fixed point theorems for continuous functions in pointed        *)
nipkow@243
    56
(* omega cpo's                                                              *)
nipkow@243
    57
(* ------------------------------------------------------------------------ *)
nipkow@243
    58
nipkow@243
    59
slotosch@2640
    60
qed_goalw "Ifix_eq" thy  [Ifix_def] "Ifix F =F`(Ifix F)"
nipkow@243
    61
 (fn prems =>
clasohm@1461
    62
        [
paulson@2033
    63
        (stac contlub_cfun_arg 1),
oheimb@4720
    64
        (rtac chain_iterate 1),
clasohm@1461
    65
        (rtac antisym_less 1),
clasohm@1461
    66
        (rtac lub_mono 1),
oheimb@4720
    67
        (rtac chain_iterate 1),
slotosch@5291
    68
        (rtac ch2ch_Rep_CFunR 1),
oheimb@4720
    69
        (rtac chain_iterate 1),
clasohm@1461
    70
        (rtac allI 1),
clasohm@1461
    71
        (rtac (iterate_Suc RS subst) 1),
oheimb@4720
    72
        (rtac (chain_iterate RS chainE RS spec) 1),
clasohm@1461
    73
        (rtac is_lub_thelub 1),
slotosch@5291
    74
        (rtac ch2ch_Rep_CFunR 1),
oheimb@4720
    75
        (rtac chain_iterate 1),
clasohm@1461
    76
        (rtac ub_rangeI 1),
clasohm@1461
    77
        (rtac allI 1),
clasohm@1461
    78
        (rtac (iterate_Suc RS subst) 1),
clasohm@1461
    79
        (rtac is_ub_thelub 1),
oheimb@4720
    80
        (rtac chain_iterate 1)
clasohm@1461
    81
        ]);
nipkow@243
    82
nipkow@243
    83
slotosch@2640
    84
qed_goalw "Ifix_least" thy [Ifix_def] "F`x=x ==> Ifix(F) << x"
nipkow@243
    85
 (fn prems =>
clasohm@1461
    86
        [
clasohm@1461
    87
        (cut_facts_tac prems 1),
clasohm@1461
    88
        (rtac is_lub_thelub 1),
oheimb@4720
    89
        (rtac chain_iterate 1),
clasohm@1461
    90
        (rtac ub_rangeI 1),
clasohm@1461
    91
        (strip_tac 1),
berghofe@5192
    92
        (induct_tac "i" 1),
clasohm@1461
    93
        (Asm_simp_tac 1),
clasohm@1461
    94
        (Asm_simp_tac 1),
clasohm@1461
    95
        (res_inst_tac [("t","x")] subst 1),
clasohm@1461
    96
        (atac 1),
clasohm@1461
    97
        (etac monofun_cfun_arg 1)
clasohm@1461
    98
        ]);
nipkow@243
    99
nipkow@243
   100
nipkow@243
   101
(* ------------------------------------------------------------------------ *)
nipkow@243
   102
(* monotonicity and continuity of iterate                                   *)
nipkow@243
   103
(* ------------------------------------------------------------------------ *)
nipkow@243
   104
slotosch@2640
   105
qed_goalw "monofun_iterate" thy  [monofun] "monofun(iterate(i))"
nipkow@243
   106
 (fn prems =>
clasohm@1461
   107
        [
clasohm@1461
   108
        (strip_tac 1),
berghofe@5192
   109
        (induct_tac "i" 1),
clasohm@1461
   110
        (Asm_simp_tac 1),
clasohm@1461
   111
        (Asm_simp_tac 1),
clasohm@1461
   112
        (rtac (less_fun RS iffD2) 1),
clasohm@1461
   113
        (rtac allI 1),
clasohm@1461
   114
        (rtac monofun_cfun 1),
clasohm@1461
   115
        (atac 1),
clasohm@1461
   116
        (rtac (less_fun RS iffD1 RS spec) 1),
clasohm@1461
   117
        (atac 1)
clasohm@1461
   118
        ]);
nipkow@243
   119
nipkow@243
   120
(* ------------------------------------------------------------------------ *)
nipkow@243
   121
(* the following lemma uses contlub_cfun which itself is based on a         *)
nipkow@243
   122
(* diagonalisation lemma for continuous functions with two arguments.       *)
slotosch@5291
   123
(* In this special case it is the application function Rep_CFun                 *)
nipkow@243
   124
(* ------------------------------------------------------------------------ *)
nipkow@243
   125
slotosch@2640
   126
qed_goalw "contlub_iterate" thy  [contlub] "contlub(iterate(i))"
nipkow@243
   127
 (fn prems =>
clasohm@1461
   128
        [
clasohm@1461
   129
        (strip_tac 1),
berghofe@5192
   130
        (induct_tac "i" 1),
clasohm@1461
   131
        (Asm_simp_tac 1),
clasohm@1461
   132
        (rtac (lub_const RS thelubI RS sym) 1),
clasohm@1461
   133
        (Asm_simp_tac 1),
clasohm@1461
   134
        (rtac ext 1),
paulson@2033
   135
        (stac thelub_fun 1),
oheimb@4720
   136
        (rtac chainI 1),
clasohm@1461
   137
        (rtac allI 1),
clasohm@1461
   138
        (rtac (less_fun RS iffD2) 1),
clasohm@1461
   139
        (rtac allI 1),
oheimb@4720
   140
        (rtac (chainE RS spec) 1),
slotosch@5291
   141
        (rtac (monofun_Rep_CFun1 RS ch2ch_MF2LR) 1),
clasohm@1461
   142
        (rtac allI 1),
slotosch@5291
   143
        (rtac monofun_Rep_CFun2 1),
clasohm@1461
   144
        (atac 1),
clasohm@1461
   145
        (rtac ch2ch_fun 1),
clasohm@1461
   146
        (rtac (monofun_iterate RS ch2ch_monofun) 1),
clasohm@1461
   147
        (atac 1),
paulson@2033
   148
        (stac thelub_fun 1),
clasohm@1461
   149
        (rtac (monofun_iterate RS ch2ch_monofun) 1),
clasohm@1461
   150
        (atac 1),
clasohm@1461
   151
        (rtac contlub_cfun  1),
clasohm@1461
   152
        (atac 1),
clasohm@1461
   153
        (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun) 1)
clasohm@1461
   154
        ]);
nipkow@243
   155
nipkow@243
   156
slotosch@2640
   157
qed_goal "cont_iterate" thy "cont(iterate(i))"
nipkow@243
   158
 (fn prems =>
clasohm@1461
   159
        [
clasohm@1461
   160
        (rtac monocontlub2cont 1),
clasohm@1461
   161
        (rtac monofun_iterate 1),
clasohm@1461
   162
        (rtac contlub_iterate 1)
clasohm@1461
   163
        ]);
nipkow@243
   164
nipkow@243
   165
(* ------------------------------------------------------------------------ *)
nipkow@243
   166
(* a lemma about continuity of iterate in its third argument                *)
nipkow@243
   167
(* ------------------------------------------------------------------------ *)
nipkow@243
   168
slotosch@2640
   169
qed_goal "monofun_iterate2" thy "monofun(iterate n F)"
nipkow@243
   170
 (fn prems =>
clasohm@1461
   171
        [
clasohm@1461
   172
        (rtac monofunI 1),
clasohm@1461
   173
        (strip_tac 1),
berghofe@5192
   174
        (induct_tac "n" 1),
clasohm@1461
   175
        (Asm_simp_tac 1),
clasohm@1461
   176
        (Asm_simp_tac 1),
clasohm@1461
   177
        (etac monofun_cfun_arg 1)
clasohm@1461
   178
        ]);
nipkow@243
   179
slotosch@2640
   180
qed_goal "contlub_iterate2" thy "contlub(iterate n F)"
nipkow@243
   181
 (fn prems =>
clasohm@1461
   182
        [
clasohm@1461
   183
        (rtac contlubI 1),
clasohm@1461
   184
        (strip_tac 1),
berghofe@5192
   185
        (induct_tac "n" 1),
clasohm@1461
   186
        (Simp_tac 1),
clasohm@1461
   187
        (Simp_tac 1),
nipkow@3044
   188
        (res_inst_tac [("t","iterate n F (lub(range(%u. Y u)))"),
nipkow@3044
   189
        ("s","lub(range(%i. iterate n F (Y i)))")] ssubst 1),
clasohm@1461
   190
        (atac 1),
clasohm@1461
   191
        (rtac contlub_cfun_arg 1),
clasohm@1461
   192
        (etac (monofun_iterate2 RS ch2ch_monofun) 1)
clasohm@1461
   193
        ]);
nipkow@243
   194
slotosch@2640
   195
qed_goal "cont_iterate2" thy "cont (iterate n F)"
nipkow@243
   196
 (fn prems =>
clasohm@1461
   197
        [
clasohm@1461
   198
        (rtac monocontlub2cont 1),
clasohm@1461
   199
        (rtac monofun_iterate2 1),
clasohm@1461
   200
        (rtac contlub_iterate2 1)
clasohm@1461
   201
        ]);
nipkow@243
   202
nipkow@243
   203
(* ------------------------------------------------------------------------ *)
nipkow@243
   204
(* monotonicity and continuity of Ifix                                      *)
nipkow@243
   205
(* ------------------------------------------------------------------------ *)
nipkow@243
   206
slotosch@2640
   207
qed_goalw "monofun_Ifix" thy  [monofun,Ifix_def] "monofun(Ifix)"
nipkow@243
   208
 (fn prems =>
clasohm@1461
   209
        [
clasohm@1461
   210
        (strip_tac 1),
clasohm@1461
   211
        (rtac lub_mono 1),
oheimb@4720
   212
        (rtac chain_iterate 1),
oheimb@4720
   213
        (rtac chain_iterate 1),
clasohm@1461
   214
        (rtac allI 1),
clasohm@1461
   215
        (rtac (less_fun RS iffD1 RS spec) 1),
clasohm@1461
   216
        (etac (monofun_iterate RS monofunE RS spec RS spec RS mp) 1)
clasohm@1461
   217
        ]);
nipkow@243
   218
nipkow@243
   219
(* ------------------------------------------------------------------------ *)
nipkow@243
   220
(* since iterate is not monotone in its first argument, special lemmas must *)
nipkow@243
   221
(* be derived for lubs in this argument                                     *)
nipkow@243
   222
(* ------------------------------------------------------------------------ *)
nipkow@243
   223
oheimb@4720
   224
qed_goal "chain_iterate_lub" thy   
oheimb@4720
   225
"chain(Y) ==> chain(%i. lub(range(%ia. iterate ia (Y i) UU)))"
nipkow@243
   226
 (fn prems =>
clasohm@1461
   227
        [
clasohm@1461
   228
        (cut_facts_tac prems 1),
oheimb@4720
   229
        (rtac chainI 1),
clasohm@1461
   230
        (strip_tac 1),
clasohm@1461
   231
        (rtac lub_mono 1),
oheimb@4720
   232
        (rtac chain_iterate 1),
oheimb@4720
   233
        (rtac chain_iterate 1),
clasohm@1461
   234
        (strip_tac 1),
oheimb@4720
   235
        (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun RS chainE 
nipkow@243
   236
         RS spec) 1)
clasohm@1461
   237
        ]);
nipkow@243
   238
nipkow@243
   239
(* ------------------------------------------------------------------------ *)
nipkow@243
   240
(* this exchange lemma is analog to the one for monotone functions          *)
nipkow@243
   241
(* observe that monotonicity is not really needed. The propagation of       *)
nipkow@243
   242
(* chains is the essential argument which is usually derived from monot.    *)
nipkow@243
   243
(* ------------------------------------------------------------------------ *)
nipkow@243
   244
slotosch@2640
   245
qed_goal "contlub_Ifix_lemma1" thy 
oheimb@4720
   246
"chain(Y) ==>iterate n (lub(range Y)) y = lub(range(%i. iterate n (Y i) y))"
nipkow@243
   247
 (fn prems =>
clasohm@1461
   248
        [
clasohm@1461
   249
        (cut_facts_tac prems 1),
clasohm@1461
   250
        (rtac (thelub_fun RS subst) 1),
clasohm@1461
   251
        (rtac (monofun_iterate RS ch2ch_monofun) 1),
clasohm@1461
   252
        (atac 1),
clasohm@1461
   253
        (rtac fun_cong 1),
paulson@2033
   254
        (stac (contlub_iterate RS contlubE RS spec RS mp) 1),
clasohm@1461
   255
        (atac 1),
clasohm@1461
   256
        (rtac refl 1)
clasohm@1461
   257
        ]);
nipkow@243
   258
nipkow@243
   259
oheimb@4720
   260
qed_goal "ex_lub_iterate" thy  "chain(Y) ==>\
regensbu@1168
   261
\         lub(range(%i. lub(range(%ia. iterate i (Y ia) UU)))) =\
regensbu@1168
   262
\         lub(range(%i. lub(range(%ia. iterate ia (Y i) UU))))"
nipkow@243
   263
 (fn prems =>
clasohm@1461
   264
        [
clasohm@1461
   265
        (cut_facts_tac prems 1),
clasohm@1461
   266
        (rtac antisym_less 1),
clasohm@1461
   267
        (rtac is_lub_thelub 1),
clasohm@1461
   268
        (rtac (contlub_Ifix_lemma1 RS ext RS subst) 1),
clasohm@1461
   269
        (atac 1),
oheimb@4720
   270
        (rtac chain_iterate 1),
clasohm@1461
   271
        (rtac ub_rangeI 1),
clasohm@1461
   272
        (strip_tac 1),
clasohm@1461
   273
        (rtac lub_mono 1),
clasohm@1461
   274
        (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun) 1),
oheimb@4720
   275
        (etac chain_iterate_lub 1),
clasohm@1461
   276
        (strip_tac 1),
clasohm@1461
   277
        (rtac is_ub_thelub 1),
oheimb@4720
   278
        (rtac chain_iterate 1),
clasohm@1461
   279
        (rtac is_lub_thelub 1),
oheimb@4720
   280
        (etac chain_iterate_lub 1),
clasohm@1461
   281
        (rtac ub_rangeI 1),
clasohm@1461
   282
        (strip_tac 1),
clasohm@1461
   283
        (rtac lub_mono 1),
oheimb@4720
   284
        (rtac chain_iterate 1),
clasohm@1461
   285
        (rtac (contlub_Ifix_lemma1 RS ext RS subst) 1),
clasohm@1461
   286
        (atac 1),
oheimb@4720
   287
        (rtac chain_iterate 1),
clasohm@1461
   288
        (strip_tac 1),
clasohm@1461
   289
        (rtac is_ub_thelub 1),
clasohm@1461
   290
        (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun) 1)
clasohm@1461
   291
        ]);
nipkow@243
   292
nipkow@243
   293
slotosch@2640
   294
qed_goalw "contlub_Ifix" thy  [contlub,Ifix_def] "contlub(Ifix)"
nipkow@243
   295
 (fn prems =>
clasohm@1461
   296
        [
clasohm@1461
   297
        (strip_tac 1),
paulson@2033
   298
        (stac (contlub_Ifix_lemma1 RS ext) 1),
clasohm@1461
   299
        (atac 1),
clasohm@1461
   300
        (etac ex_lub_iterate 1)
clasohm@1461
   301
        ]);
nipkow@243
   302
nipkow@243
   303
slotosch@2640
   304
qed_goal "cont_Ifix" thy "cont(Ifix)"
nipkow@243
   305
 (fn prems =>
clasohm@1461
   306
        [
clasohm@1461
   307
        (rtac monocontlub2cont 1),
clasohm@1461
   308
        (rtac monofun_Ifix 1),
clasohm@1461
   309
        (rtac contlub_Ifix 1)
clasohm@1461
   310
        ]);
nipkow@243
   311
nipkow@243
   312
(* ------------------------------------------------------------------------ *)
nipkow@243
   313
(* propagate properties of Ifix to its continuous counterpart               *)
nipkow@243
   314
(* ------------------------------------------------------------------------ *)
nipkow@243
   315
slotosch@2640
   316
qed_goalw "fix_eq" thy  [fix_def] "fix`F = F`(fix`F)"
nipkow@243
   317
 (fn prems =>
clasohm@1461
   318
        [
wenzelm@4098
   319
        (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1),
clasohm@1461
   320
        (rtac Ifix_eq 1)
clasohm@1461
   321
        ]);
nipkow@243
   322
slotosch@2640
   323
qed_goalw "fix_least" thy [fix_def] "F`x = x ==> fix`F << x"
nipkow@243
   324
 (fn prems =>
clasohm@1461
   325
        [
clasohm@1461
   326
        (cut_facts_tac prems 1),
wenzelm@4098
   327
        (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1),
clasohm@1461
   328
        (etac Ifix_least 1)
clasohm@1461
   329
        ]);
nipkow@243
   330
nipkow@243
   331
slotosch@2640
   332
qed_goal "fix_eqI" thy
regensbu@1274
   333
"[| F`x = x; !z. F`z = z --> x << z |] ==> x = fix`F"
regensbu@1274
   334
 (fn prems =>
clasohm@1461
   335
        [
clasohm@1461
   336
        (cut_facts_tac prems 1),
clasohm@1461
   337
        (rtac antisym_less 1),
clasohm@1461
   338
        (etac allE 1),
clasohm@1461
   339
        (etac mp 1),
clasohm@1461
   340
        (rtac (fix_eq RS sym) 1),
clasohm@1461
   341
        (etac fix_least 1)
clasohm@1461
   342
        ]);
regensbu@1274
   343
regensbu@1274
   344
slotosch@2640
   345
qed_goal "fix_eq2" thy "f == fix`F ==> f = F`f"
nipkow@243
   346
 (fn prems =>
clasohm@1461
   347
        [
clasohm@1461
   348
        (rewrite_goals_tac prems),
clasohm@1461
   349
        (rtac fix_eq 1)
clasohm@1461
   350
        ]);
nipkow@243
   351
slotosch@2640
   352
qed_goal "fix_eq3" thy "f == fix`F ==> f`x = F`f`x"
nipkow@243
   353
 (fn prems =>
clasohm@1461
   354
        [
clasohm@1461
   355
        (rtac trans 1),
clasohm@1461
   356
        (rtac ((hd prems) RS fix_eq2 RS cfun_fun_cong) 1),
clasohm@1461
   357
        (rtac refl 1)
clasohm@1461
   358
        ]);
nipkow@243
   359
nipkow@243
   360
fun fix_tac3 thm i  = ((rtac trans i) THEN (rtac (thm RS fix_eq3) i)); 
nipkow@243
   361
slotosch@2640
   362
qed_goal "fix_eq4" thy "f = fix`F ==> f = F`f"
nipkow@243
   363
 (fn prems =>
clasohm@1461
   364
        [
clasohm@1461
   365
        (cut_facts_tac prems 1),
clasohm@1461
   366
        (hyp_subst_tac 1),
clasohm@1461
   367
        (rtac fix_eq 1)
clasohm@1461
   368
        ]);
nipkow@243
   369
slotosch@2640
   370
qed_goal "fix_eq5" thy "f = fix`F ==> f`x = F`f`x"
nipkow@243
   371
 (fn prems =>
clasohm@1461
   372
        [
clasohm@1461
   373
        (rtac trans 1),
clasohm@1461
   374
        (rtac ((hd prems) RS fix_eq4 RS cfun_fun_cong) 1),
clasohm@1461
   375
        (rtac refl 1)
clasohm@1461
   376
        ]);
nipkow@243
   377
nipkow@243
   378
fun fix_tac5 thm i  = ((rtac trans i) THEN (rtac (thm RS fix_eq5) i)); 
nipkow@243
   379
oheimb@3652
   380
(* proves the unfolding theorem for function equations f = fix`... *)
oheimb@3652
   381
fun fix_prover thy fixeq s = prove_goal thy s (fn prems => [
nipkow@243
   382
        (rtac trans 1),
oheimb@3652
   383
        (rtac (fixeq RS fix_eq4) 1),
nipkow@243
   384
        (rtac trans 1),
nipkow@243
   385
        (rtac beta_cfun 1),
oheimb@2566
   386
        (Simp_tac 1)
nipkow@243
   387
        ]);
nipkow@243
   388
oheimb@3652
   389
(* proves the unfolding theorem for function definitions f == fix`... *)
oheimb@3652
   390
fun fix_prover2 thy fixdef s = prove_goal thy s (fn prems => [
clasohm@1461
   391
        (rtac trans 1),
clasohm@1461
   392
        (rtac (fix_eq2) 1),
clasohm@1461
   393
        (rtac fixdef 1),
clasohm@1461
   394
        (rtac beta_cfun 1),
oheimb@2566
   395
        (Simp_tac 1)
regensbu@1168
   396
        ]);
nipkow@243
   397
oheimb@3652
   398
(* proves an application case for a function from its unfolding thm *)
oheimb@3652
   399
fun case_prover thy unfold s = prove_goal thy s (fn prems => [
oheimb@3652
   400
	(cut_facts_tac prems 1),
oheimb@3652
   401
	(rtac trans 1),
oheimb@3652
   402
	(stac unfold 1),
paulson@4477
   403
	Auto_tac
oheimb@3652
   404
	]);
oheimb@3652
   405
nipkow@243
   406
(* ------------------------------------------------------------------------ *)
nipkow@243
   407
(* better access to definitions                                             *)
nipkow@243
   408
(* ------------------------------------------------------------------------ *)
nipkow@243
   409
nipkow@243
   410
slotosch@2640
   411
qed_goal "Ifix_def2" thy "Ifix=(%x. lub(range(%i. iterate i x UU)))"
nipkow@243
   412
 (fn prems =>
clasohm@1461
   413
        [
clasohm@1461
   414
        (rtac ext 1),
clasohm@1461
   415
        (rewtac Ifix_def),
clasohm@1461
   416
        (rtac refl 1)
clasohm@1461
   417
        ]);
nipkow@243
   418
nipkow@243
   419
(* ------------------------------------------------------------------------ *)
nipkow@243
   420
(* direct connection between fix and iteration without Ifix                 *)
nipkow@243
   421
(* ------------------------------------------------------------------------ *)
nipkow@243
   422
slotosch@2640
   423
qed_goalw "fix_def2" thy [fix_def]
regensbu@1168
   424
 "fix`F = lub(range(%i. iterate i F UU))"
nipkow@243
   425
 (fn prems =>
clasohm@1461
   426
        [
clasohm@1461
   427
        (fold_goals_tac [Ifix_def]),
wenzelm@4098
   428
        (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1)
clasohm@1461
   429
        ]);
nipkow@243
   430
nipkow@243
   431
nipkow@243
   432
(* ------------------------------------------------------------------------ *)
nipkow@243
   433
(* Lemmas about admissibility and fixed point induction                     *)
nipkow@243
   434
(* ------------------------------------------------------------------------ *)
nipkow@243
   435
nipkow@243
   436
(* ------------------------------------------------------------------------ *)
nipkow@243
   437
(* access to definitions                                                    *)
nipkow@243
   438
(* ------------------------------------------------------------------------ *)
nipkow@243
   439
nipkow@3460
   440
qed_goalw "admI" thy [adm_def]
oheimb@4720
   441
        "(!!Y. [| chain(Y); !i. P(Y(i)) |] ==> P(lub(range(Y)))) ==> adm(P)"
nipkow@3460
   442
 (fn prems => [fast_tac (HOL_cs addIs prems) 1]);
nipkow@3460
   443
nipkow@3460
   444
qed_goalw "admD" thy [adm_def]
oheimb@4720
   445
        "!!P. [| adm(P); chain(Y); !i. P(Y(i)) |] ==> P(lub(range(Y)))"
nipkow@3460
   446
 (fn prems => [fast_tac HOL_cs 1]);
nipkow@243
   447
slotosch@2640
   448
qed_goalw "admw_def2" thy [admw_def]
wenzelm@3842
   449
        "admw(P) = (!F.(!n. P(iterate n F UU)) -->\
wenzelm@3842
   450
\                        P (lub(range(%i. iterate i F UU))))"
nipkow@243
   451
 (fn prems =>
clasohm@1461
   452
        [
clasohm@1461
   453
        (rtac refl 1)
clasohm@1461
   454
        ]);
nipkow@243
   455
nipkow@243
   456
(* ------------------------------------------------------------------------ *)
nipkow@243
   457
(* an admissible formula is also weak admissible                            *)
nipkow@243
   458
(* ------------------------------------------------------------------------ *)
nipkow@243
   459
nipkow@3460
   460
qed_goalw "adm_impl_admw"  thy [admw_def] "!!P. adm(P)==>admw(P)"
nipkow@243
   461
 (fn prems =>
clasohm@1461
   462
        [
clasohm@1461
   463
        (strip_tac 1),
nipkow@3460
   464
        (etac admD 1),
oheimb@4720
   465
        (rtac chain_iterate 1),
clasohm@1461
   466
        (atac 1)
clasohm@1461
   467
        ]);
nipkow@243
   468
nipkow@243
   469
(* ------------------------------------------------------------------------ *)
nipkow@243
   470
(* fixed point induction                                                    *)
nipkow@243
   471
(* ------------------------------------------------------------------------ *)
nipkow@243
   472
slotosch@2640
   473
qed_goal "fix_ind"  thy  
regensbu@1168
   474
"[| adm(P);P(UU);!!x. P(x) ==> P(F`x)|] ==> P(fix`F)"
nipkow@243
   475
 (fn prems =>
clasohm@1461
   476
        [
clasohm@1461
   477
        (cut_facts_tac prems 1),
paulson@2033
   478
        (stac fix_def2 1),
nipkow@3460
   479
        (etac admD 1),
oheimb@4720
   480
        (rtac chain_iterate 1),
clasohm@1461
   481
        (rtac allI 1),
berghofe@5192
   482
        (induct_tac "i" 1),
paulson@2033
   483
        (stac iterate_0 1),
clasohm@1461
   484
        (atac 1),
paulson@2033
   485
        (stac iterate_Suc 1),
clasohm@1461
   486
        (resolve_tac prems 1),
clasohm@1461
   487
        (atac 1)
clasohm@1461
   488
        ]);
nipkow@243
   489
slotosch@2640
   490
qed_goal "def_fix_ind" thy "[| f == fix`F; adm(P); \
oheimb@2568
   491
\       P(UU);!!x. P(x) ==> P(F`x)|] ==> P f" (fn prems => [
oheimb@2568
   492
        (cut_facts_tac prems 1),
oheimb@2568
   493
	(asm_simp_tac HOL_ss 1),
oheimb@2568
   494
	(etac fix_ind 1),
oheimb@2568
   495
	(atac 1),
oheimb@2568
   496
	(eresolve_tac prems 1)]);
oheimb@2568
   497
	
nipkow@243
   498
(* ------------------------------------------------------------------------ *)
nipkow@243
   499
(* computational induction for weak admissible formulae                     *)
nipkow@243
   500
(* ------------------------------------------------------------------------ *)
nipkow@243
   501
slotosch@2640
   502
qed_goal "wfix_ind"  thy  
regensbu@1168
   503
"[| admw(P); !n. P(iterate n F UU)|] ==> P(fix`F)"
nipkow@243
   504
 (fn prems =>
clasohm@1461
   505
        [
clasohm@1461
   506
        (cut_facts_tac prems 1),
paulson@2033
   507
        (stac fix_def2 1),
clasohm@1461
   508
        (rtac (admw_def2 RS iffD1 RS spec RS mp) 1),
clasohm@1461
   509
        (atac 1),
clasohm@1461
   510
        (rtac allI 1),
clasohm@1461
   511
        (etac spec 1)
clasohm@1461
   512
        ]);
nipkow@243
   513
slotosch@2640
   514
qed_goal "def_wfix_ind" thy "[| f == fix`F; admw(P); \
oheimb@2568
   515
\       !n. P(iterate n F UU) |] ==> P f" (fn prems => [
oheimb@2568
   516
        (cut_facts_tac prems 1),
oheimb@2568
   517
	(asm_simp_tac HOL_ss 1),
oheimb@2568
   518
	(etac wfix_ind 1),
oheimb@2568
   519
	(atac 1)]);
oheimb@2568
   520
nipkow@243
   521
(* ------------------------------------------------------------------------ *)
nipkow@243
   522
(* for chain-finite (easy) types every formula is admissible                *)
nipkow@243
   523
(* ------------------------------------------------------------------------ *)
nipkow@243
   524
slotosch@2640
   525
qed_goalw "adm_max_in_chain"  thy  [adm_def]
oheimb@4720
   526
"!Y. chain(Y::nat=>'a) --> (? n. max_in_chain n Y) ==> adm(P::'a=>bool)"
nipkow@243
   527
 (fn prems =>
clasohm@1461
   528
        [
clasohm@1461
   529
        (cut_facts_tac prems 1),
clasohm@1461
   530
        (strip_tac 1),
clasohm@1461
   531
        (rtac exE 1),
clasohm@1461
   532
        (rtac mp 1),
clasohm@1461
   533
        (etac spec 1),
clasohm@1461
   534
        (atac 1),
paulson@2033
   535
        (stac (lub_finch1 RS thelubI) 1),
clasohm@1461
   536
        (atac 1),
clasohm@1461
   537
        (atac 1),
clasohm@1461
   538
        (etac spec 1)
clasohm@1461
   539
        ]);
nipkow@243
   540
oheimb@4720
   541
bind_thm ("adm_chfin" ,chfin RS adm_max_in_chain);
nipkow@243
   542
nipkow@243
   543
(* ------------------------------------------------------------------------ *)
oheimb@4720
   544
(* some lemmata for functions with flat/chfin domain/range types	    *)
sandnerr@2354
   545
(* ------------------------------------------------------------------------ *)
sandnerr@2354
   546
slotosch@3324
   547
qed_goalw "adm_chfindom" thy [adm_def] "adm (%(u::'a::cpo->'b::chfin). P(u`s))"
slotosch@3324
   548
    (fn _ => [
sandnerr@2354
   549
	strip_tac 1,
slotosch@5291
   550
	dtac chfin_Rep_CFunR 1,
sandnerr@2354
   551
	eres_inst_tac [("x","s")] allE 1,
wenzelm@4098
   552
	fast_tac (HOL_cs addss (simpset() addsimps [chfin])) 1]);
sandnerr@2354
   553
slotosch@3324
   554
(* adm_flat not needed any more, since it is a special case of adm_chfindom *)
sandnerr@2354
   555
oheimb@1992
   556
(* ------------------------------------------------------------------------ *)
slotosch@3326
   557
(* improved admisibility introduction                                       *)
oheimb@1992
   558
(* ------------------------------------------------------------------------ *)
oheimb@1992
   559
nipkow@3460
   560
qed_goalw "admI2" thy [adm_def]
oheimb@4720
   561
 "(!!Y. [| chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j |]\
oheimb@1992
   562
\ ==> P(lub (range Y))) ==> adm P" 
oheimb@1992
   563
 (fn prems => [
paulson@2033
   564
        strip_tac 1,
paulson@2033
   565
        etac increasing_chain_adm_lemma 1, atac 1,
paulson@2033
   566
        eresolve_tac prems 1, atac 1, atac 1]);
oheimb@1992
   567
oheimb@1992
   568
nipkow@243
   569
(* ------------------------------------------------------------------------ *)
nipkow@243
   570
(* admissibility of special formulae and propagation                        *)
nipkow@243
   571
(* ------------------------------------------------------------------------ *)
nipkow@243
   572
slotosch@2640
   573
qed_goalw "adm_less"  thy [adm_def]
wenzelm@3842
   574
        "[|cont u;cont v|]==> adm(%x. u x << v x)"
nipkow@243
   575
 (fn prems =>
clasohm@1461
   576
        [
clasohm@1461
   577
        (cut_facts_tac prems 1),
clasohm@1461
   578
        (strip_tac 1),
clasohm@1461
   579
        (etac (cont2contlub RS contlubE RS spec RS mp RS ssubst) 1),
clasohm@1461
   580
        (atac 1),
clasohm@1461
   581
        (etac (cont2contlub RS contlubE RS spec RS mp RS ssubst) 1),
clasohm@1461
   582
        (atac 1),
clasohm@1461
   583
        (rtac lub_mono 1),
clasohm@1461
   584
        (cut_facts_tac prems 1),
clasohm@1461
   585
        (etac (cont2mono RS ch2ch_monofun) 1),
clasohm@1461
   586
        (atac 1),
clasohm@1461
   587
        (cut_facts_tac prems 1),
clasohm@1461
   588
        (etac (cont2mono RS ch2ch_monofun) 1),
clasohm@1461
   589
        (atac 1),
clasohm@1461
   590
        (atac 1)
clasohm@1461
   591
        ]);
nipkow@3460
   592
Addsimps [adm_less];
nipkow@243
   593
slotosch@2640
   594
qed_goal "adm_conj"  thy  
nipkow@3460
   595
        "!!P. [| adm P; adm Q |] ==> adm(%x. P x & Q x)"
nipkow@3460
   596
 (fn prems => [fast_tac (HOL_cs addEs [admD] addIs [admI]) 1]);
nipkow@3460
   597
Addsimps [adm_conj];
nipkow@3460
   598
wenzelm@3842
   599
qed_goalw "adm_not_free"  thy [adm_def] "adm(%x. t)"
nipkow@3460
   600
 (fn prems => [fast_tac HOL_cs 1]);
nipkow@3460
   601
Addsimps [adm_not_free];
nipkow@3460
   602
nipkow@3460
   603
qed_goalw "adm_not_less"  thy [adm_def]
nipkow@3460
   604
        "!!t. cont t ==> adm(%x.~ (t x) << u)"
nipkow@243
   605
 (fn prems =>
clasohm@1461
   606
        [
clasohm@1461
   607
        (strip_tac 1),
clasohm@1461
   608
        (rtac contrapos 1),
clasohm@1461
   609
        (etac spec 1),
clasohm@1461
   610
        (rtac trans_less 1),
clasohm@1461
   611
        (atac 2),
clasohm@1461
   612
        (etac (cont2mono RS monofun_fun_arg) 1),
clasohm@1461
   613
        (rtac is_ub_thelub 1),
clasohm@1461
   614
        (atac 1)
clasohm@1461
   615
        ]);
nipkow@243
   616
nipkow@3460
   617
qed_goal "adm_all" thy  
wenzelm@3842
   618
        "!!P. !y. adm(P y) ==> adm(%x.!y. P y x)"
nipkow@3460
   619
 (fn prems => [fast_tac (HOL_cs addIs [admI] addEs [admD]) 1]);
nipkow@243
   620
oheimb@1779
   621
bind_thm ("adm_all2", allI RS adm_all);
nipkow@625
   622
slotosch@2640
   623
qed_goal "adm_subst"  thy  
nipkow@3460
   624
        "!!P. [|cont t; adm P|] ==> adm(%x. P (t x))"
nipkow@243
   625
 (fn prems =>
clasohm@1461
   626
        [
nipkow@3460
   627
        (rtac admI 1),
paulson@2033
   628
        (stac (cont2contlub RS contlubE RS spec RS mp) 1),
clasohm@1461
   629
        (atac 1),
clasohm@1461
   630
        (atac 1),
nipkow@3460
   631
        (etac admD 1),
nipkow@3460
   632
        (etac (cont2mono RS ch2ch_monofun) 1),
clasohm@1461
   633
        (atac 1),
clasohm@1461
   634
        (atac 1)
clasohm@1461
   635
        ]);
nipkow@243
   636
slotosch@2640
   637
qed_goal "adm_UU_not_less"  thy "adm(%x.~ UU << t(x))"
nipkow@3460
   638
 (fn prems => [Simp_tac 1]);
nipkow@3460
   639
nipkow@3460
   640
qed_goalw "adm_not_UU"  thy [adm_def] 
nipkow@3460
   641
        "!!t. cont(t)==> adm(%x.~ (t x) = UU)"
nipkow@243
   642
 (fn prems =>
clasohm@1461
   643
        [
clasohm@1461
   644
        (strip_tac 1),
clasohm@1461
   645
        (rtac contrapos 1),
clasohm@1461
   646
        (etac spec 1),
clasohm@1461
   647
        (rtac (chain_UU_I RS spec) 1),
clasohm@1461
   648
        (rtac (cont2mono RS ch2ch_monofun) 1),
clasohm@1461
   649
        (atac 1),
clasohm@1461
   650
        (atac 1),
clasohm@1461
   651
        (rtac (cont2contlub RS contlubE RS spec RS mp RS subst) 1),
clasohm@1461
   652
        (atac 1),
clasohm@1461
   653
        (atac 1),
clasohm@1461
   654
        (atac 1)
clasohm@1461
   655
        ]);
nipkow@243
   656
slotosch@2640
   657
qed_goal "adm_eq"  thy 
nipkow@3460
   658
        "!!u. [|cont u ; cont v|]==> adm(%x. u x = v x)"
wenzelm@4098
   659
 (fn prems => [asm_simp_tac (simpset() addsimps [po_eq_conv]) 1]);
nipkow@3460
   660
nipkow@243
   661
nipkow@243
   662
nipkow@243
   663
(* ------------------------------------------------------------------------ *)
nipkow@243
   664
(* admissibility for disjunction is hard to prove. It takes 10 Lemmas       *)
nipkow@243
   665
(* ------------------------------------------------------------------------ *)
nipkow@243
   666
oheimb@1992
   667
local
oheimb@1992
   668
nipkow@2619
   669
  val adm_disj_lemma1 = prove_goal HOL.thy 
wenzelm@3842
   670
  "!n. P(Y n)|Q(Y n) ==> (? i.!j. R i j --> Q(Y(j))) | (!i.? j. R i j & P(Y(j)))"
nipkow@243
   671
 (fn prems =>
clasohm@1461
   672
        [
clasohm@1461
   673
        (cut_facts_tac prems 1),
clasohm@1461
   674
        (fast_tac HOL_cs 1)
clasohm@1461
   675
        ]);
nipkow@243
   676
slotosch@2640
   677
  val adm_disj_lemma2 = prove_goal thy  
oheimb@4720
   678
  "!!Q. [| adm(Q); ? X. chain(X) & (!n. Q(X(n))) &\
oheimb@1992
   679
  \   lub(range(Y))=lub(range(X))|] ==> Q(lub(range(Y)))"
wenzelm@4098
   680
 (fn _ => [fast_tac (claset() addEs [admD] addss simpset()) 1]);
nipkow@2619
   681
oheimb@4720
   682
  val adm_disj_lemma3 = prove_goalw thy [chain]
oheimb@4720
   683
  "!!Q. chain(Y) ==> chain(%m. if m < Suc i then Y(Suc i) else Y m)"
nipkow@2619
   684
 (fn _ =>
clasohm@1461
   685
        [
nipkow@4833
   686
        Asm_simp_tac 1,
nipkow@2619
   687
        safe_tac HOL_cs,
nipkow@2619
   688
        subgoal_tac "ia = i" 1,
nipkow@2619
   689
        Asm_simp_tac 1,
nipkow@2619
   690
        trans_tac 1
clasohm@1461
   691
        ]);
nipkow@243
   692
nipkow@2619
   693
  val adm_disj_lemma4 = prove_goal Nat.thy
nipkow@2619
   694
  "!!Q. !j. i < j --> Q(Y(j))  ==> !n. Q( if n < Suc i then Y(Suc i) else Y n)"
nipkow@2619
   695
 (fn _ =>
clasohm@1461
   696
        [
nipkow@4833
   697
        Asm_simp_tac 1,
nipkow@2619
   698
        strip_tac 1,
nipkow@2619
   699
        etac allE 1,
nipkow@2619
   700
        etac mp 1,
nipkow@2619
   701
        trans_tac 1
clasohm@1461
   702
        ]);
nipkow@243
   703
slotosch@2640
   704
  val adm_disj_lemma5 = prove_goal thy
oheimb@4720
   705
  "!!Y::nat=>'a::cpo. [| chain(Y); ! j. i < j --> Q(Y(j)) |] ==>\
oheimb@1992
   706
  \       lub(range(Y)) = lub(range(%m. if m< Suc(i) then Y(Suc(i)) else Y m))"
nipkow@243
   707
 (fn prems =>
clasohm@1461
   708
        [
nipkow@2619
   709
        safe_tac (HOL_cs addSIs [lub_equal2,adm_disj_lemma3]),
wenzelm@2764
   710
        atac 2,
nipkow@4833
   711
        Asm_simp_tac 1,
nipkow@2619
   712
        res_inst_tac [("x","i")] exI 1,
nipkow@2619
   713
        strip_tac 1,
nipkow@2619
   714
        trans_tac 1
clasohm@1461
   715
        ]);
nipkow@243
   716
slotosch@2640
   717
  val adm_disj_lemma6 = prove_goal thy
oheimb@4720
   718
  "[| chain(Y::nat=>'a::cpo); ? i. ! j. i < j --> Q(Y(j)) |] ==>\
oheimb@4720
   719
  \         ? X. chain(X) & (! n. Q(X(n))) & lub(range(Y)) = lub(range(X))"
nipkow@243
   720
 (fn prems =>
clasohm@1461
   721
        [
clasohm@1461
   722
        (cut_facts_tac prems 1),
clasohm@1461
   723
        (etac exE 1),
wenzelm@3842
   724
        (res_inst_tac [("x","%m. if m<Suc(i) then Y(Suc(i)) else Y m")] exI 1),
clasohm@1461
   725
        (rtac conjI 1),
clasohm@1461
   726
        (rtac adm_disj_lemma3 1),
clasohm@1461
   727
        (atac 1),
clasohm@1461
   728
        (rtac conjI 1),
clasohm@1461
   729
        (rtac adm_disj_lemma4 1),
clasohm@1461
   730
        (atac 1),
clasohm@1461
   731
        (rtac adm_disj_lemma5 1),
clasohm@1461
   732
        (atac 1),
clasohm@1461
   733
        (atac 1)
clasohm@1461
   734
        ]);
nipkow@243
   735
slotosch@2640
   736
  val adm_disj_lemma7 = prove_goal thy 
oheimb@4720
   737
  "[| chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j))  |] ==>\
oheimb@4720
   738
  \         chain(%m. Y(Least(%j. m<j & P(Y(j)))))"
nipkow@243
   739
 (fn prems =>
clasohm@1461
   740
        [
clasohm@1461
   741
        (cut_facts_tac prems 1),
oheimb@4720
   742
        (rtac chainI 1),
clasohm@1461
   743
        (rtac allI 1),
clasohm@1461
   744
        (rtac chain_mono3 1),
clasohm@1461
   745
        (atac 1),
oheimb@1675
   746
        (rtac Least_le 1),
clasohm@1461
   747
        (rtac conjI 1),
clasohm@1461
   748
        (rtac Suc_lessD 1),
clasohm@1461
   749
        (etac allE 1),
clasohm@1461
   750
        (etac exE 1),
oheimb@1675
   751
        (rtac (LeastI RS conjunct1) 1),
clasohm@1461
   752
        (atac 1),
clasohm@1461
   753
        (etac allE 1),
clasohm@1461
   754
        (etac exE 1),
oheimb@1675
   755
        (rtac (LeastI RS conjunct2) 1),
clasohm@1461
   756
        (atac 1)
clasohm@1461
   757
        ]);
nipkow@243
   758
slotosch@2640
   759
  val adm_disj_lemma8 = prove_goal thy 
nipkow@2619
   760
  "[| ! i. ? j. i < j & P(Y(j)) |] ==> ! m. P(Y(LEAST j::nat. m<j & P(Y(j))))"
nipkow@243
   761
 (fn prems =>
clasohm@1461
   762
        [
clasohm@1461
   763
        (cut_facts_tac prems 1),
clasohm@1461
   764
        (strip_tac 1),
clasohm@1461
   765
        (etac allE 1),
clasohm@1461
   766
        (etac exE 1),
oheimb@1675
   767
        (etac (LeastI RS conjunct2) 1)
clasohm@1461
   768
        ]);
nipkow@243
   769
slotosch@2640
   770
  val adm_disj_lemma9 = prove_goal thy
oheimb@4720
   771
  "[| chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j)) |] ==>\
oheimb@1992
   772
  \         lub(range(Y)) = lub(range(%m. Y(Least(%j. m<j & P(Y(j))))))"
nipkow@243
   773
 (fn prems =>
clasohm@1461
   774
        [
clasohm@1461
   775
        (cut_facts_tac prems 1),
clasohm@1461
   776
        (rtac antisym_less 1),
clasohm@1461
   777
        (rtac lub_mono 1),
clasohm@1461
   778
        (atac 1),
clasohm@1461
   779
        (rtac adm_disj_lemma7 1),
clasohm@1461
   780
        (atac 1),
clasohm@1461
   781
        (atac 1),
clasohm@1461
   782
        (strip_tac 1),
clasohm@1461
   783
        (rtac (chain_mono RS mp) 1),
clasohm@1461
   784
        (atac 1),
clasohm@1461
   785
        (etac allE 1),
clasohm@1461
   786
        (etac exE 1),
oheimb@1675
   787
        (rtac (LeastI RS conjunct1) 1),
clasohm@1461
   788
        (atac 1),
clasohm@1461
   789
        (rtac lub_mono3 1),
clasohm@1461
   790
        (rtac adm_disj_lemma7 1),
clasohm@1461
   791
        (atac 1),
clasohm@1461
   792
        (atac 1),
clasohm@1461
   793
        (atac 1),
clasohm@1461
   794
        (strip_tac 1),
clasohm@1461
   795
        (rtac exI 1),
clasohm@1461
   796
        (rtac (chain_mono RS mp) 1),
clasohm@1461
   797
        (atac 1),
clasohm@1461
   798
        (rtac lessI 1)
clasohm@1461
   799
        ]);
nipkow@243
   800
slotosch@2640
   801
  val adm_disj_lemma10 = prove_goal thy
oheimb@4720
   802
  "[| chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j)) |] ==>\
oheimb@4720
   803
  \         ? X. chain(X) & (! n. P(X(n))) & lub(range(Y)) = lub(range(X))"
nipkow@243
   804
 (fn prems =>
clasohm@1461
   805
        [
clasohm@1461
   806
        (cut_facts_tac prems 1),
oheimb@1675
   807
        (res_inst_tac [("x","%m. Y(Least(%j. m<j & P(Y(j))))")] exI 1),
clasohm@1461
   808
        (rtac conjI 1),
clasohm@1461
   809
        (rtac adm_disj_lemma7 1),
clasohm@1461
   810
        (atac 1),
clasohm@1461
   811
        (atac 1),
clasohm@1461
   812
        (rtac conjI 1),
clasohm@1461
   813
        (rtac adm_disj_lemma8 1),
clasohm@1461
   814
        (atac 1),
clasohm@1461
   815
        (rtac adm_disj_lemma9 1),
clasohm@1461
   816
        (atac 1),
clasohm@1461
   817
        (atac 1)
clasohm@1461
   818
        ]);
nipkow@243
   819
slotosch@2640
   820
  val adm_disj_lemma12 = prove_goal thy
oheimb@4720
   821
  "[| adm(P); chain(Y);? i. ! j. i < j --> P(Y(j))|]==>P(lub(range(Y)))"
oheimb@1992
   822
 (fn prems =>
oheimb@1992
   823
        [
oheimb@1992
   824
        (cut_facts_tac prems 1),
oheimb@1992
   825
        (etac adm_disj_lemma2 1),
oheimb@1992
   826
        (etac adm_disj_lemma6 1),
oheimb@1992
   827
        (atac 1)
oheimb@1992
   828
        ]);
nipkow@430
   829
oheimb@1992
   830
in
oheimb@1992
   831
slotosch@2640
   832
val adm_lemma11 = prove_goal thy
oheimb@4720
   833
"[| adm(P); chain(Y); ! i. ? j. i < j & P(Y(j)) |]==>P(lub(range(Y)))"
nipkow@430
   834
 (fn prems =>
clasohm@1461
   835
        [
clasohm@1461
   836
        (cut_facts_tac prems 1),
clasohm@1461
   837
        (etac adm_disj_lemma2 1),
clasohm@1461
   838
        (etac adm_disj_lemma10 1),
clasohm@1461
   839
        (atac 1)
clasohm@1461
   840
        ]);
nipkow@430
   841
slotosch@2640
   842
val adm_disj = prove_goal thy  
wenzelm@3842
   843
        "!!P. [| adm P; adm Q |] ==> adm(%x. P x | Q x)"
nipkow@243
   844
 (fn prems =>
clasohm@1461
   845
        [
nipkow@3460
   846
        (rtac admI 1),
clasohm@1461
   847
        (rtac (adm_disj_lemma1 RS disjE) 1),
clasohm@1461
   848
        (atac 1),
clasohm@1461
   849
        (rtac disjI2 1),
clasohm@1461
   850
        (etac adm_disj_lemma12 1),
clasohm@1461
   851
        (atac 1),
clasohm@1461
   852
        (atac 1),
clasohm@1461
   853
        (rtac disjI1 1),
oheimb@1992
   854
        (etac adm_lemma11 1),
clasohm@1461
   855
        (atac 1),
clasohm@1461
   856
        (atac 1)
clasohm@1461
   857
        ]);
nipkow@243
   858
oheimb@1992
   859
end;
oheimb@1992
   860
oheimb@1992
   861
bind_thm("adm_lemma11",adm_lemma11);
oheimb@1992
   862
bind_thm("adm_disj",adm_disj);
nipkow@430
   863
slotosch@2640
   864
qed_goal "adm_imp"  thy  
oheimb@4720
   865
        "!!P. [| adm(%x.~(P x)); adm Q |] ==> adm(%x. P x --> Q x)" (K [
wenzelm@3842
   866
        (subgoal_tac "(%x. P x --> Q x) = (%x. ~P x | Q x)" 1),
oheimb@4720
   867
         (etac ssubst 1),
oheimb@3652
   868
         (etac adm_disj 1),
oheimb@3652
   869
         (atac 1),
oheimb@4720
   870
        (Simp_tac 1)
clasohm@1461
   871
        ]);
nipkow@243
   872
paulson@5143
   873
Goal "[| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |] \
nipkow@3460
   874
\           ==> adm (%x. P x = Q x)";
wenzelm@4423
   875
by (subgoal_tac "(%x. P x = Q x) = (%x. (P x --> Q x) & (Q x --> P x))" 1);
nipkow@3460
   876
by (Asm_simp_tac 1);
nipkow@3460
   877
by (rtac ext 1);
nipkow@3460
   878
by (fast_tac HOL_cs 1);
nipkow@3460
   879
qed"adm_iff";
nipkow@3460
   880
nipkow@3460
   881
slotosch@2640
   882
qed_goal "adm_not_conj"  thy  
oheimb@1681
   883
"[| adm (%x. ~ P x); adm (%x. ~ Q x) |] ==> adm (%x. ~ (P x & Q x))"(fn prems=>[
paulson@2033
   884
        cut_facts_tac prems 1,
paulson@2033
   885
        subgoal_tac 
paulson@2033
   886
        "(%x. ~ (P x & Q x)) = (%x. ~ P x | ~ Q x)" 1,
paulson@2033
   887
        rtac ext 2,
paulson@2033
   888
        fast_tac HOL_cs 2,
paulson@2033
   889
        etac ssubst 1,
paulson@2033
   890
        etac adm_disj 1,
paulson@2033
   891
        atac 1]);
oheimb@1675
   892
oheimb@2566
   893
val adm_lemmas = [adm_imp,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
nipkow@3460
   894
        adm_all2,adm_not_less,adm_not_free,adm_not_conj,adm_conj,adm_less,
nipkow@3460
   895
        adm_iff];
nipkow@243
   896
oheimb@2566
   897
Addsimps adm_lemmas;