equal
deleted
inserted
replaced
1623 |
1623 |
1624 subsection {* Equivariance Predicate @{text eqvt} and @{text eqvt_at}*} |
1624 subsection {* Equivariance Predicate @{text eqvt} and @{text eqvt_at}*} |
1625 |
1625 |
1626 definition |
1626 definition |
1627 "eqvt f \<equiv> \<forall>p. p \<bullet> f = f" |
1627 "eqvt f \<equiv> \<forall>p. p \<bullet> f = f" |
|
1628 |
|
1629 lemma eqvt_boolI: |
|
1630 fixes f::"bool" |
|
1631 shows "eqvt f" |
|
1632 unfolding eqvt_def by (simp add: permute_bool_def) |
|
1633 |
1628 |
1634 |
1629 text {* equivariance of a function at a given argument *} |
1635 text {* equivariance of a function at a given argument *} |
1630 |
1636 |
1631 definition |
1637 definition |
1632 "eqvt_at f x \<equiv> \<forall>p. p \<bullet> (f x) = f (p \<bullet> x)" |
1638 "eqvt_at f x \<equiv> \<forall>p. p \<bullet> (f x) = f (p \<bullet> x)" |