src/ZF/Univ.ML
author paulson
Mon Dec 28 16:59:28 1998 +0100 (1998-12-28)
changeset 6053 8a1059aa01f0
parent 5479 5a5dfb0f0d7d
child 6071 1b2392ac5752
permissions -rw-r--r--
new inductive, datatype and primrec packages, etc.
clasohm@1461
     1
(*  Title:      ZF/Univ
clasohm@0
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@435
     4
    Copyright   1994  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!*)
wenzelm@5067
    12
Goal "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))";
paulson@2033
    13
by (stac (Vfrom_def RS def_transrec) 1);
paulson@2469
    14
by (Simp_tac 1);
clasohm@760
    15
qed "Vfrom";
clasohm@0
    16
clasohm@0
    17
(** Monotonicity **)
clasohm@0
    18
paulson@5137
    19
Goal "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);
paulson@2033
    22
by (stac Vfrom 1);
paulson@2033
    23
by (stac Vfrom 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);
paulson@3736
    31
qed_spec_mp "Vfrom_mono";
clasohm@0
    32
clasohm@0
    33
clasohm@0
    34
(** A fundamental equality: Vfrom does not require ordinals! **)
clasohm@0
    35
wenzelm@5067
    36
Goal "Vfrom(A,x) <= Vfrom(A,rank(x))";
clasohm@0
    37
by (eps_ind_tac "x" 1);
paulson@2033
    38
by (stac Vfrom 1);
paulson@2033
    39
by (stac Vfrom 1);
wenzelm@4091
    40
by (blast_tac (claset() addSIs [rank_lt RS ltD]) 1);
clasohm@760
    41
qed "Vfrom_rank_subset1";
clasohm@0
    42
wenzelm@5067
    43
Goal "Vfrom(A,rank(x)) <= Vfrom(A,x)";
clasohm@0
    44
by (eps_ind_tac "x" 1);
paulson@2033
    45
by (stac Vfrom 1);
paulson@2033
    46
by (stac Vfrom 1);
lcp@15
    47
by (rtac (subset_refl RS Un_mono) 1);
lcp@15
    48
by (rtac UN_least 1);
lcp@27
    49
(*expand rank(x1) = (UN y:x1. succ(rank(y))) in assumptions*)
lcp@27
    50
by (etac (rank RS equalityD1 RS subsetD RS UN_E) 1);
lcp@15
    51
by (rtac subset_trans 1);
lcp@15
    52
by (etac UN_upper 2);
lcp@27
    53
by (rtac (subset_refl RS Vfrom_mono RS subset_trans RS Pow_mono) 1);
lcp@27
    54
by (etac (ltI RS le_imp_subset) 1);
lcp@27
    55
by (rtac (Ord_rank RS Ord_succ) 1);
clasohm@0
    56
by (etac bspec 1);
clasohm@0
    57
by (assume_tac 1);
clasohm@760
    58
qed "Vfrom_rank_subset2";
clasohm@0
    59
wenzelm@5067
    60
Goal "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@760
    64
qed "Vfrom_rank_eq";
clasohm@0
    65
clasohm@0
    66
clasohm@0
    67
(*** Basic closure properties ***)
clasohm@0
    68
paulson@5137
    69
Goal "y:x ==> 0 : Vfrom(A,x)";
paulson@2033
    70
by (stac Vfrom 1);
paulson@2925
    71
by (Blast_tac 1);
clasohm@760
    72
qed "zero_in_Vfrom";
clasohm@0
    73
wenzelm@5067
    74
Goal "i <= Vfrom(A,i)";
clasohm@0
    75
by (eps_ind_tac "i" 1);
paulson@2033
    76
by (stac Vfrom 1);
paulson@2925
    77
by (Blast_tac 1);
clasohm@760
    78
qed "i_subset_Vfrom";
clasohm@0
    79
wenzelm@5067
    80
Goal "A <= Vfrom(A,i)";
paulson@2033
    81
by (stac Vfrom 1);
clasohm@0
    82
by (rtac Un_upper1 1);
clasohm@760
    83
qed "A_subset_Vfrom";
clasohm@0
    84
lcp@803
    85
bind_thm ("A_into_Vfrom", A_subset_Vfrom RS subsetD);
lcp@488
    86
paulson@5137
    87
Goal "a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))";
paulson@2033
    88
by (stac Vfrom 1);
paulson@2925
    89
by (Blast_tac 1);
clasohm@760
    90
qed "subset_mem_Vfrom";
clasohm@0
    91
clasohm@0
    92
(** Finite sets and ordered pairs **)
clasohm@0
    93
paulson@5137
    94
Goal "a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))";
clasohm@0
    95
by (rtac subset_mem_Vfrom 1);
paulson@4152
    96
by Safe_tac;
clasohm@760
    97
qed "singleton_in_Vfrom";
clasohm@0
    98
paulson@5147
    99
Goal "[| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> {a,b} : Vfrom(A,succ(i))";
clasohm@0
   100
by (rtac subset_mem_Vfrom 1);
paulson@4152
   101
by Safe_tac;
clasohm@760
   102
qed "doubleton_in_Vfrom";
clasohm@0
   103
wenzelm@5067
   104
Goalw [Pair_def]
paulson@5147
   105
    "[| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> \
clasohm@0
   106
\         <a,b> : Vfrom(A,succ(succ(i)))";
clasohm@0
   107
by (REPEAT (ares_tac [doubleton_in_Vfrom] 1));
clasohm@760
   108
qed "Pair_in_Vfrom";
clasohm@0
   109
paulson@5321
   110
Goal "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);
paulson@5321
   113
by (REPEAT (ares_tac [subset_refl, subset_succI] 1));
clasohm@760
   114
qed "succ_in_Vfrom";
clasohm@0
   115
clasohm@0
   116
(*** 0, successor and limit equations fof Vfrom ***)
clasohm@0
   117
wenzelm@5067
   118
Goal "Vfrom(A,0) = A";
paulson@2033
   119
by (stac Vfrom 1);
paulson@2925
   120
by (Blast_tac 1);
clasohm@760
   121
qed "Vfrom_0";
clasohm@0
   122
paulson@5137
   123
Goal "Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
clasohm@0
   124
