128 \begin{tabular}{@ {}l} |
124 \begin{tabular}{@ {}l} |
129 @{text "finite ((supp x) :: \<alpha>\<^isub>1 set) , \<dots>, finite ((supp x) :: \<alpha>\<^isub>n set)"} |
125 @{text "finite ((supp x) :: \<alpha>\<^isub>1 set) , \<dots>, finite ((supp x) :: \<alpha>\<^isub>n set)"} |
130 \end{tabular}\hfill\numbered{fssequence} |
126 \end{tabular}\hfill\numbered{fssequence} |
131 \end{isabelle} |
127 \end{isabelle} |
132 |
128 |
133 |
129 \noindent |
134 |
130 Because of these disadvantages, we will use a single unified atom type to |
135 |
131 represent atoms of different sorts. As a result, we have to deal with the |
136 |
132 case that a swapping of two atoms is ill-sorted: we cannot rely anymore on |
137 |
133 the type systems to exclude them. |
138 |
134 |
139 |
135 We also will not represent permutations as lists of pairs of atoms. An |
140 |
136 advantage of this representation is that the basic operations on |
141 An advantage of the |
137 permutations are already defined in Isabelle's list library: composition of |
142 list representation is that the basic operations on permutations are already |
138 two permutations (written @{text "_ @ _"}) is just list append, and |
143 defined in the list library: composition of two permutations (written @{text |
139 inversion of a permutation (written @{text "_\<^sup>-\<^sup>1"}) is just |
144 "_ @ _"}) is just list append, and inversion of a permutation (written |
140 list reversal. Another advantage is that there is a well-understood |
145 @{text "_\<^sup>-\<^sup>1"}) is just list reversal. A disadvantage is that |
141 induction principle for lists. A disadvantage, however, is that permutations |
146 permutations do not have unique representations as lists; we had to |
142 do not have unique representations as lists; we have to explicitly identify |
147 explicitly identify permutations according to the relation |
143 them according to the relation |
148 |
144 |
149 |
145 |
150 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
146 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
151 \begin{tabular}{@ {}l} |
147 \begin{tabular}{@ {}l} |
152 @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2 \<equiv> \<forall>a. \<pi>\<^isub>1 \<bullet> a = \<pi>\<^isub>2 \<bullet> a"} |
148 @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2 \<equiv> \<forall>a. \<pi>\<^isub>1 \<bullet> a = \<pi>\<^isub>2 \<bullet> a"} |
153 \end{tabular}\hfill\numbered{permequ} |
149 \end{tabular}\hfill\numbered{permequ} |
154 \end{isabelle} |
150 \end{isabelle} |
155 |
151 |
156 When lifting the permutation operation to other types, for example sets, |
152 \noindent |
157 functions and so on, we needed to ensure that every definition is |
153 This is a problem when lifting the permutation operation to other types, for |
158 well-behaved in the sense that it satisfies the following three |
154 example sets, functions and so on, we need to ensure that every definition |
159 \emph{permutation properties}: |
155 is well-behaved in the sense that it satisfies some |
|
156 \emph{permutation properties}. In the list representation we need |
|
157 to state these properties as follows: |
|
158 |
160 |
159 |
161 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
160 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
162 \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}} |
161 \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}} |
163 i) & @{text "[] \<bullet> x = x"}\\ |
162 i) & @{text "[] \<bullet> x = x"}\\ |
164 ii) & @{text "(\<pi>\<^isub>1 @ \<pi>\<^isub>2) \<bullet> x = \<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x)"}\\ |
163 ii) & @{text "(\<pi>\<^isub>1 @ \<pi>\<^isub>2) \<bullet> x = \<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x)"}\\ |
165 iii) & if @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2"} then @{text "\<pi>\<^isub>1 \<bullet> x = \<pi>\<^isub>2 \<bullet> x"} |
164 iii) & if @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2"} then @{text "\<pi>\<^isub>1 \<bullet> x = \<pi>\<^isub>2 \<bullet> x"} |
166 \end{tabular}\hfill\numbered{permprops} |
165 \end{tabular}\hfill\numbered{permprops} |
167 \end{isabelle} |
166 \end{isabelle} |
168 |
167 |
169 \noindent |
168 \noindent |
170 From these properties we were able to derive most facts about permutations, and |
169 where the last clause explicitly states that the permutation operation has |
171 the type classes of Isabelle/HOL allowed us to reason abstractly about these |
170 to produce the same result for related permutations. Moreover, permutations |
172 three properties, and then let the type system automatically enforce these |
171 as list do not satisfy the usual properties about groups. This means by |
173 properties for each type. |
172 using this representation we will not be able to reuse the extensive |
174 |
173 reasoning infrastructure in Isabelle about groups. Therefore, we will use |
175 The major problem with Isabelle/HOL's type classes, however, is that they |
174 in this paper a unique representation for permutations by representing them |
176 support operations with only a single type parameter and the permutation |
175 as functions from atoms to atoms. |
177 operations @{text "_ \<bullet> _"} used above in the permutation properties |
176 |
178 contain two! To work around this obstacle, Nominal Isabelle |
177 Using a single atom type to represent atoms of different sorts and |
179 required the user to |
178 representing permutations as functions are not new ideas. The main |
180 declare up-front the collection of \emph{all} atom types, say @{text |
179 contribution of this paper is to show an example of how to make better |
181 "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}. From this collection it used custom ML-code to |
180 theorem proving tools by choosing the right level of abstraction for the |
182 generate @{text n} type classes corresponding to the permutation properties, |
181 underlying theory---our design choices take advantage of Isabelle's type |
183 whereby in these type classes the permutation operation is restricted to |
182 system, type classes and reasoning infrastructure. The novel technical |
184 |
183 contribution is a mechanism for dealing with ``Church-style'' lambda-terms |
185 @{text [display,indent=10] "_ \<bullet> _ :: (\<alpha>\<^isub>i \<times> \<alpha>\<^isub>i) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} |
184 \cite{Church40} and HOL-based languages \cite{PittsHOL4} where variables and |
186 |
185 variable binding depend on type annotations. |
187 \noindent |
186 |
188 This operation has only a single type parameter @{text "\<beta>"} (the @{text "\<alpha>\<^isub>i"} are the |
187 The paper is organised as follows |
189 atom types given by the user). |
|
190 |
|
191 While the representation of permutations-as-lists solved the |
|
192 ``sort-respecting'' requirement and the declaration of all atom types |
|
193 up-front solved the problem with Isabelle/HOL's type classes, this setup |
|
194 caused several problems for formalising the nominal logic work: First, |
|
195 Nominal Isabelle had to generate @{text "n\<^sup>2"} definitions for the |
|
196 permutation operation over @{text "n"} types of atoms. Second, whenever we |
|
197 need to generalise induction hypotheses by quantifying over permutations, we |
|
198 have to build cumbersome quantifications like |
|
199 |
|
200 @{text [display,indent=10] "\<forall>\<pi>\<^isub>1 \<dots> \<forall>\<pi>\<^isub>n. \<dots>"} |
|
201 |
|
202 \noindent |
|
203 where the @{text "\<pi>\<^isub>i"} are of type @{text "(\<alpha>\<^isub>i \<times> \<alpha>\<^isub>i) list"}. |
|
204 The reason is that the permutation operation behaves differently for |
|
205 every @{text "\<alpha>\<^isub>i"}. Third, although the notion of support |
|
206 |
|
207 @{text [display,indent=10] "supp _ :: \<beta> \<Rightarrow> \<alpha> set"} |
|
208 |
|
209 \noindent |
|
210 which we will define later, has a generic type @{text "\<alpha> set"}, it cannot be |
|
211 used to express the support of an object over \emph{all} atoms. The reason |
|
212 is again that support can behave differently for each @{text |
|
213 "\<alpha>\<^isub>i"}. This problem is annoying, because if we need to know in |
|
214 a statement that an object, say @{text "x"}, is finitely supported we end up |
|
215 with having to state premises of the form |
|
216 |
|
217 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
|
218 \begin{tabular}{@ {}l} |
|
219 @{text "finite ((supp x) :: \<alpha>\<^isub>1 set) , \<dots>, finite ((supp x) :: \<alpha>\<^isub>n set)"} |
|
220 \end{tabular}\hfill\numbered{fssequence} |
|
221 \end{isabelle} |
|
222 |
|
223 \noindent |
|
224 Sometimes we can avoid such premises completely, if @{text x} is a member of a |
|
225 \emph{finitely supported type}. However, keeping track of finitely supported |
|
226 types requires another @{text n} type classes, and for technical reasons not |
|
227 all types can be shown to be finitely supported. |
|
228 |
|
229 The real pain of having a separate type for each atom sort arises, however, |
|
230 from another permutation property |
|
231 |
|
232 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
|
233 \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}} |
|
234 iv) & @{text "\<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x) = (\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"} |
|
235 \end{tabular} |
|
236 \end{isabelle} |
|
237 |
|
238 \noindent |
|
239 where permutation @{text "\<pi>\<^isub>1"} has type @{text "(\<alpha> \<times> \<alpha>) list"}, |
|
240 @{text "\<pi>\<^isub>2"} type @{text "(\<alpha>' \<times> \<alpha>') list"} and @{text x} type @{text |
|
241 "\<beta>"}. This property is needed in order to derive facts about how |
|
242 permutations of different types interact, which is not covered by the |
|
243 permutation properties @{text "i"}-@{text "iii"} shown in |
|
244 \eqref{permprops}. The problem is that this property involves three type |
|
245 parameters. In order to use again Isabelle/HOL's type class mechanism with |
|
246 only permitting a single type parameter, we have to instantiate the atom |
|
247 types. Consequently we end up with an additional @{text "n\<^sup>2"} |
|
248 slightly different type classes for this permutation property. |
|
249 |
|
250 While the problems and pain can be almost completely hidden from the user in |
|
251 the existing implementation of Nominal Isabelle, the work is \emph{not} |
|
252 pretty. It requires a large amount of custom ML-code and also forces the |
|
253 user to declare up-front all atom-types that are ever going to be used in a |
|
254 formalisation. In this paper we set out to solve the problems with multiple |
|
255 type parameters in the permutation operation, and in this way can dispense |
|
256 with the large amounts of custom ML-code for generating multiple variants |
|
257 for some basic definitions. The result is that we can implement a pleasingly |
|
258 simple formalisation of the nominal logic work.\smallskip |
|
259 |
|
260 \noindent |
|
261 {\bf Contributions of the paper:} Using a single atom type to represent |
|
262 atoms of different sorts and representing permutations as functions are not |
|
263 new ideas. The main contribution of this paper is to show an example of how |
|
264 to make better theorem proving tools by choosing the right level of |
|
265 abstraction for the underlying theory---our design choices take advantage of |
|
266 Isabelle's type system, type classes, and reasoning infrastructure. |
|
267 The novel |
|
268 technical contribution is a mechanism for dealing with |
|
269 ``Church-style'' lambda-terms \cite{Church40} and HOL-based languages |
|
270 \cite{PittsHOL4} where variables and variable binding depend on type |
|
271 annotations. |
|
272 |
|
273 Therefore it was decided in earlier versions of Nominal Isabelle to use a |
|
274 separate type for each sort of atoms and let the type system enforce the |
|
275 sort-respecting property of permutations. Inspired by the work on nominal |
|
276 unification \cite{UrbanPittsGabbay04}, it seemed best at the time to also |
|
277 implement permutations concretely as lists of pairs of atoms. |
|
278 |
|
279 |
|
280 *} |
188 *} |
281 |
189 |
282 section {* Sorted Atoms and Sort-Respecting Permutations *} |
190 section {* Sorted Atoms and Sort-Respecting Permutations *} |
283 |
191 |
284 text {* |
192 text {* |
285 In the nominal logic work of Pitts, binders and bound variables are |
193 In the nominal logic work of Pitts, binders and bound variables are |
286 represented by \emph{atoms}. As stated above, we need to have different |
194 represented by \emph{atoms}. As stated above, we need to have different |
287 \emph{sorts} of atoms to be able to bind different kinds of variables. A |
195 \emph{sorts} of atoms to be able to bind different kinds of variables. A |
288 basic requirement is that there must be a countably infinite number of atoms |
196 basic requirement is that there must be a countably infinite number of atoms |
289 of each sort. Unlike in our earlier work, where we identified each sort with |
197 of each sort. We implement these atoms as |
290 a separate type, we implement here atoms to be |
|
291 *} |
198 *} |
292 |
199 |
293 datatype atom\<iota> = Atom\<iota> string nat |
200 datatype atom\<iota> = Atom\<iota> string nat |
294 |
201 |
295 text {* |
202 text {* |
296 \noindent |
203 \noindent |
297 whereby the string argument specifies the sort of the atom.\footnote{A similar |
204 whereby the string argument specifies the sort of the atom.\footnote{A |
298 design choice was made by Gunter et al \cite{GunterOsbornPopescu09} |
205 similar design choice was made by Gunter et al \cite{GunterOsbornPopescu09} |
299 for their variables.} (The use type |
206 for their variables.} (The use type \emph{string} is merely for |
300 \emph{string} is merely for convenience; any countably infinite type would work |
207 convenience; any countably infinite type would work as well.) We have an |
301 as well.) |
208 auxiliary function @{text sort} that is defined as @{thm |
302 We have an auxiliary function @{text sort} that is defined as @{thm |
209 sort_of.simps[no_vars]}, and we clearly have for every finite set @{text X} |
303 sort_of.simps[no_vars]}, and we clearly have for every finite set @{text X} of |
210 of atoms and every sort @{text s} the property: |
304 atoms and every sort @{text s} the property: |
211 |
305 |
|
306 \begin{proposition}\label{choosefresh} |
212 \begin{proposition}\label{choosefresh} |
307 @{text "If finite X then there exists an atom a such that |
213 @{text "For a finite set of atoms S, there exists an atom a such that |
308 sort a = s and a \<notin> X"}. |
214 sort a = s and a \<notin> S"}. |
309 \end{proposition} |
215 \end{proposition} |
310 |
216 |
311 For implementing sort-respecting permutations, we use functions of type @{typ |
217 For implementing sort-respecting permutations, we use functions of type @{typ |
312 "atom => atom"} that @{text "i)"} are bijective; @{text "ii)"} are the |
218 "atom => atom"} that @{text "i)"} are bijective; @{text "ii)"} are the |
313 identity on all atoms, except a finite number of them; and @{text "iii)"} map |
219 identity on all atoms, except a finite number of them; and @{text "iii)"} map |
944 However, it is not too difficult to derive an induction principle, |
850 However, it is not too difficult to derive an induction principle, |
945 given the fact that we allow only permutations with a finite domain. |
851 given the fact that we allow only permutations with a finite domain. |
946 *} |
852 *} |
947 |
853 |
948 |
854 |
|
855 section {* An Abstraction Type *} |
|
856 |
|
857 text {* |
|
858 To that end, we will consider |
|
859 first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}. These pairs |
|
860 are intended to represent the abstraction, or binding, of the set of atoms @{text |
|
861 "as"} in the body @{text "x"}. |
|
862 |
|
863 The first question we have to answer is when two pairs @{text "(as, x)"} and |
|
864 @{text "(bs, y)"} are $\alpha$-equivalent? (For the moment we are interested in |
|
865 the notion of $\alpha$-equivalence that is \emph{not} preserved by adding |
|
866 vacuous binders.) To answer this question, we identify four conditions: {\it (i)} |
|
867 given a free-atom function @{text "fa"} of type \mbox{@{text "\<beta> \<Rightarrow> atom |
|
868 set"}}, then @{text x} and @{text y} need to have the same set of free |
|
869 atoms; moreover there must be a permutation @{text p} such that {\it |
|
870 (ii)} @{text p} leaves the free atoms of @{text x} and @{text y} unchanged, but |
|
871 {\it (iii)} ``moves'' their bound names so that we obtain modulo a relation, |
|
872 say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)} |
|
873 @{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The |
|
874 requirements {\it (i)} to {\it (iv)} can be stated formally as follows: |
|
875 % |
|
876 \begin{equation}\label{alphaset} |
|
877 \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r} |
|
878 \multicolumn{3}{l}{@{text "(as, x) \<approx>set R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm] |
|
879 & @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\ |
|
880 @{text "\<and>"} & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\ |
|
881 @{text "\<and>"} & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\ |
|
882 @{text "\<and>"} & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\ |
|
883 \end{array} |
|
884 \end{equation} |
|
885 |
|
886 \noindent |
|
887 Note that this relation depends on the permutation @{text |
|
888 "p"}; $\alpha$-equivalence between two pairs is then the relation where we |
|
889 existentially quantify over this @{text "p"}. Also note that the relation is |
|
890 dependent on a free-atom function @{text "fa"} and a relation @{text |
|
891 "R"}. The reason for this extra generality is that we will use |
|
892 $\approx_{\,\textit{set}}$ for both ``raw'' terms and $\alpha$-equated terms. In |
|
893 the latter case, @{text R} will be replaced by equality @{text "="} and we |
|
894 will prove that @{text "fa"} is equal to @{text "supp"}. |
|
895 |
|
896 It might be useful to consider first some examples about how these definitions |
|
897 of $\alpha$-equivalence pan out in practice. For this consider the case of |
|
898 abstracting a set of atoms over types (as in type-schemes). We set |
|
899 @{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we |
|
900 define |
|
901 |
|
902 \begin{center} |
|
903 @{text "fa(x) = {x}"} \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) = fa(T\<^isub>1) \<union> fa(T\<^isub>2)"} |
|
904 \end{center} |
|
905 |
|
906 \noindent |
|
907 Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and |
|
908 \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and |
|
909 @{text "({y, x}, y \<rightarrow> x)"} are $\alpha$-equivalent according to |
|
910 $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{res}}$ by taking @{text p} to |
|
911 be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then @{text |
|
912 "([x, y], x \<rightarrow> y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"} |
|
913 since there is no permutation that makes the lists @{text "[x, y]"} and |
|
914 @{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \<rightarrow> y"}} |
|
915 unchanged. Another example is @{text "({x}, x)"} $\approx_{\,\textit{res}}$ |
|
916 @{text "({x, y}, x)"} which holds by taking @{text p} to be the identity |
|
917 permutation. However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"} |
|
918 $\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no |
|
919 permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal |
|
920 (similarly for $\approx_{\,\textit{list}}$). It can also relatively easily be |
|
921 shown that all three notions of $\alpha$-equivalence coincide, if we only |
|
922 abstract a single atom. |
|
923 |
|
924 In the rest of this section we are going to introduce three abstraction |
|
925 types. For this we define |
|
926 % |
|
927 \begin{equation} |
|
928 @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_set (as, x) equal supp p (bs, x)"} |
|
929 \end{equation} |
|
930 |
|
931 \noindent |
|
932 (similarly for $\approx_{\,\textit{abs\_res}}$ |
|
933 and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence |
|
934 relations and equivariant. |
|
935 |
|
936 \begin{lemma}\label{alphaeq} |
|
937 The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$ |
|
938 and $\approx_{\,\textit{abs\_res}}$ are equivalence relations, and if @{term |
|
939 "abs_set (as, x) (bs, y)"} then also @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> |
|
940 bs, p \<bullet> y)"} (similarly for the other two relations). |
|
941 \end{lemma} |
|
942 |
|
943 \begin{proof} |
|
944 Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have |
|
945 a permutation @{text p} and for the proof obligation take @{term "-p"}. In case |
|
946 of transitivity, we have two permutations @{text p} and @{text q}, and for the |
|
947 proof obligation use @{text "q + p"}. All conditions are then by simple |
|
948 calculations. |
|
949 \end{proof} |
|
950 |
|
951 \noindent |
|
952 This lemma allows us to use our quotient package for introducing |
|
953 new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"} |
|
954 representing $\alpha$-equivalence classes of pairs of type |
|
955 @{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"} |
|
956 (in the third case). |
|
957 The elements in these types will be, respectively, written as: |
|
958 |
|
959 \begin{center} |
|
960 @{term "Abs_set as x"} \hspace{5mm} |
|
961 @{term "Abs_res as x"} \hspace{5mm} |
|
962 @{term "Abs_lst as x"} |
|
963 \end{center} |
|
964 |
|
965 \noindent |
|
966 indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will |
|
967 call the types \emph{abstraction types} and their elements |
|
968 \emph{abstractions}. The important property we need to derive is the support of |
|
969 abstractions, namely: |
|
970 |
|
971 \begin{theorem}[Support of Abstractions]\label{suppabs} |
|
972 Assuming @{text x} has finite support, then\\[-6mm] |
|
973 \begin{center} |
|
974 \begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l} |
|
975 %@ {thm (lhs) supp_abs(1)[no_vars]} & $=$ & @ {thm (rhs) supp_abs(1)[no_vars]}\\ |
|
976 %@ {thm (lhs) supp_abs(2)[no_vars]} & $=$ & @ {thm (rhs) supp_abs(2)[no_vars]}\\ |
|
977 %@ {thm (lhs) supp_abs(3)[where bs="as", no_vars]} & $=$ & @ {thm (rhs) supp_abs(3)[where bs="as", no_vars]} |
|
978 \end{tabular} |
|
979 \end{center} |
|
980 \end{theorem} |
|
981 |
|
982 \noindent |
|
983 Below we will show the first equation. The others |
|
984 follow by similar arguments. By definition of the abstraction type @{text "abs_set"} |
|
985 we have |
|
986 % |
|
987 \begin{equation}\label{abseqiff} |
|
988 %@ {thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\; |
|
989 %@ {thm (rhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} |
|
990 \end{equation} |
|
991 |
|
992 \noindent |
|
993 and also |
|
994 % |
|
995 \begin{equation}\label{absperm} |
|
996 @{thm permute_Abs[no_vars]} |
|
997 \end{equation} |
|
998 |
|
999 \noindent |
|
1000 The second fact derives from the definition of permutations acting on pairs |
|
1001 \eqref{permute} and $\alpha$-equivalence being equivariant |
|
1002 (see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show |
|
1003 the following lemma about swapping two atoms in an abstraction. |
|
1004 |
|
1005 \begin{lemma} |
|
1006 %@ {thm[mode=IfThen] abs_swap1(1)[where bs="as", no_vars]} |
|
1007 \end{lemma} |
|
1008 |
|
1009 \begin{proof} |
|
1010 This lemma is straightforward using \eqref{abseqiff} and observing that |
|
1011 the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}. |
|
1012 Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}). |
|
1013 \end{proof} |
|
1014 |
|
1015 \noindent |
|
1016 Assuming that @{text "x"} has finite support, this lemma together |
|
1017 with \eqref{absperm} allows us to show |
|
1018 % |
|
1019 \begin{equation}\label{halfone} |
|
1020 %@ {thm abs_supports(1)[no_vars]} |
|
1021 \end{equation} |
|
1022 |
|
1023 \noindent |
|
1024 which by Property~\ref{supportsprop} gives us ``one half'' of |
|
1025 Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish |
|
1026 it, we use a trick from \cite{Pitts04} and first define an auxiliary |
|
1027 function @{text aux}, taking an abstraction as argument: |
|
1028 % |
|
1029 \begin{center} |
|
1030 @{thm supp_set.simps[THEN eq_reflection, no_vars]} |
|
1031 \end{center} |
|
1032 |
|
1033 \noindent |
|
1034 Using the second equation in \eqref{equivariance}, we can show that |
|
1035 @{text "aux"} is equivariant (since @{term "p \<bullet> (supp x - as) = |
|
1036 (supp (p \<bullet> x)) - (p \<bullet> as)"}) and therefore has empty support. |
|
1037 This in turn means |
|
1038 % |
|
1039 \begin{center} |
|
1040 @{term "supp (supp_gen (Abs_set as x)) \<subseteq> supp (Abs_set as x)"} |
|
1041 \end{center} |
|
1042 |
|
1043 \noindent |
|
1044 using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set, |
|
1045 we further obtain |
|
1046 % |
|
1047 \begin{equation}\label{halftwo} |
|
1048 %@ {thm (concl) supp_abs_subset1(1)[no_vars]} |
|
1049 \end{equation} |
|
1050 |
|
1051 \noindent |
|
1052 since for finite sets of atoms, @{text "bs"}, we have |
|
1053 @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}. |
|
1054 Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes |
|
1055 Theorem~\ref{suppabs}. |
|
1056 |
|
1057 The method of first considering abstractions of the |
|
1058 form @{term "Abs_set as x"} etc is motivated by the fact that |
|
1059 we can conveniently establish at the Isabelle/HOL level |
|
1060 properties about them. It would be |
|
1061 laborious to write custom ML-code that derives automatically such properties |
|
1062 for every term-constructor that binds some atoms. Also the generality of |
|
1063 the definitions for $\alpha$-equivalence will help us in the next section. |
|
1064 *} |
|
1065 |
|
1066 |
949 section {* Concrete Atom Types *} |
1067 section {* Concrete Atom Types *} |
950 |
1068 |
951 text {* |
1069 text {* |
952 |
1070 |
953 So far, we have presented a system that uses only a single multi-sorted atom |
1071 So far, we have presented a system that uses only a single multi-sorted atom |