278 |
278 |
279 ML {* |
279 ML {* |
280 fun reflp_tac induct inj = |
280 fun reflp_tac induct inj = |
281 rtac induct THEN_ALL_NEW |
281 rtac induct THEN_ALL_NEW |
282 asm_full_simp_tac (HOL_ss addsimps inj) 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 |
283 TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW |
284 (rtac @{thm exI[of _ "0 :: perm"]} THEN' |
284 (rtac @{thm exI[of _ "0 :: perm"]} THEN' |
285 asm_full_simp_tac (HOL_ss addsimps |
285 asm_full_simp_tac (HOL_ss addsimps |
286 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) |
286 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) |
287 *} |
287 *} |
288 |
288 |
289 ML {* |
289 ML {* |
290 fun symp_tac induct inj eqvt = |
290 fun symp_tac induct inj eqvt = |
291 ((rtac @{thm impI} THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
291 ((rtac @{thm impI} THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
292 asm_full_simp_tac (HOL_ss addsimps inj) 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 |
293 TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW |
294 (etac @{thm alpha_gen_compose_sym} THEN' eresolve_tac eqvt) |
294 (etac @{thm alpha_gen_compose_sym} THEN' eresolve_tac eqvt) |
295 *} |
295 *} |
296 |
296 |
297 ML {* |
297 ML {* |
298 fun imp_elim_tac case_rules = |
298 fun imp_elim_tac case_rules = |
321 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt = |
321 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt = |
322 ((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
322 ((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
323 (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW |
323 (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW |
324 ( |
324 ( |
325 asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct) THEN' |
325 asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct) THEN' |
326 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
326 TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW |
327 (etac @{thm alpha_gen_compose_trans} THEN' RANGE [atac, eresolve_tac eqvt]) |
327 (etac @{thm alpha_gen_compose_trans} THEN' RANGE [atac, eresolve_tac eqvt]) |
328 ) |
328 ) |
329 *} |
329 *} |
330 |
330 |
331 lemma transp_aux: |
331 lemma transp_aux: |
334 by blast |
334 by blast |
335 |
335 |
336 ML {* |
336 ML {* |
337 fun equivp_tac reflps symps transps = |
337 fun equivp_tac reflps symps transps = |
338 simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def}) |
338 simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def}) |
339 THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN' |
339 THEN' rtac conjI THEN' rtac allI THEN' |
340 resolve_tac reflps THEN' |
340 resolve_tac reflps THEN' |
341 rtac @{thm conjI} THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' |
341 rtac conjI THEN' rtac allI THEN' rtac allI THEN' |
342 resolve_tac symps THEN' |
342 resolve_tac symps THEN' |
343 rtac @{thm transp_aux} THEN' resolve_tac transps |
343 rtac @{thm transp_aux} THEN' resolve_tac transps |
344 *} |
344 *} |
345 |
345 |
346 ML {* |
346 ML {* |