by (rtac (Vfrom RS trans) 1);
lcp@6
   125
by (rtac (succI1 RS RepFunI RS Union_upper RSN
clasohm@1461
   126
              (2, equalityI RS subst_context)) 1);
clasohm@0
   127
by (rtac UN_least 1);
clasohm@0
   128
by (rtac (subset_refl RS Vfrom_mono RS Pow_mono) 1);
lcp@27
   129
by (etac (ltI RS le_imp_subset) 1);
lcp@27
   130
by (etac Ord_succ 1);
clasohm@760
   131
qed "Vfrom_succ_lemma";
clasohm@0
   132
wenzelm@5067
   133
Goal "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
clasohm@0
   134
by (res_inst_tac [("x1", "succ(i)")] (Vfrom_rank_eq RS subst) 1);
clasohm@0
   135
by (res_inst_tac [("x1", "i")] (Vfrom_rank_eq RS subst) 1);
paulson@2033
   136
by (stac rank_succ 1);
clasohm@0
   137
by (rtac (Ord_rank RS Vfrom_succ_lemma) 1);
clasohm@760
   138
qed "Vfrom_succ";
clasohm@0
   139
clasohm@0
   140
(*The premise distinguishes this from Vfrom(A,0);  allowing X=0 forces
clasohm@0
   141
  the conclusion to be Vfrom(A,Union(X)) = A Un (UN y:X. Vfrom(A,y)) *)
paulson@5321
   142
Goal "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))";
paulson@5321
   143
by (stac Vfrom 1);
paulson@5321
   144
by (rtac equalityI 1);
paulson@5321
   145
(*first inclusion*)
paulson@5321
   146
by (rtac Un_least 1);
paulson@5321
   147
by (rtac (A_subset_Vfrom RS subset_trans) 1);
paulson@5321
   148
by (rtac UN_upper 1);
paulson@5321
   149
by (assume_tac 1);
paulson@5321
   150
by (rtac UN_least 1);
paulson@5321
   151
by (etac UnionE 1);
paulson@5321
   152
by (rtac subset_trans 1);
paulson@5321
   153
by (etac UN_upper 2 THEN stac Vfrom 1 THEN 
paulson@5321
   154
    etac ([UN_upper, Un_upper2] MRS subset_trans) 1);
paulson@5321
   155
(*opposite inclusion*)
paulson@5321
   156
by (rtac UN_least 1);
paulson@5321
   157
by (stac Vfrom 1);
paulson@5321
   158
by (Blast_tac 1);
paulson@5321
   159
qed "Vfrom_Union";
paulson@5321
   160
clasohm@0
   161
val [prem] = goal Univ.thy "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))";
paulson@2033
   162
by (stac Vfrom 1);
clasohm@0
   163
by (rtac equalityI 1);
clasohm@0
   164
(*first inclusion*)
clasohm@0
   165
by (rtac Un_least 1);
lcp@15
   166
by (rtac (A_subset_Vfrom RS subset_trans) 1);
paulson@5321
   167
lcp@15
   168
by (rtac (prem RS UN_upper) 1);
lcp@15
   169
by (rtac UN_least 1);
lcp@15
   170
by (etac UnionE 1);
lcp@15
   171
by (rtac subset_trans 1);
lcp@15
   172
by (etac UN_upper 2);
paulson@2033
   173
by (stac Vfrom 1);
lcp@15
   174
by (etac ([UN_upper, Un_upper2] MRS subset_trans) 1);
clasohm@0
   175
(*opposite inclusion*)
lcp@15
   176
by (rtac UN_least 1);
paulson@2033
   177
by (stac Vfrom 1);
paulson@2925
   178
by (Blast_tac 1);
clasohm@760
   179
qed "Vfrom_Union";
clasohm@0
   180
clasohm@0
   181
(*** Vfrom applied to Limit ordinals ***)
clasohm@0
   182
clasohm@0
   183
(*NB. limit ordinals are non-empty;
clasohm@0
   184
                        Vfrom(A,0) = A = A Un (UN y:0. Vfrom(A,y)) *)
clasohm@0
   185
val [limiti] = goal Univ.thy
clasohm@0
   186
    "Limit(i) ==> Vfrom(A,i) = (UN y:i. Vfrom(A,y))";
lcp@27
   187
by (rtac (limiti RS (Limit_has_0 RS ltD) RS Vfrom_Union RS subst) 1);
paulson@2033
   188
by (stac (limiti RS Limit_Union_eq) 1);
clasohm@0
   189
by (rtac refl 1);
clasohm@760
   190
qed "Limit_Vfrom_eq";
clasohm@0
   191
paulson@5137
   192
Goal "[| a: Vfrom(A,j);  Limit(i);  j<i |] ==> a : Vfrom(A,i)";
lcp@27
   193
by (rtac (Limit_Vfrom_eq RS equalityD2 RS subsetD) 1);
lcp@27
   194
by (REPEAT (ares_tac [ltD RS UN_I] 1));
clasohm@760
   195
qed "Limit_VfromI";
lcp@27
   196
paulson@5321
   197
val prems = Goal
clasohm@1461
   198
    "[| a: Vfrom(A,i);  Limit(i);               \
clasohm@1461
   199
\       !!x. [| x<i;  a: Vfrom(A,x) |] ==> R    \
lcp@27
   200
\    |] ==> R";
lcp@27
   201
by (rtac (Limit_Vfrom_eq RS equalityD1 RS subsetD RS UN_E) 1);
lcp@27
   202
by (REPEAT (ares_tac (prems @ [ltI, Limit_is_Ord]) 1));
clasohm@760
   203
qed "Limit_VfromE";
clasohm@0
   204
lcp@516
   205
val zero_in_VLimit = Limit_has_0 RS ltD RS zero_in_Vfrom;
lcp@484
   206
clasohm@0
   207
val [major,limiti] = goal Univ.thy
clasohm@0
   208
    "[| a: Vfrom(A,i);  Limit(i) |] ==> {a} : Vfrom(A,i)";
lcp@27
   209
by (rtac ([major,limiti] MRS Limit_VfromE) 1);
lcp@27
   210
by (etac ([singleton_in_Vfrom, limiti] MRS Limit_VfromI) 1);
clasohm@0
   211
