# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1270085308 -7200
# Node ID 468c3c1adcba6bc7f795d6f92c9fca70d095d542
# Parent  be28f7b4b97b5106d972e3f003f3c610b8a1924d
more on the paper

diff -r be28f7b4b97b -r 468c3c1adcba Nominal/ExLet.thy
--- a/Nominal/ExLet.thy	Thu Apr 01 01:05:05 2010 +0200
+++ b/Nominal/ExLet.thy	Thu Apr 01 03:28:28 2010 +0200
@@ -6,7 +6,7 @@
 
 atom_decl name
 
-ML {* val _ = recursive := false  *}
+ML {* val _ = recursive := true *}
 ML {* val _ = alpha_type := AlphaLst *}
 nominal_datatype trm =
   Vr "name"
@@ -36,6 +36,7 @@
 (*thm trm_lts.supp*)
 thm trm_lts.fv[simplified trm_lts.supp(1-2)]
 
+
 primrec
   permute_bn_raw
 where
diff -r be28f7b4b97b -r 468c3c1adcba Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Apr 01 01:05:05 2010 +0200
+++ b/Paper/Paper.thy	Thu Apr 01 03:28:28 2010 +0200
@@ -18,9 +18,9 @@
   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
-  alpha_res ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{res}}$}}>\<^bsup>_,_,_\<^esup> _") 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
+  alpha_res ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and
   abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
   fv ("fv'(_')" [100] 100) and
   equal ("=") and
@@ -31,13 +31,14 @@
   Cons ("_::_" [78,77] 73) and
   supp_gen ("aux _" [1000] 10) and
   alpha_bn ("_ \<approx>bn _")
-
 (*>*)
 
 
 section {* Introduction *}
 
 text {*
+  @{text "(1, (2, 3))"}
+
   So far, Nominal Isabelle provides a mechanism for constructing
   alpha-equated terms, for example
 
@@ -733,14 +734,11 @@
   and $\approx_{\textit{abs\_res}}$). We can show that these relations are equivalence 
   relations and equivariant.
 
-  \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)"} (similarly for 
-  the other two relations).
+  \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)"} (similarly for the other two relations).
   \end{lemma}
 
   \begin{proof}
@@ -1343,7 +1341,16 @@
 *}
 (*<*)
 consts alpha_ty ::'a
