28 lemma supp_at_base: |
28 lemma supp_at_base: |
29 fixes a::"'a::at_base" |
29 fixes a::"'a::at_base" |
30 shows "supp a = {atom a}" |
30 shows "supp a = {atom a}" |
31 by (simp add: supp_atom [symmetric] supp_def atom_eqvt) |
31 by (simp add: supp_atom [symmetric] supp_def atom_eqvt) |
32 |
32 |
33 lemma fresh_at: |
33 lemma fresh_at_base: |
34 shows "a \<sharp> b \<longleftrightarrow> a \<noteq> atom b" |
34 shows "a \<sharp> b \<longleftrightarrow> a \<noteq> atom b" |
35 unfolding fresh_def by (simp add: supp_at_base) |
35 unfolding fresh_def by (simp add: supp_at_base) |
36 |
36 |
37 instance at_base < fs |
37 instance at_base < fs |
38 proof qed (simp add: supp_at_base) |
38 proof qed (simp add: supp_at_base) |
39 |
|
40 |
39 |
41 lemma at_base_infinite [simp]: |
40 lemma at_base_infinite [simp]: |
42 shows "infinite (UNIV :: 'a::at_base set)" (is "infinite ?U") |
41 shows "infinite (UNIV :: 'a::at_base set)" (is "infinite ?U") |
43 proof |
42 proof |
44 obtain a :: 'a where "True" by auto |
43 obtain a :: 'a where "True" by auto |
155 |
154 |
156 text {* |
155 text {* |
157 New atom types are defined as subtypes of @{typ atom}. |
156 New atom types are defined as subtypes of @{typ atom}. |
158 *} |
157 *} |
159 |
158 |
160 lemma exists_eq_sort: |
159 lemma exists_eq_simple_sort: |
161 shows "\<exists>a. a \<in> {a. sort_of a = s}" |
160 shows "\<exists>a. a \<in> {a. sort_of a = s}" |
162 by (rule_tac x="Atom s 0" in exI, simp) |
161 by (rule_tac x="Atom s 0" in exI, simp) |
163 |
162 |
|
163 lemma exists_eq_sort: |
|
164 shows "\<exists>a. a \<in> {a. sort_of a \<in> range sort_fun}" |
|
165 by (rule_tac x="Atom (sort_fun x) y" in exI, simp) |
|
166 |
164 lemma at_base_class: |
167 lemma at_base_class: |
165 fixes s :: atom_sort |
168 fixes sort_fun :: "'b \<Rightarrow>atom_sort" |
166 fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a" |
169 fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a" |
167 assumes type: "type_definition Rep Abs {a. P (sort_of a)}" |
170 assumes type: "type_definition Rep Abs {a. sort_of a \<in> range sort_fun}" |
168 assumes atom_def: "\<And>a. atom a = Rep a" |
171 assumes atom_def: "\<And>a. atom a = Rep a" |
169 assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)" |
172 assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)" |
170 shows "OFCLASS('a, at_base_class)" |
173 shows "OFCLASS('a, at_base_class)" |
171 proof |
174 proof |
172 interpret type_definition Rep Abs "{a. P (sort_of a)}" by (rule type) |
175 interpret type_definition Rep Abs "{a. sort_of a \<in> range sort_fun}" by (rule type) |
173 have sort_of_Rep: "\<And>a. P (sort_of (Rep a))" using Rep by simp |
176 have sort_of_Rep: "\<And>a. sort_of (Rep a) \<in> range sort_fun" using Rep by simp |
174 fix a b :: 'a and p p1 p2 :: perm |
177 fix a b :: 'a and p p1 p2 :: perm |
175 show "0 \<bullet> a = a" |
178 show "0 \<bullet> a = a" |
176 unfolding permute_def by (simp add: Rep_inverse) |
179 unfolding permute_def by (simp add: Rep_inverse) |
177 show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a" |
180 show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a" |
178 unfolding permute_def by (simp add: Abs_inverse sort_of_Rep) |
181 unfolding permute_def by (simp add: Abs_inverse sort_of_Rep) |
180 unfolding atom_def by (simp add: Rep_inject) |
183 unfolding atom_def by (simp add: Rep_inject) |
181 show "p \<bullet> atom a = atom (p \<bullet> a)" |
184 show "p \<bullet> atom a = atom (p \<bullet> a)" |
182 unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep) |
185 unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep) |
183 qed |
186 qed |
184 |
187 |
|
188 (* |
185 lemma at_class: |
189 lemma at_class: |
186 fixes s :: atom_sort |
190 fixes s :: atom_sort |
187 fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a" |
191 fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a" |
188 assumes type: "type_definition Rep Abs {a. sort_of a = s}" |
192 assumes type: "type_definition Rep Abs {a. sort_of a \<in> range (\<lambda>x::unit. s)}" |
189 assumes atom_def: "\<And>a. atom a = Rep a" |
193 assumes atom_def: "\<And>a. atom a = Rep a" |
190 assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)" |
194 assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)" |
191 shows "OFCLASS('a, at_class)" |
195 shows "OFCLASS('a, at_class)" |
192 proof |
196 proof |
193 interpret type_definition Rep Abs "{a. sort_of a = s}" by (rule type) |
197 interpret type_definition Rep Abs "{a. sort_of a \<in> range (\<lambda>x::unit. s)}" by (rule type) |
194 have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by simp |
198 have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by (simp add: image_def) |
195 fix a b :: 'a and p p1 p2 :: perm |
199 fix a b :: 'a and p p1 p2 :: perm |
196 show "0 \<bullet> a = a" |
200 show "0 \<bullet> a = a" |
197 unfolding permute_def by (simp add: Rep_inverse) |
201 unfolding permute_def by (simp add: Rep_inverse) |
198 show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a" |
202 show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a" |
199 unfolding permute_def by (simp add: Abs_inverse sort_of_Rep) |
203 unfolding permute_def by (simp add: Abs_inverse sort_of_Rep) |
202 show "atom a = atom b \<longleftrightarrow> a = b" |
206 show "atom a = atom b \<longleftrightarrow> a = b" |
203 unfolding atom_def by (simp add: Rep_inject) |
207 unfolding atom_def by (simp add: Rep_inject) |
204 show "p \<bullet> atom a = atom (p \<bullet> a)" |
208 show "p \<bullet> atom a = atom (p \<bullet> a)" |
205 unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep) |
209 unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep) |
206 qed |
210 qed |
|
211 *) |
|
212 |
|
213 lemma at_class: |
|
214 fixes s :: atom_sort |
|
215 fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a" |
|
216 assumes type: "type_definition Rep Abs {a. sort_of a = s}" |
|
217 assumes atom_def: "\<And>a. atom a = Rep a" |
|
218 assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)" |
|
219 shows "OFCLASS('a, at_class)" |
|
220 proof |
|
221 interpret type_definition Rep Abs "{a. sort_of a = s}" by (rule type) |
|
222 have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by (simp add: image_def) |
|
223 fix a b :: 'a and p p1 p2 :: perm |
|
224 show "0 \<bullet> a = a" |
|
225 unfolding permute_def by (simp add: Rep_inverse) |
|
226 show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a" |
|
227 unfolding permute_def by (simp add: Abs_inverse sort_of_Rep) |
|
228 show "sort_of (atom a) = sort_of (atom b)" |
|
229 unfolding atom_def by (simp add: sort_of_Rep) |
|
230 show "atom a = atom b \<longleftrightarrow> a = b" |
|
231 unfolding atom_def by (simp add: Rep_inject) |
|
232 show "p \<bullet> atom a = atom (p \<bullet> a)" |
|
233 unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep) |
|
234 qed |
207 |
235 |
208 setup {* Sign.add_const_constraint |
236 setup {* Sign.add_const_constraint |
209 (@{const_name "permute"}, SOME @{typ "perm \<Rightarrow> 'a::pt \<Rightarrow> 'a"}) *} |
237 (@{const_name "permute"}, SOME @{typ "perm \<Rightarrow> 'a::pt \<Rightarrow> 'a"}) *} |
210 setup {* Sign.add_const_constraint |
238 setup {* Sign.add_const_constraint |
211 (@{const_name "atom"}, SOME @{typ "'a::at_base \<Rightarrow> atom"}) *} |
239 (@{const_name "atom"}, SOME @{typ "'a::at_base \<Rightarrow> atom"}) *} |