
diff -r 7b3dd407f6b3 -r 51bc795b81fd Paper/Paper.thy
--- a/Paper/Paper.thy	Sun Mar 28 22:54:38 2010 +0200
+++ b/Paper/Paper.thy	Mon Mar 29 00:30:20 2010 +0200
@@ -41,7 +41,7 @@
   \end{center}
 
   \noindent
-  where free and bound variables have names.  For such terms Nominal Isabelle
+  where free and bound variables have names.  For such alpha-equated terms,  Nominal Isabelle
   derives automatically a reasoning infrastructure that has been used
   successfully in formalisations of an equivalence checking algorithm for LF
   \cite{UrbanCheneyBerghofer08}, Typed
@@ -52,8 +52,8 @@
   binding \cite{SatoPollack10}.
 
   However, Nominal Isabelle has fared less well in a formalisation of
-  the algorithm W \cite{UrbanNipkow09}, where types and type-schemes
-  are of the form
+  the algorithm W \cite{UrbanNipkow09}, where types and type-schemes,
+  respectively, are of the form
   %
   \begin{equation}\label{tysch}
   \begin{array}{l}
@@ -171,7 +171,8 @@
   where the notation @{text "[_]._"} indicates that the @{text "x\<^isub>i"}
   become bound in @{text s}. In this representation the term 
   \mbox{@{text "\<LET> [x].s [t\<^isub>1, t\<^isub>2]"}} would be a perfectly legal
-  instance. To exclude such terms, additional predicates about well-formed
+  instance, but the lengths of two lists do not agree. To exclude such terms, 
+  additional predicates about well-formed
   terms are needed in order to ensure that the two lists are of equal
   length. This can result into very messy reasoning (see for
   example~\cite{BengtsonParow09}). To avoid this, we will allow type
@@ -190,7 +191,7 @@
   \noindent
   where @{text assn} is an auxiliary type representing a list of assignments
   and @{text bn} an auxiliary function identifying the variables to be bound
-  by the @{text "\<LET>"}. This function is defined by recursion over @{text
+  by the @{text "\<LET>"}. This function can be defined by recursion over @{text
   assn} as follows
 
   \begin{center}
@@ -238,7 +239,9 @@
   only support specifications that make sense on the level of alpha-equated
   terms (offending specifications, which for example bind a variable according
   to a variable bound somewhere else, are not excluded by Ott, but we have
-  to).  Our insistence on reasoning with alpha-equated terms comes from the
+  to).  
+
+  Our insistence on reasoning with alpha-equated terms comes from the
   wealth of experience we gained with the older version of Nominal Isabelle:
   for non-trivial properties, reasoning about alpha-equated terms is much
   easier than reasoning with raw terms. The fundamental reason for this is
@@ -311,7 +314,7 @@
   \end{center}
   
   \noindent
-  then with not too great effort we obtain a function @{text "fv\<^sup>\<alpha>"}
+  then with the help of te quotient package we obtain a function @{text "fv\<^sup>\<alpha>"}
   operating on quotients, or alpha-equivalence classes of lambda-terms. This
   lifted function is characterised by the equations
 
