src/ZF/Epsilon.ML
author paulson
Fri Jan 29 17:08:20 1999 +0100 (1999-01-29)
changeset 6163 be8234f37e48
parent 6071 1b2392ac5752
child 8127 68c6159440f1
permissions -rw-r--r--
expandshort
clasohm@1461
     1
(*  Title:      ZF/epsilon.ML
clasohm@0
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
paulson@5809
     6
Epsilon induction and recursion
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
(*** Basic closure properties ***)
clasohm@0
    10
wenzelm@5067
    11
Goalw [eclose_def] "A <= eclose(A)";
clasohm@0
    12
by (rtac (nat_rec_0 RS equalityD2 RS subset_trans) 1);
lcp@14
    13
by (rtac (nat_0I RS UN_upper) 1);
clasohm@760
    14
qed "arg_subset_eclose";
clasohm@0
    15
clasohm@0
    16
val arg_into_eclose = arg_subset_eclose RS subsetD;
clasohm@0
    17
wenzelm@5067
    18
Goalw [eclose_def,Transset_def] "Transset(eclose(A))";
clasohm@0
    19
by (rtac (subsetI RS ballI) 1);
clasohm@0
    20
by (etac UN_E 1);
clasohm@0
    21
by (rtac (nat_succI RS UN_I) 1);
clasohm@0
    22
by (assume_tac 1);
clasohm@0
    23
by (etac (nat_rec_succ RS ssubst) 1);
clasohm@0
    24
by (etac UnionI 1);
clasohm@0
    25
by (assume_tac 1);
clasohm@760
    26
qed "Transset_eclose";
clasohm@0
    27
clasohm@0
    28
(* x : eclose(A) ==> x <= eclose(A) *)
clasohm@782
    29
bind_thm ("eclose_subset",
clasohm@782
    30
    rewrite_rule [Transset_def] Transset_eclose RS bspec);
clasohm@0
    31
clasohm@0
    32
(* [| A : eclose(B); c : A |] ==> c : eclose(B) *)
clasohm@782
    33
bind_thm ("ecloseD", eclose_subset RS subsetD);
clasohm@0
    34
clasohm@0
    35
val arg_in_eclose_sing = arg_subset_eclose RS singleton_subsetD;
clasohm@0
    36
val arg_into_eclose_sing = arg_in_eclose_sing RS ecloseD;
clasohm@0
    37
clasohm@0
    38
(* This is epsilon-induction for eclose(A); see also eclose_induct_down...
clasohm@0
    39
   [| a: eclose(A);  !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x) 
clasohm@0
    40
   |] ==> P(a) 
clasohm@0
    41
*)
clasohm@782
    42
bind_thm ("eclose_induct", Transset_eclose RSN (2, Transset_induct));
clasohm@0
    43
clasohm@0
    44
(*Epsilon induction*)
clasohm@0
    45
val prems = goal Epsilon.thy
clasohm@0
    46
    "[| !!x. ALL y:x. P(y) ==> P(x) |]  ==>  P(a)";
clasohm@0
    47
by (rtac (arg_in_eclose_sing RS eclose_induct) 1);
clasohm@0
    48
by (eresolve_tac prems 1);
clasohm@760
    49
qed "eps_induct";
clasohm@0
    50
clasohm@0
    51
(*Perform epsilon-induction on i. *)
clasohm@0
    52
fun eps_ind_tac a = 
clasohm@0
    53
    EVERY' [res_inst_tac [("a",a)] eps_induct,
clasohm@1461
    54
            rename_last_tac a ["1"]];
clasohm@0
    55
clasohm@0
    56
clasohm@0
    57
(*** Leastness of eclose ***)
clasohm@0
    58
clasohm@0
    59
(** eclose(A) is the least transitive set including A as a subset. **)
clasohm@0
    60
wenzelm@5067
    61
Goalw [Transset_def]
paulson@5147
    62
    "[| Transset(X);  A<=X;  n: nat |] ==> \
clasohm@0
    63
