nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:6ca795b1cd76
+:26e44bcddb5b
 can be dealt with as in Lemma~\ref{alphaeq}.
 \end{proof}
 \noindent
 We can feed this lemma into our quotient package and obtain new types @{text
-"ty"}$^\alpha_{1..n}$ representing alpha-equated terms. We also obtain
+"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
 "fv_ty"}$^\alpha_{1..n}$ and the binding functions @{text
 "bn"}$^\alpha_{1..k}$. However, these definitions are not really useful to the
 \noindent
 In order to generate \eqref{distinctalpha} from \eqref{distinctraw}, the quotient
 package needs to know that the term-constructors @{text "C\<^isub>i"} and @{text "C\<^isub>j"}
 are \emph{respectful} w.r.t.~the alpha-equivalence relations (see \cite{Homeier05}).
 Assuming @{text "C\<^isub>i"} is of type @{text "ty"} with argument types
-@{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, then respectfulness amounts to showing
+@{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}, then respectfulness amounts to showing that
 \begin{center}
-@{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"}
+@{text "C\<^isub>i x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C\<^isub>i y\<^isub>1 \<dots> y\<^isub>n"}
 \end{center}
 \noindent
 are alpha-equivalent under the assumption that @{text "x\<^isub>i \<approx>ty\<^isub>i y\<^isub>i"} holds for all recursive arguments
-and  @{text "x\<^isub>i = y\<^isub>i"} holds for all non-recursive arguments. We can prove this by
+and  @{text "x\<^isub>i = y\<^isub>i"} holds for all non-recursive arguments of @{text "C\<^isub>i"}. We can prove this by
-analysing the definition of @{text "\<approx>ty"}. For this to succeed we have to establish
+analysing the definition of @{text "\<approx>ty"}. For this proof to succeed we have to establish
 the following auxiliary fact about binding functions. Given a binding function @{text bn\<^isub>i} defined
 for the type @{text ty\<^isub>i}, we have that
 %
 \begin{center}
 @{text "x \<approx>ty\<^isub>i y"} implies @{text "x \<approx>bn\<^isub>i y"}
 \noindent
 This can be established by induction on the definition of @{text "\<approx>ty\<^isub>i"}.
 Having established respectfulness for every raw term-constructor, the
 quotient package is able to automatically deduce \eqref{distinctalpha} from \eqref{distinctraw}.
-In fact we can from now on lift any fact from the raw level to the alpha-equated level that
+In fact we can from now on lift facts from the raw level to the alpha-equated level
-apart from variables only contains the raw term-constructors. The
+as long as they contain raw term-constructors only. The
-induction principles derived by the datatype package in Isabelle/HOL for teh types @{text
+induction principles derived by the datatype package in Isabelle/HOL for the types @{text
-"ty"}$^\alpha_{1..n}$ fall into this category. So we can also add to our infrastructure
+"ty\<AL>\<^bsub>1..n\<^esub>"} fall into this category. So we can also add to our infrastructure
 induction principles that establish
 \begin{center}
 @{text "P\<^bsub>ty\<^isub>1\<^esub> y\<^isub>1 \<dots> P\<^bsub>ty\<^isub>n\<^esub> y\<^isub>n "}
 \end{center}
 \noindent
 for all @{text "y\<^isub>i"} wherby the variables @{text "P\<^bsub>ty\<^isub>i\<^esub>"} stand for properties
-defined over the types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}. The premises of
+defined over the types @{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"}. The premises of
 these induction principles look
 as follows
 \begin{center}
 @{text "\<forall>x\<^isub>1\<dots>x\<^isub>n. P\<^bsub>ty\<^isub>i\<^esub> x\<^isub>i \<and> \<dots> \<and> P\<^bsub>ty\<^isub>j\<^esub> x\<^isub>j \<Rightarrow> P\<^bsub>ty\<^esub> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"}
 to the term-constructors, also permutations operations. In order to make the
 lifting to go through,
 we have to know that the permutation operations are respectful
 w.r.t.~alpha-equivalence. This amounts to showing that the
 alpha-equivalence relations are equivariant, which we already established
-in Lemma~\ref{equiv}. As a result we can add the equations
+in Lemma~\ref{equiv}. As a result we can establish the equations
 \begin{equation}\label{ceqvt}
 @{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
-to our infrastructure. In a similar fashion we can lift the equations
+for our infrastructure. In a similar fashion we can lift the equations
-characterising the free-variable functions @{text "fn_ty\<AL>\<^isub>j"} and the
+characterising the free-variable functions @{text "fn_ty\<AL>\<^isub>j"} and @{text "fv_bn\<AL>\<^isub>k"}, and the
 binding functions @{text "bn\<AL>\<^isub>k"}. The necessary respectfulness lemmas for this
-lifting are the two properties:
+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 "bn\<^isub>k x = bn\<^isub>k 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 "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 how we defined the free-variable
-functions, the second does \emph{not} hold in general. There is, in principle,
+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 second property is just not true. However, our
+variable. 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
 @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n = C\<^sup>\<alpha> y\<^isub>1 \<dots> y\<^isub>n"}
 \end{center}
 \noindent
 We call these conditions as \emph{quasi-injectivity}. Except for one function, which
-we have to lift in the next section, this stage completes
+we have to lift in the next section, we completed
-the lifting part of establishing the reasoning infrastructure. From
+the lifting part of establishing the reasoning infrastructure.
-now on, we can almost completely ``forget'' about the raw types @{text "ty\<^bsub>1..n\<^esub>"} and only
-reason about @{text "ty\<AL>\<^bsub>1..n\<^esub>"}.
+Working bow completely on the alpha-equated level, we can first show that
+the free-variable functions and binding functions
-We can first show that the free-variable 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> (fv_bn\<^sup>\<alpha> x)"} & $=$ & @{text "fv_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
-These two properties can be established by structural induction over the @{text x}.
+These properties can be established by structural induction over the @{text x}
+(using the induction principles we lifted above for the types @{text "ty\<AL>\<^bsub>1..n\<^esub>"}).
-Until now we have not yet derived any fact about the support of the
-alpha-equated terms. Using the equivariance properties in \eqref{ceqvt} we can
+Until now we have not yet derived anything about the support of the
+alpha-equated terms. This however will be necessary in order to derive
+the strong induction principles in the next section.
+Using the equivariance properties in \eqref{ceqvt} we can
 show for every term-constructor @{text "C\<^sup>\<alpha>"} that
 \begin{center}
-@{text "supp x\<^isub>1 \<union> \<dots> supp x\<^isub>n supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"}.
+@{text "(supp x\<^isub>1 \<union> \<dots> supp x\<^isub>n) supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"}
 \end{center}
 \noindent
-This together with Property~\ref{supportsprop} allows us to show
+holds. This together with Property~\ref{supportsprop} allows us to show
 \begin{center}
 @{text "finite (supp x\<^isub>i)"}
 \end{center}
 \noindent
 \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
-term-constructors and the use the quasi-injectivity lemmas in order to complete the
+term-constructors and the use then quasi-injectivity lemmas in order to complete the
-proof.
+proof. For the abstraction cases we use the facts derived in Theorem~\ref{suppabs}.
 \end{proof}
 \noindent
-To sum up this section, we established a reasoning infrastructure
+To sum up, we can established automatically a reasoning infrastructure
 for the types @{text "ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"}
 by first lifting definitions from the raw level to the quotient level and
 then establish facts about these lifted definitions. All necessary proofs
-are generated automatically by custom ML-code we implemented. This code can deal with
+are generated automatically by custom ML-code. This code can deal with
 specifications like the one shown in Figure~\ref{nominalcorehas} for Core-Haskell.
 \begin{figure}[t!]
 \begin{boxedminipage}{\linewidth}
 \small
 section {* Strong Induction Principles *}
 text {*
 In the previous section we were able to provide induction principles that
 allow us to perform structural inductions over alpha-equated terms.
-We call such induction principles \emph{weak}, because in case of a term-contructor @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n"},
+We call such induction principles \emph{weak}, because in case of a term-constructor @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n"},
 the induction hypothesis requires us to establish the implication
 %
 \begin{equation}\label{weakprem}
 @{text "\<forall>x\<^isub>1\<dots>x\<^isub>n. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"}
 \end{equation}
 \noindent
 where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}.
-The problem with this implication is that in general it is not easy to establish this
+The problem with this implication is that in general it is not easy to establish it.
-implication
 The reason is we cannot make any assumption about the binders in @{text "C\<^sup>\<alpha>"}
-(for example we cannot assume the variable convention).
+(for example we cannot assume the variable convention for them).
 In \cite{UrbanTasson05} we introduced a method for automatically
 strengthening weak induction principles for terms containing single
 binders. These stronger induction principles allow the user to make additional
 assumptions about binders when proving the induction hypotheses.
 These additional assumptions amount to a formal
 version of the informal variable convention for binders. A natural question is
 whether we can also strengthen the weak induction principles involving
 general binders. We will indeed be able to so, but for this we need an
-additional notion of permuting deep binders.
+additional notion for permuting deep binders.
 Given a binding function @{text "bn"} we define an auxiliary permutation
 operation @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder.
-Given a clause of @{text bn} is defined as @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then
+Assuming a clause of @{text bn} is defined as @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then
-%
+we define  %
 \begin{center}
 @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>n) \<equiv> C y\<^isub>1 \<dots> y\<^isub>n"}
 \end{center}
 \noindent
 \end{tabular}
 \end{center}
 \noindent
 Using the quotient package again we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to
-alpha-equated terms. We can then prove:
+alpha-equated terms. We can then prove the following two facts
-\begin{lemma} Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}
+\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\<^sup>\<alpha>\<^esub> x)"} and {\it ii)}
 @{text "fv_bn\<^isup>\<alpha> x = fv_bn\<^isup>\<alpha> (p \<bullet>\<^bsub>bn\<^sup>\<alpha>\<^esub> x)"}.
 \end{lemma}
 \begin{proof}
 equivalent to first permuting the binders and then calculating the bound
 variables. The second amounts to the fact that permuting the binders has no
 effect on the free-variable 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, without ``changing'' the term. In case of the
+to rename the binders in @{text x}, without ``changing'' @{text x}. In case of the
 @{text "Let"} term-constructor from the example shown
-in \eqref{letpat} this means:
+\eqref{letpat} this means for a permutation @{text "r"}:
+%
-\begin{center}
+\begin{equation}\label{renaming}
-if @{term "supp (Abs_lst (bn p) t)  \<sharp>* q"} then @{text "Let p t = Let (q \<bullet>\<^bsub>bn\<^bsub>pat\<^esub>\<^esub> p) (q \<bullet> t)"}
+\mbox{if @{term "supp (Abs_lst (bn p) t)  \<sharp>* r"}
-\end{center}
+then @{text "Let p t = Let (r \<bullet>\<^bsub>bn\<^bsub>pat\<^esub>\<^esub> p) (r \<bullet> t)"}}
+\end{equation}
 \noindent
 This fact will be used when establishing the strong induction principles.
-They state that instead of establishing the implication
-\begin{center}
+In our running example about @{text "Let"}, they state that instead
-@{text "\<forall>p t\<^isub>1 t\<^isub>2. P\<^bsub>pat\<^esub> p \<and> P\<^bsub>trm\<^esub> t\<^isub>1 \<and> P\<^bsub>trm\<^esub> t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Let p t\<^isub>1 t\<^isub>2)"}
+of establishing the implication
+\begin{center}
+@{text "\<forall>p t. P\<^bsub>pat\<^esub> p \<and> P\<^bsub>trm\<^esub> t \<Rightarrow> P\<^bsub>trm\<^esub> (Let p t)"}
 \end{center}
 \noindent
 it is sufficient to establish the following implication