-notation alpha_ty ("\<approx>ty")
+consts alpha_trm ::'a
+consts fv_trm :: 'a
+consts alpha_trm2 ::'a
+consts fv_trm2 :: 'a
+notation (latex output) 
+  alpha_ty ("\<approx>ty") and
+  alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and
+  fv_trm ("fv\<^bsub>trm\<^esub>") and
+  alpha_trm2 ("\<approx>\<^bsub>assn\<^esub> \<otimes> \<approx>\<^bsub>trm\<^esub>") and
+  fv_trm2 ("fv\<^bsub>assn\<^esub> \<oplus> fv\<^bsub>trm\<^esub>") 
 (*>*)
 text {*
   \begin{itemize}
@@ -1399,7 +1406,7 @@
   recursive arguments of the term-constructor. If they are non-recursive arguments
   then we generate just @{text "x\<^isub>i = y\<^isub>i"}.
 
-  TODO  
+  {\bf TODO (I do not understand the definition below yet).} 
 
   The alpha-equivalence relations for binding functions are similar to the alpha-equivalences
   for their respective types, the difference is that they ommit checking the arguments that
@@ -1418,23 +1425,81 @@
   \end{tabular}
   \end{center}
 
+  Again lets take a look at an example for these definitions. For \eqref{letrecs}
+  we have three relations, namely $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
+  $\approx_{\textit{bn}}$, with the clauses as follows:
+
+  \begin{center}
+  \begin{tabular}{@ {}c @ {}}
+  \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
+  {@{text "as \<approx>\<^bsub>bn\<^esub> as'"} & @{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fv_trm p (bn as', t')"}}\smallskip\\
+  \infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
+  {@{term "\<exists>p. (bn as, (as, t)) \<approx>lst alpha_trm2 fv_trm2 p (bn as', (as', t'))"}}
+  \end{tabular}
+  \end{center}
+
+  \begin{center}
+  \begin{tabular}{@ {}c @ {}}
+  \infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\\
+  \infer{@{text "ACons a t as \<approx>\<^bsub>assn\<^esub> ACons a' t' as"}}
+  {@{text "a = a'"} & @{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>assn\<^esub> as'"}}\medskip\\
+  \end{tabular}
+  \end{center}
+
+  \begin{center}
+  \begin{tabular}{@ {}c @ {}}
+  \infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\\
+  \infer{@{text "ACons a t as \<approx>\<^bsub>bn\<^esub> ACons a' t' as"}}
+  {@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\medskip\\
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  Note the difference between  $\approx_{\textit{assn}}$ and
+  $\approx_{\textit{bn}}$: the latter only ``tracks'' alpha-equivalence of 
+  the components in an assignment that are \emph{not} bound. Therefore we have
+  a $\approx_{\textit{bn}}$-premise in the clause for @{text "Let"} (which is 
+  a non-recursive binder), since the terms inside an assignment are not meant 
+  to be under the binder. Such a premise is not needed in @{text "Let_rec"}, 
+  because there everything from the assignment is under the binder. 
 *}
 
-section {* The Lifting of Definitions and Properties *}
+section {* Establishing the Reasoning Infrastructure *}
 
 text {*
-  To define the quotient types we first need to show that the defined
-  relations are equivalence relations.
+  Having made all these definition for raw terms, we can start to introduce
+  the resoning infrastructure for the specified types. For this we first
+  have to show that the alpha-equivalence relation defined in the previous
+  sections are indeed equivalence relations. 
 
-  \begin{lemma} The relations @{text "\<approx>\<^isub>1 \<dots> \<approx>\<^isub>1"} and @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"}
-  defined as above are equivalence relations and are equivariant.
+  \begin{lemma} 
+  Given the raw types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} and binding functions
+  @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, the relations @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"} and 
+  @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"} are equivalence relations and equivariant.
   \end{lemma}
-  \begin{proof} Reflexivity by induction on the raw datatype. Symmetry,
-  transitivity and equivariance by induction on the alpha equivalence
-  relation. Using lemma \ref{alphaeq}, the conditions follow by simple
-  calculations.  \end{proof}
+
+  \begin{proof} 
+  The proof is by induction over the definitions. The non-trivial
+  cases involves premises build up by $\approx_{\textit{set}}$, 
+  $\approx_{\textit{res}}$ and $\approx_{\textit{list}}$. They 
+  can be dealt with like in Lemma~\ref{alphaeq}.
+  \end{proof}
 
-  \noindent We then define the quotient types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}.  To lift
+  \noindent 
+  We can feed this lemma into our quotient package and obtain new types @{text
+  "ty"}$^\alpha_{1..n}$ representing alpha-equated terms of types @{text
+  "ty"}$_{1..n}$. We also obtain definitions for the term-constructors @{text
+  "C"}$^\alpha_{1..m}$ from the raw term-constructors @{text
+  "C"}$_{1..m}$. Similarly for the free-variable functions @{text
+  "fv_ty"}$^\alpha_{1..n}$ and the binding functions @{text
+  "bn"}$^\alpha_{1..k}$. However, these definitions are of not much use for the 
+  user, since the are formulated in terms of the isomorphism we obtained by 
+  cerating a new type in Isabelle/HOL (remember the picture shown in the 
+  Introduction).
+
+  {\bf TODO below.}
+
+  then define the quotient types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}.  To lift
   the raw definitions to the quotient type, we need to prove that they
   \emph{respect} the relation. We follow the definition of respectfullness given
   by Homeier~\cite{Homeier05}. The intuition behind a respectfullness condition
@@ -1572,28 +1637,8 @@
     permutations on the lifted type and the lifted defining eqautions of @{text "\<bullet>bn"}.
   \end{proof}
 
-
-
 *}
 
-(* @{thm "ACons_subst[no_vars]"}*)
-
-text {*
-%%% FIXME: The restricions should have already been described in previous sections?
-  Restrictions
-
-  \begin{itemize}
-  \item non-emptiness
-  \item positive datatype definitions
-  \item finitely supported abstractions
-  \item respectfulness of the bn-functions\bigskip
-  \item binders can only have a ``single scope''
-  \item all bindings must have the same mode
-  \end{itemize}
-*}
-
-section {* Examples *}
-
 text {*
 
   \begin{figure}
@@ -1629,7 +1674,7 @@
   $|$~@{text "LAM_cty cv::cvar ckind t::trm"}   \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text t}\\
   $|$~@{text "App_ty trm ty"}~$|$~@{text "App_cty trm cty"}~$|$~@{text "App trm trm"}\\
   $|$~@{text "Lam v::var ty t::trm"}  \isacommand{bind}~@{text "v"}~\isacommand{in}~@{text t}\\
-  $|$~@{text "Let x::var ty trm t::trm"}  \isacommand{bind}~{text x}~\isacommand{in}~{text t}\\
+  $|$~@{text "Let x::var ty trm t::trm"}  \isacommand{bind}~@{text x}~\isacommand{in}~@{text t}\\
   $|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\
   \isacommand{and}~@{text "assoc_lst ="}\\
   \phantom{$|$}~@{text ANil}~%
@@ -1657,14 +1702,20 @@
   $|$~@{text "bv3 (TVCKCons c cty tl) = (atom c)::(bv3 tl)"}\\
   \end{tabular}
   \end{boxedminipage}
-  \caption{\label{nominalcorehas}}
+  \caption{The nominal datatype declaration for Core-Haskell. At the moment we
+  do not support nested types; therefore we explicitly have to unfold the 
+  lists @{text "co_lst"}, @{text "assoc_lst"} and so on. This will be improved
+  in a future version of Nominal Isabelle. Apart from that, the 
+  declaration follows closely the original in Figure~\ref{corehas}. The
+  point of our work is that having made such a declaration one obtains
+  automatically a reasoning infrastructure for Core-Haskell.\label{nominalcorehas}}
   \end{figure}
 *}
 
 
-
+(* @{thm "ACons_subst[no_vars]"}*)
 
-section {* Adequacy *}
+section {* Strong Induction Principles *}
 
 section {* Related Work *}
 
@@ -1698,8 +1749,22 @@
   The reasoning there turned out to be quite complex. 
 
   Ott is better with list dot specifications; subgrammars, is untyped; 
+*}
+
+text {*
+%%% FIXME: The restricions should have already been described in previous sections?
+  Restrictions
+
+  \begin{itemize}
+  \item non-emptiness
+  \item positive datatype definitions
+  \item finitely supported abstractions
+  \item respectfulness of the bn-functions\bigskip
+  \item binders can only have a ``single scope''
+  \item all bindings must have the same mode
+  \end{itemize}
+*}
   
