equal
deleted
inserted
replaced
20 where |
20 where |
21 "as \<sharp>* x \<equiv> \<forall>a \<in> as. a \<sharp> x" |
21 "as \<sharp>* x \<equiv> \<forall>a \<in> as. a \<sharp> x" |
22 |
22 |
23 lemma fresh_star_prod: |
23 lemma fresh_star_prod: |
24 fixes as::"atom set" |
24 fixes as::"atom set" |
25 shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" |
25 shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" |
26 by (auto simp add: fresh_star_def fresh_Pair) |
26 by (auto simp add: fresh_star_def fresh_Pair) |
27 |
27 |
28 lemma fresh_star_union: |
28 lemma fresh_star_union: |
29 shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)" |
29 shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)" |
30 by (auto simp add: fresh_star_def) |
30 by (auto simp add: fresh_star_def) |
65 by (simp add: fresh_plus_perm) |
65 by (simp add: fresh_plus_perm) |
66 |
66 |
67 lemma fresh_star_permute_iff: |
67 lemma fresh_star_permute_iff: |
68 shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x" |
68 shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x" |
69 unfolding fresh_star_def |
69 unfolding fresh_star_def |
70 by (metis mem_permute_iff permute_minus_cancel fresh_permute_iff) |
70 by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff) |
71 |
71 |
72 lemma fresh_star_eqvt[eqvt]: |
72 lemma fresh_star_eqvt[eqvt]: |
73 shows "(p \<bullet> (as \<sharp>* x)) = (p \<bullet> as) \<sharp>* (p \<bullet> x)" |
73 shows "(p \<bullet> (as \<sharp>* x)) = (p \<bullet> as) \<sharp>* (p \<bullet> x)" |
74 unfolding fresh_star_def |
74 unfolding fresh_star_def |
75 unfolding Ball_def |
75 unfolding Ball_def |
164 have a: "{a} \<sharp>* x" unfolding fresh_star_def by (simp add: b) |
164 have a: "{a} \<sharp>* x" unfolding fresh_star_def by (simp add: b) |
165 obtain p where p1: "(p \<bullet> {a}) \<sharp>* c" and p2: "supp x \<sharp>* p" |
165 obtain p where p1: "(p \<bullet> {a}) \<sharp>* c" and p2: "supp x \<sharp>* p" |
166 using at_set_avoiding2[of "{a}" "c" "x"] assms a by blast |
166 using at_set_avoiding2[of "{a}" "c" "x"] assms a by blast |
167 have c: "(p \<bullet> a) \<sharp> c" using p1 |
167 have c: "(p \<bullet> a) \<sharp> c" using p1 |
168 unfolding fresh_star_def Ball_def |
168 unfolding fresh_star_def Ball_def |
169 by (erule_tac x="p \<bullet> a" in allE) (simp add: eqvts) |
169 by(erule_tac x="p \<bullet> a" in allE) (simp add: permute_set_eq) |
170 hence "p \<bullet> a \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast |
170 hence "p \<bullet> a \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast |
171 then show "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p" by blast |
171 then show "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p" by blast |
172 qed |
172 qed |
173 |
173 |
174 |
174 |
479 apply(assumption) |
479 apply(assumption) |
480 done |
480 done |
481 |
481 |
482 lemma Union_supports_set: |
482 lemma Union_supports_set: |
483 shows "(\<Union>x \<in> S. supp x) supports S" |
483 shows "(\<Union>x \<in> S. supp x) supports S" |
484 apply(simp add: supports_def fresh_def[symmetric]) |
484 proof - |
485 apply(rule allI)+ |
485 { fix a b |
486 apply(rule impI) |
486 have "\<forall>x \<in> S. (a \<rightleftharpoons> b) \<bullet> x = x \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> S = S" |
487 apply(erule conjE) |
487 unfolding permute_set_eq by force |
488 apply(simp add: permute_set_eq) |
488 } |
489 apply(auto) |
489 then show "(\<Union>x \<in> S. supp x) supports S" |
490 apply(subgoal_tac "(a \<rightleftharpoons> b) \<bullet> xa = xa")(*A*) |
490 unfolding supports_def |
491 apply(simp) |
491 by (simp add: fresh_def[symmetric] swap_fresh_fresh) |
492 apply(rule swap_fresh_fresh) |
492 qed |
493 apply(force) |
|
494 apply(force) |
|
495 apply(rule_tac x="x" in exI) |
|
496 apply(simp) |
|
497 apply(rule sym) |
|
498 apply(rule swap_fresh_fresh) |
|
499 apply(auto) |
|
500 done |
|
501 |
493 |
502 lemma Union_of_fin_supp_sets: |
494 lemma Union_of_fin_supp_sets: |
503 fixes S::"('a::fs set)" |
495 fixes S::"('a::fs set)" |
504 assumes fin: "finite S" |
496 assumes fin: "finite S" |
505 shows "finite (\<Union>x\<in>S. supp x)" |
497 shows "finite (\<Union>x\<in>S. supp x)" |
510 assumes fin: "finite S" |
502 assumes fin: "finite S" |
511 shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S" |
503 shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S" |
512 proof - |
504 proof - |
513 have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)" |
505 have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)" |
514 apply(rule supp_finite_atom_set[symmetric]) |
506 apply(rule supp_finite_atom_set[symmetric]) |
515 apply(rule Union_of_fin_supp_sets) |
507 apply(rule Union_of_fin_supp_sets[OF fin]) |
516 apply(rule fin) |
|
517 done |
508 done |
518 also have "\<dots> \<subseteq> supp S" |
509 also have "\<dots> \<subseteq> supp S" |
519 apply(rule supp_subset_fresh) |
510 apply(rule supp_subset_fresh) |
520 apply(simp add: Union_fresh) |
511 apply(simp add: Union_fresh) |
521 done |
512 done |