1186 apply(subst (2) permute_fun_def) |
1186 apply(subst (2) permute_fun_def) |
1187 apply(simp add: atom_eqvt) |
1187 apply(simp add: atom_eqvt) |
1188 apply(simp add: atom_image_cong) |
1188 apply(simp add: atom_image_cong) |
1189 done |
1189 done |
1190 |
1190 |
1191 lemma supp_finite_at_set: |
1191 lemma supp_finite_set_at_base: |
1192 assumes a: "finite S" |
1192 assumes a: "finite S" |
1193 shows "supp S = atom ` S" |
1193 shows "supp S = atom ` S" |
1194 proof - |
1194 proof - |
1195 have fin: "finite (atom ` S)" |
1195 have fin: "finite (atom ` S)" |
1196 using a by (simp add: finite_imageI) |
1196 using a by (simp add: finite_imageI) |
1197 have "supp S = supp (atom ` S)" by (rule atom_image_supp) |
1197 have "supp S = supp (atom ` S)" by (rule atom_image_supp) |
1198 also have "\<dots> = atom ` S" using fin by (simp add: supp_finite_atom_set) |
1198 also have "\<dots> = atom ` S" using fin by (simp add: supp_finite_atom_set) |
1199 finally show "supp S = atom ` S" by simp |
1199 finally show "supp S = atom ` S" by simp |
1200 qed |
1200 qed |
1201 |
1201 |
1202 lemma supp_at_insert: |
1202 lemma supp_at_base_insert: |
1203 fixes a::"'a::at_base" |
1203 fixes a::"'a::at_base" |
1204 assumes a: "finite S" |
1204 assumes a: "finite S" |
1205 shows "supp (insert a S) = supp a \<union> supp S" |
1205 shows "supp (insert a S) = supp a \<union> supp S" |
1206 using a by (simp add: supp_finite_at_set supp_at_base) |
1206 using a by (simp add: supp_finite_set_at_base supp_at_base) |
1207 |
1207 |
1208 section {* library functions for the nominal infrastructure *} |
1208 section {* library functions for the nominal infrastructure *} |
1209 use "nominal_library.ML" |
1209 use "nominal_library.ML" |
1210 |
1210 |
1211 end |
1211 end |