\             nat_rec(n, A, %m r. Union(r)) <= X";
clasohm@0
    64
by (etac nat_induct 1);
wenzelm@4091
    65
by (asm_simp_tac (simpset() addsimps [nat_rec_0]) 1);
wenzelm@4091
    66
by (asm_simp_tac (simpset() addsimps [nat_rec_succ]) 1);
paulson@3016
    67
by (Blast_tac 1);
clasohm@760
    68
qed "eclose_least_lemma";
clasohm@0
    69
wenzelm@5067
    70
Goalw [eclose_def]
paulson@5147
    71
     "[| Transset(X);  A<=X |] ==> eclose(A) <= X";
lcp@14
    72
by (rtac (eclose_least_lemma RS UN_least) 1);
clasohm@0
    73
by (REPEAT (assume_tac 1));
clasohm@760
    74
qed "eclose_least";
clasohm@0
    75
clasohm@0
    76
(*COMPLETELY DIFFERENT induction principle from eclose_induct!!*)
clasohm@0
    77
val [major,base,step] = goal Epsilon.thy
clasohm@1461
    78
    "[| a: eclose(b);                                           \
clasohm@1461
    79
\       !!y.   [| y: b |] ==> P(y);                             \
clasohm@1461
    80
\       !!y z. [| y: eclose(b);  P(y);  z: y |] ==> P(z)        \
clasohm@0
    81
\    |] ==> P(a)";
clasohm@0
    82
by (rtac (major RSN (3, eclose_least RS subsetD RS CollectD2)) 1);
clasohm@0
    83
by (rtac (CollectI RS subsetI) 2);
clasohm@0
    84
by (etac (arg_subset_eclose RS subsetD) 2);
clasohm@0
    85
by (etac base 2);
clasohm@0
    86
by (rewtac Transset_def);
wenzelm@4091
    87
by (blast_tac (claset() addIs [step,ecloseD]) 1);
clasohm@760
    88
qed "eclose_induct_down";
clasohm@0
    89
paulson@5137
    90
Goal "Transset(X) ==> eclose(X) = X";
lcp@14
    91
by (etac ([eclose_least, arg_subset_eclose] MRS equalityI) 1);
lcp@14
    92
by (rtac subset_refl 1);
clasohm@760
    93
qed "Transset_eclose_eq_arg";
clasohm@0
    94
clasohm@0
    95
clasohm@0
    96
(*** Epsilon recursion ***)
clasohm@0
    97
clasohm@0
    98
(*Unused...*)
paulson@5137
    99
Goal "[| A: eclose(B);  B: eclose(C) |] ==> A: eclose(C)";
clasohm@0
   100
by (rtac ([Transset_eclose, eclose_subset] MRS eclose_least RS subsetD) 1);
clasohm@0
   101
by (REPEAT (assume_tac 1));
clasohm@760
   102
qed "mem_eclose_trans";
clasohm@0
   103
clasohm@0
   104
(*Variant of the previous lemma in a useable form for the sequel*)
paulson@5268
   105
Goal "[| A: eclose({B});  B: eclose({C}) |] ==> A: eclose({C})";
clasohm@0
   106
by (rtac ([Transset_eclose, singleton_subsetI] MRS eclose_least RS subsetD) 1);
clasohm@0
   107
by (REPEAT (assume_tac 1));
clasohm@760
   108
qed "mem_eclose_sing_trans";
clasohm@0
   109
wenzelm@5067
   110
Goalw [Transset_def]
paulson@5147
   111
    "[| Transset(i);  j:i |] ==> Memrel(i)-``{j} = j";
wenzelm@4091
   112
by (blast_tac (claset() addSIs [MemrelI] addSEs [MemrelE]) 1);
clasohm@760
   113
qed "under_Memrel";
clasohm@0
   114
clasohm@0
   115
(* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
clasohm@0
   116
val under_Memrel_eclose = Transset_eclose RS under_Memrel;
clasohm@0
   117
paulson@2469
   118
val wfrec_ssubst = standard (wf_Memrel RS wfrec RS ssubst);
clasohm@0
   119
clasohm@0
   120
val [kmemj,jmemi] = goal Epsilon.thy
clasohm@0
   121
    "[| k:eclose({j});  j:eclose({i}) |] ==> \
clasohm@0
   122
\    wfrec(Memrel(eclose({i})), k, H) = wfrec(Memrel(eclose({j})), k, H)";
clasohm@0
   123
by (rtac (kmemj RS eclose_induct) 1);
clasohm@0
   124
by (rtac wfrec_ssubst 1);
clasohm@0
   125
by (rtac wfrec_ssubst 1);
wenzelm@4091
   126
by (asm_simp_tac (simpset() addsimps [under_Memrel_eclose,
clasohm@1461
   127
                                  jmemi RSN (2,mem_eclose_sing_trans)]) 1);
clasohm@760
   128
qed "wfrec_eclose_eq";
clasohm@0
   129
clasohm@0
   130
val [prem] = goal Epsilon.thy
clasohm@0
   131
    "k: i ==> wfrec(Memrel(eclose({i})),k,H) = wfrec(Memrel(eclose({k})),k,H)";
clasohm@0
   132
by (rtac (arg_in_eclose_sing RS wfrec_eclose_eq) 1);
clasohm@0
   133
by (rtac (prem RS arg_into_eclose_sing) 1);
clasohm@760
   134
qed "wfrec_eclose_eq2";
clasohm@0
   135
wenzelm@5067
   136
Goalw [transrec_def]
clasohm@0
   137
    "transrec(a,H) = H(a, lam x:a. transrec(x,H))";
clasohm@0
   138
by (rtac wfrec_ssubst 1);
wenzelm@4091
   139
by (simp_tac (simpset() addsimps [wfrec_eclose_eq2, arg_in_eclose_sing,
clasohm@1461
   140
                              under_Memrel_eclose]) 1);
clasohm@760
   141
qed "transrec";
clasohm@0
   142
clasohm@0
   143
(*Avoids explosions in proofs; resolve it with a meta-level definition.*)
clasohm@0
   144
val rew::prems = goal Epsilon.thy
clasohm@0
   145
    "[| !!x. f(x)==transrec(x,H) |] ==> f(a) = H(a, lam x:a. f(x))";
clasohm@0
   146
by (rewtac rew);
clasohm@0
   147
by (REPEAT (resolve_tac (prems@[transrec]) 1));
clasohm@760
   148
qed "def_transrec";
clasohm@0
   149
clasohm@0
   150
val prems = goal Epsilon.thy
clasohm@0
   151
    "[| !!x u. [| x:eclose({a});  u: Pi(x,B) |] ==> H(x,u) : B(x)   \
clasohm@0
   152
\    |]  ==> transrec(a,H) : B(a)";
clasohm@0
   153
by (res_inst_tac [("i", "a")] (arg_in_eclose_sing RS eclose_induct) 1);
paulson@2033
   154
by (stac transrec 1);
clasohm@0
   155
by (REPEAT (ares_tac (prems @ [lam_type]) 1 ORELSE etac bspec 1));
clasohm@760
   156
qed "transrec_type";
clasohm@0
   157
paulson@5137
   158
Goal "Ord(i) ==> eclose({i}) <= succ(i)";
clasohm@0
   159
by (etac (Ord_is_Transset RS Transset_succ RS eclose_least) 1);
clasohm@0
   160
by (rtac (succI1 RS singleton_subsetI) 1);
clasohm@760
   161
qed "eclose_sing_Ord";
clasohm@0
   162
clasohm@0
   163
val prems = goal Epsilon.thy
clasohm@0
   164
    "[| j: i;  Ord(i);  \
clasohm@0
   165
