src/ZF/univ.ML
author paulson
Fri, 11 Aug 2000 13:26:40 +0200
changeset 9577 9e66e8ed8237
parent 187 8729bfdcb638
permissions -rw-r--r--
ZF arith
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/univ
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   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
The cumulative hierarchy and a small universe for recursive types
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 Univ;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
goal Univ.thy "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
by (rtac (Vfrom_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
    14
by (simp_tac ZF_ss 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
val Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
(** Monotonicity **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
goal Univ.thy "!!A B. A<=B ==> ALL j. i<=j --> Vfrom(A,i) <= Vfrom(B,j)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
by (eps_ind_tac "i" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
by (rtac (impI RS allI) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
by (etac Un_mono 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
by (rtac UN_mono 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
by (rtac Pow_mono 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
by (etac (bspec RS spec RS mp) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
by (rtac subset_refl 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
val Vfrom_mono_lemma = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
(*  [| A<=B; i<=x |] ==> Vfrom(A,i) <= Vfrom(B,x)  *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
val Vfrom_mono = standard (Vfrom_mono_lemma RS spec RS mp);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
(** A fundamental equality: Vfrom does not require ordinals! **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
goal Univ.thy "Vfrom(A,x) <= Vfrom(A,rank(x))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
by (eps_ind_tac "x" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
by (rtac (Vfrom RS ssubst) 1);
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
    43
by (fast_tac (ZF_cs addSIs [rank_lt RS ltD]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
val Vfrom_rank_subset1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
goal Univ.thy "Vfrom(A,rank(x)) <= Vfrom(A,x)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
by (eps_ind_tac "x" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
by (rtac (Vfrom RS ssubst) 1);
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    50
by (rtac (subset_refl RS Un_mono) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    51
by (rtac UN_least 1);
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
    52
(*expand rank(x1) = (UN y:x1. succ(rank(y))) in assumptions*)
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
    53
by (etac (rank RS equalityD1 RS subsetD RS UN_E) 1);
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    54
by (rtac subset_trans 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    55
by (etac UN_upper 2);
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
    56
by (rtac (subset_refl RS Vfrom_mono RS subset_trans RS Pow_mono) 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
    57
by (etac (ltI RS le_imp_subset) 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
    58
by (rtac (Ord_rank RS Ord_succ) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
by (etac bspec 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
val Vfrom_rank_subset2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
goal Univ.thy "Vfrom(A,rank(x)) = Vfrom(A,x)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
by (rtac equalityI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
by (rtac Vfrom_rank_subset2 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
by (rtac Vfrom_rank_subset1 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
val Vfrom_rank_eq = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
(*** Basic closure properties ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
goal Univ.thy "!!x y. y:x ==> 0 : Vfrom(A,x)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
val zero_in_Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
goal Univ.thy "i <= Vfrom(A,i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
by (eps_ind_tac "i" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
val i_subset_Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
goal Univ.thy "A <= Vfrom(A,i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
by (rtac Un_upper1 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
val A_subset_Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
goal Univ.thy "!!A a i. a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
val subset_mem_Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
(** Finite sets and ordered pairs **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
goal Univ.thy "!!a. a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
by (rtac subset_mem_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
by (safe_tac ZF_cs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
val singleton_in_Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
    "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> {a,b} : Vfrom(A,succ(i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
by (rtac subset_mem_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
by (safe_tac ZF_cs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
val doubleton_in_Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
goalw Univ.thy [Pair_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
    "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
\         <a,b> : Vfrom(A,succ(succ(i)))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
by (REPEAT (ares_tac [doubleton_in_Vfrom] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
val Pair_in_Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
val [prem] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
    "a<=Vfrom(A,i) ==> succ(a) : Vfrom(A,succ(succ(i)))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
by (REPEAT (resolve_tac [subset_mem_Vfrom, succ_subsetI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
by (rtac (Vfrom_mono RSN (2,subset_trans)) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
by (REPEAT (resolve_tac [prem, subset_refl, subset_succI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
val succ_in_Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
(*** 0, successor and limit equations fof Vfrom ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
goal Univ.thy "Vfrom(A,0) = A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
val Vfrom_0 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
goal Univ.thy "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
by (rtac (Vfrom RS trans) 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   128
by (rtac (succI1 RS RepFunI RS Union_upper RSN
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   129
	      (2, equalityI RS subst_context)) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
by (rtac UN_least 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
by (rtac (subset_refl RS Vfrom_mono RS Pow_mono) 1);
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   132
by (etac (ltI RS le_imp_subset) 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   133
by (etac Ord_succ 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
val Vfrom_succ_lemma = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
goal Univ.thy "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
by (res_inst_tac [("x1", "succ(i)")] (Vfrom_rank_eq RS subst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
by (res_inst_tac [("x1", "i")] (Vfrom_rank_eq RS subst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
by (rtac (rank_succ RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
by (rtac (Ord_rank RS Vfrom_succ_lemma) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
val Vfrom_succ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
(*The premise distinguishes this from Vfrom(A,0);  allowing X=0 forces
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
  the conclusion to be Vfrom(A,Union(X)) = A Un (UN y:X. Vfrom(A,y)) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
val [prem] = goal Univ.thy "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
by (rtac equalityI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
(*first inclusion*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
by (rtac Un_least 1);
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   150
by (rtac (A_subset_Vfrom RS subset_trans) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   151
by (rtac (prem RS UN_upper) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   152
by (rtac UN_least 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   153
by (etac UnionE 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   154
by (rtac subset_trans 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   155
by (etac UN_upper 2);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
by (rtac (Vfrom RS ssubst) 1);
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   157
by (etac ([UN_upper, Un_upper2] MRS subset_trans) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
(*opposite inclusion*)
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   159
by (rtac UN_least 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
val Vfrom_Union = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
(*** Limit ordinals -- general properties ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> Union(i) = i";
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   167
by (fast_tac (eq_cs addSIs [ltI] addSEs [ltE] addEs [Ord_trans]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
val Limit_Union_eq = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> Ord(i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
by (etac conjunct1 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
val Limit_is_Ord = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   174
goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> 0 < i";
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   175
by (etac (conjunct2 RS conjunct1) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
val Limit_has_0 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   178
goalw Univ.thy [Limit_def] "!!i. [| Limit(i);  j<i |] ==> succ(j) < i";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
val Limit_has_succ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
goalw Univ.thy [Limit_def] "Limit(nat)";
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   183
by (safe_tac (ZF_cs addSIs (ltI::nat_typechecks)));
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   184
by (etac ltD 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
val Limit_nat = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
goalw Univ.thy [Limit_def]
37
cebe01deba80 added ~: for "not in"
lcp
parents: 27
diff changeset
   188
    "!!i. [| 0<i;  ALL y. succ(y) ~= i |] ==> Limit(i)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
by (safe_tac subset_cs);
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   190
by (rtac (not_le_iff_lt RS iffD1) 2);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   191
by (fast_tac (lt_cs addEs [lt_anti_sym]) 4);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   192
by (REPEAT (eresolve_tac [asm_rl, ltE, Ord_succ] 1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
val non_succ_LimitI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
goal Univ.thy "!!i. Ord(i) ==> i=0 | (EX j. i=succ(j)) | Limit(i)";
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   196
by (fast_tac (ZF_cs addSIs [non_succ_LimitI, Ord_0_lt]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
val Ord_cases_lemma = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
val major::prems = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
    "[| Ord(i);			\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
\       i=0            ==> P;	\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
\       !!j. i=succ(j) ==> P;	\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
\       Limit(i)       ==> P	\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
\    |] ==> P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
by (cut_facts_tac [major RS Ord_cases_lemma] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
by (REPEAT (eresolve_tac (prems@[disjE, exE]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
val Ord_cases = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
(*** Vfrom applied to Limit ordinals ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
(*NB. limit ordinals are non-empty;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
                        Vfrom(A,0) = A = A Un (UN y:0. Vfrom(A,y)) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
val [limiti] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
    "Limit(i) ==> Vfrom(A,i) = (UN y:i. Vfrom(A,y))";
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   216
by (rtac (limiti RS (Limit_has_0 RS ltD) RS Vfrom_Union RS subst) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
by (rtac (limiti RS Limit_Union_eq RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
by (rtac refl 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
val Limit_Vfrom_eq = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   221
goal Univ.thy "!!a. [| a: Vfrom(A,j);  Limit(i);  j<i |] ==> a : Vfrom(A,i)";
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   222
by (rtac (Limit_Vfrom_eq RS equalityD2 RS subsetD) 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   223
by (REPEAT (ares_tac [ltD RS UN_I] 1));
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   224
val Limit_VfromI = result();
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   225
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   226
val prems = goal Univ.thy
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   227
    "[| a: Vfrom(A,i);  Limit(i);		\
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   228
\       !!x. [| x<i;  a: Vfrom(A,x) |] ==> R 	\
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   229
\    |] ==> R";
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   230
by (rtac (Limit_Vfrom_eq RS equalityD1 RS subsetD RS UN_E) 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   231
by (REPEAT (ares_tac (prems @ [ltI, Limit_is_Ord]) 1));
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   232
val Limit_VfromE = result();
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
val [major,limiti] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
    "[| a: Vfrom(A,i);  Limit(i) |] ==> {a} : Vfrom(A,i)";
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   236
by (rtac ([major,limiti] MRS Limit_VfromE) 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   237
by (etac ([singleton_in_Vfrom, limiti] MRS Limit_VfromI) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
by (etac (limiti RS Limit_has_succ) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
val singleton_in_Vfrom_limit = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   240
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
val Vfrom_UnI1 = Un_upper1 RS (subset_refl RS Vfrom_mono RS subsetD)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
and Vfrom_UnI2 = Un_upper2 RS (subset_refl RS Vfrom_mono RS subsetD);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
(*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
val [aprem,bprem,limiti] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
    "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
\    {a,b} : Vfrom(A,i)";
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   248
by (rtac ([aprem,limiti] MRS Limit_VfromE) 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   249
by (rtac ([bprem,limiti] MRS Limit_VfromE) 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   250
by (rtac ([doubleton_in_Vfrom, limiti] MRS Limit_VfromI) 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   251
by (etac Vfrom_UnI1 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   252
by (etac Vfrom_UnI2 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   253
by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
val doubleton_in_Vfrom_limit = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
val [aprem,bprem,limiti] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   257
    "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
\    <a,b> : Vfrom(A,i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
(*Infer that a, b occur at ordinals x,xa < i.*)
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   260
by (rtac ([aprem,limiti] MRS Limit_VfromE) 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   261
by (rtac ([bprem,limiti] MRS Limit_VfromE) 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   262
by (rtac ([Pair_in_Vfrom, limiti] MRS Limit_VfromI) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
(*Infer that succ(succ(x Un xa)) < i *)
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   264
by (etac Vfrom_UnI1 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   265
by (etac Vfrom_UnI2 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   266
by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
val Pair_in_Vfrom_limit = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
(*** Properties assuming Transset(A) ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
goal Univ.thy "!!i A. Transset(A) ==> Transset(Vfrom(A,i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
by (eps_ind_tac "i" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
by (fast_tac (ZF_cs addSIs [Transset_Union_family, Transset_Un,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
			    Transset_Pow]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
val Transset_Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
goal Univ.thy "!!A i. Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
by (rtac (Vfrom_succ RS trans) 1);
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   281
by (rtac (Un_upper2 RSN (2,equalityI)) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   282
by (rtac (subset_refl RSN (2,Un_least)) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   283
by (rtac (A_subset_Vfrom RS subset_trans) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   284
by (etac (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285
val Transset_Vfrom_succ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   286
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
goalw Ord.thy [Pair_def,Transset_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   288
    "!!C. [| <a,b> <= C; Transset(C) |] ==> a: C & b: C";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   289
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   290
val Transset_Pair_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   291
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   293
    "!!a b.[| <a,b> <= Vfrom(A,i);  Transset(A);  Limit(i) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
\          <a,b> : Vfrom(A,i)";
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   295
by (etac (Transset_Pair_subset RS conjE) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   296
by (etac Transset_Vfrom 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
by (REPEAT (ares_tac [Pair_in_Vfrom_limit] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
val Transset_Pair_subset_Vfrom_limit = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   299
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   300
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
(*** Closure under product/sum applied to elements -- thus Vfrom(A,i) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   302
     is a model of simple type theory provided A is a transitive set
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   303
     and i is a limit ordinal
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   304
***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   305
187
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   306
(*General theorem for membership in Vfrom(A,i) when i is a limit ordinal*)
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   307
val [aprem,bprem,limiti,step] = goal Univ.thy
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   308
  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);			\
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   309
\     !!x y j. [| j<i; 1:j; x: Vfrom(A,j); y: Vfrom(A,j) \
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   310
\              |] ==> EX k. h(x,y): Vfrom(A,k) & k<i |] ==> 	\
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   311
\  h(a,b) : Vfrom(A,i)";
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   312
(*Infer that a, b occur at ordinals x,xa < i.*)
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   313
by (rtac ([aprem,limiti] MRS Limit_VfromE) 1);
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   314
by (rtac ([bprem,limiti] MRS Limit_VfromE) 1);
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   315
by (res_inst_tac [("j1", "x Un xa Un succ(1)")] (step RS exE) 1);
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   316
by (DO_GOAL [etac conjE, etac Limit_VfromI, rtac limiti, atac] 5);
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   317
by (etac (Vfrom_UnI2 RS Vfrom_UnI1) 4);
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   318
by (etac (Vfrom_UnI1 RS Vfrom_UnI1) 3);
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   319
by (rtac (succI1 RS UnI2) 2);
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   320
by (REPEAT (ares_tac [limiti, Limit_has_0, Limit_has_succ, Un_least_lt] 1));
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   321
val in_Vfrom_limit = result();
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   322
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   323
(** products **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   324
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   325
goal Univ.thy
187
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   326
    "!!A. [| a: Vfrom(A,j);  b: Vfrom(A,j);  Transset(A) |] ==> \
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   327
\         a*b : Vfrom(A, succ(succ(succ(j))))";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   328
by (dtac Transset_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   329
by (rtac subset_mem_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   330
by (rewtac Transset_def);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   331
by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   332
val prod_in_Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   333
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   334
val [aprem,bprem,limiti,transset] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   335
  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   336
\  a*b : Vfrom(A,i)";
187
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   337
by (rtac ([aprem,bprem,limiti] MRS in_Vfrom_limit) 1);
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   338
by (REPEAT (ares_tac [exI, conjI, prod_in_Vfrom, transset,
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   339
		      limiti RS Limit_has_succ] 1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   340
val prod_in_Vfrom_limit = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   341
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   342
(** Disjoint sums, aka Quine ordered pairs **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   343
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   344
goalw Univ.thy [sum_def]
187
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   345
    "!!A. [| a: Vfrom(A,j);  b: Vfrom(A,j);  Transset(A);  1:j |] ==> \
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   346
\         a+b : Vfrom(A, succ(succ(succ(j))))";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   347
by (dtac Transset_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   348
by (rtac subset_mem_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   349
by (rewtac Transset_def);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   350
by (fast_tac (ZF_cs addIs [zero_in_Vfrom, Pair_in_Vfrom, 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   351
			   i_subset_Vfrom RS subsetD]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   352
val sum_in_Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   353
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   354
val [aprem,bprem,limiti,transset] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   355
  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   356
\  a+b : Vfrom(A,i)";
187
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   357
by (rtac ([aprem,bprem,limiti] MRS in_Vfrom_limit) 1);
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   358
by (REPEAT (ares_tac [exI, conjI, sum_in_Vfrom, transset,
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   359
		      limiti RS Limit_has_succ] 1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   360
val sum_in_Vfrom_limit = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   361
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   362
(** function space! **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   363
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   364
goalw Univ.thy [Pi_def]
187
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   365
    "!!A. [| a: Vfrom(A,j);  b: Vfrom(A,j);  Transset(A) |] ==> \
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   366
\         a->b : Vfrom(A, succ(succ(succ(succ(j)))))";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   367
by (dtac Transset_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   368
by (rtac subset_mem_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   369
by (rtac (Collect_subset RS subset_trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   370
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   371
by (rtac (subset_trans RS subset_trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   372
by (rtac Un_upper2 3);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   373
by (rtac (succI1 RS UN_upper) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   374
by (rtac Pow_mono 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   375
by (rewtac Transset_def);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   376
by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   377
val fun_in_Vfrom = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   378
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   379
val [aprem,bprem,limiti,transset] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   380
  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   381
\  a->b : Vfrom(A,i)";
187
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   382
by (rtac ([aprem,bprem,limiti] MRS in_Vfrom_limit) 1);
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   383
by (REPEAT (ares_tac [exI, conjI, fun_in_Vfrom, transset,
8729bfdcb638 ZF/univ/in_Vfrom_limit: new
lcp
parents: 37
diff changeset
   384
		      limiti RS Limit_has_succ] 1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   385
val fun_in_Vfrom_limit = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   386
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   387
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   388
(*** The set Vset(i) ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   389
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   390
goal Univ.thy "Vset(i) = (UN j:i. Pow(Vset(j)))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   391
by (rtac (Vfrom RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   392
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   393
val Vset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   394
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   395
val Vset_succ = Transset_0 RS Transset_Vfrom_succ;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   396
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   397
val Transset_Vset = Transset_0 RS Transset_Vfrom;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   398
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   399
(** Characterisation of the elements of Vset(i) **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   400
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   401
val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) < i";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   402
by (rtac (ordi RS trans_induct) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   403
by (rtac (Vset RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   404
by (safe_tac ZF_cs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   405
by (rtac (rank RS ssubst) 1);
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   406
by (rtac UN_succ_least_lt 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   407
by (fast_tac ZF_cs 2);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   408
by (REPEAT (ares_tac [ltI] 1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   409
val Vset_rank_imp1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   410
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   411
(*  [| Ord(i); x : Vset(i) |] ==> rank(x) < i  *)
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   412
val VsetD = standard (Vset_rank_imp1 RS spec RS mp);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   413
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   414
val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   415
by (rtac (ordi RS trans_induct) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   416
by (rtac allI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   417
by (rtac (Vset RS ssubst) 1);
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   418
by (fast_tac (ZF_cs addSIs [rank_lt RS ltD]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   419
val Vset_rank_imp2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   420
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   421
goal Univ.thy "!!x i. rank(x)<i ==> x : Vset(i)";
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   422
by (etac ltE 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   423
by (etac (Vset_rank_imp2 RS spec RS mp) 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   424
by (assume_tac 1);
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   425
val VsetI = result();
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   426
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   427
goal Univ.thy "!!i. Ord(i) ==> b : Vset(i) <-> rank(b) < i";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   428
by (rtac iffI 1);
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   429
by (REPEAT (eresolve_tac [asm_rl, VsetD, VsetI] 1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   430
val Vset_Ord_rank_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   431
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   432
goal Univ.thy "b : Vset(a) <-> rank(b) < rank(a)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   433
by (rtac (Vfrom_rank_eq RS subst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   434
by (rtac (Ord_rank RS Vset_Ord_rank_iff) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   435
val Vset_rank_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   436
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   437
goal Univ.thy "!!i. Ord(i) ==> rank(Vset(i)) = i";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   438
by (rtac (rank RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   439
by (rtac equalityI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   440
by (safe_tac ZF_cs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   441
by (EVERY' [rtac UN_I, 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   442
	    etac (i_subset_Vfrom RS subsetD),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   443
	    etac (Ord_in_Ord RS rank_of_Ord RS ssubst),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   444
	    assume_tac,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   445
	    rtac succI1] 3);
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   446
by (REPEAT (eresolve_tac [asm_rl, VsetD RS ltD, Ord_trans] 1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   447
val rank_Vset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   448
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   449
(** Lemmas for reasoning about sets in terms of their elements' ranks **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   450
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   451
goal Univ.thy "a <= Vset(rank(a))";
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   452
by (rtac subsetI 1);
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   453
by (etac (rank_lt RS VsetI) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   454
val arg_subset_Vset_rank = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   455
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   456
val [iprem] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   457
    "[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b";
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   458
by (rtac ([subset_refl, arg_subset_Vset_rank] MRS 
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   459
	  Int_greatest RS subset_trans) 1);
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   460
by (rtac (Ord_rank RS iprem) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   461
val Int_Vset_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   462
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   463
(** Set up an environment for simplification **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   464
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   465
val rank_rls = [rank_Inl, rank_Inr, rank_pair1, rank_pair2];
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   466
val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [lt_trans]));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   467
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   468
val rank_ss = ZF_ss 
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   469
    addsimps [case_Inl, case_Inr, VsetI]
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   470
    addsimps rank_trans_rls;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   471
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   472
(** Recursion over Vset levels! **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   473
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   474
(*NOT SUITABLE FOR REWRITING: recursive!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   475
goalw Univ.thy [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   476
by (rtac (transrec RS ssubst) 1);
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   477
by (simp_tac (ZF_ss addsimps [Ord_rank, Ord_succ, VsetD RS ltD RS beta, 
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   478
			      VsetI RS beta, le_refl]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   479
val Vrec = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   480
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   481
(*This form avoids giant explosions in proofs.  NOTE USE OF == *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   482
val rew::prems = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   483
    "[| !!x. h(x)==Vrec(x,H) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   484
\    h(a) = H(a, lam x: Vset(rank(a)). h(x))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   485
by (rewtac rew);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   486
by (rtac Vrec 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   487
val def_Vrec = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   488
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   489
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   490
(*** univ(A) ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   491
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   492
goalw Univ.thy [univ_def] "!!A B. A<=B ==> univ(A) <= univ(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   493
by (etac Vfrom_mono 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   494
by (rtac subset_refl 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   495
val univ_mono = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   496
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   497
goalw Univ.thy [univ_def] "!!A. Transset(A) ==> Transset(univ(A))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   498
by (etac Transset_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   499
val Transset_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   500
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   501
(** univ(A) as a limit **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   502
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   503
goalw Univ.thy [univ_def] "univ(A) = (UN i:nat. Vfrom(A,i))";
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   504
by (rtac (Limit_nat RS Limit_Vfrom_eq) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   505
val univ_eq_UN = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   506
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   507
goal Univ.thy "!!c. c <= univ(A) ==> c = (UN i:nat. c Int Vfrom(A,i))";
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   508
by (rtac (subset_UN_iff_eq RS iffD1) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   509
by (etac (univ_eq_UN RS subst) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   510
val subset_univ_eq_Int = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   511
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   512
val [aprem, iprem] = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   513
    "[| a <= univ(X);			 	\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   514
\       !!i. i:nat ==> a Int Vfrom(X,i) <= b 	\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   515
\    |] ==> a <= b";
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   516
by (rtac (aprem RS subset_univ_eq_Int RS ssubst) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   517
by (rtac UN_least 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   518
by (etac iprem 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   519
val univ_Int_Vfrom_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   520
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   521
val prems = goal Univ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   522
    "[| a <= univ(X);   b <= univ(X);   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   523
\       !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i) \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   524
\    |] ==> a = b";
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   525
by (rtac equalityI 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   526
by (ALLGOALS
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   527
    (resolve_tac (prems RL [univ_Int_Vfrom_subset]) THEN'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   528
     eresolve_tac (prems RL [equalityD1,equalityD2] RL [subset_trans]) THEN'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   529
     rtac Int_lower1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   530
val univ_Int_Vfrom_eq = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   531
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   532
(** Closure properties **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   533
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   534
goalw Univ.thy [univ_def] "0 : univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   535
by (rtac (nat_0I RS zero_in_Vfrom) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   536
val zero_in_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   537
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   538
goalw Univ.thy [univ_def] "A <= univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   539
by (rtac A_subset_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   540
val A_subset_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   541
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   542
val A_into_univ = A_subset_univ RS subsetD;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   543
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   544
(** Closure under unordered and ordered pairs **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   545
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   546
goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> {a} : univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   547
by (rtac singleton_in_Vfrom_limit 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   548
by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   549
val singleton_in_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   550
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   551
goalw Univ.thy [univ_def] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   552
    "!!A a. [| a: univ(A);  b: univ(A) |] ==> {a,b} : univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   553
by (rtac doubleton_in_Vfrom_limit 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   554
by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   555
val doubleton_in_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   556
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   557
goalw Univ.thy [univ_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   558
    "!!A a. [| a: univ(A);  b: univ(A) |] ==> <a,b> : univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   559
by (rtac Pair_in_Vfrom_limit 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   560
by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   561
val Pair_in_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   562
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   563
goal Univ.thy "univ(A)*univ(A) <= univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   564
by (REPEAT (ares_tac [subsetI,Pair_in_univ] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   565
     ORELSE eresolve_tac [SigmaE, ssubst] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   566
val product_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   567
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   568
val Sigma_subset_univ = standard
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   569
    (Sigma_mono RS (product_univ RSN (2,subset_trans)));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   570
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   571
goalw Univ.thy [univ_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   572
    "!!a b.[| <a,b> <= univ(A);  Transset(A) |] ==> <a,b> : univ(A)";
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   573
by (etac Transset_Pair_subset_Vfrom_limit 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   574
by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   575
val Transset_Pair_subset_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   576
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   577
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   578
(** The natural numbers **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   579
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   580
goalw Univ.thy [univ_def] "nat <= univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   581
by (rtac i_subset_Vfrom 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   582
val nat_subset_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   583
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   584
(* n:nat ==> n:univ(A) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   585
val nat_into_univ = standard (nat_subset_univ RS subsetD);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   586
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   587
(** instances for 1 and 2 **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   588
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   589
goal Univ.thy "1 : univ(A)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   590
by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   591
val one_in_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   592
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   593
(*unused!*)
27
0e152fe9571e Retry of the previous commit (network outage)
lcp
parents: 14
diff changeset
   594
goal Univ.thy "succ(1) : univ(A)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   595
by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   596
val two_in_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   597
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   598
goalw Univ.thy [bool_def] "bool <= univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   599
by (fast_tac (ZF_cs addSIs [zero_in_univ,one_in_univ]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   600
val bool_subset_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   601
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   602
val bool_into_univ = standard (bool_subset_univ RS subsetD);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   603
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   604
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   605
(** Closure under disjoint union **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   606
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   607
goalw Univ.thy [Inl_def] "!!A a. a: univ(A) ==> Inl(a) : univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   608
by (REPEAT (ares_tac [zero_in_univ,Pair_in_univ] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   609
val Inl_in_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   610
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   611
goalw Univ.thy [Inr_def] "!!A b. b: univ(A) ==> Inr(b) : univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   612
by (REPEAT (ares_tac [one_in_univ, Pair_in_univ] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   613
val Inr_in_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   614
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   615
goal Univ.thy "univ(C)+univ(C) <= univ(C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   616
by (REPEAT (ares_tac [subsetI,Inl_in_univ,Inr_in_univ] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   617
     ORELSE eresolve_tac [sumE, ssubst] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   618
val sum_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   619
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   620
val sum_subset_univ = standard
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   621
    (sum_mono RS (sum_univ RSN (2,subset_trans)));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   622
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   623
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   624
(** Closure under binary union -- use Un_least **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   625
(** Closure under Collect -- use  (Collect_subset RS subset_trans)  **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   626
(** Closure under RepFun -- use   RepFun_subset  **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   627
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   628