317 rtac ctxt @{thm ordLeq_ordIso_trans[OF cprod_mono2 ordIso_symmetric[OF cprod_cexp]]}), |
317 rtac ctxt @{thm ordLeq_ordIso_trans[OF cprod_mono2 ordIso_symmetric[OF cprod_cexp]]}), |
318 rtac ctxt @{thm ordLeq_refl[OF Card_order_cexp]}] 1 THEN |
318 rtac ctxt @{thm ordLeq_refl[OF Card_order_cexp]}] 1 THEN |
319 unfold_thms_tac ctxt [bd_card_order RS @{thm card_order_csum_cone_cexp_def}] THEN |
319 unfold_thms_tac ctxt [bd_card_order RS @{thm card_order_csum_cone_cexp_def}] THEN |
320 unfold_thms_tac ctxt @{thms cprod_def Field_card_of} THEN |
320 unfold_thms_tac ctxt @{thms cprod_def Field_card_of} THEN |
321 EVERY' [rtac ctxt (Drule.rotate_prems 1 ctrans), rtac ctxt surj_imp_ordLeq_inst, rtac ctxt subsetI, |
321 EVERY' [rtac ctxt (Drule.rotate_prems 1 ctrans), rtac ctxt surj_imp_ordLeq_inst, rtac ctxt subsetI, |
322 Method.insert_tac inserts, REPEAT_DETERM o dtac ctxt meta_spec, |
322 Method.insert_tac ctxt inserts, REPEAT_DETERM o dtac ctxt meta_spec, |
323 REPEAT_DETERM o eresolve_tac ctxt [exE, Tactic.make_elim conjunct1], etac ctxt CollectE, |
323 REPEAT_DETERM o eresolve_tac ctxt [exE, Tactic.make_elim conjunct1], etac ctxt CollectE, |
324 if live = 1 then K all_tac |
324 if live = 1 then K all_tac |
325 else REPEAT_DETERM_N (live - 2) o (etac ctxt conjE THEN' rotate_tac ~1) THEN' etac ctxt conjE, |
325 else REPEAT_DETERM_N (live - 2) o (etac ctxt conjE THEN' rotate_tac ~1) THEN' etac ctxt conjE, |
326 rtac ctxt (Drule.rotate_prems 1 @{thm image_eqI}), rtac ctxt @{thm SigmaI}, rtac ctxt @{thm UNIV_I}, |
326 rtac ctxt (Drule.rotate_prems 1 @{thm image_eqI}), rtac ctxt @{thm SigmaI}, rtac ctxt @{thm UNIV_I}, |
327 CONJ_WRAP_GEN' (rtac ctxt @{thm SigmaI}) |
327 CONJ_WRAP_GEN' (rtac ctxt @{thm SigmaI}) |