src/HOLCF/Fix.ML
author paulson
Wed Dec 24 10:02:30 1997 +0100 (1997-12-24 ago)
changeset 4477 b3e5857d8d99
parent 4423 a129b817b58a
child 4720 c1b83b42f65a
permissions -rw-r--r--
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
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] 
wenzelm@3842
    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  
wenzelm@3842
    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
        [
wenzelm@4098
   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),
wenzelm@4098
   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
oheimb@3652
   394
(* proves the unfolding theorem for function equations f = fix`... *)
oheimb@3652
   395
fun fix_prover thy fixeq s = prove_goal thy s (fn prems => [
nipkow@243
   396
        (rtac trans 1),
oheimb@3652
   397
        (rtac (fixeq RS fix_eq4) 1),
nipkow@243
   398
        (rtac trans 1),
nipkow@243
   399
        (rtac beta_cfun 1),
oheimb@2566
   400
        (Simp_tac 1)
nipkow@243
   401
        ]);
nipkow@243
   402
oheimb@3652
   403
(* proves the unfolding theorem for function definitions f == fix`... *)
oheimb@3652
   404
fun fix_prover2 thy fixdef s = prove_goal thy s (fn prems => [
clasohm@1461
   405
        (rtac trans 1),
clasohm@1461
   406
        (rtac (fix_eq2) 1),
clasohm@1461
   407
        (rtac fixdef 1),
clasohm@1461
   408
        (rtac beta_cfun 1),
oheimb@2566
   409
        (Simp_tac 1)
regensbu@1168
   410
        ]);
nipkow@243
   411
oheimb@3652
   412
(* proves an application case for a function from its unfolding thm *)
oheimb@3652
   413
fun case_prover thy unfold s = prove_goal thy s (fn prems => [
oheimb@3652
   414
	(cut_facts_tac prems 1),
oheimb@3652
   415
	(rtac trans 1),
oheimb@3652
   416
	(stac unfold 1),
paulson@4477
   417
	Auto_tac
oheimb@3652
   418
	]);
oheimb@3652
   419
nipkow@243
   420
(* ------------------------------------------------------------------------ *)
nipkow@243
   421
(* better access to definitions                                             *)
nipkow@243
   422
(* ------------------------------------------------------------------------ *)
nipkow@243
   423
nipkow@243
   424
slotosch@2640
   425
qed_goal "Ifix_def2" thy "Ifix=(%x. lub(range(%i. iterate i x UU)))"
nipkow@243
   426
 (fn prems =>
clasohm@1461
   427
        [
clasohm@1461
   428
        (rtac ext 1),
clasohm@1461
   429
        (rewtac Ifix_def),
clasohm@1461
   430
        (rtac refl 1)
clasohm@1461
   431
        ]);
nipkow@243
   432
nipkow@243
   433
(* ------------------------------------------------------------------------ *)
nipkow@243
   434
(* direct connection between fix and iteration without Ifix                 *)
nipkow@243
   435
(* ------------------------------------------------------------------------ *)
nipkow@243
   436
slotosch@2640
   437
qed_goalw "fix_def2" thy [fix_def]
regensbu@1168
   438
 "fix`F = lub(range(%i. iterate i F UU))"
nipkow@243
   439
 (fn prems =>
clasohm@1461
   440
        [
clasohm@1461
   441
        (fold_goals_tac [Ifix_def]),
wenzelm@4098
   442
        (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1)
clasohm@1461
   443
        ]);
nipkow@243
   444
nipkow@243
   445
nipkow@243
   446
(* ------------------------------------------------------------------------ *)
nipkow@243
   447
(* Lemmas about admissibility and fixed point induction                     *)
nipkow@243
   448
(* ------------------------------------------------------------------------ *)
nipkow@243
   449
nipkow@243
   450
(* ------------------------------------------------------------------------ *)
nipkow@243
   451
(* access to definitions                                                    *)
nipkow@243
   452
(* ------------------------------------------------------------------------ *)
nipkow@243
   453
nipkow@3460
   454
qed_goalw "admI" thy [adm_def]
wenzelm@3842
   455
        "(!!Y. [| is_chain(Y); !i. P(Y(i)) |] ==> P(lub(range(Y)))) ==> adm(P)"
