equal
deleted
inserted
replaced
2271 have "p1 \<bullet> x = x" "p2 \<bullet> x = x" by fact+ |
2271 have "p1 \<bullet> x = x" "p2 \<bullet> x = x" by fact+ |
2272 then show "(p1 + p2) \<bullet> x = x" by simp |
2272 then show "(p1 + p2) \<bullet> x = x" by simp |
2273 qed |
2273 qed |
2274 qed |
2274 qed |
2275 |
2275 |
2276 |
|
2277 lemma supp_perm_perm_eq: |
2276 lemma supp_perm_perm_eq: |
2278 assumes a: "\<forall>a \<in> supp x. p \<bullet> a = q \<bullet> a" |
2277 assumes a: "\<forall>a \<in> supp x. p \<bullet> a = q \<bullet> a" |
2279 shows "p \<bullet> x = q \<bullet> x" |
2278 shows "p \<bullet> x = q \<bullet> x" |
2280 proof - |
2279 proof - |
2281 from a have "\<forall>a \<in> supp x. (-q + p) \<bullet> a = a" by simp |
2280 from a have "\<forall>a \<in> supp x. (-q + p) \<bullet> a = a" by simp |
2289 qed |
2288 qed |
2290 |
2289 |
2291 text {* disagreement set *} |
2290 text {* disagreement set *} |
2292 |
2291 |
2293 definition |
2292 definition |
2294 ds :: "perm \<Rightarrow> perm \<Rightarrow> atom set" |
2293 dset :: "perm \<Rightarrow> perm \<Rightarrow> atom set" |
2295 where |
2294 where |
2296 "ds p q = {a::atom. p \<bullet> a \<noteq> q \<bullet> a}" |
2295 "dset p q = {a::atom. p \<bullet> a \<noteq> q \<bullet> a}" |
2297 |
2296 |
2298 lemma ds_fresh: |
2297 lemma ds_fresh: |
2299 assumes "ds p q \<sharp>* x" |
2298 assumes "dset p q \<sharp>* x" |
2300 shows "p \<bullet> x = q \<bullet> x" |
2299 shows "p \<bullet> x = q \<bullet> x" |
2301 using assms |
2300 using assms |
2302 unfolding ds_def fresh_star_def fresh_def |
2301 unfolding dset_def fresh_star_def fresh_def |
2303 by (auto intro: supp_perm_perm_eq) |
2302 by (auto intro: supp_perm_perm_eq) |
2304 |
2303 |
2305 |
|
2306 lemma atom_set_perm_eq: |
2304 lemma atom_set_perm_eq: |
2307 assumes a: "as \<sharp>* p" |
2305 assumes a: "as \<sharp>* p" |
2308 shows "p \<bullet> as = as" |
2306 shows "p \<bullet> as = as" |
2309 proof - |
2307 proof - |
2310 from a have "supp p \<subseteq> {a. a \<notin> as}" |
2308 from a have "supp p \<subseteq> {a. a \<notin> as}" |