62 lemma univ_subset_quniv: "univ(A) <= quniv(A)" |
62 lemma univ_subset_quniv: "univ(A) <= quniv(A)" |
63 apply (rule arg_subset_eclose [THEN univ_mono, THEN subset_trans]) |
63 apply (rule arg_subset_eclose [THEN univ_mono, THEN subset_trans]) |
64 apply (rule univ_eclose_subset_quniv) |
64 apply (rule univ_eclose_subset_quniv) |
65 done |
65 done |
66 |
66 |
67 lemmas univ_into_quniv = univ_subset_quniv [THEN subsetD, standard] |
67 lemmas univ_into_quniv = univ_subset_quniv [THEN subsetD] |
68 |
68 |
69 lemma Pow_univ_subset_quniv: "Pow(univ(A)) <= quniv(A)" |
69 lemma Pow_univ_subset_quniv: "Pow(univ(A)) <= quniv(A)" |
70 apply (unfold quniv_def) |
70 apply (unfold quniv_def) |
71 apply (rule arg_subset_eclose [THEN univ_mono, THEN Pow_mono]) |
71 apply (rule arg_subset_eclose [THEN univ_mono, THEN Pow_mono]) |
72 done |
72 done |
73 |
73 |
74 lemmas univ_subset_into_quniv = |
74 lemmas univ_subset_into_quniv = |
75 PowI [THEN Pow_univ_subset_quniv [THEN subsetD], standard] |
75 PowI [THEN Pow_univ_subset_quniv [THEN subsetD]] |
76 |
76 |
77 lemmas zero_in_quniv = zero_in_univ [THEN univ_into_quniv, standard] |
77 lemmas zero_in_quniv = zero_in_univ [THEN univ_into_quniv] |
78 lemmas one_in_quniv = one_in_univ [THEN univ_into_quniv, standard] |
78 lemmas one_in_quniv = one_in_univ [THEN univ_into_quniv] |
79 lemmas two_in_quniv = two_in_univ [THEN univ_into_quniv, standard] |
79 lemmas two_in_quniv = two_in_univ [THEN univ_into_quniv] |
80 |
80 |
81 lemmas A_subset_quniv = subset_trans [OF A_subset_univ univ_subset_quniv] |
81 lemmas A_subset_quniv = subset_trans [OF A_subset_univ univ_subset_quniv] |
82 |
82 |
83 lemmas A_into_quniv = A_subset_quniv [THEN subsetD, standard] |
83 lemmas A_into_quniv = A_subset_quniv [THEN subsetD] |
84 |
84 |
85 (*** univ(A) closure for Quine-inspired pairs and injections ***) |
85 (*** univ(A) closure for Quine-inspired pairs and injections ***) |
86 |
86 |
87 (*Quine ordered pairs*) |
87 (*Quine ordered pairs*) |
88 lemma QPair_subset_univ: |
88 lemma QPair_subset_univ: |
95 apply (unfold QInl_def) |
95 apply (unfold QInl_def) |
96 apply (erule empty_subsetI [THEN QPair_subset_univ]) |
96 apply (erule empty_subsetI [THEN QPair_subset_univ]) |
97 done |
97 done |
98 |
98 |
99 lemmas naturals_subset_nat = |
99 lemmas naturals_subset_nat = |
100 Ord_nat [THEN Ord_is_Transset, unfolded Transset_def, THEN bspec, standard] |
100 Ord_nat [THEN Ord_is_Transset, unfolded Transset_def, THEN bspec] |
101 |
101 |
102 lemmas naturals_subset_univ = |
102 lemmas naturals_subset_univ = |
103 subset_trans [OF naturals_subset_nat nat_subset_univ] |
103 subset_trans [OF naturals_subset_nat nat_subset_univ] |
104 |
104 |
105 lemma QInr_subset_univ: "a <= univ(A) ==> QInr(a) <= univ(A)" |
105 lemma QInr_subset_univ: "a <= univ(A) ==> QInr(a) <= univ(A)" |
126 apply (rule Transset_includes_summands [THEN conjE]) |
126 apply (rule Transset_includes_summands [THEN conjE]) |
127 apply (rule Transset_eclose [THEN Transset_univ]) |
127 apply (rule Transset_eclose [THEN Transset_univ]) |
128 apply (erule PowD, blast) |
128 apply (erule PowD, blast) |
129 done |
129 done |
130 |
130 |
131 lemmas quniv_QPair_E = quniv_QPair_D [THEN conjE, standard] |
131 lemmas quniv_QPair_E = quniv_QPair_D [THEN conjE] |
132 |
132 |
133 lemma quniv_QPair_iff: "<a;b> : quniv(A) <-> a: quniv(A) & b: quniv(A)" |
133 lemma quniv_QPair_iff: "<a;b> : quniv(A) <-> a: quniv(A) & b: quniv(A)" |
134 by (blast intro: QPair_in_quniv dest: quniv_QPair_D) |
134 by (blast intro: QPair_in_quniv dest: quniv_QPair_D) |
135 |
135 |
136 |
136 |
151 subsection{*The Natural Numbers*} |
151 subsection{*The Natural Numbers*} |
152 |
152 |
153 lemmas nat_subset_quniv = subset_trans [OF nat_subset_univ univ_subset_quniv] |
153 lemmas nat_subset_quniv = subset_trans [OF nat_subset_univ univ_subset_quniv] |
154 |
154 |
155 (* n:nat ==> n:quniv(A) *) |
155 (* n:nat ==> n:quniv(A) *) |
156 lemmas nat_into_quniv = nat_subset_quniv [THEN subsetD, standard] |
156 lemmas nat_into_quniv = nat_subset_quniv [THEN subsetD] |
157 |
157 |
158 lemmas bool_subset_quniv = subset_trans [OF bool_subset_univ univ_subset_quniv] |
158 lemmas bool_subset_quniv = subset_trans [OF bool_subset_univ univ_subset_quniv] |
159 |
159 |
160 lemmas bool_into_quniv = bool_subset_quniv [THEN subsetD, standard] |
160 lemmas bool_into_quniv = bool_subset_quniv [THEN subsetD] |
161 |
161 |
162 |
162 |
163 (*Intersecting <a;b> with Vfrom...*) |
163 (*Intersecting <a;b> with Vfrom...*) |
164 |
164 |
165 lemma QPair_Int_Vfrom_succ_subset: |
165 lemma QPair_Int_Vfrom_succ_subset: |