nipkow@3460
   456
 (fn prems => [fast_tac (HOL_cs addIs prems) 1]);
nipkow@3460
   457
nipkow@3460
   458
qed_goalw "admD" thy [adm_def]
wenzelm@3842
   459
        "!!P. [| adm(P); is_chain(Y); !i. P(Y(i)) |] ==> P(lub(range(Y)))"
nipkow@3460
   460
 (fn prems => [fast_tac HOL_cs 1]);
nipkow@243
   461
slotosch@2640
   462
qed_goalw "admw_def2" thy [admw_def]
wenzelm@3842
   463
        "admw(P) = (!F.(!n. P(iterate n F UU)) -->\
wenzelm@3842
   464
\                        P (lub(range(%i. iterate i F UU))))"
nipkow@243
   465
 (fn prems =>
clasohm@1461
   466
        [
clasohm@1461
   467
        (rtac refl 1)
clasohm@1461
   468
        ]);
nipkow@243
   469
nipkow@243
   470
(* ------------------------------------------------------------------------ *)
nipkow@243
   471
(* an admissible formula is also weak admissible                            *)
nipkow@243
   472
(* ------------------------------------------------------------------------ *)
nipkow@243
   473
nipkow@3460
   474
qed_goalw "adm_impl_admw"  thy [admw_def] "!!P. adm(P)==>admw(P)"
nipkow@243
   475
 (fn prems =>
clasohm@1461
   476
        [
clasohm@1461
   477
        (strip_tac 1),
nipkow@3460
   478
        (etac admD 1),
clasohm@1461
   479
        (rtac is_chain_iterate 1),
clasohm@1461
   480
        (atac 1)
clasohm@1461
   481
        ]);
nipkow@243
   482
nipkow@243
   483
(* ------------------------------------------------------------------------ *)
nipkow@243
   484
(* fixed point induction                                                    *)
nipkow@243
   485
(* ------------------------------------------------------------------------ *)
nipkow@243
   486
slotosch@2640
   487
qed_goal "fix_ind"  thy  
regensbu@1168
   488
"[| adm(P);P(UU);!!x. P(x) ==> P(F`x)|] ==> P(fix`F)"
nipkow@243
   489
 (fn prems =>
clasohm@1461
   490
        [
clasohm@1461
   491
        (cut_facts_tac prems 1),
paulson@2033
   492
        (stac fix_def2 1),
nipkow@3460
   493
        (etac admD 1),
clasohm@1461
   494
        (rtac is_chain_iterate 1),
clasohm@1461
   495
        (rtac allI 1),
clasohm@1461
   496
        (nat_ind_tac "i" 1),
paulson@2033
   497
        (stac iterate_0 1),
clasohm@1461
   498
        (atac 1),
paulson@2033
   499
        (stac iterate_Suc 1),
clasohm@1461
   500
        (resolve_tac prems 1),
clasohm@1461
   501
        (atac 1)
clasohm@1461
   502
        ]);
nipkow@243
   503
slotosch@2640
   504
qed_goal "def_fix_ind" thy "[| f == fix`F; adm(P); \
oheimb@2568
   505
\       P(UU);!!x. P(x) ==> P(F`x)|] ==> P f" (fn prems => [
oheimb@2568
   506
        (cut_facts_tac prems 1),
oheimb@2568
   507
	(asm_simp_tac HOL_ss 1),
oheimb@2568
   508
	(etac fix_ind 1),
oheimb@2568
   509
	(atac 1),
oheimb@2568
   510
	(eresolve_tac prems 1)]);
oheimb@2568
   511
	
nipkow@243
   512
(* ------------------------------------------------------------------------ *)
nipkow@243
   513
(* computational induction for weak admissible formulae                     *)
nipkow@243
   514
(* ------------------------------------------------------------------------ *)
nipkow@243
   515
slotosch@2640
   516
qed_goal "wfix_ind"  thy  
regensbu@1168
   517
"[| admw(P); !n. P(iterate n F UU)|] ==> P(fix`F)"
nipkow@243
   518
 (fn prems =>
clasohm@1461
   519
        [
clasohm@1461
   520
        (cut_facts_tac prems 1),
paulson@2033
   521
        (stac fix_def2 1),
clasohm@1461
   522
        (rtac (admw_def2 RS iffD1 RS spec RS mp) 1),
clasohm@1461
   523
        (atac 1),
clasohm@1461
   524
        (rtac allI 1),
clasohm@1461
   525
        (etac spec 1)
clasohm@1461
   526
        ]);
