2 Authors: Brian Huffman, Christian Urban |
2 Authors: Brian Huffman, Christian Urban |
3 |
3 |
4 Instantiations of concrete atoms |
4 Instantiations of concrete atoms |
5 *) |
5 *) |
6 theory Atoms |
6 theory Atoms |
7 imports Nominal2_Atoms |
7 imports Nominal2_Base |
8 begin |
8 begin |
|
9 |
|
10 |
|
11 |
|
12 section {* @{const nat_of} is an example of a function |
|
13 without finite support *} |
|
14 |
|
15 |
|
16 lemma not_fresh_nat_of: |
|
17 shows "\<not> a \<sharp> nat_of" |
|
18 unfolding fresh_def supp_def |
|
19 proof (clarsimp) |
|
20 assume "finite {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}" |
|
21 hence "finite ({a} \<union> {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of})" |
|
22 by simp |
|
23 then obtain b where |
|
24 b1: "b \<noteq> a" and |
|
25 b2: "sort_of b = sort_of a" and |
|
26 b3: "(a \<rightleftharpoons> b) \<bullet> nat_of = nat_of" |
|
27 by (rule obtain_atom) auto |
|
28 have "nat_of a = (a \<rightleftharpoons> b) \<bullet> (nat_of a)" by (simp add: permute_nat_def) |
|
29 also have "\<dots> = ((a \<rightleftharpoons> b) \<bullet> nat_of) ((a \<rightleftharpoons> b) \<bullet> a)" by (simp add: permute_fun_app_eq) |
|
30 also have "\<dots> = nat_of ((a \<rightleftharpoons> b) \<bullet> a)" using b3 by simp |
|
31 also have "\<dots> = nat_of b" using b2 by simp |
|
32 finally have "nat_of a = nat_of b" by simp |
|
33 with b2 have "a = b" by (simp add: atom_components_eq_iff) |
|
34 with b1 show "False" by simp |
|
35 qed |
|
36 |
|
37 lemma supp_nat_of: |
|
38 shows "supp nat_of = UNIV" |
|
39 using not_fresh_nat_of [unfolded fresh_def] by auto |
|
40 |
9 |
41 |
10 section {* Manual instantiation of class @{text at}. *} |
42 section {* Manual instantiation of class @{text at}. *} |
11 |
43 |
12 typedef (open) name = "{a. sort_of a = Sort ''name'' []}" |
44 typedef (open) name = "{a. sort_of a = Sort ''name'' []}" |
13 by (rule exists_eq_simple_sort) |
45 by (rule exists_eq_simple_sort) |