by (etac (limiti RS Limit_has_succ) 1);
clasohm@760
   212
qed "singleton_in_VLimit";
clasohm@0
   213
clasohm@0
   214
val Vfrom_UnI1 = Un_upper1 RS (subset_refl RS Vfrom_mono RS subsetD)
clasohm@0
   215
and Vfrom_UnI2 = Un_upper2 RS (subset_refl RS Vfrom_mono RS subsetD);
clasohm@0
   216
clasohm@0
   217
(*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*)
clasohm@0
   218
val [aprem,bprem,limiti] = goal Univ.thy
clasohm@0
   219
    "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> \
clasohm@0
   220
\    {a,b} : Vfrom(A,i)";
lcp@27
   221
by (rtac ([aprem,limiti] MRS Limit_VfromE) 1);
lcp@27
   222
by (rtac ([bprem,limiti] MRS Limit_VfromE) 1);
lcp@27
   223
by (rtac ([doubleton_in_Vfrom, limiti] MRS Limit_VfromI) 1);
lcp@27
   224
by (etac Vfrom_UnI1 1);
lcp@27
   225
by (etac Vfrom_UnI2 1);
lcp@27
   226
by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1));
clasohm@760
   227
qed "doubleton_in_VLimit";
clasohm@0
   228
clasohm@0
   229
val [aprem,bprem,limiti] = goal Univ.thy
clasohm@0
   230
    "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> \
clasohm@0
   231
\    <a,b> : Vfrom(A,i)";
clasohm@0
   232
(*Infer that a, b occur at ordinals x,xa < i.*)
lcp@27
   233
by (rtac ([aprem,limiti] MRS Limit_VfromE) 1);
lcp@27
   234
by (rtac ([bprem,limiti] MRS Limit_VfromE) 1);
lcp@27
   235
by (rtac ([Pair_in_Vfrom, limiti] MRS Limit_VfromI) 1);
clasohm@0
   236
(*Infer that succ(succ(x Un xa)) < i *)
lcp@27
   237
by (etac Vfrom_UnI1 1);
lcp@27
   238
by (etac Vfrom_UnI2 1);
lcp@27
   239
by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1));
clasohm@760
   240
qed "Pair_in_VLimit";
lcp@484
   241
paulson@5137
   242
Goal "Limit(i) ==> Vfrom(A,i)*Vfrom(A,i) <= Vfrom(A,i)";
lcp@516
   243
by (REPEAT (ares_tac [subsetI,Pair_in_VLimit] 1
lcp@484
   244
     ORELSE eresolve_tac [SigmaE, ssubst] 1));
clasohm@760
   245
qed "product_VLimit";
lcp@484
   246
lcp@803
   247
bind_thm ("Sigma_subset_VLimit",
clasohm@1461
   248
          [Sigma_mono, product_VLimit] MRS subset_trans);
lcp@484
   249
lcp@803
   250
bind_thm ("nat_subset_VLimit", 
clasohm@1461
   251
          [nat_le_Limit RS le_imp_subset, i_subset_Vfrom] MRS subset_trans);
lcp@484
   252
paulson@5137
   253
Goal "[| n: nat;  Limit(i) |] ==> n : Vfrom(A,i)";
lcp@516
   254
by (REPEAT (ares_tac [nat_subset_VLimit RS subsetD] 1));
clasohm@760
   255
qed "nat_into_VLimit";
lcp@484
   256
lcp@484
   257
(** Closure under disjoint union **)
lcp@484
   258
lcp@803
   259
bind_thm ("zero_in_VLimit", Limit_has_0 RS ltD RS zero_in_Vfrom);
lcp@484
   260
paulson@5137
   261
Goal "Limit(i) ==> 1 : Vfrom(A,i)";
lcp@516
   262
by (REPEAT (ares_tac [nat_into_VLimit, nat_0I, nat_succI] 1));
clasohm@760
   263
qed "one_in_VLimit";
lcp@484
   264
wenzelm@5067
   265
Goalw [Inl_def]
paulson@5147
   266
    "[| a: Vfrom(A,i); Limit(i) |] ==> Inl(a) : Vfrom(A,i)";
lcp@516
   267
by (REPEAT (ares_tac [zero_in_VLimit, Pair_in_VLimit] 1));
clasohm@760
   268
qed "Inl_in_VLimit";
lcp@484
   269
wenzelm@5067
   270
Goalw [Inr_def]
paulson@5147
   271
    "[| b: Vfrom(A,i); Limit(i) |] ==> Inr(b) : Vfrom(A,i)";
lcp@516
   272
by (REPEAT (ares_tac [one_in_VLimit, Pair_in_VLimit] 1));
clasohm@760
   273
qed "Inr_in_VLimit";
lcp@484
   274
paulson@5137
   275
Goal "Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)";
wenzelm@4091
   276
by (blast_tac (claset() addSIs [Inl_in_VLimit, Inr_in_VLimit]) 1);
clasohm@760
   277
qed "sum_VLimit";
lcp@484
   278
lcp@803
   279
bind_thm ("sum_subset_VLimit", [sum_mono, sum_VLimit] MRS subset_trans);
lcp@484
   280
clasohm@0
   281
clasohm@0
   282
clasohm@0
   283
(*** Properties assuming Transset(A) ***)
clasohm@0
   284
paulson@5137
   285
Goal "Transset(A) ==> Transset(Vfrom(A,i))";
clasohm@0
   286
by (eps_ind_tac "i" 1);
paulson@2033
   287
by (stac Vfrom 1);
wenzelm@4091
   288
by (blast_tac (claset() addSIs [Transset_Union_family, Transset_Un,
clasohm@1461
   289
                            Transset_Pow]) 1);
clasohm@760
   290
qed "Transset_Vfrom";
clasohm@0
   291
paulson@5137
   292
Goal "Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))";
clasohm@0
   293
by (rtac (Vfrom_succ RS trans) 1);
lcp@15
   294
by (rtac (Un_upper2 RSN (2,equalityI)) 1);
lcp@15
   295
by (rtac (subset_refl RSN (2,Un_least)) 1);
lcp@15
   296
by (rtac (A_subset_Vfrom RS subset_trans) 1);
lcp@15
   297
