125 goal InfDatatype.thy |
125 goal InfDatatype.thy |
126 "!!K. [| |W| le K; InfCard(K); W <= Vfrom(A,csucc(K)) |] ==> \ |
126 "!!K. [| |W| le K; InfCard(K); W <= Vfrom(A,csucc(K)) |] ==> \ |
127 \ W -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))"; |
127 \ W -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))"; |
128 by (safe_tac (ZF_cs addSDs [fun_Vcsucc_lemma, subset_Vcsucc])); |
128 by (safe_tac (ZF_cs addSDs [fun_Vcsucc_lemma, subset_Vcsucc])); |
129 by (resolve_tac [Vfrom RS ssubst] 1); |
129 by (resolve_tac [Vfrom RS ssubst] 1); |
130 by (eresolve_tac [PiE] 1); |
130 by (dresolve_tac [fun_is_rel] 1); |
131 (*This level includes the function, and is below csucc(K)*) |
131 (*This level includes the function, and is below csucc(K)*) |
132 by (res_inst_tac [("a1", "succ(succ(j Un ja))")] (UN_I RS UnI2) 1); |
132 by (res_inst_tac [("a1", "succ(succ(j Un ja))")] (UN_I RS UnI2) 1); |
133 by (eresolve_tac [subset_trans RS PowI] 2); |
133 by (eresolve_tac [subset_trans RS PowI] 2); |
134 by (fast_tac (ZF_cs addIs [Pair_in_Vfrom, Vfrom_UnI1, Vfrom_UnI2]) 2); |
134 by (fast_tac (ZF_cs addIs [Pair_in_Vfrom, Vfrom_UnI1, Vfrom_UnI2]) 2); |
135 by (REPEAT (ares_tac [ltD, InfCard_csucc, InfCard_is_Limit, |
135 by (REPEAT (ares_tac [ltD, InfCard_csucc, InfCard_is_Limit, |