equal
deleted
inserted
replaced
32 thm list -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic |
32 thm list -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic |
33 val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic |
33 val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic |
34 val mk_map_disc_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic |
34 val mk_map_disc_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic |
35 val mk_map_sel_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> |
35 val mk_map_sel_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> |
36 thm list -> tactic |
36 thm list -> tactic |
|
37 val mk_rec_o_map_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> thm -> thm -> |
|
38 thm Seq.seq |
37 val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> |
39 val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> |
38 tactic |
40 tactic |
39 val mk_rec_transfer_tac: Proof.context -> int -> int list -> cterm list -> cterm list -> |
41 val mk_rec_transfer_tac: Proof.context -> int -> int list -> cterm list -> cterm list -> |
40 thm list -> thm list -> thm list -> thm list -> tactic |
42 thm list -> thm list -> thm list -> thm list -> tactic |
41 val mk_rel_cases_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> |
43 val mk_rel_cases_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> |
158 HEADGOAL (rtac refl); |
160 HEADGOAL (rtac refl); |
159 |
161 |
160 val rec_unfold_thms = |
162 val rec_unfold_thms = |
161 @{thms comp_def convol_def fst_conv id_def case_prod_Pair_iden snd_conv split_conv |
163 @{thms comp_def convol_def fst_conv id_def case_prod_Pair_iden snd_conv split_conv |
162 case_unit_Unity} @ sumprod_thms_map; |
164 case_unit_Unity} @ sumprod_thms_map; |
|
165 |
|
166 fun mk_rec_o_map_tac ctxt rec_def pre_map_defs map_ident0s abs_inverses ctor_rec_o_map = |
|
167 let |
|
168 val rec_o_map_simps = |
|
169 @{thms o_def[abs_def] id_def case_prod_app case_sum_map_sum case_prod_map_prod id_bnf_def}; |
|
170 in |
|
171 HEADGOAL (subst_tac @{context} (SOME [1, 2]) [rec_def] THEN' |
|
172 rtac (ctor_rec_o_map RS trans) THEN' |
|
173 CONVERSION Thm.eta_long_conversion THEN' |
|
174 asm_simp_tac (ss_only (pre_map_defs @ distinct Thm.eq_thm_prop (map_ident0s @ abs_inverses) @ |
|
175 rec_o_map_simps) ctxt)) |
|
176 end; |
163 |
177 |
164 fun mk_rec_tac pre_map_defs map_ident0s rec_defs ctor_rec fp_abs_inverse abs_inverse ctr_def ctxt = |
178 fun mk_rec_tac pre_map_defs map_ident0s rec_defs ctor_rec fp_abs_inverse abs_inverse ctr_def ctxt = |
165 HEADGOAL ((if is_def_looping ctr_def then subst_tac ctxt NONE |
179 HEADGOAL ((if is_def_looping ctr_def then subst_tac ctxt NONE |
166 else SELECT_GOAL o unfold_thms_tac ctxt) [ctr_def]) THEN |
180 else SELECT_GOAL o unfold_thms_tac ctxt) [ctr_def]) THEN |
167 unfold_thms_tac ctxt (ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @ |
181 unfold_thms_tac ctxt (ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @ |