equal
deleted
inserted
replaced
35 unfolding permute_plus [symmetric] add_flip_cancel by simp |
35 unfolding permute_plus [symmetric] add_flip_cancel by simp |
36 |
36 |
37 lemma permute_flip_cancel2 [simp]: "(a \<leftrightarrow> b) \<bullet> (b \<leftrightarrow> a) \<bullet> x = x" |
37 lemma permute_flip_cancel2 [simp]: "(a \<leftrightarrow> b) \<bullet> (b \<leftrightarrow> a) \<bullet> x = x" |
38 by (simp add: flip_commute) |
38 by (simp add: flip_commute) |
39 |
39 |
40 lemma flip_eqvt: |
40 lemma flip_eqvt[eqvt]: |
41 fixes a b c::"'a::at_base" |
41 fixes a b c::"'a::at_base" |
42 shows "p \<bullet> (a \<leftrightarrow> b) = (p \<bullet> a \<leftrightarrow> p \<bullet> b)" |
42 shows "p \<bullet> (a \<leftrightarrow> b) = (p \<bullet> a \<leftrightarrow> p \<bullet> b)" |
43 unfolding flip_def |
43 unfolding flip_def |
44 by (simp add: swap_eqvt atom_eqvt) |
44 by (simp add: swap_eqvt atom_eqvt) |
45 |
45 |