equal
deleted
inserted
replaced
323 |
323 |
324 ML {* |
324 ML {* |
325 fun symp_tac induct inj eqvt = |
325 fun symp_tac induct inj eqvt = |
326 (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
326 (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
327 asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW |
327 asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW |
328 (etac @{thm exi_neg} THEN' REPEAT o etac conjE THEN' |
328 (REPEAT o etac conjE THEN' etac @{thm exi_neg} THEN' REPEAT o etac conjE THEN' |
329 (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW |
329 (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW |
330 (asm_full_simp_tac HOL_ss) THEN_ALL_NEW |
330 (asm_full_simp_tac HOL_ss) THEN_ALL_NEW |
331 (etac @{thm alpha_gen_compose_sym} THEN' |
331 (etac @{thm alpha_gen_compose_sym} THEN' |
332 (asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: eqvt))))) |
332 (asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: eqvt))))) |
333 *} |
333 *} |
365 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt = |
365 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt = |
366 ((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
366 ((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
367 (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW |
367 (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW |
368 ( |
368 ( |
369 asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct) |
369 asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct) |
370 THEN_ALL_NEW (etac @{thm exi_sum} THEN' RANGE [atac]) THEN_ALL_NEW |
370 THEN_ALL_NEW (REPEAT o etac conjE THEN' etac @{thm exi_sum} THEN' RANGE [atac]) THEN_ALL_NEW |
371 (REPEAT o etac conjE THEN' (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) |
371 (REPEAT o etac conjE THEN' (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) |
372 THEN_ALL_NEW (asm_full_simp_tac HOL_ss) THEN_ALL_NEW |
372 THEN_ALL_NEW (asm_full_simp_tac HOL_ss) THEN_ALL_NEW |
373 (etac @{thm alpha_gen_compose_trans} THEN' RANGE[atac]) THEN_ALL_NEW |
373 (etac @{thm alpha_gen_compose_trans} THEN' RANGE[atac]) THEN_ALL_NEW |
374 (asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: eqvt))) |
374 (asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: eqvt))) |
375 ) |
375 ) |