src/ZF/epsilon.ML
author lcp
Fri Sep 17 16:16:38 1993 +0200 (1993-09-17)
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 14 1c0926788772
permissions -rw-r--r--
Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.
clasohm@0
     1
(*  Title: 	ZF/epsilon.ML
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
For epsilon.thy.  Epsilon induction and recursion
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
open Epsilon;
clasohm@0
    10
clasohm@0
    11
(*** Basic closure properties ***)
clasohm@0
    12
clasohm@0
    13
goalw Epsilon.thy [eclose_def] "A <= eclose(A)";
clasohm@0
    14
by (rtac (nat_rec_0 RS equalityD2 RS subset_trans) 1);
clasohm@0
    15
br (nat_0I RS UN_upper) 1;
clasohm@0
    16
val arg_subset_eclose = result();
clasohm@0
    17
clasohm@0
    18
val arg_into_eclose = arg_subset_eclose RS subsetD;
clasohm@0
    19
clasohm@0
    20
goalw Epsilon.thy [eclose_def,Transset_def] "Transset(eclose(A))";
clasohm@0
    21
by (rtac (subsetI RS ballI) 1);
clasohm@0
    22
by (etac UN_E 1);
clasohm@0
    23
by (rtac (nat_succI RS UN_I) 1);
clasohm@0
    24
by (assume_tac 1);
clasohm@0
    25
by (etac (nat_rec_succ RS ssubst) 1);
clasohm@0
    26
by (etac UnionI 1);
clasohm@0
    27
by (assume_tac 1);
clasohm@0
    28
val Transset_eclose = result();
clasohm@0
    29
clasohm@0
    30
(* x : eclose(A) ==> x <= eclose(A) *)
clasohm@0
    31
val eclose_subset = 
clasohm@0
    32
    standard (rewrite_rule [Transset_def] Transset_eclose RS bspec);
clasohm@0
    33
clasohm@0
    34
(* [| A : eclose(B); c : A |] ==> c : eclose(B) *)
clasohm@0
    35
val ecloseD = standard (eclose_subset RS subsetD);
clasohm@0
    36
clasohm@0
    37
val arg_in_eclose_sing = arg_subset_eclose RS singleton_subsetD;
clasohm@0
    38
val arg_into_eclose_sing = arg_in_eclose_sing RS ecloseD;
clasohm@0
    39
clasohm@0
    40
(* This is epsilon-induction for eclose(A); see also eclose_induct_down...
clasohm@0
    41
   [| a: eclose(A);  !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x) 
clasohm@0
    42
   |] ==> P(a) 
clasohm@0
    43
*)
clasohm@0
    44
val eclose_induct = standard (Transset_eclose RSN (2, Transset_induct));
clasohm@0
    45
clasohm@0
    46
(*Epsilon induction*)
clasohm@0
    47
val prems = goal Epsilon.thy
clasohm@0
    48
    "[| !!x. ALL y:x. P(y) ==> P(x) |]  ==>  P(a)";
clasohm@0
    49
by (rtac (arg_in_eclose_sing RS eclose_induct) 1);
clasohm@0
    50
by (eresolve_tac prems 1);
clasohm@0
    51
val eps_induct = result();
clasohm@0
    52
clasohm@0
    53
(*Perform epsilon-induction on i. *)
clasohm@0
    54
fun eps_ind_tac a = 
clasohm@0
    55
    EVERY' [res_inst_tac [("a",a)] eps_induct,
clasohm@0
    56
	    rename_last_tac a ["1"]];
clasohm@0
    57
clasohm@0
    58
clasohm@0
    59
(*** Leastness of eclose ***)
clasohm@0
    60
clasohm@0
    61
(** eclose(A) is the least transitive set including A as a subset. **)
clasohm@0
    62
clasohm@0
    63
goalw Epsilon.thy [Transset_def]
clasohm@0
    64
    "!!X A n. [| Transset(X);  A<=X;  n: nat |] ==> \
clasohm@0
    65
\             nat_rec(n, A, %m r. Union(r)) <= X";
clasohm@0
    66
by (etac nat_induct 1);
lcp@6
    67
by (asm_simp_tac (ZF_ss addsimps [nat_rec_0]) 1);
lcp@6
    68
by (asm_simp_tac (ZF_ss addsimps [nat_rec_succ]) 1);
clasohm@0
    69
by (fast_tac ZF_cs 1);
clasohm@0
    70
