# HG changeset patch # User Christian Urban # Date 1290647904 0 # Node ID 6c4372a1f2204be90135bfd2bcce98bb256a3b4f # Parent 3696659358c884e87cc69cec2bb6844514b343fe# Parent d8a676a6904795f10000b4d055d6991a6553e4d8 merged diff -r d8a676a69047 -r 6c4372a1f220 Nominal/Ex/SystemFOmega.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Ex/SystemFOmega.thy Thu Nov 25 01:18:24 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 d8a676a69047 -r 6c4372a1f220 Nominal/ROOT.ML --- a/Nominal/ROOT.ML Wed Nov 24 17:44:50 2010 +0900 +++ b/Nominal/ROOT.ML Thu Nov 25 01:18:24 2010 +0000 @@ -19,6 +19,7 @@ "Ex/Modules", "Ex/SingleLet", "Ex/Shallow", + "Ex/SystemFOmega", "Ex/TypeSchemes", "Ex/TypeVarsTest", "Ex/Foo1", diff -r d8a676a69047 -r 6c4372a1f220 Paper/Paper.thy --- a/Paper/Paper.thy Wed Nov 24 17:44:50 2010 +0900 +++ b/Paper/Paper.thy Thu Nov 25 01:18:24 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