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 |
|
150 fun all_eqvts ctxt = |
|
151 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) |
|
153 *} |
|
154 |
|
155 ML {* |
|
156 fun mk_minimal_ss ctxt = |
|
157 Simplifier.context ctxt empty_ss |
|
158 setsubgoaler asm_simp_tac |
|
159 setmksimps (mksimps []) |
|
160 *} |
|
161 |
|
162 ML {* |
|
163 fun alpha_eqvt_tac induct simps ctxt = |
|
164 indtac induct THEN_ALL_NEW |
|
165 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 |
|
167 asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW |
|
168 asm_full_simp_tac (HOL_ss addsimps |
|
169 @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alpha_gen}) THEN_ALL_NEW |
|
170 (split_conjs THEN_ALL_NEW TRY o resolve_tac |
|
171 @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]}) |
|
172 THEN_ALL_NEW |
|
173 asm_full_simp_tac (HOL_ss addsimps (@{thms permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt)) |
|
174 *} |
|
175 |
|
176 ML {* |
149 fun build_alpha_eqvts funs perms simps induct ctxt = |
177 fun build_alpha_eqvts funs perms simps induct ctxt = |
150 let |
178 let |
151 val pi = Free ("p", @{typ perm}); |
179 val pi = Free ("p", @{typ perm}); |
152 val types = map (domain_type o fastype_of) funs; |
180 val types = map (domain_type o fastype_of) funs; |
153 val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types)); |
181 val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types)); |
156 val args2 = map Free (indnames2 ~~ types); |
184 val args2 = map Free (indnames2 ~~ types); |
157 fun eqvtc ((alpha, perm), (arg, arg2)) = |
185 fun eqvtc ((alpha, perm), (arg, arg2)) = |
158 HOLogic.mk_imp (alpha $ arg $ arg2, |
186 HOLogic.mk_imp (alpha $ arg $ arg2, |
159 (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2))) |
187 (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2))) |
160 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2)))) |
188 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2)))) |
161 fun tac _ = (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
189 fun tac _ = alpha_eqvt_tac induct simps ctxt 1 |
162 ( |
|
163 (asm_full_simp_tac (HOL_ss addsimps |
|
164 ((Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps))) |
|
165 THEN_ALL_NEW (REPEAT o etac conjE THEN' etac @{thm exi[of _ _ "p"]} THEN' |
|
166 REPEAT o etac conjE THEN' |
|
167 (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW |
|
168 (asm_full_simp_tac HOL_ss) THEN_ALL_NEW |
|
169 (etac @{thm alpha_gen_compose_eqvt[of _ _ _ _ "p"]}) THEN_ALL_NEW |
|
170 (asm_full_simp_tac (HOL_ss addsimps |
|
171 ((Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps))))) 1 |
|
172 val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac |
190 val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac |
173 in |
191 in |
174 map (fn x => mp OF [x]) (HOLogic.conj_elims thm) |
192 map (fn x => mp OF [x]) (HOLogic.conj_elims thm) |
175 end |
193 end |
176 *} |
194 *} |