# HG changeset patch # User Christian Urban # Date 1315307882 -3600 # Node ID 3c8d3aaf292c3b1a4219c5e89b81a29f3963e3ae # Parent 68c894c513f619a8f9023af09a618d2b40528f00 more on the lmcs paper diff -r 68c894c513f6 -r 3c8d3aaf292c LMCS-Paper/Paper.thy --- a/LMCS-Paper/Paper.thy Sun Aug 28 14:50:13 2011 +0100 +++ b/LMCS-Paper/Paper.thy Tue Sep 06 12:18:02 2011 +0100 @@ -101,7 +101,7 @@ Binding multiple variables has interesting properties that cannot be captured easily by iterating single binders. For example in the case of type-schemes we do not want to make a distinction about the order of the bound variables. Therefore - we would like to regard the first pair of type-schemes as alpha-equivalent, + we would like to regard below the first pair of type-schemes as alpha-equivalent, but assuming that @{text x}, @{text y} and @{text z} are distinct variables, the second pair should \emph{not} be alpha-equivalent: @@ -226,9 +226,9 @@ is heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. Our work extends Ott in several aspects: one is that we support three binding modes---Ott has only one, namely the one where the order of binders matters. - Another is that our reasoning infrastructure, like the notion of support and - strong induction principles, is derived from first principles within the - Isabelle/HOL theorem prover. + Another is that our reasoning infrastructure, like strong induction principles + and the notion of free variables, is derived from first principles within + the Isabelle/HOL theorem prover. However, we will not be able to cope with all specifications that are allowed by Ott. One reason is that Ott lets the user specify ``empty'' types @@ -331,7 +331,7 @@ \noindent then with the help of the quotient package we can obtain a function @{text "fv\<^sup>\"} - operating on quotients, or alpha-equivalence classes of lambda-terms. This + operating on quotients, that is alpha-equivalence classes of lambda-terms. This lifted function is characterised by the equations \[ @@ -361,8 +361,8 @@ 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 specification of SML, - which includes includes bindings as in type-schemes.\medskip + variables need to be bound. Another example is the algorithm W + which includes multiple binders in type-schemes.\medskip \noindent {\bf Contributions:} We provide three new definitions for when terms @@ -432,7 +432,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 "p, q, \"} to stand for + b, c, \"} to stand for atoms and @{text "\, \"} to stand for permutations. 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 type-variables in Core-Haskell. @@ -447,8 +447,8 @@ where the generic type @{text "\"} is the type of the object 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 + 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}; for example permutations acting on products, lists, sets, functions and booleans are given by: @@ -456,43 +456,26 @@ \begin{equation}\label{permute} \mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}} \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]}\\ + @{thm permute_prod.simps[where p="\", no_vars, THEN eq_reflection]}\\[2mm] + @{thm permute_list.simps(1)[where p="\", no_vars, THEN eq_reflection]}\\ + @{thm permute_list.simps(2)[where p="\", no_vars, THEN eq_reflection]}\\ \end{tabular} & \begin{tabular}{@ {}l@ {}} - @{thm permute_set_eq[no_vars, THEN eq_reflection]}\\ - @{text "p \ f \ \x. p \ (f (- p \ x))"}\\ - @{thm permute_bool_def[no_vars, THEN eq_reflection]} + @{thm permute_set_eq[where p="\", no_vars, THEN eq_reflection]}\\ + @{text "\ \ f \ \x. \ \ (f (- \ \ x))"}\\ + @{thm permute_bool_def[where p="\", no_vars, THEN eq_reflection]} \end{tabular} \end{tabular}} - \end{equation} + \end{equation}\smallskip - \begin{center} - \mbox{\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {\hspace{4mm}}c@ {}} - \begin{tabular}{@ {}l@ {}} - @{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\ - @{thm permute_bool_def[no_vars, THEN eq_reflection]} - \end{tabular} & - \begin{tabular}{@ {}l@ {}} - @{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 \ f \ \x. p \ (f (- p \ x))"}\\ - \end{tabular} - \end{tabular}} - \end{center} - \noindent Concrete permutations in Nominal Isabelle are built up from swappings, written as \mbox{@{text "(a b)"}}, which are permutations that behave as follows: - \begin{center} + \[ @{text "(a b) = \c. if a = c then b else if b = c then a else c"} - \end{center} + \]\smallskip 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 @@ -508,25 +491,31 @@ \noindent There is also the derived notion for when an atom @{text a} is \emph{fresh} - for an @{text x}, defined as @{thm fresh_def[no_vars]}. + for an @{text x}, defined as + + \[ + @{thm fresh_def[no_vars]} + \]\smallskip + + \noindent We use for sets of atoms the abbreviation @{thm (lhs) fresh_star_def[no_vars]}, defined as @{thm (rhs) fresh_star_def[no_vars]}. A striking consequence of these definitions is that we can prove without knowing anything about the structure of @{term x} that swapping two fresh atoms, say @{text a} and @{text b}, leaves - @{text x} unchanged, namely if @{text "a \ x"} and @{text "b \ x"} - then @{term "(a \ b) \ x = x"}. + @{text x} unchanged, namely \begin{prop}\label{swapfreshfresh} - @{thm[mode=IfThen] swap_fresh_fresh[no_vars]} + If @{thm (prem 1) swap_fresh_fresh[no_vars]} and @{thm (prem 2) swap_fresh_fresh[no_vars]} + then @{thm (concl) swap_fresh_fresh[no_vars]} \end{prop} While often the support of an object can be relatively easily described, for example for atoms, products, lists, function applications, booleans and permutations as follows - \begin{center} + \[\mbox{ \begin{tabular}{c@ {\hspace{10mm}}c} \begin{tabular}{rcl} @{term "supp a"} & $=$ & @{term "{a}"}\\ @@ -538,18 +527,16 @@ \begin{tabular}{rcl} @{text "supp (f x)"} & @{text "\"} & @{term "supp f \ supp x"}\\ @{term "supp b"} & $=$ & @{term "{}"}\\ - @{term "supp p"} & $=$ & @{term "{a. p \ a \ a}"} + @{term "supp \"} & $=$ & @{term "{a. \ \ a \ a}"} \end{tabular} - \end{tabular} - \end{center} + \end{tabular}} + \]\smallskip \noindent in some cases it can be difficult to characterise the support precisely, and - only an approximation can be established (as for functions above). - - Reasoning about - such approximations can be simplified with the notion \emph{supports}, defined - as follows: + only an approximation can be established (as for function applications + above). Reasoning about such approximations can be simplified with the + notion \emph{supports}, defined as follows: \begin{defi} A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b} diff -r 68c894c513f6 -r 3c8d3aaf292c LMCS-Paper/document/root.tex --- a/LMCS-Paper/document/root.tex Sun Aug 28 14:50:13 2011 +0100 +++ b/LMCS-Paper/document/root.tex Tue Sep 06 12:18:02 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, formal reasoning} +\keywords{Nominal Isabelle, variable convention, theorem provers, formal reasoning} \subjclass{F.3.1} \begin{abstract}