by (etac (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1);
clasohm@760
   298
qed "Transset_Vfrom_succ";
clasohm@0
   299
paulson@5321
   300
Goalw [Pair_def,Transset_def] "[| <a,b> <= C; Transset(C) |] ==> a: C & b: C";
paulson@2925
   301
by (Blast_tac 1);
clasohm@760
   302
qed "Transset_Pair_subset";
clasohm@0
   303
paulson@5147
   304
Goal "[| <a,b> <= Vfrom(A,i);  Transset(A);  Limit(i) |] ==> \
clasohm@0
   305
\          <a,b> : Vfrom(A,i)";
lcp@15
   306
by (etac (Transset_Pair_subset RS conjE) 1);
lcp@15
   307
by (etac Transset_Vfrom 1);
lcp@516
   308
by (REPEAT (ares_tac [Pair_in_VLimit] 1));
clasohm@760
   309
qed "Transset_Pair_subset_VLimit";
clasohm@0
   310
clasohm@0
   311
clasohm@0
   312
(*** Closure under product/sum applied to elements -- thus Vfrom(A,i) 
clasohm@0
   313
     is a model of simple type theory provided A is a transitive set
clasohm@0
   314
     and i is a limit ordinal
clasohm@0
   315
***)
clasohm@0
   316
lcp@187
   317
(*General theorem for membership in Vfrom(A,i) when i is a limit ordinal*)
paulson@5321
   318
val [aprem,bprem,limiti,step] = Goal
clasohm@1461
   319
  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);                 \
lcp@187
   320
\     !!x y j. [| j<i; 1:j; x: Vfrom(A,j); y: Vfrom(A,j) \
clasohm@1461
   321
\              |] ==> EX k. h(x,y): Vfrom(A,k) & k<i |] ==>     \
lcp@187
   322
\  h(a,b) : Vfrom(A,i)";
lcp@187
   323
(*Infer that a, b occur at ordinals x,xa < i.*)
lcp@187
   324
by (rtac ([aprem,limiti] MRS Limit_VfromE) 1);
lcp@187
   325
by (rtac ([bprem,limiti] MRS Limit_VfromE) 1);
lcp@828
   326
by (res_inst_tac [("j1", "x Un xa Un 2")] (step RS exE) 1);
lcp@187
   327
by (DO_GOAL [etac conjE, etac Limit_VfromI, rtac limiti, atac] 5);
lcp@187
   328
by (etac (Vfrom_UnI2 RS Vfrom_UnI1) 4);
lcp@187
   329
by (etac (Vfrom_UnI1 RS Vfrom_UnI1) 3);
lcp@187
   330
by (rtac (succI1 RS UnI2) 2);
lcp@187
   331
by (REPEAT (ares_tac [limiti, Limit_has_0, Limit_has_succ, Un_least_lt] 1));
clasohm@760
   332
qed "in_VLimit";
clasohm@0
   333
clasohm@0
   334
(** products **)
clasohm@0
   335
paulson@5147
   336
Goal "[| a: Vfrom(A,j);  b: Vfrom(A,j);  Transset(A) |] ==> \
lcp@187
   337
\         a*b : Vfrom(A, succ(succ(succ(j))))";
clasohm@0
   338
by (dtac Transset_Vfrom 1);
clasohm@0
   339
by (rtac subset_mem_Vfrom 1);
clasohm@0
   340
by (rewtac Transset_def);
wenzelm@4091
   341
by (blast_tac (claset() addIs [Pair_in_Vfrom]) 1);
clasohm@760
   342
qed "prod_in_Vfrom";
clasohm@0
   343
clasohm@0
   344
val [aprem,bprem,limiti,transset] = goal Univ.thy
clasohm@0
   345
  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
clasohm@0
   346
\  a*b : Vfrom(A,i)";
lcp@516
   347
by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
lcp@187
   348
by (REPEAT (ares_tac [exI, conjI, prod_in_Vfrom, transset,
clasohm@1461
   349
                      limiti RS Limit_has_succ] 1));
clasohm@760
   350
qed "prod_in_VLimit";
clasohm@0
   351
clasohm@0
   352
(** Disjoint sums, aka Quine ordered pairs **)
clasohm@0
   353
wenzelm@5067
   354
Goalw [sum_def]
paulson@5147
   355
    "[| a: Vfrom(A,j);  b: Vfrom(A,j);  Transset(A);  1:j |] ==> \
lcp@187
   356
\         a+b : Vfrom(A, succ(succ(succ(j))))";
clasohm@0
   357
by (dtac Transset_Vfrom 1);
clasohm@0
   358
by (rtac subset_mem_Vfrom 1);
clasohm@0
   359
by (rewtac Transset_def);
wenzelm@4091
   360
by (blast_tac (claset() addIs [zero_in_Vfrom, Pair_in_Vfrom, 
clasohm@1461
   361
                           i_subset_Vfrom RS subsetD]) 1);
clasohm@760
   362
qed "sum_in_Vfrom";
clasohm@0
   363
clasohm@0
   364
val [aprem,bprem,limiti,transset] = goal Univ.thy
clasohm@0
   365
  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
clasohm@0
   366
\  a+b : Vfrom(A,i)";
lcp@516
   367
by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
lcp@187
   368
by (REPEAT (ares_tac [exI, conjI, sum_in_Vfrom, transset,
clasohm@1461
   369
                      limiti RS Limit_has_succ] 1));
clasohm@760
   370
qed "sum_in_VLimit";
clasohm@0
   371
clasohm@0
   372
(** function space! **)
clasohm@0
   373
wenzelm@5067
   374
Goalw [Pi_def]
paulson@5147
   375
    "[| a: Vfrom(A,j);  b: Vfrom(A,j);  Transset(A) |] ==> \
lcp@187
   376
\         a->b : Vfrom(A, succ(succ(succ(succ(j)))))";
clasohm@0
   377
by (dtac Transset_Vfrom 1);
clasohm@0
   378
by (rtac subset_mem_Vfrom 1);
clasohm@0
   379
by (rtac (Collect_subset RS subset_trans) 1);
paulson@2033
   380
by (stac Vfrom 1);
clasohm@0
   381
by (rtac (subset_trans RS subset_trans) 1);
clasohm@0
   382