\       !!x u. [| x: i;  u: Pi(x,B) |] ==> H(x,u) : B(x)   \
clasohm@0
   166
\    |]  ==> transrec(j,H) : B(j)";
clasohm@0
   167
by (rtac transrec_type 1);
clasohm@0
   168
by (resolve_tac prems 1);
clasohm@0
   169
by (rtac (Ord_in_Ord RS eclose_sing_Ord RS subsetD RS succE) 1);
clasohm@0
   170
by (DEPTH_SOLVE (ares_tac prems 1 ORELSE eresolve_tac [ssubst,Ord_trans] 1));
clasohm@760
   171
qed "Ord_transrec_type";
clasohm@0
   172
clasohm@0
   173
(*** Rank ***)
clasohm@0
   174
clasohm@0
   175
(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
wenzelm@5067
   176
Goal "rank(a) = (UN y:a. succ(rank(y)))";
paulson@2033
   177
by (stac (rank_def RS def_transrec) 1);
paulson@2469
   178
by (Simp_tac 1);
clasohm@760
   179
qed "rank";
clasohm@0
   180
wenzelm@5067
   181
Goal "Ord(rank(a))";
clasohm@0
   182
by (eps_ind_tac "a" 1);
paulson@2033
   183
by (stac rank 1);
clasohm@0
   184
by (rtac (Ord_succ RS Ord_UN) 1);
clasohm@0
   185
by (etac bspec 1);
clasohm@0
   186
by (assume_tac 1);
clasohm@760
   187
qed "Ord_rank";
paulson@6071
   188
Addsimps [Ord_rank];
clasohm@0
   189
clasohm@0
   190
val [major] = goal Epsilon.thy "Ord(i) ==> rank(i) = i";
clasohm@0
   191
by (rtac (major RS trans_induct) 1);
paulson@2033
   192
by (stac rank 1);
wenzelm@4091
   193
by (asm_simp_tac (simpset() addsimps [Ord_equality]) 1);
clasohm@760
   194
qed "rank_of_Ord";
clasohm@0
   195
paulson@5137
   196
Goal "a:b ==> rank(a) < rank(b)";
clasohm@0
   197
by (res_inst_tac [("a1","b")] (rank RS ssubst) 1);
lcp@129
   198
by (etac (UN_I RS ltI) 1);
paulson@6071
   199
by (rtac Ord_UN 2);
paulson@6071
   200
by Auto_tac;
clasohm@760
   201
qed "rank_lt";
clasohm@0
   202
lcp@25
   203
val [major] = goal Epsilon.thy "a: eclose(b) ==> rank(a) < rank(b)";
clasohm@0
   204
by (rtac (major RS eclose_induct_down) 1);
clasohm@0
   205
by (etac rank_lt 1);
lcp@25
   206
by (etac (rank_lt RS lt_trans) 1);
clasohm@0
   207
by (assume_tac 1);
clasohm@760
   208
qed "eclose_rank_lt";
clasohm@0
   209
paulson@5137
   210
Goal "a<=b ==> rank(a) le rank(b)";
lcp@25
   211
by (rtac subset_imp_le 1);
paulson@2033
   212
by (stac rank 1);
paulson@2033
   213
by (stac rank 1);
paulson@6071
   214
by Auto_tac;
clasohm@760
   215
qed "rank_mono";
clasohm@0
   216
wenzelm@5067
   217
Goal "rank(Pow(a)) = succ(rank(a))";
clasohm@0
   218
by (rtac (rank RS trans) 1);
lcp@437
   219
by (rtac le_anti_sym 1);
paulson@6163
   220
by (rtac UN_upper_le 2);
paulson@6163
   221
by (rtac UN_least_le 1);
paulson@6071
   222
by (auto_tac (claset() addIs [rank_mono], simpset()));
clasohm@760
   223
qed "rank_Pow";
clasohm@0
   224
wenzelm@5067
   225
Goal "rank(0) = 0";
clasohm@0
   226
by (rtac (rank RS trans) 1);
paulson@3016
   227
by (Blast_tac 1);
clasohm@760
   228
qed "rank_0";
clasohm@0
   229
wenzelm@5067
   230
Goal "rank(succ(x)) = succ(rank(x))";
clasohm@0
   231
by (rtac (rank RS trans) 1);
lcp@14
   232
by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1);
lcp@14
   233
