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