62 type schemes. In order to be able to separate them, each kind of variables needs to be |
74 type schemes. In order to be able to separate them, each kind of variables needs to be |
63 represented by a different sort of atoms. |
75 represented by a different sort of atoms. |
64 |
76 |
65 The nominal logic work has been the starting point for a number of proving |
77 The nominal logic work has been the starting point for a number of proving |
66 infrastructures, most notable by Norrish \cite{norrish04} in HOL4, by |
78 infrastructures, most notable by Norrish \cite{norrish04} in HOL4, by |
67 Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and teh work by Urban |
79 Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and the work by Urban |
68 and Berghofer in Isabelle/HOL \cite{Urban08}. Its key attraction is a very |
80 and Berghofer in Isabelle/HOL \cite{Urban08}. Its key attraction is a very |
69 general notion, called \emph{support}, for the `set of free variables, or |
81 general notion, called \emph{support}, for the `set of free variables, or |
70 atoms' of an object that applies not just to lambda terms and type schemes, |
82 atoms, of an object' that applies not just to lambda terms and type schemes, |
71 but also to sets, products, lists and even functions. The notion of support |
83 but also to sets, products, lists, booleans and even functions. The notion of support |
72 is derived from the permutation operation defined over atoms. This |
84 is derived from the permutation operation defined over the |
73 permutation operation, written @{text "_ \<bullet> _"}, has proved to be very |
85 hierarchy of types. This |
|
86 permutation operation, written @{text "_ \<bullet> _"}, has proved to be much more |
74 convenient for reasoning about syntax, in comparison to, say, arbitrary |
87 convenient for reasoning about syntax, in comparison to, say, arbitrary |
75 renaming substitutions of atoms. The reason is that permutations are |
88 renaming substitutions of atoms. One reason is that permutations are |
76 bijective renamings of atoms and thus they can be easily `undone'---namely |
89 bijective renamings of atoms and thus they can be easily `undone'---namely |
77 by applying the inverse permutation. A corresponding inverse substitution |
90 by applying the inverse permutation. A corresponding inverse substitution |
78 might not exist in general, since renaming substitutions are only injective. |
91 might not always exist, since renaming substitutions are in general only injective. |
79 Permutations also preserve many constructions when reasoning about syntax. |
92 Another reason is that permutations preserve many constructions when reasoning about syntax. |
80 For example validity of a typing context is preserved under permutations. |
93 For example the validity of a typing context is preserved under any permutation. |
81 Suppose a typing context @{text "\<Gamma>"} of the form |
94 Suppose a typing context @{text "\<Gamma>"} of the form |
82 |
95 |
83 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
96 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
84 @{text "x\<^isub>1:\<tau>\<^isub>1, \<dots>, x\<^isub>n:\<tau>\<^isub>n"} |
97 @{text "x\<^isub>1:\<tau>\<^isub>1, \<dots>, x\<^isub>n:\<tau>\<^isub>n"} |
85 \end{isabelle} |
98 \end{isabelle} |
86 |
99 |
87 \noindent |
100 \noindent |
88 is said to be \emph{valid} provided none of its variables, or atoms, @{text "x\<^isub>i"} |
101 is said to be \emph{valid} provided none of its variables, or atoms, @{text "x\<^isub>i"} |
89 occur twice. Then validity is preserved under |
102 occur twice. Then validity is preserved under |
90 permutations in the sense that if @{text \<Gamma>} is valid then so is @{text "\<pi> \<bullet> \<Gamma>"} for |
103 permutations in the sense that if @{text \<Gamma>} is valid then so is @{text "\<pi> \<bullet> \<Gamma>"} for |
91 all permutations @{text "\<pi>"}. This is \emph{not} the case for arbitrary |
104 all permutations @{text "\<pi>"}. This is again \emph{not} the case for arbitrary |
92 renaming substitutions, as they might identify some variables in @{text \<Gamma>}. |
105 renaming substitutions, as they might identify some of the @{text "x\<^isub>i"} in @{text \<Gamma>}. |
93 Permutations fit well with HOL's definitions. For example |
106 |
94 |
107 Permutations also behave uniformly with respect to HOL's logic connectives. |
95 |
108 Applying a permutation to a formula gives, for example |
96 Because |
109 |
97 of the good properties of permutations, we will be able to automate reasoning |
110 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
98 steps determining when a construction in HOL is |
111 \begin{tabular}{@ {}lcl} |
99 \emph{equivariant}. By equivariance we mean the property that every |
112 @{term "\<pi> \<bullet> (A \<and> B)"} & if and only if & @{text "(\<pi> \<bullet> A) \<and> (\<pi> \<bullet> B)"}\\ |
100 permutation leaves an object unchanged, that is @{term "\<forall>\<pi>. \<pi> \<bullet> x = x"}. |
113 @{term "\<pi> \<bullet> (A \<longrightarrow> B)"} & if and only if & @{text "(\<pi> \<bullet> A) \<longrightarrow> (\<pi> \<bullet> B)"}\\ |
101 This will often simplify arguments involving the notion of support. |
114 \end{tabular} |
102 |
115 \end{isabelle} |
103 |
116 |
104 There are a number of subtle differences between the nominal logic work by Pitts |
117 \noindent |
105 and the one we will present in this paper. Nominal |
118 This uniform behaviour can also be extended to quantifiers and functions. |
106 |
119 Because of these good properties of permutations, we are able to automate |
107 In the nominal logic work, the `new quantifier' plays a prominent role. |
120 reasoning to do with \emph{equivariance}. By equivariance we mean the property |
108 |
121 that every permutation leaves an object unchanged, that is @{term "\<pi> \<bullet> x = x"} |
109 |
122 for all @{text "\<pi>"}. This will often simplify arguments involving support |
110 |
123 and functions, since equivariant objects have empty support---or |
111 Using a single atom type to represent atoms of different sorts and |
124 `no free atoms'. |
112 representing permutations as functions are not new ideas; see |
125 |
113 \cite{GunterOsbornPopescu09} \footnote{function rep.} The main contribution |
126 There are a number of subtle differences between the nominal logic work by |
114 of this paper is to show an example of how to make better theorem proving |
127 Pitts and the formalisation we will present in this paper. One difference |
115 tools by choosing the right level of abstraction for the underlying |
128 is that our |
116 theory---our design choices take advantage of Isabelle's type system, type |
129 formalisation is compatible with HOL, in the sense that we only extend |
117 classes and reasoning infrastructure. The novel technical contribution is a |
130 HOL by some definitions, withouth the introduction of any new axioms. |
118 mechanism for dealing with ``Church-style'' lambda-terms \cite{Church40} and |
131 The reason why the original nominal logic work is |
119 HOL-based languages \cite{PittsHOL4} where variables and variable binding |
132 incompatible with HOL has to do with the way how the finite support property |
120 depend on type annotations. |
133 is enforced: FM-set theory is defined in \cite{Pitts01b} so that every set |
121 |
134 in the FM-set-universe has finite support. In nominal logic \cite{Pitts03}, |
122 The paper is organised as follows\ldots |
135 the axioms (E3) and (E4) imply that every function symbol and proposition |
|
136 has finite support. However, there are notions in HOL that do \emph{not} |
|
137 have finite support (we will give some examples). In our formalisation, we |
|
138 will avoid the incompatibility of the original nominal logic work by not a |
|
139 priory restricting our discourse to only finitely supported entities, rather |
|
140 we will explicitly assume this property whenever it is needed in proofs. One |
|
141 consequence is that we state our basic definitions not in terms of nominal |
|
142 sets (as done for example in \cite{Pitts06}), but in terms of the weaker |
|
143 notion of permutation types---essentially sets equipped with a ``sensible'' |
|
144 notion of permutation operation. |
|
145 |
|
146 |
|
147 |
|
148 In the nominal logic woworkrk, the `new quantifier' plays a prominent role. |
|
149 $\new$ |
|
150 |
|
151 |
123 |
152 |
124 |
153 |
125 Two binders |
154 Two binders |
126 *} |
155 *} |
127 |
156 |
128 section {* Sorted Atoms and Sort-Respecting Permutations *} |
157 section {* Sorted Atoms and Sort-Respecting Permutations *} |
129 |
158 |
130 text {* |
159 text {* |
131 The two most basic notions in the nominal logic work are |
160 The two most basic notions in the nominal logic work are a countably |
132 sort-respecting permutation operation defined over a countably infinite |
161 infinite collection of sorted atoms and sort-respecting permutations. |
133 collection of sorted atoms. |
162 The existing nominal logic work usually leaves implicit |
134 The existing nominal logic work usually leaves implicit the sorting |
163 the sorting information for atoms and as far as we know leaves out a |
135 information for atoms and as far as we know leaves out a description of how |
164 description of how sorts are represented. In our formalisation, we |
136 sorts are represented. In our formalisation, we therefore have to make a |
165 therefore have to make a design decision about how to implement sorted atoms |
137 design decision about how to implement sorted atoms and sort-respecting |
166 and sort-respecting permutations. One possibility, which we described in |
138 permutations. One possibility, which we described in \cite{Urban08}, is to |
167 \cite{Urban08}, is to have separate types for the different sorts of |
139 have separate types for the different kinds of atoms, say types @{text |
168 atoms. However, we found that this does not blend well with type-classes in |
140 "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}. However, this does not blend well with the |
169 Isabelle/HOL (see Section~\ref{related} about related work). Therefore we use here a |
141 resoning infrastructure of type-classes in Isabelle/HOL (see Section ??? |
170 single unified atom type to represent atoms of different sorts. A basic |
142 about related work). Therefore we use here a single unified atom type to |
171 requirement is that there must be a countably infinite number of atoms of |
143 represent atoms of different sorts. A basic requirement is that there must |
172 each sort. This can be implemented as the datatype |
144 be a countably infinite number of atoms of each sort. This can be |
|
145 implemented as the datatype |
|
146 |
173 |
147 *} |
174 *} |
148 |
175 |
149 datatype atom\<iota> = Atom\<iota> string nat |
176 datatype atom\<iota> = Atom\<iota> string nat |
150 |
177 |
151 text {* |
178 text {* |
152 \noindent |
179 \noindent |
153 whereby the string argument specifies the sort of the atom.\footnote{A |
180 whereby the string argument specifies the sort of the atom.\footnote{A |
154 similar design choice was made by Gunter et al \cite{GunterOsbornPopescu09} |
181 similar design choice was made by Gunter et al \cite{GunterOsbornPopescu09} |
155 for their variables.} The use of type \emph{string} for sorts is merely for |
182 for their variables.} The use of type \emph{string} for sorts is merely for |
156 convenience; any countably infinite type would work as well. We have an |
183 convenience; any countably infinite type would work as well. |
157 auxiliary function @{text sort} that is defined as |
184 The set of all atoms we shall write as @{term "UNIV::atom set"}. |
158 |
185 We have two |
159 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
186 auxiliary functions @{text sort} and @{const nat_of} that are defined as |
160 @{thm sort_of.simps[no_vars, THEN eq_reflection]} |
187 |
161 \end{isabelle} |
188 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
162 |
189 \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} |
163 \noindent |
190 @{thm (lhs) sort_of.simps[no_vars]} & @{text "\<equiv>"} & @{thm (rhs) sort_of.simps[no_vars]}\\ |
164 and we clearly have for every finite set @{text S} |
191 @{thm (lhs) nat_of.simps[no_vars]} & @{text "\<equiv>"} & @{thm (rhs) nat_of.simps[no_vars]} |
|
192 \end{tabular}\hfill\numbered{sortnatof} |
|
193 \end{isabelle} |
|
194 |
|
195 \noindent |
|
196 We clearly have for every finite set @{text S} |
165 of atoms and every sort @{text s} the property: |
197 of atoms and every sort @{text s} the property: |
166 |
198 |
167 \begin{proposition}\label{choosefresh}\mbox{}\\ |
199 \begin{proposition}\label{choosefresh}\mbox{}\\ |
168 @{text "For a finite set of atoms S, there exists an atom a such that |
200 @{text "For a finite set of atoms S, there exists an atom a such that |
169 sort a = s and a \<notin> S"}. |
201 sort a = s and a \<notin> S"}. |
200 @{text [display,indent=10] "(_ _) :: atom \<Rightarrow> atom \<Rightarrow> perm"} |
232 @{text [display,indent=10] "(_ _) :: atom \<Rightarrow> atom \<Rightarrow> perm"} |
201 |
233 |
202 \noindent |
234 \noindent |
203 but since permutations are required to respect sorts, we must carefully |
235 but since permutations are required to respect sorts, we must carefully |
204 consider what happens if a user states a swapping of atoms with different |
236 consider what happens if a user states a swapping of atoms with different |
205 sorts. In early versions of Nominal Isabelle, we avoided this problem by |
237 sorts. The following definition\footnote{To increase legibility, we omit |
206 using different types for different sorts; the type system prevented users |
238 here and in what follows the @{term Rep_perm} and @{term "Abs_perm"} |
207 from stating ill-sorted swappings. Here, however, definitions such |
239 wrappers that are needed in our implementation since we defined permutation |
208 as\footnote{To increase legibility, we omit here and in what follows the |
240 not to be the full function space, but only those functions of type @{typ |
209 @{term Rep_perm} and @{term "Abs_perm"} wrappers that are needed in our |
241 perm} satisfying properties @{text i}-@{text "iii"} in \eqref{permtype}.} |
210 implementation since we defined permutation not to be the full function space, |
242 |
211 but only those functions of type @{typ perm} satisfying properties @{text |
|
212 i}-@{text "iii"}.} |
|
213 |
243 |
214 @{text [display,indent=10] "(a b) \<equiv> \<lambda>c. if a = c then b else (if b = c then a else c)"} |
244 @{text [display,indent=10] "(a b) \<equiv> \<lambda>c. if a = c then b else (if b = c then a else c)"} |
215 |
245 |
216 \noindent |
246 \noindent |
217 do not work in general, because the type system does not prevent @{text a} |
247 does not work in general, because @{text a} and @{text b} may have different |
218 and @{text b} from having different sorts---in which case the function would |
248 sorts---in which case the function would violate property @{text iii} in \eqref{permtype}. We |
219 violate property @{text iii}. We could make the definition of swappings |
249 could make the definition of swappings partial by adding the precondition |
220 partial by adding the precondition @{term "sort a = sort b"}, |
250 @{term "sort a = sort b"}, which would mean that in case @{text a} and |
221 which would mean that in case @{text a} and @{text b} have different sorts, |
251 @{text b} have different sorts, the value of @{text "(a b)"} is unspecified. |
222 the value of @{text "(a b)"} is unspecified. However, this looked like a |
252 However, this looked like a cumbersome solution, since sort-related side |
223 cumbersome solution, since sort-related side conditions would be required |
253 conditions would be required everywhere, even to unfold the definition. It |
224 everywhere, even to unfold the definition. It turned out to be more |
254 turned out to be more convenient to actually allow the user to state |
225 convenient to actually allow the user to state `ill-sorted' swappings but |
255 `ill-sorted' swappings but limit their `damage' by defaulting to the |
226 limit their `damage' by defaulting to the identity permutation in the |
256 identity permutation in the ill-sorted case: |
227 ill-sorted case: |
257 |
228 |
258 |
229 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
259 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
230 \begin{tabular}{@ {}rl} |
260 \begin{tabular}{@ {}rl} |
231 @{text "(a b) \<equiv>"} & @{text "if (sort a = sort b)"}\\ |
261 @{text "(a b) \<equiv>"} & @{text "if (sort a = sort b)"}\\ |
232 & \hspace{3mm}@{text "then \<lambda>c. if a = c then b else (if b = c then a else c)"}\\ |
262 & \hspace{3mm}@{text "then \<lambda>c. if a = c then b else (if b = c then a else c)"}\\ |
238 This function is bijective, the identity on all atoms except |
268 This function is bijective, the identity on all atoms except |
239 @{text a} and @{text b}, and sort respecting. Therefore it is |
269 @{text a} and @{text b}, and sort respecting. Therefore it is |
240 a function in @{typ perm}. |
270 a function in @{typ perm}. |
241 |
271 |
242 One advantage of using functions as a representation for |
272 One advantage of using functions as a representation for |
243 permutations is that for example the swappings |
273 permutations is that it is unique. For example the swappings |
244 |
274 |
245 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
275 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
246 \begin{tabular}{@ {}l} |
276 \begin{tabular}{@ {}l} |
247 @{thm swap_commute[no_vars]}\hspace{10mm} |
277 @{thm swap_commute[no_vars]}\hspace{10mm} |
248 @{text "(a a) = id"} |
278 @{text "(a a) = id"} |
249 \end{tabular}\hfill\numbered{swapeqs} |
279 \end{tabular}\hfill\numbered{swapeqs} |
250 \end{isabelle} |
280 \end{isabelle} |
251 |
281 |
252 \noindent |
282 \noindent |
253 are \emph{equal}. Therfore we can use for permutations HOL's built-in |
283 are \emph{equal}. Another advantage of the function representation is that |
254 principle of `replacing equals by equals in any context'. Another advantage |
284 they form a (non-com\-mu\-ta\-tive) group provided we define |
255 of the function representation is that they form a (non-commutative) group |
285 |
256 provided we define |
286 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
257 |
287 \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{10mm}}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} |
|
288 @{thm (lhs) zero_perm_def[no_vars]} & @{text "\<equiv>"} & @{thm (rhs) zero_perm_def[no_vars]} & |
|
289 @{thm (lhs) plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2"]} & @{text "\<equiv>"} & |
|
290 @{thm (rhs) plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2"]}\\ |
|
291 @{thm (lhs) uminus_perm_def[where p="\<pi>"]} & @{text "\<equiv>"} & @{thm (rhs) uminus_perm_def[where p="\<pi>"]} & |
|
292 @{thm (lhs) minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]} & @{text "\<equiv>"} & |
|
293 @{thm (rhs) minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]} |
|
294 \end{tabular}\hfill\numbered{groupprops} |
|
295 \end{isabelle} |
|
296 |
|
297 \noindent |
|
298 and verify the four simple properties |
258 |
299 |
259 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
300 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
260 \begin{tabular}{@ {}l} |
301 \begin{tabular}{@ {}l} |
261 @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{5mm} |
302 @{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]}\\ |
262 @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{5mm} |
303 @{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{9mm} |
263 @{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{5mm} |
304 @{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{9mm} |
264 @{thm minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]} |
|
265 \end{tabular} |
|
266 \end{isabelle} |
|
267 |
|
268 \noindent |
|
269 and verify the simple properties |
|
270 |
|
271 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
|
272 \begin{tabular}{@ {}l} |
|
273 @{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]} \hspace{5mm} |
|
274 @{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{5mm} |
|
275 @{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{5mm} |
|
276 @{thm group_add_class.left_minus[where a="\<pi>::perm"]} |
305 @{thm group_add_class.left_minus[where a="\<pi>::perm"]} |
277 \end{tabular} |
306 \end{tabular} |
278 \end{isabelle} |
307 \end{isabelle} |
279 |
308 |
280 \noindent |
309 \noindent |
286 composition of permutations is not commutative in general, because @{text |
315 composition of permutations is not commutative in general, because @{text |
287 "\<pi>\<^sub>1 + \<pi>\<^sub>2 \<noteq> \<pi>\<^sub>2 + \<pi>\<^sub>1"}. But since the point of this paper is to implement the |
316 "\<pi>\<^sub>1 + \<pi>\<^sub>2 \<noteq> \<pi>\<^sub>2 + \<pi>\<^sub>1"}. But since the point of this paper is to implement the |
288 nominal theory as smoothly as possible in Isabelle/HOL, we tolerate |
317 nominal theory as smoothly as possible in Isabelle/HOL, we tolerate |
289 the non-standard notation in order to reuse the existing libraries. |
318 the non-standard notation in order to reuse the existing libraries. |
290 |
319 |
291 In order to reason abstractly about permutations, we state the following two |
320 In order to reason abstractly about permutations, we use Isabelle/HOL's |
292 \emph{permutation properties} |
321 type classes~\cite{Wenzel04} and state the following two |
|
322 \emph{permutation properties}: |
293 |
323 |
294 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
324 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
295 \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}} |
325 \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}} |
296 i) & @{thm permute_zero[no_vars]}\\ |
326 i) & @{thm permute_zero[no_vars]}\\ |
297 ii) & @{thm permute_plus[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2",no_vars]} |
327 ii) & @{thm permute_plus[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2",no_vars]} |
298 \end{tabular}\hfill\numbered{newpermprops} |
328 \end{tabular}\hfill\numbered{newpermprops} |
299 \end{isabelle} |
329 \end{isabelle} |
300 |
330 |
301 \noindent |
331 \noindent |
302 We state these properties in terms of Isabelle/HOL's type class |
332 The use of type classes allows us to delegate much of the routine resoning involved in |
303 mechanism \cite{}. |
333 determining whether these properties are satisfied to Isabelle/HOL's type system: |
304 This allows us to delegate much of the resoning involved in |
334 we only have to establish that `base' types, such as @{text booleans} and |
305 determining whether these properties are satisfied to the type system. |
335 @{text atoms}, satisfy them and that type-constructors, such as products and lists, |
306 For this we define |
336 preserve them. For this we define |
307 |
337 |
308 \begin{definition} |
338 \begin{definition}[Permutation type] |
309 A type @{text "\<beta>"} is a \emph{permutation type} if the permutation |
339 A type @{text "\<beta>"} is a \emph{permutation type} if the permutation |
310 properties in \eqref{newpermprops} are satisfied for every @{text "x"} of type |
340 properties in \eqref{newpermprops} are satisfied for every @{text "x"} of type |
311 @{text "\<beta>"}. |
341 @{text "\<beta>"}. |
312 \end{definition} |
342 \end{definition} |
313 |
343 |
314 \noindent |
344 \noindent |
315 The type class also allows us to establish generic lemmas involving the |
345 The type classes also allows us to establish generic lemmas involving the |
316 permutation operation. First, it follows from the laws governing |
346 permutation operation. First, it follows from the laws governing |
317 groups that a permutation and its inverse cancel each other. That is, for any |
347 groups that a permutation and its inverse cancel each other. That is, for any |
318 @{text "x"} of a permutation type: |
348 @{text "x"} of a permutation type: |
319 |
349 |
320 |
350 |
324 @{thm permute_minus_cancel(2)[where p="\<pi>", no_vars]} |
354 @{thm permute_minus_cancel(2)[where p="\<pi>", no_vars]} |
325 \end{tabular}\hfill\numbered{cancel} |
355 \end{tabular}\hfill\numbered{cancel} |
326 \end{isabelle} |
356 \end{isabelle} |
327 |
357 |
328 \noindent |
358 \noindent |
329 ??? Proof |
|
330 Consequently, in a permutation type the permutation operation @{text "\<pi> \<bullet> _"}~~is bijective, |
359 Consequently, in a permutation type the permutation operation @{text "\<pi> \<bullet> _"}~~is bijective, |
331 which in turn implies the property |
360 which in turn implies the property |
332 |
361 |
333 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
362 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
334 \begin{tabular}{@ {}l} |
363 \begin{tabular}{@ {}l} |
335 @{thm (lhs) permute_eq_iff[where p="\<pi>", no_vars]} |
364 @{thm (lhs) permute_eq_iff[where p="\<pi>", no_vars]} |
336 $\;$if and only if$\;$ |
365 $\;$if and only if$\;$ |
337 @{thm (rhs) permute_eq_iff[where p="\<pi>", no_vars]}. |
366 @{thm (rhs) permute_eq_iff[where p="\<pi>", no_vars]}. |
338 \end{tabular}\hfill\numbered{permuteequ} |
367 \end{tabular}\hfill\numbered{permuteequ} |
339 \end{isabelle} |
368 \end{isabelle} |
340 |
|
341 \noindent |
|
342 We can also show that the following property holds for any permutation type. |
|
343 |
|
344 \begin{lemma}\label{permutecompose} |
|
345 Given @{term x} is of permutation type, then |
|
346 @{text "\<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x) = (\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}. |
|
347 \end{lemma} |
|
348 |
|
349 \begin{proof} The proof is as follows: |
|
350 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
|
351 \begin{tabular}[b]{@ {}rcl@ {\hspace{8mm}}l} |
|
352 @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> x"} |
|
353 & @{text "="} & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> (-\<pi>\<^isub>1) \<bullet> \<pi>\<^isub>1 \<bullet> x"} & by \eqref{cancel}\\ |
|
354 & @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2 - \<pi>\<^isub>1) \<bullet> \<pi>\<^isub>1 \<bullet> x"} & by {\rm(\ref{newpermprops}.@{text "ii"})}\\ |
|
355 & @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}\\ |
|
356 \end{tabular}\hfill\qed |
|
357 \end{isabelle} |
|
358 \end{proof} |
|
359 |
369 |
360 \noindent |
370 \noindent |
361 In order to lift the permutation operation to other types, we can define for: |
371 In order to lift the permutation operation to other types, we can define for: |
362 |
372 |
363 \begin{equation}\label{permdefs} |
373 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
364 \mbox{ |
374 \begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}} |
365 \begin{tabular}{@ {}ll@ {\hspace{4mm}}l@ {}} |
375 atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\ |
366 a) & atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\ |
376 functions: & @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\ |
367 b) & functions: & @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\ |
377 permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\ |
368 c) & permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\ |
378 sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
369 d) & sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
379 booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
370 e) & booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
380 lists: & @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
371 f) & lists: & @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
381 & @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
372 & & @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
382 products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
373 g) & products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
383 nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
374 h) & nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
384 \end{tabular}\hfill\numbered{permdefs} |
375 \end{tabular}} |
385 \end{isabelle} |
376 \end{equation} |
|
377 |
386 |
378 \noindent |
387 \noindent |
379 and then establish: |
388 and then establish: |
380 |
389 |
381 \begin{theorem} |
390 \begin{theorem} |
397 & @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) + \<pi>' - \<pi>\<^isub>2 - \<pi>\<^isub>1"}\\ |
406 & @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) + \<pi>' - \<pi>\<^isub>2 - \<pi>\<^isub>1"}\\ |
398 & @{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>'"} |
407 & @{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>'"} |
399 \end{tabular}\hfill\qed |
408 \end{tabular}\hfill\qed |
400 \end{isabelle} |
409 \end{isabelle} |
401 \end{proof} |
410 \end{proof} |
|
411 |
|
412 \noindent |
|
413 Note that the permutation operation for functions is defined so that we have the property |
|
414 |
|
415 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
|
416 @{text "\<pi> \<bullet> (f x) ="} |
|
417 @{thm (rhs) permute_fun_app_eq[where p="\<pi>", no_vars]} |
|
418 \hfill\numbered{permutefunapp} |
|
419 \end{isabelle} |
|
420 |
|
421 \noindent |
|
422 which is a simple consequence of the definition and the cancellation property in \eqref{cancel}. |
|
423 We can also show that the following property holds for any permutation type. |
|
424 |
|
425 \begin{lemma}\label{permutecompose} |
|
426 Given @{term x} is of permutation type, then |
|
427 @{text "\<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x) = (\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}. |
|
428 \end{lemma} |
|
429 |
|
430 \begin{proof} The proof is as follows: |
|
431 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
|
432 \begin{tabular}[b]{@ {}c@ {\hspace{2mm}}l@ {\hspace{8mm}}l} |
|
433 & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> x"}\\ |
|
434 @{text "="} & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> (-\<pi>\<^isub>1) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"} & by \eqref{cancel}\\ |
|
435 @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2 - \<pi>\<^isub>1) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"} & by {\rm(\ref{newpermprops}.@{text "ii"})}\\ |
|
436 @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}\\ |
|
437 \end{tabular}\hfill\qed |
|
438 \end{isabelle} |
|
439 \end{proof} |
|
440 |
402 *} |
441 *} |
403 |
442 |
404 section {* Equivariance *} |
443 section {* Equivariance *} |
405 |
444 |
406 text {* |
445 text {* |
407 An important notion in the nominal logic work is \emph{equivariance}. |
446 An important notion in the nominal logic work is \emph{equivariance}. |
408 An equivariant function or predicate is one that is invariant under |
447 An equivariant function is one that is invariant under |
409 the swapping of atoms. This notion can be defined |
448 permutations of atoms. This notion can be defined |
410 uniformly as follows: |
449 uniformly as follows: |
411 |
450 |
412 |
451 |
413 \begin{definition}\label{equivariance} |
452 \begin{definition}[Equivariance]\label{equivariance} |
414 A function @{text f} is \emph{equivariant} if @{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}. |
453 A function @{text f} is \emph{equivariant} if @{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}. |
415 \end{definition} |
454 \end{definition} |
416 |
455 |
417 \noindent |
456 \noindent |
418 There are a number of equivalent formulations for the equivariance property. |
457 There are a number of equivalent formulations for the equivariance property. |
460 |
483 |
461 \noindent |
484 \noindent |
462 using the permutation operation on booleans and property \eqref{permuteequ}. |
485 using the permutation operation on booleans and property \eqref{permuteequ}. |
463 Lemma~\ref{permutecompose} establishes that the permutation operation is |
486 Lemma~\ref{permutecompose} establishes that the permutation operation is |
464 equivariant. It is also easy to see that the boolean operators, like |
487 equivariant. It is also easy to see that the boolean operators, like |
465 @{text "\<and>"}, @{text "\<or>"} and @{text "\<longrightarrow>"} are all equivariant. Furthermore |
488 @{text "\<and>"}, @{text "\<or>"}, @{text "\<not>"} and @{text "\<longrightarrow>"} are all equivariant. Furthermore |
466 a simple calculation will show that our swapping functions are equivariant, that is |
489 a simple calculation will show that our swapping functions are equivariant, that is |
467 |
490 |
468 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
491 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
469 \begin{tabular}{@ {}l} |
492 \begin{tabular}{@ {}l} |
470 @{thm swap_eqvt[where p="\<pi>", no_vars]} |
493 @{thm swap_eqvt[where p="\<pi>", no_vars]} |
471 \end{tabular}\hfill\numbered{swapeqvt} |
494 \end{tabular}\hfill\numbered{swapeqvt} |
472 \end{isabelle} |
495 \end{isabelle} |
473 |
496 |
474 \noindent |
497 \noindent |
475 for all @{text a}, @{text b} and @{text \<pi>}. |
498 for all @{text a}, @{text b} and @{text \<pi>}. |
|
499 |
|
500 In contrast, Definition~\ref{equivariance} together with the permutation |
|
501 operation for functions and \eqref{permutefunapp} lead to a simple |
|
502 rewrite system that pushes permutations inside a term until they reach |
|
503 either function constants or variables. The permutations in front of |
|
504 equivariant functions disappear. Such a rewrite system is often very helpful |
|
505 in determining whether @{text "\<pi> \<bullet> t = t"} holds for a compound term @{text t}. ??? |
|
506 |
476 *} |
507 *} |
477 |
508 |
478 |
509 |
479 section {* Support and Freshness *} |
510 section {* Support and Freshness *} |
480 |
511 |
481 text {* |
512 text {* |
482 The most original aspect of the nominal logic work of Pitts et al is a general |
513 The most original aspect of the nominal logic work of Pitts is a general |
483 definition for ``the set of free variables of an object @{text "x"}''. This |
514 definition for `the set of free variables, or free atoms, of an object @{text "x"}'. This |
484 definition is general in the sense that it applies not only to lambda-terms, |
515 definition is general in the sense that it applies not only to lambda terms, |
485 but also to lists, products, sets and even functions. The definition depends |
516 but to any type for which a permutation operation is defined |
486 only on the permutation operation and on the notion of equality defined for |
517 (like lists, sets, functions and so on). |
487 the type of @{text x}, namely: |
518 |
488 |
519 \begin{definition}[Support] Given @{text x} is of permutation type, then |
|
520 |
489 @{thm [display,indent=10] supp_def[no_vars, THEN eq_reflection]} |
521 @{thm [display,indent=10] supp_def[no_vars, THEN eq_reflection]} |
|
522 \end{definition} |
490 |
523 |
491 \noindent |
524 \noindent |
492 (Note that due to the definition of swapping in \eqref{swapdef}, we do not |
525 (Note that due to the definition of swapping in \eqref{swapdef}, we do not |
493 need to explicitly restrict @{text a} and @{text b} to have the same sort.) |
526 need to explicitly restrict @{text a} and @{text b} to have the same sort.) |
494 There is also the derived notion for when an atom @{text a} is \emph{fresh} |
527 There is also the derived notion for when an atom @{text a} is \emph{fresh} |
495 for an @{text x}, defined as |
528 for an @{text x} of permutation type, defined as |
496 |
529 |
497 @{thm [display,indent=10] fresh_def[no_vars]} |
530 @{thm [display,indent=10] fresh_def[no_vars]} |
498 |
531 |
499 \noindent |
532 \noindent |
500 We also use the notation @{thm (lhs) fresh_star_def[no_vars]} for sets ot atoms |
533 We also use the notation @{thm (lhs) fresh_star_def[no_vars]} for sets ot atoms |
501 defined as follows |
534 defined as follows |
502 |
535 |
503 @{thm [display,indent=10] fresh_star_def[no_vars]} |
536 @{thm [display,indent=10] fresh_star_def[no_vars]} |
|
537 |
504 |
538 |
505 \noindent |
539 \noindent |
506 A striking consequence of these definitions is that we can prove |
540 A striking consequence of these definitions is that we can prove |
507 without knowing anything about the structure of @{term x} that |
541 without knowing anything about the structure of @{term x} that |
508 swapping two fresh atoms, say @{text a} and @{text b}, leave |
542 swapping two fresh atoms, say @{text a} and @{text b}, leave |
509 @{text x} unchanged. For the proof we use the following lemma |
543 @{text x} unchanged. For the proof we use the following lemma |
510 about swappings applied to an @{text x}: |
544 about swappings applied to an @{text x}: |
511 |
545 |
512 \begin{lemma}\label{swaptriple} |
546 \begin{lemma}\label{swaptriple} |
513 Assuming @{text x} is of permutation type, and @{text a}, @{text b} and @{text c} |
547 Assuming @{text x} is of permutation type, and @{text a}, @{text b} and @{text c} |
514 have the same sort, then @{thm (prem 3) swap_rel_trans[no_vars]} and |
548 have the same sort, then \mbox{@{thm (prem 3) swap_rel_trans[no_vars]}} and |
515 @{thm (prem 4) swap_rel_trans[no_vars]} imply @{thm (concl) swap_rel_trans[no_vars]}. |
549 @{thm (prem 4) swap_rel_trans[no_vars]} imply @{thm (concl) swap_rel_trans[no_vars]}. |
516 \end{lemma} |
550 \end{lemma} |
517 |
551 |
518 \begin{proof} |
552 \begin{proof} |
519 The cases where @{text "a = c"} and @{text "b = c"} are immediate. |
553 The cases where @{text "a = c"} and @{text "b = c"} are immediate. |
581 |
617 |
582 @{thm [display,indent=10] supp_eqvt[where p="\<pi>",no_vars]} |
618 @{thm [display,indent=10] supp_eqvt[where p="\<pi>",no_vars]} |
583 |
619 |
584 \noindent |
620 \noindent |
585 is by noting that @{thm supp_conv_fresh[no_vars]} and that freshness and |
621 is by noting that @{thm supp_conv_fresh[no_vars]} and that freshness and |
586 the logical connectives are equivariant. |
622 the logical connectives are equivariant. ??? Equivariance |
|
623 |
|
624 A simple consequence of the definition of support and equivariance is that |
|
625 if a function @{text f} is equivariant then we have |
|
626 |
|
627 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
|
628 \begin{tabular}{@ {}l} |
|
629 @{thm (concl) supp_fun_eqvt[no_vars]} |
|
630 \end{tabular}\hfill\numbered{suppeqvtfun} |
|
631 \end{isabelle} |
|
632 |
|
633 \noindent |
|
634 For function applications we can establish the two following properties. |
|
635 |
|
636 \begin{lemma} Let @{text f} and @{text x} be of permutation type, then |
|
637 \begin{isabelle} |
|
638 \begin{tabular}{r@ {\hspace{4mm}}p{10cm}} |
|
639 @{text "i)"} & @{thm[mode=IfThen] fresh_fun_app[no_vars]}\\ |
|
640 @{text "ii)"} & @{thm supp_fun_app[no_vars]}\\ |
|
641 \end{tabular} |
|
642 \end{isabelle} |
|
643 \end{lemma} |
|
644 |
|
645 \begin{proof} |
|
646 ??? |
|
647 \end{proof} |
|
648 |
587 |
649 |
588 While the abstract properties of support and freshness, particularly |
650 While the abstract properties of support and freshness, particularly |
589 Theorem~\ref{swapfreshfresh}, are useful for developing Nominal Isabelle, |
651 Theorem~\ref{swapfreshfresh}, are useful for developing Nominal Isabelle, |
590 one often has to calculate the support of some concrete object. This is |
652 one often has to calculate the support of some concrete object. This is |
591 straightforward for example for booleans, nats, products and lists: |
653 straightforward for example for booleans, nats, products and lists: |
592 |
654 |
593 \begin{equation} |
655 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
594 \mbox{ |
656 \begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}} |
595 \begin{tabular}{@ {}r@ {\hspace{2mm}}l} |
|
596 @{text "booleans"}: & @{term "supp b = {}"}\\ |
657 @{text "booleans"}: & @{term "supp b = {}"}\\ |
597 @{text "nats"}: & @{term "supp n = {}"}\\ |
658 @{text "nats"}: & @{term "supp n = {}"}\\ |
598 @{text "products"}: & @{thm supp_Pair[no_vars]}\\ |
659 @{text "products"}: & @{thm supp_Pair[no_vars]}\\ |
599 @{text "lists:"} & @{thm supp_Nil[no_vars]}\\ |
660 @{text "lists:"} & @{thm supp_Nil[no_vars]}\\ |
600 & @{thm supp_Cons[no_vars]}\\ |
661 & @{thm supp_Cons[no_vars]}\\ |
601 \end{tabular}} |
662 \end{tabular} |
602 \end{equation} |
663 \end{isabelle} |
603 |
664 |
604 \noindent |
665 \noindent |
605 But establishing the support of atoms and permutations is a bit |
666 But establishing the support of atoms and permutations is a bit |
606 trickier. To do so we will use the following notion about a \emph{supporting set}. |
667 trickier. To do so we will use the following notion about a \emph{supporting set}. |
607 |
668 |
608 \begin{definition} |
669 \begin{definition}[Supporting Set] |
609 A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b} |
670 A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b} |
610 not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}. |
671 not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}. |
611 \end{definition} |
672 \end{definition} |
612 |
673 |
613 \noindent |
674 \noindent |
727 can define a type class for types where every element has finite support, and |
788 can define a type class for types where every element has finite support, and |
728 prove that the types @{term "atom"}, @{term "perm"}, lists, products and |
789 prove that the types @{term "atom"}, @{term "perm"}, lists, products and |
729 booleans are instances of this type class. |
790 booleans are instances of this type class. |
730 |
791 |
731 Unfortunately, this does not work for sets or Isabelle/HOL's function |
792 Unfortunately, this does not work for sets or Isabelle/HOL's function |
732 type.\footnote{Isabelle/HOL takes the type @{text "\<alpha> set"} as an abbreviation |
793 type. There are functions and sets definable in Isabelle/HOL for which the |
733 of @{text "\<alpha> \<Rightarrow> bool"}.} There are functions and sets definable in |
794 finite support property does not hold. A simple example of a function with |
734 Isabelle/HOL for which the finite support property does not hold. A simple |
795 infinite support is @{const nat_of} shown in \eqref{sortnatof}. This |
735 example of a function with infinite support is the function that returns the |
796 function's support is the set of \emph{all} atoms @{term "UNIV::atom set"}. |
736 natural number of an atom |
797 To establish this we show |
737 |
798 @{term "\<not> a \<sharp> nat_of"}. This is equivalent to assuming the set @{term |
738 @{text [display, indent=10] "nat_of (Atom s i) \<equiv> i"} |
799 "{b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"} is finite and deriving a |
739 |
800 contradiction. From the assumption we also know that @{term "{a} \<union> {b. (a \<rightleftharpoons> |
740 \noindent |
801 b) \<bullet> nat_of \<noteq> nat_of}"} is finite. Then we can use |
741 This function's support is the set of \emph{all} atoms. To establish this we show @{term "\<not> a \<sharp> nat_of"}. |
802 Proposition~\ref{choosefresh} to choose an atom @{text c} such that @{term |
742 This is equivalent to assuming the set @{term "{b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"} is finite |
803 "c \<noteq> a"}, @{term "sort_of c = sort_of a"} and @{term "(a \<rightleftharpoons> c) \<bullet> nat_of = |
743 and deriving a contradiction. From the assumption we also know that |
804 nat_of"}. Now we can reason as follows: |
744 @{term "{a} \<union> {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"} is finite. Then we can use |
|
745 Proposition~\ref{choosefresh} to choose an atom @{text c} such that |
|
746 @{term "c \<noteq> a"}, @{term "sort_of c = sort_of a"} and @{term "(a \<rightleftharpoons> c) \<bullet> nat_of = nat_of"}. |
|
747 Now we can reason as follows: |
|
748 |
805 |
749 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
806 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
750 \begin{tabular}[b]{@ {}rcl@ {\hspace{5mm}}l} |
807 \begin{tabular}[b]{@ {}rcl@ {\hspace{5mm}}l} |
751 @{text "nat_of a"} & @{text "="} & @{text "(a \<rightleftharpoons> c) \<bullet> (nat_of a)"} & by def.~of permutations on nats\\ |
808 @{text "nat_of a"} & @{text "="} & @{text "(a \<rightleftharpoons> c) \<bullet> (nat_of a)"} & by def.~of permutations on nats\\ |
752 & @{text "="} & @{term "((a \<rightleftharpoons> c) \<bullet> nat_of) ((a \<rightleftharpoons> c) \<bullet> a)"} & by \eqref{permutefunapp}\\ |
809 & @{text "="} & @{term "((a \<rightleftharpoons> c) \<bullet> nat_of) ((a \<rightleftharpoons> c) \<bullet> a)"} & by \eqref{permutefunapp}\\ |
755 \end{isabelle} |
812 \end{isabelle} |
756 |
813 |
757 \noindent |
814 \noindent |
758 But this means we have that @{term "nat_of a = nat_of c"} and @{term "sort_of a = sort_of c"}. |
815 But this means we have that @{term "nat_of a = nat_of c"} and @{term "sort_of a = sort_of c"}. |
759 This implies that atoms @{term a} and @{term c} must be equal, which clashes with our |
816 This implies that atoms @{term a} and @{term c} must be equal, which clashes with our |
760 assumption @{term "c \<noteq> a"} about how we chose @{text c}. |
817 assumption @{term "c \<noteq> a"} about how we chose @{text c}.\footnote{Cheney \cite{Cheney06} |
761 Cheney \cite{Cheney06} gives similar examples for constructions that have infinite support. |
818 gives similar examples for constructions that have infinite support.} |
762 *} |
819 *} |
763 |
820 |
764 section {* Support of Finite Sets *} |
821 section {* Support of Finite Sets *} |
765 |
822 |
766 text {* |
823 text {* |
767 As shown above, sets is one instance of a type that is not generally finitely supported. |
824 Also the set type is one instance whose elements are not generally finitely |
768 However, we can easily show that finite sets of atoms are finitely |
825 supported (we will give an example in Section~\ref{concrete}). |
|
826 However, we can easily show that finite sets and co-finite sets of atoms are finitely |
769 supported, because their support can be characterised as: |
827 supported, because their support can be characterised as: |
770 |
828 |
771 \begin{lemma}\label{finatomsets} |
829 \begin{lemma}\label{finatomsets}\mbox{}\\ |
772 If @{text S} is a finite set of atoms, then @{thm (concl) supp_finite_atom_set[no_vars]}. |
830 @{text "i)"} If @{text S} is a finite set of atoms, then @{thm (concl) supp_finite_atom_set[no_vars]}.\\ |
|
831 @{text "ii)"} If @{term "UNIV - (S::atom set)"} is a finite set of atoms, then |
|
832 @{thm (concl) supp_cofinite_atom_set[no_vars]}. |
773 \end{lemma} |
833 \end{lemma} |
774 |
834 |
775 \begin{proof} |
835 \begin{proof} |
776 finite-supp-unique |
836 Both parts can be easily shown by Lemma~\ref{optimised}. We only have to observe |
|
837 that a swapping @{text "(a b)"} leaves a set @{text S} unchanged provided both |
|
838 @{text a} and @{text b} are elements in @{text S} or both are not in @{text S}. |
|
839 However if the sorts of a @{text a} and @{text b} agree, then the swapping will |
|
840 change @{text S} if either of them is an element in @{text S} and the other is |
|
841 not.\hfill\qed |
777 \end{proof} |
842 \end{proof} |
778 |
843 |
779 \noindent |
844 \noindent |
|
845 Note that a consequence of the second part of this lemma is that |
|
846 @{term "supp (UNIV::atom set) = {}"}. |
780 More difficult, however, is it to establish that finite sets of finitely |
847 More difficult, however, is it to establish that finite sets of finitely |
781 supported objects are finitely supported. |
848 supported objects are finitely supported. For this we first show that |
|
849 the union of the suports of finitely many and finitely supported objects |
|
850 is finite, namely |
|
851 |
|
852 \begin{lemma}\label{unionsupp} |
|
853 If @{text S} is a finite set whose elements are all finitely supported, then\\ |
|
854 @{text "i)"} @{thm (concl) Union_of_finite_supp_sets[no_vars]} and\\ |
|
855 @{text "ii)"} @{thm (concl) Union_included_in_supp[no_vars]}. |
|
856 \end{lemma} |
|
857 |
|
858 \begin{proof} |
|
859 The first part is by a straightforward induction on the finiteness of @{text S}. |
|
860 For the second part, we know that @{term "\<Union>x\<in>S. supp x"} is a set of atoms, which |
|
861 by the first part is finite. Therefore we know by Lemma~\ref{finatomsets}.@{text "i)"} |
|
862 that @{term "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"}. Taking @{text "f"} to be |
|
863 \mbox{@{text "\<lambda>S. \<Union> (supp ` S)"}}, we can write the right hand side as @{text "supp (f S)"}. |
|
864 Since @{text "f"} is an equivariant function, we have that |
|
865 @{text "supp (f S) \<subseteq> supp S"} by ??? This completes the second part.\hfill\qed |
|
866 \end{proof} |
|
867 |
|
868 \noindent |
|
869 With this lemma in place we can establish that |
|
870 |
|
871 \begin{lemma} |
|
872 @{thm[mode=IfThen] supp_of_finite_sets[no_vars]} |
|
873 \end{lemma} |
|
874 |
|
875 \begin{proof} |
|
876 The right-to-left inclusion is proved in Lemma~\ref{unionsupp}.@{text "ii)"}. To show the inclusion |
|
877 in the other direction we have to show Lemma~\ref{supports}.@{text "i)"} |
|
878 \end{proof} |
782 *} |
879 *} |
783 |
880 |
784 |
881 |
785 section {* Induction Principles *} |
882 section {* Induction Principles *} |
786 |
883 |