equal
deleted
inserted
replaced
76 |
76 |
77 |
77 |
78 ML {* |
78 ML {* |
79 fun fvbv_rsp_tac induct fvbv_simps = |
79 fun fvbv_rsp_tac induct fvbv_simps = |
80 ((((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
80 ((((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
81 (TRY o rtac @{thm TrueI})) THEN_ALL_NEW asm_full_simp_tac |
81 (TRY o rtac @{thm TrueI})) THEN_ALL_NEW |
82 (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps))) |
82 asm_full_simp_tac |
|
83 (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)) |
|
84 THEN_ALL_NEW (REPEAT o eresolve_tac [conjE, exE] THEN' |
|
85 asm_full_simp_tac |
|
86 (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)))) |
83 *} |
87 *} |
84 |
88 |
85 ML {* |
89 ML {* |
86 fun constr_rsp_tac inj rsp equivps = |
90 fun constr_rsp_tac inj rsp equivps = |
87 let |
91 let |
156 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2)))) |
160 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2)))) |
157 fun tac _ = (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
161 fun tac _ = (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
158 ( |
162 ( |
159 (asm_full_simp_tac (HOL_ss addsimps |
163 (asm_full_simp_tac (HOL_ss addsimps |
160 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) |
164 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) |
161 THEN_ALL_NEW (etac @{thm exi[of _ _ "p"]} THEN' |
165 THEN_ALL_NEW (REPEAT o etac conjE THEN' etac @{thm exi[of _ _ "p"]} THEN' |
162 REPEAT o etac conjE THEN' |
166 REPEAT o etac conjE THEN' |
163 (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW |
167 (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW |
164 (asm_full_simp_tac HOL_ss) THEN_ALL_NEW |
168 (asm_full_simp_tac HOL_ss) THEN_ALL_NEW |
165 (etac @{thm alpha_gen_compose_eqvt[of _ _ _ _ "p"]}) THEN_ALL_NEW |
169 (etac @{thm alpha_gen_compose_eqvt[of _ _ _ _ "p"]}) THEN_ALL_NEW |
166 (asm_full_simp_tac (HOL_ss addsimps |
170 (asm_full_simp_tac (HOL_ss addsimps |