by (etac succE 1);
paulson@3016
   234
by (Blast_tac 1);
lcp@129
   235
by (etac (rank_lt RS leI RS succ_leI RS le_imp_subset) 1);
clasohm@760
   236
qed "rank_succ";
clasohm@0
   237
wenzelm@5067
   238
Goal "rank(Union(A)) = (UN x:A. rank(x))";
clasohm@0
   239
by (rtac equalityI 1);
lcp@25
   240
by (rtac (rank_mono RS le_imp_subset RS UN_least) 2);
clasohm@0
   241
by (etac Union_upper 2);
paulson@2033
   242
by (stac rank 1);
clasohm@0
   243
by (rtac UN_least 1);
clasohm@0
   244
by (etac UnionE 1);
clasohm@0
   245
by (rtac subset_trans 1);
clasohm@0
   246
by (etac (RepFunI RS Union_upper) 2);
lcp@25
   247
by (etac (rank_lt RS succ_leI RS le_imp_subset) 1);
clasohm@760
   248
qed "rank_Union";
clasohm@0
   249
wenzelm@5067
   250
Goal "rank(eclose(a)) = rank(a)";
lcp@437
   251
by (rtac le_anti_sym 1);
clasohm@0
   252
by (rtac (arg_subset_eclose RS rank_mono) 2);
clasohm@0
   253
by (res_inst_tac [("a1","eclose(a)")] (rank RS ssubst) 1);
lcp@25
   254
by (rtac (Ord_rank RS UN_least_le) 1);
lcp@25
   255
by (etac (eclose_rank_lt RS succ_leI) 1);
clasohm@760
   256
qed "rank_eclose";
clasohm@0
   257
wenzelm@5067
   258
Goalw [Pair_def] "rank(a) < rank(<a,b>)";
lcp@25
   259
by (rtac (consI1 RS rank_lt RS lt_trans) 1);
clasohm@0
   260
by (rtac (consI1 RS consI2 RS rank_lt) 1);
clasohm@760
   261
qed "rank_pair1";
clasohm@0
   262
wenzelm@5067
   263
Goalw [Pair_def] "rank(b) < rank(<a,b>)";
lcp@25
   264
by (rtac (consI1 RS consI2 RS rank_lt RS lt_trans) 1);
clasohm@0
   265
by (rtac (consI1 RS consI2 RS rank_lt) 1);
clasohm@760
   266
qed "rank_pair2";
clasohm@0
   267
clasohm@0
   268
(*** Corollaries of leastness ***)
clasohm@0
   269
paulson@5137
   270
Goal "A:B ==> eclose(A)<=eclose(B)";
clasohm@0
   271
by (rtac (Transset_eclose RS eclose_least) 1);
clasohm@0
   272
by (etac (arg_into_eclose RS eclose_subset) 1);
clasohm@760
   273
qed "mem_eclose_subset";
clasohm@0
   274
paulson@5137
   275
Goal "A<=B ==> eclose(A) <= eclose(B)";
clasohm@0
   276
by (rtac (Transset_eclose RS eclose_least) 1);
clasohm@0
   277
by (etac subset_trans 1);
clasohm@0
   278
by (rtac arg_subset_eclose 1);
clasohm@760
   279
qed "eclose_mono";
clasohm@0
   280
clasohm@0
   281
(** Idempotence of eclose **)
clasohm@0
   282
wenzelm@5067
   283
Goal "eclose(eclose(A)) = eclose(A)";
clasohm@0
   284
by (rtac equalityI 1);
clasohm@0
   285
