# HG changeset patch # User Christian Urban # Date 1269867480 -7200 # Node ID 3668b389edf37e43b6c80f73935f195715ae88b0 # Parent 15d2d46bf89e91f2895d4657b9a388dea37fccc3 spell check diff -r 15d2d46bf89e -r 3668b389edf3 Paper/Paper.thy --- a/Paper/Paper.thy Mon Mar 29 12:06:22 2010 +0200 +++ b/Paper/Paper.thy Mon Mar 29 14:58:00 2010 +0200 @@ -229,7 +229,7 @@ \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 "\{x}. x \ y = \{x, z}. x \ y"} @@ -329,7 +329,7 @@ (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 @@ -363,7 +363,7 @@ \begin{figure} \begin{boxedminipage}{\linewidth} \begin{center} - \begin{tabular}{rcl} + \begin{tabular}{r@ {\hspace{2mm}}cl} \multicolumn{3}{@ {}l}{Type Kinds}\\ @{text "\"} & @{text "::="} & @{text "\ | \\<^isub>1 \ \\<^isub>2"}\medskip\\ \multicolumn{3}{@ {}l}{Coercion Kinds}\\ @@ -383,7 +383,7 @@ & & @{text "\x:\.e | e\<^isub>1 e\<^isub>2 | \ x:\ = e\<^isub>1 \ e\<^isub>2 |"}\\ & & @{text "\ e\<^isub>1 \"}$\;\overline{@{text "p \ e\<^isub>2"}}$ @{text "| e \ \"}\medskip\\ \multicolumn{3}{@ {}l}{Patterns}\\ - @{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\"}}\;\overline{@{text "x:\"}}$\medskip\\ + @{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\"}}\;\overline{@{text "a:\"}}\;\overline{@{text "x:\"}}$\medskip\\ \multicolumn{3}{@ {}l}{Constants}\\ @{text C} & & coercion constant\\ @{text T} & & value type constructor\\ @@ -396,7 +396,7 @@ \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} *} @@ -495,9 +495,23 @@ 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 \ b) \ 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]} @@ -749,7 +763,7 @@ \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. *} @@ -763,7 +777,7 @@ @{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} @@ -930,7 +944,7 @@ 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 @@ -947,7 +961,7 @@ 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} @@ -983,7 +997,7 @@ 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 @@ -998,7 +1012,7 @@ \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 @@ -1013,7 +1027,7 @@ 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, \, ty\<^isub>n"} we need to define the free-variable functions @@ -1044,7 +1058,7 @@ \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}