--- a/Nominal-General/Nominal2_Eqvt.thy Fri May 07 12:28:11 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy Sun May 09 11:37:19 2010 +0100
@@ -280,6 +280,11 @@
"p \<bullet> (snd x) = snd (p \<bullet> x)"
by (cases x) simp
+lemma split_eqvt[eqvt]:
+ shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)"
+ unfolding split_def
+ by (perm_simp) (rule refl)
+
section {* Units *}
lemma supp_unit:
@@ -386,10 +391,16 @@
lemma
fixes P :: "(('b \<Rightarrow> bool) \<Rightarrow> ('b::pt)) \<Rightarrow> ('a::pt)"
- shows "(p \<bullet> (P The)) = foo"
+ shows "p \<bullet> (P The) = foo"
apply(perm_simp exclude: The)
oops
+lemma
+ fixes P :: "('a::pt) \<Rightarrow> ('b::pt) \<Rightarrow> bool"
+ shows "p \<bullet> (\<lambda>(a, b). P a b) = (\<lambda>(a, b). (p \<bullet> P) a b)"
+apply(perm_simp)
+oops
+
thm eqvts
thm eqvts_raw