equal
deleted
inserted
replaced
144 apply (erule exE) |
144 apply (erule exE) |
145 apply (rule_tac x="pi \<bullet> pia" in exI) |
145 apply (rule_tac x="pi \<bullet> pia" in exI) |
146 by auto |
146 by auto |
147 |
147 |
148 ML {* |
148 ML {* |
149 fun indtac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct |
149 fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct |
|
150 *} |
|
151 ML {* |
150 fun all_eqvts ctxt = |
152 fun all_eqvts ctxt = |
151 Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt |
153 Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt |
152 val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) |
154 val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) |
153 *} |
155 *} |
154 |
156 |
159 setmksimps (mksimps []) |
161 setmksimps (mksimps []) |
160 *} |
162 *} |
161 |
163 |
162 ML {* |
164 ML {* |
163 fun alpha_eqvt_tac induct simps ctxt = |
165 fun alpha_eqvt_tac induct simps ctxt = |
164 indtac induct THEN_ALL_NEW |
166 ind_tac induct THEN_ALL_NEW |
165 simp_tac ((mk_minimal_ss ctxt) addsimps simps) THEN_ALL_NEW |
167 simp_tac ((mk_minimal_ss ctxt) addsimps simps) THEN_ALL_NEW |
166 REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conjs THEN_ALL_NEW |
168 REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conjs THEN_ALL_NEW |
167 asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW |
169 asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW |
168 asm_full_simp_tac (HOL_ss addsimps |
170 asm_full_simp_tac (HOL_ss addsimps |
169 @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alpha_gen}) THEN_ALL_NEW |
171 @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alpha_gen}) THEN_ALL_NEW |