nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:3668b389edf3
+:3bf0fddb7d44
 "equal \<equiv> (op =)"
 notation (latex output)
 swap ("'(_ _')" [1000, 1000] 1000) and
 fresh ("_ # _" [51, 51] 50) and
-fresh_star ("_ #* _" [51, 51] 50) and
+fresh_star ("_ #\<^sup>* _" [51, 51] 50) and
 supp ("supp _" [78] 73) and
 uminus ("-_" [78] 73) and
 If  ("if _ then _ else _" 10) and
 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
 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
+\cite{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
 \end{center}
 \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
+only works if alpha-equivalence is indeed an equivalence relation, and the
-definitions and theorems are respectful w.r.t.~alpha-equivalence.  For example, we
+lifted definitions and theorems are respectful w.r.t.~alpha-equivalence.
-will not be able to lift a bound-variable function, which can be defined for
+For example, we will not be able to lift a bound-variable function. Although
-raw terms. The reason is that this function does not respect alpha-equivalence.
+this function can be defined for raw terms, it does not respect
-To sum up, every lifting of
+alpha-equivalence and therefore cannot be lifted. To sum up, every lifting
-theorems to the quotient level needs proofs of some respectfulness
+of theorems to the quotient level needs proofs of some respectfulness
 properties (see \cite{Homeier05}). In the paper we show that we are able to
-automate these
+automate these proofs and therefore can establish a reasoning infrastructure
-proofs and therefore can establish a reasoning infrastructure for
+for alpha-equated terms.
-alpha-equated terms.
 The examples we have in mind where our reasoning infrastructure will be
-helpful includes the term language of System @{text "F\<^isub>C"}, also known as
+helpful includes the term language of System @{text "F\<^isub>C"}, also
-Core-Haskell (see Figure~\ref{corehas}). This term language involves patterns
+known as Core-Haskell (see Figure~\ref{corehas}). This term language
-that include lists of
+involves patterns that have lists of type- and term-variables (the
-type- and term- variables (the arguments of constructors) all of which are
+arguments of constructors) all of which are bound in case expressions. One
-bound in case expressions. One difficulty is that each of these variables
+difficulty is that each of these variables come with a kind or type
-come with a kind or type annotation. Representing such binders with single
+annotation. Representing such binders with single binders and reasoning
-binders and reasoning about them in a theorem prover would be a major pain.
+about them in a theorem prover would be a major pain.  \medskip
-\medskip
 \noindent
 {\bf Contributions:}  We provide new definitions for when terms
 involving multiple binders are alpha-equivalent. These definitions are
 inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
 \multicolumn{3}{@ {}l}{Type Kinds}\\
 @{text "\<kappa>"} & @{text "::="} & @{text "\<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\medskip\\
 \multicolumn{3}{@ {}l}{Coercion Kinds}\\
 @{text "\<iota>"} & @{text "::="} & @{text "\<sigma>\<^isub>1 \<sim> \<sigma>\<^isub>2"}\medskip\\
 \multicolumn{3}{@ {}l}{Types}\\
-@{text "\<sigma>"} & @{text "::="} & @{text "a | T | \<sigma>\<^isub>1 \<sigma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<sigma>"}}$@{text "\<^sup>n"}\\
+@{text "\<sigma>"} & @{text "::="} & @{text "a | T | \<sigma>\<^isub>1 \<sigma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<sigma>"}}$@{text "\<^sup>n"}
-& & @{text "| \<forall>a:\<kappa>. \<sigma> "}\\
+@{text "| \<forall>a:\<kappa>. \<sigma> | \<iota> \<Rightarrow> \<sigma>"}\medskip\\
-& & ??? Type equality\medskip\\
 \multicolumn{3}{@ {}l}{Coercion Types}\\
-@{text "\<gamma>"} & @{text "::="} & @{text "a | C | S\<^isub>n"}$\;\overline{@{text "\<gamma>"}}$@{text "\<^sup>n"}\\
+@{text "\<gamma>"} & @{text "::="} & @{text "c | C | \<gamma>\<^isub>1 \<gamma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<gamma>"}}$@{text "\<^sup>n"}
-& & @{text "| \<forall>a:\<iota>. \<gamma>"}\\
+@{text "| \<forall>c:\<iota>. \<gamma> | \<iota> \<Rightarrow> \<gamma> |"}\\
-& & ??? Coercion Type equality\\
+& & @{text "refl \<sigma> | sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2 | \<gamma> @ \<sigma> |"}\\
-& & @{text "| sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2 | left \<gamma> | right \<gamma> | \<gamma>\<^isub>1 \<sim> \<gamma>\<^isub>2 "}\\
+& & @{text "left \<gamma> | right \<gamma> | \<gamma>\<^isub>1 \<sim> \<gamma>\<^isub>2 |"}\\
-& & @{text "| rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\medskip\\
+& & @{text "rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\medskip\\
 \multicolumn{3}{@ {}l}{Terms}\\
-@{text "e"} & @{text "::="} & @{text "x | K | \<Lambda>a:\<kappa>. e | \<Lambda>a:\<iota>. e | e \<sigma> | e \<gamma> |"}\\
+@{text "e"} & @{text "::="} & @{text "x | K | \<Lambda>a:\<kappa>. e | \<Lambda>c:\<iota>. e | e \<sigma> | e \<gamma> |"}\\
-& & @{text "\<lambda>x:\<sigma>.e | e\<^isub>1 e\<^isub>2 | \<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2 |"}\\
+& & @{text "\<lambda>x:\<sigma>. e | e\<^isub>1 e\<^isub>2 | \<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>"}\medskip\\
 \multicolumn{3}{@ {}l}{Patterns}\\
-@{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "a:\<iota>"}}\;\overline{@{text "x:\<sigma>"}}$\medskip\\
+@{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "c:\<iota>"}}\;\overline{@{text "x:\<sigma>"}}$\medskip\\
 \multicolumn{3}{@ {}l}{Constants}\\
-@{text C} & & coercion constant\\
+@{text C} & & coercion constants\\
-@{text T} & & value type constructor\\
+@{text T} & & value type constructors\\
-@{text "S\<^isub>n"} & & n-ary type function\\
+@{text "S\<^isub>n"} & & n-ary type functions\\
-@{text K} & & data constructor\medskip\\
+@{text K} & & data constructors\medskip\\
 \multicolumn{3}{@ {}l}{Variables}\\
-@{text a} & & type variable\\
+@{text a} & & type variables\\
-@{text x} & & term variable\\
+@{text c} & & coercion variables\\
+@{text x} & & term variables\\
 \end{tabular}
 \end{center}
 \end{boxedminipage}
-\caption{The term-language of System @{text "F\<^isub>C"}, also often referred to as Core-Haskell,
+\caption{The term-language of System @{text "F\<^isub>C"}, also often referred to as \emph{Core-Haskell}
-according to \cite{CoreHaskell}. We only made an inessential modification by
+\cite{CoreHaskell}. In this version of Core-Haskell we made a modification by
-separating the grammars for type kinds and coercion types.\label{corehas}}
+separating completely the grammars for type kinds and coercion types.\label{corehas}}
 \end{figure}
 *}
 section {* A Short Review of the Nominal Logic Work *}
 text {*
 At its core, Nominal Isabelle is an adaption of the nominal logic work by
 Pitts \cite{Pitts03}. This adaptation for Isabelle/HOL is described in
-\cite{HuffmanUrban10} (including proofs), which we review here briefly to aid the description
+\cite{HuffmanUrban10} (including proofs). We shall briefly review this work
-of what follows. Two central notions in the nominal logic work are sorted
+to aid the description of what follows.
-atoms and sort-respecting permutations of atoms. The sorts can be used to
-represent different kinds of variables, such as the term- and type-variables in
+Two central notions in the nominal
-Core-Haskell, and it is assumed that there is an infinite supply of atoms
+logic work are sorted atoms and sort-respecting permutations of atoms. The
-for each sort. However, in order to simplify the description, we shall
+sorts can be used to represent different kinds of variables, such as the
-assume in what follows that there is only one sort of atoms.
+term- and type-variables in Core-Haskell, and it is assumed that there is an
+infinite supply of atoms for each sort. However, in order to simplify the
+description, we shall assume in what follows that there is only one sort of
+atoms.
 Permutations are bijective functions from atoms to atoms that are
 the identity everywhere except on a finite number of atoms. There is a
 two-place permutation operation written
 %
 @{text[display,indent=5] "_ \<bullet> _  ::  perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
 \noindent
 in which the generic type @{text "\<beta>"} stands for the type of the object
-on which the permutation
+over which the permutation
 acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},
 the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}},
 and the inverse permutation of @{term p} as @{text "- p"}. The permutation
-operation is defined for products, lists, sets, functions, booleans etc (see \cite{HuffmanUrban10})
+operation is defined by induction over the type-hierarchy, for example as follows
+for products, lists, sets, functions and booleans (see \cite{HuffmanUrban10}):
-\begin{center}
-\begin{tabular}{@ {}cc@ {}}
+\begin{equation}
+\mbox{\begin{tabular}{@ {}cc@ {}}
 \begin{tabular}{@ {}l@ {}}
 @{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm]
 @{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\
 @{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\
 \end{tabular} &
 \begin{tabular}{@ {}l@ {}}
 @{thm permute_set_eq[no_vars, THEN eq_reflection]}\\
-@{text "p \<bullet> (f x) \<equiv> (p \<bullet> f) (p \<bullet> x)"}\\
+@{text "p \<bullet> f \<equiv> \<lambda>x. p \<bullet> (f (- p \<bullet> x))"}\\
 @{thm permute_bool_def[no_vars, THEN eq_reflection]}\\
 \end{tabular}
-\end{tabular}
+\end{tabular}}
-\end{center}
+\end{equation}
 \noindent
-Concrete  permutations are build up from
+Concrete permutations are build up from swappings, written as @{text "(a
-swappings, written as @{text "(a b)"},
+b)"}, which are permutations that behave as follows:
-which are permutations that behave as follows:
 %
 @{text[display,indent=5] "(a b) = \<lambda>c. if a = c then b else if b = c then a else c"}
 The most original aspect of the nominal logic work of Pitts is a general
 definition for the notion of ``the set of free variables of an object @{text
 @{term "supp b"} & = & @{term "{}"}
 \end{eqnarray}
 \noindent
 it can sometimes be difficult to establish the support precisely,
-and only give an over approximation (see functions above). This
+and only give an approximation (see functions above). Such approximations can
-over approximation can be formalised with the notions \emph{supports},
+be formalised with the notion \emph{supports}, defined as follows.
-defined as follows.
 \begin{defn}
 A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}
 not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.
 \end{defn}
 \noindent
-The point of this definitions is that we can show:
+The point of this definition is that we can show:
 \begin{property}
 {\it i)} @{thm[mode=IfThen] supp_is_subset[no_vars]}
 {\it ii)} @{thm supp_supports[no_vars]}.
 \end{property}
 \noindent
 Another important notion in the nominal logic work is \emph{equivariance}.
+For a function @{text f}, lets say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant
+means that every permutation leaves @{text f} unchanged, or equivalently that
+a permutation applied to an application @{text "f x"} can be moved to its
+arguments. That is
+\begin{center}
+@{text "\<forall>p. p \<bullet> f = f"} \hspace{5mm}
+@{text "\<forall>p. p \<bullet> (f x) = f (p \<bullet> x)"}
+\end{center}
+\noindent
+From the first equation we can be easily deduce that an equivariant function has
+empty support.
 %\begin{property}
 %@{thm[mode=IfThen] at_set_avoiding[no_vars]}
 %\end{property}

changeset 1694	3bf0fddb7d44
parent 1693	3668b389edf3
child 1699	2dca07aca287