7 imports Nominal2_Base |
7 imports Nominal2_Base |
8 Nominal2_Eqvt |
8 Nominal2_Eqvt |
9 uses ("nominal_atoms.ML") |
9 uses ("nominal_atoms.ML") |
10 begin |
10 begin |
11 |
11 |
12 section {* Concrete atom types *} |
12 section {* Infrastructure for concrete atom types *} |
13 |
13 |
14 text {* |
|
15 Class @{text at_base} allows types containing multiple sorts of atoms. |
|
16 Class @{text at} only allows types with a single sort. |
|
17 *} |
|
18 |
|
19 lemma atom_image_cong: |
|
20 shows "(atom ` X = atom ` Y) = (X = Y)" |
|
21 apply(rule inj_image_eq_iff) |
|
22 apply(simp add: inj_on_def) |
|
23 done |
|
24 |
|
25 lemma atom_image_supp: |
|
26 "supp S = supp (atom ` S)" |
|
27 apply(simp add: supp_def) |
|
28 apply(simp add: image_eqvt) |
|
29 apply(subst (2) permute_fun_def) |
|
30 apply(simp add: atom_eqvt) |
|
31 apply(simp add: atom_image_cong) |
|
32 done |
|
33 |
|
34 lemma supp_finite_at_set: |
|
35 assumes a: "finite S" |
|
36 shows "supp S = atom ` S" |
|
37 proof - |
|
38 have fin: "finite (atom ` S)" |
|
39 using a by (simp add: finite_imageI) |
|
40 have "supp S = supp (atom ` S)" by (rule atom_image_supp) |
|
41 also have "\<dots> = atom ` S" using fin by (simp add: supp_finite_atom_set) |
|
42 finally show "supp S = atom ` S" by simp |
|
43 qed |
|
44 |
|
45 lemma supp_at_insert: |
|
46 fixes a::"'a::at_base" |
|
47 assumes a: "finite S" |
|
48 shows "supp (insert a S) = supp a \<union> supp S" |
|
49 using a by (simp add: supp_finite_at_set supp_at_base) |
|
50 |
14 |
51 section {* A swapping operation for concrete atoms *} |
15 section {* A swapping operation for concrete atoms *} |
52 |
16 |
53 definition |
17 definition |
54 flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')") |
18 flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')") |