src/ZF/Univ.thy
author wenzelm
Tue Jul 31 19:40:22 2007 +0200 (2007-07-31)
changeset 24091 109f19a13872
parent 16417 9bc16273c2d4
child 24892 c663e675e177
permissions -rw-r--r--
added Tools/lin_arith.ML;
clasohm@1478
     1
(*  Title:      ZF/univ.thy
clasohm@0
     2
    ID:         $Id$
clasohm@1478
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1992  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Standard notation for Vset(i) is V(i), but users might want V for a variable
lcp@516
     7
lcp@516
     8
NOTE: univ(A) could be a translation; would simplify many proofs!
wenzelm@6093
     9
  But Ind_Syntax.univ refers to the constant "Univ.univ"
clasohm@0
    10
*)
clasohm@0
    11
paulson@13356
    12
header{*The Cumulative Hierarchy and a Small Universe for Recursive Types*}
paulson@13356
    13
haftmann@16417
    14
theory Univ imports Epsilon Cardinal begin
wenzelm@3923
    15
paulson@13163
    16
constdefs
paulson@13163
    17
  Vfrom       :: "[i,i]=>i"
paulson@13220
    18
    "Vfrom(A,i) == transrec(i, %x f. A Un (\<Union>y\<in>x. Pow(f`y)))"
clasohm@0
    19
paulson@13220
    20
syntax   Vset :: "i=>i"
clasohm@0
    21
translations
clasohm@1478
    22
    "Vset(x)"   ==      "Vfrom(0,x)"
clasohm@0
    23
wenzelm@3923
    24
paulson@13163
    25
constdefs
paulson@13163
    26
  Vrec        :: "[i, [i,i]=>i] =>i"
paulson@13163
    27
    "Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)).
paulson@13163
    28
 		 	   H(z, lam w:Vset(x). g`rank(w)`w)) ` a"
paulson@13163
    29
paulson@13163
    30
  Vrecursor   :: "[[i,i]=>i, i] =>i"
paulson@13163
    31
    "Vrecursor(H,a) == transrec(rank(a), %x g. lam z: Vset(succ(x)).
paulson@13163
    32
				H(lam w:Vset(x). g`rank(w)`w, z)) ` a"
paulson@13163
    33
paulson@13163
    34
  univ        :: "i=>i"
paulson@13163
    35
    "univ(A) == Vfrom(A,nat)"
paulson@13163
    36
paulson@13163
    37
paulson@13356
    38
subsection{*Immediate Consequences of the Definition of @{term "Vfrom(A,i)"}*}
paulson@13356
    39
paulson@13163
    40
text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*}
paulson@13220
    41
lemma Vfrom: "Vfrom(A,i) = A Un (\<Union>j\<in>i. Pow(Vfrom(A,j)))"
paulson@13269
    42
by (subst Vfrom_def [THEN def_transrec], simp)
paulson@13163
    43
paulson@13163
    44
subsubsection{* Monotonicity *}
paulson@13163
    45
paulson@13163
    46
lemma Vfrom_mono [rule_format]:
paulson@13220
    47
     "A<=B ==> \<forall>j. i<=j --> Vfrom(A,i) <= Vfrom(B,j)"
paulson@13163
    48
apply (rule_tac a=i in eps_induct)
paulson@13163
    49
apply (rule impI [THEN allI])
paulson@15481
    50
apply (subst Vfrom [of A])
paulson@15481
    51
apply (subst Vfrom [of B])
paulson@13163
    52
apply (erule Un_mono)
paulson@13163
    53
apply (erule UN_mono, blast) 
paulson@13163
    54
done
paulson@13163
    55
paulson@13220
    56
lemma VfromI: "[| a \<in> Vfrom(A,j);  j<i |] ==> a \<in> Vfrom(A,i)"
paulson@13203
    57
by (blast dest: Vfrom_mono [OF subset_refl le_imp_subset [OF leI]]) 
paulson@13203
    58
paulson@13163
    59
paulson@13163
    60
subsubsection{* A fundamental equality: Vfrom does not require ordinals! *}
paulson@13163
    61
paulson@15481
    62
paulson@15481
    63
paulson@13163
    64
lemma Vfrom_rank_subset1: "Vfrom(A,x) <= Vfrom(A,rank(x))"
paulson@15481
    65
proof (induct x rule: eps_induct)
paulson@15481
    66
  fix x
paulson@15481
    67
  assume "\<forall>y\<in>x. Vfrom(A,y) \<subseteq> Vfrom(A,rank(y))"
paulson@15481
    68
  thus "Vfrom(A, x) \<subseteq> Vfrom(A, rank(x))"
paulson@15481
    69
    by (simp add: Vfrom [of _ x] Vfrom [of _ "rank(x)"],
paulson@15481
    70
        blast intro!: rank_lt [THEN ltD])
paulson@15481
    71
qed
paulson@13163
    72
paulson@13163
    73
lemma Vfrom_rank_subset2: "Vfrom(A,rank(x)) <= Vfrom(A,x)"
paulson@13163
    74
apply (rule_tac a=x in eps_induct)
paulson@13163
    75
apply (subst Vfrom)
paulson@15481
    76
apply (subst Vfrom, rule subset_refl [THEN Un_mono])
paulson@13163
    77
apply (rule UN_least)
wenzelm@13288
    78
txt{*expand @{text "rank(x1) = (\<Union>y\<in>x1. succ(rank(y)))"} in assumptions*}
paulson@13163
    79
apply (erule rank [THEN equalityD1, THEN subsetD, THEN UN_E])
paulson@13163
    80
apply (rule subset_trans)
paulson@13163
    81
apply (erule_tac [2] UN_upper)
paulson@13163
    82
apply (rule subset_refl [THEN Vfrom_mono, THEN subset_trans, THEN Pow_mono])
paulson@13163
    83
apply (erule ltI [THEN le_imp_subset])
paulson@13163
    84
apply (rule Ord_rank [THEN Ord_succ])
paulson@13163
    85
apply (erule bspec, assumption)
paulson@13163
    86
done
paulson@13163
    87
paulson@13163
    88
lemma Vfrom_rank_eq: "Vfrom(A,rank(x)) = Vfrom(A,x)"
paulson@13163
    89
apply (rule equalityI)
paulson@13163
    90
apply (rule Vfrom_rank_subset2)
paulson@13163
    91
apply (rule Vfrom_rank_subset1)
paulson@13163
    92
done
paulson@13163
    93
paulson@13163
    94
paulson@13356
    95
subsection{* Basic Closure Properties *}
paulson@13163
    96
paulson@13220
    97
lemma zero_in_Vfrom: "y:x ==> 0 \<in> Vfrom(A,x)"
paulson@13163
    98
by (subst Vfrom, blast)
paulson@13163
    99
paulson@13163
   100
lemma i_subset_Vfrom: "i <= Vfrom(A,i)"
paulson@13163
   101
apply (rule_tac a=i in eps_induct)
paulson@13163
   102
apply (subst Vfrom, blast)
paulson@13163
   103
done
paulson@13163
   104
paulson@13163
   105
lemma A_subset_Vfrom: "A <= Vfrom(A,i)"
paulson@13163
   106
apply (subst Vfrom)
paulson@13163
   107
apply (rule Un_upper1)
paulson@13163
   108
done
paulson@13163
   109
paulson@13163
   110
lemmas A_into_Vfrom = A_subset_Vfrom [THEN subsetD]
paulson@13163
   111
paulson@13220
   112
lemma subset_mem_Vfrom: "a <= Vfrom(A,i) ==> a \<in> Vfrom(A,succ(i))"
paulson@13163
   113
by (subst Vfrom, blast)
paulson@13163
   114