val eclose_least_lemma = result();
clasohm@0
    71
clasohm@0
    72
goalw Epsilon.thy [eclose_def]
clasohm@0
    73
     "!!X A. [| Transset(X);  A<=X |] ==> eclose(A) <= X";
clasohm@0
    74
br (eclose_least_lemma RS UN_least) 1;
clasohm@0
    75
by (REPEAT (assume_tac 1));
clasohm@0
    76
val eclose_least = result();
clasohm@0
    77
clasohm@0
    78
(*COMPLETELY DIFFERENT induction principle from eclose_induct!!*)
clasohm@0
    79
val [major,base,step] = goal Epsilon.thy
clasohm@0
    80
    "[| a: eclose(b);						\
clasohm@0
    81
\       !!y.   [| y: b |] ==> P(y);				\
clasohm@0
    82
\       !!y z. [| y: eclose(b);  P(y);  z: y |] ==> P(z)	\
clasohm@0
    83
\    |] ==> P(a)";
clasohm@0
    84
by (rtac (major RSN (3, eclose_least RS subsetD RS CollectD2)) 1);
clasohm@0
    85
by (rtac (CollectI RS subsetI) 2);
clasohm@0
    86
by (etac (arg_subset_eclose RS subsetD) 2);
clasohm@0
    87
by (etac base 2);
clasohm@0
    88
by (rewtac Transset_def);
clasohm@0
    89
by (fast_tac (ZF_cs addEs [step,ecloseD]) 1);
clasohm@0
    90
val eclose_induct_down = result();
clasohm@0
    91
clasohm@0
    92
goal Epsilon.thy "!!X. Transset(X) ==> eclose(X) = X";
clasohm@0
    93
be ([eclose_least, arg_subset_eclose] MRS equalityI) 1;
clasohm@0
    94
br subset_refl 1;
clasohm@0
    95
val Transset_eclose_eq_arg = result();
clasohm@0
    96
clasohm@0
    97
clasohm@0
    98
(*** Epsilon recursion ***)
clasohm@0
    99
clasohm@0
   100
(*Unused...*)
clasohm@0
   101
goal Epsilon.thy "!!A B C. [| A: eclose(B);  B: eclose(C) |] ==> A: eclose(C)";
clasohm@0
   102
by (rtac ([Transset_eclose, eclose_subset] MRS eclose_least RS subsetD) 1);
clasohm@0
   103
by (REPEAT (assume_tac 1));
clasohm@0
   104
val mem_eclose_trans = result();
clasohm@0
   105
clasohm@0
   106
(*Variant of the previous lemma in a useable form for the sequel*)
clasohm@0
   107
goal Epsilon.thy
clasohm@0
   108
    "!!A B C. [| A: eclose({B});  B: eclose({C}) |] ==> A: eclose({C})";
clasohm@0
   109
by (rtac ([Transset_eclose, singleton_subsetI] MRS eclose_least RS subsetD) 1);
clasohm@0
   110
by (REPEAT (assume_tac 1));
clasohm@0
   111
val mem_eclose_sing_trans = result();
clasohm@0
   112
clasohm@0
   113
goalw Epsilon.thy [Transset_def]
clasohm@0
   114
    "!!i j. [| Transset(i);  j:i |] ==> Memrel(i)-``{j} = j";
clasohm@0
   115
by (fast_tac (eq_cs addSIs [MemrelI] addSEs [MemrelE]) 1);
clasohm@0
   116
val under_Memrel = result();
clasohm@0
   117
clasohm@0
   118
(* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
clasohm@0
   119
val under_Memrel_eclose = Transset_eclose RS under_Memrel;
clasohm@0
   120
clasohm@0
   121
val wfrec_ssubst = standard (wf_Memrel RS wfrec RS ssubst);
clasohm@0
   122
clasohm@0
   123
val [kmemj,jmemi] = goal Epsilon.thy
clasohm@0
   124
    "[| k:eclose({j});  j:eclose({i}) |] ==> \
clasohm@0
   125
\    wfrec(Memrel(eclose({i})), k, H) = wfrec(Memrel(eclose({j})), k, H)";
clasohm@0
   126
by (rtac (kmemj RS eclose_induct) 1);
clasohm@0
   127
by (rtac wfrec_ssubst 1);
clasohm@0
   128
by (rtac wfrec_ssubst 1);
lcp@6
   129
by (asm_simp_tac (ZF_ss addsimps [under_Memrel_eclose,
lcp@6
   130
				  jmemi RSN (2,mem_eclose_sing_trans)]) 1);
clasohm@0
   131
val wfrec_eclose_eq = result();
clasohm@0
   132
clasohm@0
   133
val [prem] = goal Epsilon.thy
clasohm@0
   134
    "k: i ==> wfrec(Memrel(eclose({i})),k,H) = wfrec(Memrel(eclose({k})),k,H)";
clasohm@0
   135
by (rtac (arg_in_eclose_sing RS wfrec_eclose_eq) 1);
clasohm@0
   136
by (rtac (prem RS arg_into_eclose_sing) 1);
clasohm@0
   137
val wfrec_eclose_eq2 = result();
clasohm@0
   138
clasohm@0
   139
goalw Epsilon.thy [transrec_def]
clasohm@0
   140
    "transrec(a,H) = H(a, lam x:a. transrec(x,H))";
clasohm@0
   141
by (rtac wfrec_ssubst 1);
lcp@6
   142
by (simp_tac (ZF_ss addsimps [wfrec_eclose_eq2, arg_in_eclose_sing,
lcp@6
   143
			      under_Memrel_eclose]) 1);
clasohm@0
   144
val transrec = result();
clasohm@0
   145
clasohm@0
   146
(*Avoids explosions in proofs; resolve it with a meta-level definition.*)
clasohm@0
   147
val rew::prems = goal Epsilon.thy
clasohm@0
   148
    "[| !!x. f(x)==transrec(x,H) |] ==> f(a) = H(a, lam x:a. f(x))";
clasohm@0
   149
by (rewtac rew);
clasohm@0
   150
by (REPEAT (resolve_tac (prems@[transrec]) 1));
clasohm@0
   151
val def_transrec = result();
clasohm@0
   152
clasohm@0
   153
val prems = goal Epsilon.thy
clasohm@0
   154
    "[| !!x u. [| x:eclose({a});  u: Pi(x,B) |] ==> H(x,u) : B(x)   \
clasohm@0
   155
\    |]  ==> transrec(a,H) : B(a)";
clasohm@0
   156
by (res_inst_tac [("i", "a")] (arg_in_eclose_sing RS eclose_induct) 1);
clasohm@0
   157
by (rtac (transrec RS ssubst) 1);
clasohm@0
   158
by (REPEAT (ares_tac (prems @ [lam_type]) 1 ORELSE etac bspec 1));
clasohm@0
   159
val transrec_type = result();
clasohm@0
   160
clasohm@0
   161
goal Epsilon.thy "!!i. Ord(i) ==> eclose({i}) <= succ(i)";
clasohm@0
   162
by (etac (Ord_is_Transset RS Transset_succ RS eclose_least) 1);
clasohm@0
   163
by (rtac (succI1 RS singleton_subsetI) 1);
clasohm@0
   164
val eclose_sing_Ord = result();
clasohm@0
   165
clasohm@0
   166
val prems = goal Epsilon.thy
clasohm@0
   167
    "[| j: i;  Ord(i);  \
clasohm@0
   168
\       !!x u. [| x: i;  u: Pi(x,B) |] ==> H(x,u) : B(x)   \
clasohm@0
   169
\    |]  ==> transrec(j,H) : B(j)";
clasohm@0
   170
by (rtac transrec_type 1);
clasohm@0
   171
by (resolve_tac prems 1);
clasohm@0
   172
by (rtac (Ord_in_Ord RS eclose_sing_Ord RS subsetD RS succE) 1);
clasohm@0
   173
by (DEPTH_SOLVE (ares_tac prems 1 ORELSE eresolve_tac [ssubst,Ord_trans] 1));
clasohm@0
   174
val Ord_transrec_type = result();
clasohm@0
   175
clasohm@0
   176
(*** Rank ***)
clasohm@0
   177
clasohm@0
   178
