# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1270710733 -7200
# Node ID 95df71c3df2f0dd9b64005cea8106038ef93e49f
# Parent  b7e524e7ee83e37bae7dade063b41f511fe103aa
added new paper directory for further work

diff -r b7e524e7ee83 -r 95df71c3df2f IsaMakefile
--- a/IsaMakefile	Thu Apr 08 08:40:49 2010 +0200
+++ b/IsaMakefile	Thu Apr 08 09:12:13 2010 +0200
@@ -4,7 +4,7 @@
 default: Nominal2
 images: 
 
-all: Nominal2 paper pearl
+all: Nominal2 paper pearl pearl-jv
 
 
 ## global settings
@@ -32,7 +32,7 @@
 	$(ISABELLE_TOOL) document -o pdf  Paper/generated
 	@cp Paper/document.pdf paper.pdf
 
-## Pearl Paper
+## Pearl Paper ITP
 
 pearl: $(LOG)/HOL-Pearl.gz
 
@@ -41,6 +41,15 @@
 	$(ISABELLE_TOOL) document -o pdf Pearl/generated
 	@cp Pearl/document.pdf pearl.pdf
 
+## Pearl Journal Paper 
+
+pearl-jv: $(LOG)/HOL-Pearl-jv.gz
+
+$(LOG)/HOL-Pearl-jv.gz: Pearl-jv/ROOT.ML Pearl-jv/document/root.* Pearl-jv/*.thy
+	@$(USEDIR) -D generated HOL Pearl-jv
+	$(ISABELLE_TOOL) document -o pdf Pearl-jv/generated
+	@cp Pearl-jv/document.pdf pearl-jv.pdf
+
 
 ## clean
 
diff -r b7e524e7ee83 -r 95df71c3df2f Pearl-jv/Paper.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Pearl-jv/Paper.thy	Thu Apr 08 09:12:13 2010 +0200
@@ -0,0 +1,1238 @@
+(*<*)
+theory Paper
+imports "../Nominal-General/Nominal2_Base" 
+        "../Nominal-General/Nominal2_Atoms" 
+        "../Nominal-General/Nominal2_Eqvt" 
+        "../Nominal-General/Atoms" 
+        "LaTeXsugar"
+begin
+
+notation (latex output)
+  sort_of ("sort _" [1000] 100) and
+  Abs_perm ("_") and
+  Rep_perm ("_") and
+  swap ("'(_ _')" [1000, 1000] 1000) and
+  fresh ("_ # _" [51, 51] 50) and
+  Cons ("_::_" [78,77] 73) and
+  supp ("supp _" [78] 73) and
+  uminus ("-_" [78] 73) and
+  atom ("|_|") and
+  If  ("if _ then _ else _" 10) and
+  Rep_name ("\<lfloor>_\<rfloor>") and
+  Abs_name ("\<lceil>_\<rceil>") and
+  Rep_var ("\<lfloor>_\<rfloor>") and
+  Abs_var ("\<lceil>_\<rceil>") and
+  sort_of_ty ("sort'_ty _")
+
+(* BH: uncomment if you really prefer the dot notation
+syntax (latex output)
+  "_Collect" :: "pttrn => bool => 'a set" ("(1{_ . _})")
+*)
+
+(* sort is used in Lists for sorting *)
+hide const sort
+
+abbreviation
+  "sort \<equiv> sort_of"
+
+abbreviation
+  "sort_ty \<equiv> sort_of_ty"
+
+(*>*)
+
+section {* Introduction *}
+
+text {*
+  Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
+  prover providing a proving infrastructure for convenient reasoning about
+  programming languages. It has been used to formalise an equivalence checking
+  algorithm for LF \cite{UrbanCheneyBerghofer08}, 
+  Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
+  \cite{BengtsonParrow07} 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}.
+
+  At its core Nominal Isabelle is based on the nominal logic work of Pitts et
+  al \cite{GabbayPitts02,Pitts03}.  The most basic notion in this work is a
+  sort-respecting permutation operation defined over a countably infinite
+  collection of sorted atoms. The atoms are used for representing variables
+  that might be bound. Multiple sorts are necessary for being
+  able to represent different kinds of variables. For example, in the language
+  Mini-ML there are bound term variables and bound type variables; each kind
+  needs to be represented by a different sort of atoms.
+
+  Unfortunately, the type system of Isabelle/HOL is not a good fit for the way
+  atoms and sorts are used in the original formulation of the nominal logic work.
+  Therefore it was decided in earlier versions of Nominal Isabelle to use a
+  separate type for each sort of atoms and let the type system enforce the
+  sort-respecting property of permutations. Inspired by the work on nominal
+  unification \cite{UrbanPittsGabbay04}, it seemed best at the time to also
+  implement permutations concretely as lists of pairs of atoms. Thus Nominal
+  Isabelle used the two-place permutation operation with the generic type
+
+  @{text [display,indent=10] "_ \<bullet> _  ::  (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
+
+  \noindent 
+  where @{text "\<alpha>"} stands for the type of atoms and @{text "\<beta>"} for the type
+  of the objects on which the permutation acts. For atoms of type @{text "\<alpha>"} 
+  the permutation operation is defined over the length of lists as follows
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+  @{text "[] \<bullet> c"} & @{text "="} & @{text c}\\
+  @{text "(a b)::\<pi> \<bullet> c"} & @{text "="} & 
+     $\begin{cases} @{text a} & \textrm{if}~@{text "\<pi> \<bullet> c = b"}\\ 
+                    @{text b} & \textrm{if}~@{text "\<pi> \<bullet> c = a"}\\
+                    @{text "\<pi> \<bullet> c"} & \textrm{otherwise}\end{cases}$
+  \end{tabular}\hfill\numbered{atomperm}
+  \end{isabelle}
+
+  \noindent
+  where we write @{text "(a b)"} for a swapping of atoms @{text "a"} and
+  @{text "b"}. For atoms of different type, the permutation operation
+  is defined as @{text "\<pi> \<bullet> c \<equiv> c"}.
+
+  With the list representation of permutations it is impossible to state an
+  ``ill-sorted'' permutation, since the type system excludes lists containing
+  atoms of different type. Another advantage of the list representation is that
+  the basic operations on permutations are already defined in the list library:
+  composition of two permutations (written @{text "_ @ _"}) is just list append,
+  and inversion of a permutation (written @{text "_\<^sup>-\<^sup>1"}) is just
+  list reversal. A disadvantage is that permutations do not have unique
+  representations as lists; we had to explicitly identify permutations according
+  to the relation
+  
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2  \<equiv>  \<forall>a. \<pi>\<^isub>1 \<bullet> a = \<pi>\<^isub>2 \<bullet> a"}
+  \end{tabular}\hfill\numbered{permequ}
+  \end{isabelle}
+
+  When lifting the permutation operation to other types, for example sets,
+  functions and so on, we needed to ensure that every definition is
+  well-behaved in the sense that it satisfies the following three 
+  \emph{permutation properties}:
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
+  i) & @{text "[] \<bullet> x = x"}\\
+  ii) & @{text "(\<pi>\<^isub>1 @ \<pi>\<^isub>2) \<bullet> x = \<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x)"}\\
+  iii) & if @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2"} then @{text "\<pi>\<^isub>1 \<bullet> x = \<pi>\<^isub>2 \<bullet> x"}
+  \end{tabular}\hfill\numbered{permprops}
+  \end{isabelle}
+
+  \noindent
+  From these properties we were able to derive most facts about permutations, and 
+  the type classes of Isabelle/HOL allowed us to reason abstractly about these
+  three properties, and then let the type system automatically enforce these
+  properties for each type.
+
+  The major problem with Isabelle/HOL's type classes, however, is that they
+  support operations with only a single type parameter and the permutation
+  operations @{text "_ \<bullet> _"} used above in the permutation properties
+  contain two! To work around this obstacle, Nominal Isabelle 
+  required the user to
+  declare up-front the collection of \emph{all} atom types, say @{text
+  "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}. From this collection it used custom ML-code to
+  generate @{text n} type classes corresponding to the permutation properties,
+  whereby in these type classes the permutation operation is restricted to
+
+  @{text [display,indent=10] "_ \<bullet> _ :: (\<alpha>\<^isub>i \<times> \<alpha>\<^isub>i) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
+
+  \noindent
+  This operation has only a single type parameter @{text "\<beta>"} (the @{text "\<alpha>\<^isub>i"} are the
+  atom types given by the user). 
+
+  While the representation of permutations-as-lists solved the
+  ``sort-respecting'' requirement and the declaration of all atom types
+  up-front solved the problem with Isabelle/HOL's type classes, this setup
+  caused several problems for formalising the nominal logic work: First,
+  Nominal Isabelle had to generate @{text "n\<^sup>2"} definitions for the
+  permutation operation over @{text "n"} types of atoms.  Second, whenever we
+  need to generalise induction hypotheses by quantifying over permutations, we
+  have to build cumbersome quantifications like
+
+  @{text [display,indent=10] "\<forall>\<pi>\<^isub>1 \<dots> \<forall>\<pi>\<^isub>n. \<dots>"}
+
+  \noindent
+  where the @{text "\<pi>\<^isub>i"} are of type @{text "(\<alpha>\<^isub>i \<times> \<alpha>\<^isub>i) list"}. 
+  The reason is that the permutation operation behaves differently for 
+  every @{text "\<alpha>\<^isub>i"}. Third, although the notion of support
+
+  @{text [display,indent=10] "supp _ :: \<beta> \<Rightarrow> \<alpha> set"}
+
+  \noindent
+  which we will define later, has a generic type @{text "\<alpha> set"}, it cannot be
+  used to express the support of an object over \emph{all} atoms. The reason
+  is again that support can behave differently for each @{text
+  "\<alpha>\<^isub>i"}. This problem is annoying, because if we need to know in
+  a statement that an object, say @{text "x"}, is finitely supported we end up
+  with having to state premises of the form
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{text "finite ((supp x) :: \<alpha>\<^isub>1 set) , \<dots>, finite ((supp x) :: \<alpha>\<^isub>n set)"}
+  \end{tabular}\hfill\numbered{fssequence}
+  \end{isabelle}
+
+  \noindent
+  Sometimes we can avoid such premises completely, if @{text x} is a member of a
+  \emph{finitely supported type}.  However, keeping track of finitely supported
+  types requires another @{text n} type classes, and for technical reasons not
+  all types can be shown to be finitely supported.
+
+  The real pain of having a separate type for each atom sort arises, however, 
+  from another permutation property
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
+  iv) & @{text "\<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x) = (\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  where permutation @{text "\<pi>\<^isub>1"} has type @{text "(\<alpha> \<times> \<alpha>) list"},
+  @{text "\<pi>\<^isub>2"} type @{text "(\<alpha>' \<times> \<alpha>') list"} and @{text x} type @{text
+  "\<beta>"}. This property is needed in order to derive facts about how
+  permutations of different types interact, which is not covered by the
+  permutation properties @{text "i"}-@{text "iii"} shown in
+  \eqref{permprops}. The problem is that this property involves three type
+  parameters. In order to use again Isabelle/HOL's type class mechanism with
+  only permitting a single type parameter, we have to instantiate the atom
+  types. Consequently we end up with an additional @{text "n\<^sup>2"}
+  slightly different type classes for this permutation property.
+  
+  While the problems and pain can be almost completely hidden from the user in
+  the existing implementation of Nominal Isabelle, the work is \emph{not}
+  pretty. It requires a large amount of custom ML-code and also forces the
+  user to declare up-front all atom-types that are ever going to be used in a
+  formalisation. In this paper we set out to solve the problems with multiple
+  type parameters in the permutation operation, and in this way can dispense
+  with the large amounts of custom ML-code for generating multiple variants
+  for some basic definitions. The result is that we can implement a pleasingly
+  simple formalisation of the nominal logic work.\smallskip
+
+  \noindent
+  {\bf Contributions of the paper:} Our use of a single atom type for representing
+  atoms of different sorts and of functions for representing
+  permutations is not novel, but drastically reduces the number of type classes to just
+  two (permutation types and finitely supported types) that we need in order
+  reason abstractly about properties from the nominal logic work. The novel
+  technical contribution of this paper is a mechanism for dealing with
+  ``Church-style'' lambda-terms \cite{Church40} and HOL-based languages
+  \cite{PittsHOL4} where variables and variable binding depend on type
+  annotations.
+*}
+
+section {* Sorted Atoms and Sort-Respecting Permutations *}
+
+text {*
+  In the nominal logic work of Pitts, binders and bound variables are
+  represented by \emph{atoms}.  As stated above, we need to have different
+  \emph{sorts} of atoms to be able to bind different kinds of variables.  A
+  basic requirement is that there must be a countably infinite number of atoms
+  of each sort.  Unlike in our earlier work, where we identified each sort with
+  a separate type, we implement here atoms to be
+*}
+
+          datatype atom\<iota> = Atom\<iota> string nat
+
+text {*
+  \noindent
+  whereby the string argument specifies the sort of the atom.\footnote{A similar 
+  design choice was made by Gunter et al \cite{GunterOsbornPopescu09} 
+  for their variables.}  (The use type
+  \emph{string} is merely for convenience; any countably infinite type would work
+  as well.) 
+  We have an auxiliary function @{text sort} that is defined as @{thm
+  sort_of.simps[no_vars]}, and we clearly have for every finite set @{text X} of
+  atoms and every sort @{text s} the property:
+  
+  \begin{proposition}\label{choosefresh}
+  @{text "If finite X then there exists an atom a such that
+  sort a = s and a \<notin> X"}.
+  \end{proposition}
+
+  For implementing sort-respecting permutations, we use functions of type @{typ
+  "atom => atom"} that @{text "i)"} are bijective; @{text "ii)"} are the
+  identity on all atoms, except a finite number of them; and @{text "iii)"} map
+  each atom to one of the same sort. These properties can be conveniently stated
+  for a function @{text \<pi>} as follows:
+  
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{r@ {\hspace{4mm}}l}
+  i)   & @{term "bij \<pi>"}\\
+  ii)  & @{term "finite {a. \<pi> a \<noteq> a}"}\\
+  iii) & @{term "\<forall>a. sort (\<pi> a) = sort a"}
+  \end{tabular}\hfill\numbered{permtype}
+  \end{isabelle}
+
+  \noindent
+  Like all HOL-based theorem provers, Isabelle/HOL allows us to
+  introduce a new type @{typ perm} that includes just those functions
+  satisfying all three properties. For example the identity function,
+  written @{term id}, is included in @{typ perm}. Also function composition, 
+  written  \mbox{@{text "_ \<circ> _"}}, and function inversion, given by Isabelle/HOL's 
+  inverse operator and written \mbox{@{text "inv _"}}, preserve the properties 
+  @{text "i"}-@{text "iii"}. 
+
+  However, a moment of thought is needed about how to construct non-trivial
+  permutations. In the nominal logic work it turned out to be most convenient
+  to work with swappings, written @{text "(a b)"}.  In our setting the
+  type of swappings must be
+
+  @{text [display,indent=10] "(_ _) :: atom \<Rightarrow> atom \<Rightarrow> perm"}
+
+  \noindent
+  but since permutations are required to respect sorts, we must carefully
+  consider what happens if a user states a swapping of atoms with different
+  sorts.  In earlier versions of Nominal Isabelle, we avoided this problem by
+  using different types for different sorts; the type system prevented users
+  from stating ill-sorted swappings.  Here, however, definitions such 
+  as\footnote{To increase legibility, we omit here and in what follows the
+  @{term Rep_perm} and @{term "Abs_perm"} wrappers that are needed in our
+  implementation since we defined permutation not to be the full function space,
+  but only those functions of type @{typ perm} satisfying properties @{text
+  i}-@{text "iii"}.}
+
+  @{text [display,indent=10] "(a b) \<equiv> \<lambda>c. if a = c then b else (if b = c then a else c)"}
+
+  \noindent
+  do not work in general, because the type system does not prevent @{text a}
+  and @{text b} from having different sorts---in which case the function would
+  violate property @{text iii}.  We could make the definition of swappings
+  partial by adding the precondition @{term "sort a = sort b"},
+  which would mean that in case @{text a} and @{text b} have different sorts,
+  the value of @{text "(a b)"} is unspecified.  However, this looked like a
+  cumbersome solution, since sort-related side conditions would be required
+  everywhere, even to unfold the definition.  It turned out to be more
+  convenient to actually allow the user to state ``ill-sorted'' swappings but
+  limit their ``damage'' by defaulting to the identity permutation in the
+  ill-sorted case:
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}rl}
+  @{text "(a b) \<equiv>"} & @{text "if (sort a = sort b)"}\\ 
+   & \hspace{3mm}@{text "then \<lambda>c. if a = c then b else (if b = c then a else c)"}\\ 
+   & \hspace{3mm}@{text "else id"}
+  \end{tabular}\hfill\numbered{swapdef}
+  \end{isabelle}
+
+  \noindent
+  This function is bijective, the identity on all atoms except
+  @{text a} and @{text b}, and sort respecting. Therefore it is 
+  a function in @{typ perm}. 
+
+  One advantage of using functions instead of lists as a representation for
+  permutations is that for example the swappings
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm swap_commute[no_vars]}\hspace{10mm}
+  @{text "(a a) = id"}
+  \end{tabular}\hfill\numbered{swapeqs}
+  \end{isabelle}
+
+  \noindent
+  are \emph{equal}.  We do not have to use the equivalence relation shown
+  in~\eqref{permequ} to identify them, as we would if they had been represented
+  as lists of pairs.  Another advantage of the function representation is that
+  they form an (additive non-commutative) group provided we define
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm}
+  @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm}
+  @{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{4mm}
+  @{thm diff_def[where x="\<pi>\<^isub>1" and y="\<pi>\<^isub>2"]} 
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  and verify the simple properties
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]} \hspace{3mm}
+  @{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{3mm}
+  @{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{3mm}
+  @{thm group_add_class.left_minus[where a="\<pi>::perm"]} 
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  Again this is in contrast to the list-of-pairs representation which does not
+  form a group. The technical importance of this fact is that for groups we
+  can rely on Isabelle/HOL's rich simplification infrastructure.  This will
+  come in handy when we have to do calculations with permutations. However,
+  note that in this case Isabelle/HOL neglects well-entrenched mathematical
+  terminology that associates with an additive group a commutative
+  operation. Obviously, permutations are not commutative in general, because @{text
+  "p + q \<noteq> q + p"}. However, it is quite difficult to work around this
+  idiosyncrasy of Isabelle/HOL, unless we develop our own algebraic hierarchy
+  and infrastructure. But since the point of this paper is to implement the
+  nominal theory as smoothly as possible in Isabelle/HOL, we will follow its
+  characterisation of additive groups.
+
+  By formalising permutations abstractly as functions, and using a single type
+  for all atoms, we can now restate the \emph{permutation properties} from
+  \eqref{permprops} as just the two equations
+  
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
+  i) & @{thm permute_zero[no_vars]}\\
+  ii) & @{thm permute_plus[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2",no_vars]}
+  \end{tabular}\hfill\numbered{newpermprops}
+  \end{isabelle} 
+
+  \noindent
+  in which the permutation operations are of type @{text "perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} and so
+  have only a single type parameter.  Consequently, these properties are
+  compatible with the one-parameter restriction of Isabelle/HOL's type classes.
+  There is no need to introduce a separate type class instantiated for each
+  sort, like in the old approach.
+
+  The next notion allows us to establish generic lemmas involving the
+  permutation operation.
+
+  \begin{definition}
+  A type @{text "\<beta>"} is a \emph{permutation type} if the permutation
+  properties in \eqref{newpermprops} are satisfied for every @{text "x"} of type
+  @{text "\<beta>"}.  
+  \end{definition}
+
+  \noindent
+  First, it follows from the laws governing
+  groups that a permutation and its inverse cancel each other.  That is, for any
+  @{text "x"} of a permutation type:
+
+  
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm permute_minus_cancel(1)[where p="\<pi>", no_vars]}\hspace{10mm}
+  @{thm permute_minus_cancel(2)[where p="\<pi>", no_vars]}
+  \end{tabular}\hfill\numbered{cancel}
+  \end{isabelle} 
+  
+  \noindent
+  Consequently, in a permutation type the permutation operation @{text "\<pi> \<bullet> _"} is bijective, 
+  which in turn implies the property
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm (lhs) permute_eq_iff[where p="\<pi>", no_vars]}
+  $\;$if and only if$\;$
+  @{thm (rhs) permute_eq_iff[where p="\<pi>", no_vars]}.
+  \end{tabular}\hfill\numbered{permuteequ}
+  \end{isabelle} 
+  
+  \noindent
+  In order to lift the permutation operation to other types, we can define for:
+
+  \begin{isabelle}
+  \begin{tabular}{@ {}c@ {\hspace{-1mm}}c@ {}}
+  \begin{tabular}{@ {}r@ {\hspace{2mm}}l@ {}}
+  atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\
+  functions: &  @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\
+  permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\
+  sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+   booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+  \end{tabular} &
+  \begin{tabular}{@ {}r@ {\hspace{2mm}}l@ {}}
+  lists: & @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+         & @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\[2mm]
+  products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+  nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+  \end{tabular}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  and then establish:
+
+  \begin{theorem}
+  If @{text \<beta>}, @{text "\<beta>\<^isub>1"} and @{text "\<beta>\<^isub>2"} are permutation types, 
+  then so are @{text "atom"}, @{text "\<beta>\<^isub>1 \<Rightarrow> \<beta>\<^isub>2"}, 
+  @{text perm}, @{term "\<beta> set"}, @{term "\<beta> list"}, @{term "\<beta>\<^isub>1 \<times> \<beta>\<^isub>2"},
+  @{text bool} and @{text "nat"}.
+  \end{theorem}
+
+  \begin{proof}
+  All statements are by unfolding the definitions of the permutation operations and simple 
+  calculations involving addition and minus. With permutations for example we 
+  have
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}[b]{@ {}rcl}
+  @{text "0 \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "0 + \<pi>' - 0 = \<pi>'"}\\
+  @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) + \<pi>' - (\<pi>\<^isub>1 + \<pi>\<^isub>2)"}\\
+  & @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) + \<pi>' - \<pi>\<^isub>2 - \<pi>\<^isub>1"}\\
+  & @{text "="} & @{text "\<pi>\<^isub>1 + (\<pi>\<^isub>2 + \<pi>' - \<pi>\<^isub>2) - \<pi>\<^isub>1"} @{text "\<equiv>"} @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> \<pi>'"} 
+  \end{tabular}\hfill\qed
+  \end{isabelle}
+  \end{proof}
+
+  \noindent
+  The main point is that the above reasoning blends smoothly with the reasoning
+  infrastructure of Isabelle/HOL; no custom ML-code is necessary and a single
+  type class suffices. We can also show once and for all that the following
+  property---which caused so many headaches in our earlier setup---holds for any
+  permutation type.
+
+  \begin{lemma}\label{permutecompose} 
+  Given @{term x} is of permutation type, then 
+  @{text "\<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x) = (\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}.
+  \end{lemma}
+
+  \begin{proof} The proof is as follows:
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}[b]{@ {}rcl@ {\hspace{8mm}}l}
+  @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> x"}
+  & @{text "="} & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> (-\<pi>\<^isub>1) \<bullet> \<pi>\<^isub>1 \<bullet> x"} & by \eqref{cancel}\\
+  & @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2 - \<pi>\<^isub>1) \<bullet> \<pi>\<^isub>1 \<bullet> x"}  & by {\rm(\ref{newpermprops}.@{text "ii"})}\\
+  & @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}\\
+  \end{tabular}\hfill\qed
+  \end{isabelle}
+  \end{proof}
+
+*}
+
+section {* Equivariance *}
+
+text {*
+
+  One huge advantage of using bijective permutation functions (as opposed to
+  non-bijective renaming substitutions employed in traditional works syntax) is 
+  the property of \emph{equivariance}
+  and the fact that most HOL-functions (this includes constants) whose argument
+  and result types are permutation types satisfy this property:
+
+  \begin{definition}\label{equivariance}
+  A function @{text f} is \emph{equivariant} if @{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}.
+  \end{definition}
+
+  \noindent
+  There are a number of equivalent formulations for the equivariance property. 
+  For example, assuming @{text f} is of type @{text "\<alpha> \<Rightarrow> \<beta>"}, then equivariance 
+  can also be stated as 
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{text "\<forall>\<pi> x.  \<pi> \<bullet> (f x) = f (\<pi> \<bullet> x)"}
+  \end{tabular}\hfill\numbered{altequivariance}
+  \end{isabelle} 
+
+  \noindent
+  To see that this formulation implies the definition, we just unfold the
+  definition of the permutation operation for functions and simplify with the equation
+  and the cancellation property shown in \eqref{cancel}. To see the other direction, we use 
+  the fact 
+  
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{text "\<pi> \<bullet> (f x) = (\<pi> \<bullet> f) (\<pi> \<bullet> x)"}
+  \end{tabular}\hfill\numbered{permutefunapp}
+  \end{isabelle} 
+
+  \noindent
+  which follows again directly 
+  from the definition of the permutation operation for functions and the cancellation 
+  property. Similarly for functions with more than one argument. 
+
+  Both formulations of equivariance have their advantages and disadvantages:
+  \eqref{altequivariance} is often easier to establish. For example we 
+  can easily show that equality is equivariant
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm eq_eqvt[where p="\<pi>", no_vars]}
+  \end{tabular}
+  \end{isabelle} 
+
+  \noindent
+  using the permutation operation on booleans and property \eqref{permuteequ}. 
+  Lemma~\ref{permutecompose} establishes that the permutation operation is 
+  equivariant. It is also easy to see that the boolean operators, like 
+  @{text "\<and>"}, @{text "\<or>"} and @{text "\<longrightarrow>"} are all equivariant. Furthermore 
+  a simple calculation will show that our swapping functions are equivariant, that is
+  
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm swap_eqvt[where p="\<pi>", no_vars]}
+  \end{tabular}\hfill\numbered{swapeqvt}
+  \end{isabelle} 
+
+  \noindent
+  for all @{text a}, @{text b} and @{text \<pi>}.  These equivariance properties
+  are tremendously helpful later on when we have to push permutations inside
+  terms.
+*}
+
+
+section {* Support and Freshness *}
+
+text {*
+  The most original aspect of the nominal logic work of Pitts et al is a general
+  definition for ``the set of free variables of an object @{text "x"}''.  This
+  definition is general in the sense that it applies not only to lambda-terms,
+  but also to lists, products, sets and even functions. The definition depends
+  only on the permutation operation and on the notion of equality defined for
+  the type of @{text x}, namely:
+
+  @{thm [display,indent=10] supp_def[no_vars, THEN eq_reflection]}
+
+  \noindent
+  (Note that due to the definition of swapping in \eqref{swapdef}, we do not
+  need to explicitly restrict @{text a} and @{text b} to have the same sort.)
+  There is also the derived notion for when an atom @{text a} is \emph{fresh}
+  for an @{text x}, defined as
+  
+  @{thm [display,indent=10] fresh_def[no_vars]}
+
+  \noindent
+  A striking consequence of these definitions is that we can prove
+  without knowing anything about the structure of @{term x} that
+  swapping two fresh atoms, say @{text a} and @{text b}, leave 
+  @{text x} unchanged. For the proof we use the following lemma 
+  about swappings applied to an @{text x}:
+
+  \begin{lemma}\label{swaptriple}
+  Assuming @{text x} is of permutation type, and @{text a}, @{text b} and @{text c} 
+  have the same sort, then @{thm (prem 3) swap_rel_trans[no_vars]} and 
+  @{thm (prem 4) swap_rel_trans[no_vars]} imply @{thm (concl) swap_rel_trans[no_vars]}.
+  \end{lemma}
+
+  \begin{proof}
+  The cases where @{text "a = c"} and @{text "b = c"} are immediate.
+  For the remaining case it is, given our assumptions, easy to calculate 
+  that the permutations
+
+  @{thm [display,indent=10] (concl) swap_triple[no_vars]}
+  
+  \noindent
+  are equal. The lemma is then by application of the second permutation 
+  property shown in \eqref{newpermprops}.\hfill\qed
+  \end{proof}
+
+  \begin{theorem}\label{swapfreshfresh}
+  Let @{text x} be of permutation type.
+  @{thm [mode=IfThen] swap_fresh_fresh[no_vars]}
+  \end{theorem}
+
+  \begin{proof}
+  If @{text a} and @{text b} have different sort, then the swapping is the identity.
+  If they have the same sort, we know by definition of support that both
+  @{term "finite {c. (a \<rightleftharpoons> c) \<bullet> x \<noteq> x}"} and  @{term "finite {c. (b \<rightleftharpoons> c) \<bullet> x \<noteq> x}"}
+  hold. So the union of these sets is finite too, and we know by Proposition~\ref{choosefresh} 
+  that there is an atom @{term c}, with the same sort as @{term a} and @{term b}, 
+  that satisfies \mbox{@{term "(a \<rightleftharpoons> c) \<bullet> x = x"}} and @{term "(b \<rightleftharpoons> c) \<bullet> x = x"}. 
+  Now the theorem follows from Lemma~\ref{swaptriple}.\hfill\qed
+  \end{proof}
+  
+  \noindent
+  Two important properties that need to be established for later calculations is 
+  that @{text "supp"} and freshness are equivariant. For this we first show that:
+
+  \begin{lemma}\label{half}
+  If @{term x} is a permutation type, then @{thm (lhs) fresh_permute_iff[where p="\<pi>",no_vars]} 
+  if and only if @{thm (rhs) fresh_permute_iff[where p="\<pi>",no_vars]}.
+  \end{lemma}
+
+  \begin{proof}
+  \begin{isabelle}
+  \begin{tabular}[t]{c@ {\hspace{2mm}}l@ {\hspace{5mm}}l}
+  & \multicolumn{2}{@ {}l}{@{thm (lhs) fresh_permute_iff[where p="\<pi>",no_vars]} @{text "\<equiv>"}
+    @{term "finite {b. (\<pi> \<bullet> a \<rightleftharpoons> b) \<bullet> \<pi> \<bullet> x \<noteq> \<pi> \<bullet> x}"}}\\
+  @{text "\<Leftrightarrow>"}
+  & @{term "finite {b. (\<pi> \<bullet> a \<rightleftharpoons> \<pi> \<bullet> b) \<bullet> \<pi> \<bullet> x \<noteq> \<pi> \<bullet> x}"} 
+  & since @{text "\<pi> \<bullet> _"} is bijective\\ 
+  @{text "\<Leftrightarrow>"}
+  & @{term "finite {b. \<pi> \<bullet> (a \<rightleftharpoons> b) \<bullet> x \<noteq> \<pi> \<bullet> x}"}
+  & by \eqref{permutecompose} and \eqref{swapeqvt}\\
+  @{text "\<Leftrightarrow>"}
+  & @{term "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"} @{text "\<equiv>"}
+    @{thm (rhs) fresh_permute_iff[where p="\<pi>",no_vars]}
+  & by \eqref{permuteequ}\\
+  \end{tabular}
+  \end{isabelle}\hfill\qed
+  \end{proof}
+
+  \noindent
+  Together with the definition of the permutation operation on booleans,
+  we can immediately infer equivariance of freshness: 
+
+  @{thm [display,indent=10] fresh_eqvt[where p="\<pi>",no_vars]}
+
+  \noindent
+  Now equivariance of @{text "supp"}, namely
+  
+  @{thm [display,indent=10] supp_eqvt[where p="\<pi>",no_vars]}
+  
+  \noindent
+  is by noting that @{thm supp_conv_fresh[no_vars]} and that freshness and 
+  the logical connectives are equivariant.
+
+  While the abstract properties of support and freshness, particularly 
+  Theorem~\ref{swapfreshfresh}, are useful for developing Nominal Isabelle, 
+  one often has to calculate the support of some concrete object. This is 
+  straightforward for example for booleans, nats, products and lists:
+
+  \begin{center}
+  \begin{tabular}{@ {}c@ {\hspace{2mm}}c@ {}}
+  \begin{tabular}{@ {}r@ {\hspace{2mm}}l}
+  @{text "booleans"}: & @{term "supp b = {}"}\\
+  @{text "nats"}:     & @{term "supp n = {}"}\\
+  @{text "products"}: & @{thm supp_Pair[no_vars]}\\
+  \end{tabular} &
+  \begin{tabular}{r@ {\hspace{2mm}}l@ {}}
+  @{text "lists:"} & @{thm supp_Nil[no_vars]}\\
+                   & @{thm supp_Cons[no_vars]}\\
+  \end{tabular}
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  But establishing the support of atoms and permutations in our setup here is a bit 
+  trickier. To do so we will use the following notion about a \emph{supporting set}.
+  
+  \begin{definition}
+  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{definition}
+
+  \noindent
+  The main motivation for this notion is that we can characterise @{text "supp x"} 
+  as the smallest finite set that supports @{text "x"}. For this we prove:
+
+  \begin{lemma}\label{supports} Let @{text x} be of permutation type.
+  \begin{isabelle}
+  \begin{tabular}{r@ {\hspace{4mm}}p{10cm}}
+  i)    & @{thm[mode=IfThen] supp_is_subset[no_vars]}\\
+  ii)   & @{thm[mode=IfThen] supp_supports[no_vars]}\\
+  iii)  & @{thm (concl) supp_is_least_supports[no_vars]}
+         provided @{thm (prem 1) supp_is_least_supports[no_vars]},
+         @{thm (prem 2) supp_is_least_supports[no_vars]}
+         and @{text "S"} is the least such set, that means formally,
+         for all @{text "S'"}, if @{term "finite S'"} and 
+         @{term "S' supports x"} then @{text "S \<subseteq> S'"}.
+  \end{tabular}
+  \end{isabelle} 
+  \end{lemma}
+
+  \begin{proof}
+  For @{text "i)"} we derive a contradiction by assuming there is an atom @{text a}
+  with @{term "a \<in> supp x"} and @{text "a \<notin> S"}. Using the second fact, the 
+  assumption that @{term "S supports x"} gives us that @{text S} is a superset of 
+  @{term "{b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"}, which is finite by the assumption of @{text S}
+  being finite. But this means @{term "a \<notin> supp x"}, contradicting our assumption.
+  Property @{text "ii)"} is by a direct application of 
+  Theorem~\ref{swapfreshfresh}. For the last property, part @{text "i)"} proves
+  one ``half'' of the claimed equation. The other ``half'' is by property 
+  @{text "ii)"} and the fact that @{term "supp x"} is finite by @{text "i)"}.\hfill\qed  
+  \end{proof}
+
+  \noindent
+  These are all relatively straightforward proofs adapted from the existing 
+  nominal logic work. However for establishing the support of atoms and 
+  permutations we found  the following ``optimised'' variant of @{text "iii)"} 
+  more useful:
+
+  \begin{lemma}\label{optimised} Let @{text x} be of permutation type.
+  We have that @{thm (concl) finite_supp_unique[no_vars]}
+  provided @{thm (prem 1) finite_supp_unique[no_vars]},
+  @{thm (prem 2) finite_supp_unique[no_vars]}, and for
+  all @{text "a \<in> S"} and all @{text "b \<notin> S"}, with @{text a}
+  and @{text b} having the same sort, then \mbox{@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"}}
+  \end{lemma}
+
+  \begin{proof}
+  By Lemma \ref{supports}@{text ".iii)"} we have to show that for every finite
+  set @{text S'} that supports @{text x}, \mbox{@{text "S \<subseteq> S'"}} holds. We will
+  assume that there is an atom @{text "a"} that is element of @{text S}, but
+  not @{text "S'"} and derive a contradiction.  Since both @{text S} and
+  @{text S'} are finite, we can by Proposition \ref{choosefresh} obtain an atom
+  @{text b}, which has the same sort as @{text "a"} and for which we know
+  @{text "b \<notin> S"} and @{text "b \<notin> S'"}. Since we assumed @{text "a \<notin> S'"} and
+  we have that @{text "S' supports x"}, we have on one hand @{term "(a \<rightleftharpoons> b) \<bullet> x
+  = x"}. On the other hand, the fact @{text "a \<in> S"} and @{text "b \<notin> S"} imply
+  @{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"} using the assumed implication. This gives us the
+  contradiction.\hfill\qed
+  \end{proof}
+
+  \noindent
+  Using this lemma we only have to show the following three proof-obligations
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}r@ {\hspace{4mm}}l}
+  i)   & @{term "{c} supports c"}\\
+  ii)  & @{term "finite {c}"}\\
+  iii) & @{text "\<forall>a \<in> {c} b \<notin> {c}. sort a = sort b \<longrightarrow> (a b) \<bullet> c \<noteq> c"}
+  \end{tabular}
+  \end{isabelle} 
+
+  \noindent
+  in order to establish that @{thm supp_atom[where a="c", no_vars]} holds.  In
+  Isabelle/HOL these proof-obligations can be discharged by easy
+  simplifications. Similar proof-obligations arise for the support of
+  permutations, which is
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm supp_perm[where p="\<pi>", no_vars]}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  The only proof-obligation that is 
+  interesting is the one where we have to show that
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{text "If \<pi> \<bullet> a \<noteq> a, \<pi> \<bullet> b = b and sort a = sort b, then (a b) \<bullet> \<pi> \<noteq> \<pi>"}.
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  For this we observe that 
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}rcl}
+  @{thm (lhs) perm_swap_eq[where p="\<pi>", no_vars]} &
+  if and only if &
+  @{thm (rhs) perm_swap_eq[where p="\<pi>", no_vars]}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  holds by a simple calculation using the group properties of permutations.
+  The proof-obligation can then be discharged by analysing the inequality
+  between the permutations @{term "(\<pi> \<bullet> a \<rightleftharpoons> b)"} and @{term "(a \<rightleftharpoons> b)"}.
+
+  The main point about support is that whenever an object @{text x} has finite
+  support, then Proposition~\ref{choosefresh} allows us to choose for @{text x} a 
+  fresh atom with arbitrary sort. This is an important operation in Nominal
+  Isabelle in situations where, for example, a bound variable needs to be
+  renamed. To allow such a choice, we only have to assume \emph{one} premise
+  of the form @{text "finite (supp x)"}
+  for each @{text x}. Compare that with the sequence of premises in our earlier
+  version of Nominal Isabelle (see~\eqref{fssequence}). For more convenience we
+  can define a type class for types where every element has finite support, and
+  prove that the types @{term "atom"}, @{term "perm"}, lists, products and
+  booleans are instances of this type class. Then \emph{no} premise is needed,
+  as the type system of Isabelle/HOL can figure out automatically when an object
+  is finitely supported.
+
+  Unfortunately, this does not work for sets or Isabelle/HOL's function type.
+  There are functions and sets definable in Isabelle/HOL for which the finite
+  support property does not hold.  A simple example of a function with
+  infinite support is the function that returns the natural number of an atom
+  
+  @{text [display, indent=10] "nat_of (Atom s i) \<equiv> i"}
+
+  \noindent
+  This function's support is the set of \emph{all} atoms. To establish this we show @{term "\<not> a \<sharp> nat_of"}. 
+  This is equivalent to assuming the set @{term "{b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"} is finite
+  and deriving a contradiction. From the assumption we also know that 
+  @{term "{a} \<union> {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"} is finite. Then we can use 
+  Proposition~\ref{choosefresh} to choose an atom @{text c} such that
+  @{term "c \<noteq> a"}, @{term "sort_of c = sort_of a"} and @{term "(a \<rightleftharpoons> c) \<bullet> nat_of = nat_of"}.
+  Now we can reason as follows:
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}[b]{@ {}rcl@ {\hspace{5mm}}l}
+  @{text "nat_of a"} & @{text "="} & @{text "(a \<rightleftharpoons> c) \<bullet> (nat_of a)"} & by def.~of permutations on nats\\
+  & @{text "="} & @{term "((a \<rightleftharpoons> c) \<bullet> nat_of) ((a \<rightleftharpoons> c) \<bullet> a)"} & by \eqref{permutefunapp}\\
+  & @{text "="} & @{term "nat_of c"} & by assumptions on @{text c}\\
+  \end{tabular}
+  \end{isabelle}
+  
+
+  \noindent
+  But this means we have that @{term "nat_of a = nat_of c"} and @{term "sort_of a = sort_of c"}.
+  This implies that atoms @{term a} and @{term c} must be equal, which clashes with our
+  assumption @{term "c \<noteq> a"} about how we chose @{text c}. 
+  Cheney \cite{Cheney06} gives similar examples for constructions that have infinite support.
+*}
+
+section {* Induction Principles *}
+
+
+
+
+section {* Concrete Atom Types *}
+
+text {*
+
+  So far, we have presented a system that uses only a single multi-sorted atom
+  type.  This design gives us the flexibility to define operations and prove
+  theorems that are generic with respect to atom sorts.  For example, as
+  illustrated above the @{term supp} function returns a set that includes the
+  free atoms of \emph{all} sorts together; the flexibility offered by the new
+  atom type makes this possible.  
+
+  However, the single multi-sorted atom type does not make an ideal interface
+  for end-users of Nominal Isabelle.  If sorts are not distinguished by
+  Isabelle's type system, users must reason about atom sorts manually.  That
+  means subgoals involving sorts must be discharged explicitly within proof
+  scripts, instead of being inferred by Isabelle/HOL's type checker.  In other
+  cases, lemmas might require additional side conditions about sorts to be true.
+  For example, swapping @{text a} and @{text b} in the pair \mbox{@{term "(a,
+  b)"}} will only produce the expected result if we state the lemma in
+  Isabelle/HOL as:
+*}
+
+          lemma
+	    fixes a b :: "atom"
+	    assumes asm: "sort a = sort b"
+	    shows "(a \<rightleftharpoons> b) \<bullet> (a, b) = (b, a)" 
+          using asm by simp
+
+text {*
+  \noindent
+  Fortunately, it is possible to regain most of the type-checking automation
+  that is lost by moving to a single atom type.  We accomplish this by defining
+  \emph{subtypes} of the generic atom type that only include atoms of a single
+  specific sort.  We call such subtypes \emph{concrete atom types}.
+
+  The following Isabelle/HOL command defines a concrete atom type called
+  \emph{name}, which consists of atoms whose sort equals the string @{term
+  "''name''"}.
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \isacommand{typedef}\ \ @{typ name} = @{term "{a. sort\<iota> a = ''name''}"}
+  \end{isabelle}
+
+  \noindent
+  This command automatically generates injective functions that map from the
+  concrete atom type into the generic atom type and back, called
+  representation and abstraction functions, respectively. We will write these
+  functions as follows:
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l@ {\hspace{10mm}}l}
+  @{text "\<lfloor>_\<rfloor> :: name \<Rightarrow> atom"} & 
+  @{text "\<lceil>_\<rceil> :: atom \<Rightarrow> name"}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  With the definition @{thm permute_name_def [where p="\<pi>", THEN
+  eq_reflection, no_vars]}, it is straightforward to verify that the type 
+  @{typ name} is a permutation type.
+
+  In order to reason uniformly about arbitrary concrete atom types, we define a
+  type class that characterises type @{typ name} and other similarly-defined
+  types.  The definition of the concrete atom type class is as follows: First,
+  every concrete atom type must be a permutation type.  In addition, the class
+  defines an overloaded function that maps from the concrete type into the
+  generic atom type, which we will write @{text "|_|"}.  For each class
+  instance, this function must be injective and equivariant, and its outputs
+  must all have the same sort, that is
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{r@ {\hspace{3mm}}l}
+  i)   if @{thm (lhs) atom_eq_iff [no_vars]} then @{thm (rhs) atom_eq_iff [no_vars]}\\
+  ii)  @{thm atom_eqvt[where p="\<pi>", no_vars]}\\
+  iii) @{thm sort_of_atom_eq [no_vars]}
+  \end{tabular}\hfill\numbered{atomprops}
+  \end{isabelle}
+
+  \noindent
+  With the definition @{thm atom_name_def [THEN eq_reflection, no_vars]} we can
+  show that @{typ name} satisfies all the above requirements of a concrete atom
+  type.
+
+  The whole point of defining the concrete atom type class was to let users
+  avoid explicit reasoning about sorts.  This benefit is realised by defining a
+  special swapping operation of type @{text "\<alpha> \<Rightarrow> \<alpha>
+  \<Rightarrow> perm"}, where @{text "\<alpha>"} is a concrete atom type:
+
+  @{thm [display,indent=10] flip_def [THEN eq_reflection, no_vars]}
+
+  \noindent
+  As a consequence of its type, the @{text "\<leftrightarrow>"}-swapping
+  operation works just like the generic swapping operation, but it does not
+  require any sort-checking side conditions---the sort-correctness is ensured by
+  the types!  For @{text "\<leftrightarrow>"} we can establish the following
+  simplification rule:
+
+  @{thm [display,indent=10] permute_flip_at[no_vars]} 
+
+  \noindent
+  If we now want to swap the \emph{concrete} atoms @{text a} and @{text b}
+  in the pair @{term "(a, b)"} we can establish the lemma as follows:
+*}
+
+          lemma
+	    fixes a b :: "name"
+	    shows "(a \<leftrightarrow> b) \<bullet> (a, b) = (b, a)" 
+	  by simp
+
+text {*
+  \noindent
+  There is no need to state an explicit premise involving sorts.
+
+  We can automate the process of creating concrete atom types, so that users 
+  can define a new one simply by issuing the command 
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  \isacommand{atom\_decl}~~@{text "name"}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  This command can be implemented using less than 100 lines of custom ML-code.
+  In comparison, the old version of Nominal Isabelle included more than 1000
+  lines of ML-code for creating concrete atom types, and for defining various
+  type classes and instantiating generic lemmas for them.  In addition to
+  simplifying the ML-code, the setup here also offers user-visible improvements:
+  Now concrete atoms can be declared at any point of a formalisation, and
+  theories that separately declare different atom types can be merged
+  together---it is no longer required to collect all atom declarations in one
+  place.
+*}
+
+
+section {* Multi-Sorted Concrete Atoms *}
+
+(*<*)
+datatype ty = TVar string | Fun ty ty ("_ \<rightarrow> _") 
+(*>*)
+
+text {*
+  The formalisation presented so far allows us to streamline proofs and reduce
+  the amount of custom ML-code in the existing implementation of Nominal
+  Isabelle. In this section we describe a mechanism that extends the
+  capabilities of Nominal Isabelle. This mechanism is about variables with 
+  additional information, for example typing constraints.
+  While we leave a detailed treatment of binders and binding of variables for a 
+  later paper, we will have a look here at how such variables can be 
+  represented by concrete atoms.
+  
+  In the previous section we considered concrete atoms that can be used in
+  simple binders like \emph{@{text "\<lambda>x. x"}}.  Such concrete atoms do
+  not carry any information beyond their identities---comparing for equality
+  is really the only way to analyse ordinary concrete atoms.
+  However, in ``Church-style'' lambda-terms \cite{Church40} and in the terms
+  underlying HOL-systems \cite{PittsHOL4} binders and bound variables have a
+  more complicated structure. For example in the ``Church-style'' lambda-term
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{text "\<lambda>x\<^isub>\<alpha>. x\<^isub>\<alpha> x\<^isub>\<beta>"}
+  \end{tabular}\hfill\numbered{church}
+  \end{isabelle}
+
+  \noindent
+  both variables and binders include typing information indicated by @{text \<alpha>}
+  and @{text \<beta>}. In this setting, we treat @{text "x\<^isub>\<alpha>"} and @{text
+  "x\<^isub>\<beta>"} as distinct variables (assuming @{term "\<alpha>\<noteq>\<beta>"}) so that the
+  variable @{text "x\<^isub>\<alpha>"} is bound by the lambda-abstraction, but not
+  @{text "x\<^isub>\<beta>"}.
+
+  To illustrate how we can deal with this phenomenon, let us represent object
+  types like @{text \<alpha>} and @{text \<beta>} by the datatype
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  \isacommand{datatype}~~@{text "ty = TVar string | ty \<rightarrow> ty"}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  If we attempt to encode a variable naively as a pair of a @{text name} and a @{text ty}, we have the 
+  problem that a swapping, say @{term "(x \<leftrightarrow> y)"}, applied to the pair @{text "((x, \<alpha>), (x, \<beta>))"}
+  will always permute \emph{both} occurrences of @{text x}, even if the types
+  @{text "\<alpha>"} and @{text "\<beta>"} are different. This is unwanted, because it will
+  eventually mean that both occurrences of @{text x} will become bound by a
+  corresponding binder. 
+
+  Another attempt might be to define variables as an instance of the concrete
+  atom type class, where a @{text ty} is somehow encoded within each variable.
+  Remember we defined atoms as the datatype:
+*}
+
+          datatype  atom\<iota>\<iota> = Atom\<iota>\<iota> string nat
+  
+text {*
+  \noindent
+  Considering our method of defining concrete atom types, the usage of a string
+  for the sort of atoms seems a natural choice.  However, none of the results so
+  far depend on this choice and we are free to change it.
+  One possibility is to encode types or any other information by making the sort
+  argument parametric as follows:
+*}
+
+          datatype  'a \<iota>atom\<iota>\<iota>\<iota> = \<iota>Atom\<iota>\<iota> 'a nat
+
+text {*
+  \noindent
+  The problem with this possibility is that we are then back in the old
+  situation where our permutation operation is parametric in two types and
+  this would require to work around Isabelle/HOL's restriction on type
+  classes. Fortunately, encoding the types in a separate parameter is not
+  necessary for what we want to achieve, as we only have to know when two
+  types are equal or not. The solution is to use a different sort for each
+  object type.  Then we can use the fact that permutations respect \emph{sorts} to
+  ensure that permutations also respect \emph{object types}.  In order to do
+  this, we must define an injective function @{text "sort_ty"} mapping from
+  object types to sorts.  For defining functions like @{text "sort_ty"}, it is
+  more convenient to use a tree datatype for sorts. Therefore we define
+*}
+
+          datatype  sort = Sort string "(sort list)"
+          datatype  atom\<iota>\<iota>\<iota>\<iota> = Atom\<iota>\<iota>\<iota>\<iota> sort nat
+
+text {*
+  \noindent
+  With this definition,
+  the sorts we considered so far can be encoded just as \mbox{@{text "Sort s []"}}.
+  The point, however, is that we can now define the function @{text sort_ty} simply as
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{text "sort_ty (TVar s) = Sort ''TVar'' [Sort s []]"}\\
+  @{text "sort_ty (\<tau>\<^isub>1 \<rightarrow> \<tau>\<^isub>2) = Sort ''Fun''  [sort_ty \<tau>\<^isub>1, sort_ty \<tau>\<^isub>2]"}
+  \end{tabular}\hfill\numbered{sortty}
+  \end{isabelle}
+
+  \noindent
+  which can easily be shown to be injective.  
+  
+  Having settled on what the sorts should be for ``Church-like'' atoms, we have to
+  give a subtype definition for concrete atoms. Previously we identified a subtype consisting 
+  of atoms of only one specified sort. This must be generalised to all sorts the
+  function @{text "sort_ty"} might produce, i.e.~the
+  range of @{text "sort_ty"}. Therefore we define
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \isacommand{typedef}\ \ @{text var} = @{term "{a. sort a : range sort_ty}"}
+  \end{isabelle}
+
+  \noindent
+  This command gives us again injective representation and abstraction
+  functions. We will write them also as \mbox{@{text "\<lfloor>_\<rfloor> :: var \<Rightarrow> atom"}} and
+  @{text "\<lceil>_\<rceil> :: atom \<Rightarrow> var"}, respectively. 
+
+  We can define the permutation operation for @{text var} as @{thm
+  permute_var_def[where p="\<pi>", THEN eq_reflection, no_vars]} and the
+  injective function to type @{typ atom} as @{thm atom_var_def[THEN
+  eq_reflection, no_vars]}. Finally, we can define a constructor function that
+  makes a @{text var} from a variable name and an object type:
+
+  @{thm [display,indent=10] Var_def[where t="\<alpha>", THEN eq_reflection, no_vars]}
+
+  \noindent
+  With these definitions we can verify all the properties for concrete atom
+  types except Property \ref{atomprops}@{text ".iii)"}, which requires every
+  atom to have the same sort.  This last property is clearly not true for type
+  @{text "var"}.
+  This fact is slightly unfortunate since this
+  property allowed us to use the type-checker in order to shield the user from
+  all sort-constraints.  But this failure is expected here, because we cannot
+  burden the type-system of Isabelle/HOL with the task of deciding when two
+  object types are equal.  This means we sometimes need to explicitly state sort
+  constraints or explicitly discharge them, but as we will see in the lemma
+  below this seems a natural price to pay in these circumstances.
+
+  To sum up this section, the encoding of type-information into atoms allows us 
+  to form the swapping @{term "(Var x \<alpha> \<leftrightarrow> Var y \<alpha>)"} and to prove the following 
+  lemma
+*}
+
+          lemma
+	    assumes asm: "\<alpha> \<noteq> \<beta>" 
+	    shows "(Var x \<alpha> \<leftrightarrow> Var y \<alpha>) \<bullet> (Var x \<alpha>, Var x \<beta>) = (Var y \<alpha>, Var x \<beta>)"
+	    using asm by simp
+
+text {*
+  \noindent 
+  As we expect, the atom @{term "Var x \<beta>"} is left unchanged by the
+  swapping. With this we can faithfully represent bindings in languages
+  involving ``Church-style'' terms and bindings as shown in \eqref{church}. We
+  expect that the creation of such atoms can be easily automated so that the
+  user just needs to specify \isacommand{atom\_decl}~~@{text "var (ty)"}
+  where the argument, or arguments, are datatypes for which we can automatically
+  define an injective function like @{text "sort_ty"} (see \eqref{sortty}).
+  Our hope is that with this approach Benzmueller and Paulson, the authors of 
+  \cite{PaulsonBenzmueller}, can make headway with formalising their results 
+  about simple type theory.  
+  Because of its limitations, they did not attempt this with the old version 
+  of Nominal Isabelle. We also hope we can make progress with formalisations of
+  HOL-based languages.
+*}
+
+
+section {* Conclusion *}
+
+text {*
+  This proof pearl describes a new formalisation of the nominal logic work by
+  Pitts et al. With the definitions we presented here, the formal reasoning blends 
+  smoothly with the infrastructure of the Isabelle/HOL theorem prover. 
+  Therefore the formalisation will be the underlying theory for a 
+  new version of Nominal Isabelle.
+
+  The main difference of this paper with respect to existing work on Nominal
+  Isabelle is the representation of atoms and permutations. First, we used a
+  single type for sorted atoms. This design choice means for a term @{term t},
+  say, that its support is completely characterised by @{term "supp t"}, even
+  if the term contains different kinds of atoms. Also, whenever we have to
+  generalise an induction so that a property @{text P} is not just established
+  for all @{text t}, but for all @{text t} \emph{and} under all permutations
+  @{text \<pi>}, then we only have to state @{term "\<forall>\<pi>. P (\<pi> \<bullet> t)"}. The reason is
+  that permutations can now consist of multiple swapping each of which can
+  swap different kinds of atoms. This simplifies considerably the reasoning
+  involved in building Nominal Isabelle.
+
+  Second, we represented permutations as functions so that the associated
+  permutation operation has only a single type parameter. This is very convenient
+  because the abstract reasoning about permutations fits cleanly
+  with Isabelle/HOL's type classes. No custom ML-code is required to work
+  around rough edges. Moreover, by establishing that our permutations-as-functions
+  representation satisfy the group properties, we were able to use extensively 
+  Isabelle/HOL's reasoning infrastructure for groups. This often reduced proofs 
+  to simple calculations over @{text "+"}, @{text "-"} and @{text "0"}.
+  An interesting point is that we defined the swapping operation so that a 
+  swapping of two atoms with different sorts is \emph{not} excluded, like 
+  in our older work on Nominal Isabelle, but there is no ``effect'' of such 
+  a swapping (it is defined as the identity). This is a crucial insight
+  in order to make the approach based on a single type of sorted atoms to work.
+  But of course it is analogous to the well-known trick of defining division by 
+  zero to return zero.
+
+  We noticed only one disadvantage of the permutations-as-functions: Over
+  lists we can easily perform inductions. For permutation made up from
+  functions, we have to manually derive an appropriate induction principle. We
+  can establish such a principle, but we have no real experience yet whether ours
+  is the most useful principle: such an induction principle was not needed in
+  any of the reasoning we ported from the old Nominal Isabelle, except
+  when showing that if @{term "\<forall>a \<in> supp x. a \<sharp> p"} implies @{term "p \<bullet> x = x"}.
+
+  Finally, our implementation of sorted atoms turned out powerful enough to
+  use it for representing variables that carry on additional information, for
+  example typing annotations. This information is encoded into the sorts. With
+  this we can represent conveniently binding in ``Church-style'' lambda-terms
+  and HOL-based languages. While dealing with such additional information in 
+  dependent type-theories, such as LF or Coq, is straightforward, we are not 
+  aware of any  other approach in a non-dependent HOL-setting that can deal 
+  conveniently with such binders.
+ 
+  The formalisation presented here will eventually become part of the Isabelle 
+  distribution, but for the moment it can be downloaded from the 
+  Mercurial repository linked at 
+  \href{http://isabelle.in.tum.de/nominal/download}
+  {http://isabelle.in.tum.de/nominal/download}.\smallskip
+
+  \noindent
+  {\bf Acknowledgements:} We are very grateful to Jesper Bengtson, Stefan 
+  Berghofer and Cezary Kaliszyk for their comments on earlier versions 
+  of this paper. We are also grateful to the anonymous referee who helped us to
+  put the work into the right context.  
+*}
+
+
+(*<*)
+end
+(*>*)
\ No newline at end of file
diff -r b7e524e7ee83 -r 95df71c3df2f Pearl-jv/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Pearl-jv/ROOT.ML	Thu Apr 08 09:12:13 2010 +0200
@@ -0,0 +1,7 @@
+no_document use_thys ["../Nominal-General/Nominal2_Base", 
+                      "../Nominal-General/Nominal2_Atoms", 
+                      "../Nominal-General/Nominal2_Eqvt",
+                      "../Nominal-General/Atoms", 
+                      "LaTeXsugar"];
+
+use_thys ["Paper"];
\ No newline at end of file
diff -r b7e524e7ee83 -r 95df71c3df2f Pearl-jv/document/llncs.cls
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Pearl-jv/document/llncs.cls	Thu Apr 08 09:12:13 2010 +0200
@@ -0,0 +1,1189 @@
+% LLNCS DOCUMENT CLASS -- version 2.13 (28-Jan-2002)
+% Springer Verlag LaTeX2e support for Lecture Notes in Computer Science
+%
+%%
+%% \CharacterTable
+%%  {Upper-case    \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
+%%   Lower-case    \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
+%%   Digits        \0\1\2\3\4\5\6\7\8\9
+%%   Exclamation   \!     Double quote  \"     Hash (number) \#
+%%   Dollar        \$     Percent       \%     Ampersand     \&
+%%   Acute accent  \'     Left paren    \(     Right paren   \)
+%%   Asterisk      \*     Plus          \+     Comma         \,
+%%   Minus         \-     Point         \.     Solidus       \/
+%%   Colon         \:     Semicolon     \;     Less than     \<
+%%   Equals        \=     Greater than  \>     Question mark \?
+%%   Commercial at \@     Left bracket  \[     Backslash     \\
+%%   Right bracket \]     Circumflex    \^     Underscore    \_
+%%   Grave accent  \`     Left brace    \{     Vertical bar  \|
+%%   Right brace   \}     Tilde         \~}
+%%
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+\ProvidesClass{llncs}[2002/01/28 v2.13
+^^J LaTeX document class for Lecture Notes in Computer Science]
+% Options
+\let\if@envcntreset\iffalse
+\DeclareOption{envcountreset}{\let\if@envcntreset\iftrue}
+\DeclareOption{citeauthoryear}{\let\citeauthoryear=Y}
+\DeclareOption{oribibl}{\let\oribibl=Y}
+\let\if@custvec\iftrue
+\DeclareOption{orivec}{\let\if@custvec\iffalse}
+\let\if@envcntsame\iffalse
+\DeclareOption{envcountsame}{\let\if@envcntsame\iftrue}
+\let\if@envcntsect\iffalse
+\DeclareOption{envcountsect}{\let\if@envcntsect\iftrue}
+\let\if@runhead\iffalse
+\DeclareOption{runningheads}{\let\if@runhead\iftrue}
+
+\let\if@openbib\iffalse
+\DeclareOption{openbib}{\let\if@openbib\iftrue}
+
+% languages
+\let\switcht@@therlang\relax
+\def\ds@deutsch{\def\switcht@@therlang{\switcht@deutsch}}
+\def\ds@francais{\def\switcht@@therlang{\switcht@francais}}
+
+\DeclareOption*{\PassOptionsToClass{\CurrentOption}{article}}
+
+\ProcessOptions
+
+\LoadClass[twoside]{article}
+\RequirePackage{multicol} % needed for the list of participants, index
+
+\setlength{\textwidth}{12.2cm}
+\setlength{\textheight}{19.3cm}
+\renewcommand\@pnumwidth{2em}
+\renewcommand\@tocrmarg{3.5em}
+%
+\def\@dottedtocline#1#2#3#4#5{%
+  \ifnum #1>\c@tocdepth \else
+    \vskip \z@ \@plus.2\p@
+    {\leftskip #2\relax \rightskip \@tocrmarg \advance\rightskip by 0pt plus 2cm
+               \parfillskip -\rightskip \pretolerance=10000
+     \parindent #2\relax\@afterindenttrue
+     \interlinepenalty\@M
+     \leavevmode
+     \@tempdima #3\relax
+     \advance\leftskip \@tempdima \null\nobreak\hskip -\leftskip
+     {#4}\nobreak
+     \leaders\hbox{$\m@th
+        \mkern \@dotsep mu\hbox{.}\mkern \@dotsep
+        mu$}\hfill
+     \nobreak
+     \hb@xt@\@pnumwidth{\hfil\normalfont \normalcolor #5}%
+     \par}%
+  \fi}
+%
+\def\switcht@albion{%
+\def\abstractname{Abstract.}
+\def\ackname{Acknowledgement.}
+\def\andname{and}
+\def\lastandname{\unskip, and}
+\def\appendixname{Appendix}
+\def\chaptername{Chapter}
+\def\claimname{Claim}
+\def\conjecturename{Conjecture}
+\def\contentsname{Table of Contents}
+\def\corollaryname{Corollary}
+\def\definitionname{Definition}
+\def\examplename{Example}
+\def\exercisename{Exercise}
+\def\figurename{Fig.}
+\def\keywordname{{\bf Key words:}}
+\def\indexname{Index}
+\def\lemmaname{Lemma}
+\def\contriblistname{List of Contributors}
+\def\listfigurename{List of Figures}
+\def\listtablename{List of Tables}
+\def\mailname{{\it Correspondence to\/}:}
+\def\noteaddname{Note added in proof}
+\def\notename{Note}
+\def\partname{Part}
+\def\problemname{Problem}
+\def\proofname{Proof}
+\def\propertyname{Property}
+\def\propositionname{Proposition}
+\def\questionname{Question}
+\def\remarkname{Remark}
+\def\seename{see}
+\def\solutionname{Solution}
+\def\subclassname{{\it Subject Classifications\/}:}
+\def\tablename{Table}
+\def\theoremname{Theorem}}
+\switcht@albion
+% Names of theorem like environments are already defined
+% but must be translated if another language is chosen
+%
+% French section
+\def\switcht@francais{%\typeout{On parle francais.}%
+ \def\abstractname{R\'esum\'e.}%
+ \def\ackname{Remerciements.}%
+ \def\andname{et}%
+ \def\lastandname{ et}%
+ \def\appendixname{Appendice}
+ \def\chaptername{Chapitre}%
+ \def\claimname{Pr\'etention}%
+ \def\conjecturename{Hypoth\`ese}%
+ \def\contentsname{Table des mati\`eres}%
+ \def\corollaryname{Corollaire}%
+ \def\definitionname{D\'efinition}%
+ \def\examplename{Exemple}%
+ \def\exercisename{Exercice}%
+ \def\figurename{Fig.}%
+ \def\keywordname{{\bf Mots-cl\'e:}}
+ \def\indexname{Index}
+ \def\lemmaname{Lemme}%
+ \def\contriblistname{Liste des contributeurs}
+ \def\listfigurename{Liste des figures}%
+ \def\listtablename{Liste des tables}%
+ \def\mailname{{\it Correspondence to\/}:}
+ \def\noteaddname{Note ajout\'ee \`a l'\'epreuve}%
+ \def\notename{Remarque}%
+ \def\partname{Partie}%
+ \def\problemname{Probl\`eme}%
+ \def\proofname{Preuve}%
+ \def\propertyname{Caract\'eristique}%
+%\def\propositionname{Proposition}%
+ \def\questionname{Question}%
+ \def\remarkname{Remarque}%
+ \def\seename{voir}
+ \def\solutionname{Solution}%
+ \def\subclassname{{\it Subject Classifications\/}:}
+ \def\tablename{Tableau}%
+ \def\theoremname{Th\'eor\`eme}%
+}
+%
+% German section
+\def\switcht@deutsch{%\typeout{Man spricht deutsch.}%
+ \def\abstractname{Zusammenfassung.}%
+ \def\ackname{Danksagung.}%
+ \def\andname{und}%
+ \def\lastandname{ und}%
+ \def\appendixname{Anhang}%
+ \def\chaptername{Kapitel}%
+ \def\claimname{Behauptung}%
+ \def\conjecturename{Hypothese}%
+ \def\contentsname{Inhaltsverzeichnis}%
+ \def\corollaryname{Korollar}%
+%\def\definitionname{Definition}%
+ \def\examplename{Beispiel}%
+ \def\exercisename{\"Ubung}%
+ \def\figurename{Abb.}%
+ \def\keywordname{{\bf Schl\"usselw\"orter:}}
+ \def\indexname{Index}
+%\def\lemmaname{Lemma}%
+ \def\contriblistname{Mitarbeiter}
+ \def\listfigurename{Abbildungsverzeichnis}%
+ \def\listtablename{Tabellenverzeichnis}%
+ \def\mailname{{\it Correspondence to\/}:}
+ \def\noteaddname{Nachtrag}%
+ \def\notename{Anmerkung}%
+ \def\partname{Teil}%
+%\def\problemname{Problem}%
+ \def\proofname{Beweis}%
+ \def\propertyname{Eigenschaft}%
+%\def\propositionname{Proposition}%
+ \def\questionname{Frage}%
+ \def\remarkname{Anmerkung}%
+ \def\seename{siehe}
+ \def\solutionname{L\"osung}%
+ \def\subclassname{{\it Subject Classifications\/}:}
+ \def\tablename{Tabelle}%
+%\def\theoremname{Theorem}%
+}
+
+% Ragged bottom for the actual page
+\def\thisbottomragged{\def\@textbottom{\vskip\z@ plus.0001fil
+\global\let\@textbottom\relax}}
+
+\renewcommand\small{%
+   \@setfontsize\small\@ixpt{11}%
+   \abovedisplayskip 8.5\p@ \@plus3\p@ \@minus4\p@
+   \abovedisplayshortskip \z@ \@plus2\p@
+   \belowdisplayshortskip 4\p@ \@plus2\p@ \@minus2\p@
+   \def\@listi{\leftmargin\leftmargini
+               \parsep 0\p@ \@plus1\p@ \@minus\p@
+               \topsep 8\p@ \@plus2\p@ \@minus4\p@
+               \itemsep0\p@}%
+   \belowdisplayskip \abovedisplayskip
+}
+
+\frenchspacing
+\widowpenalty=10000
+\clubpenalty=10000
+
+\setlength\oddsidemargin   {63\p@}
+\setlength\evensidemargin  {63\p@}
+\setlength\marginparwidth  {90\p@}
+
+\setlength\headsep   {16\p@}
+
+\setlength\footnotesep{7.7\p@}
+\setlength\textfloatsep{8mm\@plus 2\p@ \@minus 4\p@}
+\setlength\intextsep   {8mm\@plus 2\p@ \@minus 2\p@}
+
+\setcounter{secnumdepth}{2}
+
+\newcounter {chapter}
+\renewcommand\thechapter      {\@arabic\c@chapter}
+
+\newif\if@mainmatter \@mainmattertrue
+\newcommand\frontmatter{\cleardoublepage
+            \@mainmatterfalse\pagenumbering{Roman}}
+\newcommand\mainmatter{\cleardoublepage
+       \@mainmattertrue\pagenumbering{arabic}}
+\newcommand\backmatter{\if@openright\cleardoublepage\else\clearpage\fi
+      \@mainmatterfalse}
+
+\renewcommand\part{\cleardoublepage
+                 \thispagestyle{empty}%
+                 \if@twocolumn
+                     \onecolumn
+                     \@tempswatrue
+                   \else
+                     \@tempswafalse
+                 \fi
+                 \null\vfil
+                 \secdef\@part\@spart}
+
+\def\@part[#1]#2{%
+    \ifnum \c@secnumdepth >-2\relax
+      \refstepcounter{part}%
+      \addcontentsline{toc}{part}{\thepart\hspace{1em}#1}%
+    \else
+      \addcontentsline{toc}{part}{#1}%
+    \fi
+    \markboth{}{}%
+    {\centering
+     \interlinepenalty \@M
+     \normalfont
+     \ifnum \c@secnumdepth >-2\relax
+       \huge\bfseries \partname~\thepart
+       \par
+       \vskip 20\p@
+     \fi
+     \Huge \bfseries #2\par}%
+    \@endpart}
+\def\@spart#1{%
+    {\centering
+     \interlinepenalty \@M
+     \normalfont
+     \Huge \bfseries #1\par}%
+    \@endpart}
+\def\@endpart{\vfil\newpage
+              \if@twoside
+                \null
+                \thispagestyle{empty}%
+                \newpage
+              \fi
+              \if@tempswa
+                \twocolumn
+              \fi}
+
+\newcommand\chapter{\clearpage
+                    \thispagestyle{empty}%
+                    \global\@topnum\z@
+                    \@afterindentfalse
+                    \secdef\@chapter\@schapter}
+\def\@chapter[#1]#2{\ifnum \c@secnumdepth >\m@ne
+                       \if@mainmatter
+                         \refstepcounter{chapter}%
+                         \typeout{\@chapapp\space\thechapter.}%
+                         \addcontentsline{toc}{chapter}%
+                                  {\protect\numberline{\thechapter}#1}%
+                       \else
+                         \addcontentsline{toc}{chapter}{#1}%
+                       \fi
+                    \else
+                      \addcontentsline{toc}{chapter}{#1}%
+                    \fi
+                    \chaptermark{#1}%
+                    \addtocontents{lof}{\protect\addvspace{10\p@}}%
+                    \addtocontents{lot}{\protect\addvspace{10\p@}}%
+                    \if@twocolumn
+                      \@topnewpage[\@makechapterhead{#2}]%
+                    \else
+                      \@makechapterhead{#2}%
+                      \@afterheading
+                    \fi}
+\def\@makechapterhead#1{%
+% \vspace*{50\p@}%
+  {\centering
+    \ifnum \c@secnumdepth >\m@ne
+      \if@mainmatter
+        \large\bfseries \@chapapp{} \thechapter
+        \par\nobreak
+        \vskip 20\p@
+      \fi
+    \fi
+    \interlinepenalty\@M
+    \Large \bfseries #1\par\nobreak
+    \vskip 40\p@
+  }}
+\def\@schapter#1{\if@twocolumn
+                   \@topnewpage[\@makeschapterhead{#1}]%
+                 \else
+                   \@makeschapterhead{#1}%
+                   \@afterheading
+                 \fi}
+\def\@makeschapterhead#1{%
+% \vspace*{50\p@}%
+  {\centering
+    \normalfont
+    \interlinepenalty\@M
+    \Large \bfseries  #1\par\nobreak
+    \vskip 40\p@
+  }}
+
+\renewcommand\section{\@startsection{section}{1}{\z@}%
+                       {-18\p@ \@plus -4\p@ \@minus -4\p@}%
+                       {12\p@ \@plus 4\p@ \@minus 4\p@}%
+                       {\normalfont\large\bfseries\boldmath
+                        \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
+\renewcommand\subsection{\@startsection{subsection}{2}{\z@}%
+                       {-18\p@ \@plus -4\p@ \@minus -4\p@}%
+                       {8\p@ \@plus 4\p@ \@minus 4\p@}%
+                       {\normalfont\normalsize\bfseries\boldmath
+                        \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
+\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}%
+                       {-18\p@ \@plus -4\p@ \@minus -4\p@}%
+                       {-0.5em \@plus -0.22em \@minus -0.1em}%
+                       {\normalfont\normalsize\bfseries\boldmath}}
+\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}%
+                       {-12\p@ \@plus -4\p@ \@minus -4\p@}%
+                       {-0.5em \@plus -0.22em \@minus -0.1em}%
+                       {\normalfont\normalsize\itshape}}
+\renewcommand\subparagraph[1]{\typeout{LLNCS warning: You should not use
+                  \string\subparagraph\space with this class}\vskip0.5cm
+You should not use \verb|\subparagraph| with this class.\vskip0.5cm}
+
+\DeclareMathSymbol{\Gamma}{\mathalpha}{letters}{"00}
+\DeclareMathSymbol{\Delta}{\mathalpha}{letters}{"01}
+\DeclareMathSymbol{\Theta}{\mathalpha}{letters}{"02}
+\DeclareMathSymbol{\Lambda}{\mathalpha}{letters}{"03}
+\DeclareMathSymbol{\Xi}{\mathalpha}{letters}{"04}
+\DeclareMathSymbol{\Pi}{\mathalpha}{letters}{"05}
+\DeclareMathSymbol{\Sigma}{\mathalpha}{letters}{"06}
+\DeclareMathSymbol{\Upsilon}{\mathalpha}{letters}{"07}
+\DeclareMathSymbol{\Phi}{\mathalpha}{letters}{"08}
+\DeclareMathSymbol{\Psi}{\mathalpha}{letters}{"09}
+\DeclareMathSymbol{\Omega}{\mathalpha}{letters}{"0A}
+
+\let\footnotesize\small
+
+\if@custvec
+\def\vec#1{\mathchoice{\mbox{\boldmath$\displaystyle#1$}}
+{\mbox{\boldmath$\textstyle#1$}}
+{\mbox{\boldmath$\scriptstyle#1$}}
+{\mbox{\boldmath$\scriptscriptstyle#1$}}}
+\fi
+
+\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}}
+\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil
+\penalty50\hskip1em\null\nobreak\hfil\squareforqed
+\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi}
+
+\def\getsto{\mathrel{\mathchoice {\vcenter{\offinterlineskip
+\halign{\hfil
+$\displaystyle##$\hfil\cr\gets\cr\to\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr\gets
+\cr\to\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr\gets
+\cr\to\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+\gets\cr\to\cr}}}}}
+\def\lid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
+$\displaystyle##$\hfil\cr<\cr\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr<\cr
+\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr<\cr
+\noalign{\vskip1pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+<\cr
+\noalign{\vskip0.9pt}=\cr}}}}}
+\def\gid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
+$\displaystyle##$\hfil\cr>\cr\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr>\cr
+\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr>\cr
+\noalign{\vskip1pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+>\cr
+\noalign{\vskip0.9pt}=\cr}}}}}
+\def\grole{\mathrel{\mathchoice {\vcenter{\offinterlineskip
+\halign{\hfil
+$\displaystyle##$\hfil\cr>\cr\noalign{\vskip-1pt}<\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr
+>\cr\noalign{\vskip-1pt}<\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr
+>\cr\noalign{\vskip-0.8pt}<\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+>\cr\noalign{\vskip-0.3pt}<\cr}}}}}
+\def\bbbr{{\rm I\!R}} %reelle Zahlen
+\def\bbbm{{\rm I\!M}}
+\def\bbbn{{\rm I\!N}} %natuerliche Zahlen
+\def\bbbf{{\rm I\!F}}
+\def\bbbh{{\rm I\!H}}
+\def\bbbk{{\rm I\!K}}
+\def\bbbp{{\rm I\!P}}
+\def\bbbone{{\mathchoice {\rm 1\mskip-4mu l} {\rm 1\mskip-4mu l}
+{\rm 1\mskip-4.5mu l} {\rm 1\mskip-5mu l}}}
+\def\bbbc{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}}}
+\def\bbbq{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
+Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle\rm Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle\rm Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}}}
+\def\bbbt{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
+T$}\hbox{\hbox to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle\rm T$}\hbox{\hbox
+to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle\rm T$}\hbox{\hbox
+to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm T$}\hbox{\hbox
+to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}}}
+\def\bbbs{{\mathchoice
+{\setbox0=\hbox{$\displaystyle     \rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
+to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle        \rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
+to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle      \rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
+to0pt{\kern0.5\wd0\vrule height0.45\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.4\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
+to0pt{\kern0.55\wd0\vrule height0.45\ht0\hss}\box0}}}}
+\def\bbbz{{\mathchoice {\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}}
+{\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}}
+{\hbox{$\mathsf\scriptstyle Z\kern-0.3em Z$}}
+{\hbox{$\mathsf\scriptscriptstyle Z\kern-0.2em Z$}}}}
+
+\let\ts\,
+
+\setlength\leftmargini  {17\p@}
+\setlength\leftmargin    {\leftmargini}
+\setlength\leftmarginii  {\leftmargini}
+\setlength\leftmarginiii {\leftmargini}
+\setlength\leftmarginiv  {\leftmargini}
+\setlength  \labelsep  {.5em}
+\setlength  \labelwidth{\leftmargini}
+\addtolength\labelwidth{-\labelsep}
+
+\def\@listI{\leftmargin\leftmargini
+            \parsep 0\p@ \@plus1\p@ \@minus\p@
+            \topsep 8\p@ \@plus2\p@ \@minus4\p@
+            \itemsep0\p@}
+\let\@listi\@listI
+\@listi
+\def\@listii {\leftmargin\leftmarginii
+              \labelwidth\leftmarginii
+              \advance\labelwidth-\labelsep
+              \topsep    0\p@ \@plus2\p@ \@minus\p@}
+\def\@listiii{\leftmargin\leftmarginiii
+              \labelwidth\leftmarginiii
+              \advance\labelwidth-\labelsep
+              \topsep    0\p@ \@plus\p@\@minus\p@
+              \parsep    \z@
+              \partopsep \p@ \@plus\z@ \@minus\p@}
+
+\renewcommand\labelitemi{\normalfont\bfseries --}
+\renewcommand\labelitemii{$\m@th\bullet$}
+
+\setlength\arraycolsep{1.4\p@}
+\setlength\tabcolsep{1.4\p@}
+
+\def\tableofcontents{\chapter*{\contentsname\@mkboth{{\contentsname}}%
+                                                    {{\contentsname}}}
+ \def\authcount##1{\setcounter{auco}{##1}\setcounter{@auth}{1}}
+ \def\lastand{\ifnum\value{auco}=2\relax
+                 \unskip{} \andname\
+              \else
+                 \unskip \lastandname\
+              \fi}%
+ \def\and{\stepcounter{@auth}\relax
+          \ifnum\value{@auth}=\value{auco}%
+             \lastand
+          \else
+             \unskip,
+          \fi}%
+ \@starttoc{toc}\if@restonecol\twocolumn\fi}
+
+\def\l@part#1#2{\addpenalty{\@secpenalty}%
+   \addvspace{2em plus\p@}%  % space above part line
+   \begingroup
+     \parindent \z@
+     \rightskip \z@ plus 5em
+     \hrule\vskip5pt
+     \large               % same size as for a contribution heading
+     \bfseries\boldmath   % set line in boldface
+     \leavevmode          % TeX command to enter horizontal mode.
+     #1\par
+     \vskip5pt
+     \hrule
+     \vskip1pt
+     \nobreak             % Never break after part entry
+   \endgroup}
+
+\def\@dotsep{2}
+
+\def\hyperhrefextend{\ifx\hyper@anchor\@undefined\else
+{chapter.\thechapter}\fi}
+
+\def\addnumcontentsmark#1#2#3{%
+\addtocontents{#1}{\protect\contentsline{#2}{\protect\numberline
+                     {\thechapter}#3}{\thepage}\hyperhrefextend}}
+\def\addcontentsmark#1#2#3{%
+\addtocontents{#1}{\protect\contentsline{#2}{#3}{\thepage}\hyperhrefextend}}
+\def\addcontentsmarkwop#1#2#3{%
+\addtocontents{#1}{\protect\contentsline{#2}{#3}{0}\hyperhrefextend}}
+
+\def\@adcmk[#1]{\ifcase #1 \or
+\def\@gtempa{\addnumcontentsmark}%
+  \or    \def\@gtempa{\addcontentsmark}%
+  \or    \def\@gtempa{\addcontentsmarkwop}%
+  \fi\@gtempa{toc}{chapter}}
+\def\addtocmark{\@ifnextchar[{\@adcmk}{\@adcmk[3]}}
+
+\def\l@chapter#1#2{\addpenalty{-\@highpenalty}
+ \vskip 1.0em plus 1pt \@tempdima 1.5em \begingroup
+ \parindent \z@ \rightskip \@tocrmarg
+ \advance\rightskip by 0pt plus 2cm
+ \parfillskip -\rightskip \pretolerance=10000
+ \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip
+ {\large\bfseries\boldmath#1}\ifx0#2\hfil\null
+ \else
+      \nobreak
+      \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern
+      \@dotsep mu$}\hfill
+      \nobreak\hbox to\@pnumwidth{\hss #2}%
+ \fi\par
+ \penalty\@highpenalty \endgroup}
+
+\def\l@title#1#2{\addpenalty{-\@highpenalty}
+ \addvspace{8pt plus 1pt}
+ \@tempdima \z@
+ \begingroup
+ \parindent \z@ \rightskip \@tocrmarg
+ \advance\rightskip by 0pt plus 2cm
+ \parfillskip -\rightskip \pretolerance=10000
+ \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip
+ #1\nobreak
+ \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern
+ \@dotsep mu$}\hfill
+ \nobreak\hbox to\@pnumwidth{\hss #2}\par
+ \penalty\@highpenalty \endgroup}
+
+\def\l@author#1#2{\addpenalty{\@highpenalty}
+ \@tempdima=\z@ %15\p@
+ \begingroup
+ \parindent \z@ \rightskip \@tocrmarg
+ \advance\rightskip by 0pt plus 2cm
+ \pretolerance=10000
+ \leavevmode \advance\leftskip\@tempdima %\hskip -\leftskip
+ \textit{#1}\par
+ \penalty\@highpenalty \endgroup}
+
+%\setcounter{tocdepth}{0}
+\newdimen\tocchpnum
+\newdimen\tocsecnum
+\newdimen\tocsectotal
+\newdimen\tocsubsecnum
+\newdimen\tocsubsectotal
+\newdimen\tocsubsubsecnum
+\newdimen\tocsubsubsectotal
+\newdimen\tocparanum
+\newdimen\tocparatotal
+\newdimen\tocsubparanum
+\tocchpnum=\z@            % no chapter numbers
+\tocsecnum=15\p@          % section 88. plus 2.222pt
+\tocsubsecnum=23\p@       % subsection 88.8 plus 2.222pt
+\tocsubsubsecnum=27\p@    % subsubsection 88.8.8 plus 1.444pt
+\tocparanum=35\p@         % paragraph 88.8.8.8 plus 1.666pt
+\tocsubparanum=43\p@      % subparagraph 88.8.8.8.8 plus 1.888pt
+\def\calctocindent{%
+\tocsectotal=\tocchpnum
+\advance\tocsectotal by\tocsecnum
+\tocsubsectotal=\tocsectotal
+\advance\tocsubsectotal by\tocsubsecnum
+\tocsubsubsectotal=\tocsubsectotal
+\advance\tocsubsubsectotal by\tocsubsubsecnum
+\tocparatotal=\tocsubsubsectotal
+\advance\tocparatotal by\tocparanum}
+\calctocindent
+
+\def\l@section{\@dottedtocline{1}{\tocchpnum}{\tocsecnum}}
+\def\l@subsection{\@dottedtocline{2}{\tocsectotal}{\tocsubsecnum}}
+\def\l@subsubsection{\@dottedtocline{3}{\tocsubsectotal}{\tocsubsubsecnum}}
+\def\l@paragraph{\@dottedtocline{4}{\tocsubsubsectotal}{\tocparanum}}
+\def\l@subparagraph{\@dottedtocline{5}{\tocparatotal}{\tocsubparanum}}
+
+\def\listoffigures{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
+ \fi\section*{\listfigurename\@mkboth{{\listfigurename}}{{\listfigurename}}}
+ \@starttoc{lof}\if@restonecol\twocolumn\fi}
+\def\l@figure{\@dottedtocline{1}{0em}{1.5em}}
+
+\def\listoftables{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
+ \fi\section*{\listtablename\@mkboth{{\listtablename}}{{\listtablename}}}
+ \@starttoc{lot}\if@restonecol\twocolumn\fi}
+\let\l@table\l@figure
+
+\renewcommand\listoffigures{%
+    \section*{\listfigurename
+      \@mkboth{\listfigurename}{\listfigurename}}%
+    \@starttoc{lof}%
+    }
+
+\renewcommand\listoftables{%
+    \section*{\listtablename
+      \@mkboth{\listtablename}{\listtablename}}%
+    \@starttoc{lot}%
+    }
+
+\ifx\oribibl\undefined
+\ifx\citeauthoryear\undefined
+\renewenvironment{thebibliography}[1]
+     {\section*{\refname}
+      \def\@biblabel##1{##1.}
+      \small
+      \list{\@biblabel{\@arabic\c@enumiv}}%
+           {\settowidth\labelwidth{\@biblabel{#1}}%
+            \leftmargin\labelwidth
+            \advance\leftmargin\labelsep
+            \if@openbib
+              \advance\leftmargin\bibindent
+              \itemindent -\bibindent
+              \listparindent \itemindent
+              \parsep \z@
+            \fi
+            \usecounter{enumiv}%
+            \let\p@enumiv\@empty
+            \renewcommand\theenumiv{\@arabic\c@enumiv}}%
+      \if@openbib
+        \renewcommand\newblock{\par}%
+      \else
+        \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}%
+      \fi
+      \sloppy\clubpenalty4000\widowpenalty4000%
+      \sfcode`\.=\@m}
+     {\def\@noitemerr
+       {\@latex@warning{Empty `thebibliography' environment}}%
+      \endlist}
+\def\@lbibitem[#1]#2{\item[{[#1]}\hfill]\if@filesw
+     {\let\protect\noexpand\immediate
+     \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces}
+\newcount\@tempcntc
+\def\@citex[#1]#2{\if@filesw\immediate\write\@auxout{\string\citation{#2}}\fi
+  \@tempcnta\z@\@tempcntb\m@ne\def\@citea{}\@cite{\@for\@citeb:=#2\do
+    {\@ifundefined
+       {b@\@citeb}{\@citeo\@tempcntb\m@ne\@citea\def\@citea{,}{\bfseries
+        ?}\@warning
+       {Citation `\@citeb' on page \thepage \space undefined}}%
+    {\setbox\z@\hbox{\global\@tempcntc0\csname b@\@citeb\endcsname\relax}%
+     \ifnum\@tempcntc=\z@ \@citeo\@tempcntb\m@ne
+       \@citea\def\@citea{,}\hbox{\csname b@\@citeb\endcsname}%
+     \else
+      \advance\@tempcntb\@ne
+      \ifnum\@tempcntb=\@tempcntc
+      \else\advance\@tempcntb\m@ne\@citeo
+      \@tempcnta\@tempcntc\@tempcntb\@tempcntc\fi\fi}}\@citeo}{#1}}
+\def\@citeo{\ifnum\@tempcnta>\@tempcntb\else
+               \@citea\def\@citea{,\,\hskip\z@skip}%
+               \ifnum\@tempcnta=\@tempcntb\the\@tempcnta\else
+               {\advance\@tempcnta\@ne\ifnum\@tempcnta=\@tempcntb \else
+                \def\@citea{--}\fi
+      \advance\@tempcnta\m@ne\the\@tempcnta\@citea\the\@tempcntb}\fi\fi}
+\else
+\renewenvironment{thebibliography}[1]
+     {\section*{\refname}
+      \small
+      \list{}%
+           {\settowidth\labelwidth{}%
+            \leftmargin\parindent
+            \itemindent=-\parindent
+            \labelsep=\z@
+            \if@openbib
+              \advance\leftmargin\bibindent
+              \itemindent -\bibindent
+              \listparindent \itemindent
+              \parsep \z@
+            \fi
+            \usecounter{enumiv}%
+            \let\p@enumiv\@empty
+            \renewcommand\theenumiv{}}%
+      \if@openbib
+        \renewcommand\newblock{\par}%
+      \else
+        \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}%
+      \fi
+      \sloppy\clubpenalty4000\widowpenalty4000%
+      \sfcode`\.=\@m}
+     {\def\@noitemerr
+       {\@latex@warning{Empty `thebibliography' environment}}%
+      \endlist}
+      \def\@cite#1{#1}%
+      \def\@lbibitem[#1]#2{\item[]\if@filesw
+        {\def\protect##1{\string ##1\space}\immediate
+      \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces}
+   \fi
+\else
+\@cons\@openbib@code{\noexpand\small}
+\fi
+
+\def\idxquad{\hskip 10\p@}% space that divides entry from number
+
+\def\@idxitem{\par\hangindent 10\p@}
+
+\def\subitem{\par\setbox0=\hbox{--\enspace}% second order
+                \noindent\hangindent\wd0\box0}% index entry
+
+\def\subsubitem{\par\setbox0=\hbox{--\,--\enspace}% third
+                \noindent\hangindent\wd0\box0}% order index entry
+
+\def\indexspace{\par \vskip 10\p@ plus5\p@ minus3\p@\relax}
+
+\renewenvironment{theindex}
+               {\@mkboth{\indexname}{\indexname}%
+                \thispagestyle{empty}\parindent\z@
+                \parskip\z@ \@plus .3\p@\relax
+                \let\item\par
+                \def\,{\relax\ifmmode\mskip\thinmuskip
+                             \else\hskip0.2em\ignorespaces\fi}%
+                \normalfont\small
+                \begin{multicols}{2}[\@makeschapterhead{\indexname}]%
+                }
+                {\end{multicols}}
+
+\renewcommand\footnoterule{%
+  \kern-3\p@
+  \hrule\@width 2truecm
+  \kern2.6\p@}
+  \newdimen\fnindent
+  \fnindent1em
+\long\def\@makefntext#1{%
+    \parindent \fnindent%
+    \leftskip \fnindent%
+    \noindent
+    \llap{\hb@xt@1em{\hss\@makefnmark\ }}\ignorespaces#1}
+
+\long\def\@makecaption#1#2{%
+  \vskip\abovecaptionskip
+  \sbox\@tempboxa{{\bfseries #1.} #2}%
+  \ifdim \wd\@tempboxa >\hsize
+    {\bfseries #1.} #2\par
+  \else
+    \global \@minipagefalse
+    \hb@xt@\hsize{\hfil\box\@tempboxa\hfil}%
+  \fi
+  \vskip\belowcaptionskip}
+
+\def\fps@figure{htbp}
+\def\fnum@figure{\figurename\thinspace\thefigure}
+\def \@floatboxreset {%
+        \reset@font
+        \small
+        \@setnobreak
+        \@setminipage
+}
+\def\fps@table{htbp}
+\def\fnum@table{\tablename~\thetable}
+\renewenvironment{table}
+               {\setlength\abovecaptionskip{0\p@}%
+                \setlength\belowcaptionskip{10\p@}%
+                \@float{table}}
+               {\end@float}
+\renewenvironment{table*}
+               {\setlength\abovecaptionskip{0\p@}%
+                \setlength\belowcaptionskip{10\p@}%
+                \@dblfloat{table}}
+               {\end@dblfloat}
+
+\long\def\@caption#1[#2]#3{\par\addcontentsline{\csname
+  ext@#1\endcsname}{#1}{\protect\numberline{\csname
+  the#1\endcsname}{\ignorespaces #2}}\begingroup
+    \@parboxrestore
+    \@makecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par
+  \endgroup}
+
+% LaTeX does not provide a command to enter the authors institute
+% addresses. The \institute command is defined here.
+
+\newcounter{@inst}
+\newcounter{@auth}
+\newcounter{auco}
+\newdimen\instindent
+\newbox\authrun
+\newtoks\authorrunning
+\newtoks\tocauthor
+\newbox\titrun
+\newtoks\titlerunning
+\newtoks\toctitle
+
+\def\clearheadinfo{\gdef\@author{No Author Given}%
+                   \gdef\@title{No Title Given}%
+                   \gdef\@subtitle{}%
+                   \gdef\@institute{No Institute Given}%
+                   \gdef\@thanks{}%
+                   \global\titlerunning={}\global\authorrunning={}%
+                   \global\toctitle={}\global\tocauthor={}}
+
+\def\institute#1{\gdef\@institute{#1}}
+
+\def\institutename{\par
+ \begingroup
+ \parskip=\z@
+ \parindent=\z@
+ \setcounter{@inst}{1}%
+ \def\and{\par\stepcounter{@inst}%
+ \noindent$^{\the@inst}$\enspace\ignorespaces}%
+ \setbox0=\vbox{\def\thanks##1{}\@institute}%
+ \ifnum\c@@inst=1\relax
+   \gdef\fnnstart{0}%
+ \else
+   \xdef\fnnstart{\c@@inst}%
+   \setcounter{@inst}{1}%
+   \noindent$^{\the@inst}$\enspace
+ \fi
+ \ignorespaces
+ \@institute\par
+ \endgroup}
+
+\def\@fnsymbol#1{\ensuremath{\ifcase#1\or\star\or{\star\star}\or
+   {\star\star\star}\or \dagger\or \ddagger\or
+   \mathchar "278\or \mathchar "27B\or \|\or **\or \dagger\dagger
+   \or \ddagger\ddagger \else\@ctrerr\fi}}
+
+\def\inst#1{\unskip$^{#1}$}
+\def\fnmsep{\unskip$^,$}
+\def\email#1{{\tt#1}}
+\AtBeginDocument{\@ifundefined{url}{\def\url#1{#1}}{}%
+\@ifpackageloaded{babel}{%
+\@ifundefined{extrasenglish}{}{\addto\extrasenglish{\switcht@albion}}%
+\@ifundefined{extrasfrenchb}{}{\addto\extrasfrenchb{\switcht@francais}}%
+\@ifundefined{extrasgerman}{}{\addto\extrasgerman{\switcht@deutsch}}%
+}{\switcht@@therlang}%
+}
+\def\homedir{\~{ }}
+
+\def\subtitle#1{\gdef\@subtitle{#1}}
+\clearheadinfo
+
+\renewcommand\maketitle{\newpage
+  \refstepcounter{chapter}%
+  \stepcounter{section}%
+  \setcounter{section}{0}%
+  \setcounter{subsection}{0}%
+  \setcounter{figure}{0}
+  \setcounter{table}{0}
+  \setcounter{equation}{0}
+  \setcounter{footnote}{0}%
+  \begingroup
+    \parindent=\z@
+    \renewcommand\thefootnote{\@fnsymbol\c@footnote}%
+    \if@twocolumn
+      \ifnum \col@number=\@ne
+        \@maketitle
+      \else
+        \twocolumn[\@maketitle]%
+      \fi
+    \else
+      \newpage
+      \global\@topnum\z@   % Prevents figures from going at top of page.
+      \@maketitle
+    \fi
+    \thispagestyle{empty}\@thanks
+%
+    \def\\{\unskip\ \ignorespaces}\def\inst##1{\unskip{}}%
+    \def\thanks##1{\unskip{}}\def\fnmsep{\unskip}%
+    \instindent=\hsize
+    \advance\instindent by-\headlineindent
+%    \if!\the\toctitle!\addcontentsline{toc}{title}{\@title}\else
+%       \addcontentsline{toc}{title}{\the\toctitle}\fi
+    \if@runhead
+       \if!\the\titlerunning!\else
+         \edef\@title{\the\titlerunning}%
+       \fi
+       \global\setbox\titrun=\hbox{\small\rm\unboldmath\ignorespaces\@title}%
+       \ifdim\wd\titrun>\instindent
+          \typeout{Title too long for running head. Please supply}%
+          \typeout{a shorter form with \string\titlerunning\space prior to
+                   \string\maketitle}%
+          \global\setbox\titrun=\hbox{\small\rm
+          Title Suppressed Due to Excessive Length}%
+       \fi
+       \xdef\@title{\copy\titrun}%
+    \fi
+%
+    \if!\the\tocauthor!\relax
+      {\def\and{\noexpand\protect\noexpand\and}%
+      \protected@xdef\toc@uthor{\@author}}%
+    \else
+      \def\\{\noexpand\protect\noexpand\newline}%
+      \protected@xdef\scratch{\the\tocauthor}%
+      \protected@xdef\toc@uthor{\scratch}%
+    \fi
+%    \addcontentsline{toc}{author}{\toc@uthor}%
+    \if@runhead
+       \if!\the\authorrunning!
+         \value{@inst}=\value{@auth}%
+         \setcounter{@auth}{1}%
+       \else
+         \edef\@author{\the\authorrunning}%
+       \fi
+       \global\setbox\authrun=\hbox{\small\unboldmath\@author\unskip}%
+       \ifdim\wd\authrun>\instindent
+          \typeout{Names of authors too long for running head. Please supply}%
+          \typeout{a shorter form with \string\authorrunning\space prior to
+                   \string\maketitle}%
+          \global\setbox\authrun=\hbox{\small\rm
+          Authors Suppressed Due to Excessive Length}%
+       \fi
+       \xdef\@author{\copy\authrun}%
+       \markboth{\@author}{\@title}%
+     \fi
+  \endgroup
+  \setcounter{footnote}{\fnnstart}%
+  \clearheadinfo}
+%
+\def\@maketitle{\newpage
+ \markboth{}{}%
+ \def\lastand{\ifnum\value{@inst}=2\relax
+                 \unskip{} \andname\
+              \else
+                 \unskip \lastandname\
+              \fi}%
+ \def\and{\stepcounter{@auth}\relax
+          \ifnum\value{@auth}=\value{@inst}%
+             \lastand
+          \else
+             \unskip,
+          \fi}%
+ \begin{center}%
+ \let\newline\\
+ {\Large \bfseries\boldmath
+  \pretolerance=10000
+  \@title \par}\vskip .8cm
+\if!\@subtitle!\else {\large \bfseries\boldmath
+  \vskip -.65cm
+  \pretolerance=10000
+  \@subtitle \par}\vskip .8cm\fi
+ \setbox0=\vbox{\setcounter{@auth}{1}\def\and{\stepcounter{@auth}}%
+ \def\thanks##1{}\@author}%
+ \global\value{@inst}=\value{@auth}%
+ \global\value{auco}=\value{@auth}%
+ \setcounter{@auth}{1}%
+{\lineskip .5em
+\noindent\ignorespaces
+\@author\vskip.35cm}
+ {\small\institutename}
+ \end{center}%
+ }
+
+% definition of the "\spnewtheorem" command.
+%
+% Usage:
+%
+%     \spnewtheorem{env_nam}{caption}[within]{cap_font}{body_font}
+% or  \spnewtheorem{env_nam}[numbered_like]{caption}{cap_font}{body_font}
+% or  \spnewtheorem*{env_nam}{caption}{cap_font}{body_font}
+%
+% New is "cap_font" and "body_font". It stands for
+% fontdefinition of the caption and the text itself.
+%
+% "\spnewtheorem*" gives a theorem without number.
+%
+% A defined spnewthoerem environment is used as described
+% by Lamport.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\def\@thmcountersep{}
+\def\@thmcounterend{.}
+
+\def\spnewtheorem{\@ifstar{\@sthm}{\@Sthm}}
+
+% definition of \spnewtheorem with number
+
+\def\@spnthm#1#2{%
+  \@ifnextchar[{\@spxnthm{#1}{#2}}{\@spynthm{#1}{#2}}}
+\def\@Sthm#1{\@ifnextchar[{\@spothm{#1}}{\@spnthm{#1}}}
+
+\def\@spxnthm#1#2[#3]#4#5{\expandafter\@ifdefinable\csname #1\endcsname
+   {\@definecounter{#1}\@addtoreset{#1}{#3}%
+   \expandafter\xdef\csname the#1\endcsname{\expandafter\noexpand
+     \csname the#3\endcsname \noexpand\@thmcountersep \@thmcounter{#1}}%
+   \expandafter\xdef\csname #1name\endcsname{#2}%
+   \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}%
+                              \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@spynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
+   {\@definecounter{#1}%
+   \expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}%
+   \expandafter\xdef\csname #1name\endcsname{#2}%
+   \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#3}{#4}}%
+                               \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@spothm#1[#2]#3#4#5{%
+  \@ifundefined{c@#2}{\@latexerr{No theorem environment `#2' defined}\@eha}%
+  {\expandafter\@ifdefinable\csname #1\endcsname
+  {\global\@namedef{the#1}{\@nameuse{the#2}}%
+  \expandafter\xdef\csname #1name\endcsname{#3}%
+  \global\@namedef{#1}{\@spthm{#2}{\csname #1name\endcsname}{#4}{#5}}%
+  \global\@namedef{end#1}{\@endtheorem}}}}
+
+\def\@spthm#1#2#3#4{\topsep 7\p@ \@plus2\p@ \@minus4\p@
+\refstepcounter{#1}%
+\@ifnextchar[{\@spythm{#1}{#2}{#3}{#4}}{\@spxthm{#1}{#2}{#3}{#4}}}
+
+\def\@spxthm#1#2#3#4{\@spbegintheorem{#2}{\csname the#1\endcsname}{#3}{#4}%
+                    \ignorespaces}
+
+\def\@spythm#1#2#3#4[#5]{\@spopargbegintheorem{#2}{\csname
+       the#1\endcsname}{#5}{#3}{#4}\ignorespaces}
+
+\def\@spbegintheorem#1#2#3#4{\trivlist
+                 \item[\hskip\labelsep{#3#1\ #2\@thmcounterend}]#4}
+
+\def\@spopargbegintheorem#1#2#3#4#5{\trivlist
+      \item[\hskip\labelsep{#4#1\ #2}]{#4(#3)\@thmcounterend\ }#5}
+
+% definition of \spnewtheorem* without number
+
+\def\@sthm#1#2{\@Ynthm{#1}{#2}}
+
+\def\@Ynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
+   {\global\@namedef{#1}{\@Thm{\csname #1name\endcsname}{#3}{#4}}%
+    \expandafter\xdef\csname #1name\endcsname{#2}%
+    \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@Thm#1#2#3{\topsep 7\p@ \@plus2\p@ \@minus4\p@
+\@ifnextchar[{\@Ythm{#1}{#2}{#3}}{\@Xthm{#1}{#2}{#3}}}
+
+\def\@Xthm#1#2#3{\@Begintheorem{#1}{#2}{#3}\ignorespaces}
+
+\def\@Ythm#1#2#3[#4]{\@Opargbegintheorem{#1}
+       {#4}{#2}{#3}\ignorespaces}
+
+\def\@Begintheorem#1#2#3{#3\trivlist
+                           \item[\hskip\labelsep{#2#1\@thmcounterend}]}
+
+\def\@Opargbegintheorem#1#2#3#4{#4\trivlist
+      \item[\hskip\labelsep{#3#1}]{#3(#2)\@thmcounterend\ }}
+
+\if@envcntsect
+   \def\@thmcountersep{.}
+   \spnewtheorem{theorem}{Theorem}[section]{\bfseries}{\itshape}
+\else
+   \spnewtheorem{theorem}{Theorem}{\bfseries}{\itshape}
+   \if@envcntreset
+      \@addtoreset{theorem}{section}
+   \else
+      \@addtoreset{theorem}{chapter}
+   \fi
+\fi
+
+%definition of divers theorem environments
+\spnewtheorem*{claim}{Claim}{\itshape}{\rmfamily}
+\spnewtheorem*{proof}{Proof}{\itshape}{\rmfamily}
+\if@envcntsame % alle Umgebungen wie Theorem.
+   \def\spn@wtheorem#1#2#3#4{\@spothm{#1}[theorem]{#2}{#3}{#4}}
+\else % alle Umgebungen mit eigenem Zaehler
+   \if@envcntsect % mit section numeriert
+      \def\spn@wtheorem#1#2#3#4{\@spxnthm{#1}{#2}[section]{#3}{#4}}
+   \else % nicht mit section numeriert
+      \if@envcntreset
+         \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4}
+                                   \@addtoreset{#1}{section}}
+      \else
+         \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4}
+                                   \@addtoreset{#1}{chapter}}%
+      \fi
+   \fi
+\fi
+\spn@wtheorem{case}{Case}{\itshape}{\rmfamily}
+\spn@wtheorem{conjecture}{Conjecture}{\itshape}{\rmfamily}
+\spn@wtheorem{corollary}{Corollary}{\bfseries}{\itshape}
+\spn@wtheorem{definition}{Definition}{\bfseries}{\itshape}
+\spn@wtheorem{example}{Example}{\itshape}{\rmfamily}
+\spn@wtheorem{exercise}{Exercise}{\itshape}{\rmfamily}
+\spn@wtheorem{lemma}{Lemma}{\bfseries}{\itshape}
+\spn@wtheorem{note}{Note}{\itshape}{\rmfamily}
+\spn@wtheorem{problem}{Problem}{\itshape}{\rmfamily}
+\spn@wtheorem{property}{Property}{\itshape}{\rmfamily}
+\spn@wtheorem{proposition}{Proposition}{\bfseries}{\itshape}
+\spn@wtheorem{question}{Question}{\itshape}{\rmfamily}
+\spn@wtheorem{solution}{Solution}{\itshape}{\rmfamily}
+\spn@wtheorem{remark}{Remark}{\itshape}{\rmfamily}
+
+\def\@takefromreset#1#2{%
+    \def\@tempa{#1}%
+    \let\@tempd\@elt
+    \def\@elt##1{%
+        \def\@tempb{##1}%
+        \ifx\@tempa\@tempb\else
+            \@addtoreset{##1}{#2}%
+        \fi}%
+    \expandafter\expandafter\let\expandafter\@tempc\csname cl@#2\endcsname
+    \expandafter\def\csname cl@#2\endcsname{}%
+    \@tempc
+    \let\@elt\@tempd}
+
+\def\theopargself{\def\@spopargbegintheorem##1##2##3##4##5{\trivlist
+      \item[\hskip\labelsep{##4##1\ ##2}]{##4##3\@thmcounterend\ }##5}
+                  \def\@Opargbegintheorem##1##2##3##4{##4\trivlist
+      \item[\hskip\labelsep{##3##1}]{##3##2\@thmcounterend\ }}
+      }
+
+\renewenvironment{abstract}{%
+      \list{}{\advance\topsep by0.35cm\relax\small
+      \leftmargin=1cm
+      \labelwidth=\z@
+      \listparindent=\z@
+      \itemindent\listparindent
+      \rightmargin\leftmargin}\item[\hskip\labelsep
+                                    \bfseries\abstractname]}
+    {\endlist}
+
+\newdimen\headlineindent             % dimension for space between
+\headlineindent=1.166cm              % number and text of headings.
+
+\def\ps@headings{\let\@mkboth\@gobbletwo
+   \let\@oddfoot\@empty\let\@evenfoot\@empty
+   \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}%
+                  \leftmark\hfil}
+   \def\@oddhead{\normalfont\small\hfil\rightmark\hspace{\headlineindent}%
+                 \llap{\thepage}}
+   \def\chaptermark##1{}%
+   \def\sectionmark##1{}%
+   \def\subsectionmark##1{}}
+
+\def\ps@titlepage{\let\@mkboth\@gobbletwo
+   \let\@oddfoot\@empty\let\@evenfoot\@empty
+   \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}%
+                  \hfil}
+   \def\@oddhead{\normalfont\small\hfil\hspace{\headlineindent}%
+                 \llap{\thepage}}
+   \def\chaptermark##1{}%
+   \def\sectionmark##1{}%
+   \def\subsectionmark##1{}}
+
+\if@runhead\ps@headings\else
+\ps@empty\fi
+
+\setlength\arraycolsep{1.4\p@}
+\setlength\tabcolsep{1.4\p@}
+
+\endinput
+%end of file llncs.cls
diff -r b7e524e7ee83 -r 95df71c3df2f Pearl-jv/document/root.bib
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Pearl-jv/document/root.bib	Thu Apr 08 09:12:13 2010 +0200
@@ -0,0 +1,135 @@
+@InProceedings{GunterOsbornPopescu09,
+  author = 	 {E.L.~Gunter and C.J.~Osborn and A.~Popescu},
+  title = 	 {{T}heory {S}upport for {W}eak {H}igher {O}rder {A}bstract {S}yntax in
+                  {I}sabelle/{HOL}},
+  booktitle = 	 {Proc.~of the 4th International Workshop on Logical Frameworks and Meta-Languages: 
+                  Theory and Practice (LFMTP)},
+  pages = 	 {12--20},
+  year = 	 {2009},
+  series = 	 {ENTCS}
+}
+
+@Unpublished{SatoPollack10,
+  author = 	 {M.~Sato and R.~Pollack},
+  title = 	 {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus},
+  note = 	 {To appear in {\it Journal of Symbolic Computation}}
+}
+
+@article{GabbayPitts02,
+  author =	 {M.~J.~Gabbay and A.~M.~Pitts},
+  title =	 {{A} {N}ew {A}pproach to {A}bstract {S}yntax with {V}ariable
+                  {B}inding},
+  journal =	 {Formal Aspects of Computing},
+  volume =	 {13},
+  year =	 2002,
+  pages =	 {341--363}
+}
+
+@article{Pitts03,
+  author =	 {A.~M.~Pitts},
+  title =	 {{N}ominal {L}ogic, {A} {F}irst {O}rder {T}heory of {N}ames and
+                  {B}inding},
+  journal =	 {Information and Computation},
+  year =	 {2003},
+  volume =	 {183},
+  pages =	 {165--193}
+}
+
+@InProceedings{BengtsonParrow07,
+  author    = {J.~Bengtson and J.~Parrow},
+  title     = {Formalising the pi-{C}alculus using {N}ominal {L}ogic},
+  booktitle = {Proc.~of the 10th International Conference on
+               Foundations of Software Science and Computation Structures (FOSSACS)},
+  year      = 2007,
+  pages     = {63--77},
+  series    = {LNCS},
+  volume    = {4423}
+}
+
+@inproceedings{BengtsonParow09,
+  author    = {J.~Bengtson and J.~Parrow},
+  title     = {{P}si-{C}alculi in {I}sabelle},
+  booktitle = {Proc of the 22nd Conference on Theorem Proving in 
+               Higher Order Logics (TPHOLs)},
+  year      = 2009,
+  pages     = {99--114},
+  series    = {LNCS},
+  volume    = {5674}
+}
+
+@inproceedings{TobinHochstadtFelleisen08,
+  author    = {S.~Tobin-Hochstadt and M.~Felleisen},
+  booktitle = {Proc.~of the 35rd Symposium on
+               Principles of Programming Languages (POPL)},
+  title     = {{T}he {D}esign and {I}mplementation of {T}yped {S}cheme},
+  publisher = {ACM},
+  year      = {2008},
+  pages     = {395--406}
+}
+
+@InProceedings{UrbanCheneyBerghofer08,
+  author = "C.~Urban and J.~Cheney and S.~Berghofer",
+  title = "{M}echanizing the {M}etatheory of {LF}",
+  pages = "45--56",
+  year = 2008,
+  booktitle = "Proc.~of the 23rd IEEE Symposium on Logic in Computer Science (LICS)"
+}
+
+@InProceedings{UrbanZhu08,
+  title = "{R}evisiting {C}ut-{E}limination: {O}ne {D}ifficult {P}roof is {R}eally a {P}roof",
+  author = "C.~Urban and B.~Zhu",
+  booktitle = "Proc.~of the 9th International Conference on Rewriting Techniques 
+                     and Applications (RTA)",
+  year = "2008",
+  pages = "409--424",
+  series = "LNCS",
+  volume = 5117
+}
+
+@Article{UrbanPittsGabbay04,
+  title = "{N}ominal {U}nification",
+  author = "C.~Urban and A.M.~Pitts and M.J.~Gabbay",
+  journal = "Theoretical Computer Science",
+  pages = "473--497",
+  volume = "323",
+  number = "1-3",
+  year = "2004"
+}
+
+@Article{Church40,
+  author = 	 {A.~Church},
+  title = 	 {{A} {F}ormulation of the {S}imple {T}heory of {T}ypes},
+  journal = 	 {Journal of Symbolic Logic},
+  year = 	 {1940},
+  volume = 	 {5},
+  number = 	 {2},
+  pages = 	 {56--68}
+}
+
+
+@Manual{PittsHOL4,
+  title = 	 {{S}yntax and {S}emantics},
+  author = 	 {A.~M.~Pitts},
+  note = 	 {Part of the documentation for the HOL4 system.}
+}
+
+
+@book{PaulsonBenzmueller,
+  year={2009},
+  author={Benzm{\"u}ller, Christoph and Paulson, Lawrence C.},
+  title={Quantified Multimodal Logics in Simple Type Theory},
+  note={{http://arxiv.org/abs/0905.2435}},
+  series={{SEKI Report SR--2009--02 (ISSN 1437-4447)}},
+  publisher={{SEKI Publications}}
+}
+
+@Article{Cheney06,
+  author = 	 {J.~Cheney},
+  title = 	 {{C}ompleteness and {H}erbrand {T}heorems for {N}ominal {L}ogic},
+  journal = 	 {Journal of Symbolic Logic},
+  year = 	 {2006},
+  volume = 	 {71},
+  number = 	 {1},
+  pages = 	 {299--320}
+}
+
diff -r b7e524e7ee83 -r 95df71c3df2f Pearl-jv/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Pearl-jv/document/root.tex	Thu Apr 08 09:12:13 2010 +0200
@@ -0,0 +1,63 @@
+\documentclass{llncs}
+\usepackage{times}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{longtable}
+
+
+\usepackage{pdfsetup}
+\urlstyle{rm}
+\isabellestyle{it}
+\renewcommand{\isastyle}{\isastyleminor}
+\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
+\renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}}
+\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
+\renewcommand{\isasymequiv}{$\dn$}
+\renewcommand{\isasymiota}{}
+\renewcommand{\isasymrightleftharpoons}{}
+\renewcommand{\isasymemptyset}{$\varnothing$}
+
+\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
+
+
+\begin{document}
+
+\title{Proof Pearl: A New Foundation for Nominal Isabelle}
+\author{Brian Huffman\inst{1} and Christian Urban\inst{2}}
+\institute{Portland State University \and Technical University of Munich}
+\maketitle
+
+\begin{abstract}
+Pitts et al introduced a beautiful theory about names and binding based on the
+notions of permutation and support. The engineering challenge is to smoothly
+adapt this theory to a theorem prover environment, in our case Isabelle/HOL.
+We present a formalisation of this work that differs from our earlier approach
+in two important respects: First, instead of representing permutations as
+lists of pairs of atoms, we now use a more abstract representation based on
+functions.  Second, whereas the earlier work modeled different sorts of atoms
+using different types, we now introduce a unified atom type that includes all
+sorts of atoms. Interestingly, we allow swappings, that is permutations build from
+two atoms, to be ill-sorted.  As a result of these design changes, we can iron
+out inconveniences for the user, considerably simplify proofs and also
+drastically reduce the amount of custom ML-code. Furthermore we can extend the
+capabilities of Nominal Isabelle to deal with variables that carry additional
+information. We end up with a pleasing and formalised theory of permutations
+and support, on which we can build an improved and more powerful version of
+Nominal Isabelle.
+\end{abstract}
+
+% generated text of all theories
+\input{session}
+
+% optional bibliography
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End: