
diff -r fb4be1983a71 -r 6f669bba4f0c Paper/Paper.thy
--- a/Paper/Paper.thy	Mon Mar 29 16:44:05 2010 +0200
+++ b/Paper/Paper.thy	Mon Mar 29 16:44:26 2010 +0200
@@ -13,7 +13,7 @@
 notation (latex output)
   swap ("'(_ _')" [1000, 1000] 1000) and
   fresh ("_ # _" [51, 51] 50) and
-  fresh_star ("_ #* _" [51, 51] 50) and
+  fresh_star ("_ #\<^sup>* _" [51, 51] 50) and
   supp ("supp _" [78] 73) and
   uminus ("-_" [78] 73) and
   If  ("if _ then _ else _" 10) and
@@ -47,7 +47,7 @@
   successfully in formalisations of an equivalence checking algorithm for LF
   \cite{UrbanCheneyBerghofer08}, Typed
   Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
-  \cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result
+  \cite{BengtsonParow09} 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}.
@@ -328,27 +328,24 @@
   \noindent
   (Note that this means also the term-constructors for variables, applications
   and lambda are lifted to the quotient level.)  This construction, of course,
-  only works if alpha-equivalence is indeed an equivalence relation, and the lifted
-  definitions and theorems are respectful w.r.t.~alpha-equivalence.  For example, we
-  will not be able to lift a bound-variable function, which can be defined for
-  raw terms. The reason is that this function does not respect alpha-equivalence. 
-  To sum up, every lifting of
-  theorems to the quotient level needs proofs of some respectfulness
-  properties (see \cite{Homeier05}). In the paper we show that we are able to 
-  automate these
-  proofs and therefore can establish a reasoning infrastructure for
-  alpha-equated terms.
+  only works if alpha-equivalence is indeed an equivalence relation, and the
+  lifted definitions and theorems are respectful w.r.t.~alpha-equivalence.
+  For example, we will not be able to lift a bound-variable function. Although
+  this function can be defined for raw terms, it does not respect
+  alpha-equivalence and therefore cannot be lifted. To sum up, every lifting
+  of theorems to the quotient level needs proofs of some respectfulness
+  properties (see \cite{Homeier05}). In the paper we show that we are able to
+  automate these proofs and therefore can establish a reasoning infrastructure
+  for alpha-equated terms.
 
   The examples we have in mind where our reasoning infrastructure will be
-  helpful includes the term language of System @{text "F\<^isub>C"}, also known as 
-  Core-Haskell (see Figure~\ref{corehas}). This term language involves patterns 
-  that include lists of
-  type- and term- variables (the arguments of constructors) all of which are
-  bound in case expressions. One difficulty is that each of these variables
-  come with a kind or type annotation. Representing such binders with single
-  binders and reasoning about them in a theorem prover would be a major pain.
-  \medskip
-
+  helpful includes the term language of System @{text "F\<^isub>C"}, also
+  known as Core-Haskell (see Figure~\ref{corehas}). This term language
+  involves patterns that have lists of type- and term-variables (the
+  arguments of constructors) all of which are bound in case expressions. One
+  difficulty is that each of these variables come with a kind or type
+  annotation. Representing such binders with single binders and reasoning
+  about them in a theorem prover would be a major pain.  \medskip
 
   \noindent
   {\bf Contributions:}  We provide new definitions for when terms
@@ -369,35 +366,35 @@
   \multicolumn{3}{@ {}l}{Coercion Kinds}\\
   @{text "\<iota>"} & @{text "::="} & @{text "\<sigma>\<^isub>1 \<sim> \<sigma>\<^isub>2"}\medskip\\
   \multicolumn{3}{@ {}l}{Types}\\
-  @{text "\<sigma>"} & @{text "::="} & @{text "a | T | \<sigma>\<^isub>1 \<sigma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<sigma>"}}$@{text "\<^sup>n"}\\
-              & & @{text "| \<forall>a:\<kappa>. \<sigma> "}\\
-              & & ??? Type equality\medskip\\
+  @{text "\<sigma>"} & @{text "::="} & @{text "a | T | \<sigma>\<^isub>1 \<sigma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<sigma>"}}$@{text "\<^sup>n"} 
+  @{text "| \<forall>a:\<kappa>. \<sigma> | \<iota> \<Rightarrow> \<sigma>"}\medskip\\
   \multicolumn{3}{@ {}l}{Coercion Types}\\
