274 in |
274 in |
275 (conj refl_eqs, (conj sym_eqs, conj trans_eqs)) |
275 (conj refl_eqs, (conj sym_eqs, conj trans_eqs)) |
276 end |
276 end |
277 *} |
277 *} |
278 |
278 |
279 |
279 ML {* |
280 end |
280 fun reflp_tac induct inj = |
|
281 rtac induct THEN_ALL_NEW |
|
282 asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW |
|
283 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
|
284 (rtac @{thm exI[of _ "0 :: perm"]} THEN' |
|
285 asm_full_simp_tac (HOL_ss addsimps |
|
286 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) |
|
287 *} |
|
288 |
|
289 ML {* |
|
290 fun symp_tac induct inj eqvt = |
|
291 rtac induct THEN_ALL_NEW |
|
292 asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW |
|
293 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
|
294 (etac @{thm alpha_gen_compose_sym} THEN' eresolve_tac eqvt) |
|
295 *} |
|
296 |
|
297 ML {* |
|
298 fun transp_tac induct alpha_inj term_inj distinct cases eqvt = |
|
299 rtac induct THEN_ALL_NEW |
|
300 (rtac allI THEN' rtac impI THEN' rotate_tac (~1) THEN' |
|
301 eresolve_tac cases) THEN_ALL_NEW |
|
302 ( |
|
303 asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct) THEN' |
|
304 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
|
305 (etac @{thm alpha_gen_compose_trans} THEN' RANGE [atac, eresolve_tac eqvt]) |
|
306 ) |
|
307 *} |
|
308 |
|
309 ML {* |
|
310 fun build_equivps alphas induct alpha_inj term_inj distinct cases eqvt ctxt = |
|
311 let |
|
312 val (reflg, (symg, transg)) = build_alpha_refl_gl alphas |
|
313 fun reflp_tac' _ = reflp_tac induct term_inj 1; |
|
314 fun symp_tac' _ = symp_tac induct alpha_inj eqvt 1; |
|
315 fun transp_tac' _ = transp_tac induct alpha_inj term_inj distinct cases eqvt 1; |
|
316 val reflt = Goal.prove ctxt ["x"] [] reflg reflp_tac'; |
|
317 val symt = Goal.prove ctxt ["x","y"] [] symg symp_tac'; |
|
318 val transt = Goal.prove ctxt ["x","y","z"] [] transg transp_tac'; |
|
319 in |
|
320 (reflt, symt, transt) |
|
321 end |
|
322 *} |
|
323 |
|
324 end |