1 (* Title: Nominal2_Atoms |
|
2 Authors: Brian Huffman, Christian Urban |
|
3 |
|
4 Definitions for concrete atom types. |
|
5 *) |
|
6 theory Nominal2_Atoms |
|
7 imports Nominal2_Base |
|
8 uses ("nominal_atoms.ML") |
|
9 begin |
|
10 |
|
11 section {* Concrete atom types *} |
|
12 |
|
13 text {* |
|
14 Class @{text at_base} allows types containing multiple sorts of atoms. |
|
15 Class @{text at} only allows types with a single sort. |
|
16 *} |
|
17 |
|
18 class at_base = pt + |
|
19 fixes atom :: "'a \<Rightarrow> atom" |
|
20 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 |
|
23 class at = at_base + |
|
24 assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)" |
|
25 |
|
26 instance at < at_base .. |
|
27 |
|
28 lemma supp_at_base: |
|
29 fixes a::"'a::at_base" |
|
30 shows "supp a = {atom a}" |
|
31 by (simp add: supp_atom [symmetric] supp_def atom_eqvt) |
|
32 |
|
33 lemma fresh_at_base: |
|
34 shows "a \<sharp> b \<longleftrightarrow> a \<noteq> atom b" |
|
35 unfolding fresh_def by (simp add: supp_at_base) |
|
36 |
|
37 instance at_base < fs |
|
38 proof qed (simp add: supp_at_base) |
|
39 |
|
40 lemma at_base_infinite [simp]: |
|
41 shows "infinite (UNIV :: 'a::at_base set)" (is "infinite ?U") |
|
42 proof |
|
43 obtain a :: 'a where "True" by auto |
|
44 assume "finite ?U" |
|
45 hence "finite (atom ` ?U)" |
|
46 by (rule finite_imageI) |
|
47 then obtain b where b: "b \<notin> atom ` ?U" "sort_of b = sort_of (atom a)" |
|
48 by (rule obtain_atom) |
|
49 from b(2) have "b = atom ((atom a \<rightleftharpoons> b) \<bullet> a)" |
|
50 unfolding atom_eqvt [symmetric] |
|
51 by (simp add: swap_atom) |
|
52 hence "b \<in> atom ` ?U" by simp |
|
53 with b(1) show "False" by simp |
|
54 qed |
|
55 |
|
56 lemma swap_at_base_simps [simp]: |
|
57 fixes x y::"'a::at_base" |
|
58 shows "sort_of (atom x) = sort_of (atom y) \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> x = y" |
|
59 and "sort_of (atom x) = sort_of (atom y) \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> y = x" |
|
60 and "atom x \<noteq> a \<Longrightarrow> atom x \<noteq> b \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> x = x" |
|
61 unfolding atom_eq_iff [symmetric] |
|
62 unfolding atom_eqvt [symmetric] |
|
63 by simp_all |
|
64 |
|
65 lemma obtain_at_base: |
|
66 assumes X: "finite X" |
|
67 obtains a::"'a::at_base" where "atom a \<notin> X" |
|
68 proof - |
|
69 have "inj (atom :: 'a \<Rightarrow> atom)" |
|
70 by (simp add: inj_on_def) |
|
71 with X have "finite (atom -` X :: 'a set)" |
|
72 by (rule finite_vimageI) |
|
73 with at_base_infinite have "atom -` X \<noteq> (UNIV :: 'a set)" |
|
74 by auto |
|
75 then obtain a :: 'a where "atom a \<notin> X" |
|
76 by auto |
|
77 thus ?thesis .. |
|
78 qed |
|
79 |
|
80 |
|
81 section {* A swapping operation for concrete atoms *} |
|
82 |
|
83 definition |
|
84 flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')") |
|
85 where |
|
86 "(a \<leftrightarrow> b) = (atom a \<rightleftharpoons> atom b)" |
|
87 |
|
88 lemma flip_self [simp]: "(a \<leftrightarrow> a) = 0" |
|
89 unfolding flip_def by (rule swap_self) |
|
90 |
|
91 lemma flip_commute: "(a \<leftrightarrow> b) = (b \<leftrightarrow> a)" |
|
92 unfolding flip_def by (rule swap_commute) |
|
93 |
|
94 lemma minus_flip [simp]: "- (a \<leftrightarrow> b) = (a \<leftrightarrow> b)" |
|
95 unfolding flip_def by (rule minus_swap) |
|
96 |
|
97 lemma add_flip_cancel: "(a \<leftrightarrow> b) + (a \<leftrightarrow> b) = 0" |
|
98 unfolding flip_def by (rule swap_cancel) |
|
99 |
|
100 lemma permute_flip_cancel [simp]: "(a \<leftrightarrow> b) \<bullet> (a \<leftrightarrow> b) \<bullet> x = x" |
|
101 unfolding permute_plus [symmetric] add_flip_cancel by simp |
|
102 |
|
103 lemma permute_flip_cancel2 [simp]: "(a \<leftrightarrow> b) \<bullet> (b \<leftrightarrow> a) \<bullet> x = x" |
|
104 by (simp add: flip_commute) |
|
105 |
|
106 lemma flip_eqvt: |
|
107 fixes a b c::"'a::at_base" |
|
108 shows "p \<bullet> (a \<leftrightarrow> b) = (p \<bullet> a \<leftrightarrow> p \<bullet> b)" |
|
109 unfolding flip_def |
|
110 by (simp add: swap_eqvt atom_eqvt) |
|
111 |
|
112 lemma flip_at_base_simps [simp]: |
|
113 shows "sort_of (atom a) = sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> a = b" |
|
114 and "sort_of (atom a) = sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> b = a" |
|
115 and "\<lbrakk>a \<noteq> c; b \<noteq> c\<rbrakk> \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> c = c" |
|
116 and "sort_of (atom a) \<noteq> sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> x = x" |
|
117 unfolding flip_def |
|
118 unfolding atom_eq_iff [symmetric] |
|
119 unfolding atom_eqvt [symmetric] |
|
120 by simp_all |
|
121 |
|
122 text {* the following two lemmas do not hold for at_base, |
|
123 only for single sort atoms from at *} |
|
124 |
|
125 lemma permute_flip_at: |
|
126 fixes a b c::"'a::at" |
|
127 shows "(a \<leftrightarrow> b) \<bullet> c = (if c = a then b else if c = b then a else c)" |
|
128 unfolding flip_def |
|
129 apply (rule atom_eq_iff [THEN iffD1]) |
|
130 apply (subst atom_eqvt [symmetric]) |
|
131 apply (simp add: swap_atom) |
|
132 done |
|
133 |
|
134 lemma flip_at_simps [simp]: |
|
135 fixes a b::"'a::at" |
|
136 shows "(a \<leftrightarrow> b) \<bullet> a = b" |
|
137 and "(a \<leftrightarrow> b) \<bullet> b = a" |
|
138 unfolding permute_flip_at by simp_all |
|
139 |
|
140 |
|
141 subsection {* Syntax for coercing at-elements to the atom-type *} |
|
142 |
|
143 syntax |
|
144 "_atom_constrain" :: "logic \<Rightarrow> type \<Rightarrow> logic" ("_:::_" [4, 0] 3) |
|
145 |
|
146 translations |
|
147 "_atom_constrain a t" => "atom (_constrain a t)" |
|
148 |
|
149 |
|
150 subsection {* A lemma for proving instances of class @{text at}. *} |
|
151 |
|
152 setup {* Sign.add_const_constraint (@{const_name "permute"}, NONE) *} |
|
153 setup {* Sign.add_const_constraint (@{const_name "atom"}, NONE) *} |
|
154 |
|
155 text {* |
|
156 New atom types are defined as subtypes of @{typ atom}. |
|
157 *} |
|
158 |
|
159 lemma exists_eq_simple_sort: |
|
160 shows "\<exists>a. a \<in> {a. sort_of a = s}" |
|
161 by (rule_tac x="Atom s 0" in exI, simp) |
|
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 |
|
167 lemma at_base_class: |
|
168 fixes sort_fun :: "'b \<Rightarrow>atom_sort" |
|
169 fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a" |
|
170 assumes type: "type_definition Rep Abs {a. sort_of a \<in> range sort_fun}" |
|
171 assumes atom_def: "\<And>a. atom a = Rep a" |
|
172 assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)" |
|
173 shows "OFCLASS('a, at_base_class)" |
|
174 proof |
|
175 interpret type_definition Rep Abs "{a. sort_of a \<in> range sort_fun}" by (rule type) |
|
176 have sort_of_Rep: "\<And>a. sort_of (Rep a) \<in> range sort_fun" using Rep by simp |
|
177 fix a b :: 'a and p p1 p2 :: perm |
|
178 show "0 \<bullet> a = a" |
|
179 unfolding permute_def by (simp add: Rep_inverse) |
|
180 show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a" |
|
181 unfolding permute_def by (simp add: Abs_inverse sort_of_Rep) |
|
182 show "atom a = atom b \<longleftrightarrow> a = b" |
|
183 unfolding atom_def by (simp add: Rep_inject) |
|
184 show "p \<bullet> atom a = atom (p \<bullet> a)" |
|
185 unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep) |
|
186 qed |
|
187 |
|
188 (* |
|
189 lemma at_class: |
|
190 fixes s :: atom_sort |
|
191 fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a" |
|
192 assumes type: "type_definition Rep Abs {a. sort_of a \<in> range (\<lambda>x::unit. s)}" |
|
193 assumes atom_def: "\<And>a. atom a = Rep a" |
|
194 assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)" |
|
195 shows "OFCLASS('a, at_class)" |
|
196 proof |
|
197 interpret type_definition Rep Abs "{a. sort_of a \<in> range (\<lambda>x::unit. s)}" by (rule type) |
|
198 have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by (simp add: image_def) |
|
199 fix a b :: 'a and p p1 p2 :: perm |
|
200 show "0 \<bullet> a = a" |
|
201 unfolding permute_def by (simp add: Rep_inverse) |
|
202 show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a" |
|
203 unfolding permute_def by (simp add: Abs_inverse sort_of_Rep) |
|
204 show "sort_of (atom a) = sort_of (atom b)" |
|
205 unfolding atom_def by (simp add: sort_of_Rep) |
|
206 show "atom a = atom b \<longleftrightarrow> a = b" |
|
207 unfolding atom_def by (simp add: Rep_inject) |
|
208 show "p \<bullet> atom a = atom (p \<bullet> a)" |
|
209 unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep) |
|
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 |
|
235 |
|
236 setup {* Sign.add_const_constraint |
|
237 (@{const_name "permute"}, SOME @{typ "perm \<Rightarrow> 'a::pt \<Rightarrow> 'a"}) *} |
|
238 setup {* Sign.add_const_constraint |
|
239 (@{const_name "atom"}, SOME @{typ "'a::at_base \<Rightarrow> atom"}) *} |
|
240 |
|
241 |
|
242 section {* Automation for creating concrete atom types *} |
|
243 |
|
244 text {* at the moment only single-sort concrete atoms are supported *} |
|
245 |
|
246 use "nominal_atoms.ML" |
|
247 |
|
248 |
|
249 |
|
250 |
|
251 end |
|