@@ -325,18 +328,20 @@
   (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.  Accordingly, we
+  definitions and theorems are respectful w.r.t.~alpha-equivalence.  For exmple, we
   will not be able to lift a bound-variable function, which can be defined for
-  raw terms, to alpha-equated terms
-  (since it does not respect alpha-equivalence). To sum up, every lifting of
+  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. In the paper we show that we are able to automate these
+  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
-  immeasurably helpful is what is often referred to as Core-Haskell (see
-  Figure~\ref{corehas}). There terms include patterns which include a list of
+  helpful is the term language of System @{text "F\<^isub>C"}, also known as 
+  Core-Haskell (see Figure~\ref{corehas}). This term language has patterns 
+  which 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
@@ -355,8 +360,45 @@
   have the variable convention already built in.
 
   \begin{figure}
-
-  \caption{Core Haskell.\label{corehas}}
+  \begin{boxedminipage}{\linewidth}
+  \begin{center}
+  \begin{tabular}{l}
+  Type Kinds\\
+  @{text "\<kappa> ::= \<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\\
+  Coercion Kinds\\
+  @{text "\<iota> ::= \<sigma>\<^isub>1 \<sim> \<sigma>\<^isub>2"}\\
+  Types\\
+  @{text "\<sigma> ::= a | T | \<sigma>\<^isub>1 \<sigma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<sigma>"}}$@{text "\<^sup>n"}\\
+  @{text "| \<forall>a:\<kappa>. \<sigma> "}\\
+  ??? Type equality\\
+  Coercion Types\\
+  @{text "\<gamma> ::= 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"}\\
+  Terms\\
+  @{text "e ::= 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"}\\
+  @{text "| \<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>"}\\
+  Patterns\\
+  @{text "p ::= K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "x:\<sigma>"}}$\\
+  Constants\\
+  @{text C} coercion constant\\
+  @{text T} value type constructor\\
+  @{text "S\<^isub>n"} n-ary type function\\
+  @{text K} data constructor\\
+  Variables\\
+  @{text a} type variable\\
+  @{text x} term variable\\
+  \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 issential modification by 
+  separating the grammars for type kinds and coercion types.\label{corehas}}
   \end{figure}
 *}
 