by (rtac Un_upper2 3);
clasohm@0
   383
by (rtac (succI1 RS UN_upper) 2);
clasohm@0
   384
by (rtac Pow_mono 1);
clasohm@0
   385
by (rewtac Transset_def);
wenzelm@4091
   386
by (blast_tac (claset() addIs [Pair_in_Vfrom]) 1);
clasohm@760
   387
qed "fun_in_Vfrom";
clasohm@0
   388
clasohm@0
   389
val [aprem,bprem,limiti,transset] = goal Univ.thy
clasohm@0
   390
  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
clasohm@0
   391
\  a->b : Vfrom(A,i)";
lcp@516
   392
by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
lcp@187
   393
by (REPEAT (ares_tac [exI, conjI, fun_in_Vfrom, transset,
clasohm@1461
   394
                      limiti RS Limit_has_succ] 1));
clasohm@760
   395
qed "fun_in_VLimit";
clasohm@0
   396
wenzelm@5067
   397
Goalw [Pi_def]
paulson@5321
   398
    "[| a: Vfrom(A,j);  Transset(A) |] ==> Pow(a) : Vfrom(A, succ(succ(j)))";
paulson@3074
   399
by (dtac Transset_Vfrom 1);
paulson@3074
   400
by (rtac subset_mem_Vfrom 1);
paulson@3074
   401
by (rewtac Transset_def);
paulson@3074
   402
by (stac Vfrom 1);
paulson@3074
   403
by (Blast_tac 1);
paulson@3074
   404
qed "Pow_in_Vfrom";
paulson@3074
   405
paulson@5268
   406
Goal "[| a: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Pow(a) : Vfrom(A,i)";
paulson@5479
   407
by (blast_tac (claset() addEs [Limit_VfromE]
paulson@5479
   408
		        addIs [Limit_has_succ, Pow_in_Vfrom, Limit_VfromI]) 1);
paulson@3074
   409
qed "Pow_in_VLimit";
paulson@3074
   410
clasohm@0
   411
clasohm@0
   412
(*** The set Vset(i) ***)
clasohm@0
   413
wenzelm@5067
   414
Goal "Vset(i) = (UN j:i. Pow(Vset(j)))";
paulson@2033
   415
by (stac Vfrom 1);
paulson@2925
   416
by (Blast_tac 1);
clasohm@760
   417
qed "Vset";
clasohm@0
   418
clasohm@0
   419
val Vset_succ = Transset_0 RS Transset_Vfrom_succ;
clasohm@0
   420
clasohm@0
   421
val Transset_Vset = Transset_0 RS Transset_Vfrom;
clasohm@0
   422
clasohm@0
   423
(** Characterisation of the elements of Vset(i) **)
clasohm@0
   424
paulson@5321
   425
Goal "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) < i";
paulson@5321
   426
by (etac trans_induct 1);
paulson@2033
   427
by (stac Vset 1);
paulson@4152
   428
by Safe_tac;
paulson@2033
   429
by (stac rank 1);
lcp@27
   430
by (rtac UN_succ_least_lt 1);
paulson@2925
   431
by (Blast_tac 2);
lcp@27
   432
by (REPEAT (ares_tac [ltI] 1));
paulson@3736
   433
qed_spec_mp "VsetD";
clasohm@0
   434
paulson@5321
   435
Goal "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)";
paulson@5321
   436
by (etac trans_induct 1);
clasohm@0
   437
by (rtac allI 1);
paulson@2033
   438
by (stac Vset 1);
wenzelm@4091
   439
by (blast_tac (claset() addSIs [rank_lt RS ltD]) 1);
paulson@3736
   440
val lemma = result();
clasohm@0
   441
paulson@5137
   442
Goal "rank(x)<i ==> x : Vset(i)";
lcp@27
   443
by (etac ltE 1);
paulson@3736
   444
by (etac (lemma RS spec RS mp) 1);
lcp@27
   445
by (assume_tac 1);
clasohm@760
   446
qed "VsetI";
clasohm@0
   447
paulson@5137
   448
Goal "Ord(i) ==> b : Vset(i) <-> rank(b) < i";
clasohm@0
   449
by (rtac iffI 1);
lcp@27
   450
by (REPEAT (eresolve_tac [asm_rl, VsetD, VsetI] 1));
clasohm@760
   451
qed "Vset_Ord_rank_iff";
clasohm@0
   452
wenzelm@5067
   453
Goal "b : Vset(a) <-> rank(b) < rank(a)";
clasohm@0
   454
by (rtac (Vfrom_rank_eq RS subst) 1);
clasohm@0
   455
by (rtac (Ord_rank RS Vset_Ord_rank_iff) 1);
clasohm@760
   456
qed "Vset_rank_iff";
clasohm@0
   457
paulson@5137
   458
Goal "Ord(i) ==> rank(Vset(i)) = i";
paulson@2033
   459
by (stac rank 1);
clasohm@0
   460
by (rtac equalityI 1);
paulson@4152
   461
by Safe_tac;
lcp@828
   462
by (EVERY' [rtac UN_I, 
clasohm@1461
   463
            etac (i_subset_Vfrom RS subsetD),
clasohm@1461
   464
            etac (Ord_in_Ord RS rank_of_Ord RS ssubst),
clasohm@1461
   465
            assume_tac,
clasohm@1461
   466
            rtac succI1] 3);
lcp@27
   467
by (REPEAT (eresolve_tac [asm_rl, VsetD RS ltD, Ord_trans] 1));
clasohm@760
   468
qed "rank_Vset";
clasohm@0
   469
clasohm@0
   470
