# HG changeset patch # User Christian Urban # Date 1290768835 0 # Node ID cb16f22bc660ad007065a4f9cda217650e9a40d6 # Parent 6c4372a1f2204be90135bfd2bcce98bb256a3b4f# Parent dc988b07755ef2e5496273b04fce5fd8264818ad merged diff -r dc988b07755e -r cb16f22bc660 Nominal/Ex/SystemFOmega.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Ex/SystemFOmega.thy Fri Nov 26 10:53:55 2010 +0000 @@ -0,0 +1,51 @@ +theory SystemFOmega +imports "../Nominal2" +begin + +text {* + System from the F-ing paper by Rossberg, Russo and + Dreyer, TLDI'10 +*} + + +atom_decl var +atom_decl tvar +atom_decl label + +nominal_datatype kind = + \ | KFun kind kind + +nominal_datatype ty = + TVar tvar +| TFun ty ty +| TAll a::tvar kind t::ty bind a in t +| TEx a::tvar kind t::ty bind a in t +| TLam a::tvar kind t::ty bind a in t +| TApp ty ty +| TRec trec +and trec = + TRNil +| TRCons label ty trec + +nominal_datatype trm = + Var var +| Lam x::var ty t::trm bind x in t +| App trm trm +| Dot trm label +| LAM a::tvar kind t::trm bind a in t +| APP trm ty +| Pack ty trm +| Unpack a::tvar x::var trm t::trm bind a x in t +| Rec rec +and rec = + RNil +| RCons label trm rec + + + + +end + + + + diff -r dc988b07755e -r cb16f22bc660 Nominal/ROOT.ML --- a/Nominal/ROOT.ML Fri Nov 26 12:17:24 2010 +0900 +++ b/Nominal/ROOT.ML Fri Nov 26 10:53:55 2010 +0000 @@ -19,6 +19,7 @@ "Ex/Modules", "Ex/SingleLet", "Ex/Shallow", + "Ex/SystemFOmega", "Ex/TypeSchemes", "Ex/TypeVarsTest", "Ex/Foo1", diff -r dc988b07755e -r cb16f22bc660 Paper/Paper.thy --- a/Paper/Paper.thy Fri Nov 26 12:17:24 2010 +0900 +++ b/Paper/Paper.thy Fri Nov 26 10:53:55 2010 +0000 @@ -274,7 +274,7 @@ Although in informal settings a reasoning infrastructure for $\alpha$-equated terms is nearly always taken for granted, establishing it automatically in - the Isabelle/HOL is a rather non-trivial task. For every + Isabelle/HOL is a rather non-trivial task. For every specification we will need to construct type(s) containing as elements the $\alpha$-equated terms. To do so, we use the standard HOL-technique of defining a new type by identifying a non-empty subset of an existing type. The @@ -441,10 +441,9 @@ b, c, \"} to stand for atoms and @{text "p, q, \"} 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. + variables, such as the term-, coercion- and type-variables in Core-Haskell. It is assumed that there is an infinite supply of atoms for each - sort. However, in the interest of brevity, we shall restrict ourselves + sort. In the interest of brevity, we shall restrict ourselves in what follows to only one sort of atoms. Permutations are bijective functions from atoms to atoms that are @@ -457,7 +456,7 @@ 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 over the type-hierarchy \cite{HuffmanUrban10}; - for example permutations acting on products, lists, sets, functions and booleans is + for example permutations acting on products, lists, sets, functions and booleans are given by: % %\begin{equation}\label{permute} @@ -1429,7 +1428,7 @@ %\noindent for the binding functions @{text "bn"}$_{1..m}$, To simplify our definitions we will use the following abbreviations for - \emph{compound equivalence relations} and \emph{compound free-atom functions} acting on tuples + \emph{compound equivalence relations} and \emph{compound free-atom functions} acting on tuples. % \begin{center} \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} @@ -1619,7 +1618,7 @@ Note the difference between $\approx_{\textit{assn}}$ and $\approx_{\textit{bn}}$: the latter only ``tracks'' $\alpha$-equivalence of the components in an assignment that are \emph{not} bound. This is needed in the - in the clause for @{text "Let"} (which is has + clause for @{text "Let"} (which has a non-recursive binder). %The underlying reason is that the terms inside an assignment are not meant %to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"}, @@ -1834,7 +1833,7 @@ \end{proof} \noindent - To sum up this section, we can established automatically a reasoning infrastructure + To sum up this section, we can establish automatically a reasoning infrastructure for the types @{text "ty\"}$_{1..n}$ by first lifting definitions from the raw level to the quotient level and then by establishing facts about these lifted definitions. All necessary proofs @@ -1949,7 +1948,7 @@ In \cite{UrbanTasson05} we showed how the weaker induction principles imply the stronger ones. This was done by some quite complicated, nevertheless automated, induction proofs. In this paper we simplify this work by leveraging the automated proof - methods from the function package of Isabelle/HOL generates. + methods from the function package of Isabelle/HOL. The reasoning principle these methods employ is well-founded induction. To use them in our setting, we have to discharge two proof obligations: one is that we have @@ -2032,8 +2031,8 @@ \noindent Now Properties \ref{supppermeq} and \ref{avoiding} give us a permutation @{text q} such that @{text "(set (bn (q \\<^bsub>bn\<^esub> p)) \\<^sup>* c"} holds and such that @{text "[q \\<^bsub>bn\<^esub> p]\<^bsub>list\<^esub>.(q \ t)"} - is equal to @{text "[p]\<^bsub>list\<^esub>. t"}. We can also show that @{text "(q \\<^bsub>bn\<^esub> p) \\<^bsub>bn\<^esub> p"}. T - hese facts establish that @{text "Let (q \\<^bsub>bn\<^esub> p) (p \ t) = Let p t"}, as we need. This + is equal to @{text "[p]\<^bsub>list\<^esub>. t"}. We can also show that @{text "(q \\<^bsub>bn\<^esub> p) \\<^bsub>bn\<^esub> p"}. + These facts establish that @{text "Let (q \\<^bsub>bn\<^esub> p) (p \ t) = Let p t"}, as we need. This completes the non-trivial cases in \eqref{letpat} for strengthening the corresponding induction principle. @@ -2203,7 +2202,7 @@ de-Bruijn representation), but to different bound variables. A similar idea has been recently explored for general binders in the locally nameless 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 + 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 theorem provers like Isabelle/HOL or Coq, since the corresponding term-calculi can be implemented as ``normal'' @@ -2250,8 +2249,9 @@ $\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 - is in Ott work in progress. + notion of $\alpha$-equivalence. Also the definition for the + notion of free variables + is work in progress. Although we were heavily inspired by the syntax of Ott, its definition of $\alpha$-equivalence is unsuitable for our extension of