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