# HG changeset patch # User Christian Urban # Date 1315477263 -3600 # Node ID 02d98590454da6a39f08d0bb053ad8c641c26f22 # Parent 8d7d85e915b5f7f027d085ca361161c0d088ade5 more on the paper diff -r 8d7d85e915b5 -r 02d98590454d LMCS-Paper/Paper.thy --- a/LMCS-Paper/Paper.thy Wed Sep 07 12:38:32 2011 +0100 +++ b/LMCS-Paper/Paper.thy Thu Sep 08 11:21:03 2011 +0100 @@ -30,6 +30,8 @@ fv ("fa'(_')" [100] 100) and equal ("=") and alpha_abs_set ("_ \\<^raw:{$\,_{\textit{abs\_set}}$}> _") and + alpha_abs_lst ("_ \\<^raw:{$\,_{\textit{abs\_list}}$}> _") and + alpha_abs_res ("_ \\<^raw:{$\,_{\textit{abs\_set+}}$}> _") and Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and Abs_lst ("[_]\<^bsub>list\<^esub>._") and Abs_dist ("[_]\<^bsub>#list\<^esub>._") and @@ -94,7 +96,7 @@ binders by iterating single binders, this leads to a rather clumsy formalisation of W. The need of iterating single binders is also one reason why Nominal Isabelle and similar theorem provers that only provide - mechanisms for binding single variables has not fared extremely well with + mechanisms for binding single variables have not fared extremely well with the more advanced tasks in the POPLmark challenge \cite{challenge05}, because also there one would like to bind multiple variables at once. @@ -123,8 +125,8 @@ give a general binding mechanism and associated notion of alpha-equivalence that can be used to faithfully represent this kind of binding in Nominal Isabelle. The difficulty of finding the right notion for alpha-equivalence - can be appreciated in this case by considering that the definition given by - Leroy in \cite[Page 18--19]{Leroy92} is incorrect (it omits a side-condition). + can be appreciated in this case by considering that the definition given for + type-schemes by Leroy in \cite[Page 18--19]{Leroy92} is incorrect (it omits a side-condition). However, the notion of alpha-equivalence that is preserved by vacuous binders is not always wanted. For example in terms like @@ -361,7 +363,7 @@ Figure~\ref{corehas}). This term language involves patterns that have lists of type-, coercion- and term-variables, all of which are bound in @{text "\"}-expressions. In these patterns we do not know in advance how many - variables need to be bound. Another example is the algorithm W + variables need to be bound. Another example is the algorithm W, which includes multiple binders in type-schemes.\medskip \noindent @@ -432,7 +434,7 @@ Two central notions in the nominal logic work are sorted atoms and sort-respecting permutations of atoms. We will use the letters @{text "a, b, - c, \"} to stand for atoms and @{text "\, \"} to stand for permutations, + c, \"} to stand for atoms and @{text "\, \\<^isub>1, \"} to stand for permutations, which in Nominal Isabelle have type @{typ perm}. The purpose of atoms is to represent variables, be they bound or free. The sorts of atoms can be used to represent different kinds of variables, such as the term-, coercion- and @@ -449,7 +451,7 @@ acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"}, the composition of two permutations @{term "\\<^isub>1"} and @{term "\\<^isub>2"} as \mbox{@{term "\\<^isub>1 + \\<^isub>2"}}, and the inverse permutation of @{term "\"} as @{text "- \"}. The permutation - operation is defined over the type-hierarchy \cite{HuffmanUrban10}; + operation is defined over Isabelle/HOL's type-hierarchy \cite{HuffmanUrban10}; for example permutations acting on products, lists, sets, functions and booleans are given by: @@ -610,7 +612,9 @@ as long as it is finitely supported) and also @{text "\"} does not affect anything in the support of @{text x} (that is @{term "supp x \* \"}). The last fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders - @{text as} in @{text x}, because @{term "\ \ x = x"}. + @{text as} in @{text x}, because @{term "\ \ x = x"}. Note that @{term "supp x \* \"} + is equivalent with @{term "supp \ \* x"}, which means we could also use the other + `direction' in Propositions \ref{supppermeq} and \ref{avoiding}. Most properties given in this section are described in detail in \cite{HuffmanUrban10} and all are formalised in Isabelle/HOL. In the next sections we will make @@ -732,15 +736,15 @@ abstract a single atom. In the rest of this section we are going to introduce three abstraction - types. For this we define + types. For this we define the relations \begin{equation} - \begin{array}{l} - @{term "abs_set (as, x) (bs, x) \ \\. alpha_set (as, x) equal supp \ (bs, x)"}\\ - @{term "abs_res (as, x) (bs, x) \ \\. alpha_res (as, x) equal supp \ (bs, x)"}\\ - @{term "abs_lst (as, x) (bs, x) \ \\. alpha_lst (as, x) equal supp \ (bs, x)"}\\ + \begin{array}{r} + @{term "alpha_abs_set (as, x) (bs, y) \ \\. alpha_set (as, x) equal supp \ (bs, y)"}\\ + @{term "alpha_abs_res (as, x) (bs, y) \ \\. alpha_res (as, x) equal supp \ (bs, y)"}\\ + @{term "alpha_abs_lst (as, x) (bs, y) \ \\. alpha_lst (as, x) equal supp \ (bs, y)"}\\ \end{array} - \end{equation} + \end{equation}\smallskip \noindent We can show that these relations are equivalence @@ -748,32 +752,35 @@ \begin{lem}\label{alphaeq} The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$ - and $\approx_{\,\textit{abs\_set+}}$ are equivalence relations. %, and if + and $\approx_{\,\textit{abs\_set+}}$ are equivalence relations and equivariant. + %, and if %@{term "abs_set (as, x) (bs, y)"} then also %@{term "abs_set (p \ as, p \ x) (p \ bs, p \ y)"} (similarly for the other two relations). \end{lem} \begin{proof} Reflexivity is by taking @{text "\"} to be @{text "0"}. For symmetry we have - a permutation @{text p} and for the proof obligation take @{term "- \"}. In case + a permutation @{text "\"} and for the proof obligation take @{term "- \"}. In case of transitivity, we have two permutations @{text "\\<^isub>1"} and @{text "\\<^isub>2"}, and for the - proof obligation use @{text "\\<^isub>1 + \\<^isub>2"}. All conditions are then by simple - calculations. + proof obligation use @{text "\\<^isub>1 + \\<^isub>2"}. Equivariance means + @{term "abs_set (p \ as, p \ x) (p \ bs, p \ y)"} holds provided + @{term "abs_set (as, x) (bs, y)"}. + \end{proof} \noindent This lemma allows us to use our quotient package for introducing - new types @{text "\ abs_set"}, @{text "\ abs_set+"} and @{text "\ abs_list"} + new types @{text "\ abs\<^bsub>set\<^esub>"}, @{text "\ abs\<^bsub>set+\<^esub>"} and @{text "\ abs\<^bsub>list\<^esub>"} representing alpha-equivalence classes of pairs of type @{text "(atom set) \ \"} (in the first two cases) and of type @{text "(atom list) \ \"} (in the third case). The elements in these types will be, respectively, written as - \begin{center} - @{term "Abs_set as x"}, \hspace{5mm} - @{term "Abs_res as x"} and \hspace{5mm} - @{term "Abs_lst as x"}, - \end{center} + \[ + @{term "Abs_set as x"} \hspace{10mm} + @{term "Abs_res as x"} \hspace{10mm} + @{term "Abs_lst as x"} + \]\smallskip \noindent indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will @@ -784,37 +791,33 @@ \begin{thm}[Support of Abstractions]\label{suppabs} Assuming @{text x} has finite support, then - \begin{center} - \begin{tabular}{l} - @{thm (lhs) supp_Abs(1)[no_vars]} $\;\;=\;\;$ - @{thm (lhs) supp_Abs(2)[no_vars]} $\;\;=\;\;$ @{thm (rhs) supp_Abs(2)[no_vars]}, and\\ - @{thm (lhs) supp_Abs(3)[where bs="bs", no_vars]} $\;\;=\;\;$ - @{thm (rhs) supp_Abs(3)[where bs="bs", no_vars]} - \end{tabular} - \end{center} + \[ + \begin{array}{l@ {\;=\;}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)[where bs="as", no_vars]} & + @{thm (rhs) supp_Abs(3)[where bs="as", no_vars]}\\ + \end{array} + \]\smallskip \end{thm} \noindent This theorem states that the bound names do not appear in the support. - For brevity we omit the proof and again refer the reader to - our formalisation in Isabelle/HOL. + Below we will show the first equation. The others follow by similar + arguments. By definition of the abstraction type @{text "abs\<^bsub>set\<^esub>"} we have - \noindent - Below we will show the first equation. The others - follow by 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} + @{term "\\. alpha_set (as, x) equal supp \ (bs, y)"} + \end{equation}\smallskip \noindent and also \begin{equation}\label{absperm} - @{thm permute_Abs[no_vars]} - \end{equation} + @{thm permute_Abs(1)[where p="\", no_vars]} + \end{equation}\smallskip \noindent The second fact derives from the definition of permutations acting on pairs diff -r 8d7d85e915b5 -r 02d98590454d LMCS-Paper/document/root.tex --- a/LMCS-Paper/document/root.tex Wed Sep 07 12:38:32 2011 +0100 +++ b/LMCS-Paper/document/root.tex Thu Sep 08 11:21:03 2011 +0100 @@ -75,7 +75,7 @@ \email{kaliszyk@score.cs.tsukuba.ac.jp} \thanks{$^\star$~This is a revised and expanded version of~\cite{UrbanKaliszyk11}} -\keywords{Nominal Isabelle, variable convention, theorem provers, formal reasoning} +\keywords{Nominal Isabelle, variable convention, theorem provers, formal reasoning,lambda-calculus} \subjclass{F.3.1} \begin{abstract}