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