73 then obtain a :: 'a where "atom a \<notin> X" |
76 then obtain a :: 'a where "atom a \<notin> X" |
74 by auto |
77 by auto |
75 thus ?thesis .. |
78 thus ?thesis .. |
76 qed |
79 qed |
77 |
80 |
|
81 lemma atom_image_cong: |
|
82 fixes X Y::"('a::at_base) set" |
|
83 shows "(atom ` X = atom ` Y) = (X = Y)" |
|
84 apply(rule inj_image_eq_iff) |
|
85 apply(simp add: inj_on_def) |
|
86 done |
|
87 |
|
88 lemma atom_image_supp: |
|
89 "supp S = supp (atom ` S)" |
|
90 apply(simp add: supp_def) |
|
91 apply(simp add: image_eqvt) |
|
92 apply(subst (2) permute_fun_def) |
|
93 apply(simp add: atom_eqvt) |
|
94 apply(simp add: atom_image_cong) |
|
95 done |
|
96 |
|
97 lemma supp_finite_at_set: |
|
98 fixes S::"('a::at) set" |
|
99 assumes a: "finite S" |
|
100 shows "supp S = atom ` S" |
|
101 apply(rule finite_supp_unique) |
|
102 apply(simp add: supports_def) |
|
103 apply(rule allI)+ |
|
104 apply(rule impI) |
|
105 apply(rule swap_fresh_fresh) |
|
106 apply(simp add: fresh_def) |
|
107 apply(simp add: atom_image_supp) |
|
108 apply(subst supp_finite_atom_set) |
|
109 apply(rule finite_imageI) |
|
110 apply(simp add: a) |
|
111 apply(simp) |
|
112 apply(simp add: fresh_def) |
|
113 apply(simp add: atom_image_supp) |
|
114 apply(subst supp_finite_atom_set) |
|
115 apply(rule finite_imageI) |
|
116 apply(simp add: a) |
|
117 apply(simp) |
|
118 apply(rule finite_imageI) |
|
119 apply(simp add: a) |
|
120 apply(drule swap_set_in) |
|
121 apply(assumption) |
|
122 apply(simp) |
|
123 apply(simp add: image_eqvt) |
|
124 apply(simp add: permute_fun_def) |
|
125 apply(simp add: atom_eqvt) |
|
126 apply(simp add: atom_image_cong) |
|
127 done |
|
128 |
|
129 lemma supp_finite_at_set_aux: |
|
130 fixes S::"('a::at) set" |
|
131 assumes a: "finite S" |
|
132 shows "supp S = atom ` S" |
|
133 proof |
|
134 show "supp S \<subseteq> ((atom::'a::at \<Rightarrow> atom) ` S)" |
|
135 apply(rule supp_is_subset) |
|
136 apply(simp add: supports_def) |
|
137 apply(rule allI)+ |
|
138 apply(rule impI) |
|
139 apply(rule swap_fresh_fresh) |
|
140 apply(simp add: fresh_def) |
|
141 apply(simp add: atom_image_supp) |
|
142 apply(subst supp_finite_atom_set) |
|
143 apply(rule finite_imageI) |
|
144 apply(simp add: a) |
|
145 apply(simp) |
|
146 apply(simp add: fresh_def) |
|
147 apply(simp add: atom_image_supp) |
|
148 apply(subst supp_finite_atom_set) |
|
149 apply(rule finite_imageI) |
|
150 apply(simp add: a) |
|
151 apply(simp) |
|
152 apply(rule finite_imageI) |
|
153 apply(simp add: a) |
|
154 done |
|
155 next |
|
156 have "supp ((atom::'a::at \<Rightarrow> atom) ` S) \<subseteq> supp ((op `) (atom::'a::at \<Rightarrow> atom)) \<union> supp S" |
|
157 by (simp add: supp_fun_app) |
|
158 moreover |
|
159 have "supp ((op `) (atom::'a::at \<Rightarrow> atom)) = {}" |
|
160 apply(rule supp_fun_eqvt) |
|
161 apply(perm_simp) |
|
162 apply(simp) |
|
163 done |
|
164 moreover |
|
165 have "supp ((atom::'a::at \<Rightarrow> atom) ` S) = ((atom::'a::at \<Rightarrow> atom) ` S)" |
|
166 apply(subst supp_finite_atom_set) |
|
167 apply(rule finite_imageI) |
|
168 apply(simp add: a) |
|
169 apply(simp) |
|
170 done |
|
171 ultimately |
|
172 show "((atom::'a::at \<Rightarrow> atom) ` S) \<subseteq> supp S" by simp |
|
173 qed |
|
174 |
|
175 |
|
176 lemma supp_at_insert: |
|
177 fixes S::"('a::at) set" |
|
178 assumes a: "finite S" |
|
179 shows "supp (insert a S) = supp a \<union> supp S" |
|
180 using a by (simp add: supp_finite_at_set supp_at_base) |
|
181 |
78 |
182 |
79 section {* A swapping operation for concrete atoms *} |
183 section {* A swapping operation for concrete atoms *} |
80 |
184 |
81 definition |
185 definition |
82 flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')") |
186 flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')") |