equal
deleted
inserted
replaced
3 |
3 |
4 Instantiations of concrete atoms |
4 Instantiations of concrete atoms |
5 *) |
5 *) |
6 theory Atoms |
6 theory Atoms |
7 imports Nominal2_Base |
7 imports Nominal2_Base |
|
8 uses "~~/src/Tools/subtyping.ML" |
8 begin |
9 begin |
9 |
10 |
10 |
11 |
11 |
12 |
12 section {* @{const nat_of} is an example of a function |
13 section {* @{const nat_of} is an example of a function |
191 shows "ty_of (p \<bullet> x) = ty_of x" |
192 shows "ty_of (p \<bullet> x) = ty_of x" |
192 unfolding ty_of_def |
193 unfolding ty_of_def |
193 unfolding atom_eqvt [symmetric] |
194 unfolding atom_eqvt [symmetric] |
194 by simp |
195 by simp |
195 |
196 |
|
197 |
|
198 section {* Tests with subtyping and automatic coercions *} |
|
199 |
|
200 setup Subtyping.setup |
|
201 |
|
202 atom_decl var1 |
|
203 atom_decl var2 |
|
204 |
|
205 declare [[coercion "atom::var1\<Rightarrow>atom"]] |
|
206 |
|
207 declare [[coercion "atom::var2\<Rightarrow>atom"]] |
|
208 |
|
209 lemma |
|
210 fixes a::"var1" and b::"var2" |
|
211 shows "a \<sharp> t \<and> b \<sharp> t" |
|
212 oops |
|
213 |
|
214 (* does not yet work: it needs image as |
|
215 coercion map *) |
|
216 |
|
217 lemma |
|
218 fixes as::"var1 set" |
|
219 shows "atom ` as \<sharp>* t" |
|
220 oops |
|
221 |
196 end |
222 end |