# HG changeset patch # User Christian Urban # Date 1269278353 -3600 # Node ID 5b0bdd64956e2c159293315647f6c5d5f859b733 # Parent 1dbc4f33549c0c0bd9102bf3cffca762b029d777 more on the paper diff -r 1dbc4f33549c -r 5b0bdd64956e Paper/Paper.thy --- a/Paper/Paper.thy Mon Mar 22 16:22:28 2010 +0100 +++ b/Paper/Paper.thy Mon Mar 22 18:19:13 2010 +0100 @@ -385,36 +385,34 @@ section {* General Binders *} text {* - In order to keep our work manageable we give need to give definitions - and perform proofs inside Isabelle wherever possible, as opposed to write - custom ML-code that generates them for each - instance of a term-calculus. To this end we will first consider pairs + In Nominal Isabelle the user is expected to write down a specification of a + term-calculus and a reasoning infrastructure is then automatically derived + from this specifcation (remember that Nominal Isabelle is a definitional + extension of Isabelle/HOL and cannot introduce new axioms). + - \begin{equation}\label{three} - \mbox{@{text "(as, x) :: (atom set) \ \"}} - \end{equation} - - \noindent - consisting of a set of atoms and an object of generic type. These pairs - are intended to represent the abstraction or binding of the set $as$ - in the body $x$ (similarly to type-schemes given in \eqref{tysch}). + In order to keep our work manageable, we will wherever possible state + definitions and perform proofs inside Isabelle, as opposed to write custom + ML-code that generates them for each instance of a term-calculus. To that + end, we will consider pairs @{text "(as, x)"} of type @{text "(atom set) \ \"}. + These pairs are intended to represent the abstraction, or binding, of the set $as$ + in the body $x$. - The first question we have to answer is when we should consider pairs such as - $(as, x)$ and $(bs, y)$ as alpha-equivalent? (At the moment we are interested in + The first question we have to answer is when the pairs $(as, x)$ and $(bs, y)$ are + alpha-equivalent? (At the moment we are interested in the notion of alpha-equivalence that is \emph{not} preserved by adding - vacuous binders.) To answer this we identify four conditions: {\it i)} given - a free-variable function of type \mbox{@{text "fv :: \ \ atom set"}}, then $x$ and $y$ + vacuous binders.) To answer this, we identify four conditions: {\it i)} given + a free-variable function $\fv$ of type \mbox{@{text "\ \ atom set"}}, then $x$ and $y$ need to have the same set of free variables; moreover there must be a permutation, - $p$ that {\it ii)} leaves the free variables $x$ and $y$ unchanged, - but {\it iii)} ``moves'' their bound names so that we obtain modulo a relation, + $p$ so that {\it ii)} it leaves the free variables $x$ and $y$ unchanged, + but {\it iii)} ``moves'' their bound names such that we obtain modulo a relation, say \mbox{@{text "_ R _"}}, two equal terms. We also require {\it iv)} that $p$ makes - the abstracted sets $as$ and $bs$ equal (since at the moment we do not want - that the sets $as$ and $bs$ differ on vacuous binders). These requirements can - be stated formally as follows + the abstracted sets $as$ and $bs$ equal. The requirements {\it i)} to {\it iv)} can + be stated formally as follows: % \begin{equation}\label{alphaset} \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l} - \multicolumn{2}{l}{(as, x) \approx_{set}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm] + \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{set}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm] & @{text "fv(x) - as = fv(y) - bs"}\\ \wedge & @{text "fv(x) - as #* p"}\\ \wedge & @{text "(p \ x) R y"}\\ @@ -423,20 +421,23 @@ \end{equation} \noindent - Alpha equivalence between such pairs is then the relation with the additional - existential quantification over $p$. Note that this relation is additionally - dependent on the free-variable function $\fv$ and the relation $R$. The reason - for this generality is that we want to use $\approx_{set}$ for both ``raw'' terms - and alpha-equated terms. In the latter case, $R$ can be replaced by equality $(op =)$ and - we are going to prove that $\fv$ will be equal to the support of $x$ and $y$. + Note that this relation is dependent on $p$. Alpha-equivalence is then the relation where + we existentially quantify over this $p$. + Also note that the relation is dependent on a free-variable function $\fv$ and a relation + $R$. The reason for this extra generality is that we will use $\approx_{set}$ for both + ``raw'' terms and alpha-equated terms. In the latter case, $R$ will be replaced by + equality $(op =)$ and we are going to prove that $\fv$ will be equal to the support + of $x$ and $y$. To have these parameters means, however, we can derive properties about + them generically. The definition in \eqref{alphaset} does not make any distinction between the - order of abstracted variables. If we do want this then we can define alpha-equivalence - for pairs of the form \mbox{@{text "(as, x) :: (atom list) \ \"}} by + order of abstracted variables. If we want this, then we can define alpha-equivalence + for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \ \"} + as follows % \begin{equation}\label{alphalist} \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l} - \multicolumn{2}{l}{(as, x) \approx_{list}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm] + \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{list}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm] & @{text "fv(x) - (set as) = fv(y) - (set bs)"}\\ \wedge & @{text "fv(x) - (set as) #* p"}\\ \wedge & @{text "(p \ x) R y"}\\ @@ -448,34 +449,65 @@ where $set$ is just the function that coerces a list of atoms into a set of atoms. If we do not want to make any difference between the order of binders and - allow vacuous binders, then we just need to drop the fourth condition in \eqref{alphaset} - and define + also allow vacuous binders, then we keep sets of binders, but drop the fourth + condition in \eqref{alphaset}: % - \begin{equation}\label{alphaset} + \begin{equation}\label{alphares} \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l} - \multicolumn{2}{l}{(as, x) \approx_{res}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm] + \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{res}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm] & @{text "fv(x) - as = fv(y) - bs"}\\ \wedge & @{text "fv(x) - as #* p"}\\ \wedge & @{text "(p \ x) R y"}\\ \end{array} \end{equation} - To get a feeling how these definitions pan out in practise consider the case of - abstracting names over types (like in type-schemes). For this we set $R$ to be - the equality and for $\fv(T)$ we define + \begin{exmple}\rm + It might be useful to consider some examples for how these definitions pan out in practise. + For this consider the case of abstracting a set of variables over types (as in type-schemes). + We set $R$ to be the equality and for $\fv(T)$ we define \begin{center} $\fv(x) = \{x\} \qquad \fv(T_1 \rightarrow T_2) = \fv(T_1) \cup \fv(T_2)$ \end{center} \noindent - Now reacall the examples in \eqref{ex1}, \eqref{ex2} and \eqref{ex3}: it can be easily - checked that @{text "({x,y}, x \ y)"} and - @{text "({y,x}, y \ x)"} are equal according to $\approx_{set}$ and $\approx_{ref}$ by taking $p$ to - be the swapping @{text "(x \ y)"}; but assuming @{text "x \ y"} then for instance - $([x,y], x \rightarrow y) \not\approx_{list} ([y,x], x \rightarrow y)$ since there is no permutation that - makes the lists @{text "[x,y]"} and @{text "[y,x]"} equal, but leaves the type \mbox{@{text "x \ y"}} - unchanged. + Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and \eqref{ex3}. It can be easily + checked that @{text "({x, y}, x \ y)"} and + @{text "({y, x}, y \ x)"} are equal according to $\approx_{set}$ and $\approx_{res}$ by taking $p$ to + be the swapping @{term "(x \ y)"}. In case of @{text "x \ y"} then + $([x, y], x \rightarrow y) \not\approx_{list} ([y,x], x \rightarrow y)$ since there is no permutation that + makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and in addition leaves the + type \mbox{@{text "x \ y"}} unchanged. Again if @{text "x \ y"}, we have that + $(\{x\}, x) \approx_{res} (\{x,y\}, x)$ by taking $p$ to be the identity permutation. + However $(\{x\}, x) \not\approx_{set} (\{x,y\}, x)$ since there is no permutation that makes + the sets $\{x\}$ and $\{x,y\}$ equal (similarly for $\approx_{list}$). + \end{exmple} + + \noindent + Let $\star$ range over $\{set, res, list\}$. We prove next under which + conditions the $\approx\hspace{0.05mm}_\star^{\fv, R, p}$ are equivalence + relations and equivariant: + + \begin{lemma} + {\it i)} Given the fact that $x\;R\;x$ holds, then + $(as, x) \approx\hspace{0.05mm}^{\fv, R, 0}_\star (as, x)$. {\it ii)} Given + that @{text "(p \ x) R y"} implies @{text "(-p \ y) R x"}, then + $(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$ implies + $(bs, y) \approx\hspace{0.05mm}^{\fv, R, - p}_\star (as, x)$. {\it iii)} Given + that @{text "(p \ x) R y"} and @{text "(q \ y) R z"} implies + @{text "((q + p) \ x) R z"}, then $(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$ + and $(bs, y) \approx\hspace{0.05mm}^{\fv, R, q}_\star (cs, z)$ implies + $(as, x) \approx\hspace{0.05mm}^{\fv, R, q + p}_\star (cs, z)$. Given + @{text "(q \ x) R y"} implies @{text "(p \ (q \ x)) R (p \ y)"} and + @{text "p \ (fv x) = fv (p \ x)"} then @{text "p \ (fv y) = fv (p \ y)"}, then + $(as, x) \approx\hspace{0.05mm}^{\fv, R, q}_\star (bs, y)$ implies + $(p \;\isasymbullet\; as, p \;\isasymbullet\; x) \approx\hspace{0.05mm}^{\fv, R, q}_\star + (p \;\isasymbullet\; bs, p \;\isasymbullet\; y)$. + \end{lemma} + + \begin{proof} + All properties are by unfolding the definitions and simple calculations. + \end{proof} *} section {* Alpha-Equivalence and Free Variables *} diff -r 1dbc4f33549c -r 5b0bdd64956e Paper/document/root.tex --- a/Paper/document/root.tex Mon Mar 22 16:22:28 2010 +0100 +++ b/Paper/document/root.tex Mon Mar 22 18:19:13 2010 +0100 @@ -3,6 +3,7 @@ \usepackage{isabellesym} \usepackage{amsmath} \usepackage{amssymb} +\usepackage{amsthm} \usepackage{tikz} \usepackage{pgf} \usepackage{pdfsetup} @@ -27,10 +28,12 @@ %----------------- theorem definitions ---------- -\newtheorem{property}{Property}[section] -\newtheorem{Theorem}{Theorem}[section] -\newtheorem{Definition}[Theorem]{Definition} -\newtheorem{Example}{\it Example}[section] +\theoremstyle{plain} +\newtheorem{thm}{Theorem}[section] +\newtheorem{property}[thm]{Property} +\newtheorem{lemma}[thm]{Lemma} +\newtheorem{defn}[thm]{Definition} +\newtheorem{exmple}[thm]{Example} %-------------------- environment definitions ----------------- \newenvironment{example}[0]{\begin{Example} \it}{\end{Example}}