(** Lemmas for reasoning about sets in terms of their elements' ranks **)
clasohm@0
   471
wenzelm@5067
   472
Goal "a <= Vset(rank(a))";
lcp@15
   473
by (rtac subsetI 1);
lcp@27
   474
by (etac (rank_lt RS VsetI) 1);
clasohm@760
   475
qed "arg_subset_Vset_rank";
clasohm@0
   476
paulson@5321
   477
val [iprem] = Goal
clasohm@0
   478
    "[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b";
lcp@27
   479
by (rtac ([subset_refl, arg_subset_Vset_rank] MRS 
clasohm@1461
   480
          Int_greatest RS subset_trans) 1);
lcp@15
   481
by (rtac (Ord_rank RS iprem) 1);
clasohm@760
   482
qed "Int_Vset_subset";
clasohm@0
   483
clasohm@0
   484
(** Set up an environment for simplification **)
clasohm@0
   485
wenzelm@5067
   486
Goalw [Inl_def] "rank(a) < rank(Inl(a))";
wenzelm@3889
   487
by (rtac rank_pair2 1);
wenzelm@3889
   488
qed "rank_Inl";
wenzelm@3889
   489
wenzelm@5067
   490
Goalw [Inr_def] "rank(a) < rank(Inr(a))";
wenzelm@3889
   491
by (rtac rank_pair2 1);
wenzelm@3889
   492
qed "rank_Inr";
wenzelm@3889
   493
clasohm@0
   494
val rank_rls = [rank_Inl, rank_Inr, rank_pair1, rank_pair2];
lcp@27
   495
val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [lt_trans]));
clasohm@0
   496
wenzelm@4091
   497
val rank_ss = simpset() addsimps [VsetI] addsimps rank_trans_rls;
clasohm@0
   498
clasohm@0
   499
(** Recursion over Vset levels! **)
clasohm@0
   500
clasohm@0
   501
(*NOT SUITABLE FOR REWRITING: recursive!*)
wenzelm@5067
   502
Goalw [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))";
paulson@2033
   503
by (stac transrec 1);
wenzelm@4091
   504
by (simp_tac (simpset() addsimps [Ord_rank, Ord_succ, VsetD RS ltD RS beta, 
clasohm@1461
   505
                              VsetI RS beta, le_refl]) 1);
clasohm@760
   506
qed "Vrec";
clasohm@0
   507
clasohm@0
   508
(*This form avoids giant explosions in proofs.  NOTE USE OF == *)
paulson@5321
   509
val rew::prems = Goal
clasohm@0
   510
    "[| !!x. h(x)==Vrec(x,H) |] ==> \
clasohm@0
   511
\    h(a) = H(a, lam x: Vset(rank(a)). h(x))";
clasohm@0
   512
by (rewtac rew);
clasohm@0
   513
by (rtac Vrec 1);
clasohm@760
   514
qed "def_Vrec";
clasohm@0
   515
paulson@6053
   516
(*NOT SUITABLE FOR REWRITING: recursive!*)
paulson@6053
   517
Goalw [Vrecursor_def]
paulson@6053
   518
     "Vrecursor(H,a) = H(lam x:Vset(rank(a)). Vrecursor(H,x),  a)";
paulson@6053
   519
by (stac transrec 1);
paulson@6053
   520
by (simp_tac (simpset() addsimps [Ord_rank, Ord_succ, VsetD RS ltD RS beta, 
paulson@6053
   521
                              VsetI RS beta, le_refl]) 1);
paulson@6053
   522
qed "Vrecursor";
paulson@6053
   523
paulson@6053
   524
(*This form avoids giant explosions in proofs.  NOTE USE OF == *)
paulson@6053
   525
Goal "h == Vrecursor(H) ==> h(a) = H(lam x: Vset(rank(a)). h(x),  a)";
paulson@6053
   526
by (Asm_simp_tac 1);
paulson@6053
   527
by (rtac Vrecursor 1);
paulson@6053
   528
qed "def_Vrecursor";
paulson@6053
   529
clasohm@0
   530
clasohm@0
   531
(*** univ(A) ***)
clasohm@0
   532
paulson@5137
   533
Goalw [univ_def] "A<=B ==> univ(A) <= univ(B)";
clasohm@0
   534
by (etac Vfrom_mono 1);
clasohm@0
   535
by (rtac subset_refl 1);
clasohm@760
   536
qed "univ_mono";
clasohm@0
   537
paulson@5137
   538
Goalw [univ_def] "Transset(A) ==> Transset(univ(A))";
clasohm@0
   539
by (etac Transset_Vfrom 1);
clasohm@760
   540
qed "Transset_univ";
clasohm@0
   541
clasohm@0
   542
(** univ(A) as a limit **)
clasohm@0
   543
wenzelm@5067
   544
Goalw [univ_def] "univ(A) = (UN i:nat. Vfrom(A,i))";
lcp@15
   545
by (rtac (Limit_nat RS Limit_Vfrom_eq) 1);
clasohm@760
   546
qed "univ_eq_UN";
clasohm@0
   547
paulson@5137
   548
Goal "c <= univ(A) ==> c = (UN i:nat. c Int Vfrom(A,i))";
lcp@15
   549
by (rtac (subset_UN_iff_eq RS iffD1) 1);
lcp@15
   550
by (etac (univ_eq_UN RS subst) 1);
clasohm@760
   551
qed "subset_univ_eq_Int";
clasohm@0
   552
paulson@5321
   553
val [aprem, iprem] = Goal
clasohm@1461
   554
    "[| a <= univ(X);                           \
clasohm@1461
   555
\       !!i. i:nat ==> a Int Vfrom(X,i) <= b    \
clasohm@0
   556
\    |] ==> a <= b";
paulson@2033
   557
by (stac (aprem RS subset_univ_eq_Int) 1);
lcp@15
   558
by (rtac UN_least 1);
lcp@15
   559
by (etac iprem 1);
clasohm@760
   560
qed "univ_Int_Vfrom_subset";
clasohm@0
   561
paulson@5321
   562
val prems = Goal
clasohm@0
   563
    "[| a <= univ(X);   b <= univ(X);   \
clasohm@0
   564
\       !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i) \
clasohm@0
   565
\    |] ==> a = b";
lcp@15
   566
by (rtac equalityI 1);
clasohm@0
   567
by (ALLGOALS
clasohm@0
   568
    (resolve_tac (prems RL [univ_Int_Vfrom_subset]) THEN'
clasohm@0
   569
     eresolve_tac (prems RL [equalityD1,equalityD2] RL [subset_trans]) THEN'
clasohm@0
   570
     rtac Int_lower1));
clasohm@760
   571
qed "univ_Int_Vfrom_eq";
clasohm@0
   572
clasohm@0
   573
(** Closure properties **)
clasohm@0
   574
