68 val fun_Limit_VfromE = |
68 val fun_Limit_VfromE = |
69 [apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS Limit_VfromE |
69 [apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS Limit_VfromE |
70 |> standard; |
70 |> standard; |
71 |
71 |
72 goal InfDatatype.thy |
72 goal InfDatatype.thy |
73 "!!K. [| f: I -> Vfrom(A,csucc(K)); |I| le K; InfCard(K) \ |
73 "!!K. [| f: W -> Vfrom(A,csucc(K)); |W| le K; InfCard(K) \ |
74 \ |] ==> EX j. f: I -> Vfrom(A,j) & j < csucc(K)"; |
74 \ |] ==> EX j. f: W -> Vfrom(A,j) & j < csucc(K)"; |
75 by (res_inst_tac [("x", "UN x:I. LEAST i. f`x : Vfrom(A,i)")] exI 1); |
75 by (res_inst_tac [("x", "UN w:W. LEAST i. f`w : Vfrom(A,i)")] exI 1); |
76 by (resolve_tac [conjI] 1); |
76 by (resolve_tac [conjI] 1); |
77 by (resolve_tac [ballI RSN (2,cardinal_UN_Ord_lt_csucc)] 2); |
77 by (resolve_tac [le_UN_Ord_lt_csucc] 2); |
78 by (eresolve_tac [fun_Limit_VfromE] 3 THEN REPEAT_SOME assume_tac); |
78 by (rtac ballI 4 THEN |
|
79 eresolve_tac [fun_Limit_VfromE] 4 THEN REPEAT_SOME assume_tac); |
79 by (fast_tac (ZF_cs addEs [Least_le RS lt_trans1, ltE]) 2); |
80 by (fast_tac (ZF_cs addEs [Least_le RS lt_trans1, ltE]) 2); |
80 by (resolve_tac [Pi_type] 1); |
81 by (resolve_tac [Pi_type] 1); |
81 by (rename_tac "k" 2); |
82 by (rename_tac "w" 2); |
82 by (eresolve_tac [fun_Limit_VfromE] 2 THEN REPEAT_SOME assume_tac); |
83 by (eresolve_tac [fun_Limit_VfromE] 2 THEN REPEAT_SOME assume_tac); |
83 by (subgoal_tac "f`k : Vfrom(A, LEAST i. f`k : Vfrom(A,i))" 1); |
84 by (subgoal_tac "f`w : Vfrom(A, LEAST i. f`w : Vfrom(A,i))" 1); |
84 by (fast_tac (ZF_cs addEs [LeastI, ltE]) 2); |
85 by (fast_tac (ZF_cs addEs [LeastI, ltE]) 2); |
85 by (eresolve_tac [[subset_refl, UN_upper] MRS Vfrom_mono RS subsetD] 1); |
86 by (eresolve_tac [[subset_refl, UN_upper] MRS Vfrom_mono RS subsetD] 1); |
86 by (assume_tac 1); |
87 by (assume_tac 1); |
87 val fun_Vcsucc_lemma = result(); |
88 val fun_Vcsucc_lemma = result(); |
88 |
89 |
89 goal InfDatatype.thy |
90 goal InfDatatype.thy |
90 "!!K. [| f: K -> Vfrom(A,csucc(K)); InfCard(K) \ |
91 "!!K. [| W <= Vfrom(A,csucc(K)); |W| le K; InfCard(K) \ |
91 \ |] ==> EX j. f: K -> Vfrom(A,j) & j < csucc(K)"; |
92 \ |] ==> EX j. W <= Vfrom(A,j) & j < csucc(K)"; |
92 by (res_inst_tac [("x", "UN k:K. LEAST i. f`k : Vfrom(A,i)")] exI 1); |
93 by (asm_full_simp_tac (ZF_ss addsimps [subset_iff_id, fun_Vcsucc_lemma]) 1); |
93 by (resolve_tac [conjI] 1); |
94 val subset_Vcsucc = result(); |
94 by (resolve_tac [ballI RSN (2,cardinal_UN_Ord_lt_csucc)] 2); |
|
95 by (eresolve_tac [fun_Limit_VfromE] 3 THEN REPEAT_SOME assume_tac); |
|
96 by (fast_tac (ZF_cs addEs [Least_le RS lt_trans1, ltE]) 2); |
|
97 by (resolve_tac [Pi_type] 1); |
|
98 by (rename_tac "k" 2); |
|
99 by (eresolve_tac [fun_Limit_VfromE] 2 THEN REPEAT_SOME assume_tac); |
|
100 by (subgoal_tac "f`k : Vfrom(A, LEAST i. f`k : Vfrom(A,i))" 1); |
|
101 by (fast_tac (ZF_cs addEs [LeastI, ltE]) 2); |
|
102 by (eresolve_tac [[subset_refl, UN_upper] MRS Vfrom_mono RS subsetD] 1); |
|
103 by (assume_tac 1); |
|
104 val fun_Vcsucc_lemma = result(); |
|
105 |
95 |
|
96 (*Version for arbitrary index sets*) |
106 goal InfDatatype.thy |
97 goal InfDatatype.thy |
107 "!!K. InfCard(K) ==> K -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))"; |
98 "!!K. [| |W| le K; W <= Vfrom(A,csucc(K)); InfCard(K) |] ==> \ |
108 by (safe_tac (ZF_cs addSDs [fun_Vcsucc_lemma])); |
99 \ W -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))"; |
|
100 by (safe_tac (ZF_cs addSDs [fun_Vcsucc_lemma, subset_Vcsucc])); |
109 by (resolve_tac [Vfrom RS ssubst] 1); |
101 by (resolve_tac [Vfrom RS ssubst] 1); |
110 by (eresolve_tac [PiE] 1); |
102 by (eresolve_tac [PiE] 1); |
111 (*This level includes the function, and is below csucc(K)*) |
103 (*This level includes the function, and is below csucc(K)*) |
112 by (res_inst_tac [("a1", "succ(succ(K Un j))")] (UN_I RS UnI2) 1); |
104 by (res_inst_tac [("a1", "succ(succ(j Un ja))")] (UN_I RS UnI2) 1); |
113 by (eresolve_tac [subset_trans RS PowI] 2); |
105 by (eresolve_tac [subset_trans RS PowI] 2); |
114 by (safe_tac (ZF_cs addSIs [Pair_in_Vfrom])); |
106 by (fast_tac (ZF_cs addIs [Pair_in_Vfrom, Vfrom_UnI1, Vfrom_UnI2]) 2); |
115 by (fast_tac (ZF_cs addIs [i_subset_Vfrom RS subsetD]) 2); |
107 |
116 by (eresolve_tac [[subset_refl, Un_upper2] MRS Vfrom_mono RS subsetD] 2); |
|
117 by (REPEAT (ares_tac [ltD, InfCard_csucc, InfCard_is_Limit, |
108 by (REPEAT (ares_tac [ltD, InfCard_csucc, InfCard_is_Limit, |
118 Limit_has_succ, Un_least_lt] 1)); |
109 Limit_has_succ, Un_least_lt] 1)); |
119 by (eresolve_tac [InfCard_is_Card RS Card_is_Ord RS lt_csucc] 1); |
|
120 by (assume_tac 1); |
|
121 val fun_Vcsucc = result(); |
110 val fun_Vcsucc = result(); |
|
111 |
|
112 goal InfDatatype.thy |
|
113 "!!K. [| f: W -> Vfrom(A, csucc(K)); |W| le K; InfCard(K); \ |
|
114 \ W <= Vfrom(A,csucc(K)) \ |
|
115 \ |] ==> f: Vfrom(A,csucc(K))"; |
|
116 by (REPEAT (ares_tac [fun_Vcsucc RS subsetD] 1)); |
|
117 val fun_in_Vcsucc = result(); |
|
118 |
|
119 goal InfDatatype.thy |
|
120 "!!K. [| W <= Vfrom(A,csucc(K)); B <= Vfrom(A,csucc(K)); \ |
|
121 \ |W| le K; InfCard(K) \ |
|
122 \ |] ==> W -> B <= Vfrom(A, csucc(K))"; |
|
123 by (REPEAT (ares_tac [[Pi_mono, fun_Vcsucc] MRS subset_trans] 1)); |
|
124 val fun_subset_Vcsucc = result(); |
|
125 |
|
126 goal InfDatatype.thy |
|
127 "!!f. [| f: W -> B; W <= Vfrom(A,csucc(K)); B <= Vfrom(A,csucc(K)); \ |
|
128 \ |W| le K; InfCard(K) \ |
|
129 \ |] ==> f: Vfrom(A,csucc(K))"; |
|
130 by (DEPTH_SOLVE (ares_tac [fun_subset_Vcsucc RS subsetD] 1)); |
|
131 val fun_into_Vcsucc = result(); |
|
132 |
|
133 (*Version where K itself is the index set*) |
|
134 goal InfDatatype.thy |
|
135 "!!K. InfCard(K) ==> K -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))"; |
|
136 by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1); |
|
137 by (REPEAT (ares_tac [fun_Vcsucc, Ord_cardinal_le, |
|
138 i_subset_Vfrom, |
|
139 lt_csucc RS leI RS le_imp_subset RS subset_trans] 1)); |
|
140 val Card_fun_Vcsucc = result(); |
122 |
141 |
123 goal InfDatatype.thy |
142 goal InfDatatype.thy |
124 "!!K. [| f: K -> Vfrom(A, csucc(K)); InfCard(K) \ |
143 "!!K. [| f: K -> Vfrom(A, csucc(K)); InfCard(K) \ |
125 \ |] ==> f: Vfrom(A,csucc(K))"; |
144 \ |] ==> f: Vfrom(A,csucc(K))"; |
126 by (REPEAT (ares_tac [fun_Vcsucc RS subsetD] 1)); |
145 by (REPEAT (ares_tac [Card_fun_Vcsucc RS subsetD] 1)); |
127 val fun_in_Vcsucc = result(); |
146 val Card_fun_in_Vcsucc = result(); |
128 |
147 |
129 val fun_subset_Vcsucc = |
148 val Card_fun_subset_Vcsucc = |
130 [Pi_mono, fun_Vcsucc] MRS subset_trans |> standard; |
149 [Pi_mono, Card_fun_Vcsucc] MRS subset_trans |> standard; |
131 |
150 |
132 goal InfDatatype.thy |
151 goal InfDatatype.thy |
133 "!!f. [| f: K -> B; B <= Vfrom(A,csucc(K)); InfCard(K) \ |
152 "!!f. [| f: K -> B; B <= Vfrom(A,csucc(K)); InfCard(K) \ |
134 \ |] ==> f: Vfrom(A,csucc(K))"; |
153 \ |] ==> f: Vfrom(A,csucc(K))"; |
135 by (REPEAT (ares_tac [fun_subset_Vcsucc RS subsetD] 1)); |
154 by (REPEAT (ares_tac [Card_fun_subset_Vcsucc RS subsetD] 1)); |
136 val fun_into_Vcsucc = result(); |
155 val Card_fun_into_Vcsucc = result(); |
137 |
|
138 val Limit_csucc = InfCard_csucc RS InfCard_is_Limit |> standard; |
|
139 |
156 |
140 val Pair_in_Vcsucc = Limit_csucc RSN (3, Pair_in_VLimit) |> standard; |
157 val Pair_in_Vcsucc = Limit_csucc RSN (3, Pair_in_VLimit) |> standard; |
141 val Inl_in_Vcsucc = Limit_csucc RSN (2, Inl_in_VLimit) |> standard; |
158 val Inl_in_Vcsucc = Limit_csucc RSN (2, Inl_in_VLimit) |> standard; |
142 val Inr_in_Vcsucc = Limit_csucc RSN (2, Inr_in_VLimit) |> standard; |
159 val Inr_in_Vcsucc = Limit_csucc RSN (2, Inr_in_VLimit) |> standard; |
143 val zero_in_Vcsucc = Limit_csucc RS zero_in_VLimit |> standard; |
160 val zero_in_Vcsucc = Limit_csucc RS zero_in_VLimit |> standard; |
144 val nat_into_Vcsucc = Limit_csucc RSN (2, nat_into_VLimit) |> standard; |
161 val nat_into_Vcsucc = Limit_csucc RSN (2, nat_into_VLimit) |> standard; |
145 |
162 |
146 (*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *) |
163 (*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *) |
147 val inf_datatype_intrs = |
164 val inf_datatype_intrs = |
148 [fun_in_Vcsucc, InfCard_nat, Pair_in_Vcsucc, |
165 [Card_fun_in_Vcsucc, fun_in_Vcsucc, InfCard_nat, Pair_in_Vcsucc, |
149 Inl_in_Vcsucc, Inr_in_Vcsucc, |
166 Inl_in_Vcsucc, Inr_in_Vcsucc, |
150 zero_in_Vcsucc, A_into_Vfrom, nat_into_Vcsucc] @ datatype_intrs; |
167 zero_in_Vcsucc, A_into_Vfrom, nat_into_Vcsucc] @ datatype_intrs; |
151 |
168 |