equal
deleted
inserted
replaced
289 lemma fresh_unit: |
289 lemma fresh_unit: |
290 shows "a \<sharp> ()" |
290 shows "a \<sharp> ()" |
291 by (simp add: fresh_def supp_unit) |
291 by (simp add: fresh_def supp_unit) |
292 |
292 |
293 |
293 |
294 section {* additional lemmas *} |
294 section {* additional eqvt lemmas *} |
295 |
|
296 ML {* Nominal_ThmDecls.is_eqvt @{context} @{term "Pair"} *} |
|
297 |
295 |
298 lemmas [eqvt] = |
296 lemmas [eqvt] = |
299 imp_eqvt [folded induct_implies_def] |
297 imp_eqvt [folded induct_implies_def] |
300 |
298 |
301 (* nominal *) |
299 (* nominal *) |
302 supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt |
300 supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt |
303 |
301 |
304 (* datatypes *) |
302 (* datatypes *) |
305 permute_prod.simps Pair_eqvt permute_list.simps |
303 Pair_eqvt permute_list.simps |
306 |
304 |
307 (* sets *) |
305 (* sets *) |
308 image_eqvt |
306 image_eqvt |
309 |
307 |
310 |
308 |
311 section {* Test cases *} |
309 section {* Test cases *} |
312 |
310 |
313 |
311 |
314 declare [[trace_eqvt = true]] |
312 declare [[trace_eqvt = false]] |
|
313 (* declare [[trace_eqvt = true]] *) |
315 |
314 |
316 lemma |
315 lemma |
317 fixes B::"'a::pt" |
316 fixes B::"'a::pt" |
318 shows "p \<bullet> (B = C)" |
317 shows "p \<bullet> (B = C)" |
319 apply(perm_simp) |
318 apply(perm_simp) |
389 thm eqvts_raw |
388 thm eqvts_raw |
390 |
389 |
391 ML {* Nominal_ThmDecls.is_eqvt @{context} @{term "supp"} *} |
390 ML {* Nominal_ThmDecls.is_eqvt @{context} @{term "supp"} *} |
392 |
391 |
393 |
392 |
394 section {* |
393 section {* Automatic equivariance procedure for inductive definitions *} |
395 Automatic equivariance procedure for inductive definitions *} |
|
396 |
394 |
397 use "nominal_eqvt.ML" |
395 use "nominal_eqvt.ML" |
398 |
396 |
399 end |
397 end |