-*}
 
 
 section {* Conclusion *}
@@ -1718,9 +1783,7 @@
   the Mercurial repository linked at 
   \href{http://isabelle.in.tum.de/nominal/download}
   {http://isabelle.in.tum.de/nominal/download}.\medskip
-*}
 
-text {*
   \noindent
   {\bf Acknowledgements:} We are very grateful to Andrew Pitts for  
   many discussions about Nominal Isabelle. We thank Peter Sewell for 
@@ -1728,11 +1791,7 @@
   also for patiently explaining some of the finer points about the abstract 
   definitions and about the implementation of the Ott-tool. We
   also thank Stephanie Weirich for suggesting to separate the subgrammars
-  of kinds and types in our Core-Haskell example.
-
-    
-
-  
+  of kinds and types in our Core-Haskell example.  
 *}
 
 
diff -r be28f7b4b97b -r 468c3c1adcba Paper/document/proof.sty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/document/proof.sty	Thu Apr 01 03:28:28 2010 +0200
@@ -0,0 +1,278 @@
+%       proof.sty       (Proof Figure Macros)
+%
+%       version 3.0 (for both LaTeX 2.09 and LaTeX 2e)
+%       Mar 6, 1997
+%       Copyright (C) 1990 -- 1997, Makoto Tatsuta (tatsuta@kusm.kyoto-u.ac.jp)
+% 
+% This program is free software; you can redistribute it or modify
+% it under the terms of the GNU General Public License as published by
+% the Free Software Foundation; either versions 1, or (at your option)
+% any later version.
+% 
+% This program is distributed in the hope that it will be useful
+% but WITHOUT ANY WARRANTY; without even the implied warranty of
+% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+% GNU General Public License for more details.
+%
+%       Usage:
+%               In \documentstyle, specify an optional style `proof', say,
+%                       \documentstyle[proof]{article}.
+%
+%       The following macros are available:
+%
+%       In all the following macros, all the arguments such as
+%       <Lowers> and <Uppers> are processed in math mode.
+%
+%       \infer<Lower><Uppers>
+%               draws an inference.
+%
+%               Use & in <Uppers> to delimit upper formulae.
+%               <Uppers> consists more than 0 formulae.
+%
+%               \infer returns \hbox{ ... } or \vbox{ ... } and
+%               sets \@LeftOffset and \@RightOffset globally.
+%
+%       \infer[<Label>]<Lower><Uppers>
+%               draws an inference labeled with <Label>.
+%
+%       \infer*<Lower><Uppers>
+%               draws a many step deduction.
+%
+%       \infer*[<Label>]<Lower><Uppers>
+%               draws a many step deduction labeled with <Label>.
+%
+%       \infer=<Lower><Uppers>
+%               draws a double-ruled deduction.
+%
+%       \infer=[<Label>]<Lower><Uppers>
+%               draws a double-ruled deduction labeled with <Label>.
+%
+%       \deduce<Lower><Uppers>
+%               draws an inference without a rule.
+%
+%       \deduce[<Proof>]<Lower><Uppers>
+%               draws a many step deduction with a proof name.
+%
+%       Example:
+%               If you want to write
+%                           B C
+%                          -----
+%                      A     D
+%                     ----------
+%                         E
+%       use
+%               \infer{E}{
+%                       A
+%                       &
+%                       \infer{D}{B & C}
+%               }
+%
+
+%       Style Parameters
+
+\newdimen\inferLineSkip         \inferLineSkip=2pt
+\newdimen\inferLabelSkip        \inferLabelSkip=5pt
+\def\inferTabSkip{\quad}
+
+%       Variables
+
+\newdimen\@LeftOffset   % global
+\newdimen\@RightOffset  % global
+\newdimen\@SavedLeftOffset      % safe from users
+
+\newdimen\UpperWidth
+\newdimen\LowerWidth
+\newdimen\LowerHeight
+\newdimen\UpperLeftOffset
+\newdimen\UpperRightOffset
+\newdimen\UpperCenter
+\newdimen\LowerCenter
+\newdimen\UpperAdjust
+\newdimen\RuleAdjust
+\newdimen\LowerAdjust
+\newdimen\RuleWidth
+\newdimen\HLabelAdjust
+\newdimen\VLabelAdjust
+\newdimen\WidthAdjust
+
+\newbox\@UpperPart
+\newbox\@LowerPart
+\newbox\@LabelPart
+\newbox\ResultBox
+
+%       Flags
+
+\newif\if@inferRule     % whether \@infer draws a rule.
+\newif\if@DoubleRule    % whether \@infer draws doulbe rules.
+\newif\if@ReturnLeftOffset      % whether \@infer returns \@LeftOffset.
+\newif\if@MathSaved     % whether inner math mode where \infer or
+                       % \deduce appears.
+
+%       Special Fonts
+
+\def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
+    \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}
+
+%       Math Save Macros
+%
+%       \@SaveMath is called in the very begining of toplevel macros
+%       which are \infer and \deduce.
+%       \@RestoreMath is called in the very last before toplevel macros end.
+%       Remark \infer and \deduce ends calling \@infer.
+
+\def\@SaveMath{\@MathSavedfalse \ifmmode \ifinner
+       \relax $\relax \@MathSavedtrue \fi\fi }
+
+\def\@RestoreMath{\if@MathSaved \relax $\relax\fi }
+
+%       Macros
+
+% Renaming @ifnextchar and @ifnch of LaTeX2e to @IFnextchar and @IFnch.
+
+\def\@IFnextchar#1#2#3{%
+  \let\reserved@e=#1\def\reserved@a{#2}\def\reserved@b{#3}\futurelet
+    \reserved@c\@IFnch}
+\def\@IFnch{\ifx \reserved@c \@sptoken \let\reserved@d\@xifnch
+      \else \ifx \reserved@c \reserved@e\let\reserved@d\reserved@a\else
+          \let\reserved@d\reserved@b\fi
+      \fi \reserved@d}
+
+\def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax
+       \ifx \@tempa \@tempb #2\else #3\fi }
+
+\def\infer{\@SaveMath \@IFnextchar *{\@inferSteps}{\relax
+       \@IFnextchar ={\@inferDoubleRule}{\@inferOneStep}}}
+
+\def\@inferOneStep{\@inferRuletrue \@DoubleRulefalse
+       \@IFnextchar [{\@infer}{\@infer[\@empty]}}
+
+\def\@inferDoubleRule={\@inferRuletrue \@DoubleRuletrue
+       \@IFnextchar [{\@infer}{\@infer[\@empty]}}
+
+\def\@inferSteps*{\@IFnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}}
+
+\def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]}
+
+\def\deduce{\@SaveMath \@IFnextchar [{\@deduce{\@empty}}
+       {\@inferRulefalse \@infer[\@empty]}}
+
+%       \@deduce<Proof Label>[<Proof>]<Lower><Uppers>
+
+\def\@deduce#1[#2]#3#4{\@inferRulefalse
+       \@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}}
+
+%       \@infer[<Label>]<Lower><Uppers>
+%               If \@inferRuletrue, it draws a rule and <Label> is right to
+%               a rule. In this case, if \@DoubleRuletrue, it draws
+%               double rules.
+%
+%               Otherwise, draws no rule and <Label> is right to <Lower>.
+
+\def\@infer[#1]#2#3{\relax
+% Get parameters
+       \if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi
+       \setbox\@LabelPart=\hbox{$#1$}\relax
+       \setbox\@LowerPart=\hbox{$#2$}\relax
+%
+       \global\@LeftOffset=0pt
+       \setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax
+               \global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&&
+               \inferTabSkip
+               \global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr
+               #3\cr}}\relax
+%                       Here is a little trick.
+%                       \@ReturnLeftOffsettrue(false) influences on \infer or
+%                       \deduce placed in ## locally
+%                       because of \@SaveMath and \@RestoreMath.
+       \UpperLeftOffset=\@LeftOffset
+       \UpperRightOffset=\@RightOffset
+% Calculate Adjustments
+       \LowerWidth=\wd\@LowerPart
+       \LowerHeight=\ht\@LowerPart
+       \LowerCenter=0.5\LowerWidth
+%
+       \UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset
+       \advance\UpperWidth by -\UpperRightOffset
+       \UpperCenter=\UpperLeftOffset
+       \advance\UpperCenter by 0.5\UpperWidth
+%
+       \ifdim \UpperWidth > \LowerWidth
+               % \UpperCenter > \LowerCenter
+       \UpperAdjust=0pt
+       \RuleAdjust=\UpperLeftOffset
+       \LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter
+       \RuleWidth=\UpperWidth
+       \global\@LeftOffset=\LowerAdjust
+%
+       \else   % \UpperWidth <= \LowerWidth
+       \ifdim \UpperCenter > \LowerCenter
+%
+       \UpperAdjust=0pt
+       \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter
+       \LowerAdjust=\RuleAdjust
+       \RuleWidth=\LowerWidth
+       \global\@LeftOffset=\LowerAdjust
+%
+       \else   % \UpperWidth <= \LowerWidth
+               % \UpperCenter <= \LowerCenter
+%
+       \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter
+       \RuleAdjust=0pt
+       \LowerAdjust=0pt
+       \RuleWidth=\LowerWidth
+       \global\@LeftOffset=0pt
+%
+       \fi\fi
+% Make a box
+       \if@inferRule
+%
+       \setbox\ResultBox=\vbox{
+               \moveright \UpperAdjust \box\@UpperPart
+               \nointerlineskip \kern\inferLineSkip
+               \if@DoubleRule
+               \moveright \RuleAdjust \vbox{\hrule width\RuleWidth
+                       \kern 1pt\hrule width\RuleWidth}\relax
+               \else
+               \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax
+               \fi
+               \nointerlineskip \kern\inferLineSkip
+               \moveright \LowerAdjust \box\@LowerPart }\relax
+%
+       \@ifEmpty{#1}{}{\relax
+%
+       \HLabelAdjust=\wd\ResultBox     \advance\HLabelAdjust by -\RuleAdjust
+       \advance\HLabelAdjust by -\RuleWidth
+       \WidthAdjust=\HLabelAdjust
+       \advance\WidthAdjust by -\inferLabelSkip
+       \advance\WidthAdjust by -\wd\@LabelPart
+       \ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi
+%
+       \VLabelAdjust=\dp\@LabelPart
+       \advance\VLabelAdjust by -\ht\@LabelPart
+       \VLabelAdjust=0.5\VLabelAdjust  \advance\VLabelAdjust by \LowerHeight
+       \advance\VLabelAdjust by \inferLineSkip
+%
+       \setbox\ResultBox=\hbox{\box\ResultBox
+               \kern -\HLabelAdjust \kern\inferLabelSkip
+               \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax
+%
+       }\relax % end @ifEmpty
+%
+       \else % \@inferRulefalse
+%
+       \setbox\ResultBox=\vbox{
+               \moveright \UpperAdjust \box\@UpperPart
+               \nointerlineskip \kern\inferLineSkip
+               \moveright \LowerAdjust \hbox{\unhbox\@LowerPart
+                       \@ifEmpty{#1}{}{\relax
+                       \kern\inferLabelSkip \unhbox\@LabelPart}}}\relax
+       \fi
+%
+       \global\@RightOffset=\wd\ResultBox
+       \global\advance\@RightOffset by -\@LeftOffset
+       \global\advance\@RightOffset by -\LowerWidth
+       \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi
+%
+       \box\ResultBox
+       \@RestoreMath
+}
diff -r be28f7b4b97b -r 468c3c1adcba Paper/document/root.bib
--- a/Paper/document/root.bib	Thu Apr 01 01:05:05 2010 +0200
+++ b/Paper/document/root.bib	Thu Apr 01 03:28:28 2010 +0200
@@ -11,7 +11,7 @@
   title        = "{T}he {L}ocally {N}ameless {R}epresentation",
   year         = "2009",
   note         = "To appear in J.~of Automated Reasoning. 
-                  {http://arthur.chargueraud.org/research/2009/ln/}",
+                  http://arthur.chargueraud.org/research/2009/ln",
 }
 
 @article{NaraschewskiNipkow99,
diff -r be28f7b4b97b -r 468c3c1adcba Paper/document/root.tex
--- a/Paper/document/root.tex	Thu Apr 01 01:05:05 2010 +0200
+++ b/Paper/document/root.tex	Thu Apr 01 03:28:28 2010 +0200
@@ -10,7 +10,7 @@
 \usepackage{ot1patch}
 \usepackage{times}
 \usepackage{boxedminipage}
-
+\usepackage{proof}
 
 \urlstyle{rm}
 \isabellestyle{it}