(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
clasohm@0
   179
goal Epsilon.thy "rank(a) = (UN y:a. succ(rank(y)))";
clasohm@0
   180
by (rtac (rank_def RS def_transrec RS ssubst) 1);
lcp@6
   181
by (simp_tac ZF_ss 1);
clasohm@0
   182
val rank = result();
clasohm@0
   183
clasohm@0
   184
goal Epsilon.thy "Ord(rank(a))";
clasohm@0
   185
by (eps_ind_tac "a" 1);
clasohm@0
   186
by (rtac (rank RS ssubst) 1);
clasohm@0
   187
by (rtac (Ord_succ RS Ord_UN) 1);
clasohm@0
   188
by (etac bspec 1);
clasohm@0
   189
by (assume_tac 1);
clasohm@0
   190
val Ord_rank = result();
clasohm@0
   191
clasohm@0
   192
val [major] = goal Epsilon.thy "Ord(i) ==> rank(i) = i";
clasohm@0
   193
by (rtac (major RS trans_induct) 1);
clasohm@0
   194
by (rtac (rank RS ssubst) 1);
lcp@6
   195
by (asm_simp_tac (ZF_ss addsimps [Ord_equality]) 1);
clasohm@0
   196
val rank_of_Ord = result();
clasohm@0
   197
clasohm@0
   198
val [prem] = goal Epsilon.thy "a:b ==> rank(a) : rank(b)";
clasohm@0
   199
by (res_inst_tac [("a1","b")] (rank RS ssubst) 1);
clasohm@0
   200
by (rtac (prem RS UN_I) 1);
clasohm@0
   201
by (rtac succI1 1);
clasohm@0
   202
val rank_lt = result();
clasohm@0
   203
clasohm@0
   204
val [major] = goal Epsilon.thy "a: eclose(b) ==> rank(a) : rank(b)";
clasohm@0
   205
by (rtac (major RS eclose_induct_down) 1);
clasohm@0
   206
by (etac rank_lt 1);
clasohm@0
   207
by (etac (rank_lt RS Ord_trans) 1);
clasohm@0
   208
by (assume_tac 1);
clasohm@0
   209
by (rtac Ord_rank 1);
clasohm@0
   210
val eclose_rank_lt = result();
clasohm@0
   211
clasohm@0
   212
goal Epsilon.thy "!!a b. a<=b ==> rank(a) <= rank(b)";
clasohm@0
   213
by (rtac (rank RS ssubst) 1);
clasohm@0
   214
by (rtac (rank RS ssubst) 1);
clasohm@0
   215
by (etac UN_mono 1);
clasohm@0
   216
by (rtac subset_refl 1);
clasohm@0
   217
val rank_mono = result();
clasohm@0
   218
clasohm@0
   219
goal Epsilon.thy "rank(Pow(a)) = succ(rank(a))";
clasohm@0
   220
by (rtac (rank RS trans) 1);
clasohm@0
   221
by (rtac equalityI 1);
clasohm@0
   222
by (fast_tac ZF_cs 2);
clasohm@0
   223
by (rtac UN_least 1);
clasohm@0
   224
by (etac (PowD RS rank_mono RS Ord_succ_mono) 1);
clasohm@0
   225
by (rtac Ord_rank 1);
clasohm@0
   226
by (rtac Ord_rank 1);
clasohm@0
   227
val rank_Pow = result();
clasohm@0
   228
clasohm@0
   229
goal Epsilon.thy "rank(0) = 0";
clasohm@0
   230
by (rtac (rank RS trans) 1);
clasohm@0
   231
by (fast_tac (ZF_cs addSIs [equalityI]) 1);
clasohm@0
   232
val rank_0 = result();
clasohm@0
   233
clasohm@0
   234
goal Epsilon.thy "rank(succ(x)) = succ(rank(x))";
clasohm@0
   235
by (rtac (rank RS trans) 1);
clasohm@0
   236
br ([UN_least, succI1 RS UN_upper] MRS equalityI) 1;
clasohm@0
   237
be succE 1;
clasohm@0
   238
by (fast_tac ZF_cs 1);
clasohm@0
   239
by (REPEAT (ares_tac [Ord_succ_mono,Ord_rank,OrdmemD,rank_lt] 1));
clasohm@0
   240
val rank_succ = result();
clasohm@0
   241
clasohm@0
   242
goal Epsilon.thy "rank(Union(A)) = (UN x:A. rank(x))";
clasohm@0
   243
by (rtac equalityI 1);
clasohm@0
   244
by (rtac (rank_mono RS UN_least) 2);
clasohm@0
   245
by (etac Union_upper 2);
clasohm@0
   246
by (rtac (rank RS ssubst) 1);
clasohm@0
   247
by (rtac UN_least 1);
clasohm@0
   248
by (etac UnionE 1);
clasohm@0
   249
by (rtac subset_trans 1);
clasohm@0
   250
by (etac (RepFunI RS Union_upper) 2);
clasohm@0
   251
by (etac (rank_lt RS Ord_succ_subsetI) 1);
clasohm@0
   252
by (rtac Ord_rank 1);
clasohm@0
   253
val rank_Union = result();
clasohm@0
   254
clasohm@0
   255
goal Epsilon.thy "rank(eclose(a)) = rank(a)";
clasohm@0
   256
by (rtac equalityI 1);
clasohm@0
   257
by (rtac (arg_subset_eclose RS rank_mono) 2);
clasohm@0
   258
by (res_inst_tac [("a1","eclose(a)")] (rank RS ssubst) 1);
clasohm@0
   259
by (rtac UN_least 1);
clasohm@0
   260
by (etac ([eclose_rank_lt, Ord_rank] MRS Ord_succ_subsetI) 1);
clasohm@0
   261
val rank_eclose = result();
clasohm@0
   262
clasohm@0
   263
(*  [| i: j; j: rank(a) |] ==> i: rank(a)  *)
clasohm@0
   264
val rank_trans = Ord_rank RSN (3, Ord_trans);
clasohm@0
   265
clasohm@0
   266
goalw Epsilon.thy [Pair_def] "rank(a) : rank(<a,b>)";
clasohm@0
   267
by (rtac (consI1 RS rank_lt RS Ord_trans) 1);
clasohm@0
   268
by (rtac (consI1 RS consI2 RS rank_lt) 1);
clasohm@0
   269
by (rtac Ord_rank 1);
clasohm@0
   270
val rank_pair1 = result();
clasohm@0
   271
clasohm@0
   272
goalw Epsilon.thy [Pair_def] "rank(b) : rank(<a,b>)";
clasohm@0
   273
by (rtac (consI1 RS consI2 RS rank_lt RS Ord_trans) 1);
clasohm@0
   274
by (rtac (consI1 RS consI2 RS rank_lt) 1);
clasohm@0
   275
by (rtac Ord_rank 1);
clasohm@0
   276
val rank_pair2 = result();
clasohm@0
   277
clasohm@0
   278
goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inl_def] "rank(a) : rank(Inl(a))";
clasohm@0
   279
