diff -r 3668b389edf3 -r 3bf0fddb7d44 Paper/Paper.thy --- a/Paper/Paper.thy Mon Mar 29 14:58:00 2010 +0200 +++ b/Paper/Paper.thy Mon Mar 29 16:41:21 2010 +0200 @@ -13,7 +13,7 @@ notation (latex output) swap ("'(_ _')" [1000, 1000] 1000) and fresh ("_ # _" [51, 51] 50) and - fresh_star ("_ #* _" [51, 51] 50) and + fresh_star ("_ #\<^sup>* _" [51, 51] 50) and supp ("supp _" [78] 73) and uminus ("-_" [78] 73) and If ("if _ then _ else _" 10) and @@ -47,7 +47,7 @@ successfully in formalisations of an equivalence checking algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency - \cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result + \cite{BengtsonParow09} and a strong normalisation result 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}. @@ -328,27 +328,24 @@ \noindent (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. For example, we - will not be able to lift a bound-variable function, which can be defined for - 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 (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. + only works if alpha-equivalence is indeed an equivalence relation, and the + lifted definitions and theorems are respectful w.r.t.~alpha-equivalence. + For example, we will not be able to lift a bound-variable function. Although + this function can be defined for raw terms, it does not respect + alpha-equivalence and therefore cannot be lifted. To sum up, every lifting + of theorems to the quotient level needs proofs of some respectfulness + 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 - 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 - binders and reasoning about them in a theorem prover would be a major pain. - \medskip - + 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 have 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 \noindent {\bf Contributions:} We provide new definitions for when terms @@ -369,35 +366,35 @@ \multicolumn{3}{@ {}l}{Coercion Kinds}\\ @{text "\"} & @{text "::="} & @{text "\\<^isub>1 \ \\<^isub>2"}\medskip\\ \multicolumn{3}{@ {}l}{Types}\\ - @{text "\"} & @{text "::="} & @{text "a | T | \\<^isub>1 \\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\"}}$@{text "\<^sup>n"}\\ - & & @{text "| \a:\. \ "}\\ - & & ??? Type equality\medskip\\ + @{text "\"} & @{text "::="} & @{text "a | T | \\<^isub>1 \\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\"}}$@{text "\<^sup>n"} + @{text "| \a:\. \ | \ \ \"}\medskip\\ \multicolumn{3}{@ {}l}{Coercion Types}\\ - @{text "\"} & @{text "::="} & @{text "a | C | S\<^isub>n"}$\;\overline{@{text "\"}}$@{text "\<^sup>n"}\\ - & & @{text "| \a:\. \"}\\ - & & ??? Coercion Type equality\\ - & & @{text "| sym \ | \\<^isub>1 \ \\<^isub>2 | left \ | right \ | \\<^isub>1 \ \\<^isub>2 "}\\ - & & @{text "| rightc \ | leftc \ | \\<^isub>1 \ \\<^isub>2"}\medskip\\ + @{text "\"} & @{text "::="} & @{text "c | C | \\<^isub>1 \\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\"}}$@{text "\<^sup>n"} + @{text "| \c:\. \ | \ \ \ |"}\\ + & & @{text "refl \ | sym \ | \\<^isub>1 \ \\<^isub>2 | \ @ \ |"}\\ + & & @{text "left \ | right \ | \\<^isub>1 \ \\<^isub>2 |"}\\ + & & @{text "rightc \ | leftc \ | \\<^isub>1 \ \\<^isub>2"}\medskip\\ \multicolumn{3}{@ {}l}{Terms}\\ - @{text "e"} & @{text "::="} & @{text "x | K | \a:\. e | \a:\. e | e \ | e \ |"}\\ - & & @{text "\x:\.e | e\<^isub>1 e\<^isub>2 | \ x:\ = e\<^isub>1 \ e\<^isub>2 |"}\\ + @{text "e"} & @{text "::="} & @{text "x | K | \a:\. e | \c:\. e | e \ | e \ |"}\\ + & & @{text "\x:\. e | e\<^isub>1 e\<^isub>2 | \ x:\ = e\<^isub>1 \ e\<^isub>2 |"}\\ & & @{text "\ e\<^isub>1 \"}$\;\overline{@{text "p \ e\<^isub>2"}}$ @{text "| e \ \"}\medskip\\ \multicolumn{3}{@ {}l}{Patterns}\\ - @{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\"}}\;\overline{@{text "a:\"}}\;\overline{@{text "x:\"}}$\medskip\\ + @{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\"}}\;\overline{@{text "c:\"}}\;\overline{@{text "x:\"}}$\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\\ + @{text C} & & coercion constants\\ + @{text T} & & value type constructors\\ + @{text "S\<^isub>n"} & & n-ary type functions\\ + @{text K} & & data constructors\medskip\\ \multicolumn{3}{@ {}l}{Variables}\\ - @{text a} & & type variable\\ - @{text x} & & term variable\\ + @{text a} & & type variables\\ + @{text c} & & coercion variables\\ + @{text x} & & term variables\\ \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 inessential modification by - separating the grammars for type kinds and coercion types.\label{corehas}} + \caption{The term-language of System @{text "F\<^isub>C"}, also often referred to as \emph{Core-Haskell} + \cite{CoreHaskell}. In this version of Core-Haskell we made a modification by + separating completely the grammars for type kinds and coercion types.\label{corehas}} \end{figure} *} @@ -406,13 +403,16 @@ 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} (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 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. + \cite{HuffmanUrban10} (including proofs). We shall briefly review this work + 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 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 the identity everywhere except on a finite number of atoms. There is a @@ -422,14 +422,15 @@ \noindent in which the generic type @{text "\"} stands for the type of the object - on which the permutation + 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 - operation is defined for products, lists, sets, functions, booleans etc (see \cite{HuffmanUrban10}) + operation is defined by induction over the type-hierarchy, for example as follows + for products, lists, sets, functions and booleans (see \cite{HuffmanUrban10}): - \begin{center} - \begin{tabular}{@ {}cc@ {}} + \begin{equation} + \mbox{\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]}\\ @@ -437,16 +438,15 @@ \end{tabular} & \begin{tabular}{@ {}l@ {}} @{thm permute_set_eq[no_vars, THEN eq_reflection]}\\ - @{text "p \ (f x) \ (p \ f) (p \ x)"}\\ + @{text "p \ f \ \x. p \ (f (- p \ x))"}\\ @{thm permute_bool_def[no_vars, THEN eq_reflection]}\\ \end{tabular} - \end{tabular} - \end{center} + \end{tabular}} + \end{equation} \noindent - Concrete permutations are build up from - swappings, written as @{text "(a b)"}, - which are permutations that behave as follows: + 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) = \c. if a = c then b else if b = c then a else c"} @@ -493,9 +493,8 @@ \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. + and only give an approximation (see functions above). Such approximations can + be formalised with the notion \emph{supports}, defined as follows. \begin{defn} A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b} @@ -503,7 +502,7 @@ \end{defn} \noindent - The point of this definitions is that we can show: + The point of this definition is that we can show: \begin{property} {\it i)} @{thm[mode=IfThen] supp_is_subset[no_vars]} @@ -512,6 +511,19 @@ \noindent Another important notion in the nominal logic work is \emph{equivariance}. + For a function @{text f}, lets say of type @{text "\ \ \"}, to be equivariant + means that every permutation leaves @{text f} unchanged, or equivalently that + a permutation applied to an application @{text "f x"} can be moved to its + arguments. That is + + \begin{center} + @{text "\p. p \ f = f"} \hspace{5mm} + @{text "\p. p \ (f x) = f (p \ x)"} + \end{center} + + \noindent + From the first equation we can be easily deduce that an equivariant function has + empty support. %\begin{property} %@{thm[mode=IfThen] at_set_avoiding[no_vars]}