paulson@13163
   115
subsubsection{* Finite sets and ordered pairs *}
paulson@13163
   116
paulson@13220
   117
lemma singleton_in_Vfrom: "a \<in> Vfrom(A,i) ==> {a} \<in> Vfrom(A,succ(i))"
paulson@13163
   118
by (rule subset_mem_Vfrom, safe)
paulson@13163
   119
paulson@13163
   120
lemma doubleton_in_Vfrom:
paulson@13220
   121
     "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i) |] ==> {a,b} \<in> Vfrom(A,succ(i))"
paulson@13163
   122
by (rule subset_mem_Vfrom, safe)
paulson@13163
   123
paulson@13163
   124
lemma Pair_in_Vfrom:
paulson@13220
   125
    "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i) |] ==> <a,b> \<in> Vfrom(A,succ(succ(i)))"
paulson@13163
   126
apply (unfold Pair_def)
paulson@13163
   127
apply (blast intro: doubleton_in_Vfrom) 
paulson@13163
   128
done
paulson@13163
   129
paulson@13220
   130
lemma succ_in_Vfrom: "a <= Vfrom(A,i) ==> succ(a) \<in> Vfrom(A,succ(succ(i)))"
paulson@13163
   131
apply (intro subset_mem_Vfrom succ_subsetI, assumption)
paulson@13163
   132
apply (erule subset_trans) 
paulson@13163
   133
apply (rule Vfrom_mono [OF subset_refl subset_succI]) 
paulson@13163
   134
done
paulson@13163
   135
paulson@13356
   136
subsection{* 0, Successor and Limit Equations for @{term Vfrom} *}
paulson@13163
   137
paulson@13163
   138
lemma Vfrom_0: "Vfrom(A,0) = A"
paulson@13163
   139
by (subst Vfrom, blast)
paulson@13163
   140
paulson@13163
   141
lemma Vfrom_succ_lemma: "Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"
paulson@13163
   142
apply (rule Vfrom [THEN trans])
paulson@13163
   143
apply (rule equalityI [THEN subst_context, 
paulson@13163
   144
                       OF _ succI1 [THEN RepFunI, THEN Union_upper]])
paulson@13163
   145
apply (rule UN_least)
paulson@13163
   146
apply (rule subset_refl [THEN Vfrom_mono, THEN Pow_mono])
paulson@13163
   147
apply (erule ltI [THEN le_imp_subset])
paulson@13163
   148
apply (erule Ord_succ)
paulson@13163
   149
done
paulson@13163
   150
paulson@13163
   151
lemma Vfrom_succ: "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"
paulson@13163
   152
apply (rule_tac x1 = "succ (i)" in Vfrom_rank_eq [THEN subst])
paulson@13784
   153
apply (rule_tac x1 = i in Vfrom_rank_eq [THEN subst])
paulson@13163
   154
apply (subst rank_succ)
paulson@13163
   155
apply (rule Ord_rank [THEN Vfrom_succ_lemma])
paulson@13163
   156
done
paulson@13163
   157
paulson@13163
   158
(*The premise distinguishes this from Vfrom(A,0);  allowing X=0 forces
paulson@13220
   159
  the conclusion to be Vfrom(A,Union(X)) = A Un (\<Union>y\<in>X. Vfrom(A,y)) *)
paulson@13220
   160
lemma Vfrom_Union: "y:X ==> Vfrom(A,Union(X)) = (\<Union>y\<in>X. Vfrom(A,y))"
paulson@13163
   161
apply (subst Vfrom)
paulson@13163
   162
apply (rule equalityI)
paulson@13163
   163
txt{*first inclusion*}
paulson@13163
   164
apply (rule Un_least)
paulson@13163
   165
apply (rule A_subset_Vfrom [THEN subset_trans])
paulson@13163
   166
apply (rule UN_upper, assumption)
paulson@13163
   167
apply (rule UN_least)
paulson@13163
   168
apply (erule UnionE)
paulson@13163
   169
apply (rule subset_trans)
paulson@13163
   170
apply (erule_tac [2] UN_upper,
paulson@13163
   171
       subst Vfrom, erule subset_trans [OF UN_upper Un_upper2])
paulson@13163
   172
txt{*opposite inclusion*}
paulson@13163
   173
apply (rule UN_least)
paulson@13163
   174
apply (subst Vfrom, blast)
paulson@13163
   175
done
paulson@13163
   176
paulson@13356
   177
subsection{* @{term Vfrom} applied to Limit Ordinals *}
paulson@13163
   178
paulson@13163
   179
(*NB. limit ordinals are non-empty:
paulson@13220
   180
      Vfrom(A,0) = A = A Un (\<Union>y\<in>0. Vfrom(A,y)) *)
paulson@13163
   181
lemma Limit_Vfrom_eq:
paulson@13220
   182
    "Limit(i) ==> Vfrom(A,i) = (\<Union>y\<in>i. Vfrom(A,y))"
paulson@13163
   183
apply (rule Limit_has_0 [THEN ltD, THEN Vfrom_Union, THEN subst], assumption)
paulson@13163
   184
apply (simp add: Limit_Union_eq) 
paulson@13163
   185
done
paulson@13163
   186
paulson@13163
   187
lemma Limit_VfromE:
paulson@13220
   188
    "[| a \<in> Vfrom(A,i);  ~R ==> Limit(i);
paulson@13220
   189
        !!x. [| x<i;  a \<in> Vfrom(A,x) |] ==> R
paulson@13163
   190
     |] ==> R"
paulson@13163
   191
apply (rule classical)
paulson@13163
   192
apply (rule Limit_Vfrom_eq [THEN equalityD1, THEN subsetD, THEN UN_E])
paulson@13203
   193
  prefer 2 apply assumption
paulson@13203
   194
 apply blast 
paulson@13203
   195
apply (blast intro: ltI Limit_is_Ord)
paulson@13163
   196
done
paulson@13163
   197
paulson@13163
   198
lemma singleton_in_VLimit:
paulson@13220
   199
    "[| a \<in> Vfrom(A,i);  Limit(i) |] ==> {a} \<in> Vfrom(A,i)"
paulson@13163
   200
apply (erule Limit_VfromE, assumption)
paulson@13203
   201
apply (erule singleton_in_Vfrom [THEN VfromI])
paulson@13163
   202
apply (blast intro: Limit_has_succ) 
paulson@13163
   203
done
paulson@13163
   204
paulson@13163
   205
lemmas Vfrom_UnI1 = 
paulson@13163
   206
    Un_upper1 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD], standard]
paulson@13163
   207
lemmas Vfrom_UnI2 = 
paulson@13163
   208
    Un_upper2 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD], standard]
paulson@13163
   209
paulson@13163
   210
text{*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*}
paulson@13163
   211
lemma doubleton_in_VLimit:
paulson@13220
   212
    "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i);  Limit(i) |] ==> {a,b} \<in> Vfrom(A,i)"
paulson@13163
   213
apply (erule Limit_VfromE, assumption)
paulson@13163
   214
apply (erule Limit_VfromE, assumption)
paulson@13203
   215
apply (blast intro:  VfromI [OF doubleton_in_Vfrom]
paulson@13163
   216
                     Vfrom_UnI1 Vfrom_UnI2 Limit_has_succ Un_least_lt)
paulson@13163
   217
done
paulson@13163
   218
paulson@13163
   219
lemma Pair_in_VLimit:
paulson@13220
   220
    "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i);  Limit(i) |] ==> <a,b> \<in> Vfrom(A,i)"
paulson@13163
   221
txt{*Infer that a, b occur at ordinals x,xa < i.*}
paulson@13163
   222
apply (erule Limit_VfromE, assumption)
paulson@13163
   223
