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