nipkow@243
   527
slotosch@2640
   528
qed_goal "def_wfix_ind" thy "[| f == fix`F; admw(P); \
oheimb@2568
   529
\       !n. P(iterate n F UU) |] ==> P f" (fn prems => [
oheimb@2568
   530
        (cut_facts_tac prems 1),
oheimb@2568
   531
	(asm_simp_tac HOL_ss 1),
oheimb@2568
   532
	(etac wfix_ind 1),
oheimb@2568
   533
	(atac 1)]);
oheimb@2568
   534
nipkow@243
   535
(* ------------------------------------------------------------------------ *)
nipkow@243
   536
(* for chain-finite (easy) types every formula is admissible                *)
nipkow@243
   537
(* ------------------------------------------------------------------------ *)
nipkow@243
   538
slotosch@2640
   539
qed_goalw "adm_max_in_chain"  thy  [adm_def]
wenzelm@3842
   540
"!Y. is_chain(Y::nat=>'a) --> (? n. max_in_chain n Y) ==> adm(P::'a=>bool)"
nipkow@243
   541
 (fn prems =>
clasohm@1461
   542
        [
clasohm@1461
   543
        (cut_facts_tac prems 1),
clasohm@1461
   544
        (strip_tac 1),
clasohm@1461
   545
        (rtac exE 1),
clasohm@1461
   546
        (rtac mp 1),
clasohm@1461
   547
        (etac spec 1),
clasohm@1461
   548
        (atac 1),
paulson@2033
   549
        (stac (lub_finch1 RS thelubI) 1),
clasohm@1461
   550
        (atac 1),
clasohm@1461
   551
        (atac 1),
clasohm@1461
   552
        (etac spec 1)
clasohm@1461
   553
        ]);
nipkow@243
   554
slotosch@3324
   555
bind_thm ("adm_chain_finite" ,chfin RS adm_max_in_chain);
nipkow@243
   556
nipkow@243
   557
(* ------------------------------------------------------------------------ *)
sandnerr@2354
   558
(* some lemmata for functions with flat/chain_finite domain/range types	    *)
sandnerr@2354
   559
(* ------------------------------------------------------------------------ *)
sandnerr@2354
   560
slotosch@3324
   561
qed_goalw "adm_chfindom" thy [adm_def] "adm (%(u::'a::cpo->'b::chfin). P(u`s))"
slotosch@3324
   562
    (fn _ => [
sandnerr@2354
   563
	strip_tac 1,
sandnerr@2354
   564
	dtac chfin_fappR 1,
sandnerr@2354
   565
	eres_inst_tac [("x","s")] allE 1,
wenzelm@4098
   566
	fast_tac (HOL_cs addss (simpset() addsimps [chfin])) 1]);
sandnerr@2354
   567
slotosch@3324
   568
(* adm_flat not needed any more, since it is a special case of adm_chfindom *)
sandnerr@2354
   569
oheimb@1992
   570
(* ------------------------------------------------------------------------ *)
slotosch@3326
   571
(* improved admisibility introduction                                       *)
oheimb@1992
   572
(* ------------------------------------------------------------------------ *)
oheimb@1992
   573
nipkow@3460
   574
qed_goalw "admI2" thy [adm_def]
oheimb@1992
   575
 "(!!Y. [| is_chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j |]\
oheimb@1992
   576
\ ==> P(lub (range Y))) ==> adm P" 
oheimb@1992
   577
 (fn prems => [
paulson@2033
   578
        strip_tac 1,
paulson@2033
   579
        etac increasing_chain_adm_lemma 1, atac 1,
paulson@2033
   580
        eresolve_tac prems 1, atac 1, atac 1]);
oheimb@1992
   581
oheimb@1992
   582
nipkow@243
   583
(* ------------------------------------------------------------------------ *)
nipkow@243
   584
(* admissibility of special formulae and propagation                        *)
nipkow@243
   585
(* ------------------------------------------------------------------------ *)
nipkow@243
   586
slotosch@2640
   587
