equal
deleted
inserted
replaced
403 |
403 |
404 lemma permute_fun_app_eq: |
404 lemma permute_fun_app_eq: |
405 shows "p \<bullet> (f x) = (p \<bullet> f) (p \<bullet> x)" |
405 shows "p \<bullet> (f x) = (p \<bullet> f) (p \<bullet> x)" |
406 unfolding permute_fun_def by simp |
406 unfolding permute_fun_def by simp |
407 |
407 |
|
408 lemma permute_fun_comp: |
|
409 shows "p \<bullet> f = (permute p) o f o (permute (-p))" |
|
410 by (simp add: comp_def permute_fun_def) |
408 |
411 |
409 subsection {* Permutations for booleans *} |
412 subsection {* Permutations for booleans *} |
410 |
413 |
411 instantiation bool :: pt |
414 instantiation bool :: pt |
412 begin |
415 begin |