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