nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:7b3dd407f6b3
+:51bc795b81fd
 \begin{center}
 @{text "t ::= x | t t | \<lambda>x. t"}
 \end{center}
 \noindent
-where free and bound variables have names.  For such terms Nominal Isabelle
+where free and bound variables have names.  For such alpha-equated terms,  Nominal Isabelle
 derives automatically a reasoning infrastructure that has been used
 successfully in formalisations of an equivalence checking algorithm for LF
 \cite{UrbanCheneyBerghofer08}, Typed
 Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
 \cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result
 for cut-elimination in classical logic \cite{UrbanZhu08}. It has also been
 used by Pollack for formalisations in the locally-nameless approach to
 binding \cite{SatoPollack10}.
 However, Nominal Isabelle has fared less well in a formalisation of
-the algorithm W \cite{UrbanNipkow09}, where types and type-schemes
+the algorithm W \cite{UrbanNipkow09}, where types and type-schemes,
-are of the form
+respectively, are of the form
 %
 \begin{equation}\label{tysch}
 \begin{array}{l}
 @{text "T ::= x | T \<rightarrow> T"}\hspace{5mm}
 @{text "S ::= \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. T"}
 \noindent
 where the notation @{text "[_]._"} indicates that the @{text "x\<^isub>i"}
 become bound in @{text s}. In this representation the term
 \mbox{@{text "\<LET> [x].s [t\<^isub>1, t\<^isub>2]"}} would be a perfectly legal
-instance. To exclude such terms, additional predicates about well-formed
+instance, but the lengths of two lists do not agree. To exclude such terms,
+additional predicates about well-formed
 terms are needed in order to ensure that the two lists are of equal
 length. This can result into very messy reasoning (see for
 example~\cite{BengtsonParow09}). To avoid this, we will allow type
 specifications for $\mathtt{let}$s as follows
 %
 \end{center}
 \noindent
 where @{text assn} is an auxiliary type representing a list of assignments
 and @{text bn} an auxiliary function identifying the variables to be bound
-by the @{text "\<LET>"}. This function is defined by recursion over @{text
+by the @{text "\<LET>"}. This function can be defined by recursion over @{text
 assn} as follows
 \begin{center}
 @{text "bn(\<ANIL>) ="} @{term "{}"} \hspace{5mm}
 @{text "bn(\<ACONS> x t as) = {x} \<union> bn(as)"}
 \noindent
 are not just alpha-equal, but actually \emph{equal}. As a result, we can
 only support specifications that make sense on the level of alpha-equated
 terms (offending specifications, which for example bind a variable according
 to a variable bound somewhere else, are not excluded by Ott, but we have
-to).  Our insistence on reasoning with alpha-equated terms comes from the
+to).
+Our insistence on reasoning with alpha-equated terms comes from the
 wealth of experience we gained with the older version of Nominal Isabelle:
 for non-trivial properties, reasoning about alpha-equated terms is much
 easier than reasoning with raw terms. The fundamental reason for this is
 that the HOL-logic underlying Nominal Isabelle allows us to replace
 ``equals-by-equals''. In contrast, replacing
 @{text "fv(t\<^isub>1 t\<^isub>2) = fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\\[1mm]
 @{text "fv(\<lambda>x.t) = fv(t) - {x}"}
 \end{center}
 \noindent
-then with not too great effort we obtain a function @{text "fv\<^sup>\<alpha>"}
+then with the help of te quotient package we obtain a function @{text "fv\<^sup>\<alpha>"}
 operating on quotients, or alpha-equivalence classes of lambda-terms. This
 lifted function is characterised by the equations
 \begin{center}
 @{text "fv\<^sup>\<alpha>(x) = {x}"}\hspace{10mm}
 \noindent
 (Note that this means also the term-constructors for variables, applications
 and lambda are lifted to the quotient level.)  This construction, of course,
 only works if alpha-equivalence is indeed an equivalence relation, and the lifted
-definitions and theorems are respectful w.r.t.~alpha-equivalence.  Accordingly, we
+definitions and theorems are respectful w.r.t.~alpha-equivalence.  For exmple, we
 will not be able to lift a bound-variable function, which can be defined for
-raw terms, to alpha-equated terms
+raw terms. The reason is that this function does not respect alpha-equivalence.
-(since it does not respect alpha-equivalence). To sum up, every lifting of
+To sum up, every lifting of
 theorems to the quotient level needs proofs of some respectfulness
-properties. In the paper we show that we are able to automate these
+properties (see \cite{Homeier05}). In the paper we show that we are able to
+automate these
 proofs and therefore can establish a reasoning infrastructure for
 alpha-equated terms.
 The examples we have in mind where our reasoning infrastructure will be
-immeasurably helpful is what is often referred to as Core-Haskell (see
+helpful is the term language of System @{text "F\<^isub>C"}, also known as
-Figure~\ref{corehas}). There terms include patterns which include a list of
+Core-Haskell (see Figure~\ref{corehas}). This term language has patterns
+which include lists of
 type- and term- variables (the arguments of constructors) all of which are
 bound in case expressions. One difficulty is that each of these variables
 come 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
 conditions for alpha-equated terms. We are also able to derive, at the moment
 only manually, strong induction principles that
 have the variable convention already built in.
 \begin{figure}
+\begin{boxedminipage}{\linewidth}
-\caption{Core Haskell.\label{corehas}}
+\begin{center}
+\begin{tabular}{l}
+Type Kinds\\
+@{text "\<kappa> ::= \<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\\
+Coercion Kinds\\
+@{text "\<iota> ::= \<sigma>\<^isub>1 \<sim> \<sigma>\<^isub>2"}\\
+Types\\
+@{text "\<sigma> ::= a | T | \<sigma>\<^isub>1 \<sigma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<sigma>"}}$@{text "\<^sup>n"}\\
+@{text "| \<forall>a:\<kappa>. \<sigma> "}\\
+??? Type equality\\
+Coercion Types\\
+@{text "\<gamma> ::= a | C | S\<^isub>n"}$\;\overline{@{text "\<gamma>"}}$@{text "\<^sup>n"}\\
+@{text "| \<forall>a:\<iota>. \<gamma>"}\\
+??? Coercion Type equality\\
+@{text "| sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2 | left \<gamma> | right \<gamma> | \<gamma>\<^isub>1 \<sim> \<gamma>\<^isub>2 "}\\
+@{text "| rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\\
+Terms\\
+@{text "e ::= x | K | \<Lambda>a:\<kappa>. e | \<Lambda>a:\<iota>. e | e \<sigma> | e \<gamma>"}\\
+@{text "| \<lambda>x:\<sigma>.e | e\<^isub>1 e\<^isub>2"}\\
+@{text "| \<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2"}\\
+@{text "| \<CASE> e\<^isub>1 \<OF>"}$\;\overline{@{text "p \<rightarrow> e\<^isub>2"}}$\\
+@{text "| e \<triangleright> \<gamma>"}\\
+Patterns\\
+@{text "p ::= K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "x:\<sigma>"}}$\\
+Constants\\
+@{text C} coercion constant\\
+@{text T} value type constructor\\
+@{text "S\<^isub>n"} n-ary type function\\
+@{text K} data constructor\\
+Variables\\
+@{text a} type variable\\
+@{text x} term variable\\
+\end{tabular}
+\end{center}
+\end{boxedminipage}
+\caption{The term-language of System @{text "F\<^isub>C"}, also often referred to as Core-Haskell,
+according to \cite{CoreHaskell}. We only made an issential modification by
+separating the grammars for type kinds and coercion types.\label{corehas}}
 \end{figure}
 *}
 section {* A Short Review of the Nominal Logic Work *}
 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 @{text "fv"} 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
-ii)} it leaves the free variables of @{text x} and @{text y} unchanged, but
+ii)} @{text p} leaves the free variables 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 {\it iv)} that
 @{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}
