equal
deleted
inserted
replaced
278 |
278 |
279 lemma snd_eqvt[eqvt]: |
279 lemma snd_eqvt[eqvt]: |
280 "p \<bullet> (snd x) = snd (p \<bullet> x)" |
280 "p \<bullet> (snd x) = snd (p \<bullet> x)" |
281 by (cases x) simp |
281 by (cases x) simp |
282 |
282 |
|
283 lemma split_eqvt[eqvt]: |
|
284 shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)" |
|
285 unfolding split_def |
|
286 by (perm_simp) (rule refl) |
|
287 |
283 section {* Units *} |
288 section {* Units *} |
284 |
289 |
285 lemma supp_unit: |
290 lemma supp_unit: |
286 shows "supp () = {}" |
291 shows "supp () = {}" |
287 by (simp add: supp_def) |
292 by (simp add: supp_def) |
384 apply(perm_simp exclude: The) |
389 apply(perm_simp exclude: The) |
385 oops |
390 oops |
386 |
391 |
387 lemma |
392 lemma |
388 fixes P :: "(('b \<Rightarrow> bool) \<Rightarrow> ('b::pt)) \<Rightarrow> ('a::pt)" |
393 fixes P :: "(('b \<Rightarrow> bool) \<Rightarrow> ('b::pt)) \<Rightarrow> ('a::pt)" |
389 shows "(p \<bullet> (P The)) = foo" |
394 shows "p \<bullet> (P The) = foo" |
390 apply(perm_simp exclude: The) |
395 apply(perm_simp exclude: The) |
|
396 oops |
|
397 |
|
398 lemma |
|
399 fixes P :: "('a::pt) \<Rightarrow> ('b::pt) \<Rightarrow> bool" |
|
400 shows "p \<bullet> (\<lambda>(a, b). P a b) = (\<lambda>(a, b). (p \<bullet> P) a b)" |
|
401 apply(perm_simp) |
391 oops |
402 oops |
392 |
403 |
393 thm eqvts |
404 thm eqvts |
394 thm eqvts_raw |
405 thm eqvts_raw |
395 |
406 |