(* Title: ZF/univ.thy ID: $Id: Univ.thy,v 1.32 2005/06/17 14:15:09 haftmann Exp $ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge Standard notation for Vset(i) is V(i), but users might want V for a variable NOTE: univ(A) could be a translation; would simplify many proofs! But Ind_Syntax.univ refers to the constant "Univ.univ" *) header{*The Cumulative Hierarchy and a Small Universe for Recursive Types*} theory Univ imports Epsilon Cardinal begin constdefs Vfrom :: "[i,i]=>i" "Vfrom(A,i) == transrec(i, %x f. A Un (\<Union>y∈x. Pow(f`y)))" syntax Vset :: "i=>i" translations "Vset(x)" == "Vfrom(0,x)" constdefs Vrec :: "[i, [i,i]=>i] =>i" "Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)). H(z, lam w:Vset(x). g`rank(w)`w)) ` a" Vrecursor :: "[[i,i]=>i, i] =>i" "Vrecursor(H,a) == transrec(rank(a), %x g. lam z: Vset(succ(x)). H(lam w:Vset(x). g`rank(w)`w, z)) ` a" univ :: "i=>i" "univ(A) == Vfrom(A,nat)" subsection{*Immediate Consequences of the Definition of @{term "Vfrom(A,i)"}*} text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*} lemma Vfrom: "Vfrom(A,i) = A Un (\<Union>j∈i. Pow(Vfrom(A,j)))" by (subst Vfrom_def [THEN def_transrec], simp) subsubsection{* Monotonicity *} lemma Vfrom_mono [rule_format]: "A<=B ==> ∀j. i<=j --> Vfrom(A,i) <= Vfrom(B,j)" apply (rule_tac a=i in eps_induct) apply (rule impI [THEN allI]) apply (subst Vfrom [of A]) apply (subst Vfrom [of B]) apply (erule Un_mono) apply (erule UN_mono, blast) done lemma VfromI: "[| a ∈ Vfrom(A,j); j<i |] ==> a ∈ Vfrom(A,i)" by (blast dest: Vfrom_mono [OF subset_refl le_imp_subset [OF leI]]) subsubsection{* A fundamental equality: Vfrom does not require ordinals! *} lemma Vfrom_rank_subset1: "Vfrom(A,x) <= Vfrom(A,rank(x))" proof (induct x rule: eps_induct) fix x assume "∀y∈x. Vfrom(A,y) ⊆ Vfrom(A,rank(y))" thus "Vfrom(A, x) ⊆ Vfrom(A, rank(x))" by (simp add: Vfrom [of _ x] Vfrom [of _ "rank(x)"], blast intro!: rank_lt [THEN ltD]) qed lemma Vfrom_rank_subset2: "Vfrom(A,rank(x)) <= Vfrom(A,x)" apply (rule_tac a=x in eps_induct) apply (subst Vfrom) apply (subst Vfrom, rule subset_refl [THEN Un_mono]) apply (rule UN_least) txt{*expand @{text "rank(x1) = (\<Union>y∈x1. succ(rank(y)))"} in assumptions*} apply (erule rank [THEN equalityD1, THEN subsetD, THEN UN_E]) apply (rule subset_trans) apply (erule_tac [2] UN_upper) apply (rule subset_refl [THEN Vfrom_mono, THEN subset_trans, THEN Pow_mono]) apply (erule ltI [THEN le_imp_subset]) apply (rule Ord_rank [THEN Ord_succ]) apply (erule bspec, assumption) done lemma Vfrom_rank_eq: "Vfrom(A,rank(x)) = Vfrom(A,x)" apply (rule equalityI) apply (rule Vfrom_rank_subset2) apply (rule Vfrom_rank_subset1) done subsection{* Basic Closure Properties *} lemma zero_in_Vfrom: "y:x ==> 0 ∈ Vfrom(A,x)" by (subst Vfrom, blast) lemma i_subset_Vfrom: "i <= Vfrom(A,i)" apply (rule_tac a=i in eps_induct) apply (subst Vfrom, blast) done lemma A_subset_Vfrom: "A <= Vfrom(A,i)" apply (subst Vfrom) apply (rule Un_upper1) done lemmas A_into_Vfrom = A_subset_Vfrom [THEN subsetD] lemma subset_mem_Vfrom: "a <= Vfrom(A,i) ==> a ∈ Vfrom(A,succ(i))" by (subst Vfrom, blast) subsubsection{* Finite sets and ordered pairs *} lemma singleton_in_Vfrom: "a ∈ Vfrom(A,i) ==> {a} ∈ Vfrom(A,succ(i))" by (rule subset_mem_Vfrom, safe) lemma doubleton_in_Vfrom: "[| a ∈ Vfrom(A,i); b ∈ Vfrom(A,i) |] ==> {a,b} ∈ Vfrom(A,succ(i))" by (rule subset_mem_Vfrom, safe) lemma Pair_in_Vfrom: "[| a ∈ Vfrom(A,i); b ∈ Vfrom(A,i) |] ==> <a,b> ∈ Vfrom(A,succ(succ(i)))" apply (unfold Pair_def) apply (blast intro: doubleton_in_Vfrom) done lemma succ_in_Vfrom: "a <= Vfrom(A,i) ==> succ(a) ∈ Vfrom(A,succ(succ(i)))" apply (intro subset_mem_Vfrom succ_subsetI, assumption) apply (erule subset_trans) apply (rule Vfrom_mono [OF subset_refl subset_succI]) done subsection{* 0, Successor and Limit Equations for @{term Vfrom} *} lemma Vfrom_0: "Vfrom(A,0) = A" by (subst Vfrom, blast) lemma Vfrom_succ_lemma: "Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))" apply (rule Vfrom [THEN trans]) apply (rule equalityI [THEN subst_context, OF _ succI1 [THEN RepFunI, THEN Union_upper]]) apply (rule UN_least) apply (rule subset_refl [THEN Vfrom_mono, THEN Pow_mono]) apply (erule ltI [THEN le_imp_subset]) apply (erule Ord_succ) done lemma Vfrom_succ: "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))" apply (rule_tac x1 = "succ (i)" in Vfrom_rank_eq [THEN subst]) apply (rule_tac x1 = i in Vfrom_rank_eq [THEN subst]) apply (subst rank_succ) apply (rule Ord_rank [THEN Vfrom_succ_lemma]) done (*The premise distinguishes this from Vfrom(A,0); allowing X=0 forces the conclusion to be Vfrom(A,Union(X)) = A Un (\<Union>y∈X. Vfrom(A,y)) *) lemma Vfrom_Union: "y:X ==> Vfrom(A,Union(X)) = (\<Union>y∈X. Vfrom(A,y))" apply (subst Vfrom) apply (rule equalityI) txt{*first inclusion*} apply (rule Un_least) apply (rule A_subset_Vfrom [THEN subset_trans]) apply (rule UN_upper, assumption) apply (rule UN_least) apply (erule UnionE) apply (rule subset_trans) apply (erule_tac [2] UN_upper, subst Vfrom, erule subset_trans [OF UN_upper Un_upper2]) txt{*opposite inclusion*} apply (rule UN_least) apply (subst Vfrom, blast) done subsection{* @{term Vfrom} applied to Limit Ordinals *} (*NB. limit ordinals are non-empty: Vfrom(A,0) = A = A Un (\<Union>y∈0. Vfrom(A,y)) *) lemma Limit_Vfrom_eq: "Limit(i) ==> Vfrom(A,i) = (\<Union>y∈i. Vfrom(A,y))" apply (rule Limit_has_0 [THEN ltD, THEN Vfrom_Union, THEN subst], assumption) apply (simp add: Limit_Union_eq) done lemma Limit_VfromE: "[| a ∈ Vfrom(A,i); ~R ==> Limit(i); !!x. [| x<i; a ∈ Vfrom(A,x) |] ==> R |] ==> R" apply (rule classical) apply (rule Limit_Vfrom_eq [THEN equalityD1, THEN subsetD, THEN UN_E]) prefer 2 apply assumption apply blast apply (blast intro: ltI Limit_is_Ord) done lemma singleton_in_VLimit: "[| a ∈ Vfrom(A,i); Limit(i) |] ==> {a} ∈ Vfrom(A,i)" apply (erule Limit_VfromE, assumption) apply (erule singleton_in_Vfrom [THEN VfromI]) apply (blast intro: Limit_has_succ) done lemmas Vfrom_UnI1 = Un_upper1 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD], standard] lemmas Vfrom_UnI2 = Un_upper2 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD], standard] text{*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*} lemma doubleton_in_VLimit: "[| a ∈ Vfrom(A,i); b ∈ Vfrom(A,i); Limit(i) |] ==> {a,b} ∈ Vfrom(A,i)" apply (erule Limit_VfromE, assumption) apply (erule Limit_VfromE, assumption) apply (blast intro: VfromI [OF doubleton_in_Vfrom] Vfrom_UnI1 Vfrom_UnI2 Limit_has_succ Un_least_lt) done lemma Pair_in_VLimit: "[| a ∈ Vfrom(A,i); b ∈ Vfrom(A,i); Limit(i) |] ==> <a,b> ∈ Vfrom(A,i)" txt{*Infer that a, b occur at ordinals x,xa < i.*} apply (erule Limit_VfromE, assumption) apply (erule Limit_VfromE, assumption) txt{*Infer that succ(succ(x Un xa)) < i *} apply (blast intro: VfromI [OF Pair_in_Vfrom] Vfrom_UnI1 Vfrom_UnI2 Limit_has_succ Un_least_lt) done lemma product_VLimit: "Limit(i) ==> Vfrom(A,i) * Vfrom(A,i) <= Vfrom(A,i)" by (blast intro: Pair_in_VLimit) lemmas Sigma_subset_VLimit = subset_trans [OF Sigma_mono product_VLimit] lemmas nat_subset_VLimit = subset_trans [OF nat_le_Limit [THEN le_imp_subset] i_subset_Vfrom] lemma nat_into_VLimit: "[| n: nat; Limit(i) |] ==> n ∈ Vfrom(A,i)" by (blast intro: nat_subset_VLimit [THEN subsetD]) subsubsection{* Closure under Disjoint Union *} lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom, standard] lemma one_in_VLimit: "Limit(i) ==> 1 ∈ Vfrom(A,i)" by (blast intro: nat_into_VLimit) lemma Inl_in_VLimit: "[| a ∈ Vfrom(A,i); Limit(i) |] ==> Inl(a) ∈ Vfrom(A,i)" apply (unfold Inl_def) apply (blast intro: zero_in_VLimit Pair_in_VLimit) done lemma Inr_in_VLimit: "[| b ∈ Vfrom(A,i); Limit(i) |] ==> Inr(b) ∈ Vfrom(A,i)" apply (unfold Inr_def) apply (blast intro: one_in_VLimit Pair_in_VLimit) done lemma sum_VLimit: "Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)" by (blast intro!: Inl_in_VLimit Inr_in_VLimit) lemmas sum_subset_VLimit = subset_trans [OF sum_mono sum_VLimit] subsection{* Properties assuming @{term "Transset(A)"} *} lemma Transset_Vfrom: "Transset(A) ==> Transset(Vfrom(A,i))" apply (rule_tac a=i in eps_induct) apply (subst Vfrom) apply (blast intro!: Transset_Union_family Transset_Un Transset_Pow) done lemma Transset_Vfrom_succ: "Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))" apply (rule Vfrom_succ [THEN trans]) apply (rule equalityI [OF _ Un_upper2]) apply (rule Un_least [OF _ subset_refl]) apply (rule A_subset_Vfrom [THEN subset_trans]) apply (erule Transset_Vfrom [THEN Transset_iff_Pow [THEN iffD1]]) done lemma Transset_Pair_subset: "[| <a,b> <= C; Transset(C) |] ==> a: C & b: C" by (unfold Pair_def Transset_def, blast) lemma Transset_Pair_subset_VLimit: "[| <a,b> <= Vfrom(A,i); Transset(A); Limit(i) |] ==> <a,b> ∈ Vfrom(A,i)" apply (erule Transset_Pair_subset [THEN conjE]) apply (erule Transset_Vfrom) apply (blast intro: Pair_in_VLimit) done lemma Union_in_Vfrom: "[| X ∈ Vfrom(A,j); Transset(A) |] ==> Union(X) ∈ Vfrom(A, succ(j))" apply (drule Transset_Vfrom) apply (rule subset_mem_Vfrom) apply (unfold Transset_def, blast) done lemma Union_in_VLimit: "[| X ∈ Vfrom(A,i); Limit(i); Transset(A) |] ==> Union(X) ∈ Vfrom(A,i)" apply (rule Limit_VfromE, assumption+) apply (blast intro: Limit_has_succ VfromI Union_in_Vfrom) done (*** Closure under product/sum applied to elements -- thus Vfrom(A,i) is a model of simple type theory provided A is a transitive set and i is a limit ordinal ***) text{*General theorem for membership in Vfrom(A,i) when i is a limit ordinal*} lemma in_VLimit: "[| a ∈ Vfrom(A,i); b ∈ Vfrom(A,i); Limit(i); !!x y j. [| j<i; 1:j; x ∈ Vfrom(A,j); y ∈ Vfrom(A,j) |] ==> EX k. h(x,y) ∈ Vfrom(A,k) & k<i |] ==> h(a,b) ∈ Vfrom(A,i)" txt{*Infer that a, b occur at ordinals x,xa < i.*} apply (erule Limit_VfromE, assumption) apply (erule Limit_VfromE, assumption, atomize) apply (drule_tac x=a in spec) apply (drule_tac x=b in spec) apply (drule_tac x="x Un xa Un 2" in spec) apply (simp add: Un_least_lt_iff lt_Ord Vfrom_UnI1 Vfrom_UnI2) apply (blast intro: Limit_has_0 Limit_has_succ VfromI) done subsubsection{* Products *} lemma prod_in_Vfrom: "[| a ∈ Vfrom(A,j); b ∈ Vfrom(A,j); Transset(A) |] ==> a*b ∈ Vfrom(A, succ(succ(succ(j))))" apply (drule Transset_Vfrom) apply (rule subset_mem_Vfrom) apply (unfold Transset_def) apply (blast intro: Pair_in_Vfrom) done lemma prod_in_VLimit: "[| a ∈ Vfrom(A,i); b ∈ Vfrom(A,i); Limit(i); Transset(A) |] ==> a*b ∈ Vfrom(A,i)" apply (erule in_VLimit, assumption+) apply (blast intro: prod_in_Vfrom Limit_has_succ) done subsubsection{* Disjoint Sums, or Quine Ordered Pairs *} lemma sum_in_Vfrom: "[| a ∈ Vfrom(A,j); b ∈ Vfrom(A,j); Transset(A); 1:j |] ==> a+b ∈ Vfrom(A, succ(succ(succ(j))))" apply (unfold sum_def) apply (drule Transset_Vfrom) apply (rule subset_mem_Vfrom) apply (unfold Transset_def) apply (blast intro: zero_in_Vfrom Pair_in_Vfrom i_subset_Vfrom [THEN subsetD]) done lemma sum_in_VLimit: "[| a ∈ Vfrom(A,i); b ∈ Vfrom(A,i); Limit(i); Transset(A) |] ==> a+b ∈ Vfrom(A,i)" apply (erule in_VLimit, assumption+) apply (blast intro: sum_in_Vfrom Limit_has_succ) done subsubsection{* Function Space! *} lemma fun_in_Vfrom: "[| a ∈ Vfrom(A,j); b ∈ Vfrom(A,j); Transset(A) |] ==> a->b ∈ Vfrom(A, succ(succ(succ(succ(j)))))" apply (unfold Pi_def) apply (drule Transset_Vfrom) apply (rule subset_mem_Vfrom) apply (rule Collect_subset [THEN subset_trans]) apply (subst Vfrom) apply (rule subset_trans [THEN subset_trans]) apply (rule_tac [3] Un_upper2) apply (rule_tac [2] succI1 [THEN UN_upper]) apply (rule Pow_mono) apply (unfold Transset_def) apply (blast intro: Pair_in_Vfrom) done lemma fun_in_VLimit: "[| a ∈ Vfrom(A,i); b ∈ Vfrom(A,i); Limit(i); Transset(A) |] ==> a->b ∈ Vfrom(A,i)" apply (erule in_VLimit, assumption+) apply (blast intro: fun_in_Vfrom Limit_has_succ) done lemma Pow_in_Vfrom: "[| a ∈ Vfrom(A,j); Transset(A) |] ==> Pow(a) ∈ Vfrom(A, succ(succ(j)))" apply (drule Transset_Vfrom) apply (rule subset_mem_Vfrom) apply (unfold Transset_def) apply (subst Vfrom, blast) done lemma Pow_in_VLimit: "[| a ∈ Vfrom(A,i); Limit(i); Transset(A) |] ==> Pow(a) ∈ Vfrom(A,i)" by (blast elim: Limit_VfromE intro: Limit_has_succ Pow_in_Vfrom VfromI) subsection{* The Set @{term "Vset(i)"} *} lemma Vset: "Vset(i) = (\<Union>j∈i. Pow(Vset(j)))" by (subst Vfrom, blast) lemmas Vset_succ = Transset_0 [THEN Transset_Vfrom_succ, standard] lemmas Transset_Vset = Transset_0 [THEN Transset_Vfrom, standard] subsubsection{* Characterisation of the elements of @{term "Vset(i)"} *} lemma VsetD [rule_format]: "Ord(i) ==> ∀b. b ∈ Vset(i) --> rank(b) < i" apply (erule trans_induct) apply (subst Vset, safe) apply (subst rank) apply (blast intro: ltI UN_succ_least_lt) done lemma VsetI_lemma [rule_format]: "Ord(i) ==> ∀b. rank(b) ∈ i --> b ∈ Vset(i)" apply (erule trans_induct) apply (rule allI) apply (subst Vset) apply (blast intro!: rank_lt [THEN ltD]) done lemma VsetI: "rank(x)<i ==> x ∈ Vset(i)" by (blast intro: VsetI_lemma elim: ltE) text{*Merely a lemma for the next result*} lemma Vset_Ord_rank_iff: "Ord(i) ==> b ∈ Vset(i) <-> rank(b) < i" by (blast intro: VsetD VsetI) lemma Vset_rank_iff [simp]: "b ∈ Vset(a) <-> rank(b) < rank(a)" apply (rule Vfrom_rank_eq [THEN subst]) apply (rule Ord_rank [THEN Vset_Ord_rank_iff]) done text{*This is rank(rank(a)) = rank(a) *} declare Ord_rank [THEN rank_of_Ord, simp] lemma rank_Vset: "Ord(i) ==> rank(Vset(i)) = i" apply (subst rank) apply (rule equalityI, safe) apply (blast intro: VsetD [THEN ltD]) apply (blast intro: VsetD [THEN ltD] Ord_trans) apply (blast intro: i_subset_Vfrom [THEN subsetD] Ord_in_Ord [THEN rank_of_Ord, THEN ssubst]) done lemma Finite_Vset: "i ∈ nat ==> Finite(Vset(i))"; apply (erule nat_induct) apply (simp add: Vfrom_0) apply (simp add: Vset_succ) done subsubsection{* Reasoning about Sets in Terms of Their Elements' Ranks *} lemma arg_subset_Vset_rank: "a <= Vset(rank(a))" apply (rule subsetI) apply (erule rank_lt [THEN VsetI]) done lemma Int_Vset_subset: "[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b" apply (rule subset_trans) apply (rule Int_greatest [OF subset_refl arg_subset_Vset_rank]) apply (blast intro: Ord_rank) done subsubsection{* Set Up an Environment for Simplification *} lemma rank_Inl: "rank(a) < rank(Inl(a))" apply (unfold Inl_def) apply (rule rank_pair2) done lemma rank_Inr: "rank(a) < rank(Inr(a))" apply (unfold Inr_def) apply (rule rank_pair2) done lemmas rank_rls = rank_Inl rank_Inr rank_pair1 rank_pair2 subsubsection{* Recursion over Vset Levels! *} text{*NOT SUITABLE FOR REWRITING: recursive!*} lemma Vrec: "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))" apply (unfold Vrec_def) apply (subst transrec, simp) apply (rule refl [THEN lam_cong, THEN subst_context], simp add: lt_def) done text{*This form avoids giant explosions in proofs. NOTE USE OF == *} lemma def_Vrec: "[| !!x. h(x)==Vrec(x,H) |] ==> h(a) = H(a, lam x: Vset(rank(a)). h(x))" apply simp apply (rule Vrec) done text{*NOT SUITABLE FOR REWRITING: recursive!*} lemma Vrecursor: "Vrecursor(H,a) = H(lam x:Vset(rank(a)). Vrecursor(H,x), a)" apply (unfold Vrecursor_def) apply (subst transrec, simp) apply (rule refl [THEN lam_cong, THEN subst_context], simp add: lt_def) done text{*This form avoids giant explosions in proofs. NOTE USE OF == *} lemma def_Vrecursor: "h == Vrecursor(H) ==> h(a) = H(lam x: Vset(rank(a)). h(x), a)" apply simp apply (rule Vrecursor) done subsection{* The Datatype Universe: @{term "univ(A)"} *} lemma univ_mono: "A<=B ==> univ(A) <= univ(B)" apply (unfold univ_def) apply (erule Vfrom_mono) apply (rule subset_refl) done lemma Transset_univ: "Transset(A) ==> Transset(univ(A))" apply (unfold univ_def) apply (erule Transset_Vfrom) done subsubsection{* The Set @{term"univ(A)"} as a Limit *} lemma univ_eq_UN: "univ(A) = (\<Union>i∈nat. Vfrom(A,i))" apply (unfold univ_def) apply (rule Limit_nat [THEN Limit_Vfrom_eq]) done lemma subset_univ_eq_Int: "c <= univ(A) ==> c = (\<Union>i∈nat. c Int Vfrom(A,i))" apply (rule subset_UN_iff_eq [THEN iffD1]) apply (erule univ_eq_UN [THEN subst]) done lemma univ_Int_Vfrom_subset: "[| a <= univ(X); !!i. i:nat ==> a Int Vfrom(X,i) <= b |] ==> a <= b" apply (subst subset_univ_eq_Int, assumption) apply (rule UN_least, simp) done lemma univ_Int_Vfrom_eq: "[| a <= univ(X); b <= univ(X); !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i) |] ==> a = b" apply (rule equalityI) apply (rule univ_Int_Vfrom_subset, assumption) apply (blast elim: equalityCE) apply (rule univ_Int_Vfrom_subset, assumption) apply (blast elim: equalityCE) done subsection{* Closure Properties for @{term "univ(A)"}*} lemma zero_in_univ: "0 ∈ univ(A)" apply (unfold univ_def) apply (rule nat_0I [THEN zero_in_Vfrom]) done lemma zero_subset_univ: "{0} <= univ(A)" by (blast intro: zero_in_univ) lemma A_subset_univ: "A <= univ(A)" apply (unfold univ_def) apply (rule A_subset_Vfrom) done lemmas A_into_univ = A_subset_univ [THEN subsetD, standard] subsubsection{* Closure under Unordered and Ordered Pairs *} lemma singleton_in_univ: "a: univ(A) ==> {a} ∈ univ(A)" apply (unfold univ_def) apply (blast intro: singleton_in_VLimit Limit_nat) done lemma doubleton_in_univ: "[| a: univ(A); b: univ(A) |] ==> {a,b} ∈ univ(A)" apply (unfold univ_def) apply (blast intro: doubleton_in_VLimit Limit_nat) done lemma Pair_in_univ: "[| a: univ(A); b: univ(A) |] ==> <a,b> ∈ univ(A)" apply (unfold univ_def) apply (blast intro: Pair_in_VLimit Limit_nat) done lemma Union_in_univ: "[| X: univ(A); Transset(A) |] ==> Union(X) ∈ univ(A)" apply (unfold univ_def) apply (blast intro: Union_in_VLimit Limit_nat) done lemma product_univ: "univ(A)*univ(A) <= univ(A)" apply (unfold univ_def) apply (rule Limit_nat [THEN product_VLimit]) done subsubsection{* The Natural Numbers *} lemma nat_subset_univ: "nat <= univ(A)" apply (unfold univ_def) apply (rule i_subset_Vfrom) done text{* n:nat ==> n:univ(A) *} lemmas nat_into_univ = nat_subset_univ [THEN subsetD, standard] subsubsection{* Instances for 1 and 2 *} lemma one_in_univ: "1 ∈ univ(A)" apply (unfold univ_def) apply (rule Limit_nat [THEN one_in_VLimit]) done text{*unused!*} lemma two_in_univ: "2 ∈ univ(A)" by (blast intro: nat_into_univ) lemma bool_subset_univ: "bool <= univ(A)" apply (unfold bool_def) apply (blast intro!: zero_in_univ one_in_univ) done lemmas bool_into_univ = bool_subset_univ [THEN subsetD, standard] subsubsection{* Closure under Disjoint Union *} lemma Inl_in_univ: "a: univ(A) ==> Inl(a) ∈ univ(A)" apply (unfold univ_def) apply (erule Inl_in_VLimit [OF _ Limit_nat]) done lemma Inr_in_univ: "b: univ(A) ==> Inr(b) ∈ univ(A)" apply (unfold univ_def) apply (erule Inr_in_VLimit [OF _ Limit_nat]) done lemma sum_univ: "univ(C)+univ(C) <= univ(C)" apply (unfold univ_def) apply (rule Limit_nat [THEN sum_VLimit]) done lemmas sum_subset_univ = subset_trans [OF sum_mono sum_univ] lemma Sigma_subset_univ: "[|A ⊆ univ(D); !!x. x ∈ A ==> B(x) ⊆ univ(D)|] ==> Sigma(A,B) ⊆ univ(D)" apply (simp add: univ_def) apply (blast intro: Sigma_subset_VLimit del: subsetI) done (*Closure under binary union -- use Un_least Closure under Collect -- use Collect_subset [THEN subset_trans] Closure under RepFun -- use RepFun_subset *) subsection{* Finite Branching Closure Properties *} subsubsection{* Closure under Finite Powerset *} lemma Fin_Vfrom_lemma: "[| b: Fin(Vfrom(A,i)); Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i" apply (erule Fin_induct) apply (blast dest!: Limit_has_0, safe) apply (erule Limit_VfromE, assumption) apply (blast intro!: Un_least_lt intro: Vfrom_UnI1 Vfrom_UnI2) done lemma Fin_VLimit: "Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)" apply (rule subsetI) apply (drule Fin_Vfrom_lemma, safe) apply (rule Vfrom [THEN ssubst]) apply (blast dest!: ltD) done lemmas Fin_subset_VLimit = subset_trans [OF Fin_mono Fin_VLimit] lemma Fin_univ: "Fin(univ(A)) <= univ(A)" apply (unfold univ_def) apply (rule Limit_nat [THEN Fin_VLimit]) done subsubsection{* Closure under Finite Powers: Functions from a Natural Number *} lemma nat_fun_VLimit: "[| n: nat; Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)" apply (erule nat_fun_subset_Fin [THEN subset_trans]) apply (blast del: subsetI intro: subset_refl Fin_subset_VLimit Sigma_subset_VLimit nat_subset_VLimit) done lemmas nat_fun_subset_VLimit = subset_trans [OF Pi_mono nat_fun_VLimit] lemma nat_fun_univ: "n: nat ==> n -> univ(A) <= univ(A)" apply (unfold univ_def) apply (erule nat_fun_VLimit [OF _ Limit_nat]) done subsubsection{* Closure under Finite Function Space *} text{*General but seldom-used version; normally the domain is fixed*} lemma FiniteFun_VLimit1: "Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) <= Vfrom(A,i)" apply (rule FiniteFun.dom_subset [THEN subset_trans]) apply (blast del: subsetI intro: Fin_subset_VLimit Sigma_subset_VLimit subset_refl) done lemma FiniteFun_univ1: "univ(A) -||> univ(A) <= univ(A)" apply (unfold univ_def) apply (rule Limit_nat [THEN FiniteFun_VLimit1]) done text{*Version for a fixed domain*} lemma FiniteFun_VLimit: "[| W <= Vfrom(A,i); Limit(i) |] ==> W -||> Vfrom(A,i) <= Vfrom(A,i)" apply (rule subset_trans) apply (erule FiniteFun_mono [OF _ subset_refl]) apply (erule FiniteFun_VLimit1) done lemma FiniteFun_univ: "W <= univ(A) ==> W -||> univ(A) <= univ(A)" apply (unfold univ_def) apply (erule FiniteFun_VLimit [OF _ Limit_nat]) done lemma FiniteFun_in_univ: "[| f: W -||> univ(A); W <= univ(A) |] ==> f ∈ univ(A)" by (erule FiniteFun_univ [THEN subsetD], assumption) text{*Remove <= from the rule above*} lemmas FiniteFun_in_univ' = FiniteFun_in_univ [OF _ subsetI] subsection{** For QUniv. Properties of Vfrom analogous to the "take-lemma" **} text{* Intersecting a*b with Vfrom... *} text{*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*} lemma doubleton_in_Vfrom_D: "[| {a,b} ∈ Vfrom(X,succ(i)); Transset(X) |] ==> a ∈ Vfrom(X,i) & b ∈ Vfrom(X,i)" by (drule Transset_Vfrom_succ [THEN equalityD1, THEN subsetD, THEN PowD], assumption, fast) text{*This weaker version says a, b exist at the same level*} lemmas Vfrom_doubleton_D = Transset_Vfrom [THEN Transset_doubleton_D, standard] (** Using only the weaker theorem would prove <a,b> ∈ Vfrom(X,i) implies a, b ∈ Vfrom(X,i), which is useless for induction. Using only the stronger theorem would prove <a,b> ∈ Vfrom(X,succ(succ(i))) implies a, b ∈ Vfrom(X,i), leaving the succ(i) case untreated. The combination gives a reduction by precisely one level, which is most convenient for proofs. **) lemma Pair_in_Vfrom_D: "[| <a,b> ∈ Vfrom(X,succ(i)); Transset(X) |] ==> a ∈ Vfrom(X,i) & b ∈ Vfrom(X,i)" apply (unfold Pair_def) apply (blast dest!: doubleton_in_Vfrom_D Vfrom_doubleton_D) done lemma product_Int_Vfrom_subset: "Transset(X) ==> (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))" by (blast dest!: Pair_in_Vfrom_D) ML {* val Vfrom = thm "Vfrom"; val Vfrom_mono = thm "Vfrom_mono"; val Vfrom_rank_subset1 = thm "Vfrom_rank_subset1"; val Vfrom_rank_subset2 = thm "Vfrom_rank_subset2"; val Vfrom_rank_eq = thm "Vfrom_rank_eq"; val zero_in_Vfrom = thm "zero_in_Vfrom"; val i_subset_Vfrom = thm "i_subset_Vfrom"; val A_subset_Vfrom = thm "A_subset_Vfrom"; val subset_mem_Vfrom = thm "subset_mem_Vfrom"; val singleton_in_Vfrom = thm "singleton_in_Vfrom"; val doubleton_in_Vfrom = thm "doubleton_in_Vfrom"; val Pair_in_Vfrom = thm "Pair_in_Vfrom"; val succ_in_Vfrom = thm "succ_in_Vfrom"; val Vfrom_0 = thm "Vfrom_0"; val Vfrom_succ = thm "Vfrom_succ"; val Vfrom_Union = thm "Vfrom_Union"; val Limit_Vfrom_eq = thm "Limit_Vfrom_eq"; val zero_in_VLimit = thm "zero_in_VLimit"; val singleton_in_VLimit = thm "singleton_in_VLimit"; val Vfrom_UnI1 = thm "Vfrom_UnI1"; val Vfrom_UnI2 = thm "Vfrom_UnI2"; val doubleton_in_VLimit = thm "doubleton_in_VLimit"; val Pair_in_VLimit = thm "Pair_in_VLimit"; val product_VLimit = thm "product_VLimit"; val Sigma_subset_VLimit = thm "Sigma_subset_VLimit"; val nat_subset_VLimit = thm "nat_subset_VLimit"; val nat_into_VLimit = thm "nat_into_VLimit"; val zero_in_VLimit = thm "zero_in_VLimit"; val one_in_VLimit = thm "one_in_VLimit"; val Inl_in_VLimit = thm "Inl_in_VLimit"; val Inr_in_VLimit = thm "Inr_in_VLimit"; val sum_VLimit = thm "sum_VLimit"; val sum_subset_VLimit = thm "sum_subset_VLimit"; val Transset_Vfrom = thm "Transset_Vfrom"; val Transset_Vfrom_succ = thm "Transset_Vfrom_succ"; val Transset_Pair_subset = thm "Transset_Pair_subset"; val Union_in_Vfrom = thm "Union_in_Vfrom"; val Union_in_VLimit = thm "Union_in_VLimit"; val in_VLimit = thm "in_VLimit"; val prod_in_Vfrom = thm "prod_in_Vfrom"; val prod_in_VLimit = thm "prod_in_VLimit"; val sum_in_Vfrom = thm "sum_in_Vfrom"; val sum_in_VLimit = thm "sum_in_VLimit"; val fun_in_Vfrom = thm "fun_in_Vfrom"; val fun_in_VLimit = thm "fun_in_VLimit"; val Pow_in_Vfrom = thm "Pow_in_Vfrom"; val Pow_in_VLimit = thm "Pow_in_VLimit"; val Vset = thm "Vset"; val Vset_succ = thm "Vset_succ"; val Transset_Vset = thm "Transset_Vset"; val VsetD = thm "VsetD"; val VsetI = thm "VsetI"; val Vset_Ord_rank_iff = thm "Vset_Ord_rank_iff"; val Vset_rank_iff = thm "Vset_rank_iff"; val rank_Vset = thm "rank_Vset"; val arg_subset_Vset_rank = thm "arg_subset_Vset_rank"; val Int_Vset_subset = thm "Int_Vset_subset"; val rank_Inl = thm "rank_Inl"; val rank_Inr = thm "rank_Inr"; val Vrec = thm "Vrec"; val def_Vrec = thm "def_Vrec"; val Vrecursor = thm "Vrecursor"; val def_Vrecursor = thm "def_Vrecursor"; val univ_mono = thm "univ_mono"; val Transset_univ = thm "Transset_univ"; val univ_eq_UN = thm "univ_eq_UN"; val subset_univ_eq_Int = thm "subset_univ_eq_Int"; val univ_Int_Vfrom_subset = thm "univ_Int_Vfrom_subset"; val univ_Int_Vfrom_eq = thm "univ_Int_Vfrom_eq"; val zero_in_univ = thm "zero_in_univ"; val A_subset_univ = thm "A_subset_univ"; val A_into_univ = thm "A_into_univ"; val singleton_in_univ = thm "singleton_in_univ"; val doubleton_in_univ = thm "doubleton_in_univ"; val Pair_in_univ = thm "Pair_in_univ"; val Union_in_univ = thm "Union_in_univ"; val product_univ = thm "product_univ"; val nat_subset_univ = thm "nat_subset_univ"; val nat_into_univ = thm "nat_into_univ"; val one_in_univ = thm "one_in_univ"; val two_in_univ = thm "two_in_univ"; val bool_subset_univ = thm "bool_subset_univ"; val bool_into_univ = thm "bool_into_univ"; val Inl_in_univ = thm "Inl_in_univ"; val Inr_in_univ = thm "Inr_in_univ"; val sum_univ = thm "sum_univ"; val sum_subset_univ = thm "sum_subset_univ"; val Fin_VLimit = thm "Fin_VLimit"; val Fin_subset_VLimit = thm "Fin_subset_VLimit"; val Fin_univ = thm "Fin_univ"; val nat_fun_VLimit = thm "nat_fun_VLimit"; val nat_fun_subset_VLimit = thm "nat_fun_subset_VLimit"; val nat_fun_univ = thm "nat_fun_univ"; val FiniteFun_VLimit1 = thm "FiniteFun_VLimit1"; val FiniteFun_univ1 = thm "FiniteFun_univ1"; val FiniteFun_VLimit = thm "FiniteFun_VLimit"; val FiniteFun_univ = thm "FiniteFun_univ"; val FiniteFun_in_univ = thm "FiniteFun_in_univ"; val FiniteFun_in_univ' = thm "FiniteFun_in_univ'"; val doubleton_in_Vfrom_D = thm "doubleton_in_Vfrom_D"; val Vfrom_doubleton_D = thm "Vfrom_doubleton_D"; val Pair_in_Vfrom_D = thm "Pair_in_Vfrom_D"; val product_Int_Vfrom_subset = thm "product_Int_Vfrom_subset"; val rank_rls = thms "rank_rls"; val rank_ss = simpset() addsimps [VsetI] addsimps rank_rls @ (rank_rls RLN (2, [lt_trans])); *} end
lemma Vfrom:
Vfrom(A, i) = A ∪ (\<Union>j∈i. Pow(Vfrom(A, j)))
lemma Vfrom_mono:
[| A ⊆ B; i ⊆ j |] ==> Vfrom(A, i) ⊆ Vfrom(B, j)
lemma VfromI:
[| a ∈ Vfrom(A, j); j < i |] ==> a ∈ Vfrom(A, i)
lemma Vfrom_rank_subset1:
Vfrom(A, x) ⊆ Vfrom(A, rank(x))
lemma Vfrom_rank_subset2:
Vfrom(A, rank(x)) ⊆ Vfrom(A, x)
lemma Vfrom_rank_eq:
Vfrom(A, rank(x)) = Vfrom(A, x)
lemma zero_in_Vfrom:
y ∈ x ==> 0 ∈ Vfrom(A, x)
lemma i_subset_Vfrom:
i ⊆ Vfrom(A, i)
lemma A_subset_Vfrom:
A ⊆ Vfrom(A, i)
lemmas A_into_Vfrom:
c ∈ A ==> c ∈ Vfrom(A, i1)
lemmas A_into_Vfrom:
c ∈ A ==> c ∈ Vfrom(A, i1)
lemma subset_mem_Vfrom:
a ⊆ Vfrom(A, i) ==> a ∈ Vfrom(A, succ(i))
lemma singleton_in_Vfrom:
a ∈ Vfrom(A, i) ==> {a} ∈ Vfrom(A, succ(i))
lemma doubleton_in_Vfrom:
[| a ∈ Vfrom(A, i); b ∈ Vfrom(A, i) |] ==> {a, b} ∈ Vfrom(A, succ(i))
lemma Pair_in_Vfrom:
[| a ∈ Vfrom(A, i); b ∈ Vfrom(A, i) |] ==> 〈a, b〉 ∈ Vfrom(A, succ(succ(i)))
lemma succ_in_Vfrom:
a ⊆ Vfrom(A, i) ==> succ(a) ∈ Vfrom(A, succ(succ(i)))
lemma Vfrom_0:
Vfrom(A, 0) = A
lemma Vfrom_succ_lemma:
Ord(i) ==> Vfrom(A, succ(i)) = A ∪ Pow(Vfrom(A, i))
lemma Vfrom_succ:
Vfrom(A, succ(i)) = A ∪ Pow(Vfrom(A, i))
lemma Vfrom_Union:
y ∈ X ==> Vfrom(A, \<Union>X) = (\<Union>y∈X. Vfrom(A, y))
lemma Limit_Vfrom_eq:
Limit(i) ==> Vfrom(A, i) = (\<Union>y∈i. Vfrom(A, y))
lemma Limit_VfromE:
[| a ∈ Vfrom(A, i); ¬ R ==> Limit(i); !!x. [| x < i; a ∈ Vfrom(A, x) |] ==> R |] ==> R
lemma singleton_in_VLimit:
[| a ∈ Vfrom(A, i); Limit(i) |] ==> {a} ∈ Vfrom(A, i)
lemmas Vfrom_UnI1:
c ∈ Vfrom(A, i) ==> c ∈ Vfrom(A, i ∪ B)
lemmas Vfrom_UnI1:
c ∈ Vfrom(A, i) ==> c ∈ Vfrom(A, i ∪ B)
lemmas Vfrom_UnI2:
c ∈ Vfrom(A, i) ==> c ∈ Vfrom(A, Aa ∪ i)
lemmas Vfrom_UnI2:
c ∈ Vfrom(A, i) ==> c ∈ Vfrom(A, Aa ∪ i)
lemma doubleton_in_VLimit:
[| a ∈ Vfrom(A, i); b ∈ Vfrom(A, i); Limit(i) |] ==> {a, b} ∈ Vfrom(A, i)
lemma Pair_in_VLimit:
[| a ∈ Vfrom(A, i); b ∈ Vfrom(A, i); Limit(i) |] ==> 〈a, b〉 ∈ Vfrom(A, i)
lemma product_VLimit:
Limit(i) ==> Vfrom(A, i) × Vfrom(A, i) ⊆ Vfrom(A, i)
lemmas Sigma_subset_VLimit:
[| A2 ⊆ Vfrom(A1, i1); !!x. x ∈ A2 ==> B2(x) ⊆ Vfrom(A1, i1); Limit(i1) |] ==> Sigma(A2, B2) ⊆ Vfrom(A1, i1)
lemmas Sigma_subset_VLimit:
[| A2 ⊆ Vfrom(A1, i1); !!x. x ∈ A2 ==> B2(x) ⊆ Vfrom(A1, i1); Limit(i1) |] ==> Sigma(A2, B2) ⊆ Vfrom(A1, i1)
lemmas nat_subset_VLimit:
Limit(B) ==> nat ⊆ Vfrom(A1, B)
lemmas nat_subset_VLimit:
Limit(B) ==> nat ⊆ Vfrom(A1, B)
lemma nat_into_VLimit:
[| n ∈ nat; Limit(i) |] ==> n ∈ Vfrom(A, i)
lemmas zero_in_VLimit:
Limit(x) ==> 0 ∈ Vfrom(A, x)
lemmas zero_in_VLimit:
Limit(x) ==> 0 ∈ Vfrom(A, x)
lemma one_in_VLimit:
Limit(i) ==> 1 ∈ Vfrom(A, i)
lemma Inl_in_VLimit:
[| a ∈ Vfrom(A, i); Limit(i) |] ==> Inl(a) ∈ Vfrom(A, i)
lemma Inr_in_VLimit:
[| b ∈ Vfrom(A, i); Limit(i) |] ==> Inr(b) ∈ Vfrom(A, i)
lemma sum_VLimit:
Limit(i) ==> Vfrom(C, i) + Vfrom(C, i) ⊆ Vfrom(C, i)
lemmas sum_subset_VLimit:
[| A2 ⊆ Vfrom(C1, i1); B2 ⊆ Vfrom(C1, i1); Limit(i1) |] ==> A2 + B2 ⊆ Vfrom(C1, i1)
lemmas sum_subset_VLimit:
[| A2 ⊆ Vfrom(C1, i1); B2 ⊆ Vfrom(C1, i1); Limit(i1) |] ==> A2 + B2 ⊆ Vfrom(C1, i1)
lemma Transset_Vfrom:
Transset(A) ==> Transset(Vfrom(A, i))
lemma Transset_Vfrom_succ:
Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A, i))
lemma Transset_Pair_subset:
[| 〈a, b〉 ⊆ C; Transset(C) |] ==> a ∈ C ∧ b ∈ C
lemma Transset_Pair_subset_VLimit:
[| 〈a, b〉 ⊆ Vfrom(A, i); Transset(A); Limit(i) |] ==> 〈a, b〉 ∈ Vfrom(A, i)
lemma Union_in_Vfrom:
[| X ∈ Vfrom(A, j); Transset(A) |] ==> \<Union>X ∈ Vfrom(A, succ(j))
lemma Union_in_VLimit:
[| X ∈ Vfrom(A, i); Limit(i); Transset(A) |] ==> \<Union>X ∈ Vfrom(A, i)
lemma in_VLimit:
[| a ∈ Vfrom(A, i); b ∈ Vfrom(A, i); Limit(i); !!x y j. [| j < i; 1 ∈ j; x ∈ Vfrom(A, j); y ∈ Vfrom(A, j) |] ==> ∃k. h(x, y) ∈ Vfrom(A, k) ∧ k < i |] ==> h(a, b) ∈ Vfrom(A, i)
lemma prod_in_Vfrom:
[| a ∈ Vfrom(A, j); b ∈ Vfrom(A, j); Transset(A) |] ==> a × b ∈ Vfrom(A, succ(succ(succ(j))))
lemma prod_in_VLimit:
[| a ∈ Vfrom(A, i); b ∈ Vfrom(A, i); Limit(i); Transset(A) |] ==> a × b ∈ Vfrom(A, i)
lemma sum_in_Vfrom:
[| a ∈ Vfrom(A, j); b ∈ Vfrom(A, j); Transset(A); 1 ∈ j |] ==> a + b ∈ Vfrom(A, succ(succ(succ(j))))
lemma sum_in_VLimit:
[| a ∈ Vfrom(A, i); b ∈ Vfrom(A, i); Limit(i); Transset(A) |] ==> a + b ∈ Vfrom(A, i)
lemma fun_in_Vfrom:
[| a ∈ Vfrom(A, j); b ∈ Vfrom(A, j); Transset(A) |] ==> a -> b ∈ Vfrom(A, succ(succ(succ(succ(j)))))
lemma fun_in_VLimit:
[| a ∈ Vfrom(A, i); b ∈ Vfrom(A, i); Limit(i); Transset(A) |] ==> a -> b ∈ Vfrom(A, i)
lemma Pow_in_Vfrom:
[| a ∈ Vfrom(A, j); Transset(A) |] ==> Pow(a) ∈ Vfrom(A, succ(succ(j)))
lemma Pow_in_VLimit:
[| a ∈ Vfrom(A, i); Limit(i); Transset(A) |] ==> Pow(a) ∈ Vfrom(A, i)
lemma Vset:
Vset(i) = (\<Union>j∈i. Pow(Vset(j)))
lemmas Vset_succ:
Vset(succ(i)) = Pow(Vset(i))
lemmas Vset_succ:
Vset(succ(i)) = Pow(Vset(i))
lemmas Transset_Vset:
Transset(Vset(i))
lemmas Transset_Vset:
Transset(Vset(i))
lemma VsetD:
[| Ord(i); b ∈ Vset(i) |] ==> rank(b) < i
lemma VsetI_lemma:
[| Ord(i); rank(b) ∈ i |] ==> b ∈ Vset(i)
lemma VsetI:
rank(x) < i ==> x ∈ Vset(i)
lemma Vset_Ord_rank_iff:
Ord(i) ==> b ∈ Vset(i) <-> rank(b) < i
lemma Vset_rank_iff:
b ∈ Vset(a) <-> rank(b) < rank(a)
lemma rank_Vset:
Ord(i) ==> rank(Vset(i)) = i
lemma Finite_Vset:
i ∈ nat ==> Finite(Vset(i))
lemma arg_subset_Vset_rank:
a ⊆ Vset(rank(a))
lemma Int_Vset_subset:
(!!i. Ord(i) ==> a ∩ Vset(i) ⊆ b) ==> a ⊆ b
lemma rank_Inl:
rank(a) < rank(Inl(a))
lemma rank_Inr:
rank(a) < rank(Inr(a))
lemmas rank_rls:
rank(a) < rank(Inl(a))
rank(a) < rank(Inr(a))
rank(a) < rank(〈a, b〉)
rank(b) < rank(〈a, b〉)
lemmas rank_rls:
rank(a) < rank(Inl(a))
rank(a) < rank(Inr(a))
rank(a) < rank(〈a, b〉)
rank(b) < rank(〈a, b〉)
lemma Vrec:
Vrec(a, H) = H(a, λx∈Vset(rank(a)). Vrec(x, H))
lemma def_Vrec:
(!!x. h(x) == Vrec(x, H)) ==> h(a) = H(a, λx∈Vset(rank(a)). h(x))
lemma Vrecursor:
Vrecursor(H, a) = H(λx∈Vset(rank(a)). Vrecursor(H, x), a)
lemma def_Vrecursor:
h == Vrecursor(H) ==> h(a) = H(λx∈Vset(rank(a)). h(x), a)
lemma univ_mono:
A ⊆ B ==> univ(A) ⊆ univ(B)
lemma Transset_univ:
Transset(A) ==> Transset(univ(A))
lemma univ_eq_UN:
univ(A) = (\<Union>i∈nat. Vfrom(A, i))
lemma subset_univ_eq_Int:
c ⊆ univ(A) ==> c = (\<Union>i∈nat. c ∩ Vfrom(A, i))
lemma univ_Int_Vfrom_subset:
[| a ⊆ univ(X); !!i. i ∈ nat ==> a ∩ Vfrom(X, i) ⊆ b |] ==> a ⊆ b
lemma univ_Int_Vfrom_eq:
[| a ⊆ univ(X); b ⊆ univ(X); !!i. i ∈ nat ==> a ∩ Vfrom(X, i) = b ∩ Vfrom(X, i) |] ==> a = b
lemma zero_in_univ:
0 ∈ univ(A)
lemma zero_subset_univ:
{0} ⊆ univ(A)
lemma A_subset_univ:
A ⊆ univ(A)
lemmas A_into_univ:
c ∈ A ==> c ∈ univ(A)
lemmas A_into_univ:
c ∈ A ==> c ∈ univ(A)
lemma singleton_in_univ:
a ∈ univ(A) ==> {a} ∈ univ(A)
lemma doubleton_in_univ:
[| a ∈ univ(A); b ∈ univ(A) |] ==> {a, b} ∈ univ(A)
lemma Pair_in_univ:
[| a ∈ univ(A); b ∈ univ(A) |] ==> 〈a, b〉 ∈ univ(A)
lemma Union_in_univ:
[| X ∈ univ(A); Transset(A) |] ==> \<Union>X ∈ univ(A)
lemma product_univ:
univ(A) × univ(A) ⊆ univ(A)
lemma nat_subset_univ:
nat ⊆ univ(A)
lemmas nat_into_univ:
c ∈ nat ==> c ∈ univ(A)
lemmas nat_into_univ:
c ∈ nat ==> c ∈ univ(A)
lemma one_in_univ:
1 ∈ univ(A)
lemma two_in_univ:
2 ∈ univ(A)
lemma bool_subset_univ:
bool ⊆ univ(A)
lemmas bool_into_univ:
c ∈ bool ==> c ∈ univ(A)
lemmas bool_into_univ:
c ∈ bool ==> c ∈ univ(A)
lemma Inl_in_univ:
a ∈ univ(A) ==> Inl(a) ∈ univ(A)
lemma Inr_in_univ:
b ∈ univ(A) ==> Inr(b) ∈ univ(A)
lemma sum_univ:
univ(C) + univ(C) ⊆ univ(C)
lemmas sum_subset_univ:
[| A2 ⊆ univ(C1); B2 ⊆ univ(C1) |] ==> A2 + B2 ⊆ univ(C1)
lemmas sum_subset_univ:
[| A2 ⊆ univ(C1); B2 ⊆ univ(C1) |] ==> A2 + B2 ⊆ univ(C1)
lemma Sigma_subset_univ:
[| A ⊆ univ(D); !!x. x ∈ A ==> B(x) ⊆ univ(D) |] ==> Sigma(A, B) ⊆ univ(D)
lemma Fin_Vfrom_lemma:
[| b ∈ Fin(Vfrom(A, i)); Limit(i) |] ==> ∃j. b ⊆ Vfrom(A, j) ∧ j < i
lemma Fin_VLimit:
Limit(i) ==> Fin(Vfrom(A, i)) ⊆ Vfrom(A, i)
lemmas Fin_subset_VLimit:
[| A2 ⊆ Vfrom(A1, i1); Limit(i1) |] ==> Fin(A2) ⊆ Vfrom(A1, i1)
lemmas Fin_subset_VLimit:
[| A2 ⊆ Vfrom(A1, i1); Limit(i1) |] ==> Fin(A2) ⊆ Vfrom(A1, i1)
lemma Fin_univ:
Fin(univ(A)) ⊆ univ(A)
lemma nat_fun_VLimit:
[| n ∈ nat; Limit(i) |] ==> n -> Vfrom(A, i) ⊆ Vfrom(A, i)
lemmas nat_fun_subset_VLimit:
[| B2 ⊆ Vfrom(A3, i4); n1 ∈ nat; Limit(i4) |] ==> n1 -> B2 ⊆ Vfrom(A3, i4)
lemmas nat_fun_subset_VLimit:
[| B2 ⊆ Vfrom(A3, i4); n1 ∈ nat; Limit(i4) |] ==> n1 -> B2 ⊆ Vfrom(A3, i4)
lemma nat_fun_univ:
n ∈ nat ==> n -> univ(A) ⊆ univ(A)
lemma FiniteFun_VLimit1:
Limit(i) ==> Vfrom(A, i) -||> Vfrom(A, i) ⊆ Vfrom(A, i)
lemma FiniteFun_univ1:
univ(A) -||> univ(A) ⊆ univ(A)
lemma FiniteFun_VLimit:
[| W ⊆ Vfrom(A, i); Limit(i) |] ==> W -||> Vfrom(A, i) ⊆ Vfrom(A, i)
lemma FiniteFun_univ:
W ⊆ univ(A) ==> W -||> univ(A) ⊆ univ(A)
lemma FiniteFun_in_univ:
[| f ∈ W -||> univ(A); W ⊆ univ(A) |] ==> f ∈ univ(A)
lemmas FiniteFun_in_univ':
[| f ∈ W -||> univ(A); !!x. x ∈ W ==> x ∈ univ(A) |] ==> f ∈ univ(A)
lemmas FiniteFun_in_univ':
[| f ∈ W -||> univ(A); !!x. x ∈ W ==> x ∈ univ(A) |] ==> f ∈ univ(A)
lemma doubleton_in_Vfrom_D:
[| {a, b} ∈ Vfrom(X, succ(i)); Transset(X) |] ==> a ∈ Vfrom(X, i) ∧ b ∈ Vfrom(X, i)
lemmas Vfrom_doubleton_D:
[| Transset(A); {a, b} ∈ Vfrom(A, i) |] ==> a ∈ Vfrom(A, i) ∧ b ∈ Vfrom(A, i)
lemmas Vfrom_doubleton_D:
[| Transset(A); {a, b} ∈ Vfrom(A, i) |] ==> a ∈ Vfrom(A, i) ∧ b ∈ Vfrom(A, i)
lemma Pair_in_Vfrom_D:
[| 〈a, b〉 ∈ Vfrom(X, succ(i)); Transset(X) |] ==> a ∈ Vfrom(X, i) ∧ b ∈ Vfrom(X, i)
lemma product_Int_Vfrom_subset:
Transset(X) ==> a × b ∩ Vfrom(X, succ(i)) ⊆ (a ∩ Vfrom(X, i)) × (b ∩ Vfrom(X, i))