equal
deleted
inserted
replaced
174 THEN_ALL_NEW |
174 THEN_ALL_NEW |
175 asm_full_simp_tac (HOL_ss addsimps (@{thms permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt)) |
175 asm_full_simp_tac (HOL_ss addsimps (@{thms permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt)) |
176 *} |
176 *} |
177 |
177 |
178 ML {* |
178 ML {* |
179 fun build_alpha_eqvts funs perms simps induct ctxt = |
179 fun build_alpha_eqvts funs perms tac ctxt = |
180 let |
180 let |
181 val pi = Free ("p", @{typ perm}); |
181 val pi = Free ("p", @{typ perm}); |
182 val types = map (domain_type o fastype_of) funs; |
182 val types = map (domain_type o fastype_of) funs; |
183 val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types)); |
183 val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types)); |
184 val indnames2 = Name.variant_list ("p" :: indnames) (Datatype_Prop.make_tnames (map body_type types)); |
184 val indnames2 = Name.variant_list ("p" :: indnames) (Datatype_Prop.make_tnames (map body_type types)); |
186 val args2 = map Free (indnames2 ~~ types); |
186 val args2 = map Free (indnames2 ~~ types); |
187 fun eqvtc ((alpha, perm), (arg, arg2)) = |
187 fun eqvtc ((alpha, perm), (arg, arg2)) = |
188 HOLogic.mk_imp (alpha $ arg $ arg2, |
188 HOLogic.mk_imp (alpha $ arg $ arg2, |
189 (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2))) |
189 (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2))) |
190 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2)))) |
190 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2)))) |
191 fun tac _ = alpha_eqvt_tac induct simps ctxt 1 |
|
192 val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac |
191 val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac |
193 in |
192 in |
194 map (fn x => mp OF [x]) (HOLogic.conj_elims thm) |
193 map (fn x => mp OF [x]) (HOLogic.conj_elims thm) |
195 end |
194 end |
196 *} |
195 *} |