|
1 (* Title: HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML |
|
2 Author: Jasmin Blanchette, TU Muenchen |
|
3 Copyright 2012 |
|
4 |
|
5 Tactics for datatype and codatatype sugar. |
|
6 *) |
|
7 |
|
8 signature BNF_FP_DEF_SUGAR_TACTICS = |
|
9 sig |
|
10 val sum_prod_thms_map: thm list |
|
11 val sum_prod_thms_set: thm list |
|
12 val sum_prod_thms_rel: thm list |
|
13 |
|
14 val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list -> |
|
15 thm list -> thm list -> thm list list -> thm list list list -> thm list list list -> tactic |
|
16 val mk_coiter_tac: thm list -> thm list -> thm -> thm -> thm -> Proof.context -> tactic |
|
17 val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm -> |
|
18 tactic |
|
19 val mk_disc_coiter_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic |
|
20 val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic |
|
21 val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic |
|
22 val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list -> |
|
23 thm list -> thm -> thm list -> thm list list -> tactic |
|
24 val mk_inject_tac: Proof.context -> thm -> thm -> tactic |
|
25 val mk_iter_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic |
|
26 end; |
|
27 |
|
28 structure BNF_FP_Def_Sugar_Tactics : BNF_FP_DEF_SUGAR_TACTICS = |
|
29 struct |
|
30 |
|
31 open BNF_Tactics |
|
32 open BNF_Util |
|
33 open BNF_FP_Util |
|
34 |
|
35 val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)}; |
|
36 val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)}; |
|
37 |
|
38 val sum_prod_thms_map = @{thms id_apply map_pair_simp prod.cases sum.cases sum_map.simps}; |
|
39 val sum_prod_thms_set0 = |
|
40 @{thms SUP_empty Sup_empty Sup_insert UN_insert Un_empty_left Un_empty_right Un_iff |
|
41 Union_Un_distrib collect_def[abs_def] image_def o_apply map_pair_simp |
|
42 mem_Collect_eq mem_UN_compreh_eq prod_set_simps sum_map.simps sum_set_simps}; |
|
43 val sum_prod_thms_set = @{thms UN_compreh_eq_eq} @ sum_prod_thms_set0; |
|
44 val sum_prod_thms_rel = @{thms prod_rel_simp sum_rel_simps id_apply}; |
|
45 |
|
46 fun hhf_concl_conv cv ctxt ct = |
|
47 (case Thm.term_of ct of |
|
48 Const (@{const_name all}, _) $ Abs _ => |
|
49 Conv.arg_conv (Conv.abs_conv (hhf_concl_conv cv o snd) ctxt) ct |
|
50 | _ => Conv.concl_conv ~1 cv ct); |
|
51 |
|
52 fun co_induct_inst_as_projs ctxt k thm = |
|
53 let |
|
54 val fs = Term.add_vars (prop_of thm) [] |
|
55 |> filter (fn (_, Type (@{type_name fun}, [_, T'])) => T' <> HOLogic.boolT | _ => false); |
|
56 fun mk_cfp (f as (_, T)) = |
|
57 (certify ctxt (Var f), certify ctxt (mk_proj T (num_binder_types T) k)); |
|
58 val cfps = map mk_cfp fs; |
|
59 in |
|
60 Drule.cterm_instantiate cfps thm |
|
61 end; |
|
62 |
|
63 val co_induct_inst_as_projs_tac = PRIMITIVE oo co_induct_inst_as_projs; |
|
64 |
|
65 fun mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor sumEN' = |
|
66 unfold_thms_tac ctxt (ctor_iff_dtor :: ctr_defs) THEN HEADGOAL (rtac sumEN') THEN |
|
67 unfold_thms_tac ctxt @{thms split_paired_all} THEN |
|
68 HEADGOAL (EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k, |
|
69 REPEAT_DETERM o dtac meta_spec, etac meta_mp, atac]) (1 upto n))); |
|
70 |
|
71 fun mk_ctor_iff_dtor_tac ctxt cTs cctor cdtor ctor_dtor dtor_ctor = |
|
72 HEADGOAL (rtac iffI THEN' |
|
73 EVERY' (map3 (fn cTs => fn cx => fn th => |
|
74 dtac (Drule.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN' |
|
75 SELECT_GOAL (unfold_thms_tac ctxt [th]) THEN' |
|
76 atac) [rev cTs, cTs] [cdtor, cctor] [dtor_ctor, ctor_dtor])); |
|
77 |
|
78 fun mk_half_distinct_tac ctxt ctor_inject ctr_defs = |
|
79 unfold_thms_tac ctxt (ctor_inject :: @{thms sum.inject} @ ctr_defs) THEN |
|
80 HEADGOAL (rtac @{thm sum.distinct(1)}); |
|
81 |
|
82 fun mk_inject_tac ctxt ctr_def ctor_inject = |
|
83 unfold_thms_tac ctxt [ctr_def] THEN HEADGOAL (rtac (ctor_inject RS ssubst)) THEN |
|
84 unfold_thms_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN HEADGOAL (rtac refl); |
|
85 |
|
86 val iter_unfold_thms = |
|
87 @{thms comp_def convol_def fst_conv id_def prod_case_Pair_iden snd_conv |
|
88 split_conv unit_case_Unity} @ sum_prod_thms_map; |
|
89 |
|
90 fun mk_iter_tac pre_map_defs map_idents iter_defs ctor_iter ctr_def ctxt = |
|
91 unfold_thms_tac ctxt (ctr_def :: ctor_iter :: iter_defs @ pre_map_defs @ map_idents @ |
|
92 iter_unfold_thms) THEN HEADGOAL (rtac refl); |
|
93 |
|
94 val coiter_unfold_thms = @{thms id_def} @ sum_prod_thms_map; |
|
95 val ss_if_True_False = simpset_of (ss_only @{thms if_True if_False} @{context}); |
|
96 |
|
97 fun mk_coiter_tac coiter_defs map_idents ctor_dtor_coiter pre_map_def ctr_def ctxt = |
|
98 unfold_thms_tac ctxt (ctr_def :: coiter_defs) THEN |
|
99 HEADGOAL (rtac (ctor_dtor_coiter RS trans) THEN' |
|
100 asm_simp_tac (put_simpset ss_if_True_False ctxt)) THEN_MAYBE |
|
101 (unfold_thms_tac ctxt (pre_map_def :: map_idents @ coiter_unfold_thms) THEN |
|
102 HEADGOAL (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong))); |
|
103 |
|
104 fun mk_disc_coiter_iff_tac case_splits' coiters discs ctxt = |
|
105 EVERY (map3 (fn case_split_tac => fn coiter_thm => fn disc => |
|
106 HEADGOAL case_split_tac THEN unfold_thms_tac ctxt [coiter_thm] THEN |
|
107 HEADGOAL (asm_simp_tac (ss_only basic_simp_thms ctxt)) THEN |
|
108 (if is_refl disc then all_tac else HEADGOAL (rtac disc))) |
|
109 (map rtac case_splits' @ [K all_tac]) coiters discs); |
|
110 |
|
111 fun solve_prem_prem_tac ctxt = |
|
112 REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE' |
|
113 hyp_subst_tac ctxt ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN' |
|
114 (rtac refl ORELSE' atac ORELSE' rtac @{thm singletonI}); |
|
115 |
|
116 fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_maps pre_set_defs = |
|
117 HEADGOAL (EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp, |
|
118 SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ set_maps @ sum_prod_thms_set0)), |
|
119 solve_prem_prem_tac ctxt]) (rev kks))); |
|
120 |
|
121 fun mk_induct_discharge_prem_tac ctxt nn n set_maps pre_set_defs m k kks = |
|
122 let val r = length kks in |
|
123 HEADGOAL (EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac ctxt, |
|
124 REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)]) THEN |
|
125 EVERY [REPEAT_DETERM_N r |
|
126 (HEADGOAL (rotate_tac ~1 THEN' dtac meta_mp THEN' rotate_tac 1) THEN prefer_tac 2), |
|
127 if r > 0 then ALLGOALS (Goal.norm_hhf_tac ctxt) else all_tac, HEADGOAL atac, |
|
128 mk_induct_leverage_prem_prems_tac ctxt nn kks set_maps pre_set_defs] |
|
129 end; |
|
130 |
|
131 fun mk_induct_tac ctxt nn ns mss kkss ctr_defs ctor_induct' set_maps pre_set_defss = |
|
132 let val n = Integer.sum ns in |
|
133 unfold_thms_tac ctxt ctr_defs THEN HEADGOAL (rtac ctor_induct') THEN |
|
134 co_induct_inst_as_projs_tac ctxt 0 THEN |
|
135 EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_maps) pre_set_defss |
|
136 mss (unflat mss (1 upto n)) kkss) |
|
137 end; |
|
138 |
|
139 fun mk_coinduct_same_ctr_tac ctxt rel_eqs pre_rel_def dtor_ctor ctr_def discs sels = |
|
140 hyp_subst_tac ctxt THEN' |
|
141 CONVERSION (hhf_concl_conv |
|
142 (Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv ctr_def))) ctxt) ctxt) THEN' |
|
143 SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels)) THEN' |
|
144 SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels @ sum_prod_thms_rel)) THEN' |
|
145 (atac ORELSE' REPEAT o etac conjE THEN' |
|
146 full_simp_tac |
|
147 (ss_only (@{thm prod.inject} :: no_refl discs @ rel_eqs @ more_simp_thms) ctxt) THEN' |
|
148 REPEAT o etac conjE THEN_MAYBE' REPEAT o hyp_subst_tac ctxt THEN' |
|
149 REPEAT o (resolve_tac [refl, conjI] ORELSE' atac)); |
|
150 |
|
151 fun mk_coinduct_distinct_ctrs_tac ctxt discs discs' = |
|
152 let |
|
153 val discs'' = map (perhaps (try (fn th => th RS @{thm notnotD}))) (discs @ discs') |
|
154 |> distinct Thm.eq_thm_prop; |
|
155 in |
|
156 hyp_subst_tac ctxt THEN' REPEAT o etac conjE THEN' |
|
157 full_simp_tac (ss_only (refl :: no_refl discs'' @ basic_simp_thms) ctxt) |
|
158 end; |
|
159 |
|
160 fun mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn kk n pre_rel_def dtor_ctor exhaust ctr_defs |
|
161 discss selss = |
|
162 let val ks = 1 upto n in |
|
163 EVERY' ([rtac allI, rtac allI, rtac impI, select_prem_tac nn (dtac meta_spec) kk, |
|
164 dtac meta_spec, dtac meta_mp, atac, rtac exhaust, K (co_induct_inst_as_projs_tac ctxt 0), |
|
165 hyp_subst_tac ctxt] @ |
|
166 map4 (fn k => fn ctr_def => fn discs => fn sels => |
|
167 EVERY' ([rtac exhaust, K (co_induct_inst_as_projs_tac ctxt 1)] @ |
|
168 map2 (fn k' => fn discs' => |
|
169 if k' = k then |
|
170 mk_coinduct_same_ctr_tac ctxt rel_eqs' pre_rel_def dtor_ctor ctr_def discs sels |
|
171 else |
|
172 mk_coinduct_distinct_ctrs_tac ctxt discs discs') ks discss)) ks ctr_defs discss selss) |
|
173 end; |
|
174 |
|
175 fun mk_coinduct_tac ctxt rel_eqs' nn ns dtor_coinduct' pre_rel_defs dtor_ctors exhausts ctr_defss |
|
176 discsss selsss = |
|
177 HEADGOAL (rtac dtor_coinduct' THEN' |
|
178 EVERY' (map8 (mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn) |
|
179 (1 upto nn) ns pre_rel_defs dtor_ctors exhausts ctr_defss discsss selsss)); |
|
180 |
|
181 end; |