31 apply(simp add: atom_eqvt) |
30 apply(simp add: atom_eqvt) |
32 apply(simp add: atom_image_cong) |
31 apply(simp add: atom_image_cong) |
33 done |
32 done |
34 |
33 |
35 lemma supp_finite_at_set: |
34 lemma supp_finite_at_set: |
36 fixes S::"('a::at) set" |
|
37 assumes a: "finite S" |
35 assumes a: "finite S" |
38 shows "supp S = atom ` S" |
36 shows "supp S = atom ` S" |
39 apply(rule finite_supp_unique) |
37 proof - |
40 apply(simp add: supports_def) |
38 have fin: "finite (atom ` S)" |
41 apply(rule allI)+ |
39 using a by (simp add: finite_imageI) |
42 apply(rule impI) |
40 have "supp S = supp (atom ` S)" by (rule atom_image_supp) |
43 apply(rule swap_fresh_fresh) |
41 also have "\<dots> = atom ` S" using fin by (simp add: supp_finite_atom_set) |
44 apply(simp add: fresh_def) |
42 finally show "supp S = atom ` S" by simp |
45 apply(simp add: atom_image_supp) |
43 qed |
46 apply(subst supp_finite_atom_set) |
|
47 apply(rule finite_imageI) |
|
48 apply(simp add: a) |
|
49 apply(simp) |
|
50 apply(simp add: fresh_def) |
|
51 apply(simp add: atom_image_supp) |
|
52 apply(subst supp_finite_atom_set) |
|
53 apply(rule finite_imageI) |
|
54 apply(simp add: a) |
|
55 apply(simp) |
|
56 apply(rule finite_imageI) |
|
57 apply(simp add: a) |
|
58 apply(drule swap_set_in) |
|
59 apply(assumption) |
|
60 apply(simp) |
|
61 apply(simp add: image_eqvt) |
|
62 apply(simp add: permute_fun_def) |
|
63 apply(simp add: atom_eqvt) |
|
64 apply(simp add: atom_image_cong) |
|
65 done |
|
66 |
|
67 lemma supp_finite_at_set_aux: |
|
68 fixes S::"('a::at) set" |
|
69 assumes a: "finite S" |
|
70 shows "supp S = atom ` S" |
|
71 proof |
|
72 show "supp S \<subseteq> ((atom::'a::at \<Rightarrow> atom) ` S)" |
|
73 apply(rule supp_is_subset) |
|
74 apply(simp add: supports_def) |
|
75 apply(rule allI)+ |
|
76 apply(rule impI) |
|
77 apply(rule swap_fresh_fresh) |
|
78 apply(simp add: fresh_def) |
|
79 apply(simp add: atom_image_supp) |
|
80 apply(subst supp_finite_atom_set) |
|
81 apply(rule finite_imageI) |
|
82 apply(simp add: a) |
|
83 apply(simp) |
|
84 apply(simp add: fresh_def) |
|
85 apply(simp add: atom_image_supp) |
|
86 apply(subst supp_finite_atom_set) |
|
87 apply(rule finite_imageI) |
|
88 apply(simp add: a) |
|
89 apply(simp) |
|
90 apply(rule finite_imageI) |
|
91 apply(simp add: a) |
|
92 done |
|
93 next |
|
94 have "supp ((atom::'a::at \<Rightarrow> atom) ` S) \<subseteq> supp ((op `) (atom::'a::at \<Rightarrow> atom)) \<union> supp S" |
|
95 by (simp add: supp_fun_app) |
|
96 moreover |
|
97 have "supp ((op `) (atom::'a::at \<Rightarrow> atom)) = {}" |
|
98 apply(rule supp_fun_eqvt) |
|
99 apply(perm_simp) |
|
100 apply(simp) |
|
101 done |
|
102 moreover |
|
103 have "supp ((atom::'a::at \<Rightarrow> atom) ` S) = ((atom::'a::at \<Rightarrow> atom) ` S)" |
|
104 apply(subst supp_finite_atom_set) |
|
105 apply(rule finite_imageI) |
|
106 apply(simp add: a) |
|
107 apply(simp) |
|
108 done |
|
109 ultimately |
|
110 show "((atom::'a::at \<Rightarrow> atom) ` S) \<subseteq> supp S" by simp |
|
111 qed |
|
112 |
|
113 |
44 |
114 lemma supp_at_insert: |
45 lemma supp_at_insert: |
115 fixes S::"('a::at) set" |
46 fixes a::"'a::at_base" |
116 assumes a: "finite S" |
47 assumes a: "finite S" |
117 shows "supp (insert a S) = supp a \<union> supp S" |
48 shows "supp (insert a S) = supp a \<union> supp S" |
118 using a by (simp add: supp_finite_at_set supp_at_base) |
49 using a by (simp add: supp_finite_at_set supp_at_base) |
119 |
|
120 |
50 |
121 section {* A swapping operation for concrete atoms *} |
51 section {* A swapping operation for concrete atoms *} |
122 |
52 |
123 definition |
53 definition |
124 flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')") |
54 flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')") |