
diff -r 8c0eef2b84e7 -r 44a5edac90ad Paper/Paper.thy
--- a/Paper/Paper.thy	Mon Mar 29 01:23:24 2010 +0200
+++ b/Paper/Paper.thy	Mon Mar 29 11:23:29 2010 +0200
@@ -26,7 +26,8 @@
   alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and 
   Abs ("[_]\<^raw:$\!$>\<^bsub>set\<^esub>._") and
   Abs_lst ("[_]\<^raw:$\!$>\<^bsub>list\<^esub>._") and
-  Abs_res ("[_]\<^raw:$\!$>\<^bsub>res\<^esub>._") 
+  Abs_res ("[_]\<^raw:$\!$>\<^bsub>res\<^esub>._") and
+  Cons ("_::_" [78,77] 73)
 (*>*)
 
 
@@ -52,8 +53,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,
-  respectively, are of the form
+  the algorithm W \cite{UrbanNipkow09}, where types and type-schemes are,
+  respectively, of the form
   %
   \begin{equation}\label{tysch}
   \begin{array}{l}
@@ -128,7 +129,7 @@
 
   However, we found that this is still not sufficient for dealing with
   language constructs frequently occurring in programming language
-  research. For example in @{text "\<LET>"}s containing patterns
+  research. For example in @{text "\<LET>"}s containing patterns like
   %
   \begin{equation}\label{two}
   @{text "\<LET> (x, y) = (3, 2) \<IN> x - y \<END>"}
@@ -170,7 +171,7 @@
   \noindent
   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
+  \mbox{@{text "\<LET> [x].s [t\<^isub>1, t\<^isub>2]"}} is a perfectly legal
   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
@@ -227,8 +228,8 @@
   infrastructure in Isabelle/HOL for
   \emph{non}-alpha-equated, or ``raw'', terms. While our alpha-equated terms
   and the raw terms produced by Ott use names for bound variables,
-  there is a key difference: working with alpha-equated terms means that the
-  two type-schemes (with $x$, $y$ and $z$ being distinct)
+  there is a key difference: working with alpha-equated terms means, for example,  
+  that the two type-schemes (with $x$, $y$ and $z$ being distinct)
 
   \begin{center}
   @{text "\<forall>{x}. x \<rightarrow> y  = \<forall>{x, z}. x \<rightarrow> y"} 
@@ -288,7 +289,7 @@
   the type of sets of raw terms according to our alpha-equivalence relation
   and finally define the new type as these alpha-equivalence classes
   (non-emptiness is satisfied whenever the raw terms are definable as datatype
-  in Isabelle/HOL and the fact that our relation for alpha-equivalence is
+  in Isabelle/HOL and the property that our relation for alpha-equivalence is
   indeed an equivalence relation).
 
   The fact that we obtain an isomorphism between the new type and the
@@ -314,7 +315,7 @@
   \end{center}
   
   \noindent
-  then with the help of te quotient package we obtain a function @{text "fv\<^sup>\<alpha>"}
+  then with the help of the 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
 
@@ -339,9 +340,9 @@
   alpha-equated terms.
 
   The examples we have in mind where our reasoning infrastructure will be
-  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
+  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
@@ -362,37 +363,35 @@
   \begin{figure}
   \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\\
+  \begin{tabular}{rcl}
+  \multicolumn{3}{@ {}l}{Type Kinds}\\
+  @{text "\<kappa>"} & @{text "::="} & @{text "\<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\medskip\\
+  \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\\
+  \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\\
+  \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 "\<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 "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\\
+  \multicolumn{3}{@ {}l}{Variables}\\
+  @{text a} & & type variable\\
+  @{text x} & & term variable\\
   \end{tabular}
   \end{center}
   \end{boxedminipage}
@@ -407,10 +406,10 @@
 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}, which we review here briefly to aid the description
+  \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 term- and type-variables in
+  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.
@@ -425,16 +424,32 @@
   in which the generic type @{text "\<beta>"} stands for the type of the object 
   on 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"}} 
+  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}). Concrete  permutations are build up from 
+  operation is defined for products, lists, sets, functions, booleans etc (see \cite{HuffmanUrban10})
+  
+  \begin{center}
+  \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]}\\
+  @{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\
+  \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)"}\\
+  @{thm permute_bool_def[no_vars, THEN eq_reflection]}\\
+  \end{tabular}
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  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"}
   
-
   The most original aspect of the nominal logic work of Pitts is a general
   definition for the notion of ``the set of free variables of an object @{text
   "x"}''.  This notion, written @{term "supp x"}, is general in the sense that
@@ -465,7 +480,24 @@
   \end{property}
 
   \noindent
-  For a proof see \cite{HuffmanUrban10}.
+  While it is often clear what the support for a construction is, for
+  example
+  %
+  \begin{eqnarray}
+  @{term "supp (x, y)"} & = & @{term "supp x \<union> supp y"}\\
+  @{term "supp []"} & = & @{term "{}"}\\
+  @{term "supp (x#xs)"} & = & @{term "supp (x, xs)"}\\
+  @{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp (f, x)"}\\
+  @{term "supp b"} & = & @{term "{}"}
+  \end{eqnarray}
+  
+  \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:
+  
+
 
   %\begin{property}
   %@{thm[mode=IfThen] at_set_avoiding[no_vars]}




