# HG changeset patch # User Cezary Kaliszyk # Date 1274431665 -7200 # Node ID 1fe84fd8f8a45364fa76ad77fe7bd52d2014a35a # Parent 687369ae8f8122f2b645221b44b31b6da6d985d6# Parent 61a89e41c55bb3795876b65726af7902dffa4f7c merge diff -r 687369ae8f81 -r 1fe84fd8f8a4 Nominal-General/nominal_atoms.ML --- a/Nominal-General/nominal_atoms.ML Fri May 21 10:47:07 2010 +0200 +++ b/Nominal-General/nominal_atoms.ML Fri May 21 10:47:45 2010 +0200 @@ -71,10 +71,10 @@ (** outer syntax **) -local structure P = OuterParse and K = OuterKeyword in +local structure P = Parse and K = Keyword in val _ = - OuterSyntax.command "atom_decl" "declaration of a concrete atom type" K.thy_decl + Outer_Syntax.command "atom_decl" "declaration of a concrete atom type" K.thy_decl ((P.binding -- Scan.option (Args.parens (P.binding))) >> (Toplevel.print oo (Toplevel.theory o add_atom_decl))); diff -r 687369ae8f81 -r 1fe84fd8f8a4 Nominal-General/nominal_eqvt.ML --- a/Nominal-General/nominal_eqvt.ML Fri May 21 10:47:07 2010 +0200 +++ b/Nominal-General/nominal_eqvt.ML Fri May 21 10:47:45 2010 +0200 @@ -184,10 +184,10 @@ equivariance preds raw_induct intrs ctxt |> snd end -local structure P = OuterParse and K = OuterKeyword in +local structure P = Parse and K = Keyword in val _ = - OuterSyntax.local_theory "equivariance" + Outer_Syntax.local_theory "equivariance" "Proves equivariance for inductive predicate involving nominal datatypes." K.thy_decl (P.xname >> equivariance_cmd); end; diff -r 687369ae8f81 -r 1fe84fd8f8a4 Nominal-General/nominal_permeq.ML --- a/Nominal-General/nominal_permeq.ML Fri May 21 10:47:07 2010 +0200 +++ b/Nominal-General/nominal_permeq.ML Fri May 21 10:47:45 2010 +0200 @@ -155,7 +155,7 @@ (** methods **) -val _ = OuterKeyword.keyword "exclude" +val _ = Keyword.keyword "exclude" val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) []; val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- (Scan.repeat (Args.const true))) [] diff -r 687369ae8f81 -r 1fe84fd8f8a4 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Fri May 21 10:47:07 2010 +0200 +++ b/Nominal/Ex/Lambda.thy Fri May 21 10:47:45 2010 +0200 @@ -456,10 +456,10 @@ fun prove_strong_ind (pred_name, avoids) ctxt = Proof.theorem NONE (K I) [] ctxt -local structure P = OuterParse and K = OuterKeyword in +local structure P = Parse and K = Keyword in val _ = - OuterSyntax.local_theory_to_proof "nominal_inductive" + Outer_Syntax.local_theory_to_proof "nominal_inductive" "proves strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal (P.xname -- (Scan.optional (P.$$$ "avoids" |-- P.enum1 "|" (P.name -- (P.$$$ ":" |-- P.and_list1 P.term))) []) >> prove_strong_ind) diff -r 687369ae8f81 -r 1fe84fd8f8a4 Nominal/Ex/Test.thy --- a/Nominal/Ex/Test.thy Fri May 21 10:47:07 2010 +0200 +++ b/Nominal/Ex/Test.thy Fri May 21 10:47:45 2010 +0200 @@ -2,12 +2,22 @@ imports "../NewParser" begin +declare [[STEPS = 4]] + +atom_decl name + +(* +nominal_datatype trm = + Vr "name" +| Ap "trm" "trm" + +thm fv_trm_raw.simps[no_vars] +*) (* This file contains only the examples that are not supposed to work yet. *) declare [[STEPS = 2]] -atom_decl name (* example 4 from Terms.thy *) (* fv_eqvt does not work, we need to repaire defined permute functions diff -r 687369ae8f81 -r 1fe84fd8f8a4 Nominal/NewFv.thy --- a/Nominal/NewFv.thy Fri May 21 10:47:07 2010 +0200 +++ b/Nominal/NewFv.thy Fri May 21 10:47:45 2010 +0200 @@ -290,4 +290,21 @@ end *} +(**************************************************) + +datatype foo = + C1 nat +| C2 foo int + +(* +ML {* +fun mk_body descr sorts fv_ty_map dtyp = +let + val nth_dtyp_constr_tys descr sorts +in + true end +*} +*) + +end diff -r 687369ae8f81 -r 1fe84fd8f8a4 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Fri May 21 10:47:07 2010 +0200 +++ b/Nominal/NewParser.thy Fri May 21 10:47:45 2010 +0200 @@ -11,7 +11,7 @@ ML {* (* nominal datatype parser *) local - structure P = OuterParse; + structure P = Parse; structure S = Scan fun triple1 ((x, y), z) = (x, y, z) @@ -20,9 +20,9 @@ fun tswap (((x, y), z), u) = (x, y, u, z) in -val _ = OuterKeyword.keyword "bind" -val _ = OuterKeyword.keyword "bind_set" -val _ = OuterKeyword.keyword "bind_res" +val _ = Keyword.keyword "bind" +val _ = Keyword.keyword "bind_set" +val _ = Keyword.keyword "bind_res" val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ @@ -41,7 +41,7 @@ (* binding function parser *) val bnfun_parser = - S.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([], []) + S.optional (P.$$$ "binder" |-- P.fixes -- Parse_Spec.where_alt_specs) ([], []) (* main parser *) val main_parser = @@ -714,7 +714,7 @@ (* Command Keyword *) -val _ = OuterSyntax.local_theory "nominal_datatype" "test" OuterKeyword.thy_decl +val _ = Outer_Syntax.local_theory "nominal_datatype" "test" Keyword.thy_decl (main_parser >> nominal_datatype2_cmd) *} diff -r 687369ae8f81 -r 1fe84fd8f8a4 Nominal/Perm.thy --- a/Nominal/Perm.thy Fri May 21 10:47:07 2010 +0200 +++ b/Nominal/Perm.thy Fri May 21 10:47:45 2010 +0200 @@ -7,20 +7,32 @@ ML {* (* returns the type of the nth datatype *) -fun nth_dtyp dt_descr sorts i = - Datatype_Aux.typ_of_dtyp dt_descr sorts (Datatype_Aux.DtRec i); +fun nth_dtyp descr sorts n = + Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n); + +(* returns the constructors of the nth datatype *) +fun nth_dtyp_constrs descr n = +let + val (_, (_, _, constrs)) = nth descr n +in + constrs +end + +(* returns the types of the constructors of the nth datatype *) +fun nth_dtyp_constr_typs descr sorts n = + map (map (Datatype_Aux.typ_of_dtyp descr sorts) o snd) (nth_dtyp_constrs descr n) *} ML {* (* generates for every datatype a name str ^ dt_name plus and index for multiple occurences of a string *) -fun prefix_dt_names dt_descr sorts str = +fun prefix_dt_names descr sorts str = let fun get_nth_name (i, _) = - Datatype_Aux.name_of_typ (nth_dtyp dt_descr sorts i) + Datatype_Aux.name_of_typ (nth_dtyp descr sorts i) in Datatype_Prop.indexify_names - (map (prefix str o get_nth_name) dt_descr) + (map (prefix str o get_nth_name) descr) end *} diff -r 687369ae8f81 -r 1fe84fd8f8a4 Paper/Paper.thy --- a/Paper/Paper.thy Fri May 21 10:47:07 2010 +0200 +++ b/Paper/Paper.thy Fri May 21 10:47:45 2010 +0200 @@ -9,7 +9,7 @@ alpha_bn :: "'a \ 'a \ bool" abs_set2 :: "'a \ perm \ 'b \ 'c" Abs_dist :: "'a \ 'b \ 'c" - + Abs_print :: "'a \ 'b \ 'c" definition "equal \ (op =)" @@ -33,6 +33,7 @@ Abs_lst ("[_]\<^raw:$\!$>\<^bsub>list\<^esub>._") and Abs_dist ("[_]\<^raw:$\!$>\<^bsub>#list\<^esub>._") and Abs_res ("[_]\<^raw:$\!$>\<^bsub>res\<^esub>._") and + Abs_print ("_\<^raw:$\!$>\<^bsub>set\<^esub>._") and Cons ("_::_" [78,77] 73) and supp_gen ("aux _" [1000] 10) and alpha_bn ("_ \bn _") @@ -52,15 +53,15 @@ \end{center} \noindent - where free and bound variables have names. For such alpha-equated terms, Nominal Isabelle - derives automatically a reasoning infrastructure that has been used - successfully in formalisations of an equivalence checking algorithm for LF - \cite{UrbanCheneyBerghofer08}, Typed + where free and bound variables have names. For such alpha-equated terms, + Nominal Isabelle derives automatically a reasoning infrastructure that has + been used successfully in formalisations of an equivalence checking + algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency - \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}. + \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}. However, Nominal Isabelle has fared less well in a formalisation of the algorithm W \cite{UrbanNipkow09}, where types and type-schemes are, @@ -546,7 +547,7 @@ \noindent or equivalently that a permutation applied to the application @{text "f x"} can be moved to the argument @{text x}. That means for equivariant - functions @{text f} we have for all permutations @{text p} + functions @{text f}, we have for all permutations @{text p} % \begin{equation}\label{equivariance} @{text "p \ f = f"} \;\;\;\textit{if and only if}\;\;\; @@ -798,7 +799,8 @@ \end{proof} \noindent - This lemma together with \eqref{absperm} allows us to show + Assuming that @{text "x"} has finite support, this lemma together + with \eqref{absperm} allows us to show % \begin{equation}\label{halfone} @{thm abs_supports(1)[no_vars]} @@ -918,11 +920,10 @@ the second is for sets of binders (the order does not matter, but the cardinality does) and the last is for sets of binders (with vacuous binders preserving alpha-equivalence). The ``\isacommand{in}-part'' of a binding - clause will be called \emph{bodies} (there can be more than one); the - ``\isacommand{bind}-part'' will be called \emph{binders}. - - In contrast to Ott, we allow multiple labels in binders and bodies. For example - we allow binding clauses of the form: + clause will be called \emph{bodies} (there can be more than one); the + ``\isacommand{bind}-part'' will be called \emph{binders}. In contrast to + Ott, we allow multiple labels in binders and bodies. For example we allow + binding clauses of the form: \begin{center} \begin{tabular}{@ {}ll@ {}} @@ -936,8 +937,9 @@ \noindent Similarly for the other binding modes. Interestingly, in case of \isacommand{bind\_set} - and \isacommand{bind\_res} the binding clauses will make a difference in - terms of the corresponding alpha-equivalence. We will show this later with an example. + and \isacommand{bind\_res} the binding clauses will make a difference to the semantics + of the specification (the corresponding alpha-equivalence will differ). We will + show this later with an example. There are some restrictions we need to impose: First, a body can only occur in \emph{one} binding clause of a term constructor. For binders we @@ -972,8 +974,8 @@ \noindent Note that for @{text lam} it does not matter which binding mode we use. The reason is that we bind only a single @{text name}. However, having - \isacommand{bind\_set} or \isacommand{bind} in the second case again makes a - difference to the underlying notion of alpha-equivalence. Note also that in + \isacommand{bind\_set} or \isacommand{bind} in the second case makes again a + difference to the semantics of the specification. Note also that in these specifications @{text "name"} refers to an atom type, and @{text "fset"} to the type of finite sets. @@ -1032,7 +1034,7 @@ binders \emph{recursive}. To see the purpose of such recursive binders, compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s in the following specification: - % + \begin{equation}\label{letrecs} \mbox{% \begin{tabular}{@ {}l@ {}} @@ -1055,11 +1057,10 @@ The difference is that with @{text Let} we only want to bind the atoms @{text "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms inside the assignment. This difference has consequences for the free-variable - function and alpha-equivalence relation, which we are going to describe in the - rest of this section. + function and alpha-equivalence relation, which we are going to define below. - The restriction we have to impose on deep binders is that we cannot have - more than one binding function for one binder. So we exclude: + For this definition, we have to impose some restrictions on deep binders. First, + we cannot have more than one binding function for one binder. So we exclude: \begin{center} \begin{tabular}{ll} @@ -1090,8 +1091,8 @@ In order to simplify our definitions, we shall assume specifications of term-calculi are \emph{completed}. By this we mean that for every argument of a term-constructor that is \emph{not} - already part of a binding clause, we add implicitly a special \emph{empty} binding - clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "label"}. In case + already part of a binding clause given by the user, we add implicitly a special \emph{empty} binding + clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case of the lambda-calculus, the completion produces \begin{center} @@ -1100,8 +1101,7 @@ \hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"} \;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "x"}\\ \hspace{5mm}$\mid$~@{text "App t\<^isub>1::lam t\<^isub>2::lam"} - \;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>1"}, - \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>2"}\\ + \;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>1 t\<^isub>2"}\\ \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"} \;\;\isacommand{bind}~@{text x} \isacommand{in} @{text t}\\ \end{tabular} @@ -1913,13 +1913,13 @@ approach to binding \cite{chargueraud09}. There, de-Bruijn indices consist of two numbers, one referring to the place where a variable is bound and the other to which variable is bound. The reasoning infrastructure for both - representations of bindings comes for free in the theorem provers, like Isabelle/HOL or + representations of bindings comes for free in theorem provers like Isabelle/HOL or Coq, as the corresponding term-calculi can be implemented as ``normal'' datatypes. However, in both approaches it seems difficult to achieve our fine-grained control over the ``semantics'' of bindings (i.e.~whether the order of binders should matter, or vacuous binders should be taken into account). To do so, one would require additional predicates that filter out - unwanted terms. Our guess is that such predicates results in rather + unwanted terms. Our guess is that such predicates result in rather intricate formal reasoning. Another representation technique for binding is higher-order abstract syntax @@ -1936,39 +1936,93 @@ all the unwanted consequences when reasoning about the resulting terms. Two formalisations involving general binders have also been performed in older - versions of Nominal Isabelle \cite{BengtsonParow09, UrbanNipkow09}. Both + versions of Nominal Isabelle (one about Psi-calculi and one about alpgorithm W + \cite{BengtsonParow09, UrbanNipkow09}). Both use the approach based on iterated single binders. Our experience with the latter formalisation has been disappointing. The major pain arose from the need to ``unbind'' variables. This can be done in one step with our - general binders, for example @{term "Abs as x"}, but needs a cumbersome + general binders, but needs a cumbersome iteration with single binders. The resulting formal reasoning turned out to be rather unpleasant. The hope is that the extension presented in this paper is a substantial improvement. - The most closely related work to the one presented here is the Ott-tool \cite{ott-jfp}. This tool is a - nifty front-end for creating \LaTeX{} documents from specifications of - term-calculi involving general binders. For a subset of the specifications, Ott can also generate - theorem prover code using a raw representation of terms, and in Coq also a - locally nameless representation. The developers of this tool have also put - forward (on paper) a definition for alpha-equivalence of terms that can be - specified in Ott. This definition is rather different from ours, not using - any nominal techniques. Although we were heavily inspired by their syntax, + The most closely related work to the one presented here is the Ott-tool + \cite{ott-jfp} and the C$\alpha$ml language \cite{Pottier06}. Ott is a nifty + front-end for creating \LaTeX{} documents from specifications of + term-calculi involving general binders. For a subset of the specifications, + Ott can also generate theorem prover code using a raw representation of + terms, and in Coq also a locally nameless representation. The developers of + this tool have also put forward (on paper) a definition for + alpha-equivalence of terms that can be specified in Ott. This definition is + rather different from ours, not using any nominal techniques. To our + knowledge there is also no concrete mathematical result concerning this + notion of alpha-equivalence. A definition for the notion of free variables + in a term are work in progress in Ott. + + Although we were heavily inspired by their syntax, their definition of alpha-equivalence is unsuitable for our extension of Nominal Isabelle. First, it is far too complicated to be a basis for automated proofs implemented on the ML-level of Isabelle/HOL. Second, it covers cases of binders depending on other binders, which just do not make sense for our alpha-equated terms. Third, it allows empty types that have no - meaning in a HOL-based theorem prover. + meaning in a HOL-based theorem prover. We also had to generalise slightly their + 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}. This makes + + \begin{center} + \begin{tabular}{@ {}ll@ {}} + @{text "Foo\<^isub>1 xs::name fset x::name y::name"} & + \isacommand{bind\_set} @{text "xs"} \isacommand{in} @{text "x y"}\\ + @{text "Foo\<^isub>2 xs::name fset x::name y::name"} & + \isacommand{bind\_set} @{text "xs"} \isacommand{in} @{text "x"}, + \isacommand{bind\_set} @{text "xs"} \isacommand{in} @{text "y"}\\ + \end{tabular} + \end{center} + + \noindent + behave differently. To see this, consider the following equations + + \begin{center} + \begin{tabular}{c} + @{term "Abs_print [a,b] (a, b) = Abs_print [a,b] (b, a)"}\\ + @{term "Abs_print [a,b] (a, b) = Abs_print [a,b] (a, b)"}\\ + \end{tabular} + \end{center} + + \noindent + The interesting point is that they do not imply + + \begin{center} + \begin{tabular}{c} + @{term "Abs_print [a,b] ((a, b), (a, b)) = Abs_print [a,b] ((a, b), (b, a))"}\\ + \end{tabular} + \end{center} Because of how we set up our definitions, we had to impose restrictions, - like excluding overlapping deep binders, that are not present in Ott. Our + like a single binding function for a deep binder, that are not present in Ott. Our expectation is that we can still cover many interesting term-calculi from programming language research, for example Core-Haskell. For providing support of neat features in Ott, such as subgrammars, the existing datatype infrastructure in Isabelle/HOL is unfortunately not powerful enough. On the other hand, we are not aware that Ott can make the distinction between our - three different binding modes. Also, definitions for notions like the free - variables of a term are work in progress in Ott. + three different binding modes. + + Pottier presents in \cite{Pottier06} a language, called C$\alpha$ml, for + representing terms with general binders inside OCaml. This language is + implemented as a front-end that can be translated to OCaml with a help of + a library. He presents a type-system in which the scope of general binders + can be indicated with some special constructs, written @{text "inner"} and + @{text "outer"}. With this, it seems, our and his specifications can be + inter-translated, but we have not proved this. However, we believe the + binding specifications in the style of Ott are a more natural way for + representing terms involving bindings. Pottier gives a definition for + alpha-equivalence, which is similar to our binding mod \isacommand{bind}. + Although he uses also a permutation in case of abstractions, his + definition is rather different from ours. He proves that his notion + of alpha-equivalence is indeed a equivalence relation, but a complete + reasoning infrastructure is well beyond the purposes of his language. *} section {* Conclusion *} @@ -2002,45 +2056,7 @@ version @{text "TFun string ty_list"} in Figure~\ref{nominalcorehas}. For them we need a more clever implementation than we have at the moment. - More - interesting is lifting our restriction about overlapping deep binders. Given - our current setup, we cannot deal with specifications such as - - - \begin{center} - \begin{tabular}{ll} - @{text "Foo r::pat s::pat t::trm"} & - \isacommand{bind} @{text "bn(r)"} \isacommand{in} @{text t},\; - \isacommand{bind} @{text "bn(s)"} \isacommand{in} @{text t} - \end{tabular} - \end{center} - - \noindent - where the deep binders @{text "bn(r)"} and @{text "bn(s)"} overlap. - The difficulty is that we would need to implement such overlapping bindings - with alpha-equivalences like - - \begin{center} - @{term "\p q. abs_set2 (bn r\<^isub>1, t\<^isub>1) p (bn r\<^isub>2, t\<^isub>2) \ abs_set2 (bn s\<^isub>1, t\<^isub>1) q (bn s\<^isub>2, t\<^isub>2)"} - \end{center} - - \noindent - or - - \begin{center} - @{term "\p q. abs_set2 (bn r\<^isub>1 \ bn s\<^isub>1, t\<^isub>1) (p + q) (bn r\<^isub>2 \ bn s\<^isub>2, t\<^isub>2)"} - \end{center} - - \noindent - Both versions require two permutations (for each binding). But unfortunately the - first version cannot work since it leaves some atoms unbound that should be - bound by the respective other binder. This problem is avoided in the second - version, but at the expense that the two permutations can interfere with each - other. We have not yet been able to find a way to avoid such interferences. - On the other hand, such bindings can be made sense of informally \cite{SewellBestiary}. - This suggest there should be an approriate notion of alpha-equivalence. - - Another interesting line of investigation is whether we can go beyond the + More interesting line of investigation is whether we can go beyond the simple-minded form for binding functions that we adopted from Ott. At the moment, binding functions can only return the empty set, a singleton atom set or unions of atom sets (similarly for lists). It remains to be seen whether