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