equal
deleted
inserted
replaced
731 shows "p \<bullet> (f x) \<equiv> (p \<bullet> f) (p \<bullet> x)" |
731 shows "p \<bullet> (f x) \<equiv> (p \<bullet> f) (p \<bullet> x)" |
732 unfolding permute_fun_def by simp |
732 unfolding permute_fun_def by simp |
733 |
733 |
734 lemma eqvt_lambda: |
734 lemma eqvt_lambda: |
735 fixes f :: "'a::pt \<Rightarrow> 'b::pt" |
735 fixes f :: "'a::pt \<Rightarrow> 'b::pt" |
736 shows "p \<bullet> (\<lambda>x. f x) \<equiv> (\<lambda>x. p \<bullet> (f (unpermute p x)))" |
736 shows "p \<bullet> f \<equiv> (\<lambda>x. p \<bullet> (f (unpermute p x)))" |
737 unfolding permute_fun_def unpermute_def by simp |
737 unfolding permute_fun_def unpermute_def by simp |
738 |
738 |
739 lemma eqvt_bound: |
739 lemma eqvt_bound: |
740 shows "p \<bullet> unpermute p x \<equiv> x" |
740 shows "p \<bullet> unpermute p x \<equiv> x" |
741 unfolding unpermute_def by simp |
741 unfolding unpermute_def by simp |