nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:4c5881455923
+:9807d30c0e54
 alpha_gen ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and
 alpha_lst ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and
 alpha_res ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and
 abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
 abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup>  _") and
-fv ("fv'(_')" [100] 100) and
+fv ("fa'(_')" [100] 100) and
 equal ("=") and
 alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
 Abs ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and
 Abs_lst ("[_]\<^bsub>list\<^esub>._") and
 Abs_dist ("[_]\<^bsub>#list\<^esub>._") and
 section {* Introduction *}
 text {*
-%%%  @{text "(1, (2, 3))"}
 So far, Nominal Isabelle provided a mechanism for constructing
 $\alpha$-equated terms, for example lambda-terms
 \begin{center}
 be bound. Another is that each bound variable comes with a kind or type
 annotation. Representing such binders with single binders and reasoning
 about them in a theorem prover would be a major pain.  \medskip
 \noindent
-{\bf Contributions:}  We provide novel three definitions for when terms
+{\bf Contributions:}  We provide three novel definitions for when terms
 involving general binders are $\alpha$-equivalent. These definitions are
 inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
 proofs, we establish a reasoning infrastructure for $\alpha$-equated
 terms, including properties about support, freshness and equality
 conditions for $\alpha$-equated terms. We are also able to derive strong
 to aid the description of what follows.
 Two central notions in the nominal logic work are sorted atoms and
 sort-respecting permutations of atoms. We will use the letters @{text "a,
 b, c, \<dots>"} to stand for atoms and @{text "p, q, \<dots>"} to stand for
-permutations.  The sorts of atoms can be used to represent different kinds of
+permutations. The purpose of atoms is to represent variables, be they bound or free.
+The sorts of atoms can be used to represent different kinds of
 variables, such as the term-, coercion- and type-variables in Core-Haskell.
 It is assumed that there is an infinite supply of atoms for each
 sort. However, in the interest of brevity, we shall restrict ourselves
 in what follows to only one sort of atoms.
 @{term "supp b"} & = & @{term "{}"}\\
 @{term "supp p"} & = & @{term "{a. p \<bullet> a \<noteq> a}"}
 \end{eqnarray}
 \noindent
-In some cases it can be difficult to characterise the support precisely, and
+in some cases it can be difficult to characterise the support precisely, and
 only an approximation can be established (see \eqref{suppfun} above). Reasoning about
 such approximations can be simplified with the notion \emph{supports}, defined
 as follows:
 \begin{defn}
 The first question we have to answer is when two pairs @{text "(as, x)"} and
 @{text "(bs, y)"} are $\alpha$-equivalent? (For the moment we are interested in
 the notion of $\alpha$-equivalence that is \emph{not} preserved by adding
 vacuous binders.) To answer this question, we identify four conditions: {\it (i)}
-given a free-variable function @{text "fv"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
+given a free-atom function @{text "fa"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
 set"}}, then @{text x} and @{text y} need to have the same set of free
-variables; moreover there must be a permutation @{text p} such that {\it
+atomss; moreover there must be a permutation @{text p} such that {\it
-(ii)} @{text p} leaves the free variables of @{text x} and @{text y} unchanged, but
+(ii)} @{text p} leaves the free atoms of @{text x} and @{text y} unchanged, but
 {\it (iii)} ``moves'' their bound names so that we obtain modulo a relation,
 say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)}
 @{text p} makes the sets of abstracted atoms @{text as} and @{text 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@ {\hspace{4mm}}r}
-\multicolumn{3}{l}{@{term "(as, x) \<approx>gen R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+\multicolumn{3}{l}{@{term "(as, x) \<approx>gen R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
-& @{term "fv(x) - as = fv(y) - bs"} & \mbox{\it (i)}\\
+& @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\
-@{text "\<and>"} & @{term "(fv(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
+@{text "\<and>"} & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
 @{text "\<and>"} & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
 @{text "\<and>"} & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\
 \end{array}
 \end{equation}
 \noindent
 Note that this relation depends on the permutation @{text
 "p"}; $\alpha$-equivalence between two pairs is then the relation where we
 existentially quantify over this @{text "p"}. Also note that the relation is
-dependent on a free-variable function @{text "fv"} and a relation @{text
+dependent on a free-atom function @{text "fa"} and a relation @{text
 "R"}. The reason for this extra generality is that we will use
 $\approx_{\,\textit{set}}$ for both ``raw'' terms and $\alpha$-equated terms. In
 the latter case, @{text R} will be replaced by equality @{text "="} and we
-will prove that @{text "fv"} is equal to @{text "supp"}.
+will prove that @{text "fa"} is equal to @{text "supp"}.
 The definition in \eqref{alphaset} does not make any distinction between the
-order of abstracted variables. If we want this, then we can define $\alpha$-equivalence
+order of abstracted atoms. If we want this, then we can define $\alpha$-equivalence
 for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \<times> \<beta>"}
 as follows
 %
 \begin{equation}\label{alphalist}
 \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
-\multicolumn{2}{l}{@{term "(as, x) \<approx>lst R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+\multicolumn{2}{l}{@{term "(as, x) \<approx>lst R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
-& @{term "fv(x) - (set as) = fv(y) - (set bs)"} & \mbox{\it (i)}\\
+& @{term "fa(x) - (set as) = fa(y) - (set bs)"} & \mbox{\it (i)}\\
-\wedge     & @{term "(fv(x) - set as) \<sharp>* p"} & \mbox{\it (ii)}\\
+\wedge     & @{term "(fa(x) - set as) \<sharp>* p"} & \mbox{\it (ii)}\\
 \wedge     & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
 \wedge     & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\
 \end{array}
 \end{equation}
 also allow vacuous binders, then we keep sets of binders, but drop the fourth
 condition in \eqref{alphaset}:
 %
 \begin{equation}\label{alphares}
 \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
-\multicolumn{2}{l}{@{term "(as, x) \<approx>res R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+\multicolumn{2}{l}{@{term "(as, x) \<approx>res R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
-& @{term "fv(x) - as = fv(y) - bs"} & \mbox{\it (i)}\\
+& @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\
-\wedge     & @{term "(fv(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
+\wedge     & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
 \wedge     & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
 \end{array}
 \end{equation}
 It might be useful to consider first some examples about how these definitions
 of $\alpha$-equivalence pan out in practice.  For this consider the case of
-abstracting a set of variables over types (as in type-schemes). We set
+abstracting a set of atoms over types (as in type-schemes). We set
-@{text R} to be the usual equality @{text "="} and for @{text "fv(T)"} we
+@{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we
 define
 \begin{center}
-@{text "fv(x) = {x}"}  \hspace{5mm} @{text "fv(T\<^isub>1 \<rightarrow> T\<^isub>2) = fv(T\<^isub>1) \<union> fv(T\<^isub>2)"}
+@{text "fa(x) = {x}"}  \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) = fa(T\<^isub>1) \<union> fa(T\<^isub>2)"}
 \end{center}
 \noindent
 Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and
 \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and
 %Interestingly, in case of \isacommand{bind\_set}
 %and \isacommand{bind\_res} the binding clauses above will make a difference to the semantics
 %of the specifications (the corresponding $\alpha$-equivalence will differ). We will
 %show this later with an example.
-There are also some restrictions we need to impose on binding clauses. The
+There are also some restrictions we need to impose on our binding clauses in comparison to
+the ones of Ott. The
 main idea behind these restrictions is that we obtain a sensible notion of
-$\alpha$-equivalence where it is ensured that within a given scope a
+$\alpha$-equivalence where it is ensured that within a given scope an
-variable occurence cannot be both bound and free at the same time.  The first
+atom occurence cannot be both bound and free at the same time.  The first
 restriction is that a body can only occur in
 \emph{one} binding clause of a term constructor (this ensures that the bound
-variables of a body cannot be free at the same time by specifying an
+atoms of a body cannot be free at the same time by specifying an
 alternative binder for the same body). For binders we distinguish between
 \emph{shallow} and \emph{deep} binders.  Shallow binders are just
 labels. The restriction we need to impose on them is that in case of
 \isacommand{bind\_set} and \isacommand{bind\_res} the labels must either
 refer to atom types or to sets of atom types; in case of \isacommand{bind}
 \noindent
 The difference is that with @{text Let} we only want to bind the atoms @{text
 "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms
 inside the assignment. This difference has consequences for the associated
-notions of free-variables and $\alpha$-equivalence.
+notions of free-atoms and $\alpha$-equivalence.
-To make sure that variables bound by deep binders cannot be free at the
+To make sure that atoms bound by deep binders cannot be free at the
 same time, we cannot have more than one binding function for a deep binder.
 Consequently we exclude specifications such as
 \begin{center}
 \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
 \end{tabular}
 \end{center}
 \noindent
 Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"}  pick
-out different atoms to become bound, respectively be free, in @{text "p"}.
+out different atoms to become bound, respectively be free, in @{text "p"}
+(since the Ott-tool does not derive a reasoning for $\alpha$-equated terms, it can permit
+such specifications).
 We also need to restrict the form of the binding functions in order
 to ensure the @{text "bn"}-functions can be defined for $\alpha$-equated
 terms. The main restriction is that we cannot return an atom in a binding function that is also
 bound in the corresponding term-constructor. That means in \eqref{letpat}
 (as in case @{text PNil}), a singleton set or singleton list containing an
 atom (case @{text PVar}), or unions of atom sets or appended atom lists
 (case @{text PTup}). This restriction will simplify some automatic definitions and proofs
 later on.
-In order to simplify our definitions of free variables and $\alpha$-equivalence,
+In order to simplify our definitions of free atoms and $\alpha$-equivalence,
 we shall assume specifications
 of term-calculi are implicitly \emph{completed}. By this we mean that
 for every argument of a term-constructor that is \emph{not}
 already part of a binding clause given by the user, we add implicitly a special \emph{empty} binding
 clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case
 \noindent
 The point of completion is that we can make definitions over the binding
 clauses and be sure to have captured all arguments of a term constructor.
 *}
-section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *}
+section {* Alpha-Equivalence and Free Atoms\label{sec:alpha} *}
 text {*
 Having dealt with all syntax matters, the problem now is how we can turn
 specifications into actual type definitions in Isabelle/HOL and then
 establish a reasoning infrastructure for them. As
 Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, just
 re-arranging the arguments of
 term-constructors so that binders and their bodies are next to each other will
-result in inadequate representations in cases like @{text "Let x\<^isub>1=t\<^isub>1\<dots>x\<^isub>n=t\<^isub>n in s"}.
+result in inadequate representations in cases like @{text "Let x\<^isub>1 = t\<^isub>1\<dots>x\<^isub>n = t\<^isub>n in s"}.
 Therefore we will first
 extract ``raw'' datatype definitions from the specification and then define
 explicitly an $\alpha$-equivalence relation over them. We subsequently
 quotient the datatypes according to our $\alpha$-equivalence.
 @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor on the ``raw'' type @{text "ty"}.
 The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are
 non-empty and the types in the constructors only occur in positive
 position (see \cite{Berghofer99} for an indepth description of the datatype package
-in Isabelle/HOL). We then define the user-specified binding
+in Isabelle/HOL). We then define each of the user-specified binding
-functions @{term "bn"} by recursion over the corresponding
+function @{term "bn\<^isub>i"} by recursion over the corresponding
 raw datatype. We can also easily define permutation operations by
 recursion so that for each term constructor @{text "C"} we have that
 %
 \begin{equation}\label{ceqvt}
 @{text "p \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (p \<bullet> z\<^isub>1) \<dots> (p \<bullet> z\<^isub>n)"}
 \end{equation}
 The first non-trivial step we have to perform is the generation of
-free-variable functions from the specifications. For the
+free-atom functions from the specifications. For the
-\emph{raw} types @{text "ty"}$_{1..n}$ we define the free-variable functions
+\emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions
 %
 \begin{equation}\label{fvars}
-@{text "fv_ty\<^isub>1, \<dots>, fv_ty\<^isub>n"}
+@{text "fa_ty\<^isub>1, \<dots>, fa_ty\<^isub>n"}
 \end{equation}
 \noindent
 by mutual recursion.
-We define these functions together with auxiliary free-variable functions for
+We define these functions together with auxiliary free-atom functions for
 the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$
 we define
 %
 \begin{center}
-@{text "fv_bn\<^isub>1, \<dots>, fv_bn\<^isub>m"}
+@{text "fa_bn\<^isub>1, \<dots>, fa_bn\<^isub>m"}
 \end{center}
 \noindent
 The reason for this setup is that in a deep binder not all atoms have to be
 bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function
 that calculates those unbound atoms in a deep binder.
-While the idea behind these free-variable functions is clear (they just
+While the idea behind these free-atom functions is clear (they just
 collect all atoms that are not bound), because of our rather complicated
 binding mechanisms their definitions are somewhat involved.  Given
 a term-constructor @{text "C"} of type @{text ty} and some associated
 binding clauses @{text "bc\<^isub>1\<dots>bc\<^isub>k"}, the result of @{text
-"fv_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be the union @{text
+"fa_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be the union @{text
-"fv(bc\<^isub>1) \<union> \<dots> \<union> fv(bc\<^isub>k)"} where we define below what @{text "fv"} of a binding
+"fa(bc\<^isub>1) \<union> \<dots> \<union> fa(bc\<^isub>k)"} where we define below what @{text "fa"} for a binding
-clause means. We only show the mode \isacommand{bind\_set} (the other modes are similar).
+clause means. We only show the details for the mode \isacommand{bind\_set} (the other modes are similar).
 Suppose the binding clause @{text bc\<^isub>i} is of the form
 %
 \begin{equation}
 \mbox{\isacommand{bind\_set} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
 \end{equation}
 binding atoms in the binders and @{text "B'"} for the free atoms in
 non-recursive deep binders,
 then the free atoms of the binding clause @{text bc\<^isub>i} are given by
 %
 \begin{center}
-@{text "fv(bc\<^isub>i) \<equiv> (D - B) \<union> B'"}
+@{text "fa(bc\<^isub>i) \<equiv> (D - B) \<union> B'"}
 \end{center}
 \noindent
-The set @{text D} is formally defined as
+whereby the set @{text D} is formally defined as
 %
 \begin{center}
-@{text "D \<equiv> fv_ty\<^isub>1 d\<^isub>1 \<union> ... \<union> fv_ty\<^isub>q d\<^isub>q"}
+@{text "D \<equiv> fa_ty\<^isub>1 d\<^isub>1 \<union> ... \<union> fa_ty\<^isub>q d\<^isub>q"}
 \end{center}
 \noindent
-whereby the functions @{text "fv_ty\<^isub>i"} are the ones we are defining by recursion
+The functions @{text "fa_ty\<^isub>i"} are the ones we are defining by recursion
-(see \eqref{fvars}) provided the @{text "d\<^isub>i"} refers to one of the raw types
+(see \eqref{fvars}) in case the @{text "d\<^isub>i"} refers to one of the raw types
-@{text "ty"}$_{1..n}$ from the specification; otherwise we set @{text "fv_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
+@{text "ty"}$_{1..n}$ from the specification; otherwise we set @{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
 In order to define the set @{text B} we use the following auxiliary @{text "bn"}-functions
 for atom types to which shallow binders have to refer
 %
 \begin{center}
 \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
 @{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> ... \<union> bn_ty\<^isub>p b\<^isub>p"}
 \end{center}
 \noindent
 The set @{text "B'"} collects all free atoms in non-recursive deep
-binders. Lets assume these binders in @{text "bc\<^isub>i"} are
+binders. Let us assume these binders in @{text "bc\<^isub>i"} are
 %
 \begin{center}
 @{text "bn\<^isub>1 a\<^isub>1, \<dots>, bn\<^isub>r a\<^isub>r"}
 \end{center}
 \noindent
 with none of the @{text "a"}$_{1..r}$ being among the bodies @{text
 "d"}$_{1..q}$. The set @{text "B'"} is defined as
 %
 \begin{center}
-@{text "B' \<equiv> fv_bn\<^isub>1 a\<^isub>1 \<union> ... \<union> fv_bn\<^isub>r a\<^isub>r"}
+@{text "B' \<equiv> fa_bn\<^isub>1 a\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r a\<^isub>r"}
 \end{center}
 \noindent
-This completes the definition of the free-variable functions.
+This completes the definition of the free-atom functions.
 Note that for non-recursive deep binders, we have to add all atoms that are left
-unbound by the binding function @{text "bn"}. This is the purpose of the functions
+unbound by the binding function @{text "bn"} (the set @{text "B'"}). We use for this
-@{text "fv_bn"}, also defined by recursion. Assume the user specified
+the functions @{text "fa_bn"}, also defined by recursion. Assume the user specified
 a @{text bn}-clause of the form
 %
 \begin{center}
-@{text "bn (C z\<^isub>1 \<dots> z\<^isub>n) = rhs"}
+@{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
 \end{center}
 \noindent
-where the @{text "z"}$_{1..n}$ are of types @{text "ty"}$_{1..n}$. For each of
+where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$. For each of
 the arguments we calculate the free atoms as follows:
 %
 \begin{center}
 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-$\bullet$ & @{term "fv_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"}
+$\bullet$ & @{term "fa_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"}
-(nothing gets bound in @{text "z\<^isub>i"}),\\
+(that means nothing is bound in @{text "z\<^isub>i"}),\\
-$\bullet$ & @{term "fv_bn\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} occurs in  @{text "rhs"}
+$\bullet$ & @{term "fa_bn\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} occurs in  @{text "rhs"}
 with the recursive call @{text "bn\<^isub>i z\<^isub>i"}, and\\
 $\bullet$ & @{term "{}"} provided @{text "z\<^isub>i"} occurs in  @{text "rhs"},
-but without a recursive call
+but without a recursive call.
 \end{tabular}
 \end{center}
 \noindent
-For defining @{text "fv_bn (C z\<^isub>1 \<dots> z\<^isub>n)"} we just union up all these values.
+For defining @{text "fa_bn (C z\<^isub>1 \<dots> z\<^isub>n)"} we just union up all these values.
 To see how these definitions work in practice, let us reconsider the term-constructors
 @{text "Let"} and @{text "Let_rec"}, as well as @{text "ANil"} and @{text "ACons"}
 from the example shown in \eqref{letrecs}.
-For them we define three free-variable functions, namely
+For them we define three free-atom functions, namely
-@{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"} as follows:
+@{text "fa\<^bsub>trm\<^esub>"}, @{text "fa\<^bsub>assn\<^esub>"} and @{text "fa\<^bsub>bn\<^esub>"} as follows:
 %
 \begin{center}
 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
-@{text "fv\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fv\<^bsub>trm\<^esub> t - set (bn as)) \<union> fv\<^bsub>bn\<^esub> as"}\\
+@{text "fa\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t - set (bn as)) \<union> fa\<^bsub>bn\<^esub> as"}\\
-@{text "fv\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fv\<^bsub>assn\<^esub> as \<union> fv\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm]
+@{text "fa\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fa\<^bsub>assn\<^esub> as \<union> fa\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm]
-@{text "fv\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
+@{text "fa\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
-@{text "fv\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(supp a) \<union> (fv\<^bsub>trm\<^esub> t) \<union> (fv\<^bsub>assn\<^esub> as)"}\\[1mm]
+@{text "fa\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(supp a) \<union> (fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>assn\<^esub> as)"}\\[1mm]
-@{text "fv\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
+@{text "fa\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
-@{text "fv\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fv\<^bsub>trm\<^esub> t) \<union> (fv\<^bsub>bn\<^esub> as)"}
+@{text "fa\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>bn\<^esub> as)"}
 \end{tabular}
 \end{center}
 \noindent
-To see the ``pattern'', recall that @{text ANil} and @{text "ACons"} have no
+To see the pattern, recall that @{text ANil} and @{text "ACons"} have no
-binding clause in the specification. The corresponding free-variable
+binding clause in the specification. The corresponding free-atom
-function @{text "fv\<^bsub>assn\<^esub>"} therefore returns all atoms
+function @{text "fa\<^bsub>assn\<^esub>"} therefore returns all atoms
 occurring in an assignment. The binding only takes place in @{text Let} and
 @{text "Let_rec"}. In the @{text "Let"}-clause, the binding clause specifies
 that all atoms given by @{text "set (bn as)"} have to be bound in @{text
 t}. Therefore we have to subtract @{text "set (bn as)"} from @{text
-"fv\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are
+"fa\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are
 free in @{text "as"}.  In contrast, in @{text "Let_rec"} we have a recursive
 binder where we want to also bind all occurrences of the atoms in @{text
 "set (bn as)"} also inside @{text "as"}. Therefore we have to subtract
-@{text "set (bn as)"} from the union @{text "fv\<^bsub>trm\<^esub> t"} and @{text "fv\<^bsub>assn\<^esub> as"}.
+@{text "set (bn as)"} from the union @{text "fa\<^bsub>trm\<^esub> t"} and @{text "fa\<^bsub>assn\<^esub> as"}.
 An interesting point in this
 example is that a ``naked'' assignment does not bind any
 atoms. Only in the context of a @{text Let} or @{text "Let_rec"} will
 some atoms from an assignment become bound.  This is a phenomenon that has also been pointed
 not be able to lift the @{text "bn"}-function if it was defined over assignments
 where some atoms are bound. In that case @{text "bn"} would \emph{not} respect
 $\alpha$-equivalence.
 Next we define $\alpha$-equivalence relations for the raw types @{text
-"ty"}$_{1..n}$. We call them
+"ty"}$_{1..n}$. We write them
 %
 \begin{center}
 @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}.
 \end{center}
 \noindent
-Like with the free-variable functions, we also need to
+Like with the free-atom functions, we also need to
 define auxiliary $\alpha$-equivalence relations
 %
 \begin{center}
 @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}
 \end{center}
 \noindent
 for the binding functions @{text "bn"}$_{1..m}$,
 To simplify our definitions we will use the following abbreviations for
-equivalence relations and free-variable functions acting on pairs
+equivalence relations and free-atom functions acting on pairs
 %
 \begin{center}
 \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
 @{text "(x\<^isub>1, y\<^isub>1) (R\<^isub>1 \<otimes> R\<^isub>2) (x\<^isub>2, y\<^isub>2)"} & @{text "\<equiv>"} & @{text "x\<^isub>1 R\<^isub>1 y\<^isub>1 \<and> x\<^isub>2 R\<^isub>2 y\<^isub>2"}\\
-@{text "(fv\<^isub>1 \<oplus> fv\<^isub>2) (x, y)"} & @{text "\<equiv>"} & @{text "fv\<^isub>1 x \<union> fv\<^isub>2 y"}\\
+@{text "(fa\<^isub>1 \<oplus> fa\<^isub>2) (x, y)"} & @{text "\<equiv>"} & @{text "fa\<^isub>1 x \<union> fa\<^isub>2 y"}\\
 \end{tabular}
 \end{center}
 The relations for $\alpha$-equivalence are inductively defined
 analyse the binding clauses and produce a corresponding premise.
 *}
 (*<*)
 consts alpha_ty ::'a
 consts alpha_trm ::'a
-consts fv_trm :: 'a
+consts fa_trm :: 'a
 consts alpha_trm2 ::'a
-consts fv_trm2 :: 'a
+consts fa_trm2 :: 'a
 notation (latex output)
 alpha_ty ("\<approx>ty") and
 alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and
-fv_trm ("fv\<^bsub>trm\<^esub>") and
+fa_trm ("fa\<^bsub>trm\<^esub>") and
 alpha_trm2 ("\<approx>\<^bsub>assn\<^esub> \<otimes> \<approx>\<^bsub>trm\<^esub>") and
-fv_trm2 ("fv\<^bsub>assn\<^esub> \<oplus> fv\<^bsub>trm\<^esub>")
+fa_trm2 ("fa\<^bsub>assn\<^esub> \<oplus> fa\<^bsub>trm\<^esub>")
 (*>*)
 text {*
 *TBD below *
 \begin{equation}\label{alpha}
 $\bullet$ & @{term "x\<^isub>i = y\<^isub>i"} provided @{text "x\<^isub>i"} and @{text "y\<^isub>i"} are
 non-recursive arguments\smallskip\\
 \multicolumn{2}{@ {}l}{Shallow binders of the form
 \isacommand{bind\_set}~@{text "x\<^isub>1\<dots>x\<^isub>n"}~\isacommand{in}~@{text "x'\<^isub>1\<dots>x'\<^isub>m"}:}\\
 $\bullet$ & Assume the bodies @{text "x'\<^isub>1\<dots>x'\<^isub>m"} are of type @{text "ty\<^isub>1\<dots>ty\<^isub>m"},
-@{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is
+@{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fa} is
-@{text "fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}, then
+@{text "fa_ty\<^isub>1 \<oplus> ... \<oplus> fa_ty\<^isub>m"}, then
 \begin{center}
-@{term "\<exists>p. (x\<^isub>1 \<union> \<xi> \<union> x\<^isub>n, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fv p (y\<^isub>1 \<union> \<xi> \<union> y\<^isub>n, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}
+@{term "\<exists>p. (x\<^isub>1 \<union> \<xi> \<union> x\<^isub>n, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fa p (y\<^isub>1 \<union> \<xi> \<union> y\<^isub>n, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}
 \end{center}\\
 \multicolumn{2}{@ {}l}{Deep binders of the form
 \isacommand{bind\_set}~@{text "bn x"}~\isacommand{in}~@{text "x'\<^isub>1\<dots>x'\<^isub>m"}:}\\
 $\bullet$ & Assume the bodies @{text "x'\<^isub>1\<dots>x'\<^isub>m"} are of type @{text "ty\<^isub>1\<dots>ty\<^isub>m"},
-@{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is
+@{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fa} is
-@{text "fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}, then for recursive deep binders
+@{text "fa_ty\<^isub>1 \<oplus> ... \<oplus> fa_ty\<^isub>m"}, then for recursive deep binders
 \begin{center}
-@{term "\<exists>p. (bn x, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fv p (bn y, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}
+@{term "\<exists>p. (bn x, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fa p (bn y, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}
 \end{center}\\
 $\bullet$ & for non-recursive binders we generate in addition @{text "x \<approx>bn y"}\\
 \end{tabular}}
 \end{equation}
 $\approx_{\textit{bn}}$, with the clauses as follows:
 \begin{center}
 \begin{tabular}{@ {}c @ {}}
 \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
-{@{text "as \<approx>\<^bsub>bn\<^esub> as'"} & @{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fv_trm p (bn as', t')"}}\smallskip\\
+{@{text "as \<approx>\<^bsub>bn\<^esub> as'"} & @{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"}}\smallskip\\
 \infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
-{@{term "\<exists>p. (bn as, (as, t)) \<approx>lst alpha_trm2 fv_trm2 p (bn as', (as', t'))"}}
+{@{term "\<exists>p. (bn as, (as, t)) \<approx>lst alpha_trm2 fa_trm2 p (bn as', (as', t'))"}}
 \end{tabular}
 \end{center}
 \begin{center}
 \begin{tabular}{@ {}c @ {}}
 \noindent
 We can feed this lemma into our quotient package and obtain new types @{text
 "ty\<AL>\<^bsub>1..n\<^esub>"} representing $\alpha$-equated terms of types @{text "ty\<^bsub>1..n\<^esub>"}. We also obtain
 definitions for the term-constructors @{text
 "C"}$^\alpha_{1..m}$ from the raw term-constructors @{text
-"C"}$_{1..m}$, and similar definitions for the free-variable functions @{text
+"C"}$_{1..m}$, and similar definitions for the free-atom functions @{text
-"fv_ty"}$^\alpha_{1..n}$ and the binding functions @{text
+"fa_ty"}$^\alpha_{1..n}$ and the binding functions @{text
 "bn"}$^\alpha_{1..k}$. However, these definitions are not really useful to the
 user, since they are given in terms of the isomorphisms we obtained by
 creating new types in Isabelle/HOL (recall the picture shown in the
 Introduction).
 @{text "p \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n) = C\<^sup>\<alpha> (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}
 \end{equation}
 \noindent
 for our infrastructure. In a similar fashion we can lift the equations
-characterising the free-variable functions @{text "fn_ty\<AL>\<^isub>j"} and @{text "fv_bn\<AL>\<^isub>k"}, and the
+characterising the free-atom functions @{text "fn_ty\<AL>\<^isub>j"} and @{text "fa_bn\<AL>\<^isub>k"}, and the
 binding functions @{text "bn\<AL>\<^isub>k"}. The necessary respectfulness lemmas for these
 lifting are the properties:
 %
 \begin{equation}\label{fnresp}
 \mbox{%
 \begin{tabular}{l}
-@{text "x \<approx>ty\<^isub>j y"} implies @{text "fv_ty\<^isub>j x = fv_ty\<^isub>j y"}\\
+@{text "x \<approx>ty\<^isub>j y"} implies @{text "fa_ty\<^isub>j x = fa_ty\<^isub>j y"}\\
-@{text "x \<approx>ty\<^isub>k y"} implies @{text "fv_bn\<^isub>k x = fv_bn\<^isub>k y"}\\
+@{text "x \<approx>ty\<^isub>k y"} implies @{text "fa_bn\<^isub>k x = fa_bn\<^isub>k y"}\\
 @{text "x \<approx>ty\<^isub>k y"} implies @{text "bn\<^isub>k x = bn\<^isub>k y"}
 \end{tabular}}
 \end{equation}
 \noindent
 which can be established by induction on @{text "\<approx>ty"}. Whereas the first
-property is always true by the way we defined the free-variable
+property is always true by the way we defined the free-atom
 functions for types, the second and third do \emph{not} hold in general. There is, in principle,
 the possibility that the user defines @{text "bn\<^isub>k"} so that it returns an already bound
-variable. Then the third property is just not true. However, our
+atom. Then the third property is just not true. However, our
 restrictions imposed on the binding functions
 exclude this possibility.
 Having the facts \eqref{fnresp} at our disposal, we can lift the
 definitions that characterise when two terms of the form
 We call these conditions as \emph{quasi-injectivity}. Except for one function, which
 we have to lift in the next section, we completed
 the lifting part of establishing the reasoning infrastructure.
 By working now completely on the $\alpha$-equated level, we can first show that
-the free-variable functions and binding functions
+the free-atom functions and binding functions
 are equivariant, namely
 \begin{center}
 \begin{tabular}{rcl}
-@{text "p \<bullet> (fv_ty\<^sup>\<alpha> x)"} & $=$ & @{text "fv_ty\<^sup>\<alpha> (p \<bullet> x)"}\\
+@{text "p \<bullet> (fa_ty\<^sup>\<alpha> x)"} & $=$ & @{text "fa_ty\<^sup>\<alpha> (p \<bullet> x)"}\\
-@{text "p \<bullet> (fv_bn\<^sup>\<alpha> x)"} & $=$ & @{text "fv_bn\<^sup>\<alpha> (p \<bullet> x)"}\\
+@{text "p \<bullet> (fa_bn\<^sup>\<alpha> x)"} & $=$ & @{text "fa_bn\<^sup>\<alpha> (p \<bullet> x)"}\\
 @{text "p \<bullet> (bn\<^sup>\<alpha> x)"}    & $=$ & @{text "bn\<^sup>\<alpha> (p \<bullet> x)"}
 \end{tabular}
 \end{center}
 \noindent
 \end{center}
 \noindent
 by a structural induction over @{text "x\<^isub>1, \<dots>, x\<^isub>n"} (whereby @{text "x\<^isub>i"} ranges over the types
 @{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"}). Lastly, we can show that the support of elements in
-@{text "ty\<AL>\<^bsub>1..n\<^esub>"} coincides with @{text "fv_ty\<AL>\<^bsub>1..n\<^esub>"}.
+@{text "ty\<AL>\<^bsub>1..n\<^esub>"} coincides with @{text "fa_ty\<AL>\<^bsub>1..n\<^esub>"}.
 \begin{lemma}
 For every @{text "x\<^isub>i"} of type @{text "ty\<AL>\<^bsub>1..n\<^esub>"}, we have that
-@{text "supp x\<^isub>i = fv_ty\<AL>\<^isub>i x\<^isub>i"} holds.
+@{text "supp x\<^isub>i = fa_ty\<AL>\<^isub>i x\<^isub>i"} holds.
 \end{lemma}
 \begin{proof}
 The proof proceeds by structural induction over the @{text "x\<^isub>i"}. In each case
 we unfold the definition of @{text "supp"}, move the swapping inside the
 $\alpha$-equated terms. We can then prove the following two facts
 \begin{lemma}\label{permutebn}
 Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}
 {\it i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<^bsub>bn\<^esub>\<^sup>\<alpha> x)"} and {\it ii)}
-@{text "fv_bn\<^isup>\<alpha> x = fv_bn\<^isup>\<alpha> (p \<bullet>\<^bsub>bn\<^esub>\<^sup>\<alpha> x)"}.
+@{text "fa_bn\<^isup>\<alpha> x = fa_bn\<^isup>\<alpha> (p \<bullet>\<^bsub>bn\<^esub>\<^sup>\<alpha> x)"}.
 \end{lemma}
 \begin{proof}
 By induction on @{text x}. The equations follow by simple unfolding
 of the definitions.
 \end{proof}
 \noindent
 The first property states that a permutation applied to a binding function is
 equivalent to first permuting the binders and then calculating the bound
-variables. The second amounts to the fact that permuting the binders has no
+atoms. The second amounts to the fact that permuting the binders has no
-effect on the free-variable function. The main point of this permutation
+effect on the free-atom function. The main point of this permutation
 function, however, is that if we have a permutation that is fresh
 for the support of an object @{text x}, then we can use this permutation
 to rename the binders in @{text x}, without ``changing'' @{text x}. In case of the
 @{text "Let"} term-constructor from the example shown
 \eqref{letpat} this means for a permutation @{text "r"}:
 text {*
 We can also see that
 %
 \begin{equation}\label{bnprop}
-@{text "fv_ty x  =  bn x \<union> fv_bn x"}.
+@{text "fa_ty x  =  bn x \<union> fa_bn x"}.
 \end{equation}
 \noindent
 holds for any @{text "bn"}-function defined for the type @{text "ty"}.

changeset 2347	9807d30c0e54
parent 2346	4c5881455923
child 2348	09b476c20fe1