apply (erule Limit_VfromE, assumption)
paulson@13163
   224
txt{*Infer that succ(succ(x Un xa)) < i *}
paulson@13203
   225
apply (blast intro: VfromI [OF Pair_in_Vfrom]
paulson@13203
   226
                    Vfrom_UnI1 Vfrom_UnI2 Limit_has_succ Un_least_lt)
paulson@13163
   227
done
paulson@13163
   228
paulson@13163
   229
lemma product_VLimit: "Limit(i) ==> Vfrom(A,i) * Vfrom(A,i) <= Vfrom(A,i)"
paulson@13163
   230
by (blast intro: Pair_in_VLimit)
paulson@13163
   231
paulson@13163
   232
lemmas Sigma_subset_VLimit =
paulson@13163
   233
     subset_trans [OF Sigma_mono product_VLimit]
paulson@13163
   234
paulson@13163
   235
lemmas nat_subset_VLimit =
paulson@13163
   236
     subset_trans [OF nat_le_Limit [THEN le_imp_subset] i_subset_Vfrom]
paulson@13163
   237
paulson@13220
   238
lemma nat_into_VLimit: "[| n: nat;  Limit(i) |] ==> n \<in> Vfrom(A,i)"
paulson@13163
   239
by (blast intro: nat_subset_VLimit [THEN subsetD])
paulson@13163
   240
paulson@13356
   241
subsubsection{* Closure under Disjoint Union *}
paulson@13163
   242
paulson@13163
   243
lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom, standard]
paulson@13163
   244
paulson@13220
   245
lemma one_in_VLimit: "Limit(i) ==> 1 \<in> Vfrom(A,i)"
paulson@13163
   246
by (blast intro: nat_into_VLimit)
paulson@13163
   247
paulson@13163
   248
lemma Inl_in_VLimit:
paulson@13220
   249
    "[| a \<in> Vfrom(A,i); Limit(i) |] ==> Inl(a) \<in> Vfrom(A,i)"
paulson@13163
   250
apply (unfold Inl_def)
paulson@13163
   251
apply (blast intro: zero_in_VLimit Pair_in_VLimit)
paulson@13163
   252
done
paulson@13163
   253
paulson@13163
   254
lemma Inr_in_VLimit:
paulson@13220
   255
    "[| b \<in> Vfrom(A,i); Limit(i) |] ==> Inr(b) \<in> Vfrom(A,i)"
paulson@13163
   256
apply (unfold Inr_def)
paulson@13163
   257
apply (blast intro: one_in_VLimit Pair_in_VLimit)
paulson@13163
   258
done
paulson@13163
   259
paulson@13163
   260
lemma sum_VLimit: "Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)"
paulson@13163
   261
by (blast intro!: Inl_in_VLimit Inr_in_VLimit)
paulson@13163
   262
paulson@13163
   263
lemmas sum_subset_VLimit = subset_trans [OF sum_mono sum_VLimit]
paulson@13163
   264
paulson@13163
   265
paulson@13163
   266
paulson@13356
   267
subsection{* Properties assuming @{term "Transset(A)"} *}
paulson@13163
   268
paulson@13163
   269
lemma Transset_Vfrom: "Transset(A) ==> Transset(Vfrom(A,i))"
paulson@13163
   270
apply (rule_tac a=i in eps_induct)
paulson@13163
   271
apply (subst Vfrom)
paulson@13163
   272
apply (blast intro!: Transset_Union_family Transset_Un Transset_Pow)
paulson@13163
   273
done
paulson@13163
   274
paulson@13163
   275
lemma Transset_Vfrom_succ:
paulson@13163
   276
     "Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))"
paulson@13163
   277
apply (rule Vfrom_succ [THEN trans])
paulson@13163
   278
apply (rule equalityI [OF _ Un_upper2])
paulson@13163
   279
apply (rule Un_least [OF _ subset_refl])
paulson@13163
   280
apply (rule A_subset_Vfrom [THEN subset_trans])
paulson@13163
   281
apply (erule Transset_Vfrom [THEN Transset_iff_Pow [THEN iffD1]])
paulson@13163
   282
done
paulson@13163
   283
paulson@13163
   284
lemma Transset_Pair_subset: "[| <a,b> <= C; Transset(C) |] ==> a: C & b: C"
paulson@13163
   285
by (unfold Pair_def Transset_def, blast)
paulson@13163
   286
paulson@13163
   287
lemma Transset_Pair_subset_VLimit:
paulson@13163
   288
     "[| <a,b> <= Vfrom(A,i);  Transset(A);  Limit(i) |]
paulson@13220
   289
      ==> <a,b> \<in> Vfrom(A,i)"
paulson@13163
   290
apply (erule Transset_Pair_subset [THEN conjE])
paulson@13163
   291
apply (erule Transset_Vfrom)
paulson@13163
   292
apply (blast intro: Pair_in_VLimit)
paulson@13163
   293
done
paulson@13163
   294
paulson@13163
   295
lemma Union_in_Vfrom:
paulson@13220
   296
     "[| X \<in> Vfrom(A,j);  Transset(A) |] ==> Union(X) \<in> Vfrom(A, succ(j))"
paulson@13163
   297
apply (drule Transset_Vfrom)
paulson@13163
   298
apply (rule subset_mem_Vfrom)
paulson@13163
   299
apply (unfold Transset_def, blast)
paulson@13163
   300
done
paulson@13163
   301
paulson@13163
   302
lemma Union_in_VLimit:
paulson@13220
   303
     "[| X \<in> Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Union(X) \<in> Vfrom(A,i)"
paulson@13163
   304
apply (rule Limit_VfromE, assumption+)
paulson@13203
   305
apply (blast intro: Limit_has_succ VfromI Union_in_Vfrom)
paulson@13163
   306
done
paulson@13163
   307
paulson@13163
   308
paulson@13163
   309
(*** Closure under product/sum applied to elements -- thus Vfrom(A,i)
paulson@13163
   310
     is a model of simple type theory provided A is a transitive set
paulson@13163
   311
     and i is a limit ordinal
paulson@13163
   312
***)
paulson@13163
   313
paulson@13163
   314
text{*General theorem for membership in Vfrom(A,i) when i is a limit ordinal*}
paulson@13163
   315
lemma in_VLimit:
paulson@13220
   316
  "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i);  Limit(i);
paulson@13220
   317
      !!x y j. [| j<i; 1:j; x \<in> Vfrom(A,j); y \<in> Vfrom(A,j) |]
paulson@13220
   318
               ==> EX k. h(x,y) \<in> Vfrom(A,k) & k<i |]
paulson@13220
   319
   ==> h(a,b) \<in> Vfrom(A,i)"
paulson@13163
   320
txt{*Infer that a, b occur at ordinals x,xa < i.*}
paulson@13163
   321
apply (erule Limit_VfromE, assumption)
paulson@13163
   322
apply (erule Limit_VfromE, assumption, atomize)
paulson@13163
   323
apply (drule_tac x=a in spec) 
paulson@13163
   324
apply (drule_tac x=b in spec) 
paulson@13163
   325
apply (drule_tac x="x Un xa Un 2" in spec) 
paulson@13203
   326
apply (simp add: Un_least_lt_iff lt_Ord Vfrom_UnI1 Vfrom_UnI2) 
paulson@13203
   327
apply (blast intro: Limit_has_0 Limit_has_succ VfromI)
paulson@13163
   328
done
paulson@13163
   329
paulson@13356
   330
subsubsection{* Products *}
paulson@13163
   331
paulson@13163
   332
lemma prod_in_Vfrom:
paulson@13220
   333
    "[| a \<in> Vfrom(A,j);  b \<in> Vfrom(A,j);  Transset(A) |]
