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