qed_goalw "adm_less"  thy [adm_def]
wenzelm@3842
   588
        "[|cont u;cont v|]==> adm(%x. u x << v x)"
nipkow@243
   589
 (fn prems =>
clasohm@1461
   590
        [
clasohm@1461
   591
        (cut_facts_tac prems 1),
clasohm@1461
   592
        (strip_tac 1),
clasohm@1461
   593
        (etac (cont2contlub RS contlubE RS spec RS mp RS ssubst) 1),
clasohm@1461
   594
        (atac 1),
clasohm@1461
   595
        (etac (cont2contlub RS contlubE RS spec RS mp RS ssubst) 1),
clasohm@1461
   596
        (atac 1),
clasohm@1461
   597
        (rtac lub_mono 1),
clasohm@1461
   598
        (cut_facts_tac prems 1),
clasohm@1461
   599
        (etac (cont2mono RS ch2ch_monofun) 1),
clasohm@1461
   600
        (atac 1),
clasohm@1461
   601
        (cut_facts_tac prems 1),
clasohm@1461
   602
        (etac (cont2mono RS ch2ch_monofun) 1),
clasohm@1461
   603
        (atac 1),
clasohm@1461
   604
        (atac 1)
clasohm@1461
   605
        ]);
nipkow@3460
   606
Addsimps [adm_less];
nipkow@243
   607
slotosch@2640
   608
qed_goal "adm_conj"  thy  
nipkow@3460
   609
        "!!P. [| adm P; adm Q |] ==> adm(%x. P x & Q x)"
nipkow@3460
   610
 (fn prems => [fast_tac (HOL_cs addEs [admD] addIs [admI]) 1]);
nipkow@3460
   611
Addsimps [adm_conj];
nipkow@3460
   612
wenzelm@3842
   613
qed_goalw "adm_not_free"  thy [adm_def] "adm(%x. t)"
nipkow@3460
   614
 (fn prems => [fast_tac HOL_cs 1]);
nipkow@3460
   615
Addsimps [adm_not_free];
nipkow@3460
   616
nipkow@3460
   617
qed_goalw "adm_not_less"  thy [adm_def]
nipkow@3460
   618
        "!!t. cont t ==> adm(%x.~ (t x) << u)"
nipkow@243
   619
 (fn prems =>
clasohm@1461
   620
        [
clasohm@1461
   621
        (strip_tac 1),
clasohm@1461
   622
        (rtac contrapos 1),
clasohm@1461
   623
        (etac spec 1),
clasohm@1461
   624
        (rtac trans_less 1),
clasohm@1461
   625
        (atac 2),
clasohm@1461
   626
        (etac (cont2mono RS monofun_fun_arg) 1),
clasohm@1461
   627
        (rtac is_ub_thelub 1),
clasohm@1461
   628
        (atac 1)
clasohm@1461
   629
        ]);
nipkow@243
   630
nipkow@3460
   631
qed_goal "adm_all" thy  
wenzelm@3842
   632
        "!!P. !y. adm(P y) ==> adm(%x.!y. P y x)"
nipkow@3460
   633
 (fn prems => [fast_tac (HOL_cs addIs [admI] addEs [admD]) 1]);
nipkow@243
   634
oheimb@1779
   635
bind_thm ("adm_all2", allI RS adm_all);
nipkow@625
   636
slotosch@2640
   637
qed_goal "adm_subst"  thy  
nipkow@3460
   638
        "!!P. [|cont t; adm P|] ==> adm(%x. P (t x))"
nipkow@243
   639
 (fn prems =>
clasohm@1461
   640
        [
nipkow@3460
   641
        (rtac admI 1),
paulson@2033
   642
        (stac (cont2contlub RS contlubE RS spec RS mp) 1),
clasohm@1461
   643
        (atac 1),
clasohm@1461
   644
        (atac 1),
nipkow@3460
   645
        (etac admD 1),
nipkow@3460
   646
        (etac (cont2mono RS ch2ch_monofun) 1),
clasohm@1461
   647
        (atac 1),
clasohm@1461
   648
        (atac 1)
clasohm@1461
   649
        ]);
nipkow@243
   650
slotosch@2640
   651