-  @{text "\<gamma>"} & @{text "::="} & @{text "a | C | S\<^isub>n"}$\;\overline{@{text "\<gamma>"}}$@{text "\<^sup>n"}\\
-  & & @{text "| \<forall>a:\<iota>. \<gamma>"}\\
-  & & ??? Coercion Type equality\\
-  & & @{text "| sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2 | left \<gamma> | right \<gamma> | \<gamma>\<^isub>1 \<sim> \<gamma>\<^isub>2 "}\\
-  & & @{text "| rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\medskip\\
+  @{text "\<gamma>"} & @{text "::="} & @{text "c | C | \<gamma>\<^isub>1 \<gamma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<gamma>"}}$@{text "\<^sup>n"}
+  @{text "| \<forall>c:\<iota>. \<gamma> | \<iota> \<Rightarrow> \<gamma> |"}\\
+  & & @{text "refl \<sigma> | sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2 | \<gamma> @ \<sigma> |"}\\
+  & & @{text "left \<gamma> | right \<gamma> | \<gamma>\<^isub>1 \<sim> \<gamma>\<^isub>2 |"}\\
+  & & @{text "rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\medskip\\
   \multicolumn{3}{@ {}l}{Terms}\\
-  @{text "e"} & @{text "::="} & @{text "x | K | \<Lambda>a:\<kappa>. e | \<Lambda>a:\<iota>. e | e \<sigma> | e \<gamma> |"}\\
-  & & @{text "\<lambda>x:\<sigma>.e | e\<^isub>1 e\<^isub>2 | \<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2 |"}\\
+  @{text "e"} & @{text "::="} & @{text "x | K | \<Lambda>a:\<kappa>. e | \<Lambda>c:\<iota>. e | e \<sigma> | e \<gamma> |"}\\
+  & & @{text "\<lambda>x:\<sigma>. e | e\<^isub>1 e\<^isub>2 | \<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2 |"}\\
   & & @{text "\<CASE> e\<^isub>1 \<OF>"}$\;\overline{@{text "p \<rightarrow> e\<^isub>2"}}$ @{text "| e \<triangleright> \<gamma>"}\medskip\\
   \multicolumn{3}{@ {}l}{Patterns}\\
-  @{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "a:\<iota>"}}\;\overline{@{text "x:\<sigma>"}}$\medskip\\
+  @{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "c:\<iota>"}}\;\overline{@{text "x:\<sigma>"}}$\medskip\\
   \multicolumn{3}{@ {}l}{Constants}\\
-  @{text C} & & coercion constant\\
-  @{text T} & & value type constructor\\
-  @{text "S\<^isub>n"} & & n-ary type function\\
-  @{text K} & & data constructor\medskip\\
+  @{text C} & & coercion constants\\
+  @{text T} & & value type constructors\\
+  @{text "S\<^isub>n"} & & n-ary type functions\\
+  @{text K} & & data constructors\medskip\\
   \multicolumn{3}{@ {}l}{Variables}\\
-  @{text a} & & type variable\\
-  @{text x} & & term variable\\
+  @{text a} & & type variables\\
+  @{text c} & & coercion variables\\
+  @{text x} & & term variables\\
   \end{tabular}
   \end{center}
   \end{boxedminipage}
-  \caption{The term-language of System @{text "F\<^isub>C"}, also often referred to as Core-Haskell, 
-  according to \cite{CoreHaskell}. We only made an inessential modification by 
-  separating the grammars for type kinds and coercion types.\label{corehas}}
+  \caption{The term-language of System @{text "F\<^isub>C"}, also often referred to as \emph{Core-Haskell}
+   \cite{CoreHaskell}. In this version of Core-Haskell we made a modification by 
+  separating completely the grammars for type kinds and coercion types.\label{corehas}}
   \end{figure}
 *}
 
