Paper/Paper.thy
changeset 1579 5b0bdd64956e
parent 1577 8466fe2216da
child 1587 b6da798cef68
equal deleted inserted replaced
1578:1dbc4f33549c 1579:5b0bdd64956e
   383 
   383 
   384 
   384 
   385 section {* General Binders *}
   385 section {* General Binders *}
   386 
   386 
   387 text {*
   387 text {*
   388   In order to keep our work manageable we give need to give definitions  
   388   In Nominal Isabelle the user is expected to write down a specification of a
   389   and perform proofs inside Isabelle wherever possible, as opposed to write
   389   term-calculus and a reasoning infrastructure is then automatically derived
   390   custom ML-code that generates them  for each 
   390   from this specifcation (remember that Nominal Isabelle is a definitional
   391   instance of a term-calculus. To this end we will first consider pairs
   391   extension of Isabelle/HOL and cannot introduce new axioms).
   392 
   392 
   393   \begin{equation}\label{three}
   393 
   394   \mbox{@{text "(as, x) :: (atom set) \<times> \<beta>"}}
   394   In order to keep our work manageable, we will wherever possible state
   395   \end{equation}
   395   definitions and perform proofs inside Isabelle, as opposed to write custom
   396  
   396   ML-code that generates them for each instance of a term-calculus. To that
   397   \noindent
   397   end, we will consider pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}.
   398   consisting of a set of atoms and an object of generic type. These pairs
   398   These pairs are intended to represent the abstraction, or binding, of the set $as$ 
   399   are intended to represent the abstraction or binding of the set $as$ 
   399   in the body $x$.
   400   in the body $x$ (similarly to type-schemes given in \eqref{tysch}). 
   400 
   401 
   401   The first question we have to answer is when the pairs $(as, x)$ and $(bs, y)$ are
   402   The first question we have to answer is when we should consider pairs such as
   402   alpha-equivalent? (At the moment we are interested in
   403   $(as, x)$ and $(bs, y)$ as alpha-equivalent? (At the moment we are interested in
       
   404   the notion of alpha-equivalence that is \emph{not} preserved by adding 
   403   the notion of alpha-equivalence that is \emph{not} preserved by adding 
   405   vacuous binders.) To answer this we identify four conditions: {\it i)} given 
   404   vacuous binders.) To answer this, we identify four conditions: {\it i)} given 
   406   a free-variable function of type \mbox{@{text "fv :: \<beta> \<Rightarrow> atom set"}}, then $x$ and $y$ 
   405   a free-variable function $\fv$ of type \mbox{@{text "\<beta> \<Rightarrow> atom set"}}, then $x$ and $y$ 
   407   need to have the same set of free variables; moreover there must be a permutation,
   406   need to have the same set of free variables; moreover there must be a permutation,
   408   $p$ that {\it ii)} leaves the free variables $x$ and $y$ unchanged, 
   407   $p$ so that {\it ii)} it leaves the free variables $x$ and $y$ unchanged, 
   409   but {\it iii)} ``moves'' their bound names so that we obtain modulo a relation, 
   408   but {\it iii)} ``moves'' their bound names such that we obtain modulo a relation, 
   410   say \mbox{@{text "_ R _"}}, two equal terms. We also require {\it iv)} that $p$ makes 
   409   say \mbox{@{text "_ R _"}}, two equal terms. We also require {\it iv)} that $p$ makes 
   411   the abstracted sets $as$ and $bs$ equal (since at the moment we do not want 
   410   the abstracted sets $as$ and $bs$ equal. The requirements {\it i)} to {\it iv)} can 
   412   that the sets $as$ and $bs$ differ on vacuous binders). These requirements can 
   411   be stated formally as follows:
   413   be stated formally as follows
       
   414   %
   412   %
   415   \begin{equation}\label{alphaset}
   413   \begin{equation}\label{alphaset}
   416   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
   414   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
   417   \multicolumn{2}{l}{(as, x) \approx_{set}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
   415   \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{set}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
   418              & @{text "fv(x) - as = fv(y) - bs"}\\
   416              & @{text "fv(x) - as = fv(y) - bs"}\\
   419   \wedge     & @{text "fv(x) - as #* p"}\\
   417   \wedge     & @{text "fv(x) - as #* p"}\\
   420   \wedge     & @{text "(p \<bullet> x) R y"}\\
   418   \wedge     & @{text "(p \<bullet> x) R y"}\\
   421   \wedge     & @{text "(p \<bullet> as) = bs"}\\ 
   419   \wedge     & @{text "(p \<bullet> as) = bs"}\\ 
   422   \end{array}
   420   \end{array}
   423   \end{equation}
   421   \end{equation}
   424 
   422 
   425   \noindent
   423   \noindent
   426   Alpha equivalence between such pairs is then the relation with the additional 
   424   Note that this relation is dependent on $p$. Alpha-equivalence is then the relation where 
   427   existential quantification over $p$. Note that this relation is additionally 
   425   we existentially quantify over this $p$. 
   428   dependent on the free-variable function $\fv$ and the relation $R$. The reason 
   426   Also note that the relation is dependent on a free-variable function $\fv$ and a relation 
   429   for this generality is that we want to use $\approx_{set}$ for both ``raw'' terms
   427   $R$. The reason for this extra generality is that we will use $\approx_{set}$ for both 
   430   and alpha-equated terms. In the latter case, $R$ can be replaced by equality $(op =)$ and
   428   ``raw'' terms and alpha-equated terms. In the latter case, $R$ will be replaced by 
   431   we are going to prove that $\fv$ will be equal to the support of $x$ and $y$.
   429   equality $(op =)$ and we are going to prove that $\fv$ will be equal to the support 
       
   430   of $x$ and $y$. To have these parameters means, however, we can derive properties about 
       
   431   them generically.
   432 
   432 
   433   The definition in \eqref{alphaset} does not make any distinction between the
   433   The definition in \eqref{alphaset} does not make any distinction between the
   434   order of abstracted variables. If we do want this then we can define alpha-equivalence 
   434   order of abstracted variables. If we want this, then we can define alpha-equivalence 
   435   for pairs of the form \mbox{@{text "(as, x) :: (atom list) \<times> \<beta>"}} by
   435   for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \<times> \<beta>"} 
       
   436   as follows
   436   %
   437   %
   437   \begin{equation}\label{alphalist}
   438   \begin{equation}\label{alphalist}
   438   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
   439   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
   439   \multicolumn{2}{l}{(as, x) \approx_{list}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
   440   \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{list}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
   440              & @{text "fv(x) - (set as) = fv(y) - (set bs)"}\\
   441              & @{text "fv(x) - (set as) = fv(y) - (set bs)"}\\
   441   \wedge     & @{text "fv(x) - (set as) #* p"}\\
   442   \wedge     & @{text "fv(x) - (set as) #* p"}\\
   442   \wedge     & @{text "(p \<bullet> x) R y"}\\
   443   \wedge     & @{text "(p \<bullet> x) R y"}\\
   443   \wedge     & @{text "(p \<bullet> as) = bs"}\\ 
   444   \wedge     & @{text "(p \<bullet> as) = bs"}\\ 
   444   \end{array}
   445   \end{array}
   446   
   447   
   447   \noindent
   448   \noindent
   448   where $set$ is just the function that coerces a list of atoms into a set of atoms.
   449   where $set$ is just the function that coerces a list of atoms into a set of atoms.
   449 
   450 
   450   If we do not want to make any difference between the order of binders and
   451   If we do not want to make any difference between the order of binders and
   451   allow vacuous binders, then we just need to drop the fourth condition in \eqref{alphaset}
   452   also allow vacuous binders, then we keep sets of binders, but drop the fourth 
   452   and define
   453   condition in \eqref{alphaset}:
   453   %
   454   %
   454   \begin{equation}\label{alphaset}
   455   \begin{equation}\label{alphares}
   455   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
   456   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
   456   \multicolumn{2}{l}{(as, x) \approx_{res}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
   457   \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{res}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
   457              & @{text "fv(x) - as = fv(y) - bs"}\\
   458              & @{text "fv(x) - as = fv(y) - bs"}\\
   458   \wedge     & @{text "fv(x) - as #* p"}\\
   459   \wedge     & @{text "fv(x) - as #* p"}\\
   459   \wedge     & @{text "(p \<bullet> x) R y"}\\
   460   \wedge     & @{text "(p \<bullet> x) R y"}\\
   460   \end{array}
   461   \end{array}
   461   \end{equation}
   462   \end{equation}
   462 
   463 
   463   To get a feeling how these definitions pan out in practise consider the case of 
   464   \begin{exmple}\rm
   464   abstracting names over types (like in type-schemes). For this we set $R$ to be 
   465   It might be useful to consider some examples for how these definitions pan out in practise.
   465   the equality and for $\fv(T)$ we define
   466   For this consider the case of abstracting a set of variables over types (as in type-schemes). 
       
   467   We set $R$ to be the equality and for $\fv(T)$ we define
   466 
   468 
   467   \begin{center}
   469   \begin{center}
   468   $\fv(x) = \{x\}  \qquad \fv(T_1 \rightarrow T_2) = \fv(T_1) \cup \fv(T_2)$
   470   $\fv(x) = \{x\}  \qquad \fv(T_1 \rightarrow T_2) = \fv(T_1) \cup \fv(T_2)$
   469   \end{center}
   471   \end{center}
   470 
   472 
   471   \noindent
   473   \noindent
   472   Now reacall the examples in \eqref{ex1}, \eqref{ex2} and \eqref{ex3}: it can be easily 
   474   Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and \eqref{ex3}. It can be easily 
   473   checked that @{text "({x,y}, x \<rightarrow> y)"} and
   475   checked that @{text "({x, y}, x \<rightarrow> y)"} and
   474   @{text "({y,x}, y \<rightarrow> x)"} are equal according to $\approx_{set}$ and $\approx_{ref}$ by taking $p$ to
   476   @{text "({y, x}, y \<rightarrow> x)"} are equal according to $\approx_{set}$ and $\approx_{res}$ by taking $p$ to
   475   be the swapping @{text "(x \<rightleftharpoons> y)"}; but assuming @{text "x \<noteq> y"} then for instance 
   477   be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"} then 
   476   $([x,y], x \rightarrow y) \not\approx_{list} ([y,x], x \rightarrow y)$ since there is no permutation that 
   478   $([x, y], x \rightarrow y) \not\approx_{list} ([y,x], x \rightarrow y)$ since there is no permutation that 
   477   makes the lists @{text "[x,y]"} and @{text "[y,x]"} equal, but leaves the type \mbox{@{text "x \<rightarrow> y"}}
   479   makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and in addition leaves the 
   478   unchanged.
   480   type \mbox{@{text "x \<rightarrow> y"}} unchanged. Again if @{text "x \<noteq> y"}, we have that
       
   481    $(\{x\}, x) \approx_{res} (\{x,y\}, x)$ by taking $p$ to be the identity permutation.
       
   482   However $(\{x\}, x) \not\approx_{set} (\{x,y\}, x)$ since there is no permutation that makes
       
   483   the sets $\{x\}$ and $\{x,y\}$ equal (similarly for $\approx_{list}$).
       
   484   \end{exmple}
       
   485 
       
   486   \noindent
       
   487   Let $\star$ range over $\{set, res, list\}$. We prove next under which 
       
   488   conditions the $\approx\hspace{0.05mm}_\star^{\fv, R, p}$ are equivalence 
       
   489   relations and equivariant:
       
   490 
       
   491   \begin{lemma}
       
   492   {\it i)} Given the fact that $x\;R\;x$ holds, then 
       
   493   $(as, x) \approx\hspace{0.05mm}^{\fv, R, 0}_\star (as, x)$. {\it ii)} Given
       
   494   that @{text "(p \<bullet> x) R y"} implies @{text "(-p \<bullet> y) R x"}, then
       
   495   $(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$ implies
       
   496   $(bs, y) \approx\hspace{0.05mm}^{\fv, R, - p}_\star (as, x)$. {\it iii)} Given
       
   497   that @{text "(p \<bullet> x) R y"} and @{text "(q \<bullet> y) R z"} implies 
       
   498   @{text "((q + p) \<bullet> x) R z"}, then $(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$
       
   499   and $(bs, y) \approx\hspace{0.05mm}^{\fv, R, q}_\star (cs, z)$ implies
       
   500   $(as, x) \approx\hspace{0.05mm}^{\fv, R, q + p}_\star (cs, z)$. Given
       
   501   @{text "(q \<bullet> x) R y"} implies @{text "(p \<bullet> (q \<bullet> x)) R (p \<bullet> y)"} and
       
   502   @{text "p \<bullet> (fv x) = fv (p \<bullet> x)"} then @{text "p \<bullet> (fv y) = fv (p \<bullet> y)"}, then
       
   503   $(as, x) \approx\hspace{0.05mm}^{\fv, R, q}_\star (bs, y)$ implies
       
   504   $(p \;\isasymbullet\; as, p \;\isasymbullet\; x) \approx\hspace{0.05mm}^{\fv, R, q}_\star 
       
   505   (p \;\isasymbullet\; bs, p \;\isasymbullet\; y)$.
       
   506   \end{lemma}
       
   507   
       
   508   \begin{proof}
       
   509   All properties are by unfolding the definitions and simple calculations. 
       
   510   \end{proof}
   479 *}
   511 *}
   480 
   512 
   481 section {* Alpha-Equivalence and Free Variables *}
   513 section {* Alpha-Equivalence and Free Variables *}
   482 
   514 
   483 text {*
   515 text {*