qed_goal "adm_UU_not_less"  thy "adm(%x.~ UU << t(x))"
nipkow@3460
   652
 (fn prems => [Simp_tac 1]);
nipkow@3460
   653
nipkow@3460
   654
qed_goalw "adm_not_UU"  thy [adm_def] 
nipkow@3460
   655
        "!!t. cont(t)==> adm(%x.~ (t x) = UU)"
nipkow@243
   656
 (fn prems =>
clasohm@1461
   657
        [
clasohm@1461
   658
        (strip_tac 1),
clasohm@1461
   659
        (rtac contrapos 1),
clasohm@1461
   660
        (etac spec 1),
clasohm@1461
   661
        (rtac (chain_UU_I RS spec) 1),
clasohm@1461
   662
        (rtac (cont2mono RS ch2ch_monofun) 1),
clasohm@1461
   663
        (atac 1),
clasohm@1461
   664
        (atac 1),
clasohm@1461
   665
        (rtac (cont2contlub RS contlubE RS spec RS mp RS subst) 1),
clasohm@1461
   666
        (atac 1),
clasohm@1461
   667
        (atac 1),
clasohm@1461
   668
        (atac 1)
clasohm@1461
   669
        ]);
nipkow@243
   670
slotosch@2640
   671
qed_goal "adm_eq"  thy 
nipkow@3460
   672
        "!!u. [|cont u ; cont v|]==> adm(%x. u x = v x)"
wenzelm@4098
   673
 (fn prems => [asm_simp_tac (simpset() addsimps [po_eq_conv]) 1]);
nipkow@3460
   674
nipkow@243
   675
nipkow@243
   676
nipkow@243
   677
(* ------------------------------------------------------------------------ *)
nipkow@243
   678
(* admissibility for disjunction is hard to prove. It takes 10 Lemmas       *)
nipkow@243
   679
(* ------------------------------------------------------------------------ *)
nipkow@243
   680
oheimb@1992
   681
local
oheimb@1992
   682
nipkow@2619
   683
  val adm_disj_lemma1 = prove_goal HOL.thy 
wenzelm@3842
   684
  "!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
   685
 (fn prems =>
clasohm@1461
   686
        [
clasohm@1461
   687
        (cut_facts_tac prems 1),
clasohm@1461
   688
        (fast_tac HOL_cs 1)
clasohm@1461
   689
        ]);
nipkow@243
   690
slotosch@2640
   691
  val adm_disj_lemma2 = prove_goal thy  
wenzelm@3842
   692
  "!!Q. [| adm(Q); ? X. is_chain(X) & (!n. Q(X(n))) &\
oheimb@1992
   693
  \   lub(range(Y))=lub(range(X))|] ==> Q(lub(range(Y)))"
wenzelm@4098
   694
 (fn _ => [fast_tac (claset() addEs [admD] addss simpset()) 1]);
nipkow@2619
   695
slotosch@2640
   696
  val adm_disj_lemma3 = prove_goalw thy [is_chain]
nipkow@2619
   697
  "!!Q. is_chain(Y) ==> is_chain(%m. if m < Suc i then Y(Suc i) else Y m)"
nipkow@2619
   698
 (fn _ =>
clasohm@1461
   699
        [
wenzelm@4098
   700
        asm_simp_tac (simpset() setloop (split_tac[expand_if])) 1,
nipkow@2619
   701
        safe_tac HOL_cs,
nipkow@2619
   702
        subgoal_tac "ia = i" 1,
nipkow@2619
   703
        Asm_simp_tac 1,
nipkow@2619
   704
        trans_tac 1
clasohm@1461
   705
        ]);
nipkow@243
   706
nipkow@2619
   707
  val adm_disj_lemma4 = prove_goal Nat.thy
nipkow@2619
   708
  "!!Q. !j. i < j --> Q(Y(j))  ==> !n. Q( if n < Suc i then Y(Suc i) else Y n)"
nipkow@2619
   709
 (fn _ =>
clasohm@1461
   710
        [
wenzelm@4098
   711
        asm_simp_tac (simpset() setloop (split_tac[expand_if])) 1,
nipkow@2619
   712
        strip_tac 1,
nipkow@2619
   713
        etac allE 1,
nipkow@2619
   714
        etac mp 1,
nipkow@2619
   715
        trans_tac 1
clasohm@1461
   716
        ]);
