nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:8c0eef2b84e7
+:44a5edac90ad
 fv ("fv'(_')" [100] 100) and
 equal ("=") and
 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)
 (*>*)
 section {* Introduction *}
 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}.
 However, Nominal Isabelle has fared less well in a formalisation of
-the algorithm W \cite{UrbanNipkow09}, where types and type-schemes,
+the algorithm W \cite{UrbanNipkow09}, where types and type-schemes are,
-respectively, are of the form
+respectively, of the form
 %
 \begin{equation}\label{tysch}
 \begin{array}{l}
 @{text "T ::= x | T \<rightarrow> T"}\hspace{5mm}
 @{text "S ::= \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. T"}
 which the order of binders does not matter, but the ``cardinality'' of the
 binders has to agree.
 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>"}
 \end{equation}
 \end{center}
 \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
 length. This can result into very messy reasoning (see for
 example~\cite{BengtsonParow09}). To avoid this, we will allow type
 Another reason is that we establish the reasoning infrastructure
 for alpha-\emph{equated} terms. In contrast, Ott produces  a reasoning
 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
+there is a key difference: working with alpha-equated terms means, for example,
-two type-schemes (with $x$, $y$ and $z$ being distinct)
+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"}
 \end{center}
 We take as the starting point a definition of raw terms (defined as a
 datatype in Isabelle/HOL); identify then the alpha-equivalence classes in
 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
 non-empty subset shows that the new type is a faithful representation of
 alpha-equated terms. That is not the case for example for terms using the
 @{text "fv(t\<^isub>1 t\<^isub>2) = fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\\[1mm]
 @{text "fv(\<lambda>x.t) = fv(t) - {x}"}
 \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
 \begin{center}
 @{text "fv\<^sup>\<alpha>(x) = {x}"}\hspace{10mm}
 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 is the term language of System @{text "F\<^isub>C"}, also known as
+helpful includes the term language of System @{text "F\<^isub>C"}, also known as
-Core-Haskell (see Figure~\ref{corehas}). This term language has patterns
+Core-Haskell (see Figure~\ref{corehas}). This term language involves patterns
-which include lists of
+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
 have the variable convention already built in.
 \begin{figure}
 \begin{boxedminipage}{\linewidth}
 \begin{center}
-\begin{tabular}{l}
+\begin{tabular}{rcl}
-Type Kinds\\
+\multicolumn{3}{@ {}l}{Type Kinds}\\
-@{text "\<kappa> ::= \<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\\
+@{text "\<kappa>"} & @{text "::="} & @{text "\<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\medskip\\
-Coercion Kinds\\
+\multicolumn{3}{@ {}l}{Coercion Kinds}\\
-@{text "\<iota> ::= \<sigma>\<^isub>1 \<sim> \<sigma>\<^isub>2"}\\
+@{text "\<iota>"} & @{text "::="} & @{text "\<sigma>\<^isub>1 \<sim> \<sigma>\<^isub>2"}\medskip\\
-Types\\
+\multicolumn{3}{@ {}l}{Types}\\
-@{text "\<sigma> ::= a | T | \<sigma>\<^isub>1 \<sigma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<sigma>"}}$@{text "\<^sup>n"}\\
+@{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> "}\\
+& & @{text "| \<forall>a:\<kappa>. \<sigma> "}\\
-??? Type equality\\
+& & ??? Type equality\medskip\\
-Coercion Types\\
+\multicolumn{3}{@ {}l}{Coercion Types}\\
-@{text "\<gamma> ::= a | C | S\<^isub>n"}$\;\overline{@{text "\<gamma>"}}$@{text "\<^sup>n"}\\
+@{text "\<gamma>"} & @{text "::="} & @{text "a | C | S\<^isub>n"}$\;\overline{@{text "\<gamma>"}}$@{text "\<^sup>n"}\\
-@{text "| \<forall>a:\<iota>. \<gamma>"}\\
+& & @{text "| \<forall>a:\<iota>. \<gamma>"}\\
-??? Coercion Type equality\\
+& & ??? 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 "| 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"}\\
+& & @{text "| rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\medskip\\
-Terms\\
+\multicolumn{3}{@ {}l}{Terms}\\
-@{text "e ::= x | K | \<Lambda>a:\<kappa>. e | \<Lambda>a:\<iota>. e | e \<sigma> | e \<gamma>"}\\
+@{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"}\\
+& & @{text "\<lambda>x:\<sigma>.e | e\<^isub>1 e\<^isub>2 | \<LET> x:\<sigma> = e\<^isub>1 \<IN> 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>"}\medskip\\
-@{text "| \<CASE> e\<^isub>1 \<OF>"}$\;\overline{@{text "p \<rightarrow> e\<^isub>2"}}$\\
+\multicolumn{3}{@ {}l}{Patterns}\\
-@{text "| e \<triangleright> \<gamma>"}\\
+@{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "x:\<sigma>"}}$\medskip\\
-Patterns\\
+\multicolumn{3}{@ {}l}{Constants}\\
-@{text "p ::= K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "x:\<sigma>"}}$\\
+@{text C} & & coercion constant\\
-Constants\\
+@{text T} & & value type constructor\\
-@{text C} coercion constant\\
+@{text "S\<^isub>n"} & & n-ary type function\\
-@{text T} value type constructor\\
+@{text K} & & data constructor\medskip\\
-@{text "S\<^isub>n"} n-ary type function\\
+\multicolumn{3}{@ {}l}{Variables}\\
-@{text K} data constructor\\
+@{text a} & & type variable\\
-Variables\\
+@{text x} & & term variable\\
-@{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
 section {* A Short Review of the Nominal Logic Work *}
 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.
 Permutations are bijective functions from atoms to atoms that are
 \noindent
 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
+operation is defined for products, lists, sets, functions, booleans etc (see \cite{HuffmanUrban10})
-(see \cite{HuffmanUrban10}). Concrete  permutations are build up from
+\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
 it applies not only to lambda-terms (alpha-equated or not), but also to lists,
 products, sets and even functions. The definition depends only on the
 \begin{property}
 @{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
 \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]}
 %\end{property}

changeset 1690	44a5edac90ad
parent 1687	51bc795b81fd
child 1693	3668b389edf3