30 val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic |
30 val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic |
31 val mk_half_distinct_tac: Proof.context -> thm -> thm -> thm list -> tactic |
31 val mk_half_distinct_tac: Proof.context -> thm -> thm -> thm list -> tactic |
32 val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list -> |
32 val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list -> |
33 thm list -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic |
33 thm list -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic |
34 val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic |
34 val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic |
35 val mk_map_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> thm list -> tactic |
35 val mk_map_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> thm list -> |
|
36 thm list -> tactic |
36 val mk_map_disc_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic |
37 val mk_map_disc_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic |
37 val mk_map_sel_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> |
38 val mk_map_sel_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> |
38 thm list -> tactic |
39 thm list -> tactic |
39 val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> |
40 val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> |
40 tactic |
41 tactic |
41 val mk_rec_transfer_tac: Proof.context -> int -> int list -> cterm list -> cterm list -> |
42 val mk_rec_transfer_tac: Proof.context -> int -> int list -> cterm list -> cterm list -> |
42 term list list list list -> thm list -> thm list -> thm list -> thm list -> tactic |
43 term list list list list -> thm list -> thm list -> thm list -> thm list -> tactic |
43 val mk_rel_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> thm list -> tactic |
44 val mk_rel_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> thm list -> |
|
45 thm list -> tactic |
44 val mk_rel_case_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> thm list -> |
46 val mk_rel_case_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> thm list -> |
45 thm list -> thm list -> tactic |
47 thm list -> thm list -> tactic |
46 val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list -> |
48 val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list -> |
47 thm list list -> thm list list -> thm list list -> thm list -> thm list -> thm list -> |
49 thm list list -> thm list list -> thm list list -> thm list -> thm list -> thm list -> |
48 thm list -> thm list -> thm list -> tactic |
50 thm list -> thm list -> thm list -> tactic |
388 HEADGOAL (rtac ctxt dtor_coinduct' THEN' |
390 HEADGOAL (rtac ctxt dtor_coinduct' THEN' |
389 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) |
390 (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 |
391 selsss)); |
393 selsss)); |
392 |
394 |
393 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_ident0s ctr_defs' |
|
396 extra_unfolds = |
394 TRYALL Goal.conjunction_tac THEN |
397 TRYALL Goal.conjunction_tac THEN |
395 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 @ |
396 live_nesting_map_ident0s @ |
399 live_nesting_map_ident0s @ ctr_defs' @ extra_unfolds @ sumprod_thms_map @ |
397 ctr_defs' @ sumprod_thms_map @ @{thms o_def[abs_def] id_def}) THEN |
400 @{thms o_def[abs_def] id_def}) THEN |
398 ALLGOALS (rtac ctxt refl); |
401 ALLGOALS (rtac ctxt refl); |
399 |
402 |
400 fun mk_map_disc_iff_tac ctxt ct exhaust discs maps = |
403 fun mk_map_disc_iff_tac ctxt ct exhaust discs maps = |
401 TRYALL Goal.conjunction_tac THEN |
404 TRYALL Goal.conjunction_tac THEN |
402 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 |
414 @{thms not_True_eq_False not_False_eq_True}) THEN |
417 @{thms not_True_eq_False not_False_eq_True}) THEN |
415 TRYALL (etac ctxt FalseE ORELSE' etac ctxt @{thm TrueE}) THEN |
418 TRYALL (etac ctxt FalseE ORELSE' etac ctxt @{thm TrueE}) THEN |
416 unfold_thms_tac ctxt (@{thm id_apply} :: maps @ sels @ map_id0s) THEN |
419 unfold_thms_tac ctxt (@{thm id_apply} :: maps @ sels @ map_id0s) THEN |
417 ALLGOALS (rtac ctxt refl); |
420 ALLGOALS (rtac ctxt refl); |
418 |
421 |
419 fun mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel live_nesting_rel_eqs ctr_defs' = |
422 fun mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel live_nesting_rel_eqs ctr_defs' |
|
423 extra_unfolds = |
420 TRYALL Goal.conjunction_tac THEN |
424 TRYALL Goal.conjunction_tac THEN |
421 unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: fp_rel :: abs_inverses @ live_nesting_rel_eqs @ |
425 unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: fp_rel :: abs_inverses @ live_nesting_rel_eqs @ |
422 ctr_defs' @ sumprod_thms_rel @ @{thms vimage2p_def o_apply sum.inject |
426 ctr_defs' @ extra_unfolds @ sumprod_thms_rel @ @{thms vimage2p_def o_apply sum.inject |
423 sum.distinct(1)[THEN eq_False[THEN iffD2]] not_False_eq_True}) THEN |
427 sum.distinct(1)[THEN eq_False[THEN iffD2]] not_False_eq_True}) THEN |
424 ALLGOALS (resolve_tac ctxt [TrueI, refl]); |
428 ALLGOALS (resolve_tac ctxt [TrueI, refl]); |
425 |
429 |
426 fun mk_rel_case_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs = |
430 fun mk_rel_case_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs = |
427 HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct1] exhaust) THEN_ALL_NEW |
431 HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct1] exhaust) THEN_ALL_NEW |