nipkow@243
   717
slotosch@2640
   718
  val adm_disj_lemma5 = prove_goal thy
nipkow@2841
   719
  "!!Y::nat=>'a::cpo. [| is_chain(Y); ! j. i < j --> Q(Y(j)) |] ==>\
oheimb@1992
   720
  \       lub(range(Y)) = lub(range(%m. if m< Suc(i) then Y(Suc(i)) else Y m))"
nipkow@243
   721
 (fn prems =>
clasohm@1461
   722
        [
nipkow@2619
   723
        safe_tac (HOL_cs addSIs [lub_equal2,adm_disj_lemma3]),
wenzelm@2764
   724
        atac 2,
wenzelm@4098
   725
        asm_simp_tac (simpset() setloop (split_tac[expand_if])) 1,
nipkow@2619
   726
        res_inst_tac [("x","i")] exI 1,
nipkow@2619
   727
        strip_tac 1,
nipkow@2619
   728
        trans_tac 1
clasohm@1461
   729
        ]);
nipkow@243
   730
slotosch@2640
   731
  val adm_disj_lemma6 = prove_goal thy
nipkow@2841
   732
  "[| is_chain(Y::nat=>'a::cpo); ? i. ! j. i < j --> Q(Y(j)) |] ==>\
oheimb@1992
   733
  \         ? X. is_chain(X) & (! n. Q(X(n))) & lub(range(Y)) = lub(range(X))"
nipkow@243
   734
 (fn prems =>
clasohm@1461
   735
        [
clasohm@1461
   736
        (cut_facts_tac prems 1),
clasohm@1461
   737
        (etac exE 1),
wenzelm@3842
   738
        (res_inst_tac [("x","%m. if m<Suc(i) then Y(Suc(i)) else Y m")] exI 1),
clasohm@1461
   739
        (rtac conjI 1),
clasohm@1461
   740
        (rtac adm_disj_lemma3 1),
clasohm@1461
   741
        (atac 1),
clasohm@1461
   742
        (rtac conjI 1),
clasohm@1461
   743
        (rtac adm_disj_lemma4 1),
clasohm@1461
   744
        (atac 1),
clasohm@1461
   745
        (rtac adm_disj_lemma5 1),
clasohm@1461
   746
        (atac 1),
clasohm@1461
   747
        (atac 1)
clasohm@1461
   748
        ]);
nipkow@243
   749
slotosch@2640
   750
  val adm_disj_lemma7 = prove_goal thy 
nipkow@2841
   751
  "[| is_chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j))  |] ==>\
oheimb@1992
   752
  \         is_chain(%m. Y(Least(%j. m<j & P(Y(j)))))"
nipkow@243
   753
 (fn prems =>
clasohm@1461
   754
        [
clasohm@1461
   755
        (cut_facts_tac prems 1),
clasohm@1461
   756
        (rtac is_chainI 1),
clasohm@1461
   757
        (rtac allI 1),
clasohm@1461
   758
        (rtac chain_mono3 1),
clasohm@1461
   759
        (atac 1),
oheimb@1675
   760
        (rtac Least_le 1),
clasohm@1461
   761
        (rtac conjI 1),
clasohm@1461
   762
        (rtac Suc_lessD 1),
clasohm@1461
   763
        (etac allE 1),
clasohm@1461
   764
        (etac exE 1),
oheimb@1675
   765
        (rtac (LeastI RS conjunct1) 1),
clasohm@1461
   766
        (atac 1),
clasohm@1461
   767
        (etac allE 1),
clasohm@1461
   768
        (etac exE 1),
oheimb@1675
   769
        (rtac (LeastI RS conjunct2) 1),
clasohm@1461
   770
        (atac 1)
clasohm@1461
   771
        ]);
nipkow@243
   772
slotosch@2640
   773
  val adm_disj_lemma8 = prove_goal thy 
nipkow@2619
   774
  "[| ! i. ? j. i < j & P(Y(j)) |] ==> ! m. P(Y(LEAST j::nat. m<j & P(Y(j))))"