paulson@13220
   334
     ==> a*b \<in> Vfrom(A, succ(succ(succ(j))))"
paulson@13163
   335
apply (drule Transset_Vfrom)
paulson@13163
   336
apply (rule subset_mem_Vfrom)
paulson@13163
   337
apply (unfold Transset_def)
paulson@13163
   338
apply (blast intro: Pair_in_Vfrom)
paulson@13163
   339
done
paulson@13163
   340
paulson@13163
   341
lemma prod_in_VLimit:
paulson@13220
   342
  "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i);  Limit(i);  Transset(A) |]
paulson@13220
   343
   ==> a*b \<in> Vfrom(A,i)"
paulson@13163
   344
apply (erule in_VLimit, assumption+)
paulson@13163
   345
apply (blast intro: prod_in_Vfrom Limit_has_succ)
paulson@13163
   346
done
paulson@13163
   347
paulson@13356
   348
subsubsection{* Disjoint Sums, or Quine Ordered Pairs *}
paulson@13163
   349
paulson@13163
   350
lemma sum_in_Vfrom:
paulson@13220
   351
    "[| a \<in> Vfrom(A,j);  b \<in> Vfrom(A,j);  Transset(A);  1:j |]
paulson@13220
   352
     ==> a+b \<in> Vfrom(A, succ(succ(succ(j))))"
paulson@13163
   353
apply (unfold sum_def)
paulson@13163
   354
apply (drule Transset_Vfrom)
paulson@13163
   355
apply (rule subset_mem_Vfrom)
paulson@13163
   356
apply (unfold Transset_def)
paulson@13163
   357
apply (blast intro: zero_in_Vfrom Pair_in_Vfrom i_subset_Vfrom [THEN subsetD])
paulson@13163
   358
done
paulson@13163
   359
paulson@13163
   360
lemma sum_in_VLimit:
paulson@13220
   361
  "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i);  Limit(i);  Transset(A) |]
paulson@13220
   362
   ==> a+b \<in> Vfrom(A,i)"
paulson@13163
   363
apply (erule in_VLimit, assumption+)
paulson@13163
   364
apply (blast intro: sum_in_Vfrom Limit_has_succ)
paulson@13163
   365
done
paulson@13163
   366
paulson@13356
   367
subsubsection{* Function Space! *}
paulson@13163
   368
paulson@13163
   369
lemma fun_in_Vfrom:
paulson@13220
   370
    "[| a \<in> Vfrom(A,j);  b \<in> Vfrom(A,j);  Transset(A) |] ==>
paulson@13220
   371
          a->b \<in> Vfrom(A, succ(succ(succ(succ(j)))))"
paulson@13163
   372
apply (unfold Pi_def)
paulson@13163
   373
apply (drule Transset_Vfrom)
paulson@13163
   374
apply (rule subset_mem_Vfrom)
paulson@13163
   375
apply (rule Collect_subset [THEN subset_trans])
paulson@13163
   376
apply (subst Vfrom)
paulson@13163
   377
apply (rule subset_trans [THEN subset_trans])
paulson@13163
   378
apply (rule_tac [3] Un_upper2)
paulson@13163
   379
apply (rule_tac [2] succI1 [THEN UN_upper])
paulson@13163
   380
apply (rule Pow_mono)
paulson@13163
   381
apply (unfold Transset_def)
paulson@13163
   382
apply (blast intro: Pair_in_Vfrom)
paulson@13163
   383
done
paulson@13163
   384
paulson@13163
   385
lemma fun_in_VLimit:
paulson@13220
   386
  "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i);  Limit(i);  Transset(A) |]
paulson@13220
   387
   ==> a->b \<in> Vfrom(A,i)"
paulson@13163
   388
apply (erule in_VLimit, assumption+)
paulson@13163
   389
apply (blast intro: fun_in_Vfrom Limit_has_succ)
paulson@13163
   390
done
paulson@13163
   391
paulson@13163
   392
lemma Pow_in_Vfrom:
paulson@13220
   393
    "[| a \<in> Vfrom(A,j);  Transset(A) |] ==> Pow(a) \<in> Vfrom(A, succ(succ(j)))"
paulson@13163
   394
apply (drule Transset_Vfrom)
paulson@13163
   395
apply (rule subset_mem_Vfrom)
paulson@13163
   396
apply (unfold Transset_def)
paulson@13163
   397
apply (subst Vfrom, blast)
paulson@13163
   398
done
paulson@13163
   399
paulson@13163
   400
lemma Pow_in_VLimit:
paulson@13220
   401
     "[| a \<in> Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Pow(a) \<in> Vfrom(A,i)"
paulson@13203
   402
by (blast elim: Limit_VfromE intro: Limit_has_succ Pow_in_Vfrom VfromI)
paulson@13163
   403
paulson@13163
   404
paulson@13356
   405
subsection{* The Set @{term "Vset(i)"} *}
paulson@13163
   406
paulson@13220
   407
lemma Vset: "Vset(i) = (\<Union>j\<in>i. Pow(Vset(j)))"
paulson@13163
   408
by (subst Vfrom, blast)
paulson@13163
   409
paulson@13163
   410
lemmas Vset_succ = Transset_0 [THEN Transset_Vfrom_succ, standard]
paulson@13163
   411
lemmas Transset_Vset = Transset_0 [THEN Transset_Vfrom, standard]
paulson@13163
   412
paulson@13356
   413
subsubsection{* Characterisation of the elements of @{term "Vset(i)"} *}
paulson@13163
   414
paulson@13220
   415
lemma VsetD [rule_format]: "Ord(i) ==> \<forall>b. b \<in> Vset(i) --> rank(b) < i"
paulson@13163
   416
apply (erule trans_induct)
paulson@13163
   417
apply (subst Vset, safe)
paulson@13163
   418
apply (subst rank)
paulson@13163
   419
apply (blast intro: ltI UN_succ_least_lt) 
paulson@13163
   420
done
paulson@13163
   421
paulson@13163
   422
lemma VsetI_lemma [rule_format]:
paulson@13220
   423
     "Ord(i) ==> \<forall>b. rank(b) \<in> i --> b \<in> Vset(i)"
paulson@13163
   424
apply (erule trans_induct)
paulson@13163
   425
apply (rule allI)
paulson@13163
   426
apply (subst Vset)
paulson@13163
   427
apply (blast intro!: rank_lt [THEN ltD])
paulson@13163
   428
done
paulson@13163
   429
paulson@13220
   430
lemma VsetI: "rank(x)<i ==> x \<in> Vset(i)"
paulson@13163
   431
by (blast intro: VsetI_lemma elim: ltE)
paulson@13163
   432
paulson@13163
   433
text{*Merely a lemma for the next result*}
paulson@13220
   434
lemma Vset_Ord_rank_iff: "Ord(i) ==> b \<in> Vset(i) <-> rank(b) < i"
paulson@13163
   435
by (blast intro: VsetD VsetI)
paulson@13163
   436
paulson@13220
   437
lemma Vset_rank_iff [simp]: "b \<in> Vset(a) <-> rank(b) < rank(a)"
paulson@13163
   438
apply (rule Vfrom_rank_eq [THEN subst])
paulson@13163
   439
apply (rule Ord_rank [THEN Vset_Ord_rank_iff])
paulson@13163
   440
done
paulson@13163
   441
paulson@13163
   442
text{*This is rank(rank(a)) = rank(a) *}
paulson@13163
   443
declare Ord_rank [THEN rank_of_Ord, simp]
paulson@13163
   444
paulson@13163
   445
lemma rank_Vset: "Ord(i) ==> rank(Vset(i)) = i"
paulson@13163
   446
apply (subst rank)
paulson@13163
   447
apply (rule equalityI, safe)
paulson@13163
   448
apply (blast intro: VsetD [THEN ltD]) 
paulson@13163
   449
apply (blast intro: VsetD [THEN ltD] Ord_trans) 
paulson@13163
   450
apply (blast intro: i_subset_Vfrom [THEN subsetD]
paulson@13163
   451
                    Ord_in_Ord [THEN rank_of_Ord, THEN ssubst])
paulson@13163
   452
done
paulson@13163
   453
paulson@13269
   454
lemma Finite_Vset: "i \<in> nat ==> Finite(Vset(i))";
paulson@13269
   455
apply (erule nat_induct)
paulson@13269
   456
 apply (simp add: Vfrom_0) 
paulson@13269
   457
apply (simp add: Vset_succ) 
paulson@13269
   458
done
paulson@13269
   459
paulson@13356
   460
subsubsection{* Reasoning about Sets in Terms of Their Elements' Ranks *}
clasohm@0
   461
paulson@13163
   462
lemma arg_subset_Vset_rank: "a <= Vset(rank(a))"
paulson@13163
   463
apply (rule subsetI)
paulson@13163
   464
apply (erule rank_lt [THEN VsetI])
paulson@13163
   465
done
paulson@13163
   466
paulson@13163
   467
lemma Int_Vset_subset:
paulson@13163
   468
    "[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b"
paulson@13163
   469
apply (rule subset_trans) 
paulson@13163
   470
apply (rule Int_greatest [OF subset_refl arg_subset_Vset_rank])
paulson@13163
   471
apply (blast intro: Ord_rank) 
paulson@13163
   472
done
paulson@13163
   473
paulson@13356
   474
subsubsection{* Set Up an Environment for Simplification *}
paulson@13163
   475
paulson@13163
   476
lemma rank_Inl: "rank(a) < rank(Inl(a))"
paulson@13163
   477
apply (unfold Inl_def)
paulson@13163
   478
apply (rule rank_pair2)
paulson@13163
   479
done
paulson@13163
   480
paulson@13163
   481
lemma rank_Inr: "rank(a) < rank(Inr(a))"
paulson@13163
   482
apply (unfold Inr_def)
paulson@13163
   483
apply (rule rank_pair2)
paulson@13163
   484
done
paulson@13163
   485
paulson@13163
   486
lemmas rank_rls = rank_Inl rank_Inr rank_pair1 rank_pair2
paulson@13163
   487
paulson@13356
   488
subsubsection{* Recursion over Vset Levels! *}
paulson@13163
   489
paulson@13163
   490
text{*NOT SUITABLE FOR REWRITING: recursive!*}
paulson@13163
   491
lemma Vrec: "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))"
paulson@13163
   492
apply (unfold Vrec_def)
paulson@13269
   493
apply (subst transrec, simp)
paulson@13175
   494
apply (rule refl [THEN lam_cong, THEN subst_context], simp add: lt_def)
paulson@13163
   495
done
paulson@13163
   496
paulson@13163
   497
text{*This form avoids giant explosions in proofs.  NOTE USE OF == *}
paulson@13163
   498
lemma def_Vrec:
paulson@13163
   499
    "[| !!x. h(x)==Vrec(x,H) |] ==>
paulson@13163
   500
     h(a) = H(a, lam x: Vset(rank(a)). h(x))"
paulson@13163
   501
apply simp 
paulson@13163
   502
apply (rule Vrec)
paulson@13163
   503
done
paulson@13163
   504
paulson@13163
   505
text{*NOT SUITABLE FOR REWRITING: recursive!*}
paulson@13163
   506
lemma Vrecursor:
paulson@13163
   507
     "Vrecursor(H,a) = H(lam x:Vset(rank(a)). Vrecursor(H,x),  a)"
paulson@13163
   508
apply (unfold Vrecursor_def)
paulson@13163
   509
apply (subst transrec, simp)
paulson@13175
   510
apply (rule refl [THEN lam_cong, THEN subst_context], simp add: lt_def)
paulson@13163
   511
done
paulson@13163
   512
paulson@13163
   513
text{*This form avoids giant explosions in proofs.  NOTE USE OF == *}
paulson@13163
   514
lemma def_Vrecursor:
paulson@13163
   515
     "h == Vrecursor(H) ==> h(a) = H(lam x: Vset(rank(a)). h(x),  a)"
paulson@13163
   516
apply simp
paulson@13163
   517
apply (rule Vrecursor)
paulson@13163
   518
done
paulson@13163
   519
paulson@13163
   520
paulson@13356
   521
subsection{* The Datatype Universe: @{term "univ(A)"} *}
paulson@13163
   522
paulson@13163
   523
lemma univ_mono: "A<=B ==> univ(A) <= univ(B)"
paulson@13163
   524
apply (unfold univ_def)
paulson@13163
   525
apply (erule Vfrom_mono)
paulson@13163
   526
apply (rule subset_refl)
paulson@13163
   527
done
paulson@13163
   528
paulson@13163
   529
lemma Transset_univ: "Transset(A) ==> Transset(univ(A))"
paulson@13163
   530
apply (unfold univ_def)
paulson@13163
   531
apply (erule Transset_Vfrom)
paulson@13163
   532
done
paulson@13163
   533
paulson@13356
   534
subsubsection{* The Set @{term"univ(A)"} as a Limit *}
paulson@13163
   535
paulson@13220
   536
lemma univ_eq_UN: "univ(A) = (\<Union>i\<in>nat. Vfrom(A,i))"
paulson@13163
   537
apply (unfold univ_def)
paulson@13163
   538
apply (rule Limit_nat [THEN Limit_Vfrom_eq])
paulson@13163
   539
done
paulson@13163
   540
paulson@13220
   541
lemma subset_univ_eq_Int: "c <= univ(A) ==> c = (\<Union>i\<in>nat. c Int Vfrom(A,i))"
paulson@13163
   542
apply (rule subset_UN_iff_eq [THEN iffD1])
paulson@13163
   543
apply (erule univ_eq_UN [THEN subst])
paulson@13163
   544
done
paulson@13163
   545
paulson@13163
   546
lemma univ_Int_Vfrom_subset:
paulson@13163
   547
    "[| a <= univ(X);
paulson@13163
   548
        !!i. i:nat ==> a Int Vfrom(X,i) <= b |]
paulson@13163
   549
     ==> a <= b"
paulson@13163
   550
apply (subst subset_univ_eq_Int, assumption)
paulson@13163
   551
apply (rule UN_least, simp) 
paulson@13163
   552
done
paulson@13163
   553
paulson@13163
   554
lemma univ_Int_Vfrom_eq:
paulson@13163
   555
    "[| a <= univ(X);   b <= univ(X);
paulson@13163
   556
        !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i)
paulson@13163
   557
     |] ==> a = b"
paulson@13163
   558
apply (rule equalityI)
paulson@13163
   559
apply (rule univ_Int_Vfrom_subset, assumption)
paulson@13163
   560
apply (blast elim: equalityCE) 
paulson@13163
   561
apply (rule univ_Int_Vfrom_subset, assumption)
paulson@13163
   562
apply (blast elim: equalityCE) 
paulson@13163
   563
done
paulson@13163
   564
paulson@13356
   565
subsection{* Closure Properties for @{term "univ(A)"}*}
paulson@13163
   566
paulson@13220
   567
lemma zero_in_univ: "0 \<in> univ(A)"
paulson@13163
   568
apply (unfold univ_def)
paulson@13163
   569
apply (rule nat_0I [THEN zero_in_Vfrom])
paulson@13163
   570
done
paulson@13163
   571
paulson@13255
   572
lemma zero_subset_univ: "{0} <= univ(A)"
paulson@13255
   573
by (blast intro: zero_in_univ)
paulson@13255
   574
paulson@13163
   575
lemma A_subset_univ: "A <= univ(A)"
paulson@13163
   576
apply (unfold univ_def)
paulson@13163
   577
apply (rule A_subset_Vfrom)
paulson@13163
   578
done
paulson@13163
   579
paulson@13163
   580
lemmas A_into_univ = A_subset_univ [THEN subsetD, standard]
paulson@13163
   581
paulson@13356
   582
subsubsection{* Closure under Unordered and Ordered Pairs *}
paulson@13163
   583
paulson@13220
   584
lemma singleton_in_univ: "a: univ(A) ==> {a} \<in> univ(A)"
paulson@13163
   585
apply (unfold univ_def)
paulson@13163
   586
apply (blast intro: singleton_in_VLimit Limit_nat)
paulson@13163
   587
done
paulson@13163
   588
paulson@13163
   589
lemma doubleton_in_univ:
paulson@13220
   590
    "[| a: univ(A);  b: univ(A) |] ==> {a,b} \<in> univ(A)"
paulson@13163
   591
apply (unfold univ_def)
paulson@13163
   592
apply (blast intro: doubleton_in_VLimit Limit_nat)
paulson@13163
   593
done
paulson@13163
   594
paulson@13163
   595
lemma Pair_in_univ:
paulson@13220
   596
    "[| a: univ(A);  b: univ(A) |] ==> <a,b> \<in> univ(A)"
paulson@13163
   597
apply (unfold univ_def)
paulson@13163
   598
apply (blast intro: Pair_in_VLimit Limit_nat)
paulson@13163
   599
done
paulson@13163
   600
paulson@13163
   601
lemma Union_in_univ:
paulson@13220
   602
     "[| X: univ(A);  Transset(A) |] ==> Union(X) \<in> univ(A)"
paulson@13163
   603
apply (unfold univ_def)
paulson@13163
   604
apply (blast intro: Union_in_VLimit Limit_nat)
paulson@13163
   605
done
paulson@13163
   606
paulson@13163
   607
lemma product_univ: "univ(A)*univ(A) <= univ(A)"
paulson@13163
   608
apply (unfold univ_def)
paulson@13163
   609
apply (rule Limit_nat [THEN product_VLimit])
paulson@13163
   610
done
paulson@13163
   611
paulson@13163
   612
paulson@13356
   613
subsubsection{* The Natural Numbers *}
paulson@13163
   614
paulson@13163
   615
lemma nat_subset_univ: "nat <= univ(A)"
paulson@13163
   616
apply (unfold univ_def)
paulson@13163
   617
apply (rule i_subset_Vfrom)
paulson@13163
   618
done
paulson@13163
   619
paulson@13163
   620
text{* n:nat ==> n:univ(A) *}
paulson@13163
   621
lemmas nat_into_univ = nat_subset_univ [THEN subsetD, standard]
paulson@13163
   622
paulson@13356
   623
subsubsection{* Instances for 1 and 2 *}
paulson@13163
   624
paulson@13220
   625
lemma one_in_univ: "1 \<in> univ(A)"
paulson@13163
   626
apply (unfold univ_def)
paulson@13163
   627
apply (rule Limit_nat [THEN one_in_VLimit])
paulson@13163
   628
done
paulson@13163
   629
paulson@13163
   630
text{*unused!*}
paulson@13220
   631
lemma two_in_univ: "2 \<in> univ(A)"
paulson@13163
   632
by (blast intro: nat_into_univ)
paulson@13163
   633
paulson@13163
   634
lemma bool_subset_univ: "bool <= univ(A)"
paulson@13163
   635
apply (unfold bool_def)
paulson@13163
   636
apply (blast intro!: zero_in_univ one_in_univ)
paulson@13163
   637
done
paulson@13163
   638
paulson@13163
   639
lemmas bool_into_univ = bool_subset_univ [THEN subsetD, standard]
paulson@13163
   640
paulson@13163
   641
paulson@13356
   642
subsubsection{* Closure under Disjoint Union *}
paulson@13163
   643
paulson@13220
   644
lemma Inl_in_univ: "a: univ(A) ==> Inl(a) \<in> univ(A)"
paulson@13163
   645
apply (unfold univ_def)
paulson@13163
   646
apply (erule Inl_in_VLimit [OF _ Limit_nat])
paulson@13163
   647
done
paulson@13163
   648
paulson@13220
   649
lemma Inr_in_univ: "b: univ(A) ==> Inr(b) \<in> univ(A)"
paulson@13163
   650
apply (unfold univ_def)
paulson@13163
   651
apply (erule Inr_in_VLimit [OF _ Limit_nat])
paulson@13163
   652
done
paulson@13163
   653
paulson@13163
   654
lemma sum_univ: "univ(C)+univ(C) <= univ(C)"
paulson@13163
   655
apply (unfold univ_def)
paulson@13163
   656
apply (rule Limit_nat [THEN sum_VLimit])
paulson@13163
   657
done
paulson@13163
   658
paulson@13163
   659
lemmas sum_subset_univ = subset_trans [OF sum_mono sum_univ]
paulson@13163
   660
paulson@13255
   661
lemma Sigma_subset_univ:
paulson@13255
   662
  "[|A \<subseteq> univ(D); \<And>x. x \<in> A \<Longrightarrow> B(x) \<subseteq> univ(D)|] ==> Sigma(A,B) \<subseteq> univ(D)"
paulson@13255
   663
apply (simp add: univ_def)
paulson@13255
   664
apply (blast intro: Sigma_subset_VLimit del: subsetI) 
paulson@13255
   665
done
paulson@13163
   666
paulson@13255
   667
paulson@13255
   668
(*Closure under binary union -- use Un_least
paulson@13255
   669
  Closure under Collect -- use  Collect_subset [THEN subset_trans]
paulson@13255
   670
  Closure under RepFun -- use   RepFun_subset *)
paulson@13163
   671
paulson@13163
   672
paulson@13163
   673
subsection{* Finite Branching Closure Properties *}
paulson@13163
   674
paulson@13356
   675
subsubsection{* Closure under Finite Powerset *}
paulson@13163
   676
paulson@13163
   677
lemma Fin_Vfrom_lemma:
paulson@13163
   678
     "[| b: Fin(Vfrom(A,i));  Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i"
paulson@13163
   679
apply (erule Fin_induct)
paulson@13163
   680
apply (blast dest!: Limit_has_0, safe)
paulson@13163
   681
apply (erule Limit_VfromE, assumption)
paulson@13163
   682
apply (blast intro!: Un_least_lt intro: Vfrom_UnI1 Vfrom_UnI2)
paulson@13163
   683
done
clasohm@0
   684
paulson@13163
   685
lemma Fin_VLimit: "Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)"
paulson@13163
   686
apply (rule subsetI)
paulson@13163
   687
apply (drule Fin_Vfrom_lemma, safe)
paulson@13163
   688
apply (rule Vfrom [THEN ssubst])
paulson@13163
   689
apply (blast dest!: ltD)
paulson@13163
   690
done
paulson@13163
   691
paulson@13163
   692
lemmas Fin_subset_VLimit = subset_trans [OF Fin_mono Fin_VLimit]
paulson@13163
   693
paulson@13163
   694
lemma Fin_univ: "Fin(univ(A)) <= univ(A)"
paulson@13163
   695
apply (unfold univ_def)
paulson@13163
   696
apply (rule Limit_nat [THEN Fin_VLimit])
paulson@13163
   697
done
paulson@13163
   698
paulson@13356
   699
subsubsection{* Closure under Finite Powers: Functions from a Natural Number *}
paulson@13163
   700
