equal
deleted
inserted
replaced
270 assumes permute_plus [simp]: "(p + q) \<bullet> x = p \<bullet> (q \<bullet> x)" |
270 assumes permute_plus [simp]: "(p + q) \<bullet> x = p \<bullet> (q \<bullet> x)" |
271 begin |
271 begin |
272 |
272 |
273 lemma permute_diff [simp]: |
273 lemma permute_diff [simp]: |
274 shows "(p - q) \<bullet> x = p \<bullet> - q \<bullet> x" |
274 shows "(p - q) \<bullet> x = p \<bullet> - q \<bullet> x" |
275 unfolding diff_minus by simp |
275 using permute_plus [of p "- q" x] by simp |
276 |
276 |
277 lemma permute_minus_cancel [simp]: |
277 lemma permute_minus_cancel [simp]: |
278 shows "p \<bullet> - p \<bullet> x = x" |
278 shows "p \<bullet> - p \<bullet> x = x" |
279 and "- p \<bullet> p \<bullet> x = x" |
279 and "- p \<bullet> p \<bullet> x = x" |
280 unfolding permute_plus [symmetric] by simp_all |
280 unfolding permute_plus [symmetric] by simp_all |
363 "p \<bullet> q = p + q - p" |
363 "p \<bullet> q = p + q - p" |
364 |
364 |
365 instance |
365 instance |
366 apply default |
366 apply default |
367 apply (simp add: permute_perm_def) |
367 apply (simp add: permute_perm_def) |
368 apply (simp add: permute_perm_def diff_minus minus_add add_assoc) |
368 apply (simp add: permute_perm_def algebra_simps) |
369 done |
369 done |
370 |
370 |
371 end |
371 end |
372 |
372 |
373 lemma permute_self: |
373 lemma permute_self: |
374 shows "p \<bullet> p = p" |
374 shows "p \<bullet> p = p" |
375 unfolding permute_perm_def |
375 unfolding permute_perm_def |
376 by (simp add: diff_minus add_assoc) |
376 by (simp add: add_assoc) |
377 |
377 |
378 lemma pemute_minus_self: |
378 lemma pemute_minus_self: |
379 shows "- p \<bullet> p = p" |
379 shows "- p \<bullet> p = p" |
380 unfolding permute_perm_def |
380 unfolding permute_perm_def |
381 by (simp add: diff_minus add_assoc) |
381 by (simp add: add_assoc) |
382 |
382 |
383 |
383 |
384 subsection {* Permutations for functions *} |
384 subsection {* Permutations for functions *} |
385 |
385 |
386 instantiation "fun" :: (pt, pt) pt |
386 instantiation "fun" :: (pt, pt) pt |
868 |
868 |
869 lemma uminus_eqvt [eqvt]: |
869 lemma uminus_eqvt [eqvt]: |
870 fixes p q::"perm" |
870 fixes p q::"perm" |
871 shows "p \<bullet> (- q) = - (p \<bullet> q)" |
871 shows "p \<bullet> (- q) = - (p \<bullet> q)" |
872 unfolding permute_perm_def |
872 unfolding permute_perm_def |
873 by (simp add: diff_minus minus_add add_assoc) |
873 by (simp add: diff_add_eq_diff_diff_swap) |
|
874 |
874 |
875 |
875 subsubsection {* Equivariance of Logical Operators *} |
876 subsubsection {* Equivariance of Logical Operators *} |
876 |
877 |
877 lemma eq_eqvt [eqvt]: |
878 lemma eq_eqvt [eqvt]: |
878 shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)" |
879 shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)" |