133 (asm_full_simp_tac (HOL_ss addsimps |
133 (asm_full_simp_tac (HOL_ss addsimps |
134 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))) 1 |
134 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))) 1 |
135 *} |
135 *} |
136 |
136 |
137 ML {* |
137 ML {* |
|
138 fun perm_arg arg = |
|
139 let |
|
140 val ty = fastype_of arg |
|
141 in |
|
142 Const (@{const_name permute}, @{typ perm} --> ty --> ty) |
|
143 end |
|
144 *} |
|
145 |
|
146 |
|
147 ML {* |
138 fun build_eqvts bind funs tac ctxt = |
148 fun build_eqvts bind funs tac ctxt = |
139 let |
149 let |
140 val pi = Free ("p", @{typ perm}); |
150 val pi = Free ("p", @{typ perm}); |
141 val types = map (domain_type o fastype_of) funs; |
151 val types = map (domain_type o fastype_of) funs; |
142 val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames types); |
152 val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames types); |
143 val args = map Free (indnames ~~ types); |
153 val args = map Free (indnames ~~ types); |
144 val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"} |
154 val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"} |
145 fun perm_arg arg = Const (@{const_name permute}, @{typ perm} --> fastype_of arg --> fastype_of arg) |
|
146 fun eqvtc (fnctn, arg) = |
155 fun eqvtc (fnctn, arg) = |
147 HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg))) |
156 HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg))) |
148 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ args))) |
157 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ args))) |
149 val thm = Goal.prove ctxt ("p" :: indnames) [] gl (tac indnames) |
158 val thm = Goal.prove ctxt ("p" :: indnames) [] gl (tac indnames) |
150 val thms = HOLogic.conj_elims thm |
159 val thms = HOLogic.conj_elims thm |
179 THEN_ALL_NEW |
188 THEN_ALL_NEW |
180 asm_full_simp_tac (HOL_ss addsimps (@{thms permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt)) |
189 asm_full_simp_tac (HOL_ss addsimps (@{thms permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt)) |
181 *} |
190 *} |
182 |
191 |
183 ML {* |
192 ML {* |
184 fun build_alpha_eqvts funs perms tac ctxt = |
193 fun build_alpha_eqvt alpha names = |
185 let |
194 let |
186 val pi = Free ("p", @{typ perm}); |
195 val pi = Free ("p", @{typ perm}); |
187 val types = map (domain_type o fastype_of) funs; |
196 val (tys, _) = strip_type (fastype_of alpha) |
188 val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types)); |
197 val indnames = Name.variant_list names (Datatype_Prop.make_tnames (map body_type tys)); |
189 val indnames2 = Name.variant_list ("p" :: indnames) (Datatype_Prop.make_tnames (map body_type types)); |
198 val args = map Free (indnames ~~ tys); |
190 val args = map Free (indnames ~~ types); |
199 val perm_args = map (fn x => perm_arg x $ pi $ x) args |
191 val args2 = map Free (indnames2 ~~ types); |
200 in |
192 fun eqvtc ((alpha, perm), (arg, arg2)) = |
201 (HOLogic.mk_imp (list_comb (alpha, args), list_comb (alpha, perm_args)), indnames @ names) |
193 HOLogic.mk_imp (alpha $ arg $ arg2, |
202 end |
194 (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2))) |
203 *} |
195 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2)))) |
204 |
196 val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac |
205 ML {* fold_map build_alpha_eqvt *} |
|
206 |
|
207 ML {* |
|
208 fun build_alpha_eqvts funs tac ctxt = |
|
209 let |
|
210 val (gls, names) = fold_map build_alpha_eqvt funs ["p"] |
|
211 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj gls) |
|
212 val thm = Goal.prove ctxt names [] gl tac |
197 in |
213 in |
198 map (fn x => mp OF [x]) (HOLogic.conj_elims thm) |
214 map (fn x => mp OF [x]) (HOLogic.conj_elims thm) |
199 end |
215 end |
200 *} |
216 *} |
201 |
217 |