@@ -406,13 +403,16 @@
 text {*
   At its core, Nominal Isabelle is an adaption of the nominal logic work by
   Pitts \cite{Pitts03}. This adaptation for Isabelle/HOL is described in
-  \cite{HuffmanUrban10} (including proofs), which we review here briefly to aid the description
-  of what follows. Two central notions in the nominal logic work are sorted
-  atoms and sort-respecting permutations of atoms. The sorts can be used to
-  represent different kinds of variables, such as the term- and type-variables in
-  Core-Haskell, and it is assumed that there is an infinite supply of atoms
-  for each sort. However, in order to simplify the description, we shall
-  assume in what follows that there is only one sort of atoms.
+  \cite{HuffmanUrban10} (including proofs). We shall briefly review this work
+  to aid the description of what follows. 
+
+  Two central notions in the nominal
+  logic work are sorted atoms and sort-respecting permutations of atoms. The
+  sorts can be used to represent different kinds of variables, such as the
+  term- and type-variables in Core-Haskell, and it is assumed that there is an
+  infinite supply of atoms for each sort. However, in order to simplify the
+  description, we shall assume in what follows that there is only one sort of
+  atoms.
 
   Permutations are bijective functions from atoms to atoms that are 
   the identity everywhere except on a finite number of atoms. There is a 
@@ -422,14 +422,15 @@
 
   \noindent 
   in which the generic type @{text "\<beta>"} stands for the type of the object 
-  on which the permutation 
+  over which the permutation 
   acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},
   the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}}, 
   and the inverse permutation of @{term p} as @{text "- p"}. The permutation
-  operation is defined for products, lists, sets, functions, booleans etc (see \cite{HuffmanUrban10})
+  operation is defined by induction over the type-hierarchy, for example as follows 
+  for products, lists, sets, functions and booleans (see \cite{HuffmanUrban10}):
   
-  \begin{center}
-  \begin{tabular}{@ {}cc@ {}}
+  \begin{equation}
+  \mbox{\begin{tabular}{@ {}cc@ {}}
   \begin{tabular}{@ {}l@ {}}
   @{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm]
   @{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\
@@ -437,16 +438,15 @@
   \end{tabular} &
   \begin{tabular}{@ {}l@ {}}
   @{thm permute_set_eq[no_vars, THEN eq_reflection]}\\
-  @{text "p \<bullet> (f x) \<equiv> (p \<bullet> f) (p \<bullet> x)"}\\
+  @{text "p \<bullet> f \<equiv> \<lambda>x. p \<bullet> (f (- p \<bullet> x))"}\\
   @{thm permute_bool_def[no_vars, THEN eq_reflection]}\\
   \end{tabular}
-  \end{tabular}
-  \end{center}
+  \end{tabular}}
+  \end{equation}
 
   \noindent
-  Concrete  permutations are build up from 
-  swappings, written as @{text "(a b)"},
-  which are permutations that behave as follows:
+  Concrete permutations are build up from swappings, written as @{text "(a
+  b)"}, which are permutations that behave as follows:
   %
   @{text[display,indent=5] "(a b) = \<lambda>c. if a = c then b else if b = c then a else c"}
   
@@ -493,9 +493,8 @@
   
   \noindent 
   it can sometimes be difficult to establish the support precisely,
-  and only give an over approximation (see functions above). This
-  over approximation can be formalised with the notions \emph{supports},
-  defined as follows.
+  and only give an approximation (see functions above). Such approximations can 
+  be formalised with the notion \emph{supports}, defined as follows.
 
   \begin{defn}
   A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}
@@ -503,7 +502,7 @@
   \end{defn}
 
   \noindent
-  The point of this definitions is that we can show:
+  The point of this definition is that we can show:
 
   \begin{property}
   {\it i)} @{thm[mode=IfThen] supp_is_subset[no_vars]} 
@@ -512,6 +511,19 @@
 
   \noindent
   Another important notion in the nominal logic work is \emph{equivariance}.
+  For a function @{text f}, lets say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant 
+  means that every permutation leaves @{text f} unchanged, or equivalently that
+  a permutation applied to an application @{text "f x"} can be moved to its 
+  arguments. That is
+
+  \begin{center}
+  @{text "\<forall>p. p \<bullet> f = f"} \hspace{5mm}
+  @{text "\<forall>p. p \<bullet> (f x) = f (p \<bullet> x)"}
+  \end{center}
+ 
+  \noindent
+  From the first equation we can be easily deduce that an equivariant function has
+  empty support.
 
   %\begin{property}
   %@{thm[mode=IfThen] at_set_avoiding[no_vars]}