-\multicolumn{2}{l}{@{term "(as, x) \<approx>gen R fv p (bs, y)"} @{text "\<equiv>"}\hspace{30mm}}\\
+\multicolumn{2}{l}{@{term "(as, x) \<approx>gen R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}\hspace{30mm}}\\[1mm]
 & @{term "fv(x) - as = fv(y) - bs"}\\
 @{text "\<and>"} & @{term "(fv(x) - as) \<sharp>* p"}\\
 @{text "\<and>"} & @{text "(p \<bullet> x) R y"}\\
 @{text "\<and>"} & @{term "(p \<bullet> as) = bs"}\\
 \end{array}
 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}
-\multicolumn{2}{l}{@{term "(as, x) \<approx>lst R fv p (bs, y)"} @{text "\<equiv>"}\hspace{30mm}}\\[1mm]
+\multicolumn{2}{l}{@{term "(as, x) \<approx>lst R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}\hspace{30mm}}\\[1mm]
 & @{term "fv(x) - (set as) = fv(y) - (set bs)"}\\
 \wedge     & @{term "(fv(x) - set as) \<sharp>* p"}\\
 \wedge     & @{text "(p \<bullet> x) R y"}\\
 \wedge     & @{term "(p \<bullet> as) = bs"}\\
 \end{array}
 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}
-\multicolumn{2}{l}{@{term "(as, x) \<approx>res R fv p (bs, y)"} @{text "\<equiv>"}\hspace{30mm}}\\[1mm]
+\multicolumn{2}{l}{@{term "(as, x) \<approx>res R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}\hspace{30mm}}\\[1mm]
 & @{term "fv(x) - as = fv(y) - bs"}\\
 \wedge     & @{term "(fv(x) - as) \<sharp>* p"}\\
 \wedge     & @{text "(p \<bullet> x) R y"}\\
 \end{array}
 \end{equation}
-\begin{exmple}\rm
 It might be useful to consider some examples for how these definitions of alpha-equivalence
 pan out in practise.
 For this consider the case of abstracting a set of variables over types (as in type-schemes).
 We set @{text R} to be the equality and for @{text "fv(T)"} we define
 @{text "fv(x) = {x}"}  \hspace{5mm} @{text "fv(T\<^isub>1 \<rightarrow> T\<^isub>2) = fv(T\<^isub>1) \<union> fv(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
+\eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and
-@{text "({y,x}, y \<rightarrow> x)"} are equal according to $\approx_{\textit{set}}$ and
+@{text "({y, x}, y \<rightarrow> x)"} are equal according to $\approx_{\textit{set}}$ and
 $\approx_{\textit{res}}$ by taking @{text p} to be the swapping @{term "(x \<rightleftharpoons>
 y)"}. In case of @{text "x \<noteq> y"}, then @{text "([x, y], x \<rightarrow> y)"}
-$\not\approx_{\textit{list}}$ @{text "([y,x], x \<rightarrow> y)"} since there is no permutation
+$\not\approx_{\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"} since there is no permutation
 that makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and also
 leaves the type \mbox{@{text "x \<rightarrow> y"}} unchanged. Another example is
-@{text "({x}, x)"} $\approx_{\textit{res}}$ @{text "({x,y}, x)"} which holds by
+@{text "({x}, x)"} $\approx_{\textit{res}}$ @{text "({x, y}, x)"} which holds by
 taking @{text p} to be the
 identity permutation.  However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}
-$\not\approx_{\textit{set}}$ @{text "({x,y}, x)"} since there is no permutation
+$\not\approx_{\textit{set}}$ @{text "({x, y}, x)"} since there is no permutation
 that makes the
-sets @{text "{x}"} and @{text "{x,y}"} equal (similarly for $\approx_{\textit{list}}$).
+sets @{text "{x}"} and @{text "{x, y}"} equal (similarly for $\approx_{\textit{list}}$).
-\end{exmple}
+It can also relatively easily be shown that all tree notions of alpha-equivalence
+coincide, if we only abstract a single atom.
 % looks too ugly
 %\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
 %\begin{proof}
 %All properties are by unfolding the definitions and simple calculations.
 %\end{proof}
-In the rest of this section we are going to introduce a type- and term-constructor
+In the rest of this section we are going to introduce a type- and term-constructors
-for abstractions. For this we define (similarly for $\approx_{\textit{abs\_list}}$
+for abstraction. For this we define
-and $\approx_{\textit{abs\_res}}$)
 %
 \begin{equation}
 @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_gen (as, x) equal supp p (bs, x)"}
 \end{equation}
 \noindent
-We can show that these relations are equivalence relations and equivariant
+(similarly for $\approx_{\textit{abs\_list}}$
-(we only show the $\approx_{\textit{abs\_set}}$-case).
+and $\approx_{\textit{abs\_res}}$). We can show that these relations are equivalence
+relations and equivariant.
-\begin{lemma}\label{alphaeq}
-$\approx_{\textit{abs\_set}}$ is an equivalence
+\begin{lemma}\label{alphaeq} The relations
+$\approx_{\textit{abs\_set}}$,
+$\approx_{\textit{abs\_list}}$
+and $\approx_{\textit{abs\_res}}$
+are equivalence
 relations, and if @{term "abs_set (as, x) (bs, y)"} then also
-@{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"}.
+@{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} (similarly for
+the other two relations).
 \end{lemma}
 \begin{proof}
 Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have
 a permutation @{text p} and for the proof obligation take @{term "-p"}. In case
 of transitivity, we have two permutations @{text p} and @{text q}, and for the
 proof obligation use @{text "q + p"}. All conditions are then by simple
 calculations.
 \end{proof}
 \noindent
-We are also define the following two auxiliary functions taking a pair
+This lemma allows us to use our quotient package and introduce
-as argument.
-%
-\begin{equation}\label{aux}
-\begin{array}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-@{text "aux (as, x)"}      & @{text "\<equiv>"} & @{text "supp x - as"}\\
-@{text "aux_list (bs, x)"} & @{text "\<equiv>"} & @{text "supp x - set bs"}
-\end{array}
-\end{equation}
-\noindent
-The point of these two functions is that they are preserved under
-alpha-equivalence, that means for instance
-%
-\begin{equation}\label{auxpreserved}
-@{term "abs_set (as, x) (bs, y)"} \;\;\text{implies}\;\;
-@{term "aux (as, x) = aux (bs, y)"}
-\end{equation}
-Lemma \ref{alphaeq} allows us to use our quotient package and introduce
 new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}
-representing the alpha-equivalence classes. Elements in these types
+representing alpha-equivalence classes of pairs. The elements in these types
 we will, respectively, write as:
 \begin{center}
 @{term "Abs as x"} \hspace{5mm}
 @{term "Abs_lst as x"} \hspace{5mm}
 @{term "Abs_res as x"}
 \end{center}
 \noindent
-By definition we have
+indicating that a set or list is abstracted in @{text x}. We will call the types
+\emph{abstraction types} and their elements \emph{abstractions}. The important
-\begin{center}
+property we need is a characterisation for the support of abstractions, namely
-@{thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;iff\;
+\begin{thm}[Support of Abstractions]\label{suppabs}
+Assuming @{text x} has finite support, then
+\begin{center}
+\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+@{thm (lhs) supp_abs(1)[no_vars]} & $=$ & @{thm (rhs) supp_abs(1)[no_vars]}\\
+@{thm (lhs) supp_abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_abs(2)[no_vars]}\\
+@{thm (lhs) supp_abs(3)[no_vars]} & $=$ & @{thm (rhs) supp_abs(3)[no_vars]}
+\end{tabular}
+\end{center}
+\end{thm}
+\noindent
+We will only show in the rest of the section the first equation, as the others
+follow similar arguments. By definition of the abstraction type @{text "abs_set"}
+we have
+%
+\begin{equation}\label{abseqiff}
+@{thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\text{if and only if}\;
 @{thm (rhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}
-\end{center}
+\end{equation}
+\noindent
-\noindent
+With this, we can show the following lemma about swapping two atoms (the permutation
-The following lemma (and similar ones for $\approx_{\textit{abs\_list}}$ and
+operation for abstractions is the one lifted for pairs).\footnote{metion this in the nominal
-$\approx_{\textit{abs\_res}}$) will be crucial below:
+logic section}
 \begin{lemma}
 @{thm[mode=IfThen] abs_swap1(1)[no_vars]}
 \end{lemma}
 \begin{proof}
-This lemma is straightforward by observing that the assumptions give us
+By using \eqref{abseqiff}, this lemma is straightforward when observing that
+the assumptions give us
 @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - bs) = (supp x - bs)"} and that @{text supp}
-is equivariant.
+and set difference are equivariant.
 \end{proof}
+\noindent
+This lemma gives us
+%
+\begin{equation}\label{halfone}
+@{thm abs_supports(1)[no_vars]}
+\end{equation}
+\noindent
+which with \ref{} gives us one half of Thm~\ref{suppabs}. The other half is
+a bit more involved. We first define an auxiliary function
+%
+\begin{center}
+@{thm supp_res.simps[THEN eq_reflection, no_vars]}
+\end{center}
 \begin{lemma}
 $supp ([as]set. x) = supp x - as$
 \end{lemma}
+\noindent
+The point of these general lemmas about pairs is that we can define and prove properties
+about them conveninently on the Isabelle level, and in addition can use them in what
+follows next when we have to deal with specific instances of term-specification.
 *}
 section {* Alpha-Equivalence and Free Variables *}
 text {*

changeset 1687	51bc795b81fd
parent 1667	2922b04d9545
child 1690	44a5edac90ad