10 val sum_prod_thms_map: thm list |
10 val sum_prod_thms_map: thm list |
11 val sum_prod_thms_set: thm list |
11 val sum_prod_thms_set: thm list |
12 val sum_prod_thms_rel: thm list |
12 val sum_prod_thms_rel: thm list |
13 |
13 |
14 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 -> |
15 thm list -> thm list -> thm list list -> thm list list list -> thm list list list -> tactic |
15 thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list -> |
16 val mk_coiter_tac: thm list -> thm list -> thm -> thm -> thm -> Proof.context -> tactic |
16 thm list list list -> tactic |
|
17 val mk_coiter_tac: thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic |
17 val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm -> |
18 val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm -> |
18 tactic |
19 tactic |
19 val mk_disc_coiter_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic |
20 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_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_half_distinct_tac: Proof.context -> thm -> thm -> thm list -> tactic |
22 val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list -> |
23 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 thm list -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic |
24 val mk_inject_tac: Proof.context -> thm -> thm -> tactic |
25 val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic |
25 val mk_iter_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic |
26 val mk_iter_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> |
|
27 tactic |
26 end; |
28 end; |
27 |
29 |
28 structure BNF_FP_Def_Sugar_Tactics : BNF_FP_DEF_SUGAR_TACTICS = |
30 structure BNF_FP_Def_Sugar_Tactics : BNF_FP_DEF_SUGAR_TACTICS = |
29 struct |
31 struct |
30 |
32 |
73 EVERY' (map3 (fn cTs => fn cx => fn th => |
75 EVERY' (map3 (fn cTs => fn cx => fn th => |
74 dtac (Drule.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN' |
76 dtac (Drule.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN' |
75 SELECT_GOAL (unfold_thms_tac ctxt [th]) THEN' |
77 SELECT_GOAL (unfold_thms_tac ctxt [th]) THEN' |
76 atac) [rev cTs, cTs] [cdtor, cctor] [dtor_ctor, ctor_dtor])); |
78 atac) [rev cTs, cTs] [cdtor, cctor] [dtor_ctor, ctor_dtor])); |
77 |
79 |
78 fun mk_half_distinct_tac ctxt ctor_inject ctr_defs = |
80 fun mk_half_distinct_tac ctxt ctor_inject abs_inject ctr_defs = |
79 unfold_thms_tac ctxt (ctor_inject :: @{thms sum.inject} @ ctr_defs) THEN |
81 unfold_thms_tac ctxt (ctor_inject :: abs_inject :: @{thms sum.inject} @ ctr_defs) THEN |
80 HEADGOAL (rtac @{thm sum.distinct(1)}); |
82 HEADGOAL (rtac @{thm sum.distinct(1)}); |
81 |
83 |
82 fun mk_inject_tac ctxt ctr_def ctor_inject = |
84 fun mk_inject_tac ctxt ctr_def ctor_inject abs_inject = |
83 unfold_thms_tac ctxt [ctr_def] THEN HEADGOAL (rtac (ctor_inject RS ssubst)) THEN |
85 unfold_thms_tac ctxt [ctr_def] THEN |
84 unfold_thms_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN HEADGOAL (rtac refl); |
86 HEADGOAL (rtac (ctor_inject RS ssubst)) THEN |
|
87 unfold_thms_tac ctxt (abs_inject :: @{thms sum.inject Pair_eq conj_assoc}) THEN |
|
88 HEADGOAL (rtac refl); |
85 |
89 |
86 val iter_unfold_thms = |
90 val iter_unfold_thms = |
87 @{thms comp_def convol_def fst_conv id_def case_prod_Pair_iden snd_conv split_conv |
91 @{thms comp_def convol_def fst_conv id_def case_prod_Pair_iden snd_conv split_conv |
88 case_unit_Unity} @ sum_prod_thms_map; |
92 case_unit_Unity} @ sum_prod_thms_map; |
89 |
93 |
90 fun mk_iter_tac pre_map_defs map_idents iter_defs ctor_iter ctr_def ctxt = |
94 fun mk_iter_tac pre_map_defs map_idents iter_defs ctor_iter fp_abs_inverse abs_inverse ctr_def ctxt = |
91 unfold_thms_tac ctxt (ctr_def :: ctor_iter :: iter_defs @ pre_map_defs @ map_idents @ |
95 unfold_thms_tac ctxt (ctr_def :: ctor_iter :: fp_abs_inverse :: abs_inverse :: iter_defs @ |
92 iter_unfold_thms) THEN HEADGOAL (rtac refl); |
96 pre_map_defs @ map_idents @ iter_unfold_thms) THEN HEADGOAL (rtac refl); |
93 |
97 |
94 val coiter_unfold_thms = @{thms id_def} @ sum_prod_thms_map; |
98 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 |
99 |
97 fun mk_coiter_tac coiter_defs map_idents ctor_dtor_coiter pre_map_def ctr_def ctxt = |
100 fun mk_coiter_tac coiter_defs map_idents ctor_dtor_coiter pre_map_def abs_inverse ctr_def ctxt = |
98 unfold_thms_tac ctxt (ctr_def :: coiter_defs) THEN |
101 let |
99 HEADGOAL (rtac (ctor_dtor_coiter RS trans) THEN' |
102 val ss = ss_only (pre_map_def :: abs_inverse :: map_idents @ coiter_unfold_thms @ |
100 asm_simp_tac (put_simpset ss_if_True_False ctxt)) THEN_MAYBE |
103 @{thms o_apply vimage2p_def if_True if_False}) ctxt; |
101 (unfold_thms_tac ctxt (pre_map_def :: map_idents @ coiter_unfold_thms) THEN |
104 in |
102 HEADGOAL (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong))); |
105 unfold_thms_tac ctxt (ctr_def :: coiter_defs) THEN |
|
106 HEADGOAL (rtac (ctor_dtor_coiter RS trans) THEN' asm_simp_tac ss) THEN_MAYBE |
|
107 HEADGOAL (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong)) |
|
108 end; |
103 |
109 |
104 fun mk_disc_coiter_iff_tac case_splits' coiters discs ctxt = |
110 fun mk_disc_coiter_iff_tac case_splits' coiters discs ctxt = |
105 EVERY (map3 (fn case_split_tac => fn coiter_thm => fn disc => |
111 EVERY (map3 (fn case_split_tac => fn coiter_thm => fn disc => |
106 HEADGOAL case_split_tac THEN unfold_thms_tac ctxt [coiter_thm] THEN |
112 HEADGOAL case_split_tac THEN unfold_thms_tac ctxt [coiter_thm] THEN |
107 HEADGOAL (asm_simp_tac (ss_only basic_simp_thms ctxt)) THEN |
113 HEADGOAL (asm_simp_tac (ss_only basic_simp_thms ctxt)) THEN |
111 fun solve_prem_prem_tac ctxt = |
117 fun solve_prem_prem_tac ctxt = |
112 REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE' |
118 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' |
119 hyp_subst_tac ctxt ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN' |
114 (rtac refl ORELSE' atac ORELSE' rtac @{thm singletonI}); |
120 (rtac refl ORELSE' atac ORELSE' rtac @{thm singletonI}); |
115 |
121 |
116 fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_maps pre_set_defs = |
122 fun mk_induct_leverage_prem_prems_tac ctxt nn kks fp_abs_inverses abs_inverses set_maps |
|
123 pre_set_defs = |
117 HEADGOAL (EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp, |
124 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)), |
125 SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ fp_abs_inverses @ abs_inverses @ set_maps @ |
|
126 sum_prod_thms_set0)), |
119 solve_prem_prem_tac ctxt]) (rev kks))); |
127 solve_prem_prem_tac ctxt]) (rev kks))); |
120 |
128 |
121 fun mk_induct_discharge_prem_tac ctxt nn n set_maps pre_set_defs m k kks = |
129 fun mk_induct_discharge_prem_tac ctxt nn n fp_abs_inverses abs_inverses set_maps pre_set_defs m k |
|
130 kks = |
122 let val r = length kks in |
131 let val r = length kks in |
123 HEADGOAL (EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac ctxt, |
132 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 |
133 REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)]) THEN |
125 EVERY [REPEAT_DETERM_N r |
134 EVERY [REPEAT_DETERM_N r |
126 (HEADGOAL (rotate_tac ~1 THEN' dtac meta_mp THEN' rotate_tac 1) THEN prefer_tac 2), |
135 (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, |
136 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] |
137 mk_induct_leverage_prem_prems_tac ctxt nn kks fp_abs_inverses abs_inverses set_maps |
|
138 pre_set_defs] |
129 end; |
139 end; |
130 |
140 |
131 fun mk_induct_tac ctxt nn ns mss kkss ctr_defs ctor_induct' set_maps pre_set_defss = |
141 fun mk_induct_tac ctxt nn ns mss kkss ctr_defs ctor_induct' fp_abs_inverses abs_inverses set_maps |
|
142 pre_set_defss = |
132 let val n = Integer.sum ns in |
143 let val n = Integer.sum ns in |
133 unfold_thms_tac ctxt ctr_defs THEN HEADGOAL (rtac ctor_induct') THEN |
144 unfold_thms_tac ctxt ctr_defs THEN HEADGOAL (rtac ctor_induct') THEN |
134 co_induct_inst_as_projs_tac ctxt 0 THEN |
145 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 |
146 EVERY (map4 (EVERY oooo map3 o |
136 mss (unflat mss (1 upto n)) kkss) |
147 mk_induct_discharge_prem_tac ctxt nn n fp_abs_inverses abs_inverses set_maps) |
|
148 pre_set_defss mss (unflat mss (1 upto n)) kkss) |
137 end; |
149 end; |
138 |
150 |
139 fun mk_coinduct_same_ctr_tac ctxt rel_eqs pre_rel_def dtor_ctor ctr_def discs sels = |
151 fun mk_coinduct_same_ctr_tac ctxt rel_eqs pre_rel_def fp_abs_inverse abs_inverse dtor_ctor ctr_def |
|
152 discs sels = |
140 hyp_subst_tac ctxt THEN' |
153 hyp_subst_tac ctxt THEN' |
141 CONVERSION (hhf_concl_conv |
154 CONVERSION (hhf_concl_conv |
142 (Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv ctr_def))) ctxt) ctxt) THEN' |
155 (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' |
156 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' |
157 SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: fp_abs_inverse :: abs_inverse :: dtor_ctor :: |
|
158 sels @ sum_prod_thms_rel @ @{thms o_apply vimage2p_def})) THEN' |
145 (atac ORELSE' REPEAT o etac conjE THEN' |
159 (atac ORELSE' REPEAT o etac conjE THEN' |
146 full_simp_tac |
160 full_simp_tac |
147 (ss_only (@{thm prod.inject} :: no_refl discs @ rel_eqs @ more_simp_thms) ctxt) THEN' |
161 (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' |
162 REPEAT o etac conjE THEN_MAYBE' REPEAT o hyp_subst_tac ctxt THEN' |
149 REPEAT o (resolve_tac [refl, conjI] ORELSE' atac)); |
163 REPEAT o (resolve_tac [refl, conjI] ORELSE' atac)); |
155 in |
169 in |
156 hyp_subst_tac ctxt THEN' REPEAT o etac conjE THEN' |
170 hyp_subst_tac ctxt THEN' REPEAT o etac conjE THEN' |
157 full_simp_tac (ss_only (refl :: no_refl discs'' @ basic_simp_thms) ctxt) |
171 full_simp_tac (ss_only (refl :: no_refl discs'' @ basic_simp_thms) ctxt) |
158 end; |
172 end; |
159 |
173 |
160 fun mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn kk n pre_rel_def dtor_ctor exhaust ctr_defs |
174 fun mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn kk n pre_rel_def fp_abs_inverse abs_inverse |
161 discss selss = |
175 dtor_ctor exhaust ctr_defs discss selss = |
162 let val ks = 1 upto n in |
176 let val ks = 1 upto n in |
163 EVERY' ([rtac allI, rtac allI, rtac impI, select_prem_tac nn (dtac meta_spec) kk, |
177 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), |
178 dtac meta_spec, dtac meta_mp, atac, rtac exhaust, K (co_induct_inst_as_projs_tac ctxt 0), |
165 hyp_subst_tac ctxt] @ |
179 hyp_subst_tac ctxt] @ |
166 map4 (fn k => fn ctr_def => fn discs => fn sels => |
180 map4 (fn k => fn ctr_def => fn discs => fn sels => |
167 EVERY' ([rtac exhaust, K (co_induct_inst_as_projs_tac ctxt 1)] @ |
181 EVERY' ([rtac exhaust, K (co_induct_inst_as_projs_tac ctxt 1)] @ |
168 map2 (fn k' => fn discs' => |
182 map2 (fn k' => fn discs' => |
169 if k' = k then |
183 if k' = k then |
170 mk_coinduct_same_ctr_tac ctxt rel_eqs' pre_rel_def dtor_ctor ctr_def discs sels |
184 mk_coinduct_same_ctr_tac ctxt rel_eqs' pre_rel_def fp_abs_inverse abs_inverse |
|
185 dtor_ctor ctr_def discs sels |
171 else |
186 else |
172 mk_coinduct_distinct_ctrs_tac ctxt discs discs') ks discss)) ks ctr_defs discss selss) |
187 mk_coinduct_distinct_ctrs_tac ctxt discs discs') ks discss)) ks ctr_defs discss selss) |
173 end; |
188 end; |
174 |
189 |
175 fun mk_coinduct_tac ctxt rel_eqs' nn ns dtor_coinduct' pre_rel_defs dtor_ctors exhausts ctr_defss |
190 fun mk_coinduct_tac ctxt rel_eqs' nn ns dtor_coinduct' pre_rel_defs fp_abs_inverses abs_inverses |
176 discsss selsss = |
191 dtor_ctors exhausts ctr_defss discsss selsss = |
177 HEADGOAL (rtac dtor_coinduct' THEN' |
192 HEADGOAL (rtac dtor_coinduct' THEN' |
178 EVERY' (map8 (mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn) |
193 EVERY' (map10 (mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn) |
179 (1 upto nn) ns pre_rel_defs dtor_ctors exhausts ctr_defss discsss selsss)); |
194 (1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss |
|
195 selsss)); |
180 |
196 |
181 end; |
197 end; |