equal
deleted
inserted
replaced
2285 unfolding fresh_star_def fresh_def by simp |
2285 unfolding fresh_star_def fresh_def by simp |
2286 then have "(-q + p) \<bullet> x = x" by (simp only: supp_perm_eq) |
2286 then have "(-q + p) \<bullet> x = x" by (simp only: supp_perm_eq) |
2287 then show "p \<bullet> x = q \<bullet> x" |
2287 then show "p \<bullet> x = q \<bullet> x" |
2288 by (metis permute_minus_cancel permute_plus) |
2288 by (metis permute_minus_cancel permute_plus) |
2289 qed |
2289 qed |
|
2290 |
|
2291 text {* disagreement set *} |
|
2292 |
|
2293 definition |
|
2294 ds :: "perm \<Rightarrow> perm \<Rightarrow> atom set" |
|
2295 where |
|
2296 "ds p q = {a::atom. p \<bullet> a \<noteq> q \<bullet> a}" |
|
2297 |
|
2298 lemma ds_fresh: |
|
2299 assumes "ds p q \<sharp>* x" |
|
2300 shows "p \<bullet> x = q \<bullet> x" |
|
2301 using assms |
|
2302 unfolding ds_def fresh_star_def fresh_def |
|
2303 by (auto intro: supp_perm_perm_eq) |
|
2304 |
2290 |
2305 |
2291 lemma atom_set_perm_eq: |
2306 lemma atom_set_perm_eq: |
2292 assumes a: "as \<sharp>* p" |
2307 assumes a: "as \<sharp>* p" |
2293 shows "p \<bullet> as = as" |
2308 shows "p \<bullet> as = as" |
2294 proof - |
2309 proof - |