+%
-\begin{center}
+\begin{equation}\label{strong}
-\begin{tabular}{l}
+\mbox{\begin{tabular}{l}
-@{text "\<forall>p t\<^isub>1 t\<^isub>2 c."}\\
+@{text "\<forall>p t c."}\\
-\hspace{5mm}@{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c \<and>"}\\
+\hspace{5mm}@{text "set (bn p) #\<^sup>* c \<and> (\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t)"}\\
-\hspace{5mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>2)"}\\
+\hspace{15mm}@{text "\<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t)"}
-\hspace{15mm}@{text "\<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t\<^isub>1 t\<^isub>2)"}
+\end{tabular}}
+\end{equation}
+\noindent
+While this implication contains an additional argument, namely @{text c}, and
+also additional universal quantifications, it is usually easier to establish.
+The reason is that we can make the freshness
+assumption @{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c"}, whereby @{text c} can be arbitrarily
+chosen by the user as long as it has finite support.
+Let us now show how we derive the strong induction principles from the
+weak ones. In case of the @{text "Let"}-example we derive by the weak
+induction the following two properties
+%
+\begin{equation}\label{hyps}
+@{text "\<forall>q c. P\<^bsub>trm\<^esub> c (q \<bullet> t)"} \hspace{4mm}
+@{text "\<forall>q\<^isub>1 q\<^isub>2 c. P\<^bsub>pat\<^esub> (q\<^isub>1 \<bullet>\<^bsub>bn\<^esub> (q\<^isub>2 \<bullet> p))"}
+\end{equation}
+\noindent
+For the @{text Let} term-constructor  we therefore have to establish @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t)"}
+assuming \eqref{hyps} as induction hypotheses. By Property~\ref{avoiding} we
+obtain a permutation @{text "r"} such that
+%
+\begin{equation}\label{rprops}
+@{term "(r \<bullet> set (bn (q \<bullet> p))) \<sharp>* c "}\hspace{4mm}
+@{term "supp (Abs_lst (bn (q \<bullet> p)) (q \<bullet> t)) \<sharp>* r"}
+\end{equation}
+\noindent
+hold. The latter fact and \eqref{renaming} give us
+\begin{center}
+@{text "Let (q \<bullet> p) (q \<bullet> t) = Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (r \<bullet> (q \<bullet> t))"}
+\end{center}
+\noindent
+So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t)"}, we are can equally
+establish
+\begin{center}
+@{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (r \<bullet> (q \<bullet> t)))"}
+\end{center}
+\noindent
+To do so, we will use the implication \eqref{strong} of the strong induction
+principle, which requires us to discharge
+the following three proof obligations:
+\begin{center}
+\begin{tabular}{rl}
+{\it i)} &   @{text "set (bn (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\
+{\it ii)} &  @{text "\<forall>d. P\<^bsub>pat\<^esub> d (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p))"}\\
+{\it iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t))"}\\
 \end{tabular}
 \end{center}
 \noindent
