7 *) |
7 *) |
8 |
8 |
9 signature BNF_FP_DEF_SUGAR_TACTICS = |
9 signature BNF_FP_DEF_SUGAR_TACTICS = |
10 sig |
10 sig |
11 val sumprod_thms_rel: thm list |
11 val sumprod_thms_rel: thm list |
12 val sumprod_thms_set: thm list (* FIXME *) |
|
13 val basic_sumprod_thms_set: thm list |
|
14 |
12 |
15 val mk_case_transfer_tac: Proof.context -> thm -> thm list -> tactic |
13 val mk_case_transfer_tac: Proof.context -> thm -> thm list -> tactic |
16 val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list -> |
14 val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list -> |
17 thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list -> |
15 thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list -> |
18 thm list list list -> tactic |
16 thm list list list -> tactic |
80 val simp_thms' = @{thms simp_thms(6,7,8,11,12,15,16,22,24)}; |
78 val simp_thms' = @{thms simp_thms(6,7,8,11,12,15,16,22,24)}; |
81 |
79 |
82 val sumprod_thms_map = @{thms id_apply map_prod_simp prod.case sum.case map_sum.simps}; |
80 val sumprod_thms_map = @{thms id_apply map_prod_simp prod.case sum.case map_sum.simps}; |
83 val sumprod_thms_rel = @{thms rel_sum_simps rel_prod_inject prod.inject id_apply conj_assoc}; |
81 val sumprod_thms_rel = @{thms rel_sum_simps rel_prod_inject prod.inject id_apply conj_assoc}; |
84 val basic_sumprod_thms_set = |
82 val basic_sumprod_thms_set = |
85 @{thms UN_empty UN_insert UN_iff Un_empty_left Un_empty_right Un_iff Union_Un_distrib |
83 @{thms UN_empty UN_insert UN_iff Un_empty_left Un_empty_right Un_iff Union_Un_distrib o_apply |
86 o_apply map_prod_simp mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps}; |
84 map_prod_simp mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps}; |
87 val sumprod_thms_set = @{thms UN_simps(10) image_iff} @ basic_sumprod_thms_set; |
85 val sumprod_thms_set = @{thms UN_simps(10) image_iff} @ basic_sumprod_thms_set; |
88 |
86 |
89 fun is_def_looping def = |
87 fun is_def_looping def = |
90 (case Thm.prop_of def of |
88 (case Thm.prop_of def of |
91 Const (@{const_name Pure.eq}, _) $ lhs $ rhs => Term.exists_subterm (curry (op aconv) lhs) rhs |
89 Const (@{const_name Pure.eq}, _) $ lhs $ rhs => Term.exists_subterm (curry (op aconv) lhs) rhs |
496 REPEAT_DETERM o (assume_tac ctxt ORELSE' rtac ctxt rel_funI)); |
494 REPEAT_DETERM o (assume_tac ctxt ORELSE' rtac ctxt rel_funI)); |
497 |
495 |
498 fun mk_set0_tac ctxt abs_inverses pre_set_defs dtor_ctor fp_sets fp_nesting_set_maps |
496 fun mk_set0_tac ctxt abs_inverses pre_set_defs dtor_ctor fp_sets fp_nesting_set_maps |
499 live_nesting_set_maps ctr_defs' extra_unfolds = |
497 live_nesting_set_maps ctr_defs' extra_unfolds = |
500 TRYALL Goal.conjunction_tac THEN |
498 TRYALL Goal.conjunction_tac THEN |
501 unfold_thms_tac ctxt (dtor_ctor :: abs_inverses @ pre_set_defs @ fp_sets @ fp_nesting_set_maps @ |
499 unfold_thms_tac ctxt ctr_defs' THEN |
502 live_nesting_set_maps @ ctr_defs' @ extra_unfolds @ basic_sumprod_thms_set @ |
500 ALLGOALS (subst_tac ctxt NONE fp_sets) THEN |
|
501 unfold_thms_tac ctxt (dtor_ctor :: abs_inverses @ pre_set_defs @ fp_nesting_set_maps @ |
|
502 live_nesting_set_maps @ extra_unfolds @ basic_sumprod_thms_set @ |
503 @{thms UN_UN_flatten UN_Un sup_assoc[THEN sym]}) THEN |
503 @{thms UN_UN_flatten UN_Un sup_assoc[THEN sym]}) THEN |
504 ALLGOALS (rtac ctxt refl); |
504 ALLGOALS (rtac ctxt @{thm set_eqI[OF iffI]}) THEN |
|
505 ALLGOALS (REPEAT_DETERM o etac ctxt UnE) THEN |
|
506 ALLGOALS (REPEAT o resolve_tac ctxt @{thms UnI1 UnI2} THEN' assume_tac ctxt); |
505 |
507 |
506 fun mk_set_sel_tac ctxt ct exhaust discs sels sets = |
508 fun mk_set_sel_tac ctxt ct exhaust discs sels sets = |
507 TRYALL Goal.conjunction_tac THEN |
509 TRYALL Goal.conjunction_tac THEN |
508 ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW |
510 ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW |
509 REPEAT_DETERM o hyp_subst_tac ctxt) THEN |
511 REPEAT_DETERM o hyp_subst_tac ctxt) THEN |