31 |
31 |
32 val use_induction_hypothesis_tac = |
32 val use_induction_hypothesis_tac = |
33 DEEPEN (1, 64 (* large number *)) |
33 DEEPEN (1, 64 (* large number *)) |
34 (fn depth => meta_spec_mp_tac depth THEN' etac allE THEN' etac impE THEN' atac THEN' atac) 0; |
34 (fn depth => meta_spec_mp_tac depth THEN' etac allE THEN' etac impE THEN' atac THEN' atac) 0; |
35 |
35 |
36 val same_ctr_simps = |
36 val same_ctr_simps = @{thms sum_encode_eq prod_encode_eq sum.inject prod.inject to_nat_split |
37 @{thms sum_encode_eq prod_encode_eq sum.inject prod.inject to_nat_split snd_conv simp_thms}; |
37 id_apply snd_conv simp_thms}; |
38 val distinct_ctrs_simps = @{thms sum_encode_eq sum.inject sum.distinct simp_thms}; |
38 val distinct_ctrs_simps = @{thms sum_encode_eq sum.inject sum.distinct simp_thms}; |
39 |
39 |
40 fun same_ctr_tac ctxt injects recs map_congs' inj_map_strongs' = |
40 fun same_ctr_tac ctxt injects recs map_congs' inj_map_strongs' = |
41 HEADGOAL (asm_full_simp_tac |
41 HEADGOAL (asm_full_simp_tac |
42 (ss_only (injects @ recs @ map_congs' @ same_ctr_simps) ctxt) THEN_MAYBE' |
42 (ss_only (injects @ recs @ map_congs' @ same_ctr_simps) ctxt) THEN_MAYBE' |
43 TRY o REPEAT_ALL_NEW (rtac conjI) THEN_ALL_NEW |
43 TRY o REPEAT_ALL_NEW (rtac conjI) THEN_ALL_NEW |
44 REPEAT_ALL_NEW (eresolve_tac (conjE :: inj_map_strongs')) THEN_ALL_NEW |
44 REPEAT_ALL_NEW (eresolve_tac (conjE :: inj_map_strongs')) THEN_ALL_NEW |
45 use_induction_hypothesis_tac); |
45 (atac ORELSE' use_induction_hypothesis_tac)); |
46 |
46 |
47 fun distinct_ctrs_tac ctxt recs = |
47 fun distinct_ctrs_tac ctxt recs = |
48 HEADGOAL (asm_full_simp_tac (ss_only (recs @ distinct_ctrs_simps) ctxt)); |
48 HEADGOAL (asm_full_simp_tac (ss_only (recs @ distinct_ctrs_simps) ctxt)); |
49 |
49 |
50 fun mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs' = |
50 fun mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs' = |