wenzelm@5067
   575
Goalw [univ_def] "0 : univ(A)";
clasohm@0
   576
by (rtac (nat_0I RS zero_in_Vfrom) 1);
clasohm@760
   577
qed "zero_in_univ";
clasohm@0
   578
wenzelm@5067
   579
Goalw [univ_def] "A <= univ(A)";
clasohm@0
   580
by (rtac A_subset_Vfrom 1);
clasohm@760
   581
qed "A_subset_univ";
clasohm@0
   582
clasohm@0
   583
val A_into_univ = A_subset_univ RS subsetD;
clasohm@0
   584
clasohm@0
   585
(** Closure under unordered and ordered pairs **)
clasohm@0
   586
paulson@5137
   587
Goalw [univ_def] "a: univ(A) ==> {a} : univ(A)";
lcp@516
   588
by (REPEAT (ares_tac [singleton_in_VLimit, Limit_nat] 1));
clasohm@760
   589
qed "singleton_in_univ";
clasohm@0
   590
wenzelm@5067
   591
Goalw [univ_def] 
paulson@5147
   592
    "[| a: univ(A);  b: univ(A) |] ==> {a,b} : univ(A)";
lcp@516
   593
by (REPEAT (ares_tac [doubleton_in_VLimit, Limit_nat] 1));
clasohm@760
   594
qed "doubleton_in_univ";
clasohm@0
   595
wenzelm@5067
   596
Goalw [univ_def]
paulson@5147
   597
    "[| a: univ(A);  b: univ(A) |] ==> <a,b> : univ(A)";
lcp@516
   598
by (REPEAT (ares_tac [Pair_in_VLimit, Limit_nat] 1));
clasohm@760
   599
qed "Pair_in_univ";
clasohm@0
   600
wenzelm@5067
   601
Goalw [univ_def] "univ(A)*univ(A) <= univ(A)";
lcp@516
   602
by (rtac (Limit_nat RS product_VLimit) 1);
clasohm@760
   603
qed "product_univ";
clasohm@0
   604
clasohm@0
   605
clasohm@0
   606
(** The natural numbers **)
clasohm@0
   607
wenzelm@5067
   608
Goalw [univ_def] "nat <= univ(A)";
clasohm@0
   609
by (rtac i_subset_Vfrom 1);
clasohm@760
   610
qed "nat_subset_univ";
clasohm@0
   611
clasohm@0
   612
(* n:nat ==> n:univ(A) *)
clasohm@782
   613
bind_thm ("nat_into_univ", (nat_subset_univ RS subsetD));
clasohm@0
   614
clasohm@0
   615
(** instances for 1 and 2 **)
clasohm@0
   616
wenzelm@5067
   617
Goalw [univ_def] "1 : univ(A)";
lcp@516
   618
by (rtac (Limit_nat RS one_in_VLimit) 1);
clasohm@760
   619
qed "one_in_univ";
clasohm@0
   620
clasohm@0
   621
(*unused!*)
wenzelm@5067
   622
Goal "2 : univ(A)";
clasohm@0
   623
by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1));
clasohm@760
   624
qed "two_in_univ";
clasohm@0
   625
wenzelm@5067
   626
Goalw [bool_def] "bool <= univ(A)";
wenzelm@4091
   627
by (blast_tac (claset() addSIs [zero_in_univ,one_in_univ]) 1);
clasohm@760
   628
qed "bool_subset_univ";
clasohm@0
   629
clasohm@782
   630
bind_thm ("bool_into_univ", (bool_subset_univ RS subsetD));
clasohm@0
   631
clasohm@0
   632
clasohm@0
   633
(** Closure under disjoint union **)
clasohm@0
   634
paulson@5137
   635
Goalw [univ_def] "a: univ(A) ==> Inl(a) : univ(A)";
lcp@516
   636
by (etac (Limit_nat RSN (2,Inl_in_VLimit)) 1);
clasohm@760
   637
qed "Inl_in_univ";
clasohm@0
   638
paulson@5137
   639
Goalw [univ_def] "b: univ(A) ==> Inr(b) : univ(A)";
lcp@516
   640
by (etac (Limit_nat RSN (2,Inr_in_VLimit)) 1);
clasohm@760
   641
qed "Inr_in_univ";
clasohm@0
   642
wenzelm@5067
   643
Goalw [univ_def] "univ(C)+univ(C) <= univ(C)";
lcp@516
   644
by (rtac (Limit_nat RS sum_VLimit) 1);
clasohm@760
   645
qed "sum_univ";
clasohm@0
   646
lcp@803
   647
bind_thm ("sum_subset_univ", [sum_mono, sum_univ] MRS subset_trans);
lcp@484
   648
lcp@484
   649
clasohm@0
   650
(** Closure under binary union -- use Un_least **)
clasohm@0
   651
(** Closure under Collect -- use  (Collect_subset RS subset_trans)  **)
clasohm@0
   652
(** Closure under RepFun -- use   RepFun_subset  **)
lcp@803
   653
lcp@803
   654
lcp@803
   655
(*** Finite Branching Closure Properties ***)
lcp@803
   656
lcp@803
   657
(** Closure under finite powerset **)
lcp@803
   658
paulson@5147
   659
Goal "[| b: Fin(Vfrom(A,i));  Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i";
clasohm@1461
   660
by (etac Fin_induct 1);
wenzelm@4091
   661
by (blast_tac (claset() addSDs [Limit_has_0]) 1);
paulson@4152
   662
by Safe_tac;
clasohm@1461
   663
by (etac Limit_VfromE 1);
lcp@803
   664
by (assume_tac 1);
wenzelm@4091
   665
by (blast_tac (claset() addSIs [Un_least_lt] addIs [Vfrom_UnI1, Vfrom_UnI2]) 1);
lcp@803
   666
val Fin_Vfrom_lemma = result();
lcp@803
   667
paulson@5137
   668
Goal "Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)";
lcp@803
   669
by (rtac subsetI 1);
clasohm@1461
   670
by (dtac Fin_Vfrom_lemma 1);
paulson@4152
   671
by Safe_tac;
lcp@803
   672
by (resolve_tac [Vfrom RS ssubst] 1);
wenzelm@4091
   673
