1785
|
1 |
(*<*)
|
|
2 |
theory Paper
|
2568
8193bbaa07fe
merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
3 |
imports "../Nominal/Nominal2_Base"
|
8193bbaa07fe
merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
4 |
"../Nominal/Nominal2_Eqvt"
|
8193bbaa07fe
merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
5 |
"../Nominal/Atoms"
|
2522
|
6 |
"../Nominal/Abs"
|
1785
|
7 |
"LaTeXsugar"
|
|
8 |
begin
|
|
9 |
|
|
10 |
notation (latex output)
|
|
11 |
sort_of ("sort _" [1000] 100) and
|
|
12 |
Abs_perm ("_") and
|
|
13 |
Rep_perm ("_") and
|
|
14 |
swap ("'(_ _')" [1000, 1000] 1000) and
|
|
15 |
fresh ("_ # _" [51, 51] 50) and
|
2523
|
16 |
fresh_star ("_ #\<^sup>* _" [51, 51] 50) and
|
1785
|
17 |
Cons ("_::_" [78,77] 73) and
|
|
18 |
supp ("supp _" [78] 73) and
|
|
19 |
uminus ("-_" [78] 73) and
|
|
20 |
atom ("|_|") and
|
|
21 |
If ("if _ then _ else _" 10) and
|
|
22 |
Rep_name ("\<lfloor>_\<rfloor>") and
|
|
23 |
Abs_name ("\<lceil>_\<rceil>") and
|
|
24 |
Rep_var ("\<lfloor>_\<rfloor>") and
|
|
25 |
Abs_var ("\<lceil>_\<rceil>") and
|
|
26 |
sort_of_ty ("sort'_ty _")
|
|
27 |
|
|
28 |
(* BH: uncomment if you really prefer the dot notation
|
|
29 |
syntax (latex output)
|
|
30 |
"_Collect" :: "pttrn => bool => 'a set" ("(1{_ . _})")
|
|
31 |
*)
|
|
32 |
|
|
33 |
(* sort is used in Lists for sorting *)
|
2005
|
34 |
hide_const sort
|
1785
|
35 |
|
|
36 |
abbreviation
|
|
37 |
"sort \<equiv> sort_of"
|
|
38 |
|
|
39 |
abbreviation
|
|
40 |
"sort_ty \<equiv> sort_of_ty"
|
|
41 |
|
|
42 |
(*>*)
|
|
43 |
|
2521
|
44 |
(*
|
|
45 |
TODO: write about supp of finite sets, abstraction over finite sets
|
|
46 |
*)
|
|
47 |
|
1785
|
48 |
section {* Introduction *}
|
|
49 |
|
|
50 |
text {*
|
2521
|
51 |
Nominal Isabelle provides a proving infratructure for convenient reasoning
|
2523
|
52 |
about programming language calculi involving binders such as lambda abstractions or
|
2521
|
53 |
quantifications in type schemes:
|
2466
|
54 |
|
2521
|
55 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
56 |
@{text "\<lambda>x. t \<forall>{x\<^isub>1,\<dots>,x\<^isub>n}. \<tau>"}
|
|
57 |
\hfill\numbered{atomperm}
|
|
58 |
\end{isabelle}
|
|
59 |
|
|
60 |
\noindent
|
|
61 |
At its core Nominal Isabelle is based on the nominal logic work by Pitts at
|
|
62 |
al \cite{GabbayPitts02,Pitts03}. The most basic notion in this work is a
|
|
63 |
sort-respecting permutation operation defined over a countably infinite
|
|
64 |
collection of sorted atoms. The atoms are used for representing variable names
|
2523
|
65 |
that might be bound or free. Multiple sorts are necessary for being able to
|
2065
|
66 |
represent different kinds of variables. For example, in the language Mini-ML
|
2521
|
67 |
there are bound term variables in lambda abstractions and bound type variables in
|
|
68 |
type schemes. In order to be able to separate them, each kind of variables needs to be
|
|
69 |
represented by a different sort of atoms.
|
1785
|
70 |
|
2523
|
71 |
The existing nominal logic work usually leaves implicit the sorting
|
|
72 |
information for atoms and as far as we know leaves out a description of how
|
|
73 |
sorts are represented. In our formalisation, we therefore have to make a
|
|
74 |
design decision about how to implement sorted atoms and sort-respecting
|
|
75 |
permutations. One possibility, which we described in \cite{Urban08}, is to
|
|
76 |
have separate types for the different
|
|
77 |
kinds of atoms, say types @{text "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}. With this
|
|
78 |
design one can represent permutations as lists of pairs of atoms and the
|
|
79 |
operation of applying a permutation to an object as the function
|
|
80 |
|
1785
|
81 |
|
|
82 |
@{text [display,indent=10] "_ \<bullet> _ :: (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
|
|
83 |
|
|
84 |
\noindent
|
2521
|
85 |
where @{text "\<alpha>"} stands for a type of atoms and @{text "\<beta>"} for the type
|
|
86 |
of the objects on which the permutation acts. For atoms
|
1785
|
87 |
the permutation operation is defined over the length of lists as follows
|
|
88 |
|
|
89 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
90 |
\begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
|
|
91 |
@{text "[] \<bullet> c"} & @{text "="} & @{text c}\\
|
|
92 |
@{text "(a b)::\<pi> \<bullet> c"} & @{text "="} &
|
|
93 |
$\begin{cases} @{text a} & \textrm{if}~@{text "\<pi> \<bullet> c = b"}\\
|
|
94 |
@{text b} & \textrm{if}~@{text "\<pi> \<bullet> c = a"}\\
|
|
95 |
@{text "\<pi> \<bullet> c"} & \textrm{otherwise}\end{cases}$
|
|
96 |
\end{tabular}\hfill\numbered{atomperm}
|
|
97 |
\end{isabelle}
|
|
98 |
|
|
99 |
\noindent
|
|
100 |
where we write @{text "(a b)"} for a swapping of atoms @{text "a"} and
|
2523
|
101 |
@{text "b"}. For atoms with different type than the permutation, we
|
|
102 |
define @{text "\<pi> \<bullet> c \<equiv> c"}.
|
1785
|
103 |
|
2521
|
104 |
With the separate atom types and the list representation of permutations it
|
2522
|
105 |
is impossible in systems like Isabelle/HOL to state an ``ill-sorted''
|
|
106 |
permutation, since the type system excludes lists containing atoms of
|
|
107 |
different type. However, a disadvantage is that whenever we need to
|
|
108 |
generalise induction hypotheses by quantifying over permutations, we have to
|
|
109 |
build quantifications like
|
2521
|
110 |
|
|
111 |
@{text [display,indent=10] "\<forall>\<pi>\<^isub>1 \<dots> \<forall>\<pi>\<^isub>n. \<dots>"}
|
|
112 |
|
|
113 |
\noindent
|
|
114 |
where the @{text "\<pi>\<^isub>i"} are of type @{text "(\<alpha>\<^isub>i \<times> \<alpha>\<^isub>i) list"}.
|
|
115 |
The reason is that the permutation operation behaves differently for
|
2523
|
116 |
every @{text "\<alpha>\<^isub>i"} and the type system does not allow use to have a
|
|
117 |
single quantification to stand for all permutations. Similarly, the
|
|
118 |
notion of support
|
2521
|
119 |
|
|
120 |
@{text [display,indent=10] "supp _ :: \<beta> \<Rightarrow> \<alpha> set"}
|
|
121 |
|
|
122 |
\noindent
|
|
123 |
which we will define later, cannot be
|
|
124 |
used to express the support of an object over \emph{all} atoms. The reason
|
|
125 |
is that support can behave differently for each @{text
|
|
126 |
"\<alpha>\<^isub>i"}. This problem is annoying, because if we need to know in
|
|
127 |
a statement that an object, say @{text "x"}, is finitely supported we end up
|
|
128 |
with having to state premises of the form
|
|
129 |
|
|
130 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
131 |
\begin{tabular}{@ {}l}
|
|
132 |
@{text "finite ((supp x) :: \<alpha>\<^isub>1 set) , \<dots>, finite ((supp x) :: \<alpha>\<^isub>n set)"}
|
|
133 |
\end{tabular}\hfill\numbered{fssequence}
|
|
134 |
\end{isabelle}
|
|
135 |
|
2522
|
136 |
\noindent
|
2523
|
137 |
Because of these disadvantages, we will use in this paper a single unified atom type to
|
|
138 |
represent atoms of different sorts. Consequently, we have to deal with the
|
2522
|
139 |
case that a swapping of two atoms is ill-sorted: we cannot rely anymore on
|
2523
|
140 |
the type systems to exclude them.
|
2521
|
141 |
|
2523
|
142 |
We also will not represent permutations as lists of pairs of atoms (as done in
|
|
143 |
\cite{Urban08}). Although an
|
2522
|
144 |
advantage of this representation is that the basic operations on
|
|
145 |
permutations are already defined in Isabelle's list library: composition of
|
|
146 |
two permutations (written @{text "_ @ _"}) is just list append, and
|
|
147 |
inversion of a permutation (written @{text "_\<^sup>-\<^sup>1"}) is just
|
2523
|
148 |
list reversal, and another advantage is that there is a well-understood
|
|
149 |
induction principle for lists, a disadvantage is that permutations
|
|
150 |
do not have unique representations as lists. We have to explicitly identify
|
2522
|
151 |
them according to the relation
|
2521
|
152 |
|
1785
|
153 |
|
|
154 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
155 |
\begin{tabular}{@ {}l}
|
|
156 |
@{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2 \<equiv> \<forall>a. \<pi>\<^isub>1 \<bullet> a = \<pi>\<^isub>2 \<bullet> a"}
|
|
157 |
\end{tabular}\hfill\numbered{permequ}
|
|
158 |
\end{isabelle}
|
|
159 |
|
2522
|
160 |
\noindent
|
|
161 |
This is a problem when lifting the permutation operation to other types, for
|
2523
|
162 |
example sets, functions and so on. For this we need to ensure that every definition
|
2522
|
163 |
is well-behaved in the sense that it satisfies some
|
|
164 |
\emph{permutation properties}. In the list representation we need
|
|
165 |
to state these properties as follows:
|
|
166 |
|
1785
|
167 |
|
|
168 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
169 |
\begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
|
|
170 |
i) & @{text "[] \<bullet> x = x"}\\
|
|
171 |
ii) & @{text "(\<pi>\<^isub>1 @ \<pi>\<^isub>2) \<bullet> x = \<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x)"}\\
|
|
172 |
iii) & if @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2"} then @{text "\<pi>\<^isub>1 \<bullet> x = \<pi>\<^isub>2 \<bullet> x"}
|
|
173 |
\end{tabular}\hfill\numbered{permprops}
|
|
174 |
\end{isabelle}
|
|
175 |
|
|
176 |
\noindent
|
2522
|
177 |
where the last clause explicitly states that the permutation operation has
|
2523
|
178 |
to produce the same result for related permutations. Moreover,
|
|
179 |
``permutations-as-lists'' do not satisfy the group properties. This means by
|
2522
|
180 |
using this representation we will not be able to reuse the extensive
|
2523
|
181 |
reasoning infrastructure in Isabelle about groups. Because of this, we will represent
|
|
182 |
in this paper permutations as functions from atoms to atoms. This representation
|
|
183 |
is unique and satisfies the laws of non-commutative groups.
|
1785
|
184 |
|
2522
|
185 |
Using a single atom type to represent atoms of different sorts and
|
2523
|
186 |
representing permutations as functions are not new ideas; see
|
|
187 |
\cite{GunterOsbornPopescu09} \footnote{function rep.} The main contribution
|
|
188 |
of this paper is to show an example of how to make better theorem proving
|
|
189 |
tools by choosing the right level of abstraction for the underlying
|
|
190 |
theory---our design choices take advantage of Isabelle's type system, type
|
|
191 |
classes and reasoning infrastructure. The novel technical contribution is a
|
|
192 |
mechanism for dealing with ``Church-style'' lambda-terms \cite{Church40} and
|
|
193 |
HOL-based languages \cite{PittsHOL4} where variables and variable binding
|
|
194 |
depend on type annotations.
|
1785
|
195 |
|
2523
|
196 |
The paper is organised as follows\ldots
|
1785
|
197 |
*}
|
|
198 |
|
|
199 |
section {* Sorted Atoms and Sort-Respecting Permutations *}
|
|
200 |
|
|
201 |
text {*
|
|
202 |
In the nominal logic work of Pitts, binders and bound variables are
|
|
203 |
represented by \emph{atoms}. As stated above, we need to have different
|
|
204 |
\emph{sorts} of atoms to be able to bind different kinds of variables. A
|
|
205 |
basic requirement is that there must be a countably infinite number of atoms
|
2522
|
206 |
of each sort. We implement these atoms as
|
1785
|
207 |
*}
|
|
208 |
|
|
209 |
datatype atom\<iota> = Atom\<iota> string nat
|
|
210 |
|
|
211 |
text {*
|
|
212 |
\noindent
|
2522
|
213 |
whereby the string argument specifies the sort of the atom.\footnote{A
|
|
214 |
similar design choice was made by Gunter et al \cite{GunterOsbornPopescu09}
|
2523
|
215 |
for their variables.} (The use of type \emph{string} is merely for
|
2522
|
216 |
convenience; any countably infinite type would work as well.) We have an
|
|
217 |
auxiliary function @{text sort} that is defined as @{thm
|
|
218 |
sort_of.simps[no_vars]}, and we clearly have for every finite set @{text X}
|
|
219 |
of atoms and every sort @{text s} the property:
|
|
220 |
|
1785
|
221 |
\begin{proposition}\label{choosefresh}
|
2522
|
222 |
@{text "For a finite set of atoms S, there exists an atom a such that
|
|
223 |
sort a = s and a \<notin> S"}.
|
1785
|
224 |
\end{proposition}
|
|
225 |
|
|
226 |
For implementing sort-respecting permutations, we use functions of type @{typ
|
|
227 |
"atom => atom"} that @{text "i)"} are bijective; @{text "ii)"} are the
|
|
228 |
identity on all atoms, except a finite number of them; and @{text "iii)"} map
|
|
229 |
each atom to one of the same sort. These properties can be conveniently stated
|
|
230 |
for a function @{text \<pi>} as follows:
|
|
231 |
|
|
232 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
233 |
\begin{tabular}{r@ {\hspace{4mm}}l}
|
|
234 |
i) & @{term "bij \<pi>"}\\
|
|
235 |
ii) & @{term "finite {a. \<pi> a \<noteq> a}"}\\
|
|
236 |
iii) & @{term "\<forall>a. sort (\<pi> a) = sort a"}
|
|
237 |
\end{tabular}\hfill\numbered{permtype}
|
|
238 |
\end{isabelle}
|
|
239 |
|
|
240 |
\noindent
|
|
241 |
Like all HOL-based theorem provers, Isabelle/HOL allows us to
|
|
242 |
introduce a new type @{typ perm} that includes just those functions
|
|
243 |
satisfying all three properties. For example the identity function,
|
|
244 |
written @{term id}, is included in @{typ perm}. Also function composition,
|
|
245 |
written \mbox{@{text "_ \<circ> _"}}, and function inversion, given by Isabelle/HOL's
|
|
246 |
inverse operator and written \mbox{@{text "inv _"}}, preserve the properties
|
|
247 |
@{text "i"}-@{text "iii"}.
|
|
248 |
|
|
249 |
However, a moment of thought is needed about how to construct non-trivial
|
|
250 |
permutations. In the nominal logic work it turned out to be most convenient
|
|
251 |
to work with swappings, written @{text "(a b)"}. In our setting the
|
|
252 |
type of swappings must be
|
|
253 |
|
|
254 |
@{text [display,indent=10] "(_ _) :: atom \<Rightarrow> atom \<Rightarrow> perm"}
|
|
255 |
|
|
256 |
\noindent
|
|
257 |
but since permutations are required to respect sorts, we must carefully
|
|
258 |
consider what happens if a user states a swapping of atoms with different
|
2522
|
259 |
sorts. In early versions of Nominal Isabelle, we avoided this problem by
|
1785
|
260 |
using different types for different sorts; the type system prevented users
|
|
261 |
from stating ill-sorted swappings. Here, however, definitions such
|
|
262 |
as\footnote{To increase legibility, we omit here and in what follows the
|
|
263 |
@{term Rep_perm} and @{term "Abs_perm"} wrappers that are needed in our
|
|
264 |
implementation since we defined permutation not to be the full function space,
|
|
265 |
but only those functions of type @{typ perm} satisfying properties @{text
|
|
266 |
i}-@{text "iii"}.}
|
|
267 |
|
|
268 |
@{text [display,indent=10] "(a b) \<equiv> \<lambda>c. if a = c then b else (if b = c then a else c)"}
|
|
269 |
|
|
270 |
\noindent
|
|
271 |
do not work in general, because the type system does not prevent @{text a}
|
|
272 |
and @{text b} from having different sorts---in which case the function would
|
|
273 |
violate property @{text iii}. We could make the definition of swappings
|
|
274 |
partial by adding the precondition @{term "sort a = sort b"},
|
|
275 |
which would mean that in case @{text a} and @{text b} have different sorts,
|
|
276 |
the value of @{text "(a b)"} is unspecified. However, this looked like a
|
|
277 |
cumbersome solution, since sort-related side conditions would be required
|
|
278 |
everywhere, even to unfold the definition. It turned out to be more
|
|
279 |
convenient to actually allow the user to state ``ill-sorted'' swappings but
|
|
280 |
limit their ``damage'' by defaulting to the identity permutation in the
|
|
281 |
ill-sorted case:
|
|
282 |
|
|
283 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
284 |
\begin{tabular}{@ {}rl}
|
|
285 |
@{text "(a b) \<equiv>"} & @{text "if (sort a = sort b)"}\\
|
|
286 |
& \hspace{3mm}@{text "then \<lambda>c. if a = c then b else (if b = c then a else c)"}\\
|
|
287 |
& \hspace{3mm}@{text "else id"}
|
|
288 |
\end{tabular}\hfill\numbered{swapdef}
|
|
289 |
\end{isabelle}
|
|
290 |
|
|
291 |
\noindent
|
|
292 |
This function is bijective, the identity on all atoms except
|
|
293 |
@{text a} and @{text b}, and sort respecting. Therefore it is
|
|
294 |
a function in @{typ perm}.
|
|
295 |
|
|
296 |
One advantage of using functions instead of lists as a representation for
|
|
297 |
permutations is that for example the swappings
|
|
298 |
|
|
299 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
300 |
\begin{tabular}{@ {}l}
|
|
301 |
@{thm swap_commute[no_vars]}\hspace{10mm}
|
|
302 |
@{text "(a a) = id"}
|
|
303 |
\end{tabular}\hfill\numbered{swapeqs}
|
|
304 |
\end{isabelle}
|
|
305 |
|
|
306 |
\noindent
|
|
307 |
are \emph{equal}. We do not have to use the equivalence relation shown
|
|
308 |
in~\eqref{permequ} to identify them, as we would if they had been represented
|
|
309 |
as lists of pairs. Another advantage of the function representation is that
|
1809
|
310 |
they form a (non-commutative) group provided we define
|
1785
|
311 |
|
|
312 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
313 |
\begin{tabular}{@ {}l}
|
|
314 |
@{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm}
|
|
315 |
@{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm}
|
|
316 |
@{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{4mm}
|
2382
|
317 |
@{thm diff_def[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2"]}
|
1785
|
318 |
\end{tabular}
|
|
319 |
\end{isabelle}
|
|
320 |
|
|
321 |
\noindent
|
|
322 |
and verify the simple properties
|
|
323 |
|
|
324 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
325 |
\begin{tabular}{@ {}l}
|
|
326 |
@{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]} \hspace{3mm}
|
|
327 |
@{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{3mm}
|
|
328 |
@{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{3mm}
|
|
329 |
@{thm group_add_class.left_minus[where a="\<pi>::perm"]}
|
|
330 |
\end{tabular}
|
|
331 |
\end{isabelle}
|
|
332 |
|
|
333 |
\noindent
|
|
334 |
Again this is in contrast to the list-of-pairs representation which does not
|
1809
|
335 |
form a group. The technical importance of this fact is that we can rely on
|
|
336 |
Isabelle/HOL's existing simplification infrastructure for groups, which will
|
|
337 |
come in handy when we have to do calculations with permutations.
|
1790
|
338 |
Note that Isabelle/HOL defies standard conventions of mathematical notation
|
|
339 |
by using additive syntax even for non-commutative groups. Obviously,
|
|
340 |
composition of permutations is not commutative in general, because @{text
|
|
341 |
"\<pi>\<^sub>1 + \<pi>\<^sub>2 \<noteq> \<pi>\<^sub>2 + \<pi>\<^sub>1"}. But since the point of this paper is to implement the
|
|
342 |
nominal theory as smoothly as possible in Isabelle/HOL, we tolerate
|
|
343 |
the non-standard notation in order to reuse the existing libraries.
|
1785
|
344 |
|
|
345 |
By formalising permutations abstractly as functions, and using a single type
|
|
346 |
for all atoms, we can now restate the \emph{permutation properties} from
|
|
347 |
\eqref{permprops} as just the two equations
|
|
348 |
|
|
349 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
350 |
\begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
|
|
351 |
i) & @{thm permute_zero[no_vars]}\\
|
|
352 |
ii) & @{thm permute_plus[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2",no_vars]}
|
|
353 |
\end{tabular}\hfill\numbered{newpermprops}
|
|
354 |
\end{isabelle}
|
|
355 |
|
|
356 |
\noindent
|
|
357 |
in which the permutation operations are of type @{text "perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} and so
|
|
358 |
have only a single type parameter. Consequently, these properties are
|
|
359 |
compatible with the one-parameter restriction of Isabelle/HOL's type classes.
|
|
360 |
There is no need to introduce a separate type class instantiated for each
|
|
361 |
sort, like in the old approach.
|
|
362 |
|
|
363 |
The next notion allows us to establish generic lemmas involving the
|
|
364 |
permutation operation.
|
|
365 |
|
|
366 |
\begin{definition}
|
|
367 |
A type @{text "\<beta>"} is a \emph{permutation type} if the permutation
|
|
368 |
properties in \eqref{newpermprops} are satisfied for every @{text "x"} of type
|
|
369 |
@{text "\<beta>"}.
|
|
370 |
\end{definition}
|
|
371 |
|
|
372 |
\noindent
|
|
373 |
First, it follows from the laws governing
|
|
374 |
groups that a permutation and its inverse cancel each other. That is, for any
|
|
375 |
@{text "x"} of a permutation type:
|
|
376 |
|
|
377 |
|
|
378 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
379 |
\begin{tabular}{@ {}l}
|
|
380 |
@{thm permute_minus_cancel(1)[where p="\<pi>", no_vars]}\hspace{10mm}
|
|
381 |
@{thm permute_minus_cancel(2)[where p="\<pi>", no_vars]}
|
|
382 |
\end{tabular}\hfill\numbered{cancel}
|
|
383 |
\end{isabelle}
|
|
384 |
|
|
385 |
\noindent
|
2523
|
386 |
Consequently, in a permutation type the permutation operation @{text "\<pi> \<bullet> _"}~~is bijective,
|
1785
|
387 |
which in turn implies the property
|
|
388 |
|
|
389 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
390 |
\begin{tabular}{@ {}l}
|
|
391 |
@{thm (lhs) permute_eq_iff[where p="\<pi>", no_vars]}
|
|
392 |
$\;$if and only if$\;$
|
|
393 |
@{thm (rhs) permute_eq_iff[where p="\<pi>", no_vars]}.
|
|
394 |
\end{tabular}\hfill\numbered{permuteequ}
|
|
395 |
\end{isabelle}
|
|
396 |
|
|
397 |
\noindent
|
2523
|
398 |
We can also show that the following property holds for any permutation type.
|
|
399 |
|
|
400 |
\begin{lemma}\label{permutecompose}
|
|
401 |
Given @{term x} is of permutation type, then
|
|
402 |
@{text "\<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x) = (\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}.
|
|
403 |
\end{lemma}
|
|
404 |
|
|
405 |
\begin{proof} The proof is as follows:
|
|
406 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
407 |
\begin{tabular}[b]{@ {}rcl@ {\hspace{8mm}}l}
|
|
408 |
@{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> x"}
|
|
409 |
& @{text "="} & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> (-\<pi>\<^isub>1) \<bullet> \<pi>\<^isub>1 \<bullet> x"} & by \eqref{cancel}\\
|
|
410 |
& @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2 - \<pi>\<^isub>1) \<bullet> \<pi>\<^isub>1 \<bullet> x"} & by {\rm(\ref{newpermprops}.@{text "ii"})}\\
|
|
411 |
& @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}\\
|
|
412 |
\end{tabular}\hfill\qed
|
|
413 |
\end{isabelle}
|
|
414 |
\end{proof}
|
|
415 |
|
|
416 |
\noindent
|
1785
|
417 |
In order to lift the permutation operation to other types, we can define for:
|
|
418 |
|
2523
|
419 |
\begin{equation}\label{permdefs}
|
|
420 |
\mbox{
|
|
421 |
\begin{tabular}{@ {}ll@ {\hspace{2mm}}l@ {}}
|
|
422 |
1) & atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\
|
|
423 |
2) & functions: & @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\
|
|
424 |
3) & permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\
|
|
425 |
4) & sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
|
|
426 |
5) & booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
|
|
427 |
6) & lists: & @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
|
|
428 |
& & @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
|
|
429 |
7) & products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\
|
|
430 |
8) & nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
|
|
431 |
\end{tabular}}
|
|
432 |
\end{equation}
|
1785
|
433 |
|
|
434 |
\noindent
|
|
435 |
and then establish:
|
|
436 |
|
|
437 |
\begin{theorem}
|
|
438 |
If @{text \<beta>}, @{text "\<beta>\<^isub>1"} and @{text "\<beta>\<^isub>2"} are permutation types,
|
|
439 |
then so are @{text "atom"}, @{text "\<beta>\<^isub>1 \<Rightarrow> \<beta>\<^isub>2"},
|
|
440 |
@{text perm}, @{term "\<beta> set"}, @{term "\<beta> list"}, @{term "\<beta>\<^isub>1 \<times> \<beta>\<^isub>2"},
|
|
441 |
@{text bool} and @{text "nat"}.
|
|
442 |
\end{theorem}
|
|
443 |
|
|
444 |
\begin{proof}
|
|
445 |
All statements are by unfolding the definitions of the permutation operations and simple
|
|
446 |
calculations involving addition and minus. With permutations for example we
|
|
447 |
have
|
|
448 |
|
|
449 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
450 |
\begin{tabular}[b]{@ {}rcl}
|
|
451 |
@{text "0 \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "0 + \<pi>' - 0 = \<pi>'"}\\
|
|
452 |
@{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) + \<pi>' - (\<pi>\<^isub>1 + \<pi>\<^isub>2)"}\\
|
|
453 |
& @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) + \<pi>' - \<pi>\<^isub>2 - \<pi>\<^isub>1"}\\
|
|
454 |
& @{text "="} & @{text "\<pi>\<^isub>1 + (\<pi>\<^isub>2 + \<pi>' - \<pi>\<^isub>2) - \<pi>\<^isub>1"} @{text "\<equiv>"} @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> \<pi>'"}
|
|
455 |
\end{tabular}\hfill\qed
|
|
456 |
\end{isabelle}
|
|
457 |
\end{proof}
|
|
458 |
*}
|
|
459 |
|
|
460 |
section {* Equivariance *}
|
|
461 |
|
|
462 |
text {*
|
2523
|
463 |
An important notion in the nominal logic work is \emph{equivariance}.
|
|
464 |
An equivariant function or predicate is one that is invariant under
|
|
465 |
the swapping of atoms. This notion can be defined
|
|
466 |
uniformly as follows:
|
1809
|
467 |
|
1785
|
468 |
|
|
469 |
\begin{definition}\label{equivariance}
|
|
470 |
A function @{text f} is \emph{equivariant} if @{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}.
|
|
471 |
\end{definition}
|
|
472 |
|
|
473 |
\noindent
|
|
474 |
There are a number of equivalent formulations for the equivariance property.
|
|
475 |
For example, assuming @{text f} is of type @{text "\<alpha> \<Rightarrow> \<beta>"}, then equivariance
|
|
476 |
can also be stated as
|
|
477 |
|
|
478 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
479 |
\begin{tabular}{@ {}l}
|
|
480 |
@{text "\<forall>\<pi> x. \<pi> \<bullet> (f x) = f (\<pi> \<bullet> x)"}
|
|
481 |
\end{tabular}\hfill\numbered{altequivariance}
|
|
482 |
\end{isabelle}
|
|
483 |
|
|
484 |
\noindent
|
|
485 |
To see that this formulation implies the definition, we just unfold the
|
|
486 |
definition of the permutation operation for functions and simplify with the equation
|
|
487 |
and the cancellation property shown in \eqref{cancel}. To see the other direction, we use
|
|
488 |
the fact
|
|
489 |
|
|
490 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
491 |
\begin{tabular}{@ {}l}
|
|
492 |
@{text "\<pi> \<bullet> (f x) = (\<pi> \<bullet> f) (\<pi> \<bullet> x)"}
|
|
493 |
\end{tabular}\hfill\numbered{permutefunapp}
|
|
494 |
\end{isabelle}
|
|
495 |
|
|
496 |
\noindent
|
|
497 |
which follows again directly
|
|
498 |
from the definition of the permutation operation for functions and the cancellation
|
|
499 |
property. Similarly for functions with more than one argument.
|
|
500 |
|
|
501 |
Both formulations of equivariance have their advantages and disadvantages:
|
2523
|
502 |
the definition, \eqref{permutefunapp} and (\ref{permdefs}.2) lead to a simple
|
|
503 |
rewrite system that pushes permutations inside a term until they reach
|
|
504 |
either function constants or variables. The permutations in front of
|
|
505 |
equivariant functions disappear. Such a rewrite system is often very helpful
|
|
506 |
in determining whether @{text "p \<bullet> t = t"} holds for a compound term @{text t}. In contrast
|
|
507 |
\eqref{altequivariance} is usually easier to establish, since statements are
|
|
508 |
commonly given in a form where functions are fully applied. For example we can
|
|
509 |
easily show that equality is equivariant
|
1785
|
510 |
|
|
511 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
512 |
\begin{tabular}{@ {}l}
|
|
513 |
@{thm eq_eqvt[where p="\<pi>", no_vars]}
|
|
514 |
\end{tabular}
|
|
515 |
\end{isabelle}
|
|
516 |
|
|
517 |
\noindent
|
|
518 |
using the permutation operation on booleans and property \eqref{permuteequ}.
|
|
519 |
Lemma~\ref{permutecompose} establishes that the permutation operation is
|
|
520 |
equivariant. It is also easy to see that the boolean operators, like
|
|
521 |
@{text "\<and>"}, @{text "\<or>"} and @{text "\<longrightarrow>"} are all equivariant. Furthermore
|
|
522 |
a simple calculation will show that our swapping functions are equivariant, that is
|
|
523 |
|
|
524 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
525 |
\begin{tabular}{@ {}l}
|
|
526 |
@{thm swap_eqvt[where p="\<pi>", no_vars]}
|
|
527 |
\end{tabular}\hfill\numbered{swapeqvt}
|
|
528 |
\end{isabelle}
|
|
529 |
|
|
530 |
\noindent
|
2523
|
531 |
for all @{text a}, @{text b} and @{text \<pi>}.
|
1785
|
532 |
*}
|
|
533 |
|
|
534 |
|
|
535 |
section {* Support and Freshness *}
|
|
536 |
|
|
537 |
text {*
|
|
538 |
The most original aspect of the nominal logic work of Pitts et al is a general
|
|
539 |
definition for ``the set of free variables of an object @{text "x"}''. This
|
|
540 |
definition is general in the sense that it applies not only to lambda-terms,
|
|
541 |
but also to lists, products, sets and even functions. The definition depends
|
|
542 |
only on the permutation operation and on the notion of equality defined for
|
|
543 |
the type of @{text x}, namely:
|
|
544 |
|
|
545 |
@{thm [display,indent=10] supp_def[no_vars, THEN eq_reflection]}
|
|
546 |
|
|
547 |
\noindent
|
|
548 |
(Note that due to the definition of swapping in \eqref{swapdef}, we do not
|
|
549 |
need to explicitly restrict @{text a} and @{text b} to have the same sort.)
|
|
550 |
There is also the derived notion for when an atom @{text a} is \emph{fresh}
|
|
551 |
for an @{text x}, defined as
|
|
552 |
|
|
553 |
@{thm [display,indent=10] fresh_def[no_vars]}
|
|
554 |
|
|
555 |
\noindent
|
2523
|
556 |
We also use the notation @{thm (lhs) fresh_star_def[no_vars]} for sets ot atoms
|
|
557 |
defined as follows
|
|
558 |
|
|
559 |
@{thm [display,indent=10] fresh_star_def[no_vars]}
|
|
560 |
|
|
561 |
\noindent
|
1785
|
562 |
A striking consequence of these definitions is that we can prove
|
|
563 |
without knowing anything about the structure of @{term x} that
|
|
564 |
swapping two fresh atoms, say @{text a} and @{text b}, leave
|
|
565 |
@{text x} unchanged. For the proof we use the following lemma
|
|
566 |
about swappings applied to an @{text x}:
|
|
567 |
|
|
568 |
\begin{lemma}\label{swaptriple}
|
|
569 |
Assuming @{text x} is of permutation type, and @{text a}, @{text b} and @{text c}
|
|
570 |
have the same sort, then @{thm (prem 3) swap_rel_trans[no_vars]} and
|
|
571 |
@{thm (prem 4) swap_rel_trans[no_vars]} imply @{thm (concl) swap_rel_trans[no_vars]}.
|
|
572 |
\end{lemma}
|
|
573 |
|
|
574 |
\begin{proof}
|
|
575 |
The cases where @{text "a = c"} and @{text "b = c"} are immediate.
|
|
576 |
For the remaining case it is, given our assumptions, easy to calculate
|
|
577 |
that the permutations
|
|
578 |
|
|
579 |
@{thm [display,indent=10] (concl) swap_triple[no_vars]}
|
|
580 |
|
|
581 |
\noindent
|
|
582 |
are equal. The lemma is then by application of the second permutation
|
|
583 |
property shown in \eqref{newpermprops}.\hfill\qed
|
|
584 |
\end{proof}
|
|
585 |
|
|
586 |
\begin{theorem}\label{swapfreshfresh}
|
|
587 |
Let @{text x} be of permutation type.
|
|
588 |
@{thm [mode=IfThen] swap_fresh_fresh[no_vars]}
|
|
589 |
\end{theorem}
|
|
590 |
|
|
591 |
\begin{proof}
|
|
592 |
If @{text a} and @{text b} have different sort, then the swapping is the identity.
|
|
593 |
If they have the same sort, we know by definition of support that both
|
|
594 |
@{term "finite {c. (a \<rightleftharpoons> c) \<bullet> x \<noteq> x}"} and @{term "finite {c. (b \<rightleftharpoons> c) \<bullet> x \<noteq> x}"}
|
|
595 |
hold. So the union of these sets is finite too, and we know by Proposition~\ref{choosefresh}
|
|
596 |
that there is an atom @{term c}, with the same sort as @{term a} and @{term b},
|
|
597 |
that satisfies \mbox{@{term "(a \<rightleftharpoons> c) \<bullet> x = x"}} and @{term "(b \<rightleftharpoons> c) \<bullet> x = x"}.
|
|
598 |
Now the theorem follows from Lemma~\ref{swaptriple}.\hfill\qed
|
|
599 |
\end{proof}
|
|
600 |
|
|
601 |
\noindent
|
|
602 |
Two important properties that need to be established for later calculations is
|
|
603 |
that @{text "supp"} and freshness are equivariant. For this we first show that:
|
|
604 |
|
|
605 |
\begin{lemma}\label{half}
|
|
606 |
If @{term x} is a permutation type, then @{thm (lhs) fresh_permute_iff[where p="\<pi>",no_vars]}
|
|
607 |
if and only if @{thm (rhs) fresh_permute_iff[where p="\<pi>",no_vars]}.
|
|
608 |
\end{lemma}
|
|
609 |
|
|
610 |
\begin{proof}
|
|
611 |
\begin{isabelle}
|
|
612 |
\begin{tabular}[t]{c@ {\hspace{2mm}}l@ {\hspace{5mm}}l}
|
|
613 |
& \multicolumn{2}{@ {}l}{@{thm (lhs) fresh_permute_iff[where p="\<pi>",no_vars]} @{text "\<equiv>"}
|
|
614 |
@{term "finite {b. (\<pi> \<bullet> a \<rightleftharpoons> b) \<bullet> \<pi> \<bullet> x \<noteq> \<pi> \<bullet> x}"}}\\
|
|
615 |
@{text "\<Leftrightarrow>"}
|
|
616 |
& @{term "finite {b. (\<pi> \<bullet> a \<rightleftharpoons> \<pi> \<bullet> b) \<bullet> \<pi> \<bullet> x \<noteq> \<pi> \<bullet> x}"}
|
|
617 |
& since @{text "\<pi> \<bullet> _"} is bijective\\
|
|
618 |
@{text "\<Leftrightarrow>"}
|
|
619 |
& @{term "finite {b. \<pi> \<bullet> (a \<rightleftharpoons> b) \<bullet> x \<noteq> \<pi> \<bullet> x}"}
|
|
620 |
& by \eqref{permutecompose} and \eqref{swapeqvt}\\
|
|
621 |
@{text "\<Leftrightarrow>"}
|
|
622 |
& @{term "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"} @{text "\<equiv>"}
|
|
623 |
@{thm (rhs) fresh_permute_iff[where p="\<pi>",no_vars]}
|
|
624 |
& by \eqref{permuteequ}\\
|
|
625 |
\end{tabular}
|
|
626 |
\end{isabelle}\hfill\qed
|
|
627 |
\end{proof}
|
|
628 |
|
|
629 |
\noindent
|
|
630 |
Together with the definition of the permutation operation on booleans,
|
|
631 |
we can immediately infer equivariance of freshness:
|
|
632 |
|
|
633 |
@{thm [display,indent=10] fresh_eqvt[where p="\<pi>",no_vars]}
|
|
634 |
|
|
635 |
\noindent
|
|
636 |
Now equivariance of @{text "supp"}, namely
|
|
637 |
|
|
638 |
@{thm [display,indent=10] supp_eqvt[where p="\<pi>",no_vars]}
|
|
639 |
|
|
640 |
\noindent
|
|
641 |
is by noting that @{thm supp_conv_fresh[no_vars]} and that freshness and
|
|
642 |
the logical connectives are equivariant.
|
|
643 |
|
|
644 |
While the abstract properties of support and freshness, particularly
|
|
645 |
Theorem~\ref{swapfreshfresh}, are useful for developing Nominal Isabelle,
|
|
646 |
one often has to calculate the support of some concrete object. This is
|
|
647 |
straightforward for example for booleans, nats, products and lists:
|
|
648 |
|
2523
|
649 |
\begin{equation}
|
|
650 |
\mbox{
|
1785
|
651 |
\begin{tabular}{@ {}r@ {\hspace{2mm}}l}
|
|
652 |
@{text "booleans"}: & @{term "supp b = {}"}\\
|
|
653 |
@{text "nats"}: & @{term "supp n = {}"}\\
|
|
654 |
@{text "products"}: & @{thm supp_Pair[no_vars]}\\
|
|
655 |
@{text "lists:"} & @{thm supp_Nil[no_vars]}\\
|
|
656 |
& @{thm supp_Cons[no_vars]}\\
|
2523
|
657 |
\end{tabular}}
|
|
658 |
\end{equation}
|
1785
|
659 |
|
|
660 |
\noindent
|
2523
|
661 |
But establishing the support of atoms and permutations is a bit
|
1785
|
662 |
trickier. To do so we will use the following notion about a \emph{supporting set}.
|
|
663 |
|
|
664 |
\begin{definition}
|
|
665 |
A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}
|
|
666 |
not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.
|
|
667 |
\end{definition}
|
|
668 |
|
|
669 |
\noindent
|
|
670 |
The main motivation for this notion is that we can characterise @{text "supp x"}
|
|
671 |
as the smallest finite set that supports @{text "x"}. For this we prove:
|
|
672 |
|
|
673 |
\begin{lemma}\label{supports} Let @{text x} be of permutation type.
|
|
674 |
\begin{isabelle}
|
|
675 |
\begin{tabular}{r@ {\hspace{4mm}}p{10cm}}
|
|
676 |
i) & @{thm[mode=IfThen] supp_is_subset[no_vars]}\\
|
|
677 |
ii) & @{thm[mode=IfThen] supp_supports[no_vars]}\\
|
|
678 |
iii) & @{thm (concl) supp_is_least_supports[no_vars]}
|
|
679 |
provided @{thm (prem 1) supp_is_least_supports[no_vars]},
|
|
680 |
@{thm (prem 2) supp_is_least_supports[no_vars]}
|
|
681 |
and @{text "S"} is the least such set, that means formally,
|
|
682 |
for all @{text "S'"}, if @{term "finite S'"} and
|
|
683 |
@{term "S' supports x"} then @{text "S \<subseteq> S'"}.
|
|
684 |
\end{tabular}
|
|
685 |
\end{isabelle}
|
|
686 |
\end{lemma}
|
|
687 |
|
|
688 |
\begin{proof}
|
|
689 |
For @{text "i)"} we derive a contradiction by assuming there is an atom @{text a}
|
|
690 |
with @{term "a \<in> supp x"} and @{text "a \<notin> S"}. Using the second fact, the
|
|
691 |
assumption that @{term "S supports x"} gives us that @{text S} is a superset of
|
|
692 |
@{term "{b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"}, which is finite by the assumption of @{text S}
|
|
693 |
being finite. But this means @{term "a \<notin> supp x"}, contradicting our assumption.
|
|
694 |
Property @{text "ii)"} is by a direct application of
|
|
695 |
Theorem~\ref{swapfreshfresh}. For the last property, part @{text "i)"} proves
|
|
696 |
one ``half'' of the claimed equation. The other ``half'' is by property
|
|
697 |
@{text "ii)"} and the fact that @{term "supp x"} is finite by @{text "i)"}.\hfill\qed
|
|
698 |
\end{proof}
|
|
699 |
|
|
700 |
\noindent
|
|
701 |
These are all relatively straightforward proofs adapted from the existing
|
|
702 |
nominal logic work. However for establishing the support of atoms and
|
|
703 |
permutations we found the following ``optimised'' variant of @{text "iii)"}
|
|
704 |
more useful:
|
|
705 |
|
|
706 |
\begin{lemma}\label{optimised} Let @{text x} be of permutation type.
|
|
707 |
We have that @{thm (concl) finite_supp_unique[no_vars]}
|
|
708 |
provided @{thm (prem 1) finite_supp_unique[no_vars]},
|
|
709 |
@{thm (prem 2) finite_supp_unique[no_vars]}, and for
|
|
710 |
all @{text "a \<in> S"} and all @{text "b \<notin> S"}, with @{text a}
|
1809
|
711 |
and @{text b} having the same sort, \mbox{@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"}}
|
1785
|
712 |
\end{lemma}
|
|
713 |
|
|
714 |
\begin{proof}
|
|
715 |
By Lemma \ref{supports}@{text ".iii)"} we have to show that for every finite
|
|
716 |
set @{text S'} that supports @{text x}, \mbox{@{text "S \<subseteq> S'"}} holds. We will
|
|
717 |
assume that there is an atom @{text "a"} that is element of @{text S}, but
|
|
718 |
not @{text "S'"} and derive a contradiction. Since both @{text S} and
|
|
719 |
@{text S'} are finite, we can by Proposition \ref{choosefresh} obtain an atom
|
|
720 |
@{text b}, which has the same sort as @{text "a"} and for which we know
|
|
721 |
@{text "b \<notin> S"} and @{text "b \<notin> S'"}. Since we assumed @{text "a \<notin> S'"} and
|
|
722 |
we have that @{text "S' supports x"}, we have on one hand @{term "(a \<rightleftharpoons> b) \<bullet> x
|
|
723 |
= x"}. On the other hand, the fact @{text "a \<in> S"} and @{text "b \<notin> S"} imply
|
|
724 |
@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"} using the assumed implication. This gives us the
|
|
725 |
contradiction.\hfill\qed
|
|
726 |
\end{proof}
|
|
727 |
|
|
728 |
\noindent
|
|
729 |
Using this lemma we only have to show the following three proof-obligations
|
|
730 |
|
|
731 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
732 |
\begin{tabular}{@ {}r@ {\hspace{4mm}}l}
|
|
733 |
i) & @{term "{c} supports c"}\\
|
|
734 |
ii) & @{term "finite {c}"}\\
|
|
735 |
iii) & @{text "\<forall>a \<in> {c} b \<notin> {c}. sort a = sort b \<longrightarrow> (a b) \<bullet> c \<noteq> c"}
|
|
736 |
\end{tabular}
|
|
737 |
\end{isabelle}
|
|
738 |
|
|
739 |
\noindent
|
|
740 |
in order to establish that @{thm supp_atom[where a="c", no_vars]} holds. In
|
|
741 |
Isabelle/HOL these proof-obligations can be discharged by easy
|
|
742 |
simplifications. Similar proof-obligations arise for the support of
|
|
743 |
permutations, which is
|
|
744 |
|
|
745 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
746 |
\begin{tabular}{@ {}l}
|
|
747 |
@{thm supp_perm[where p="\<pi>", no_vars]}
|
|
748 |
\end{tabular}
|
|
749 |
\end{isabelle}
|
|
750 |
|
|
751 |
\noindent
|
|
752 |
The only proof-obligation that is
|
|
753 |
interesting is the one where we have to show that
|
|
754 |
|
|
755 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
756 |
\begin{tabular}{@ {}l}
|
|
757 |
@{text "If \<pi> \<bullet> a \<noteq> a, \<pi> \<bullet> b = b and sort a = sort b, then (a b) \<bullet> \<pi> \<noteq> \<pi>"}.
|
|
758 |
\end{tabular}
|
|
759 |
\end{isabelle}
|
|
760 |
|
|
761 |
\noindent
|
|
762 |
For this we observe that
|
|
763 |
|
|
764 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
765 |
\begin{tabular}{@ {}rcl}
|
|
766 |
@{thm (lhs) perm_swap_eq[where p="\<pi>", no_vars]} &
|
|
767 |
if and only if &
|
|
768 |
@{thm (rhs) perm_swap_eq[where p="\<pi>", no_vars]}
|
|
769 |
\end{tabular}
|
|
770 |
\end{isabelle}
|
|
771 |
|
|
772 |
\noindent
|
|
773 |
holds by a simple calculation using the group properties of permutations.
|
|
774 |
The proof-obligation can then be discharged by analysing the inequality
|
|
775 |
between the permutations @{term "(\<pi> \<bullet> a \<rightleftharpoons> b)"} and @{term "(a \<rightleftharpoons> b)"}.
|
|
776 |
|
|
777 |
The main point about support is that whenever an object @{text x} has finite
|
|
778 |
support, then Proposition~\ref{choosefresh} allows us to choose for @{text x} a
|
|
779 |
fresh atom with arbitrary sort. This is an important operation in Nominal
|
|
780 |
Isabelle in situations where, for example, a bound variable needs to be
|
2523
|
781 |
renamed. To allow such a choice, we only have to assume that
|
|
782 |
@{text "finite (supp x)"} holds. For more convenience we
|
1785
|
783 |
can define a type class for types where every element has finite support, and
|
|
784 |
prove that the types @{term "atom"}, @{term "perm"}, lists, products and
|
2523
|
785 |
booleans are instances of this type class.
|
1785
|
786 |
|
2523
|
787 |
Unfortunately, this does not work for sets or Isabelle/HOL's function
|
|
788 |
type.\footnote{Isabelle/HOL takes the type @{text "\<alpha> set"} as an abbreviation
|
|
789 |
of @{text "\<alpha> \<Rightarrow> bool"}.} There are functions and sets definable in
|
|
790 |
Isabelle/HOL for which the finite support property does not hold. A simple
|
|
791 |
example of a function with infinite support is the function that returns the
|
|
792 |
natural number of an atom
|
|
793 |
|
1785
|
794 |
@{text [display, indent=10] "nat_of (Atom s i) \<equiv> i"}
|
|
795 |
|
|
796 |
\noindent
|
|
797 |
This function's support is the set of \emph{all} atoms. To establish this we show @{term "\<not> a \<sharp> nat_of"}.
|
|
798 |
This is equivalent to assuming the set @{term "{b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"} is finite
|
|
799 |
and deriving a contradiction. From the assumption we also know that
|
|
800 |
@{term "{a} \<union> {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"} is finite. Then we can use
|
|
801 |
Proposition~\ref{choosefresh} to choose an atom @{text c} such that
|
|
802 |
@{term "c \<noteq> a"}, @{term "sort_of c = sort_of a"} and @{term "(a \<rightleftharpoons> c) \<bullet> nat_of = nat_of"}.
|
|
803 |
Now we can reason as follows:
|
|
804 |
|
|
805 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
806 |
\begin{tabular}[b]{@ {}rcl@ {\hspace{5mm}}l}
|
|
807 |
@{text "nat_of a"} & @{text "="} & @{text "(a \<rightleftharpoons> c) \<bullet> (nat_of a)"} & by def.~of permutations on nats\\
|
|
808 |
& @{text "="} & @{term "((a \<rightleftharpoons> c) \<bullet> nat_of) ((a \<rightleftharpoons> c) \<bullet> a)"} & by \eqref{permutefunapp}\\
|
|
809 |
& @{text "="} & @{term "nat_of c"} & by assumptions on @{text c}\\
|
|
810 |
\end{tabular}
|
|
811 |
\end{isabelle}
|
|
812 |
|
|
813 |
\noindent
|
|
814 |
But this means we have that @{term "nat_of a = nat_of c"} and @{term "sort_of a = sort_of c"}.
|
|
815 |
This implies that atoms @{term a} and @{term c} must be equal, which clashes with our
|
|
816 |
assumption @{term "c \<noteq> a"} about how we chose @{text c}.
|
|
817 |
Cheney \cite{Cheney06} gives similar examples for constructions that have infinite support.
|
|
818 |
*}
|
|
819 |
|
2033
|
820 |
section {* Support of Finite Sets *}
|
|
821 |
|
|
822 |
text {*
|
2523
|
823 |
As shown above, sets is one instance of a type that is not generally finitely supported.
|
|
824 |
However, we can easily show that finite sets of atoms are finitely
|
2033
|
825 |
supported, because their support can be characterised as:
|
|
826 |
|
|
827 |
\begin{lemma}\label{finatomsets}
|
|
828 |
If @{text S} is a finite set of atoms, then @{thm (concl) supp_finite_atom_set[no_vars]}.
|
|
829 |
\end{lemma}
|
|
830 |
|
|
831 |
\begin{proof}
|
|
832 |
finite-supp-unique
|
|
833 |
\end{proof}
|
|
834 |
|
2523
|
835 |
\noindent
|
|
836 |
More difficult, however, is it to establish that finite sets of finitely
|
2033
|
837 |
supported objects are finitely supported.
|
|
838 |
*}
|
|
839 |
|
|
840 |
|
1785
|
841 |
section {* Induction Principles *}
|
|
842 |
|
2033
|
843 |
text {*
|
|
844 |
While the use of functions as permutation provides us with a unique
|
|
845 |
representation for permutations (for example @{term "(a \<rightleftharpoons> b)"} and
|
|
846 |
@{term "(b \<rightleftharpoons> a)"} are equal permutations), this representation has
|
|
847 |
one draw back: it does not come readily with an induction principle.
|
|
848 |
Such an induction principle is handy for deriving properties like
|
|
849 |
|
2523
|
850 |
@{thm [display, indent=10] supp_perm_eq[no_vars]}
|
1785
|
851 |
|
2033
|
852 |
\noindent
|
|
853 |
However, it is not too difficult to derive an induction principle,
|
|
854 |
given the fact that we allow only permutations with a finite domain.
|
|
855 |
*}
|
1785
|
856 |
|
|
857 |
|
2522
|
858 |
section {* An Abstraction Type *}
|
|
859 |
|
|
860 |
text {*
|
|
861 |
To that end, we will consider
|
|
862 |
first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}. These pairs
|
|
863 |
are intended to represent the abstraction, or binding, of the set of atoms @{text
|
|
864 |
"as"} in the body @{text "x"}.
|
|
865 |
|
|
866 |
The first question we have to answer is when two pairs @{text "(as, x)"} and
|
|
867 |
@{text "(bs, y)"} are $\alpha$-equivalent? (For the moment we are interested in
|
|
868 |
the notion of $\alpha$-equivalence that is \emph{not} preserved by adding
|
|
869 |
vacuous binders.) To answer this question, we identify four conditions: {\it (i)}
|
|
870 |
given a free-atom function @{text "fa"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
|
|
871 |
set"}}, then @{text x} and @{text y} need to have the same set of free
|
|
872 |
atoms; moreover there must be a permutation @{text p} such that {\it
|
|
873 |
(ii)} @{text p} leaves the free atoms of @{text x} and @{text y} unchanged, but
|
|
874 |
{\it (iii)} ``moves'' their bound names so that we obtain modulo a relation,
|
|
875 |
say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)}
|
|
876 |
@{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
|
|
877 |
requirements {\it (i)} to {\it (iv)} can be stated formally as follows:
|
|
878 |
%
|
|
879 |
\begin{equation}\label{alphaset}
|
|
880 |
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
|
|
881 |
\multicolumn{3}{l}{@{text "(as, x) \<approx>set R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
|
|
882 |
& @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\
|
|
883 |
@{text "\<and>"} & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
|
|
884 |
@{text "\<and>"} & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
|
|
885 |
@{text "\<and>"} & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\
|
|
886 |
\end{array}
|
|
887 |
\end{equation}
|
|
888 |
|
|
889 |
\noindent
|
|
890 |
Note that this relation depends on the permutation @{text
|
|
891 |
"p"}; $\alpha$-equivalence between two pairs is then the relation where we
|
|
892 |
existentially quantify over this @{text "p"}. Also note that the relation is
|
|
893 |
dependent on a free-atom function @{text "fa"} and a relation @{text
|
|
894 |
"R"}. The reason for this extra generality is that we will use
|
|
895 |
$\approx_{\,\textit{set}}$ for both ``raw'' terms and $\alpha$-equated terms. In
|
|
896 |
the latter case, @{text R} will be replaced by equality @{text "="} and we
|
|
897 |
will prove that @{text "fa"} is equal to @{text "supp"}.
|
|
898 |
|
|
899 |
It might be useful to consider first some examples about how these definitions
|
|
900 |
of $\alpha$-equivalence pan out in practice. For this consider the case of
|
|
901 |
abstracting a set of atoms over types (as in type-schemes). We set
|
|
902 |
@{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we
|
|
903 |
define
|
|
904 |
|
|
905 |
\begin{center}
|
|
906 |
@{text "fa(x) = {x}"} \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) = fa(T\<^isub>1) \<union> fa(T\<^isub>2)"}
|
|
907 |
\end{center}
|
|
908 |
|
|
909 |
\noindent
|
|
910 |
Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and
|
|
911 |
\eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and
|
|
912 |
@{text "({y, x}, y \<rightarrow> x)"} are $\alpha$-equivalent according to
|
|
913 |
$\approx_{\,\textit{set}}$ and $\approx_{\,\textit{res}}$ by taking @{text p} to
|
|
914 |
be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then @{text
|
|
915 |
"([x, y], x \<rightarrow> y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"}
|
|
916 |
since there is no permutation that makes the lists @{text "[x, y]"} and
|
|
917 |
@{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \<rightarrow> y"}}
|
|
918 |
unchanged. Another example is @{text "({x}, x)"} $\approx_{\,\textit{res}}$
|
|
919 |
@{text "({x, y}, x)"} which holds by taking @{text p} to be the identity
|
|
920 |
permutation. However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}
|
|
921 |
$\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no
|
|
922 |
permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal
|
|
923 |
(similarly for $\approx_{\,\textit{list}}$). It can also relatively easily be
|
|
924 |
shown that all three notions of $\alpha$-equivalence coincide, if we only
|
|
925 |
abstract a single atom.
|
|
926 |
|
|
927 |
In the rest of this section we are going to introduce three abstraction
|
|
928 |
types. For this we define
|
|
929 |
%
|
|
930 |
\begin{equation}
|
|
931 |
@{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_set (as, x) equal supp p (bs, x)"}
|
|
932 |
\end{equation}
|
|
933 |
|
|
934 |
\noindent
|
|
935 |
(similarly for $\approx_{\,\textit{abs\_res}}$
|
|
936 |
and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence
|
|
937 |
relations and equivariant.
|
|
938 |
|
|
939 |
\begin{lemma}\label{alphaeq}
|
|
940 |
The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$
|
|
941 |
and $\approx_{\,\textit{abs\_res}}$ are equivalence relations, and if @{term
|
|
942 |
"abs_set (as, x) (bs, y)"} then also @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet>
|
|
943 |
bs, p \<bullet> y)"} (similarly for the other two relations).
|
|
944 |
\end{lemma}
|
|
945 |
|
|
946 |
\begin{proof}
|
|
947 |
Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have
|
|
948 |
a permutation @{text p} and for the proof obligation take @{term "-p"}. In case
|
|
949 |
of transitivity, we have two permutations @{text p} and @{text q}, and for the
|
|
950 |
proof obligation use @{text "q + p"}. All conditions are then by simple
|
|
951 |
calculations.
|
|
952 |
\end{proof}
|
|
953 |
|
|
954 |
\noindent
|
|
955 |
This lemma allows us to use our quotient package for introducing
|
|
956 |
new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}
|
|
957 |
representing $\alpha$-equivalence classes of pairs of type
|
|
958 |
@{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}
|
|
959 |
(in the third case).
|
|
960 |
The elements in these types will be, respectively, written as:
|
|
961 |
|
|
962 |
\begin{center}
|
|
963 |
@{term "Abs_set as x"} \hspace{5mm}
|
|
964 |
@{term "Abs_res as x"} \hspace{5mm}
|
|
965 |
@{term "Abs_lst as x"}
|
|
966 |
\end{center}
|
|
967 |
|
|
968 |
\noindent
|
|
969 |
indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will
|
|
970 |
call the types \emph{abstraction types} and their elements
|
|
971 |
\emph{abstractions}. The important property we need to derive is the support of
|
|
972 |
abstractions, namely:
|
|
973 |
|
|
974 |
\begin{theorem}[Support of Abstractions]\label{suppabs}
|
|
975 |
Assuming @{text x} has finite support, then\\[-6mm]
|
|
976 |
\begin{center}
|
|
977 |
\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
|
|
978 |
%@ {thm (lhs) supp_abs(1)[no_vars]} & $=$ & @ {thm (rhs) supp_abs(1)[no_vars]}\\
|
|
979 |
%@ {thm (lhs) supp_abs(2)[no_vars]} & $=$ & @ {thm (rhs) supp_abs(2)[no_vars]}\\
|
|
980 |
%@ {thm (lhs) supp_abs(3)[where bs="as", no_vars]} & $=$ & @ {thm (rhs) supp_abs(3)[where bs="as", no_vars]}
|
|
981 |
\end{tabular}
|
|
982 |
\end{center}
|
|
983 |
\end{theorem}
|
|
984 |
|
|
985 |
\noindent
|
|
986 |
Below we will show the first equation. The others
|
|
987 |
follow by similar arguments. By definition of the abstraction type @{text "abs_set"}
|
|
988 |
we have
|
|
989 |
%
|
|
990 |
\begin{equation}\label{abseqiff}
|
|
991 |
%@ {thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\;
|
|
992 |
%@ {thm (rhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}
|
|
993 |
\end{equation}
|
|
994 |
|
|
995 |
\noindent
|
|
996 |
and also
|
|
997 |
%
|
|
998 |
\begin{equation}\label{absperm}
|
|
999 |
@{thm permute_Abs[no_vars]}
|
|
1000 |
\end{equation}
|
|
1001 |
|
|
1002 |
\noindent
|
|
1003 |
The second fact derives from the definition of permutations acting on pairs
|
|
1004 |
\eqref{permute} and $\alpha$-equivalence being equivariant
|
|
1005 |
(see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show
|
|
1006 |
the following lemma about swapping two atoms in an abstraction.
|
|
1007 |
|
|
1008 |
\begin{lemma}
|
|
1009 |
%@ {thm[mode=IfThen] abs_swap1(1)[where bs="as", no_vars]}
|
|
1010 |
\end{lemma}
|
|
1011 |
|
|
1012 |
\begin{proof}
|
|
1013 |
This lemma is straightforward using \eqref{abseqiff} and observing that
|
|
1014 |
the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.
|
|
1015 |
Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}).
|
|
1016 |
\end{proof}
|
|
1017 |
|
|
1018 |
\noindent
|
|
1019 |
Assuming that @{text "x"} has finite support, this lemma together
|
|
1020 |
with \eqref{absperm} allows us to show
|
|
1021 |
%
|
|
1022 |
\begin{equation}\label{halfone}
|
|
1023 |
%@ {thm abs_supports(1)[no_vars]}
|
|
1024 |
\end{equation}
|
|
1025 |
|
|
1026 |
\noindent
|
|
1027 |
which by Property~\ref{supportsprop} gives us ``one half'' of
|
|
1028 |
Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish
|
|
1029 |
it, we use a trick from \cite{Pitts04} and first define an auxiliary
|
|
1030 |
function @{text aux}, taking an abstraction as argument:
|
|
1031 |
%
|
|
1032 |
\begin{center}
|
|
1033 |
@{thm supp_set.simps[THEN eq_reflection, no_vars]}
|
|
1034 |
\end{center}
|
|
1035 |
|
|
1036 |
\noindent
|
|
1037 |
Using the second equation in \eqref{equivariance}, we can show that
|
|
1038 |
@{text "aux"} is equivariant (since @{term "p \<bullet> (supp x - as) =
|
|
1039 |
(supp (p \<bullet> x)) - (p \<bullet> as)"}) and therefore has empty support.
|
|
1040 |
This in turn means
|
|
1041 |
%
|
|
1042 |
\begin{center}
|
|
1043 |
@{term "supp (supp_gen (Abs_set as x)) \<subseteq> supp (Abs_set as x)"}
|
|
1044 |
\end{center}
|
|
1045 |
|
|
1046 |
\noindent
|
|
1047 |
using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set,
|
|
1048 |
we further obtain
|
|
1049 |
%
|
|
1050 |
\begin{equation}\label{halftwo}
|
|
1051 |
%@ {thm (concl) supp_abs_subset1(1)[no_vars]}
|
|
1052 |
\end{equation}
|
|
1053 |
|
|
1054 |
\noindent
|
|
1055 |
since for finite sets of atoms, @{text "bs"}, we have
|
|
1056 |
@{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
|
|
1057 |
Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes
|
|
1058 |
Theorem~\ref{suppabs}.
|
|
1059 |
|
|
1060 |
The method of first considering abstractions of the
|
|
1061 |
form @{term "Abs_set as x"} etc is motivated by the fact that
|
|
1062 |
we can conveniently establish at the Isabelle/HOL level
|
|
1063 |
properties about them. It would be
|
|
1064 |
laborious to write custom ML-code that derives automatically such properties
|
|
1065 |
for every term-constructor that binds some atoms. Also the generality of
|
|
1066 |
the definitions for $\alpha$-equivalence will help us in the next section.
|
|
1067 |
*}
|
|
1068 |
|
|
1069 |
|
1785
|
1070 |
section {* Concrete Atom Types *}
|
|
1071 |
|
|
1072 |
text {*
|
|
1073 |
|
|
1074 |
So far, we have presented a system that uses only a single multi-sorted atom
|
|
1075 |
type. This design gives us the flexibility to define operations and prove
|
|
1076 |
theorems that are generic with respect to atom sorts. For example, as
|
|
1077 |
illustrated above the @{term supp} function returns a set that includes the
|
|
1078 |
free atoms of \emph{all} sorts together; the flexibility offered by the new
|
|
1079 |
atom type makes this possible.
|
|
1080 |
|
|
1081 |
However, the single multi-sorted atom type does not make an ideal interface
|
|
1082 |
for end-users of Nominal Isabelle. If sorts are not distinguished by
|
|
1083 |
Isabelle's type system, users must reason about atom sorts manually. That
|
|
1084 |
means subgoals involving sorts must be discharged explicitly within proof
|
|
1085 |
scripts, instead of being inferred by Isabelle/HOL's type checker. In other
|
|
1086 |
cases, lemmas might require additional side conditions about sorts to be true.
|
|
1087 |
For example, swapping @{text a} and @{text b} in the pair \mbox{@{term "(a,
|
|
1088 |
b)"}} will only produce the expected result if we state the lemma in
|
|
1089 |
Isabelle/HOL as:
|
|
1090 |
*}
|
|
1091 |
|
|
1092 |
lemma
|
|
1093 |
fixes a b :: "atom"
|
|
1094 |
assumes asm: "sort a = sort b"
|
|
1095 |
shows "(a \<rightleftharpoons> b) \<bullet> (a, b) = (b, a)"
|
|
1096 |
using asm by simp
|
|
1097 |
|
|
1098 |
text {*
|
|
1099 |
\noindent
|
|
1100 |
Fortunately, it is possible to regain most of the type-checking automation
|
|
1101 |
that is lost by moving to a single atom type. We accomplish this by defining
|
|
1102 |
\emph{subtypes} of the generic atom type that only include atoms of a single
|
|
1103 |
specific sort. We call such subtypes \emph{concrete atom types}.
|
|
1104 |
|
|
1105 |
The following Isabelle/HOL command defines a concrete atom type called
|
|
1106 |
\emph{name}, which consists of atoms whose sort equals the string @{term
|
|
1107 |
"''name''"}.
|
|
1108 |
|
|
1109 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
1110 |
\isacommand{typedef}\ \ @{typ name} = @{term "{a. sort\<iota> a = ''name''}"}
|
|
1111 |
\end{isabelle}
|
|
1112 |
|
|
1113 |
\noindent
|
|
1114 |
This command automatically generates injective functions that map from the
|
|
1115 |
concrete atom type into the generic atom type and back, called
|
|
1116 |
representation and abstraction functions, respectively. We will write these
|
|
1117 |
functions as follows:
|
|
1118 |
|
|
1119 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
1120 |
\begin{tabular}{@ {}l@ {\hspace{10mm}}l}
|
|
1121 |
@{text "\<lfloor>_\<rfloor> :: name \<Rightarrow> atom"} &
|
|
1122 |
@{text "\<lceil>_\<rceil> :: atom \<Rightarrow> name"}
|
|
1123 |
\end{tabular}
|
|
1124 |
\end{isabelle}
|
|
1125 |
|
|
1126 |
\noindent
|
|
1127 |
With the definition @{thm permute_name_def [where p="\<pi>", THEN
|
|
1128 |
eq_reflection, no_vars]}, it is straightforward to verify that the type
|
|
1129 |
@{typ name} is a permutation type.
|
|
1130 |
|
|
1131 |
In order to reason uniformly about arbitrary concrete atom types, we define a
|
|
1132 |
type class that characterises type @{typ name} and other similarly-defined
|
|
1133 |
types. The definition of the concrete atom type class is as follows: First,
|
|
1134 |
every concrete atom type must be a permutation type. In addition, the class
|
|
1135 |
defines an overloaded function that maps from the concrete type into the
|
|
1136 |
generic atom type, which we will write @{text "|_|"}. For each class
|
|
1137 |
instance, this function must be injective and equivariant, and its outputs
|
|
1138 |
must all have the same sort, that is
|
|
1139 |
|
|
1140 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
1141 |
\begin{tabular}{r@ {\hspace{3mm}}l}
|
|
1142 |
i) if @{thm (lhs) atom_eq_iff [no_vars]} then @{thm (rhs) atom_eq_iff [no_vars]}\\
|
|
1143 |
ii) @{thm atom_eqvt[where p="\<pi>", no_vars]}\\
|
|
1144 |
iii) @{thm sort_of_atom_eq [no_vars]}
|
|
1145 |
\end{tabular}\hfill\numbered{atomprops}
|
|
1146 |
\end{isabelle}
|
|
1147 |
|
|
1148 |
\noindent
|
|
1149 |
With the definition @{thm atom_name_def [THEN eq_reflection, no_vars]} we can
|
|
1150 |
show that @{typ name} satisfies all the above requirements of a concrete atom
|
|
1151 |
type.
|
|
1152 |
|
|
1153 |
The whole point of defining the concrete atom type class was to let users
|
|
1154 |
avoid explicit reasoning about sorts. This benefit is realised by defining a
|
|
1155 |
special swapping operation of type @{text "\<alpha> \<Rightarrow> \<alpha>
|
|
1156 |
\<Rightarrow> perm"}, where @{text "\<alpha>"} is a concrete atom type:
|
|
1157 |
|
|
1158 |
@{thm [display,indent=10] flip_def [THEN eq_reflection, no_vars]}
|
|
1159 |
|
|
1160 |
\noindent
|
|
1161 |
As a consequence of its type, the @{text "\<leftrightarrow>"}-swapping
|
|
1162 |
operation works just like the generic swapping operation, but it does not
|
|
1163 |
require any sort-checking side conditions---the sort-correctness is ensured by
|
|
1164 |
the types! For @{text "\<leftrightarrow>"} we can establish the following
|
|
1165 |
simplification rule:
|
|
1166 |
|
|
1167 |
@{thm [display,indent=10] permute_flip_at[no_vars]}
|
|
1168 |
|
|
1169 |
\noindent
|
|
1170 |
If we now want to swap the \emph{concrete} atoms @{text a} and @{text b}
|
|
1171 |
in the pair @{term "(a, b)"} we can establish the lemma as follows:
|
|
1172 |
*}
|
|
1173 |
|
|
1174 |
lemma
|
|
1175 |
fixes a b :: "name"
|
|
1176 |
shows "(a \<leftrightarrow> b) \<bullet> (a, b) = (b, a)"
|
|
1177 |
by simp
|
|
1178 |
|
|
1179 |
text {*
|
|
1180 |
\noindent
|
|
1181 |
There is no need to state an explicit premise involving sorts.
|
|
1182 |
|
|
1183 |
We can automate the process of creating concrete atom types, so that users
|
|
1184 |
can define a new one simply by issuing the command
|
|
1185 |
|
|
1186 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
1187 |
\begin{tabular}{@ {}l}
|
|
1188 |
\isacommand{atom\_decl}~~@{text "name"}
|
|
1189 |
\end{tabular}
|
|
1190 |
\end{isabelle}
|
|
1191 |
|
|
1192 |
\noindent
|
|
1193 |
This command can be implemented using less than 100 lines of custom ML-code.
|
|
1194 |
In comparison, the old version of Nominal Isabelle included more than 1000
|
|
1195 |
lines of ML-code for creating concrete atom types, and for defining various
|
|
1196 |
type classes and instantiating generic lemmas for them. In addition to
|
|
1197 |
simplifying the ML-code, the setup here also offers user-visible improvements:
|
|
1198 |
Now concrete atoms can be declared at any point of a formalisation, and
|
|
1199 |
theories that separately declare different atom types can be merged
|
|
1200 |
together---it is no longer required to collect all atom declarations in one
|
|
1201 |
place.
|
|
1202 |
*}
|
|
1203 |
|
|
1204 |
|
|
1205 |
section {* Multi-Sorted Concrete Atoms *}
|
|
1206 |
|
|
1207 |
(*<*)
|
|
1208 |
datatype ty = TVar string | Fun ty ty ("_ \<rightarrow> _")
|
|
1209 |
(*>*)
|
|
1210 |
|
|
1211 |
text {*
|
|
1212 |
The formalisation presented so far allows us to streamline proofs and reduce
|
|
1213 |
the amount of custom ML-code in the existing implementation of Nominal
|
|
1214 |
Isabelle. In this section we describe a mechanism that extends the
|
|
1215 |
capabilities of Nominal Isabelle. This mechanism is about variables with
|
|
1216 |
additional information, for example typing constraints.
|
|
1217 |
While we leave a detailed treatment of binders and binding of variables for a
|
|
1218 |
later paper, we will have a look here at how such variables can be
|
|
1219 |
represented by concrete atoms.
|
|
1220 |
|
|
1221 |
In the previous section we considered concrete atoms that can be used in
|
|
1222 |
simple binders like \emph{@{text "\<lambda>x. x"}}. Such concrete atoms do
|
|
1223 |
not carry any information beyond their identities---comparing for equality
|
|
1224 |
is really the only way to analyse ordinary concrete atoms.
|
|
1225 |
However, in ``Church-style'' lambda-terms \cite{Church40} and in the terms
|
|
1226 |
underlying HOL-systems \cite{PittsHOL4} binders and bound variables have a
|
|
1227 |
more complicated structure. For example in the ``Church-style'' lambda-term
|
|
1228 |
|
|
1229 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
1230 |
\begin{tabular}{@ {}l}
|
|
1231 |
@{text "\<lambda>x\<^isub>\<alpha>. x\<^isub>\<alpha> x\<^isub>\<beta>"}
|
|
1232 |
\end{tabular}\hfill\numbered{church}
|
|
1233 |
\end{isabelle}
|
|
1234 |
|
|
1235 |
\noindent
|
|
1236 |
both variables and binders include typing information indicated by @{text \<alpha>}
|
|
1237 |
and @{text \<beta>}. In this setting, we treat @{text "x\<^isub>\<alpha>"} and @{text
|
|
1238 |
"x\<^isub>\<beta>"} as distinct variables (assuming @{term "\<alpha>\<noteq>\<beta>"}) so that the
|
|
1239 |
variable @{text "x\<^isub>\<alpha>"} is bound by the lambda-abstraction, but not
|
|
1240 |
@{text "x\<^isub>\<beta>"}.
|
|
1241 |
|
|
1242 |
To illustrate how we can deal with this phenomenon, let us represent object
|
|
1243 |
types like @{text \<alpha>} and @{text \<beta>} by the datatype
|
|
1244 |
|
|
1245 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
1246 |
\begin{tabular}{@ {}l}
|
|
1247 |
\isacommand{datatype}~~@{text "ty = TVar string | ty \<rightarrow> ty"}
|
|
1248 |
\end{tabular}
|
|
1249 |
\end{isabelle}
|
|
1250 |
|
|
1251 |
\noindent
|
|
1252 |
If we attempt to encode a variable naively as a pair of a @{text name} and a @{text ty}, we have the
|
|
1253 |
problem that a swapping, say @{term "(x \<leftrightarrow> y)"}, applied to the pair @{text "((x, \<alpha>), (x, \<beta>))"}
|
|
1254 |
will always permute \emph{both} occurrences of @{text x}, even if the types
|
|
1255 |
@{text "\<alpha>"} and @{text "\<beta>"} are different. This is unwanted, because it will
|
|
1256 |
eventually mean that both occurrences of @{text x} will become bound by a
|
|
1257 |
corresponding binder.
|
|
1258 |
|
|
1259 |
Another attempt might be to define variables as an instance of the concrete
|
|
1260 |
atom type class, where a @{text ty} is somehow encoded within each variable.
|
|
1261 |
Remember we defined atoms as the datatype:
|
|
1262 |
*}
|
|
1263 |
|
|
1264 |
datatype atom\<iota>\<iota> = Atom\<iota>\<iota> string nat
|
|
1265 |
|
|
1266 |
text {*
|
|
1267 |
\noindent
|
|
1268 |
Considering our method of defining concrete atom types, the usage of a string
|
|
1269 |
for the sort of atoms seems a natural choice. However, none of the results so
|
|
1270 |
far depend on this choice and we are free to change it.
|
|
1271 |
One possibility is to encode types or any other information by making the sort
|
|
1272 |
argument parametric as follows:
|
|
1273 |
*}
|
|
1274 |
|
|
1275 |
datatype 'a \<iota>atom\<iota>\<iota>\<iota> = \<iota>Atom\<iota>\<iota> 'a nat
|
|
1276 |
|
|
1277 |
text {*
|
|
1278 |
\noindent
|
|
1279 |
The problem with this possibility is that we are then back in the old
|
|
1280 |
situation where our permutation operation is parametric in two types and
|
|
1281 |
this would require to work around Isabelle/HOL's restriction on type
|
|
1282 |
classes. Fortunately, encoding the types in a separate parameter is not
|
|
1283 |
necessary for what we want to achieve, as we only have to know when two
|
|
1284 |
types are equal or not. The solution is to use a different sort for each
|
|
1285 |
object type. Then we can use the fact that permutations respect \emph{sorts} to
|
|
1286 |
ensure that permutations also respect \emph{object types}. In order to do
|
|
1287 |
this, we must define an injective function @{text "sort_ty"} mapping from
|
|
1288 |
object types to sorts. For defining functions like @{text "sort_ty"}, it is
|
|
1289 |
more convenient to use a tree datatype for sorts. Therefore we define
|
|
1290 |
*}
|
|
1291 |
|
|
1292 |
datatype sort = Sort string "(sort list)"
|
|
1293 |
datatype atom\<iota>\<iota>\<iota>\<iota> = Atom\<iota>\<iota>\<iota>\<iota> sort nat
|
|
1294 |
|
|
1295 |
text {*
|
|
1296 |
\noindent
|
|
1297 |
With this definition,
|
|
1298 |
the sorts we considered so far can be encoded just as \mbox{@{text "Sort s []"}}.
|
|
1299 |
The point, however, is that we can now define the function @{text sort_ty} simply as
|
|
1300 |
|
|
1301 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
1302 |
\begin{tabular}{@ {}l}
|
|
1303 |
@{text "sort_ty (TVar s) = Sort ''TVar'' [Sort s []]"}\\
|
|
1304 |
@{text "sort_ty (\<tau>\<^isub>1 \<rightarrow> \<tau>\<^isub>2) = Sort ''Fun'' [sort_ty \<tau>\<^isub>1, sort_ty \<tau>\<^isub>2]"}
|
|
1305 |
\end{tabular}\hfill\numbered{sortty}
|
|
1306 |
\end{isabelle}
|
|
1307 |
|
|
1308 |
\noindent
|
|
1309 |
which can easily be shown to be injective.
|
|
1310 |
|
|
1311 |
Having settled on what the sorts should be for ``Church-like'' atoms, we have to
|
|
1312 |
give a subtype definition for concrete atoms. Previously we identified a subtype consisting
|
|
1313 |
of atoms of only one specified sort. This must be generalised to all sorts the
|
|
1314 |
function @{text "sort_ty"} might produce, i.e.~the
|
|
1315 |
range of @{text "sort_ty"}. Therefore we define
|
|
1316 |
|
|
1317 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
|
|
1318 |
\isacommand{typedef}\ \ @{text var} = @{term "{a. sort a : range sort_ty}"}
|
|
1319 |
\end{isabelle}
|
|
1320 |
|
|
1321 |
\noindent
|
|
1322 |
This command gives us again injective representation and abstraction
|
|
1323 |
functions. We will write them also as \mbox{@{text "\<lfloor>_\<rfloor> :: var \<Rightarrow> atom"}} and
|
|
1324 |
@{text "\<lceil>_\<rceil> :: atom \<Rightarrow> var"}, respectively.
|
|
1325 |
|
|
1326 |
We can define the permutation operation for @{text var} as @{thm
|
|
1327 |
permute_var_def[where p="\<pi>", THEN eq_reflection, no_vars]} and the
|
|
1328 |
injective function to type @{typ atom} as @{thm atom_var_def[THEN
|
|
1329 |
eq_reflection, no_vars]}. Finally, we can define a constructor function that
|
|
1330 |
makes a @{text var} from a variable name and an object type:
|
|
1331 |
|
|
1332 |
@{thm [display,indent=10] Var_def[where t="\<alpha>", THEN eq_reflection, no_vars]}
|
|
1333 |
|
|
1334 |
\noindent
|
|
1335 |
With these definitions we can verify all the properties for concrete atom
|
|
1336 |
types except Property \ref{atomprops}@{text ".iii)"}, which requires every
|
|
1337 |
atom to have the same sort. This last property is clearly not true for type
|
|
1338 |
@{text "var"}.
|
|
1339 |
This fact is slightly unfortunate since this
|
|
1340 |
property allowed us to use the type-checker in order to shield the user from
|
|
1341 |
all sort-constraints. But this failure is expected here, because we cannot
|
|
1342 |
burden the type-system of Isabelle/HOL with the task of deciding when two
|
|
1343 |
object types are equal. This means we sometimes need to explicitly state sort
|
|
1344 |
constraints or explicitly discharge them, but as we will see in the lemma
|
|
1345 |
below this seems a natural price to pay in these circumstances.
|
|
1346 |
|
|
1347 |
To sum up this section, the encoding of type-information into atoms allows us
|
|
1348 |
to form the swapping @{term "(Var x \<alpha> \<leftrightarrow> Var y \<alpha>)"} and to prove the following
|
|
1349 |
lemma
|
|
1350 |
*}
|
|
1351 |
|
|
1352 |
lemma
|
|
1353 |
assumes asm: "\<alpha> \<noteq> \<beta>"
|
|
1354 |
shows "(Var x \<alpha> \<leftrightarrow> Var y \<alpha>) \<bullet> (Var x \<alpha>, Var x \<beta>) = (Var y \<alpha>, Var x \<beta>)"
|
|
1355 |
using asm by simp
|
|
1356 |
|
|
1357 |
text {*
|
|
1358 |
\noindent
|
|
1359 |
As we expect, the atom @{term "Var x \<beta>"} is left unchanged by the
|
|
1360 |
swapping. With this we can faithfully represent bindings in languages
|
|
1361 |
involving ``Church-style'' terms and bindings as shown in \eqref{church}. We
|
|
1362 |
expect that the creation of such atoms can be easily automated so that the
|
|
1363 |
user just needs to specify \isacommand{atom\_decl}~~@{text "var (ty)"}
|
|
1364 |
where the argument, or arguments, are datatypes for which we can automatically
|
|
1365 |
define an injective function like @{text "sort_ty"} (see \eqref{sortty}).
|
1809
|
1366 |
Our hope is that with this approach Benzmueller and Paulson can make
|
|
1367 |
headway with formalising their results
|
|
1368 |
about simple type theory \cite{PaulsonBenzmueller}.
|
1785
|
1369 |
Because of its limitations, they did not attempt this with the old version
|
|
1370 |
of Nominal Isabelle. We also hope we can make progress with formalisations of
|
|
1371 |
HOL-based languages.
|
|
1372 |
*}
|
|
1373 |
|
2033
|
1374 |
section {* Related Work *}
|
|
1375 |
|
|
1376 |
text {*
|
|
1377 |
Add here comparison with old work.
|
2523
|
1378 |
|
|
1379 |
|
|
1380 |
The main point is that the above reasoning blends smoothly with the reasoning
|
|
1381 |
infrastructure of Isabelle/HOL; no custom ML-code is necessary and a single
|
|
1382 |
type class suffices.
|
2033
|
1383 |
*}
|
|
1384 |
|
1785
|
1385 |
|
|
1386 |
section {* Conclusion *}
|
|
1387 |
|
|
1388 |
text {*
|
|
1389 |
This proof pearl describes a new formalisation of the nominal logic work by
|
|
1390 |
Pitts et al. With the definitions we presented here, the formal reasoning blends
|
|
1391 |
smoothly with the infrastructure of the Isabelle/HOL theorem prover.
|
|
1392 |
Therefore the formalisation will be the underlying theory for a
|
|
1393 |
new version of Nominal Isabelle.
|
|
1394 |
|
|
1395 |
The main difference of this paper with respect to existing work on Nominal
|
|
1396 |
Isabelle is the representation of atoms and permutations. First, we used a
|
|
1397 |
single type for sorted atoms. This design choice means for a term @{term t},
|
|
1398 |
say, that its support is completely characterised by @{term "supp t"}, even
|
|
1399 |
if the term contains different kinds of atoms. Also, whenever we have to
|
|
1400 |
generalise an induction so that a property @{text P} is not just established
|
|
1401 |
for all @{text t}, but for all @{text t} \emph{and} under all permutations
|
|
1402 |
@{text \<pi>}, then we only have to state @{term "\<forall>\<pi>. P (\<pi> \<bullet> t)"}. The reason is
|
|
1403 |
that permutations can now consist of multiple swapping each of which can
|
|
1404 |
swap different kinds of atoms. This simplifies considerably the reasoning
|
|
1405 |
involved in building Nominal Isabelle.
|
|
1406 |
|
|
1407 |
Second, we represented permutations as functions so that the associated
|
|
1408 |
permutation operation has only a single type parameter. This is very convenient
|
|
1409 |
because the abstract reasoning about permutations fits cleanly
|
|
1410 |
with Isabelle/HOL's type classes. No custom ML-code is required to work
|
|
1411 |
around rough edges. Moreover, by establishing that our permutations-as-functions
|
|
1412 |
representation satisfy the group properties, we were able to use extensively
|
|
1413 |
Isabelle/HOL's reasoning infrastructure for groups. This often reduced proofs
|
|
1414 |
to simple calculations over @{text "+"}, @{text "-"} and @{text "0"}.
|
|
1415 |
An interesting point is that we defined the swapping operation so that a
|
|
1416 |
swapping of two atoms with different sorts is \emph{not} excluded, like
|
|
1417 |
in our older work on Nominal Isabelle, but there is no ``effect'' of such
|
|
1418 |
a swapping (it is defined as the identity). This is a crucial insight
|
|
1419 |
in order to make the approach based on a single type of sorted atoms to work.
|
|
1420 |
But of course it is analogous to the well-known trick of defining division by
|
|
1421 |
zero to return zero.
|
|
1422 |
|
|
1423 |
We noticed only one disadvantage of the permutations-as-functions: Over
|
1809
|
1424 |
lists we can easily perform inductions. For permutations made up from
|
1785
|
1425 |
functions, we have to manually derive an appropriate induction principle. We
|
|
1426 |
can establish such a principle, but we have no real experience yet whether ours
|
|
1427 |
is the most useful principle: such an induction principle was not needed in
|
|
1428 |
any of the reasoning we ported from the old Nominal Isabelle, except
|
|
1429 |
when showing that if @{term "\<forall>a \<in> supp x. a \<sharp> p"} implies @{term "p \<bullet> x = x"}.
|
|
1430 |
|
|
1431 |
Finally, our implementation of sorted atoms turned out powerful enough to
|
|
1432 |
use it for representing variables that carry on additional information, for
|
|
1433 |
example typing annotations. This information is encoded into the sorts. With
|
|
1434 |
this we can represent conveniently binding in ``Church-style'' lambda-terms
|
|
1435 |
and HOL-based languages. While dealing with such additional information in
|
|
1436 |
dependent type-theories, such as LF or Coq, is straightforward, we are not
|
|
1437 |
aware of any other approach in a non-dependent HOL-setting that can deal
|
|
1438 |
conveniently with such binders.
|
|
1439 |
|
|
1440 |
The formalisation presented here will eventually become part of the Isabelle
|
|
1441 |
distribution, but for the moment it can be downloaded from the
|
|
1442 |
Mercurial repository linked at
|
|
1443 |
\href{http://isabelle.in.tum.de/nominal/download}
|
|
1444 |
{http://isabelle.in.tum.de/nominal/download}.\smallskip
|
|
1445 |
|
|
1446 |
\noindent
|
|
1447 |
{\bf Acknowledgements:} We are very grateful to Jesper Bengtson, Stefan
|
|
1448 |
Berghofer and Cezary Kaliszyk for their comments on earlier versions
|
|
1449 |
of this paper. We are also grateful to the anonymous referee who helped us to
|
|
1450 |
put the work into the right context.
|
|
1451 |
*}
|
|
1452 |
|
|
1453 |
|
|
1454 |
(*<*)
|
|
1455 |
end
|
|
1456 |
(*>*) |