equal
deleted
inserted
replaced
390 HEADGOAL (rtac ctxt dtor_coinduct' THEN' |
390 HEADGOAL (rtac ctxt dtor_coinduct' THEN' |
391 EVERY' (@{map 10} (mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn) |
391 EVERY' (@{map 10} (mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn) |
392 (1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss |
392 (1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss |
393 selsss)); |
393 selsss)); |
394 |
394 |
395 fun mk_map_tac ctxt abs_inverses pre_map_def dtor_ctor fp_map' live_nesting_map_ident0s ctr_defs' |
395 fun mk_map_tac ctxt abs_inverses pre_map_def dtor_ctor fp_map' live_nesting_map_id0s ctr_defs' |
396 extra_unfolds = |
396 extra_unfolds = |
397 TRYALL Goal.conjunction_tac THEN |
397 TRYALL Goal.conjunction_tac THEN |
398 unfold_thms_tac ctxt (pre_map_def :: dtor_ctor :: fp_map' :: abs_inverses @ |
398 unfold_thms_tac ctxt (pre_map_def :: dtor_ctor :: fp_map' :: abs_inverses @ |
399 live_nesting_map_ident0s @ ctr_defs' @ extra_unfolds @ sumprod_thms_map @ |
399 live_nesting_map_id0s @ ctr_defs' @ extra_unfolds @ sumprod_thms_map @ |
400 @{thms o_def[abs_def] id_def}) THEN |
400 @{thms o_apply id_apply id_o o_id}) THEN |
401 ALLGOALS (rtac ctxt refl); |
401 ALLGOALS (rtac ctxt refl); |
402 |
402 |
403 fun mk_map_disc_iff_tac ctxt ct exhaust discs maps = |
403 fun mk_map_disc_iff_tac ctxt ct exhaust discs maps = |
404 TRYALL Goal.conjunction_tac THEN |
404 TRYALL Goal.conjunction_tac THEN |
405 ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW |
405 ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW |