src/ZF/Univ.thy
changeset 13356 c9cfe1638bf2
parent 13288 9a870391ff66
child 13534 ca6debb89d77
equal deleted inserted replaced
13355:d19cdbd8b559 13356:c9cfe1638bf2
     1 (*  Title:      ZF/univ.thy
     1 (*  Title:      ZF/univ.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     4     Copyright   1992  University of Cambridge
     5 
     5 
     6 The cumulative hierarchy and a small universe for recursive types
       
     7 
       
     8 Standard notation for Vset(i) is V(i), but users might want V for a variable
     6 Standard notation for Vset(i) is V(i), but users might want V for a variable
     9 
     7 
    10 NOTE: univ(A) could be a translation; would simplify many proofs!
     8 NOTE: univ(A) could be a translation; would simplify many proofs!
    11   But Ind_Syntax.univ refers to the constant "Univ.univ"
     9   But Ind_Syntax.univ refers to the constant "Univ.univ"
    12 *)
    10 *)
       
    11 
       
    12 header{*The Cumulative Hierarchy and a Small Universe for Recursive Types*}
    13 
    13 
    14 theory Univ = Epsilon + Cardinal:
    14 theory Univ = Epsilon + Cardinal:
    15 
    15 
    16 constdefs
    16 constdefs
    17   Vfrom       :: "[i,i]=>i"
    17   Vfrom       :: "[i,i]=>i"
    32 				H(lam w:Vset(x). g`rank(w)`w, z)) ` a"
    32 				H(lam w:Vset(x). g`rank(w)`w, z)) ` a"
    33 
    33 
    34   univ        :: "i=>i"
    34   univ        :: "i=>i"
    35     "univ(A) == Vfrom(A,nat)"
    35     "univ(A) == Vfrom(A,nat)"
    36 
    36 
       
    37 
       
    38 subsection{*Immediate Consequences of the Definition of @{term "Vfrom(A,i)"}*}
    37 
    39 
    38 text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*}
    40 text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*}
    39 lemma Vfrom: "Vfrom(A,i) = A Un (\<Union>j\<in>i. Pow(Vfrom(A,j)))"
    41 lemma Vfrom: "Vfrom(A,i) = A Un (\<Union>j\<in>i. Pow(Vfrom(A,j)))"
    40 by (subst Vfrom_def [THEN def_transrec], simp)
    42 by (subst Vfrom_def [THEN def_transrec], simp)
    41 
    43 
    85 apply (rule Vfrom_rank_subset2)
    87 apply (rule Vfrom_rank_subset2)
    86 apply (rule Vfrom_rank_subset1)
    88 apply (rule Vfrom_rank_subset1)
    87 done
    89 done
    88 
    90 
    89 
    91 
    90 subsection{* Basic closure properties *}
    92 subsection{* Basic Closure Properties *}
    91 
    93 
    92 lemma zero_in_Vfrom: "y:x ==> 0 \<in> Vfrom(A,x)"
    94 lemma zero_in_Vfrom: "y:x ==> 0 \<in> Vfrom(A,x)"
    93 by (subst Vfrom, blast)
    95 by (subst Vfrom, blast)
    94 
    96 
    95 lemma i_subset_Vfrom: "i <= Vfrom(A,i)"
    97 lemma i_subset_Vfrom: "i <= Vfrom(A,i)"
   126 apply (intro subset_mem_Vfrom succ_subsetI, assumption)
   128 apply (intro subset_mem_Vfrom succ_subsetI, assumption)
   127 apply (erule subset_trans) 
   129 apply (erule subset_trans) 
   128 apply (rule Vfrom_mono [OF subset_refl subset_succI]) 
   130 apply (rule Vfrom_mono [OF subset_refl subset_succI]) 
   129 done
   131 done
   130 
   132 
   131 subsection{* 0, successor and limit equations fof Vfrom *}
   133 subsection{* 0, Successor and Limit Equations for @{term Vfrom} *}
   132 
   134 
   133 lemma Vfrom_0: "Vfrom(A,0) = A"
   135 lemma Vfrom_0: "Vfrom(A,0) = A"
   134 by (subst Vfrom, blast)
   136 by (subst Vfrom, blast)
   135 
   137 
   136 lemma Vfrom_succ_lemma: "Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"
   138 lemma Vfrom_succ_lemma: "Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"
   167 txt{*opposite inclusion*}
   169 txt{*opposite inclusion*}
   168 apply (rule UN_least)
   170 apply (rule UN_least)
   169 apply (subst Vfrom, blast)
   171 apply (subst Vfrom, blast)
   170 done
   172 done
   171 
   173 
   172 subsection{* Vfrom applied to Limit ordinals *}
   174 subsection{* @{term Vfrom} applied to Limit Ordinals *}
   173 
   175 
   174 (*NB. limit ordinals are non-empty:
   176 (*NB. limit ordinals are non-empty:
   175       Vfrom(A,0) = A = A Un (\<Union>y\<in>0. Vfrom(A,y)) *)
   177       Vfrom(A,0) = A = A Un (\<Union>y\<in>0. Vfrom(A,y)) *)
   176 lemma Limit_Vfrom_eq:
   178 lemma Limit_Vfrom_eq:
   177     "Limit(i) ==> Vfrom(A,i) = (\<Union>y\<in>i. Vfrom(A,y))"
   179     "Limit(i) ==> Vfrom(A,i) = (\<Union>y\<in>i. Vfrom(A,y))"
   233      subset_trans [OF nat_le_Limit [THEN le_imp_subset] i_subset_Vfrom]
   235      subset_trans [OF nat_le_Limit [THEN le_imp_subset] i_subset_Vfrom]
   234 
   236 
   235 lemma nat_into_VLimit: "[| n: nat;  Limit(i) |] ==> n \<in> Vfrom(A,i)"
   237 lemma nat_into_VLimit: "[| n: nat;  Limit(i) |] ==> n \<in> Vfrom(A,i)"
   236 by (blast intro: nat_subset_VLimit [THEN subsetD])
   238 by (blast intro: nat_subset_VLimit [THEN subsetD])
   237 
   239 
   238 subsubsection{* Closure under disjoint union *}
   240 subsubsection{* Closure under Disjoint Union *}
   239 
   241 
   240 lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom, standard]
   242 lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom, standard]
   241 
   243 
   242 lemma one_in_VLimit: "Limit(i) ==> 1 \<in> Vfrom(A,i)"
   244 lemma one_in_VLimit: "Limit(i) ==> 1 \<in> Vfrom(A,i)"
   243 by (blast intro: nat_into_VLimit)
   245 by (blast intro: nat_into_VLimit)
   259 
   261 
   260 lemmas sum_subset_VLimit = subset_trans [OF sum_mono sum_VLimit]
   262 lemmas sum_subset_VLimit = subset_trans [OF sum_mono sum_VLimit]
   261 
   263 
   262 
   264 
   263 
   265 
   264 subsection{* Properties assuming Transset(A) *}
   266 subsection{* Properties assuming @{term "Transset(A)"} *}
   265 
   267 
   266 lemma Transset_Vfrom: "Transset(A) ==> Transset(Vfrom(A,i))"
   268 lemma Transset_Vfrom: "Transset(A) ==> Transset(Vfrom(A,i))"
   267 apply (rule_tac a=i in eps_induct)
   269 apply (rule_tac a=i in eps_induct)
   268 apply (subst Vfrom)
   270 apply (subst Vfrom)
   269 apply (blast intro!: Transset_Union_family Transset_Un Transset_Pow)
   271 apply (blast intro!: Transset_Union_family Transset_Un Transset_Pow)
   322 apply (drule_tac x="x Un xa Un 2" in spec) 
   324 apply (drule_tac x="x Un xa Un 2" in spec) 
   323 apply (simp add: Un_least_lt_iff lt_Ord Vfrom_UnI1 Vfrom_UnI2) 
   325 apply (simp add: Un_least_lt_iff lt_Ord Vfrom_UnI1 Vfrom_UnI2) 
   324 apply (blast intro: Limit_has_0 Limit_has_succ VfromI)
   326 apply (blast intro: Limit_has_0 Limit_has_succ VfromI)
   325 done
   327 done
   326 
   328 
   327 subsubsection{* products *}
   329 subsubsection{* Products *}
   328 
   330 
   329 lemma prod_in_Vfrom:
   331 lemma prod_in_Vfrom:
   330     "[| a \<in> Vfrom(A,j);  b \<in> Vfrom(A,j);  Transset(A) |]
   332     "[| a \<in> Vfrom(A,j);  b \<in> Vfrom(A,j);  Transset(A) |]
   331      ==> a*b \<in> Vfrom(A, succ(succ(succ(j))))"
   333      ==> a*b \<in> Vfrom(A, succ(succ(succ(j))))"
   332 apply (drule Transset_Vfrom)
   334 apply (drule Transset_Vfrom)
   340    ==> a*b \<in> Vfrom(A,i)"
   342    ==> a*b \<in> Vfrom(A,i)"
   341 apply (erule in_VLimit, assumption+)
   343 apply (erule in_VLimit, assumption+)
   342 apply (blast intro: prod_in_Vfrom Limit_has_succ)
   344 apply (blast intro: prod_in_Vfrom Limit_has_succ)
   343 done
   345 done
   344 
   346 
   345 subsubsection{* Disjoint sums, aka Quine ordered pairs *}
   347 subsubsection{* Disjoint Sums, or Quine Ordered Pairs *}
   346 
   348 
   347 lemma sum_in_Vfrom:
   349 lemma sum_in_Vfrom:
   348     "[| a \<in> Vfrom(A,j);  b \<in> Vfrom(A,j);  Transset(A);  1:j |]
   350     "[| a \<in> Vfrom(A,j);  b \<in> Vfrom(A,j);  Transset(A);  1:j |]
   349      ==> a+b \<in> Vfrom(A, succ(succ(succ(j))))"
   351      ==> a+b \<in> Vfrom(A, succ(succ(succ(j))))"
   350 apply (unfold sum_def)
   352 apply (unfold sum_def)
   359    ==> a+b \<in> Vfrom(A,i)"
   361    ==> a+b \<in> Vfrom(A,i)"
   360 apply (erule in_VLimit, assumption+)
   362 apply (erule in_VLimit, assumption+)
   361 apply (blast intro: sum_in_Vfrom Limit_has_succ)
   363 apply (blast intro: sum_in_Vfrom Limit_has_succ)
   362 done
   364 done
   363 
   365 
   364 subsubsection{* function space! *}
   366 subsubsection{* Function Space! *}
   365 
   367 
   366 lemma fun_in_Vfrom:
   368 lemma fun_in_Vfrom:
   367     "[| a \<in> Vfrom(A,j);  b \<in> Vfrom(A,j);  Transset(A) |] ==>
   369     "[| a \<in> Vfrom(A,j);  b \<in> Vfrom(A,j);  Transset(A) |] ==>
   368           a->b \<in> Vfrom(A, succ(succ(succ(succ(j)))))"
   370           a->b \<in> Vfrom(A, succ(succ(succ(succ(j)))))"
   369 apply (unfold Pi_def)
   371 apply (unfold Pi_def)
   397 lemma Pow_in_VLimit:
   399 lemma Pow_in_VLimit:
   398      "[| a \<in> Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Pow(a) \<in> Vfrom(A,i)"
   400      "[| a \<in> Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Pow(a) \<in> Vfrom(A,i)"
   399 by (blast elim: Limit_VfromE intro: Limit_has_succ Pow_in_Vfrom VfromI)
   401 by (blast elim: Limit_VfromE intro: Limit_has_succ Pow_in_Vfrom VfromI)
   400 
   402 
   401 
   403 
   402 subsection{* The set Vset(i) *}
   404 subsection{* The Set @{term "Vset(i)"} *}
   403 
   405 
   404 lemma Vset: "Vset(i) = (\<Union>j\<in>i. Pow(Vset(j)))"
   406 lemma Vset: "Vset(i) = (\<Union>j\<in>i. Pow(Vset(j)))"
   405 by (subst Vfrom, blast)
   407 by (subst Vfrom, blast)
   406 
   408 
   407 lemmas Vset_succ = Transset_0 [THEN Transset_Vfrom_succ, standard]
   409 lemmas Vset_succ = Transset_0 [THEN Transset_Vfrom_succ, standard]
   408 lemmas Transset_Vset = Transset_0 [THEN Transset_Vfrom, standard]
   410 lemmas Transset_Vset = Transset_0 [THEN Transset_Vfrom, standard]
   409 
   411 
   410 subsubsection{* Characterisation of the elements of Vset(i) *}
   412 subsubsection{* Characterisation of the elements of @{term "Vset(i)"} *}
   411 
   413 
   412 lemma VsetD [rule_format]: "Ord(i) ==> \<forall>b. b \<in> Vset(i) --> rank(b) < i"
   414 lemma VsetD [rule_format]: "Ord(i) ==> \<forall>b. b \<in> Vset(i) --> rank(b) < i"
   413 apply (erule trans_induct)
   415 apply (erule trans_induct)
   414 apply (subst Vset, safe)
   416 apply (subst Vset, safe)
   415 apply (subst rank)
   417 apply (subst rank)
   452 apply (erule nat_induct)
   454 apply (erule nat_induct)
   453  apply (simp add: Vfrom_0) 
   455  apply (simp add: Vfrom_0) 
   454 apply (simp add: Vset_succ) 
   456 apply (simp add: Vset_succ) 
   455 done
   457 done
   456 
   458 
   457 subsubsection{* Reasoning about sets in terms of their elements' ranks *}
   459 subsubsection{* Reasoning about Sets in Terms of Their Elements' Ranks *}
   458 
   460 
   459 lemma arg_subset_Vset_rank: "a <= Vset(rank(a))"
   461 lemma arg_subset_Vset_rank: "a <= Vset(rank(a))"
   460 apply (rule subsetI)
   462 apply (rule subsetI)
   461 apply (erule rank_lt [THEN VsetI])
   463 apply (erule rank_lt [THEN VsetI])
   462 done
   464 done
   466 apply (rule subset_trans) 
   468 apply (rule subset_trans) 
   467 apply (rule Int_greatest [OF subset_refl arg_subset_Vset_rank])
   469 apply (rule Int_greatest [OF subset_refl arg_subset_Vset_rank])
   468 apply (blast intro: Ord_rank) 
   470 apply (blast intro: Ord_rank) 
   469 done
   471 done
   470 
   472 
   471 subsubsection{* Set up an environment for simplification *}
   473 subsubsection{* Set Up an Environment for Simplification *}
   472 
   474 
   473 lemma rank_Inl: "rank(a) < rank(Inl(a))"
   475 lemma rank_Inl: "rank(a) < rank(Inl(a))"
   474 apply (unfold Inl_def)
   476 apply (unfold Inl_def)
   475 apply (rule rank_pair2)
   477 apply (rule rank_pair2)
   476 done
   478 done
   480 apply (rule rank_pair2)
   482 apply (rule rank_pair2)
   481 done
   483 done
   482 
   484 
   483 lemmas rank_rls = rank_Inl rank_Inr rank_pair1 rank_pair2
   485 lemmas rank_rls = rank_Inl rank_Inr rank_pair1 rank_pair2
   484 
   486 
   485 subsubsection{* Recursion over Vset levels! *}
   487 subsubsection{* Recursion over Vset Levels! *}
   486 
   488 
   487 text{*NOT SUITABLE FOR REWRITING: recursive!*}
   489 text{*NOT SUITABLE FOR REWRITING: recursive!*}
   488 lemma Vrec: "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))"
   490 lemma Vrec: "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))"
   489 apply (unfold Vrec_def)
   491 apply (unfold Vrec_def)
   490 apply (subst transrec, simp)
   492 apply (subst transrec, simp)
   513 apply simp
   515 apply simp
   514 apply (rule Vrecursor)
   516 apply (rule Vrecursor)
   515 done
   517 done
   516 
   518 
   517 
   519 
   518 subsection{* univ(A) *}
   520 subsection{* The Datatype Universe: @{term "univ(A)"} *}
   519 
   521 
   520 lemma univ_mono: "A<=B ==> univ(A) <= univ(B)"
   522 lemma univ_mono: "A<=B ==> univ(A) <= univ(B)"
   521 apply (unfold univ_def)
   523 apply (unfold univ_def)
   522 apply (erule Vfrom_mono)
   524 apply (erule Vfrom_mono)
   523 apply (rule subset_refl)
   525 apply (rule subset_refl)
   526 lemma Transset_univ: "Transset(A) ==> Transset(univ(A))"
   528 lemma Transset_univ: "Transset(A) ==> Transset(univ(A))"
   527 apply (unfold univ_def)
   529 apply (unfold univ_def)
   528 apply (erule Transset_Vfrom)
   530 apply (erule Transset_Vfrom)
   529 done
   531 done
   530 
   532 
   531 subsubsection{* univ(A) as a limit *}
   533 subsubsection{* The Set @{term"univ(A)"} as a Limit *}
   532 
   534 
   533 lemma univ_eq_UN: "univ(A) = (\<Union>i\<in>nat. Vfrom(A,i))"
   535 lemma univ_eq_UN: "univ(A) = (\<Union>i\<in>nat. Vfrom(A,i))"
   534 apply (unfold univ_def)
   536 apply (unfold univ_def)
   535 apply (rule Limit_nat [THEN Limit_Vfrom_eq])
   537 apply (rule Limit_nat [THEN Limit_Vfrom_eq])
   536 done
   538 done
   557 apply (blast elim: equalityCE) 
   559 apply (blast elim: equalityCE) 
   558 apply (rule univ_Int_Vfrom_subset, assumption)
   560 apply (rule univ_Int_Vfrom_subset, assumption)
   559 apply (blast elim: equalityCE) 
   561 apply (blast elim: equalityCE) 
   560 done
   562 done
   561 
   563 
   562 subsubsection{* Closure properties *}
   564 subsection{* Closure Properties for @{term "univ(A)"}*}
   563 
   565 
   564 lemma zero_in_univ: "0 \<in> univ(A)"
   566 lemma zero_in_univ: "0 \<in> univ(A)"
   565 apply (unfold univ_def)
   567 apply (unfold univ_def)
   566 apply (rule nat_0I [THEN zero_in_Vfrom])
   568 apply (rule nat_0I [THEN zero_in_Vfrom])
   567 done
   569 done
   574 apply (rule A_subset_Vfrom)
   576 apply (rule A_subset_Vfrom)
   575 done
   577 done
   576 
   578 
   577 lemmas A_into_univ = A_subset_univ [THEN subsetD, standard]
   579 lemmas A_into_univ = A_subset_univ [THEN subsetD, standard]
   578 
   580 
   579 subsubsection{* Closure under unordered and ordered pairs *}
   581 subsubsection{* Closure under Unordered and Ordered Pairs *}
   580 
   582 
   581 lemma singleton_in_univ: "a: univ(A) ==> {a} \<in> univ(A)"
   583 lemma singleton_in_univ: "a: univ(A) ==> {a} \<in> univ(A)"
   582 apply (unfold univ_def)
   584 apply (unfold univ_def)
   583 apply (blast intro: singleton_in_VLimit Limit_nat)
   585 apply (blast intro: singleton_in_VLimit Limit_nat)
   584 done
   586 done
   605 apply (unfold univ_def)
   607 apply (unfold univ_def)
   606 apply (rule Limit_nat [THEN product_VLimit])
   608 apply (rule Limit_nat [THEN product_VLimit])
   607 done
   609 done
   608 
   610 
   609 
   611 
   610 subsubsection{* The natural numbers *}
   612 subsubsection{* The Natural Numbers *}
   611 
   613 
   612 lemma nat_subset_univ: "nat <= univ(A)"
   614 lemma nat_subset_univ: "nat <= univ(A)"
   613 apply (unfold univ_def)
   615 apply (unfold univ_def)
   614 apply (rule i_subset_Vfrom)
   616 apply (rule i_subset_Vfrom)
   615 done
   617 done
   616 
   618 
   617 text{* n:nat ==> n:univ(A) *}
   619 text{* n:nat ==> n:univ(A) *}
   618 lemmas nat_into_univ = nat_subset_univ [THEN subsetD, standard]
   620 lemmas nat_into_univ = nat_subset_univ [THEN subsetD, standard]
   619 
   621 
   620 subsubsection{* instances for 1 and 2 *}
   622 subsubsection{* Instances for 1 and 2 *}
   621 
   623 
   622 lemma one_in_univ: "1 \<in> univ(A)"
   624 lemma one_in_univ: "1 \<in> univ(A)"
   623 apply (unfold univ_def)
   625 apply (unfold univ_def)
   624 apply (rule Limit_nat [THEN one_in_VLimit])
   626 apply (rule Limit_nat [THEN one_in_VLimit])
   625 done
   627 done
   634 done
   636 done
   635 
   637 
   636 lemmas bool_into_univ = bool_subset_univ [THEN subsetD, standard]
   638 lemmas bool_into_univ = bool_subset_univ [THEN subsetD, standard]
   637 
   639 
   638 
   640 
   639 subsubsection{* Closure under disjoint union *}
   641 subsubsection{* Closure under Disjoint Union *}
   640 
   642 
   641 lemma Inl_in_univ: "a: univ(A) ==> Inl(a) \<in> univ(A)"
   643 lemma Inl_in_univ: "a: univ(A) ==> Inl(a) \<in> univ(A)"
   642 apply (unfold univ_def)
   644 apply (unfold univ_def)
   643 apply (erule Inl_in_VLimit [OF _ Limit_nat])
   645 apply (erule Inl_in_VLimit [OF _ Limit_nat])
   644 done
   646 done
   667   Closure under RepFun -- use   RepFun_subset *)
   669   Closure under RepFun -- use   RepFun_subset *)
   668 
   670 
   669 
   671 
   670 subsection{* Finite Branching Closure Properties *}
   672 subsection{* Finite Branching Closure Properties *}
   671 
   673 
   672 subsubsection{* Closure under finite powerset *}
   674 subsubsection{* Closure under Finite Powerset *}
   673 
   675 
   674 lemma Fin_Vfrom_lemma:
   676 lemma Fin_Vfrom_lemma:
   675      "[| b: Fin(Vfrom(A,i));  Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i"
   677      "[| b: Fin(Vfrom(A,i));  Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i"
   676 apply (erule Fin_induct)
   678 apply (erule Fin_induct)
   677 apply (blast dest!: Limit_has_0, safe)
   679 apply (blast dest!: Limit_has_0, safe)
   691 lemma Fin_univ: "Fin(univ(A)) <= univ(A)"
   693 lemma Fin_univ: "Fin(univ(A)) <= univ(A)"
   692 apply (unfold univ_def)
   694 apply (unfold univ_def)
   693 apply (rule Limit_nat [THEN Fin_VLimit])
   695 apply (rule Limit_nat [THEN Fin_VLimit])
   694 done
   696 done
   695 
   697 
   696 subsubsection{* Closure under finite powers: functions from a natural number *}
   698 subsubsection{* Closure under Finite Powers: Functions from a Natural Number *}
   697 
   699 
   698 lemma nat_fun_VLimit:
   700 lemma nat_fun_VLimit:
   699      "[| n: nat;  Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)"
   701      "[| n: nat;  Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)"
   700 apply (erule nat_fun_subset_Fin [THEN subset_trans])
   702 apply (erule nat_fun_subset_Fin [THEN subset_trans])
   701 apply (blast del: subsetI
   703 apply (blast del: subsetI
   708 apply (unfold univ_def)
   710 apply (unfold univ_def)
   709 apply (erule nat_fun_VLimit [OF _ Limit_nat])
   711 apply (erule nat_fun_VLimit [OF _ Limit_nat])
   710 done
   712 done
   711 
   713 
   712 
   714 
   713 subsubsection{* Closure under finite function space *}
   715 subsubsection{* Closure under Finite Function Space *}
   714 
   716 
   715 text{*General but seldom-used version; normally the domain is fixed*}
   717 text{*General but seldom-used version; normally the domain is fixed*}
   716 lemma FiniteFun_VLimit1:
   718 lemma FiniteFun_VLimit1:
   717      "Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) <= Vfrom(A,i)"
   719      "Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) <= Vfrom(A,i)"
   718 apply (rule FiniteFun.dom_subset [THEN subset_trans])
   720 apply (rule FiniteFun.dom_subset [THEN subset_trans])
   747 lemmas FiniteFun_in_univ' = FiniteFun_in_univ [OF _ subsetI]
   749 lemmas FiniteFun_in_univ' = FiniteFun_in_univ [OF _ subsetI]
   748 
   750 
   749 
   751 
   750 subsection{** For QUniv.  Properties of Vfrom analogous to the "take-lemma" **}
   752 subsection{** For QUniv.  Properties of Vfrom analogous to the "take-lemma" **}
   751 
   753 
   752 subsection{* Intersecting a*b with Vfrom... *}
   754 text{* Intersecting a*b with Vfrom... *}
   753 
   755 
   754 text{*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*}
   756 text{*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*}
   755 lemma doubleton_in_Vfrom_D:
   757 lemma doubleton_in_Vfrom_D:
   756      "[| {a,b} \<in> Vfrom(X,succ(i));  Transset(X) |]
   758      "[| {a,b} \<in> Vfrom(X,succ(i));  Transset(X) |]
   757       ==> a \<in> Vfrom(X,i)  &  b \<in> Vfrom(X,i)"
   759       ==> a \<in> Vfrom(X,i)  &  b \<in> Vfrom(X,i)"