28 val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic |
28 val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic |
29 val mk_half_distinct_tac: Proof.context -> thm -> thm -> thm list -> tactic |
29 val mk_half_distinct_tac: Proof.context -> thm -> thm -> thm list -> tactic |
30 val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list -> |
30 val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list -> |
31 thm list -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic |
31 thm list -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic |
32 val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic |
32 val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic |
33 val mk_map_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> thm list -> |
33 val mk_map_tac: Proof.context -> thm list -> thm -> thm -> thm list -> thm list -> thm list -> |
34 thm list -> tactic |
34 tactic |
35 val mk_map_disc_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic |
35 val mk_map_disc_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic |
36 val mk_map_sel_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> |
36 val mk_map_sel_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> |
37 thm list -> tactic |
37 thm list -> tactic |
38 val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> |
38 val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> |
39 tactic |
39 tactic |
40 val mk_rec_transfer_tac: Proof.context -> int -> int list -> cterm list -> cterm list -> |
40 val mk_rec_transfer_tac: Proof.context -> int -> int list -> cterm list -> cterm list -> |
41 term list list list list -> thm list -> thm list -> thm list -> thm list -> tactic |
41 term list list list list -> thm list -> thm list -> thm list -> thm list -> tactic |
42 val mk_rel_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> thm list -> |
42 val mk_rel_tac: Proof.context -> thm list -> thm -> thm -> thm list -> thm list -> thm list -> |
43 thm list -> tactic |
43 tactic |
44 val mk_rel_case_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> thm list -> |
44 val mk_rel_case_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> thm list -> |
45 thm list -> thm list -> tactic |
45 thm list -> thm list -> tactic |
46 val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list -> |
46 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 -> |
47 thm list list -> thm list list -> thm list list -> thm list -> thm list -> thm list -> |
48 thm list -> thm list -> thm list -> tactic |
48 thm list -> thm list -> thm list -> tactic |
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_id0s ctr_defs' |
395 fun mk_map_tac ctxt abs_inverses pre_map_def map_ctor 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 :: map_ctor :: abs_inverses @ live_nesting_map_id0s @ |
399 live_nesting_map_id0s @ ctr_defs' @ extra_unfolds @ sumprod_thms_map @ |
399 ctr_defs' @ extra_unfolds @ sumprod_thms_map @ |
400 @{thms o_apply id_apply id_o o_id}) 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 |
417 @{thms not_True_eq_False not_False_eq_True}) THEN |
417 @{thms not_True_eq_False not_False_eq_True}) THEN |
418 TRYALL (etac ctxt FalseE ORELSE' etac ctxt @{thm TrueE}) THEN |
418 TRYALL (etac ctxt FalseE ORELSE' etac ctxt @{thm TrueE}) THEN |
419 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 |
420 ALLGOALS (rtac ctxt refl); |
420 ALLGOALS (rtac ctxt refl); |
421 |
421 |
422 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 rel_ctor live_nesting_rel_eqs ctr_defs' extra_unfolds = |
423 extra_unfolds = |
423 TRYALL Goal.conjunction_tac THEN |
424 TRYALL Goal.conjunction_tac THEN |
424 unfold_thms_tac ctxt (pre_rel_def :: rel_ctor :: abs_inverses @ live_nesting_rel_eqs @ ctr_defs' @ |
425 unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: fp_rel :: abs_inverses @ live_nesting_rel_eqs @ |
425 extra_unfolds @ 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 |
|
427 sum.distinct(1)[THEN eq_False[THEN iffD2]] not_False_eq_True}) THEN |
426 sum.distinct(1)[THEN eq_False[THEN iffD2]] not_False_eq_True}) THEN |
428 ALLGOALS (resolve_tac ctxt [TrueI, refl]); |
427 ALLGOALS (resolve_tac ctxt [TrueI, refl]); |
429 |
428 |
430 fun mk_rel_case_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs = |
429 fun mk_rel_case_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs = |
431 HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct1] exhaust) THEN_ALL_NEW |
430 HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct1] exhaust) THEN_ALL_NEW |