106 | gen_tac _ _ = error "mk_rotate_eq_tac: different lists"; |
85 | gen_tac _ _ = error "mk_rotate_eq_tac: different lists"; |
107 in |
86 in |
108 gen_tac |
87 gen_tac |
109 end; |
88 end; |
110 |
89 |
111 fun mk_Card_order_tac card_order = |
90 fun mk_pred_unfold_tac pred_def pred_defs rel_unfold {context = ctxt, prems = _} = |
112 (rtac conjE THEN' |
91 Local_Defs.unfold_tac ctxt (@{thm mem_Collect_eq_split} :: pred_def :: pred_defs) THEN |
113 rtac @{thm card_order_on_Card_order} THEN' |
92 rtac rel_unfold 1; |
114 rtac card_order THEN' |
|
115 atac) 1; |
|
116 |
|
117 fun mk_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply}; |
|
118 fun mk_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp]; |
|
119 fun mk_set_natural' set_natural = set_natural RS @{thm pointfreeE}; |
|
120 fun mk_in_mono_tac n = if n = 0 then rtac @{thm subset_UNIV} 1 |
|
121 else (rtac subsetI THEN' |
|
122 rtac CollectI) 1 THEN |
|
123 REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN |
|
124 REPEAT_DETERM_N (n - 1) |
|
125 ((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN |
|
126 (etac subset_trans THEN' atac) 1; |
|
127 |
|
128 fun mk_map_wpull_tac comp_in_alt inner_map_wpulls outer_map_wpull = |
|
129 (rtac (@{thm wpull_cong} OF (replicate 3 comp_in_alt)) THEN' rtac outer_map_wpull) 1 THEN |
|
130 WRAP (fn thm => rtac thm 1 THEN REPEAT_DETERM (atac 1)) (K all_tac) inner_map_wpulls all_tac THEN |
|
131 TRY (REPEAT_DETERM (atac 1 ORELSE rtac @{thm wpull_id} 1)); |
|
132 |
|
133 fun mk_collect_set_natural_tac ctxt set_naturals = |
|
134 substs_tac ctxt (@{thms collect_o image_insert image_empty} @ set_naturals) 1 THEN rtac refl 1; |
|
135 |
|
136 fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms)); |
|
137 |
93 |
138 fun mk_map_comp_id_tac map_comp = |
94 fun mk_map_comp_id_tac map_comp = |
139 (rtac trans THEN' rtac map_comp) 1 THEN |
95 (rtac trans THEN' rtac map_comp) 1 THEN |
140 REPEAT_DETERM (stac @{thm o_id} 1) THEN |
96 REPEAT_DETERM (stac @{thm o_id} 1) THEN |
141 rtac refl 1; |
97 rtac refl 1; |
142 |
98 |
|
99 fun mk_map_cong_tac m map_cong {context = ctxt, prems = _} = |
|
100 EVERY' [rtac mp, rtac map_cong, |
|
101 CONJ_WRAP' (K (rtac ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1; |
|
102 |
143 fun mk_map_congL_tac passive map_cong map_id' = |
103 fun mk_map_congL_tac passive map_cong map_id' = |
144 (rtac trans THEN' rtac map_cong THEN' EVERY' (replicate passive (rtac refl))) 1 THEN |
104 (rtac trans THEN' rtac map_cong THEN' EVERY' (replicate passive (rtac refl))) 1 THEN |
145 REPEAT_DETERM (EVERY' [rtac trans, etac bspec, atac, rtac sym, rtac @{thm id_apply}] 1) THEN |
105 REPEAT_DETERM (EVERY' [rtac trans, etac bspec, atac, rtac sym, rtac @{thm id_apply}] 1) THEN |
146 rtac map_id' 1; |
106 rtac map_id' 1; |
147 |
107 |
148 fun mk_map_wppull_tac map_id map_cong map_wpull map_comp set_naturals = |
|
149 if null set_naturals then |
|
150 EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id, rtac map_id] 1 |
|
151 else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull}, |
|
152 REPEAT_DETERM o etac exE, rtac @{thm wpull_wppull}, rtac map_wpull, |
|
153 REPEAT_DETERM o rtac @{thm wpull_thePull}, rtac ballI, |
|
154 REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac CollectI, |
|
155 CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), |
|
156 rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac]) |
|
157 set_naturals, |
|
158 CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans), |
|
159 rtac (map_comp RS trans RS sym), rtac map_cong, |
|
160 REPEAT_DETERM_N (length set_naturals) o EVERY' [rtac (o_apply RS trans), |
|
161 rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm, |
|
162 rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1; |
|
163 |
|
164 fun mk_rel_Gr_tac rel_def map_id map_cong map_wpull in_cong map_id' map_comp set_naturals |
|
165 {context = ctxt, prems = _} = |
|
166 let |
|
167 val n = length set_naturals; |
|
168 in |
|
169 if null set_naturals then |
|
170 Local_Defs.unfold_tac ctxt [rel_def] THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1 |
|
171 else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN |
|
172 EVERY' [rtac equalityI, rtac subsetI, |
|
173 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], |
|
174 REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, |
|
175 REPEAT_DETERM o etac conjE, hyp_subst_tac, |
|
176 rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, |
|
177 rtac sym, rtac trans, rtac map_comp, rtac map_cong, |
|
178 REPEAT_DETERM_N n o EVERY' [dtac @{thm set_rev_mp}, atac, |
|
179 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac, |
|
180 rtac (o_apply RS trans), rtac (@{thm fst_conv} RS arg_cong RS trans), |
|
181 rtac (@{thm snd_conv} RS sym)], |
|
182 rtac CollectI, |
|
183 CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), |
|
184 rtac @{thm image_subsetI}, dtac @{thm set_rev_mp}, atac, |
|
185 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac, |
|
186 stac @{thm fst_conv}, atac]) set_naturals, |
|
187 rtac @{thm subrelI}, etac CollectE, REPEAT_DETERM o eresolve_tac [exE, conjE], |
|
188 REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, |
|
189 REPEAT_DETERM o etac conjE, hyp_subst_tac, |
|
190 rtac allE, rtac subst, rtac @{thm wpull_def}, rtac map_wpull, |
|
191 REPEAT_DETERM_N n o rtac @{thm wpull_Gr}, etac allE, etac impE, rtac conjI, atac, |
|
192 rtac conjI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI, |
|
193 CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), |
|
194 rtac @{thm image_mono}, atac]) set_naturals, |
|
195 rtac sym, rtac map_id', REPEAT_DETERM o eresolve_tac [bexE, conjE], |
|
196 rtac @{thm relcompI}, rtac @{thm converseI}, |
|
197 REPEAT_DETERM_N 2 o EVERY' [rtac CollectI, rtac exI, |
|
198 rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, etac sym, |
|
199 etac @{thm set_rev_mp}, rtac equalityD1, rtac in_cong, |
|
200 REPEAT_DETERM_N n o rtac @{thm Gr_def}]] 1 |
|
201 end; |
|
202 |
|
203 fun mk_rel_Id_tac n rel_Gr map_id {context = ctxt, prems = _} = |
|
204 Local_Defs.unfold_tac ctxt [rel_Gr, @{thm Id_alt}] THEN |
|
205 subst_tac ctxt [map_id] 1 THEN |
|
206 (if n = 0 then rtac refl 1 |
|
207 else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]}, |
|
208 rtac equalityI, rtac @{thm subset_UNIV}, rtac subsetI, rtac CollectI, |
|
209 CONJ_WRAP' (K (rtac @{thm subset_UNIV})) (1 upto n), rtac refl] 1); |
|
210 |
|
211 fun mk_rel_mono_tac rel_def in_mono {context = ctxt, prems = _} = |
|
212 Local_Defs.unfold_tac ctxt [rel_def] THEN |
|
213 EVERY' [rtac @{thm relcomp_mono}, rtac @{thm iffD2[OF converse_mono]}, |
|
214 rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac, |
|
215 rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1; |
|
216 |
|
217 fun mk_map_cong_tac m map_cong {context = ctxt, prems = _} = |
|
218 EVERY' [rtac mp, rtac map_cong, |
|
219 CONJ_WRAP' (K (rtac ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1; |
|
220 |
|
221 fun mk_rel_converse_le_tac rel_def rel_Id map_cong map_comp set_naturals |
|
222 {context = ctxt, prems = _} = |
|
223 let |
|
224 val n = length set_naturals; |
|
225 in |
|
226 if null set_naturals then |
|
227 Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1 |
|
228 else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN |
|
229 EVERY' [rtac @{thm subrelI}, |
|
230 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], |
|
231 REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, |
|
232 REPEAT_DETERM o etac conjE, hyp_subst_tac, rtac @{thm converseI}, |
|
233 rtac @{thm relcompI}, rtac @{thm converseI}, |
|
234 EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI, |
|
235 rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, rtac trans, |
|
236 rtac map_cong, REPEAT_DETERM_N n o rtac thm, |
|
237 rtac (map_comp RS sym), rtac CollectI, |
|
238 CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), |
|
239 etac @{thm flip_rel}]) set_naturals]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1 |
|
240 end; |
|
241 |
|
242 fun mk_rel_converse_tac le_converse = |
|
243 EVERY' [rtac equalityI, rtac le_converse, rtac @{thm xt1(6)}, rtac @{thm converse_shift}, |
|
244 rtac le_converse, REPEAT_DETERM o stac @{thm converse_converse}, rtac subset_refl] 1; |
|
245 |
|
246 fun mk_rel_O_tac rel_def rel_Id map_cong map_wppull map_comp set_naturals |
|
247 {context = ctxt, prems = _} = |
|
248 let |
|
249 val n = length set_naturals; |
|
250 fun in_tac nthO_in = rtac CollectI THEN' |
|
251 CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), |
|
252 rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_naturals; |
|
253 in |
|
254 if null set_naturals then Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1 |
|
255 else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN |
|
256 EVERY' [rtac equalityI, rtac @{thm subrelI}, |
|
257 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], |
|
258 REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, |
|
259 REPEAT_DETERM o etac conjE, hyp_subst_tac, |
|
260 rtac @{thm relcompI}, rtac @{thm relcompI}, rtac @{thm converseI}, |
|
261 rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, |
|
262 rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong, |
|
263 REPEAT_DETERM_N n o rtac @{thm fst_fstO}, |
|
264 in_tac @{thm fstO_in}, |
|
265 rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, |
|
266 rtac sym, rtac trans, rtac map_comp, rtac map_cong, |
|
267 REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, rtac ballE, rtac subst, |
|
268 rtac @{thm csquare_def}, rtac @{thm csquare_fstO_sndO}, atac, etac notE, |
|
269 etac set_mp, atac], |
|
270 in_tac @{thm fstO_in}, |
|
271 rtac @{thm relcompI}, rtac @{thm converseI}, |
|
272 rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, |
|
273 rtac sym, rtac trans, rtac map_comp, rtac map_cong, |
|
274 REPEAT_DETERM_N n o rtac o_apply, |
|
275 in_tac @{thm sndO_in}, |
|
276 rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, |
|
277 rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong, |
|
278 REPEAT_DETERM_N n o rtac @{thm snd_sndO}, |
|
279 in_tac @{thm sndO_in}, |
|
280 rtac @{thm subrelI}, |
|
281 REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}], |
|
282 REPEAT_DETERM o eresolve_tac [exE, conjE], |
|
283 REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, |
|
284 REPEAT_DETERM o etac conjE, hyp_subst_tac, |
|
285 rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull, |
|
286 CONJ_WRAP' (K (rtac @{thm wppull_fstO_sndO})) set_naturals, |
|
287 etac allE, etac impE, etac conjI, etac conjI, atac, |
|
288 REPEAT_DETERM o eresolve_tac [bexE, conjE], |
|
289 rtac @{thm relcompI}, rtac @{thm converseI}, |
|
290 EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI, |
|
291 rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, rtac sym, rtac trans, |
|
292 rtac trans, rtac map_cong, REPEAT_DETERM_N n o rtac thm, |
|
293 rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstO}, @{thm snd_sndO}])] 1 |
|
294 end; |
|
295 |
|
296 fun mk_in_rel_tac rel_def m {context = ctxt, prems = _} = |
|
297 let |
|
298 val ls' = replicate (Int.max (1, m)) (); |
|
299 in |
|
300 Local_Defs.unfold_tac ctxt (rel_def :: |
|
301 @{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN |
|
302 EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, |
|
303 rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl, |
|
304 REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI, rtac conjI, |
|
305 REPEAT_DETERM_N 2 o EVERY' [rtac exI, rtac conjI, etac @{thm conjI[OF refl sym]}, |
|
306 CONJ_WRAP' (K atac) ls']] 1 |
|
307 end; |
|
308 |
|
309 fun mk_pred_unfold_tac pred_def pred_defs rel_unfold {context = ctxt, prems = _} = |
|
310 Local_Defs.unfold_tac ctxt (@{thm mem_Collect_eq_split} :: pred_def :: pred_defs) THEN |
|
311 rtac rel_unfold 1; |
|
312 |
|
313 end; |
108 end; |