paulson@13163
   701
lemma nat_fun_VLimit:
paulson@13163
   702
     "[| n: nat;  Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)"
paulson@13163
   703
apply (erule nat_fun_subset_Fin [THEN subset_trans])
paulson@13163
   704
apply (blast del: subsetI
paulson@13163
   705
    intro: subset_refl Fin_subset_VLimit Sigma_subset_VLimit nat_subset_VLimit)
paulson@13163
   706
done
paulson@13163
   707
paulson@13163
   708
lemmas nat_fun_subset_VLimit = subset_trans [OF Pi_mono nat_fun_VLimit]
paulson@13163
   709
paulson@13163
   710
lemma nat_fun_univ: "n: nat ==> n -> univ(A) <= univ(A)"
paulson@13163
   711
apply (unfold univ_def)
paulson@13163
   712
apply (erule nat_fun_VLimit [OF _ Limit_nat])
paulson@13163
   713
done
paulson@13163
   714
paulson@13163
   715
paulson@13356
   716
subsubsection{* Closure under Finite Function Space *}
paulson@13163
   717
paulson@13163
   718
text{*General but seldom-used version; normally the domain is fixed*}
paulson@13163
   719
lemma FiniteFun_VLimit1:
paulson@13163
   720
     "Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) <= Vfrom(A,i)"
paulson@13163
   721
apply (rule FiniteFun.dom_subset [THEN subset_trans])
paulson@13163
   722
apply (blast del: subsetI
paulson@13163
   723
             intro: Fin_subset_VLimit Sigma_subset_VLimit subset_refl)
paulson@13163
   724
done
paulson@13163
   725
paulson@13163
   726
lemma FiniteFun_univ1: "univ(A) -||> univ(A) <= univ(A)"
paulson@13163
   727
apply (unfold univ_def)
paulson@13163
   728
apply (rule Limit_nat [THEN FiniteFun_VLimit1])
paulson@13163
   729
done
paulson@13163
   730
paulson@13163
   731
text{*Version for a fixed domain*}
paulson@13163
   732
lemma FiniteFun_VLimit:
paulson@13163
   733
     "[| W <= Vfrom(A,i); Limit(i) |] ==> W -||> Vfrom(A,i) <= Vfrom(A,i)"
paulson@13163
   734
apply (rule subset_trans) 
paulson@13163
   735
apply (erule FiniteFun_mono [OF _ subset_refl])
paulson@13163
   736
apply (erule FiniteFun_VLimit1)
paulson@13163
   737
done
paulson@13163
   738
paulson@13163
   739
lemma FiniteFun_univ:
paulson@13163
   740
    "W <= univ(A) ==> W -||> univ(A) <= univ(A)"
paulson@13163
   741
apply (unfold univ_def)
paulson@13163
   742
apply (erule FiniteFun_VLimit [OF _ Limit_nat])
paulson@13163
   743
done
paulson@13163
   744
paulson@13163
   745
lemma FiniteFun_in_univ:
paulson@13220
   746
     "[| f: W -||> univ(A);  W <= univ(A) |] ==> f \<in> univ(A)"
paulson@13163
   747
by (erule FiniteFun_univ [THEN subsetD], assumption)
paulson@13163
   748
paulson@13163
   749
text{*Remove <= from the rule above*}
paulson@13163
   750
lemmas FiniteFun_in_univ' = FiniteFun_in_univ [OF _ subsetI]
paulson@13163
   751
paulson@13163
   752
paulson@13163
   753
subsection{** For QUniv.  Properties of Vfrom analogous to the "take-lemma" **}
paulson@13163
   754
paulson@13356
   755
text{* Intersecting a*b with Vfrom... *}
paulson@13163
   756
paulson@13163
   757
text{*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*}
paulson@13163
   758
lemma doubleton_in_Vfrom_D:
paulson@13220
   759
     "[| {a,b} \<in> Vfrom(X,succ(i));  Transset(X) |]
paulson@13220
   760
      ==> a \<in> Vfrom(X,i)  &  b \<in> Vfrom(X,i)"
paulson@13163
   761
by (drule Transset_Vfrom_succ [THEN equalityD1, THEN subsetD, THEN PowD], 
paulson@13163
   762
    assumption, fast)
paulson@13163
   763
paulson@13163
   764
text{*This weaker version says a, b exist at the same level*}
paulson@13163
   765
lemmas Vfrom_doubleton_D = Transset_Vfrom [THEN Transset_doubleton_D, standard]
paulson@13163
   766
paulson@13220
   767
(** Using only the weaker theorem would prove <a,b> \<in> Vfrom(X,i)
paulson@13220
   768
      implies a, b \<in> Vfrom(X,i), which is useless for induction.
paulson@13220
   769
    Using only the stronger theorem would prove <a,b> \<in> Vfrom(X,succ(succ(i)))
paulson@13220
   770
      implies a, b \<in> Vfrom(X,i), leaving the succ(i) case untreated.
paulson@13163
   771
    The combination gives a reduction by precisely one level, which is
paulson@13163
   772
      most convenient for proofs.
paulson@13163
   773
**)
paulson@13163
   774
paulson@13163
   775
lemma Pair_in_Vfrom_D:
paulson@13220
   776
    "[| <a,b> \<in> Vfrom(X,succ(i));  Transset(X) |]
paulson@13220
   777
     ==> a \<in> Vfrom(X,i)  &  b \<in> Vfrom(X,i)"
paulson@13163
   778
apply (unfold Pair_def)
paulson@13163
   779
apply (blast dest!: doubleton_in_Vfrom_D Vfrom_doubleton_D)
paulson@13163
   780
done
paulson@13163
   781
paulson@13163
   782
lemma product_Int_Vfrom_subset:
paulson@13163
   783
     "Transset(X) ==>
paulson@13163
   784
      (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))"
paulson@13163
   785
by (blast dest!: Pair_in_Vfrom_D)
paulson@13163
   786
paulson@13163
   787
paulson@13163
   788