by (rtac ([Transset_eclose, subset_refl] MRS eclose_least) 1);
clasohm@0
   286
by (rtac arg_subset_eclose 1);
clasohm@760
   287
qed "eclose_idem";
paulson@2469
   288
paulson@6070
   289
(** Transfinite recursion for definitions based on the 
paulson@6070
   290
    three cases of ordinals **)
paulson@2469
   291
wenzelm@5067
   292
Goal "transrec2(0,a,b) = a";
paulson@2469
   293
by (rtac (transrec2_def RS def_transrec RS trans) 1);
paulson@2469
   294
by (Simp_tac 1);
paulson@2469
   295
qed "transrec2_0";
paulson@2469
   296
wenzelm@5067
   297
Goal "(THE j. i=j) = i";
paulson@5505
   298
by (Blast_tac 1);
paulson@2469
   299
qed "THE_eq";
paulson@2469
   300
wenzelm@5067
   301
Goal "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))";
paulson@2469
   302
by (rtac (transrec2_def RS def_transrec RS trans) 1);
paulson@5137
   303
by (simp_tac (simpset() addsimps [succ_not_0, THE_eq, if_P]) 1);
paulson@3016
   304
by (Blast_tac 1);
paulson@2469
   305
qed "transrec2_succ";
paulson@2469
   306
paulson@5137
   307
Goal "Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))";
paulson@2469
   308
by (rtac (transrec2_def RS def_transrec RS trans) 1);
paulson@5137
   309
by (Simp_tac 1);
wenzelm@4091
   310
by (blast_tac (claset() addSDs [Limit_has_0] addSEs [succ_LimitE]) 1);
paulson@2469
   311
qed "transrec2_Limit";
paulson@2469
   312
paulson@2469
   313
Addsimps [transrec2_0, transrec2_succ];
paulson@3016
   314
paulson@6070
   315
paulson@6070
   316
(** recursor -- better than nat_rec; the succ case has no type requirement! **)
paulson@6070
   317
paulson@6070
   318
(*NOT suitable for rewriting*)
paulson@6070
   319
val lemma = recursor_def RS def_transrec RS trans;
paulson@6070
   320
paulson@6070
   321
Goal "recursor(a,b,0) = a";
paulson@6070
   322
by (rtac (nat_case_0 RS lemma) 1);
paulson@6070
   323
qed "recursor_0";
paulson@6070
   324
paulson@6070
   325
Goal "recursor(a,b,succ(m)) = b(m, recursor(a,b,m))";
paulson@6070
   326
by (rtac lemma 1);
paulson@6070
   327
by (Simp_tac 1);
paulson@6070
   328
qed "recursor_succ";
paulson@6070
   329
paulson@6070
   330
paulson@6070
   331
(** rec: old version for compatibility **)
paulson@6070
   332
paulson@6070
   333
Goalw [rec_def] "rec(0,a,b) = a";
paulson@6070
   334
by (rtac recursor_0 1);
paulson@6070
   335
qed "rec_0";
paulson@6070
   336
paulson@6070
   337
Goalw [rec_def] "rec(succ(m),a,b) = b(m, rec(m,a,b))";
paulson@6070
   338
by (rtac recursor_succ 1);
paulson@6070
   339
qed "rec_succ";
paulson@6070
   340
paulson@6070
   341
Addsimps [rec_0, rec_succ];
paulson@6070
   342
paulson@6070
   343
val major::prems = Goal
paulson@6070
   344
    "[| n: nat;  \
paulson@6070
   345
\       a: C(0);  \
paulson@6070
   346
\       !!m z. [| m: nat;  z: C(m) |] ==> b(m,z): C(succ(m))  \
paulson@6070
   347
\    |] ==> rec(n,a,b) : C(n)";
paulson@6070
   348
by (rtac (major RS nat_induct) 1);
paulson@6070
   349
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
paulson@6070
   350
qed "rec_type";
paulson@6070
   351