diff -r 0865caafbfe6 -r 3890483c674f Paper/Paper.thy --- a/Paper/Paper.thy Mon Jan 03 16:21:12 2011 +0000 +++ b/Paper/Paper.thy Tue Jan 04 13:47:38 2011 +0000 @@ -23,7 +23,7 @@ If ("if _ then _ else _" 10) and alpha_set ("_ \\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and alpha_lst ("_ \\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and - alpha_res ("_ \\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and + alpha_res ("_ \\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set+}}$}}>\<^bsup>_, _, _\<^esup> _") and abs_set ("_ \\<^raw:{$\,_{\textit{abs\_set}}$}> _") and abs_set2 ("_ \\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup> _") and fv ("fa'(_')" [100] 100) and @@ -32,7 +32,7 @@ Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and Abs_lst ("[_]\<^bsub>list\<^esub>._") and Abs_dist ("[_]\<^bsub>#list\<^esub>._") and - Abs_res ("[_]\<^bsub>res\<^esub>._") and + Abs_res ("[_]\<^bsub>set+\<^esub>._") and Abs_print ("_\<^bsub>set\<^esub>._") and Cons ("_::_" [78,77] 73) and supp_set ("aux _" [1000] 10) and @@ -104,7 +104,7 @@ the second pair should \emph{not} be $\alpha$-equivalent: % \begin{equation}\label{ex1} - @{text "\{x, y}. x \ y \\<^isub>\ \{y, x}. x \ y"}\hspace{10mm} + @{text "\{x, y}. x \ y \\<^isub>\ \{y, x}. y \ x"}\hspace{10mm} @{text "\{x, y}. x \ y \\<^isub>\ \{z}. z \ z"} \end{equation} % @@ -138,7 +138,7 @@ \eqref{one} as $\alpha$-equivalent with % \begin{center} - @{text "\ x = 3 \ y = 2 \ z = loop \ x - y \"} + @{text "\ x = 3 \ y = 2 \ z = foo \ x - y \"} \end{center} % \noindent @@ -318,7 +318,7 @@ The problem with introducing a new type in Isabelle/HOL is that in order to be useful, a reasoning infrastructure needs to be ``lifted'' from the underlying subset to the new type. This is usually a tricky and arduous - task. To ease it, we re-implemented in Isabelle/HOL the quotient package + task. To ease it, we re-implemented in Isabelle/HOL \cite{KaliszykUrban11} the quotient package described by Homeier \cite{Homeier05} for the HOL4 system. This package allows us to lift definitions and theorems involving raw terms to definitions and theorems involving $\alpha$-equated terms. For example if we @@ -729,12 +729,12 @@ Now recall the examples shown in \eqref{ex1} and \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \ y)"} and @{text "({y, x}, y \ x)"} are $\alpha$-equivalent according to - $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{res}}$ by taking @{text p} to + $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{set+}}$ by taking @{text p} to be the swapping @{term "(x \ y)"}. In case of @{text "x \ y"}, then @{text "([x, y], x \ y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \ y)"} since there is no permutation that makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \ y"}} - unchanged. Another example is @{text "({x}, x)"} $\approx_{\,\textit{res}}$ + unchanged. Another example is @{text "({x}, x)"} $\approx_{\,\textit{set+}}$ @{text "({x, y}, x)"} which holds by taking @{text p} to be the identity permutation. However, if @{text "x \ y"}, then @{text "({x}, x)"} $\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no @@ -751,13 +751,13 @@ \end{equation} \noindent - (similarly for $\approx_{\,\textit{abs\_res}}$ + (similarly for $\approx_{\,\textit{abs\_set+}}$ and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence relations. %% and equivariant. \begin{lemma}\label{alphaeq} The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$ - and $\approx_{\,\textit{abs\_res}}$ are equivalence relations. %, and if + and $\approx_{\,\textit{abs\_set+}}$ are equivalence relations. %, 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{lemma} @@ -772,7 +772,7 @@ \noindent This lemma allows us to use our quotient package for introducing - new types @{text "\ abs_set"}, @{text "\ abs_res"} and @{text "\ abs_list"} + new types @{text "\ abs_set"}, @{text "\ abs_set+"} and @{text "\ abs_list"} 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). @@ -797,8 +797,8 @@ \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="as", no_vars]} $\;\;=\;\;$ - @{thm (rhs) supp_Abs(3)[where bs="as", no_vars]} + @{thm (lhs) supp_Abs(3)[where bs="bs", no_vars]} $\;\;=\;\;$ + @{thm (rhs) supp_Abs(3)[where bs="bs", no_vars]} \end{tabular} \end{center} \end{theorem} @@ -950,9 +950,9 @@ % \begin{center} \begin{tabular}{@ {}l@ {}} - \isacommand{bind} {\it binders} \isacommand{in} {\it bodies}\;\;\;\; - \isacommand{bind (set)} {\it binders} \isacommand{in} {\it bodies}\;\;\;\; - \isacommand{bind (res)} {\it binders} \isacommand{in} {\it bodies} + \isacommand{bind} {\it binders} \isacommand{in} {\it bodies}\;\;\;\, + \isacommand{bind (set)} {\it binders} \isacommand{in} {\it bodies}\;\;\;\, + \isacommand{bind (set+)} {\it binders} \isacommand{in} {\it bodies} \end{tabular} \end{center} % @@ -981,7 +981,7 @@ \noindent %Similarly for the other binding modes. %Interestingly, in case of \isacommand{bind (set)} - %and \isacommand{bind (res)} the binding clauses above will make a difference to the semantics + %and \isacommand{bind (set+)} the binding clauses above will make a difference to the semantics %of the specifications (the corresponding $\alpha$-equivalence will differ). We will %show this later with an example. @@ -998,7 +998,7 @@ For binders we distinguish between \emph{shallow} and \emph{deep} binders. Shallow binders are just labels. The restriction we need to impose on them is that in case of - \isacommand{bind (set)} and \isacommand{bind (res)} the labels must either + \isacommand{bind (set)} and \isacommand{bind (set+)} the labels must either refer to atom types or to sets of atom types; in case of \isacommand{bind} the labels must refer to atom types or lists of atom types. Two examples for the use of shallow binders are the specification of lambda-terms, where a @@ -1018,7 +1018,7 @@ \hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\ \hspace{5mm}$\mid$~@{text "TFun ty ty"}\\ \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}~~% - \isacommand{bind (res)} @{text xs} \isacommand{in} @{text T}\\ + \isacommand{bind (set+)} @{text xs} \isacommand{in} @{text T}\\ \end{tabular} \end{tabular} \end{center} @@ -1037,7 +1037,7 @@ other arguments and also in the same argument (we will call such binders \emph{recursive}, see below). The binding functions are expected to return either a set of atoms (for \isacommand{bind (set)} and - \isacommand{bind (res)}) or a list of atoms (for \isacommand{bind}). They can + \isacommand{bind (set+)}) or a list of atoms (for \isacommand{bind}). They can be defined by recursion over the corresponding type; the equations must be given in the binding function part of the scheme shown in \eqref{scheme}. For example a term-calculus containing @{text "Let"}s with @@ -1487,7 +1487,7 @@ \noindent In this case we define a premise @{text P} using the relation $\approx_{\,\textit{set}}$ given in Section~\ref{sec:binders} (similarly - $\approx_{\,\textit{res}}$ and $\approx_{\,\textit{list}}$ for the other + $\approx_{\,\textit{set+}}$ and $\approx_{\,\textit{list}}$ for the other binding modes). This premise defines $\alpha$-equivalence of two abstractions involving multiple binders. As above, we first build the tuples @{text "D"} and @{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding @@ -1641,7 +1641,7 @@ \begin{proof} The proof is by mutual induction over the definitions. The non-trivial cases involve premises built up by $\approx_{\textit{set}}$, - $\approx_{\textit{res}}$ and $\approx_{\textit{list}}$. They + $\approx_{\textit{set+}}$ and $\approx_{\textit{list}}$. They can be dealt with as in Lemma~\ref{alphaeq}. \end{proof} @@ -1761,7 +1761,7 @@ Finally we can add to our infrastructure a cases lemma (explained in the next section) and a structural induction principle - for the types @{text "ty\"}$_{i..n}$. The conclusion of the induction principle is + for the types @{text "ty\"}$_{1..n}$. The conclusion of the induction principle is of the form % %\begin{equation}\label{weakinduct} @@ -1794,7 +1794,7 @@ \end{center} % \noindent - These properties can be established using the induction principle. + These properties can be established using the induction principle for the types @{text "ty\"}$_{1..n}$. %%in \eqref{weakinduct}. Having these equivariant properties established, we can show that the support of term-constructors @{text "C\<^sup>\"} is included in @@ -1954,7 +1954,7 @@ %in every induction step. What is left to show is that we covered all cases. To do so, we use - a cases lemma derived for each type. For the terms in \eqref{letpat} + a \emph{cases lemma} derived for each type. For the terms in \eqref{letpat} this lemma is of the form % \begin{equation}\label{weakcases} @@ -1974,7 +1974,7 @@ principles conveniently, the cases lemma in \eqref{weakcases} is too weak. For this note that in order to apply this lemma, we have to establish @{text "P\<^bsub>trm\<^esub>"} for \emph{all} @{text Lam}- and \emph{all} @{text Let}-terms. - What we need instead is a cases rule where we only have to consider terms that have + What we need instead is a cases lemma where we only have to consider terms that have binders that are fresh w.r.t.~a context @{text "c"}. This gives the implications % \begin{center} @@ -2257,7 +2257,7 @@ binding clauses. In Ott you specify binding clauses with a single body; we allow more than one. We have to do this, because this makes a difference for our notion of $\alpha$-equivalence in case of \isacommand{bind (set)} and - \isacommand{bind (res)}. + \isacommand{bind (set+)}. % %Consider the examples % @@ -2312,7 +2312,7 @@ In a slightly different domain (programming with dependent types), the paper \cite{Altenkirch10} presents a calculus with a notion of - $\alpha$-equivalence related to our binding mode \isacommand{bind (res)}. + $\alpha$-equivalence related to our binding mode \isacommand{bind (set+)}. The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it has a more operational flavour and calculates a partial (renaming) map. In this way, the definition can deal with vacuous binders. However, to our @@ -2330,7 +2330,7 @@ To specify general binders we used the specifications from Ott, but extended them in some places and restricted them in others so that they make sense in the context of $\alpha$-equated terms. - We also introduced two binding modes (set and res) that do not + We also introduced two binding modes (set and set+) that do not exist in Ott. We have tried out the extension with calculi such as Core-Haskell, type-schemes and approximately a dozen of other typical examples from programming