ML
paulson@13163
   789
{*
paulson@6053
   790
paulson@13163
   791
val Vfrom = thm "Vfrom";
paulson@13163
   792
val Vfrom_mono = thm "Vfrom_mono";
paulson@13163
   793
val Vfrom_rank_subset1 = thm "Vfrom_rank_subset1";
paulson@13163
   794
val Vfrom_rank_subset2 = thm "Vfrom_rank_subset2";
paulson@13163
   795
val Vfrom_rank_eq = thm "Vfrom_rank_eq";
paulson@13163
   796
val zero_in_Vfrom = thm "zero_in_Vfrom";
paulson@13163
   797
val i_subset_Vfrom = thm "i_subset_Vfrom";
paulson@13163
   798
val A_subset_Vfrom = thm "A_subset_Vfrom";
paulson@13163
   799
val subset_mem_Vfrom = thm "subset_mem_Vfrom";
paulson@13163
   800
val singleton_in_Vfrom = thm "singleton_in_Vfrom";
paulson@13163
   801
val doubleton_in_Vfrom = thm "doubleton_in_Vfrom";
paulson@13163
   802
val Pair_in_Vfrom = thm "Pair_in_Vfrom";
paulson@13163
   803
val succ_in_Vfrom = thm "succ_in_Vfrom";
paulson@13163
   804
val Vfrom_0 = thm "Vfrom_0";
paulson@13163
   805
val Vfrom_succ = thm "Vfrom_succ";
paulson@13163
   806
val Vfrom_Union = thm "Vfrom_Union";
paulson@13163
   807
val Limit_Vfrom_eq = thm "Limit_Vfrom_eq";
paulson@13163
   808
val zero_in_VLimit = thm "zero_in_VLimit";
paulson@13163
   809
val singleton_in_VLimit = thm "singleton_in_VLimit";
paulson@13163
   810
val Vfrom_UnI1 = thm "Vfrom_UnI1";
paulson@13163
   811
val Vfrom_UnI2 = thm "Vfrom_UnI2";
paulson@13163
   812
val doubleton_in_VLimit = thm "doubleton_in_VLimit";
paulson@13163
   813
val Pair_in_VLimit = thm "Pair_in_VLimit";
paulson@13163
   814
val product_VLimit = thm "product_VLimit";
paulson@13163
   815
val Sigma_subset_VLimit = thm "Sigma_subset_VLimit";
paulson@13163
   816
val nat_subset_VLimit = thm "nat_subset_VLimit";
paulson@13163
   817
val nat_into_VLimit = thm "nat_into_VLimit";
paulson@13163
   818
val zero_in_VLimit = thm "zero_in_VLimit";
paulson@13163
   819
val one_in_VLimit = thm "one_in_VLimit";
paulson@13163
   820
val Inl_in_VLimit = thm "Inl_in_VLimit";
paulson@13163
   821
val Inr_in_VLimit = thm "Inr_in_VLimit";
paulson@13163
   822
val sum_VLimit = thm "sum_VLimit";
paulson@13163
   823
val sum_subset_VLimit = thm "sum_subset_VLimit";
paulson@13163
   824
val Transset_Vfrom = thm "Transset_Vfrom";
paulson@13163
   825
val Transset_Vfrom_succ = thm "Transset_Vfrom_succ";
paulson@13163
   826
val Transset_Pair_subset = thm "Transset_Pair_subset";
paulson@13163
   827
val Union_in_Vfrom = thm "Union_in_Vfrom";
paulson@13163
   828
val Union_in_VLimit = thm "Union_in_VLimit";
paulson@13163
   829
val in_VLimit = thm "in_VLimit";
paulson@13163
   830
val prod_in_Vfrom = thm "prod_in_Vfrom";
paulson@13163
   831
val prod_in_VLimit = thm "prod_in_VLimit";
paulson@13163
   832
val sum_in_Vfrom = thm "sum_in_Vfrom";
paulson@13163
   833
val sum_in_VLimit = thm "sum_in_VLimit";
paulson@13163
   834
val fun_in_Vfrom = thm "fun_in_Vfrom";
paulson@13163
   835
val fun_in_VLimit = thm "fun_in_VLimit";
paulson@13163
   836
val Pow_in_Vfrom = thm "Pow_in_Vfrom";
paulson@13163
   837
val Pow_in_VLimit = thm "Pow_in_VLimit";
paulson@13163
   838
val Vset = thm "Vset";
paulson@13163
   839
val Vset_succ = thm "Vset_succ";
paulson@13163
   840
val Transset_Vset = thm "Transset_Vset";
paulson@13163
   841
val VsetD = thm "VsetD";
paulson@13163
   842
val VsetI = thm "VsetI";
paulson@13163
   843
val Vset_Ord_rank_iff = thm "Vset_Ord_rank_iff";
paulson@13163
   844
val Vset_rank_iff = thm "Vset_rank_iff";
paulson@13163
   845
val rank_Vset = thm "rank_Vset";
paulson@13163
   846
val arg_subset_Vset_rank = thm "arg_subset_Vset_rank";
paulson@13163
   847
val Int_Vset_subset = thm "Int_Vset_subset";
paulson@13163
   848
val rank_Inl = thm "rank_Inl";
paulson@13163
   849
val rank_Inr = thm "rank_Inr";
paulson@13163
   850
val Vrec = thm "Vrec";
paulson@13163
   851
val def_Vrec = thm "def_Vrec";
paulson@13163
   852
val Vrecursor = thm "Vrecursor";
paulson@13163
   853
val def_Vrecursor = thm "def_Vrecursor";
paulson@13163
   854
val univ_mono = thm "univ_mono";
paulson@13163
   855
val Transset_univ = thm "Transset_univ";
paulson@13163
   856
val univ_eq_UN = thm "univ_eq_UN";
paulson@13163
   857
val subset_univ_eq_Int = thm "subset_univ_eq_Int";
paulson@13163
   858
val univ_Int_Vfrom_subset = thm "univ_Int_Vfrom_subset";
paulson@13163
   859
val univ_Int_Vfrom_eq = thm "univ_Int_Vfrom_eq";
paulson@13163
   860
val zero_in_univ = thm "zero_in_univ";
paulson@13163
   861
val A_subset_univ = thm "A_subset_univ";
paulson@13163
   862
val A_into_univ = thm "A_into_univ";
paulson@13163
   863
val singleton_in_univ = thm "singleton_in_univ";
paulson@13163
   864
val doubleton_in_univ = thm "doubleton_in_univ";
paulson@13163
   865
val Pair_in_univ = thm "Pair_in_univ";
paulson@13163
   866
val Union_in_univ = thm "Union_in_univ";
paulson@13163
   867
val product_univ = thm "product_univ";
paulson@13163
   868
val nat_subset_univ = thm "nat_subset_univ";
paulson@13163
   869
val nat_into_univ = thm "nat_into_univ";
paulson@13163
   870
val one_in_univ = thm "one_in_univ";
paulson@13163
   871
val two_in_univ = thm "two_in_univ";
paulson@13163
   872
val bool_subset_univ = thm "bool_subset_univ";
paulson@13163
   873
val bool_into_univ = thm "bool_into_univ";
paulson@13163
   874
val Inl_in_univ = thm "Inl_in_univ";
paulson@13163
   875
val Inr_in_univ = thm "Inr_in_univ";
paulson@13163
   876
val sum_univ = thm "sum_univ";
paulson@13163
   877
val sum_subset_univ = thm "sum_subset_univ";
paulson@13163
   878
val Fin_VLimit = thm "Fin_VLimit";
paulson@13163
   879
val Fin_subset_VLimit = thm "Fin_subset_VLimit";
paulson@13163
   880
val Fin_univ = thm "Fin_univ";
paulson@13163
   881
val nat_fun_VLimit = thm "nat_fun_VLimit";
paulson@13163
   882
val nat_fun_subset_VLimit = thm "nat_fun_subset_VLimit";
paulson@13163
   883
val nat_fun_univ = thm "nat_fun_univ";
paulson@13163
   884
val FiniteFun_VLimit1 = thm "FiniteFun_VLimit1";
paulson@13163
   885
val FiniteFun_univ1 = thm "FiniteFun_univ1";
paulson@13163
   886
val FiniteFun_VLimit = thm "FiniteFun_VLimit";
paulson@13163
   887
val FiniteFun_univ = thm "FiniteFun_univ";
paulson@13163
   888
val FiniteFun_in_univ = thm "FiniteFun_in_univ";
paulson@13163
   889
val FiniteFun_in_univ' = thm "FiniteFun_in_univ'";
paulson@13163
   890
val doubleton_in_Vfrom_D = thm "doubleton_in_Vfrom_D";
paulson@13163
   891
val Vfrom_doubleton_D = thm "Vfrom_doubleton_D";
paulson@13163
   892
val Pair_in_Vfrom_D = thm "Pair_in_Vfrom_D";
paulson@13163
   893
val product_Int_Vfrom_subset = thm "product_Int_Vfrom_subset";
paulson@13163
   894
paulson@13163
   895
val rank_rls = thms "rank_rls";
paulson@13163
   896
val rank_ss = simpset() addsimps [VsetI] 
paulson@13163
   897
              addsimps rank_rls @ (rank_rls RLN (2, [lt_trans]));
paulson@13163
   898
paulson@13163
   899
*}
clasohm@0
   900
clasohm@0
   901
end