@@ -455,7 +497,7 @@
   given a free-variable function @{text "fv"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
   set"}}, then @{text x} and @{text y} need to have the same set of free
   variables; moreover there must be a permutation @{text p} such that {\it
-  ii)} it leaves the free variables of @{text x} and @{text y} unchanged, but
+  ii)} @{text p} leaves the free variables of @{text x} and @{text y} unchanged, but
   {\it iii)} ``moves'' their bound names so that we obtain modulo a relation,
   say \mbox{@{text "_ R _"}}, two equivalent terms. We also require {\it iv)} that
   @{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
@@ -463,7 +505,7 @@
   %
   \begin{equation}\label{alphaset}
   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
-  \multicolumn{2}{l}{@{term "(as, x) \<approx>gen R fv p (bs, y)"} @{text "\<equiv>"}\hspace{30mm}}\\
+  \multicolumn{2}{l}{@{term "(as, x) \<approx>gen R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}\hspace{30mm}}\\[1mm]
                & @{term "fv(x) - as = fv(y) - bs"}\\
   @{text "\<and>"} & @{term "(fv(x) - as) \<sharp>* p"}\\
   @{text "\<and>"} & @{text "(p \<bullet> x) R y"}\\
@@ -489,7 +531,7 @@
   %
   \begin{equation}\label{alphalist}
   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
-  \multicolumn{2}{l}{@{term "(as, x) \<approx>lst R fv p (bs, y)"} @{text "\<equiv>"}\hspace{30mm}}\\[1mm]
+  \multicolumn{2}{l}{@{term "(as, x) \<approx>lst R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}\hspace{30mm}}\\[1mm]
              & @{term "fv(x) - (set as) = fv(y) - (set bs)"}\\
   \wedge     & @{term "(fv(x) - set as) \<sharp>* p"}\\
   \wedge     & @{text "(p \<bullet> x) R y"}\\
@@ -507,14 +549,13 @@
   %
   \begin{equation}\label{alphares}
   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
-  \multicolumn{2}{l}{@{term "(as, x) \<approx>res R fv p (bs, y)"} @{text "\<equiv>"}\hspace{30mm}}\\[1mm]
+  \multicolumn{2}{l}{@{term "(as, x) \<approx>res R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}\hspace{30mm}}\\[1mm]
              & @{term "fv(x) - as = fv(y) - bs"}\\
   \wedge     & @{term "(fv(x) - as) \<sharp>* p"}\\
   \wedge     & @{text "(p \<bullet> x) R y"}\\
   \end{array}
   \end{equation}
 
-  \begin{exmple}\rm
   It might be useful to consider some examples for how these definitions of alpha-equivalence
   pan out in practise.
   For this consider the case of abstracting a set of variables over types (as in type-schemes). 
@@ -526,20 +567,21 @@
 
   \noindent
   Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and
-  \eqref{ex3}. It can be easily checked that @{text "({x,y}, x \<rightarrow> y)"} and
-  @{text "({y,x}, y \<rightarrow> x)"} are equal according to $\approx_{\textit{set}}$ and
+  \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and
+  @{text "({y, x}, y \<rightarrow> x)"} are equal according to $\approx_{\textit{set}}$ and
   $\approx_{\textit{res}}$ by taking @{text p} to be the swapping @{term "(x \<rightleftharpoons>
   y)"}. In case of @{text "x \<noteq> y"}, then @{text "([x, y], x \<rightarrow> y)"}
-  $\not\approx_{\textit{list}}$ @{text "([y,x], x \<rightarrow> y)"} since there is no permutation
+  $\not\approx_{\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"} since there is no permutation
   that makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and also
   leaves the type \mbox{@{text "x \<rightarrow> y"}} unchanged. Another example is
-  @{text "({x}, x)"} $\approx_{\textit{res}}$ @{text "({x,y}, x)"} which holds by 
+  @{text "({x}, x)"} $\approx_{\textit{res}}$ @{text "({x, y}, x)"} which holds by 
   taking @{text p} to be the
   identity permutation.  However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}
-  $\not\approx_{\textit{set}}$ @{text "({x,y}, x)"} since there is no permutation 
+  $\not\approx_{\textit{set}}$ @{text "({x, y}, x)"} since there is no permutation 
   that makes the
-  sets @{text "{x}"} and @{text "{x,y}"} equal (similarly for $\approx_{\textit{list}}$).
-  \end{exmple}
+  sets @{text "{x}"} and @{text "{x, y}"} equal (similarly for $\approx_{\textit{list}}$).
+  It can also relatively easily be shown that all tree notions of alpha-equivalence
+  coincide, if we only abstract a single atom. 
 
   % looks too ugly
   %\noindent
@@ -569,22 +611,26 @@
   %\end{proof}
 
 
-  In the rest of this section we are going to introduce a type- and term-constructor 
-  for abstractions. For this we define (similarly for $\approx_{\textit{abs\_list}}$ 
-  and $\approx_{\textit{abs\_res}}$)
+  In the rest of this section we are going to introduce a type- and term-constructors 
+  for abstraction. For this we define 
   %
   \begin{equation}
   @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_gen (as, x) equal supp p (bs, x)"}
   \end{equation}
   
   \noindent
-  We can show that these relations are equivalence relations and equivariant 
-  (we only show the $\approx_{\textit{abs\_set}}$-case).
+  (similarly for $\approx_{\textit{abs\_list}}$ 
+  and $\approx_{\textit{abs\_res}}$). We can show that these relations are equivalence 
+  relations and equivariant.
 
-  \begin{lemma}\label{alphaeq}
-  $\approx_{\textit{abs\_set}}$ is an equivalence
+  \begin{lemma}\label{alphaeq} The relations
+  $\approx_{\textit{abs\_set}}$,
+  $\approx_{\textit{abs\_list}}$ 
+  and $\approx_{\textit{abs\_res}}$
+  are equivalence
   relations, and if @{term "abs_set (as, x) (bs, y)"} then also
-  @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"}.
+  @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} (similarly for 
+  the other two relations).
   \end{lemma}
 
   \begin{proof}
@@ -595,29 +641,10 @@
   calculations. 
   \end{proof}
 
-  \noindent 
-  We are also define the following two auxiliary functions taking a pair
-  as argument.
-  %
-  \begin{equation}\label{aux}
-  \begin{array}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-  @{text "aux (as, x)"}      & @{text "\<equiv>"} & @{text "supp x - as"}\\
-  @{text "aux_list (bs, x)"} & @{text "\<equiv>"} & @{text "supp x - set bs"}
-  \end{array}
-  \end{equation}
-  
   \noindent
-  The point of these two functions is that they are preserved under
-  alpha-equivalence, that means for instance
-  %
-  \begin{equation}\label{auxpreserved}
-  @{term "abs_set (as, x) (bs, y)"} \;\;\text{implies}\;\; 
-  @{term "aux (as, x) = aux (bs, y)"}
-  \end{equation}
-
-  Lemma \ref{alphaeq} allows us to use our quotient package and introduce 
+  This lemma allows us to use our quotient package and introduce 
   new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}
-  representing the alpha-equivalence classes. Elements in these types 
+  representing alpha-equivalence classes of pairs. The elements in these types 
   we will, respectively, write as:
 
   \begin{center}
@@ -627,31 +654,71 @@
   \end{center}
 
   \noindent
-  By definition we have 
+  indicating that a set or list is abstracted in @{text x}. We will call the types
+  \emph{abstraction types} and their elements \emph{abstractions}. The important 
+  property we need is a characterisation for the support of abstractions, namely
 
+  \begin{thm}[Support of Abstractions]\label{suppabs} 
+  Assuming @{text x} has finite support, then 
   \begin{center}
-  @{thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;iff\; 
-  @{thm (rhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}
+  \begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+  @{thm (lhs) supp_abs(1)[no_vars]} & $=$ & @{thm (rhs) supp_abs(1)[no_vars]}\\
+  @{thm (lhs) supp_abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_abs(2)[no_vars]}\\
+  @{thm (lhs) supp_abs(3)[no_vars]} & $=$ & @{thm (rhs) supp_abs(3)[no_vars]}
+  \end{tabular}
   \end{center}
-
+  \end{thm}
 
   \noindent
-  The following lemma (and similar ones for $\approx_{\textit{abs\_list}}$ and 
-  $\approx_{\textit{abs\_res}}$) will be crucial below: 
+  We will only show in the rest of the section the first equation, as the others 
+  follow similar arguments. By definition of the abstraction type @{text "abs_set"} 
+  we have 
+  %
+  \begin{equation}\label{abseqiff}
+  @{thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\text{if and only if}\; 
+  @{thm (rhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}
+  \end{equation}
+
+  \noindent
+  With this, we can show the following lemma about swapping two atoms (the permutation 
+  operation for abstractions is the one lifted for pairs).\footnote{metion this in the nominal 
+  logic section} 
 
   \begin{lemma}
   @{thm[mode=IfThen] abs_swap1(1)[no_vars]}
   \end{lemma}
 
   \begin{proof}
-  This lemma is straightforward by observing that the assumptions give us
+  By using \eqref{abseqiff}, this lemma is straightforward when observing that 
+  the assumptions give us
   @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - bs) = (supp x - bs)"} and that @{text supp}
-  is equivariant.
+  and set difference are equivariant.
   \end{proof}
 
+  \noindent
+  This lemma gives us
+  %
+  \begin{equation}\label{halfone}
+  @{thm abs_supports(1)[no_vars]}
+  \end{equation}
+  
+  \noindent
+  which with \ref{} gives us one half of Thm~\ref{suppabs}. The other half is 
+  a bit more involved. We first define an auxiliary function
+  %
+  \begin{center}
+  @{thm supp_res.simps[THEN eq_reflection, no_vars]}
+  \end{center}
+  
+
   \begin{lemma}
   $supp ([as]set. x) = supp x - as$ 
   \end{lemma}
+
+  \noindent
+  The point of these general lemmas about pairs is that we can define and prove properties 
+  about them conveninently on the Isabelle level, and in addition can use them in what
+  follows next when we have to deal with specific instances of term-specification. 
 *}
 
 section {* Alpha-Equivalence and Free Variables *}




