17 |
18 |
18 class at_base = pt + |
19 class at_base = pt + |
19 fixes atom :: "'a \<Rightarrow> atom" |
20 fixes atom :: "'a \<Rightarrow> atom" |
20 assumes atom_eq_iff [simp]: "atom a = atom b \<longleftrightarrow> a = b" |
21 assumes atom_eq_iff [simp]: "atom a = atom b \<longleftrightarrow> a = b" |
21 assumes atom_eqvt: "p \<bullet> (atom a) = atom (p \<bullet> a)" |
22 assumes atom_eqvt: "p \<bullet> (atom a) = atom (p \<bullet> a)" |
|
23 |
|
24 declare atom_eqvt[eqvt] |
22 |
25 |
23 class at = at_base + |
26 class at = at_base + |
24 assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)" |
27 assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)" |
25 |
28 |
26 lemma supp_at_base: |
29 lemma supp_at_base: |
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_at_insert: |
|
130 fixes S::"('a::at) set" |
|
131 assumes a: "finite S" |
|
132 shows "supp (insert a S) = supp a \<union> supp S" |
|
133 using a |
|
134 apply (simp add: supp_finite_at_set) |
|
135 apply (simp add: supp_at_base) |
|
136 done |
78 |
137 |
79 section {* A swapping operation for concrete atoms *} |
138 section {* A swapping operation for concrete atoms *} |
80 |
139 |
81 definition |
140 definition |
82 flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')") |
141 flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')") |