nipkow@243
   775
 (fn prems =>
clasohm@1461
   776
        [
clasohm@1461
   777
        (cut_facts_tac prems 1),
clasohm@1461
   778
        (strip_tac 1),
clasohm@1461
   779
        (etac allE 1),
clasohm@1461
   780
        (etac exE 1),
oheimb@1675
   781
        (etac (LeastI RS conjunct2) 1)
clasohm@1461
   782
        ]);
nipkow@243
   783
slotosch@2640
   784
  val adm_disj_lemma9 = prove_goal thy
nipkow@2841
   785
  "[| is_chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j)) |] ==>\
oheimb@1992
   786
  \         lub(range(Y)) = lub(range(%m. Y(Least(%j. m<j & P(Y(j))))))"
nipkow@243
   787
 (fn prems =>
clasohm@1461
   788
        [
clasohm@1461
   789
        (cut_facts_tac prems 1),
clasohm@1461
   790
        (rtac antisym_less 1),
clasohm@1461
   791
        (rtac lub_mono 1),
clasohm@1461
   792
        (atac 1),
clasohm@1461
   793
        (rtac adm_disj_lemma7 1),
clasohm@1461
   794
        (atac 1),
clasohm@1461
   795
        (atac 1),
clasohm@1461
   796
        (strip_tac 1),
clasohm@1461
   797
        (rtac (chain_mono RS mp) 1),
clasohm@1461
   798
        (atac 1),
clasohm@1461
   799
        (etac allE 1),
clasohm@1461
   800
        (etac exE 1),
oheimb@1675
   801
        (rtac (LeastI RS conjunct1) 1),
clasohm@1461
   802
        (atac 1),
clasohm@1461
   803
        (rtac lub_mono3 1),
clasohm@1461
   804
        (rtac adm_disj_lemma7 1),
clasohm@1461
   805
        (atac 1),
clasohm@1461
   806
        (atac 1),
clasohm@1461
   807
        (atac 1),
clasohm@1461
   808
        (strip_tac 1),
clasohm@1461
   809
        (rtac exI 1),
clasohm@1461
   810
        (rtac (chain_mono RS mp) 1),
clasohm@1461
   811
        (atac 1),
clasohm@1461
   812
        (rtac lessI 1)
clasohm@1461
   813
        ]);
nipkow@243
   814
slotosch@2640
   815
  val adm_disj_lemma10 = prove_goal thy
nipkow@2841
   816
  "[| is_chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j)) |] ==>\
oheimb@1992
   817
  \         ? X. is_chain(X) & (! n. P(X(n))) & lub(range(Y)) = lub(range(X))"
nipkow@243
   818
 (fn prems =>
clasohm@1461
   819
        [
clasohm@1461
   820
        (cut_facts_tac prems 1),
oheimb@1675
   821
        (res_inst_tac [("x","%m. Y(Least(%j. m<j & P(Y(j))))")] exI 1),
clasohm@1461
   822
        (rtac conjI 1),
clasohm@1461
   823
        (rtac adm_disj_lemma7 1),
clasohm@1461
   824
        (atac 1),
clasohm@1461
   825
        (atac 1),
clasohm@1461
   826
        (rtac conjI 1),
clasohm@1461
   827
        (rtac adm_disj_lemma8 1),
clasohm@1461
   828
        (atac 1),
clasohm@1461
   829
        (rtac adm_disj_lemma9 1),
clasohm@1461
   830
        (atac 1),
clasohm@1461
   831
        (atac 1)
clasohm@1461
   832
        ]);
nipkow@243
   833
slotosch@2640
   834
  val adm_disj_lemma12 = prove_goal thy
oheimb@1992
   835
  "[| adm(P); is_chain(Y);? i. ! j. i < j --> P(Y(j))|]==>P(lub(range(Y)))"
oheimb@1992
   836
 (fn prems =>
oheimb@1992
   837
        [
oheimb@1992
   838
        (cut_facts_tac prems 1),
oheimb@1992
   839
        (etac adm_disj_lemma2 1),
oheimb@1992
   840
        (etac adm_disj_lemma6 1),
oheimb@1992
   841
        (atac 1)
oheimb@1992
   842
        ]);
nipkow@430
   843
oheimb@1992
   844
in
oheimb@1992
   845
slotosch@2640
   846
val adm_lemma11 = prove_goal thy
nipkow@430
   847