-While this implication contains an additional argument, @{text c}, and
+The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it i)}; the
-also additional universal quantifications, it is usually easier to establish.
+second and third from the induction hypotheses in \eqref{hyps} (in the latter case
-The reason is that in the case of @{text "Let"} we can make the freshness
+we have to use the fact that @{term "(r \<bullet> (q \<bullet> t)) = (r + q) \<bullet> t"}).
-assumption @{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c"}, wherby @{text c} can be arbitrarily
-chosen by the user as long as it has finite support.
+Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps},
+we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}.
-With the help of @{text "\<bullet>bn"} functions defined in the previous section
+This completes the proof showing that the strong induction principle derives from
-we can show that binders can be substituted in term constructors. We show
+the weak induction principle. At the moment we can derive the difficult cases of
-this only for the specification from Figure~\ref{nominalcorehas}. The only
+the strong induction principles only by hand, but they are very schematically
-constructor with a complicated binding structure is @{text "ACons"}. For this
+so that with little effort we can even derive the strong induction principle for
-constructor we prove:
+Core-Haskell given in Figure~\ref{nominalcorehas}.
-\begin{eqnarray}
-\lefteqn{@{text "supp (Abs_lst (bv pat) trm) \<sharp>* \<pi> \<Longrightarrow>"}} \nonumber \\
-& & @{text "ACons pat trm al = ACons (\<pi> \<bullet>bv pat) (\<pi> \<bullet> trm) al"} \nonumber
-\end{eqnarray}
-\noindent With the Property~\ref{avoiding} we can prove a strong induction principle
-which we show again only for the interesting constructors in the Core Haskell
-example. We first show the weak induction principle for comparison:
-\begin{equation}\nonumber
-\infer
-{
-\textrm{The properties }@{text "P1, P2, \<dots>, P12"}\textrm{ hold for all }@{text "tkind, ckind, \<dots>"}
-}{
-\begin{tabular}{cp{7cm}}
-%%  @{text "P1 KStar"}\\
-%%  @{text "\<forall>tk1 tk2. \<^raw:\big(>P1 tk1 \<and> P1 tk2\<^raw:\big)> \<Longrightarrow> P1 (KFun tk1 tk2)"}\\
-%%  @{text "\<dots>"}\\
-@{text "\<forall>v ty t1 t2. \<^raw:\big(>P3 ty \<and> P7 t1 \<and> P7 t2\<^raw:\big)> \<Longrightarrow> P7 (Let v ty t1 t2)"}\\
-@{text "\<forall>p t al. \<^raw:\big(>P9 p \<and> P7 t \<and> P8 al\<^raw:\big)> \<Longrightarrow> P8 (ACons p t al)"}\\
-@{text "\<dots>"}
-\end{tabular}
-}
-\end{equation}
-\noindent In comparison, the cases for the same constructors in the derived strong
-induction principle are:
-\begin{equation}\nonumber
-\infer
-{
-\begin{tabular}{cp{7cm}}
-\textrm{The properties }@{text "P1, P2, \<dots>, P12"}\textrm{ hold for all }@{text "tkind, ckind, \<dots>"}\\
-\textrm{ avoiding any atoms in a given }@{text "y"}
-\end{tabular}
-}{
-\begin{tabular}{cp{7cm}}
-%%  @{text "\<forall>b. P1 b KStar"}\\
-%%  @{text "\<forall>tk1 tk2 b. \<^raw:\big(>\<forall>c. P1 c tk1 \<and> \<forall>c. P1 c tk2\<^raw:\big)> \<Longrightarrow> P1 b (KFun tk1 tk2)"}\\
-%%  @{text "\<dots>"}\\
-@{text "\<forall>v ty t1 t2 b. \<^raw:\big(>\<forall>c. P3 c ty \<and> \<forall>c. P7 c t1 \<and> \<forall>c. P7 c t2 \<and>"}\\
-@{text "\<^raw:\hfill>\<and> atom var \<sharp> b\<^raw:\big)> \<Longrightarrow> P7 b (Let v ty t1 t2)"}\\
-@{text "\<forall>p t al b. \<^raw:\big(>\<forall>c. P9 c p \<and> \<forall>c. P7 c t \<and> \<forall>c. P8 c al \<and>"}\\
-@{text "\<^raw:\hfill>\<and> set (bv p) \<sharp>* b\<^raw:\big)> \<Longrightarrow> P8 b (ACons p t al)"}\\
-@{text "\<dots>"}
-\end{tabular}
-}
-\end{equation}
 *}
 section {* Related Work *}

changeset 1770	26e44bcddb5b
parent 1769	6ca795b1cd76
child 1771	3e71af53cedb