66 EVERY' (map (fn set_map0 => |
66 EVERY' (map (fn set_map0 => |
67 rtac (mk_trans @{thm image_insert} @{thm arg_cong2[of _ _ _ _ insert]}) THEN' |
67 rtac (mk_trans @{thm image_insert} @{thm arg_cong2[of _ _ _ _ insert]}) THEN' |
68 rtac set_map0) set_map0s) THEN' |
68 rtac set_map0) set_map0s) THEN' |
69 rtac @{thm image_empty}) 1; |
69 rtac @{thm image_empty}) 1; |
70 |
70 |
71 fun mk_map_wppull_tac map_id0 map_cong0 map_wpull map_comp0 set_map0s = |
71 fun mk_map_wppull_tac map_id0 map_cong0 map_wpull map_comp set_maps = |
72 if null set_map0s then |
72 if null set_maps then |
73 EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id0, rtac map_id0] 1 |
73 EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id0, rtac map_id0] 1 |
74 else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull}, |
74 else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull}, |
75 REPEAT_DETERM o etac exE, rtac @{thm wpull_wppull}, rtac map_wpull, |
75 REPEAT_DETERM o etac exE, rtac @{thm wpull_wppull}, rtac map_wpull, |
76 REPEAT_DETERM o rtac @{thm wpull_thePull}, rtac ballI, |
76 REPEAT_DETERM o rtac @{thm wpull_thePull}, rtac ballI, |
77 REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac CollectI, |
77 REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac CollectI, |
78 CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans), |
78 CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans), |
79 rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac]) |
79 rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac]) |
80 set_map0s, |
80 set_maps, |
81 CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp0 RS trans), rtac (map_comp0 RS trans), |
81 CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans), |
82 rtac (map_comp0 RS trans RS sym), rtac map_cong0, |
82 rtac (map_comp RS trans RS sym), rtac map_cong0, |
83 REPEAT_DETERM_N (length set_map0s) o EVERY' [rtac (o_apply RS trans), |
83 REPEAT_DETERM_N (length set_maps) o EVERY' [rtac (o_apply RS trans), |
84 rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm, |
84 rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm, |
85 rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1; |
85 rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1; |
86 |
86 |
87 fun mk_rel_Grp_tac rel_OO_Grps map_id0 map_cong0 map_id map_comp0 set_map0s |
87 fun mk_rel_Grp_tac rel_OO_Grps map_id0 map_cong0 map_id map_comp set_maps |
88 {context = ctxt, prems = _} = |
88 {context = ctxt, prems = _} = |
89 let |
89 let |
90 val n = length set_map0s; |
90 val n = length set_maps; |
91 val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac else rtac (hd rel_OO_Grps RS trans); |
91 val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac else rtac (hd rel_OO_Grps RS trans); |
92 in |
92 in |
93 if null set_map0s then |
93 if null set_maps then |
94 unfold_thms_tac ctxt ((map_id0 RS @{thm Grp_UNIV_id}) :: rel_OO_Grps) THEN |
94 unfold_thms_tac ctxt ((map_id0 RS @{thm Grp_UNIV_id}) :: rel_OO_Grps) THEN |
95 rtac @{thm Grp_UNIV_idI[OF refl]} 1 |
95 rtac @{thm Grp_UNIV_idI[OF refl]} 1 |
96 else |
96 else |
97 EVERY' [rel_OO_Grps_tac, rtac @{thm antisym}, rtac @{thm predicate2I}, |
97 EVERY' [rel_OO_Grps_tac, rtac @{thm antisym}, rtac @{thm predicate2I}, |
98 REPEAT_DETERM o |
98 REPEAT_DETERM o |
99 eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}], |
99 eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}], |
100 hyp_subst_tac ctxt, rtac @{thm GrpI}, rtac trans, rtac map_comp0, rtac map_cong0, |
100 hyp_subst_tac ctxt, rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0, |
101 REPEAT_DETERM_N n o EVERY' [rtac @{thm Collect_split_Grp_eqD}, etac @{thm set_mp}, atac], |
101 REPEAT_DETERM_N n o EVERY' [rtac @{thm Collect_split_Grp_eqD}, etac @{thm set_mp}, atac], |
102 rtac CollectI, |
102 rtac CollectI, |
103 CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans), |
103 CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans), |
104 rtac @{thm image_subsetI}, rtac @{thm Collect_split_Grp_inD}, etac @{thm set_mp}, atac]) |
104 rtac @{thm image_subsetI}, rtac @{thm Collect_split_Grp_inD}, etac @{thm set_mp}, atac]) |
105 set_map0s, |
105 set_maps, |
106 rtac @{thm predicate2I}, REPEAT_DETERM o eresolve_tac [@{thm GrpE}, exE, conjE], |
106 rtac @{thm predicate2I}, REPEAT_DETERM o eresolve_tac [@{thm GrpE}, exE, conjE], |
107 hyp_subst_tac ctxt, |
107 hyp_subst_tac ctxt, |
108 rtac @{thm relcomppI}, rtac @{thm conversepI}, |
108 rtac @{thm relcomppI}, rtac @{thm conversepI}, |
109 EVERY' (map2 (fn convol => fn map_id0 => |
109 EVERY' (map2 (fn convol => fn map_id0 => |
110 EVERY' [rtac @{thm GrpI}, rtac (box_equals OF [map_cong0, map_comp0 RS sym, map_id0]), |
110 EVERY' [rtac @{thm GrpI}, rtac (box_equals OF [map_cong0, map_comp RS sym, map_id0]), |
111 REPEAT_DETERM_N n o rtac (convol RS fun_cong), |
111 REPEAT_DETERM_N n o rtac (convol RS fun_cong), |
112 REPEAT_DETERM o eresolve_tac [CollectE, conjE], |
112 REPEAT_DETERM o eresolve_tac [CollectE, conjE], |
113 rtac CollectI, |
113 rtac CollectI, |
114 CONJ_WRAP' (fn thm => |
114 CONJ_WRAP' (fn thm => |
115 EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI}, |
115 EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI}, |
116 rtac @{thm convol_mem_GrpI}, etac set_mp, atac]) |
116 rtac @{thm convol_mem_GrpI}, etac set_mp, atac]) |
117 set_map0s]) |
117 set_maps]) |
118 @{thms fst_convol snd_convol} [map_id, refl])] 1 |
118 @{thms fst_convol snd_convol} [map_id, refl])] 1 |
119 end; |
119 end; |
120 |
120 |
121 fun mk_rel_eq_tac n rel_Grp rel_cong map_id0 = |
121 fun mk_rel_eq_tac n rel_Grp rel_cong map_id0 = |
122 (EVERY' (rtac (rel_cong RS trans) :: replicate n (rtac @{thm eq_alt})) THEN' |
122 (EVERY' (rtac (rel_cong RS trans) :: replicate n (rtac @{thm eq_alt})) THEN' |
135 EVERY' [rel_OO_Grps_tac, rtac @{thm relcompp_mono}, rtac @{thm iffD2[OF conversep_mono]}, |
135 EVERY' [rel_OO_Grps_tac, rtac @{thm relcompp_mono}, rtac @{thm iffD2[OF conversep_mono]}, |
136 rtac @{thm Grp_mono}, rtac in_mono, REPEAT_DETERM o etac @{thm Collect_split_mono}, |
136 rtac @{thm Grp_mono}, rtac in_mono, REPEAT_DETERM o etac @{thm Collect_split_mono}, |
137 rtac @{thm Grp_mono}, rtac in_mono, REPEAT_DETERM o etac @{thm Collect_split_mono}] 1 |
137 rtac @{thm Grp_mono}, rtac in_mono, REPEAT_DETERM o etac @{thm Collect_split_mono}] 1 |
138 end; |
138 end; |
139 |
139 |
140 fun mk_rel_conversep_le_tac rel_OO_Grps rel_eq map_cong0 map_comp0 set_map0s |
140 fun mk_rel_conversep_le_tac rel_OO_Grps rel_eq map_cong0 map_comp set_maps |
141 {context = ctxt, prems = _} = |
141 {context = ctxt, prems = _} = |
142 let |
142 let |
143 val n = length set_map0s; |
143 val n = length set_maps; |
144 val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac |
144 val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac |
145 else rtac (hd rel_OO_Grps RS ord_eq_le_trans) THEN' |
145 else rtac (hd rel_OO_Grps RS ord_eq_le_trans) THEN' |
146 rtac (hd rel_OO_Grps RS sym RS @{thm arg_cong[of _ _ conversep]} RSN (2, ord_le_eq_trans)); |
146 rtac (hd rel_OO_Grps RS sym RS @{thm arg_cong[of _ _ conversep]} RSN (2, ord_le_eq_trans)); |
147 in |
147 in |
148 if null set_map0s then rtac (rel_eq RS @{thm leq_conversepI}) 1 |
148 if null set_maps then rtac (rel_eq RS @{thm leq_conversepI}) 1 |
149 else |
149 else |
150 EVERY' [rel_OO_Grps_tac, rtac @{thm predicate2I}, |
150 EVERY' [rel_OO_Grps_tac, rtac @{thm predicate2I}, |
151 REPEAT_DETERM o |
151 REPEAT_DETERM o |
152 eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}], |
152 eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}], |
153 hyp_subst_tac ctxt, rtac @{thm conversepI}, rtac @{thm relcomppI}, rtac @{thm conversepI}, |
153 hyp_subst_tac ctxt, rtac @{thm conversepI}, rtac @{thm relcomppI}, rtac @{thm conversepI}, |
154 EVERY' (map (fn thm => EVERY' [rtac @{thm GrpI}, rtac sym, rtac trans, |
154 EVERY' (map (fn thm => EVERY' [rtac @{thm GrpI}, rtac sym, rtac trans, |
155 rtac map_cong0, REPEAT_DETERM_N n o rtac thm, |
155 rtac map_cong0, REPEAT_DETERM_N n o rtac thm, |
156 rtac (map_comp0 RS sym), rtac CollectI, |
156 rtac (map_comp RS sym), rtac CollectI, |
157 CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans), |
157 CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans), |
158 etac @{thm flip_pred}]) set_map0s]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1 |
158 etac @{thm flip_pred}]) set_maps]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1 |
159 end; |
159 end; |
160 |
160 |
161 fun mk_rel_conversep_tac le_conversep rel_mono = |
161 fun mk_rel_conversep_tac le_conversep rel_mono = |
162 EVERY' [rtac @{thm antisym}, rtac le_conversep, rtac @{thm xt1(6)}, rtac conversep_shift, |
162 EVERY' [rtac @{thm antisym}, rtac le_conversep, rtac @{thm xt1(6)}, rtac conversep_shift, |
163 rtac le_conversep, rtac @{thm iffD2[OF conversep_mono]}, rtac rel_mono, |
163 rtac le_conversep, rtac @{thm iffD2[OF conversep_mono]}, rtac rel_mono, |
164 REPEAT_DETERM o rtac @{thm eq_refl[OF sym[OF conversep_conversep]]}] 1; |
164 REPEAT_DETERM o rtac @{thm eq_refl[OF sym[OF conversep_conversep]]}] 1; |
165 |
165 |
166 fun mk_rel_OO_tac rel_OO_Grps rel_eq map_cong0 map_wppull map_comp0 set_map0s |
166 fun mk_rel_OO_tac rel_OO_Grps rel_eq map_cong0 map_wppull map_comp set_maps |
167 {context = ctxt, prems = _} = |
167 {context = ctxt, prems = _} = |
168 let |
168 let |
169 val n = length set_map0s; |
169 val n = length set_maps; |
170 fun in_tac nthO_in = rtac CollectI THEN' |
170 fun in_tac nthO_in = rtac CollectI THEN' |
171 CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans), |
171 CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans), |
172 rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_map0s; |
172 rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_maps; |
173 val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac |
173 val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac |
174 else rtac (hd rel_OO_Grps RS trans) THEN' |
174 else rtac (hd rel_OO_Grps RS trans) THEN' |
175 rtac (@{thm arg_cong2[of _ _ _ _ "op OO"]} OF (replicate 2 (hd rel_OO_Grps RS sym)) RSN |
175 rtac (@{thm arg_cong2[of _ _ _ _ "op OO"]} OF (replicate 2 (hd rel_OO_Grps RS sym)) RSN |
176 (2, trans)); |
176 (2, trans)); |
177 in |
177 in |
178 if null set_map0s then rtac (rel_eq RS @{thm eq_OOI}) 1 |
178 if null set_maps then rtac (rel_eq RS @{thm eq_OOI}) 1 |
179 else |
179 else |
180 EVERY' [rel_OO_Grps_tac, rtac @{thm antisym}, rtac @{thm predicate2I}, |
180 EVERY' [rel_OO_Grps_tac, rtac @{thm antisym}, rtac @{thm predicate2I}, |
181 REPEAT_DETERM o |
181 REPEAT_DETERM o |
182 eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}], |
182 eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}], |
183 hyp_subst_tac ctxt, |
183 hyp_subst_tac ctxt, |
184 rtac @{thm relcomppI}, rtac @{thm relcomppI}, rtac @{thm conversepI}, rtac @{thm GrpI}, |
184 rtac @{thm relcomppI}, rtac @{thm relcomppI}, rtac @{thm conversepI}, rtac @{thm GrpI}, |
185 rtac trans, rtac map_comp0, rtac sym, rtac map_cong0, |
185 rtac trans, rtac map_comp, rtac sym, rtac map_cong0, |
186 REPEAT_DETERM_N n o rtac @{thm fst_fstOp}, |
186 REPEAT_DETERM_N n o rtac @{thm fst_fstOp}, |
187 in_tac @{thm fstOp_in}, |
187 in_tac @{thm fstOp_in}, |
188 rtac @{thm GrpI}, rtac trans, rtac map_comp0, rtac map_cong0, |
188 rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0, |
189 REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, |
189 REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, |
190 rtac ballE, rtac subst, |
190 rtac ballE, rtac subst, |
191 rtac @{thm csquare_def}, rtac @{thm csquare_fstOp_sndOp}, atac, etac notE, |
191 rtac @{thm csquare_def}, rtac @{thm csquare_fstOp_sndOp}, atac, etac notE, |
192 etac set_mp, atac], |
192 etac set_mp, atac], |
193 in_tac @{thm fstOp_in}, |
193 in_tac @{thm fstOp_in}, |
194 rtac @{thm relcomppI}, rtac @{thm conversepI}, rtac @{thm GrpI}, |
194 rtac @{thm relcomppI}, rtac @{thm conversepI}, rtac @{thm GrpI}, |
195 rtac trans, rtac map_comp0, rtac map_cong0, |
195 rtac trans, rtac map_comp, rtac map_cong0, |
196 REPEAT_DETERM_N n o rtac o_apply, |
196 REPEAT_DETERM_N n o rtac o_apply, |
197 in_tac @{thm sndOp_in}, |
197 in_tac @{thm sndOp_in}, |
198 rtac @{thm GrpI}, rtac trans, rtac map_comp0, rtac sym, rtac map_cong0, |
198 rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac sym, rtac map_cong0, |
199 REPEAT_DETERM_N n o rtac @{thm snd_sndOp}, |
199 REPEAT_DETERM_N n o rtac @{thm snd_sndOp}, |
200 in_tac @{thm sndOp_in}, |
200 in_tac @{thm sndOp_in}, |
201 rtac @{thm predicate2I}, |
201 rtac @{thm predicate2I}, |
202 REPEAT_DETERM o eresolve_tac [@{thm relcomppE}, @{thm conversepE}, @{thm GrpE}], |
202 REPEAT_DETERM o eresolve_tac [@{thm relcomppE}, @{thm conversepE}, @{thm GrpE}], |
203 hyp_subst_tac ctxt, |
203 hyp_subst_tac ctxt, |
204 rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull, |
204 rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull, |
205 CONJ_WRAP' (K (rtac @{thm wppull_fstOp_sndOp})) set_map0s, |
205 CONJ_WRAP' (K (rtac @{thm wppull_fstOp_sndOp})) set_maps, |
206 etac allE, etac impE, etac conjI, etac conjI, etac sym, |
206 etac allE, etac impE, etac conjI, etac conjI, etac sym, |
207 REPEAT_DETERM o eresolve_tac [bexE, conjE], |
207 REPEAT_DETERM o eresolve_tac [bexE, conjE], |
208 rtac @{thm relcomppI}, rtac @{thm conversepI}, |
208 rtac @{thm relcomppI}, rtac @{thm conversepI}, |
209 EVERY' (map (fn thm => EVERY' [rtac @{thm GrpI}, rtac trans, |
209 EVERY' (map (fn thm => EVERY' [rtac @{thm GrpI}, rtac trans, |
210 rtac trans, rtac map_cong0, REPEAT_DETERM_N n o rtac thm, |
210 rtac trans, rtac map_cong0, REPEAT_DETERM_N n o rtac thm, |
211 rtac (map_comp0 RS sym), atac, atac]) [@{thm fst_fstOp}, @{thm snd_sndOp}])] 1 |
211 rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstOp}, @{thm snd_sndOp}])] 1 |
212 end; |
212 end; |
213 |
213 |
214 fun mk_rel_mono_strong_tac in_rel set_map0s {context = ctxt, prems = _} = |
214 fun mk_rel_mono_strong_tac in_rel set_maps {context = ctxt, prems = _} = |
215 if null set_map0s then atac 1 |
215 if null set_maps then atac 1 |
216 else |
216 else |
217 unfold_tac [in_rel] ctxt THEN |
217 unfold_tac [in_rel] ctxt THEN |
218 REPEAT_DETERM (eresolve_tac [exE, CollectE, conjE] 1) THEN |
218 REPEAT_DETERM (eresolve_tac [exE, CollectE, conjE] 1) THEN |
219 hyp_subst_tac ctxt 1 THEN |
219 hyp_subst_tac ctxt 1 THEN |
220 unfold_tac set_map0s ctxt THEN |
220 unfold_tac set_maps ctxt THEN |
221 EVERY' [rtac exI, rtac @{thm conjI[OF CollectI conjI[OF refl refl]]}, |
221 EVERY' [rtac exI, rtac @{thm conjI[OF CollectI conjI[OF refl refl]]}, |
222 CONJ_WRAP' (K (etac @{thm Collect_split_mono_strong} THEN' atac)) set_map0s] 1; |
222 CONJ_WRAP' (K (etac @{thm Collect_split_mono_strong} THEN' atac)) set_maps] 1; |
223 |
223 |
224 fun mk_map_transfer_tac rel_mono in_rel set_maps map_cong0 map_comp |
224 fun mk_map_transfer_tac rel_mono in_rel set_maps map_cong0 map_comp |
225 {context = ctxt, prems = _} = |
225 {context = ctxt, prems = _} = |
226 let |
226 let |
227 val n = length set_maps; |
227 val n = length set_maps; |