338 etac ctxt CollectE, assume_tac ctxt])) alg_sets; |
338 etac ctxt CollectE, assume_tac ctxt])) alg_sets; |
339 val mor_tac = |
339 val mor_tac = |
340 CONJ_WRAP' (fn thm => EVERY' [rtac ctxt ballI, rtac ctxt thm]) str_init_defs; |
340 CONJ_WRAP' (fn thm => EVERY' [rtac ctxt ballI, rtac ctxt thm]) str_init_defs; |
341 fun alg_epi_tac ((alg_set, str_init_def), set_map) = |
341 fun alg_epi_tac ((alg_set, str_init_def), set_map) = |
342 EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt CollectI, |
342 EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt CollectI, |
343 rtac ctxt ballI, ftac ctxt (alg_select RS bspec), rtac ctxt (str_init_def RS @{thm ssubst_mem}), |
343 rtac ctxt ballI, forward_tac ctxt [alg_select RS bspec], |
|
344 rtac ctxt (str_init_def RS @{thm ssubst_mem}), |
344 etac ctxt alg_set, REPEAT_DETERM o EVERY' [rtac ctxt ord_eq_le_trans, resolve_tac ctxt set_map, |
345 etac ctxt alg_set, REPEAT_DETERM o EVERY' [rtac ctxt ord_eq_le_trans, resolve_tac ctxt set_map, |
345 rtac ctxt subset_trans, etac ctxt @{thm image_mono}, rtac ctxt @{thm image_Collect_subsetI}, etac ctxt bspec, |
346 rtac ctxt subset_trans, etac ctxt @{thm image_mono}, rtac ctxt @{thm image_Collect_subsetI}, etac ctxt bspec, |
346 assume_tac ctxt]]; |
347 assume_tac ctxt]]; |
347 in |
348 in |
348 EVERY' [rtac ctxt mor_cong, REPEAT_DETERM_N n o (rtac ctxt sym THEN' rtac ctxt @{thm comp_id}), |
349 EVERY' [rtac ctxt mor_cong, REPEAT_DETERM_N n o (rtac ctxt sym THEN' rtac ctxt @{thm comp_id}), |