by (blast_tac (claset() addSDs [ltD]) 1);
lcp@803
   674
val Fin_VLimit = result();
lcp@803
   675
lcp@803
   676
bind_thm ("Fin_subset_VLimit", [Fin_mono, Fin_VLimit] MRS subset_trans);
lcp@803
   677
wenzelm@5067
   678
Goalw [univ_def] "Fin(univ(A)) <= univ(A)";
lcp@803
   679
by (rtac (Limit_nat RS Fin_VLimit) 1);
lcp@803
   680
val Fin_univ = result();
lcp@803
   681
lcp@803
   682
(** Closure under finite powers (functions from a fixed natural number) **)
lcp@803
   683
paulson@5147
   684
Goal "[| n: nat;  Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)";
lcp@803
   685
by (eresolve_tac [nat_fun_subset_Fin RS subset_trans] 1);
lcp@803
   686
by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit,
clasohm@1461
   687
                      nat_subset_VLimit, subset_refl] 1));
lcp@803
   688
val nat_fun_VLimit = result();
lcp@803
   689
lcp@803
   690
bind_thm ("nat_fun_subset_VLimit", [Pi_mono, nat_fun_VLimit] MRS subset_trans);
lcp@803
   691
paulson@5137
   692
Goalw [univ_def] "n: nat ==> n -> univ(A) <= univ(A)";
lcp@803
   693
by (etac (Limit_nat RSN (2,nat_fun_VLimit)) 1);
lcp@803
   694
val nat_fun_univ = result();
lcp@803
   695
lcp@803
   696
lcp@803
   697
(** Closure under finite function space **)
lcp@803
   698
lcp@803
   699
(*General but seldom-used version; normally the domain is fixed*)
paulson@5147
   700
Goal "Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) <= Vfrom(A,i)";
lcp@803
   701
by (resolve_tac [FiniteFun.dom_subset RS subset_trans] 1);
lcp@803
   702
by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit, subset_refl] 1));
lcp@803
   703
val FiniteFun_VLimit1 = result();
lcp@803
   704
wenzelm@5067
   705
Goalw [univ_def] "univ(A) -||> univ(A) <= univ(A)";
lcp@803
   706
by (rtac (Limit_nat RS FiniteFun_VLimit1) 1);
lcp@803
   707
val FiniteFun_univ1 = result();
lcp@803
   708
lcp@803
   709
(*Version for a fixed domain*)
paulson@5147
   710
Goal "[| W <= Vfrom(A,i); Limit(i) |] ==> W -||> Vfrom(A,i) <= Vfrom(A,i)";
lcp@803
   711
by (eresolve_tac [subset_refl RSN (2, FiniteFun_mono) RS subset_trans] 1);
clasohm@1461
   712
by (etac FiniteFun_VLimit1 1);
lcp@803
   713
val FiniteFun_VLimit = result();
lcp@803
   714
wenzelm@5067
   715
Goalw [univ_def]
paulson@5147
   716
    "W <= univ(A) ==> W -||> univ(A) <= univ(A)";
lcp@803
   717
by (etac (Limit_nat RSN (2, FiniteFun_VLimit)) 1);
lcp@803
   718
val FiniteFun_univ = result();
lcp@803
   719
paulson@5147
   720
Goal "[| f: W -||> univ(A);  W <= univ(A) |] ==> f : univ(A)";
lcp@803
   721
by (eresolve_tac [FiniteFun_univ RS subsetD] 1);
lcp@803
   722
by (assume_tac 1);
lcp@803
   723
val FiniteFun_in_univ = result();
lcp@803
   724
lcp@803
   725
(*Remove <= from the rule above*)
lcp@803
   726
val FiniteFun_in_univ' = subsetI RSN (2, FiniteFun_in_univ);
lcp@803
   727
lcp@803
   728
paulson@5321
   729
(**** For QUniv.  Properties of Vfrom analogous to the "take-lemma" ****)
paulson@5321
   730
paulson@5321
   731
(*** Intersecting a*b with Vfrom... ***)
paulson@5321
   732
paulson@5321
   733
(*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*)
paulson@5321
   734
Goal "[| {a,b} : Vfrom(X,succ(i));  Transset(X) |]  \
paulson@5321
   735
\     ==> a: Vfrom(X,i)  &  b: Vfrom(X,i)";
paulson@5321
   736
by (dtac (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1);
paulson@5321
   737
by (assume_tac 1);
paulson@5321
   738
by (Fast_tac 1);
paulson@5321
   739
qed "doubleton_in_Vfrom_D";
paulson@5321
   740
paulson@5321
   741
(*This weaker version says a, b exist at the same level*)
paulson@5321
   742
bind_thm ("Vfrom_doubleton_D", Transset_Vfrom RS Transset_doubleton_D);
paulson@5321
   743
paulson@5321
   744
(** Using only the weaker theorem would prove <a,b> : Vfrom(X,i)
paulson@5321
   745
      implies a, b : Vfrom(X,i), which is useless for induction.
paulson@5321
   746
    Using only the stronger theorem would prove <a,b> : Vfrom(X,succ(succ(i)))
paulson@5321
   747
      implies a, b : Vfrom(X,i), leaving the succ(i) case untreated.
paulson@5321
   748
    The combination gives a reduction by precisely one level, which is
paulson@5321
   749
      most convenient for proofs.
paulson@5321
   750
**)
paulson@5321
   751
paulson@5321
   752
Goalw [Pair_def]
paulson@5321
   753
    "[| <a,b> : Vfrom(X,succ(i));  Transset(X) |]  \
paulson@5321
   754
\    ==> a: Vfrom(X,i)  &  b: Vfrom(X,i)";
paulson@5321
   755
by (blast_tac (claset() addSDs [doubleton_in_Vfrom_D, Vfrom_doubleton_D]) 1);
paulson@5321
   756
qed "Pair_in_Vfrom_D";
paulson@5321
   757
paulson@5321
   758
Goal "Transset(X) ==>          \
paulson@5321
   759
\      (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))";
paulson@5321
   760
by (blast_tac (claset() addSDs [Pair_in_Vfrom_D]) 1);
paulson@5321
   761
qed "product_Int_Vfrom_subset";
paulson@5321
   762