nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:15d2d46bf89e
+:3668b389edf3
 for alpha-\emph{equated} terms. In contrast, Ott produces  a reasoning
 infrastructure in Isabelle/HOL for
 \emph{non}-alpha-equated, or ``raw'', terms. While our alpha-equated terms
 and the raw terms produced by Ott use names for bound variables,
 there is a key difference: working with alpha-equated terms means, for example,
-that the two type-schemes (with $x$, $y$ and $z$ being distinct)
+that the two type-schemes
 \begin{center}
 @{text "\<forall>{x}. x \<rightarrow> y  = \<forall>{x, z}. x \<rightarrow> y"}
 \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
-definitions and theorems are respectful w.r.t.~alpha-equivalence.  For exmple, we
+definitions and theorems are respectful w.r.t.~alpha-equivalence.  For example, we
 will not be able to lift a bound-variable function, which can be defined for
 raw terms. The reason is that this function does not respect alpha-equivalence.
 To sum up, every lifting 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
 have the variable convention already built in.
 \begin{figure}
 \begin{boxedminipage}{\linewidth}
 \begin{center}
-\begin{tabular}{rcl}
+\begin{tabular}{r@ {\hspace{2mm}}cl}
 \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}\\
 \multicolumn{3}{@ {}l}{Terms}\\
 @{text "e"} & @{text "::="} & @{text "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 | \<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 "x:\<sigma>"}}$\medskip\\
+@{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "a:\<iota>"}}\;\overline{@{text "x:\<sigma>"}}$\medskip\\
 \multicolumn{3}{@ {}l}{Constants}\\
 @{text C} & & coercion constant\\
 @{text T} & & value type constructor\\
 @{text "S\<^isub>n"} & & n-ary type function\\
 @{text K} & & data constructor\medskip\\
 @{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
+according to \cite{CoreHaskell}. We only made an inessential modification by
 separating the grammars for type kinds and coercion types.\label{corehas}}
 \end{figure}
 *}
 section {* A Short Review of the Nominal Logic Work *}
 \noindent
 it can sometimes be difficult to establish the support precisely,
 and only give an over approximation (see functions above). This
 over approximation can be formalised with the notions \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:
+\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}.
 %\begin{property}
 %@{thm[mode=IfThen] at_set_avoiding[no_vars]}
 %\end{property}
 $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
+about them conveniently 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 *}
 \cite{ott-jfp}. A specification is a collection of (possibly mutual
 recursive) type declarations, say @{text "ty"}$^\alpha_1$, \ldots,
 @{text ty}$^\alpha_n$, and an associated collection
 of binding functions, say @{text bn}$^\alpha_1$, \ldots, @{text
 bn}$^\alpha_m$. The syntax in Nominal Isabelle for such specifications is
-rougly as follows:
+roughly as follows:
 %
 \begin{equation}\label{scheme}
 \mbox{\begin{tabular}{@ {\hspace{-5mm}}p{1.8cm}l}
 type \mbox{declaration part} &
 $\begin{cases}
 In the first case we bind all atoms from the pattern @{text p} in @{text t}
 and also all atoms from @{text q} in @{text t}. As a result we have no way
 to determine whether the binder came from the binding function @{text
 "bn(p)"} or @{text "bn(q)"}. Similarly in the second case. There the binder
 @{text "bn(p)"} overlaps with the shallow binder @{text x}. The reason why
-we must exclude such specifiactions is that they cannot be represent by
+we must exclude such specifications is that they cannot be represent by
 the general binders described in Section \ref{sec:binders}. However
 the following two term-constructors are allowed
 \begin{center}
 \begin{tabular}{ll}
 \noindent
 since there is no overlap of binders.
 Note that in the last example we wrote {\it\isacommand{bind}\;bn(p)\;\isacommand{in}\;p}.
-Whenver such a binding clause is present, we will call the binder \emph{recursive}.
+Whenever such a binding clause is present, we will call the binder \emph{recursive}.
 To see the purpose for this, consider ``plain'' Lets and Let\_recs:
 \begin{center}
 \begin{tabular}{@ {}l@ {}}
 \isacommand{nominal\_datatype} {\it trm} =\\
 Pottier and Cheney pointed out, we cannot in general re-arrange arguments of
 term-constructors so that binders and their bodies are next to each other, and
 then use the type constructors @{text "abs_set"}, @{text "abs_res"} and
 @{text "abs_list"} from Section \ref{sec:binders}. Therefore we will first
 extract datatype definitions from the specification and then define an
-alpha-equiavlence relation over them.
+alpha-equivalence relation over them.
 The datatype definition can be obtained by just stripping off the
 binding clauses and the labels on the types. We also have to invent
 new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
 \end{center}
 \noindent
 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{} for an indepth explanataion of the datatype package
+position (see \cite{} for an indepth explanation of the datatype package
 in Isabelle/HOL). We then define the user-specified binding
 functions by primitive recursion over the raw datatypes. We can also
 easily define a permutation operation by primitive recursion so that for each
 term constructor @{text "C_raw ty\<^isub>1 \<dots> ty\<^isub>n"} we have that
 \noindent
 From this definition we can easily show that the raw datatypes are
 all permutation types (Def ??) by a simple structural induction over
 the @{text "ty_raw"}s.
-The first non-trivial step we have to perform is the generatation free-variable
+The first non-trivial step we have to perform is the generation free-variable
 functions from the specifications. Given types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}
 we need to define the free-variable functions
 \begin{center}
 @{text "fv_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set \<dots> fv_ty\<^isub>n :: ty\<^isub>n \<Rightarrow> atom set"}
 whether it is a recursive or non-recursive of a binder. In these cases the value is:
 \begin{center}
 \begin{tabular}{cp{7cm}}
 $\bullet$ & @{term "{}"} provided @{text "x\<^isub>i"} is a shallow binder\\
-$\bullet$ & @{text "fv_bn_ty\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep non-recursive binder\\
+$\bullet$ & @{text "ft_bn_by\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep non-recursive binder\\
 $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i - bn_ty\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep recursive binder\\
 \end{tabular}
 \end{center}
 \noindent

changeset 1693	3668b389edf3
parent 1690	44a5edac90ad
child 1694	3bf0fddb7d44