src/ZF/Univ.thy
 changeset 13356 c9cfe1638bf2 parent 13288 9a870391ff66 child 13534 ca6debb89d77
equal 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 `
`     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)"`