equal
deleted
inserted
replaced
233 apply(simp add: expand_fun_eq permute_fun_def) |
233 apply(simp add: expand_fun_eq permute_fun_def) |
234 apply(subst permute_eqvt) |
234 apply(subst permute_eqvt) |
235 apply(simp) |
235 apply(simp) |
236 done |
236 done |
237 |
237 |
|
238 |
238 section {* Equivariance automation *} |
239 section {* Equivariance automation *} |
239 |
240 |
240 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *} |
241 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *} |
241 |
242 |
242 use "nominal_thmdecls.ML" |
243 use "nominal_thmdecls.ML" |
243 setup "Nominal_ThmDecls.setup" |
244 setup "Nominal_ThmDecls.setup" |
244 |
245 |
|
246 ML {* Thm.full_rules *} |
245 lemmas [eqvt] = |
247 lemmas [eqvt] = |
246 (* connectives *) |
248 (* connectives *) |
247 eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt |
249 eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt |
248 True_eqvt False_eqvt ex_eqvt all_eqvt ex1_eqvt |
250 True_eqvt False_eqvt ex_eqvt all_eqvt ex1_eqvt |
249 imp_eqvt [folded induct_implies_def] |
251 imp_eqvt [folded induct_implies_def] |
367 lemma "p \<bullet> (THE x. P x) = foo" |
369 lemma "p \<bullet> (THE x. P x) = foo" |
368 apply(perm_strict_simp exclude: The) |
370 apply(perm_strict_simp exclude: The) |
369 apply(perm_simp exclude: The) |
371 apply(perm_simp exclude: The) |
370 oops |
372 oops |
371 |
373 |
|
374 |
|
375 thm eqvts |
|
376 thm eqvts_raw |
|
377 |
|
378 ML {* |
|
379 Nominal_ThmDecls.is_eqvt @{context} @{term "supp"} |
|
380 *} |
|
381 |
|
382 |
372 (* automatic equivariance procedure for |
383 (* automatic equivariance procedure for |
373 inductive definitions *) |
384 inductive definitions *) |
374 use "nominal_eqvt.ML" |
385 use "nominal_eqvt.ML" |
375 |
386 |
376 end |
387 end |