equal
deleted
inserted
replaced
143 |
143 |
144 ML {* |
144 ML {* |
145 fun alpha_bn_rsp_tac simps res exhausts a ctxt = |
145 fun alpha_bn_rsp_tac simps res exhausts a ctxt = |
146 rtac allI THEN_ALL_NEW |
146 rtac allI THEN_ALL_NEW |
147 case_rules_tac ctxt a exhausts THEN_ALL_NEW |
147 case_rules_tac ctxt a exhausts THEN_ALL_NEW |
148 asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW |
148 asm_full_simp_tac (HOL_ss addsimps simps addsimps @{thms alphas}) THEN_ALL_NEW |
149 TRY o REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<and>"]}) THEN_ALL_NEW |
149 TRY o REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<and>"]}) THEN_ALL_NEW |
150 TRY o eresolve_tac res THEN_ALL_NEW |
150 TRY o eresolve_tac res THEN_ALL_NEW |
151 asm_full_simp_tac (HOL_ss addsimps simps); |
151 asm_full_simp_tac (HOL_ss addsimps simps) |
152 *} |
152 *} |
153 |
153 |
154 |
154 |
155 ML {* |
155 ML {* |
156 fun build_alpha_bn_rsp_gl a alphas alpha_bn ctxt = |
156 fun build_alpha_bn_rsp_gl a alphas alpha_bn ctxt = |
184 in |
184 in |
185 ([alpha_bn $ l $ r], ctxt) |
185 ([alpha_bn $ l $ r], ctxt) |
186 end |
186 end |
187 *} |
187 *} |
188 |
188 |
|
189 lemma exi_same: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q p) \<Longrightarrow> \<exists>pi. Q pi" |
|
190 by auto |
|
191 |
189 ML {* |
192 ML {* |
190 fun prove_alpha_alphabn alphas ind simps alpha_bns ctxt = |
193 fun prove_alpha_alphabn alphas ind simps alpha_bns ctxt = |
191 prove_by_rel_induct alphas build_alpha_alpha_bn_gl ind |
194 prove_by_rel_induct alphas build_alpha_alpha_bn_gl ind |
192 (fn _ => asm_full_simp_tac (HOL_ss addsimps simps)) alpha_bns ctxt |
195 (fn _ => asm_full_simp_tac (HOL_ss addsimps simps addsimps @{thms alphas}) |
|
196 THEN_ALL_NEW split_conj_tac THEN_ALL_NEW (TRY o etac @{thm exi_same}) |
|
197 THEN_ALL_NEW asm_full_simp_tac HOL_ss) alpha_bns ctxt |
193 *} |
198 *} |
194 |
199 |
195 ML {* |
200 ML {* |
196 fun build_rsp_gl alphas fnctn ctxt = |
201 fun build_rsp_gl alphas fnctn ctxt = |
197 let |
202 let |