"[| adm(P); is_chain(Y); ! i. ? j. i < j & P(Y(j)) |]==>P(lub(range(Y)))"
nipkow@430
   848
 (fn prems =>
clasohm@1461
   849
        [
clasohm@1461
   850
        (cut_facts_tac prems 1),
clasohm@1461
   851
        (etac adm_disj_lemma2 1),
clasohm@1461
   852
        (etac adm_disj_lemma10 1),
clasohm@1461
   853
        (atac 1)
clasohm@1461
   854
        ]);
nipkow@430
   855
slotosch@2640
   856
val adm_disj = prove_goal thy  
wenzelm@3842
   857
        "!!P. [| adm P; adm Q |] ==> adm(%x. P x | Q x)"
nipkow@243
   858
 (fn prems =>
clasohm@1461
   859
        [
nipkow@3460
   860
        (rtac admI 1),
clasohm@1461
   861
        (rtac (adm_disj_lemma1 RS disjE) 1),
clasohm@1461
   862
        (atac 1),
clasohm@1461
   863
        (rtac disjI2 1),
clasohm@1461
   864
        (etac adm_disj_lemma12 1),
clasohm@1461
   865
        (atac 1),
clasohm@1461
   866
        (atac 1),
clasohm@1461
   867
        (rtac disjI1 1),
oheimb@1992
   868
        (etac adm_lemma11 1),
clasohm@1461
   869
        (atac 1),
clasohm@1461
   870
        (atac 1)
clasohm@1461
   871
        ]);
nipkow@243
   872
oheimb@1992
   873
end;
oheimb@1992
   874
oheimb@1992
   875
bind_thm("adm_lemma11",adm_lemma11);
oheimb@1992
   876
bind_thm("adm_disj",adm_disj);
nipkow@430
   877
slotosch@2640
   878
qed_goal "adm_imp"  thy  
wenzelm@3842
   879
        "!!P. [| adm(%x.~(P x)); adm Q |] ==> adm(%x. P x --> Q x)"
nipkow@243
   880
 (fn prems =>
clasohm@1461
   881
        [
wenzelm@3842
   882
        (subgoal_tac "(%x. P x --> Q x) = (%x. ~P x | Q x)" 1),
oheimb@3652
   883
         (Asm_simp_tac 1),
oheimb@3652
   884
         (etac adm_disj 1),
oheimb@3652
   885
         (atac 1),
nipkow@3460
   886
        (rtac ext 1),
nipkow@3460
   887
        (fast_tac HOL_cs 1)
clasohm@1461
   888
        ]);
nipkow@243
   889
wenzelm@3842
   890
goal Fix.thy "!! P. [| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |] \
nipkow@3460
   891
\           ==> adm (%x. P x = Q x)";
wenzelm@4423
   892
by (subgoal_tac "(%x. P x = Q x) = (%x. (P x --> Q x) & (Q x --> P x))" 1);
nipkow@3460
   893
by (Asm_simp_tac 1);
nipkow@3460
   894
by (rtac ext 1);
nipkow@3460
   895
by (fast_tac HOL_cs 1);
nipkow@3460
   896
qed"adm_iff";
nipkow@3460
   897
nipkow@3460
   898
slotosch@2640
   899
qed_goal "adm_not_conj"  thy  
oheimb@1681
   900
"[| adm (%x. ~ P x); adm (%x. ~ Q x) |] ==> adm (%x. ~ (P x & Q x))"(fn prems=>[
paulson@2033
   901
        cut_facts_tac prems 1,
paulson@2033
   902
        subgoal_tac 
paulson@2033
   903
        "(%x. ~ (P x & Q x)) = (%x. ~ P x | ~ Q x)" 1,
paulson@2033
   904
        rtac ext 2,
paulson@2033
   905
        fast_tac HOL_cs 2,
paulson@2033
   906
        etac ssubst 1,
paulson@2033
   907
        etac adm_disj 1,
paulson@2033
   908
        atac 1]);
oheimb@1675
   909
oheimb@2566
   910
val adm_lemmas = [adm_imp,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
nipkow@3460
   911
        adm_all2,adm_not_less,adm_not_free,adm_not_conj,adm_conj,adm_less,
nipkow@3460
   912
        adm_iff];
nipkow@243
   913
oheimb@2566
   914
Addsimps adm_lemmas;