by (rtac rank_pair2 1);
clasohm@0
   280
val rank_Inl = result();
clasohm@0
   281
clasohm@0
   282
goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inr_def] "rank(a) : rank(Inr(a))";
clasohm@0
   283
by (rtac rank_pair2 1);
clasohm@0
   284
val rank_Inr = result();
clasohm@0
   285
clasohm@0
   286
val [major] = goal Epsilon.thy "i: rank(a) ==> (EX x:a. i<=rank(x))";
clasohm@0
   287
by (resolve_tac ([major] RL [rank RS subst] RL [UN_E]) 1);
clasohm@0
   288
by (rtac bexI 1);
clasohm@0
   289
by (etac member_succD 1);
clasohm@0
   290
by (rtac Ord_rank 1);
clasohm@0
   291
by (assume_tac 1);
clasohm@0
   292
val rank_implies_mem = result();
clasohm@0
   293
clasohm@0
   294
clasohm@0
   295
(*** Corollaries of leastness ***)
clasohm@0
   296
clasohm@0
   297
goal Epsilon.thy "!!A B. A:B ==> eclose(A)<=eclose(B)";
clasohm@0
   298
by (rtac (Transset_eclose RS eclose_least) 1);
clasohm@0
   299
by (etac (arg_into_eclose RS eclose_subset) 1);
clasohm@0
   300
val mem_eclose_subset = result();
clasohm@0
   301
clasohm@0
   302
goal Epsilon.thy "!!A B. A<=B ==> eclose(A) <= eclose(B)";
clasohm@0
   303
by (rtac (Transset_eclose RS eclose_least) 1);
clasohm@0
   304
by (etac subset_trans 1);
clasohm@0
   305
by (rtac arg_subset_eclose 1);
clasohm@0
   306
val eclose_mono = result();
clasohm@0
   307
clasohm@0
   308
(** Idempotence of eclose **)
clasohm@0
   309
clasohm@0
   310
goal Epsilon.thy "eclose(eclose(A)) = eclose(A)";
clasohm@0
   311
by (rtac equalityI 1);
clasohm@0
   312
by (rtac ([Transset_eclose, subset_refl] MRS eclose_least) 1);
clasohm@0
   313
by (rtac arg_subset_eclose 1);
clasohm@0
   314
val eclose_idem = result();