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