src/ZF/epsilon.ML
author lcp
Thu, 30 Sep 1993 10:10:21 +0100
changeset 14 1c0926788772
parent 6 8ce8c4d13d4d
child 25 3ac1c0c0016e
permissions -rw-r--r--
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext domrange/image_subset,vimage_subset: deleted needless premise! misc: This slightly simplifies two proofs in Schroeder-Bernstein Theorem ind-syntax/rule_concl: recoded to avoid exceptions intr-elim: now checks conclusions of introduction rules func/fun_disjoint_Un: now uses ex_ex1I list-fn/hd,tl,drop: new simpdata/bquant_simps: new list/list_case_type: restored! bool.thy: changed 1 from a "def" to a translation Removed occurreces of one_def in bool.ML, nat.ML, univ.ML, ex/integ.ML nat/succ_less_induct: new induction principle arith/add_mono: new results about monotonicity simpdata/mem_simps: removed the ones for succ and cons; added succI1, consI2 to ZF_ss upair/succ_iff: new, for use with simp_tac (cons_iff already existed) ordinal/Ord_0_in_succ: renamed from Ord_0_mem_succ nat/nat_0_in_succ: new ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed
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);
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    15
by (rtac (nat_0I RS UN_upper) 1);
0
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";
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    74
by (rtac (eclose_least_lemma RS UN_least) 1);
0
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";
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    93
by (etac ([eclose_least, arg_subset_eclose] MRS equalityI) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    94
by (rtac subset_refl 1);
0
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);
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   236
by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   237
by (etac succE 1);
0
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();