equal
deleted
inserted
replaced
410 |
410 |
411 lemma Not_eqvt: |
411 lemma Not_eqvt: |
412 shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))" |
412 shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))" |
413 by (simp add: permute_bool_def) |
413 by (simp add: permute_bool_def) |
414 |
414 |
|
415 lemma permute_boolE: |
|
416 fixes P::"bool" |
|
417 shows "p \<bullet> P \<Longrightarrow> P" |
|
418 by (simp add: permute_bool_def) |
|
419 |
|
420 lemma permute_boolI: |
|
421 fixes P::"bool" |
|
422 shows "P \<Longrightarrow> p \<bullet> P" |
|
423 by(simp add: permute_bool_def) |
415 |
424 |
416 subsection {* Permutations for sets *} |
425 subsection {* Permutations for sets *} |
417 |
426 |
418 lemma permute_set_eq: |
427 lemma permute_set_eq: |
419 fixes x::"'a::pt" |
428 fixes x::"'a::pt" |