# HG changeset patch # User Christian Urban # Date 1299024388 0 # Node ID 61d30863e5d159c683fe75f03965ad427d7c3eac # Parent d97e04126a3dab5dd0690caed97c7ccc108e497f updated pearl papers diff -r d97e04126a3d -r 61d30863e5d1 Pearl-jv/Paper.thy --- a/Pearl-jv/Paper.thy Tue Mar 01 00:14:02 2011 +0000 +++ b/Pearl-jv/Paper.thy Wed Mar 02 00:06:28 2011 +0000 @@ -1,7 +1,6 @@ (*<*) theory Paper imports "../Nominal/Nominal2_Base" - "../Nominal/Nominal2_Eqvt" "../Nominal/Atoms" "../Nominal/Nominal2_Abs" "LaTeXsugar" @@ -41,15 +40,11 @@ (*>*) -(* - TODO: write about supp of finite sets, abstraction over finite sets -*) - section {* Introduction *} text {* Nominal Isabelle provides a proving infratructure for convenient reasoning - about programming language calculi involving binders such as lambda abstractions or + about programming language calculi involving binders, such as lambda abstractions or quantifications in type schemes: \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% @@ -59,129 +54,14 @@ \noindent At its core Nominal Isabelle is based on the nominal logic work by Pitts at - al \cite{GabbayPitts02,Pitts03}. The most basic notion in this work is a + al \cite{GabbayPitts02,Pitts03}, whose most basic notion is a sort-respecting permutation operation defined over a countably infinite - collection of sorted atoms. The atoms are used for representing variable names - that might be bound or free. Multiple sorts are necessary for being able to - represent different kinds of variables. For example, in the language Mini-ML - there are bound term variables in lambda abstractions and bound type variables in - type schemes. In order to be able to separate them, each kind of variables needs to be - represented by a different sort of atoms. - - The existing nominal logic work usually leaves implicit the sorting - information for atoms and as far as we know leaves out a description of how - sorts are represented. In our formalisation, we therefore have to make a - design decision about how to implement sorted atoms and sort-respecting - permutations. One possibility, which we described in \cite{Urban08}, is to - have separate types for the different - kinds of atoms, say types @{text "\\<^isub>1,\,\\<^isub>n"}. With this - design one can represent permutations as lists of pairs of atoms and the - operation of applying a permutation to an object as the function - - - @{text [display,indent=10] "_ \ _ :: (\ \ \) list \ \ \ \"} - - \noindent - where @{text "\"} stands for a type of atoms and @{text "\"} for the type - of the objects on which the permutation acts. For atoms - the permutation operation is defined over the length of lists as follows - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} - @{text "[] \ c"} & @{text "="} & @{text c}\\ - @{text "(a b)::\ \ c"} & @{text "="} & - $\begin{cases} @{text a} & \textrm{if}~@{text "\ \ c = b"}\\ - @{text b} & \textrm{if}~@{text "\ \ c = a"}\\ - @{text "\ \ c"} & \textrm{otherwise}\end{cases}$ - \end{tabular}\hfill\numbered{atomperm} - \end{isabelle} - - \noindent - where we write @{text "(a b)"} for a swapping of atoms @{text "a"} and - @{text "b"}. For atoms with different type than the permutation, we - define @{text "\ \ c \ c"}. - - With the separate atom types and the list representation of permutations it - is impossible in systems like Isabelle/HOL to state an ``ill-sorted'' - permutation, since the type system excludes lists containing atoms of - different type. However, a disadvantage is that whenever we need to - generalise induction hypotheses by quantifying over permutations, we have to - build quantifications like - - @{text [display,indent=10] "\\\<^isub>1 \ \\\<^isub>n. \"} - - \noindent - where the @{text "\\<^isub>i"} are of type @{text "(\\<^isub>i \ \\<^isub>i) list"}. - The reason is that the permutation operation behaves differently for - every @{text "\\<^isub>i"} and the type system does not allow use to have a - single quantification to stand for all permutations. Similarly, the - notion of support - - @{text [display,indent=10] "supp _ :: \ \ \ set"} - - \noindent - which we will define later, cannot be - used to express the support of an object over \emph{all} atoms. The reason - is that support can behave differently for each @{text - "\\<^isub>i"}. This problem is annoying, because if we need to know in - a statement that an object, say @{text "x"}, is finitely supported we end up - with having to state premises of the form - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}l} - @{text "finite ((supp x) :: \\<^isub>1 set) , \, finite ((supp x) :: \\<^isub>n set)"} - \end{tabular}\hfill\numbered{fssequence} - \end{isabelle} - - \noindent - Because of these disadvantages, we will use in this paper a single unified atom type to - represent atoms of different sorts. Consequently, we have to deal with the - case that a swapping of two atoms is ill-sorted: we cannot rely anymore on - the type systems to exclude them. - - We also will not represent permutations as lists of pairs of atoms (as done in - \cite{Urban08}). Although an - advantage of this representation is that the basic operations on - permutations are already defined in Isabelle's list library: composition of - two permutations (written @{text "_ @ _"}) is just list append, and - inversion of a permutation (written @{text "_\<^sup>-\<^sup>1"}) is just - list reversal, and another advantage is that there is a well-understood - induction principle for lists, a disadvantage is that permutations - do not have unique representations as lists. We have to explicitly identify - them according to the relation + collection of sorted atoms. The nominal logic work has been starting + point for a number of formalisations, most notable Norrish \cite{norrish04} + in HOL4, Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and our own + work in Isabelle/HOL. - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}l} - @{text "\\<^isub>1 \ \\<^isub>2 \ \a. \\<^isub>1 \ a = \\<^isub>2 \ a"} - \end{tabular}\hfill\numbered{permequ} - \end{isabelle} - - \noindent - This is a problem when lifting the permutation operation to other types, for - example sets, functions and so on. For this we need to ensure that every definition - is well-behaved in the sense that it satisfies some - \emph{permutation properties}. In the list representation we need - to state these properties as follows: - - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}} - i) & @{text "[] \ x = x"}\\ - ii) & @{text "(\\<^isub>1 @ \\<^isub>2) \ x = \\<^isub>1 \ (\\<^isub>2 \ x)"}\\ - iii) & if @{text "\\<^isub>1 \ \\<^isub>2"} then @{text "\\<^isub>1 \ x = \\<^isub>2 \ x"} - \end{tabular}\hfill\numbered{permprops} - \end{isabelle} - - \noindent - where the last clause explicitly states that the permutation operation has - to produce the same result for related permutations. Moreover, - ``permutations-as-lists'' do not satisfy the group properties. This means by - using this representation we will not be able to reuse the extensive - reasoning infrastructure in Isabelle about groups. Because of this, we will represent - in this paper permutations as functions from atoms to atoms. This representation - is unique and satisfies the laws of non-commutative groups. - Using a single atom type to represent atoms of different sorts and representing permutations as functions are not new ideas; see \cite{GunterOsbornPopescu09} \footnote{function rep.} The main contribution @@ -199,6 +79,24 @@ section {* Sorted Atoms and Sort-Respecting Permutations *} text {* + The most basic notion in this work is a + sort-respecting permutation operation defined over a countably infinite + collection of sorted atoms. The atoms are used for representing variable names + that might be bound or free. Multiple sorts are necessary for being able to + represent different kinds of variables. For example, in the language Mini-ML + there are bound term variables in lambda abstractions and bound type variables in + type schemes. In order to be able to separate them, each kind of variables needs to be + represented by a different sort of atoms. + + + The existing nominal logic work usually leaves implicit the sorting + information for atoms and as far as we know leaves out a description of how + sorts are represented. In our formalisation, we therefore have to make a + design decision about how to implement sorted atoms and sort-respecting + permutations. One possibility, which we described in \cite{Urban08}, is to + have separate types for the different + kinds of atoms, say types @{text "\\<^isub>1,\,\\<^isub>n"}. + In the nominal logic work of Pitts, binders and bound variables are represented by \emph{atoms}. As stated above, we need to have different \emph{sorts} of atoms to be able to bind different kinds of variables. A @@ -314,7 +212,7 @@ @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm} @{thm plus_perm_def[where p="\\<^isub>1" and q="\\<^isub>2", THEN eq_reflection]} \hspace{4mm} @{thm uminus_perm_def[where p="\", THEN eq_reflection]} \hspace{4mm} - @{thm diff_def[where M="\\<^isub>1" and N="\\<^isub>2"]} + @{thm minus_perm_def[where ?p1.0="\\<^isub>1" and ?p2.0="\\<^isub>2"]} \end{tabular} \end{isabelle} @@ -1202,184 +1100,123 @@ *} -section {* Multi-Sorted Concrete Atoms *} - -(*<*) -datatype ty = TVar string | Fun ty ty ("_ \ _") -(*>*) - -text {* - The formalisation presented so far allows us to streamline proofs and reduce - the amount of custom ML-code in the existing implementation of Nominal - Isabelle. In this section we describe a mechanism that extends the - capabilities of Nominal Isabelle. This mechanism is about variables with - additional information, for example typing constraints. - While we leave a detailed treatment of binders and binding of variables for a - later paper, we will have a look here at how such variables can be - represented by concrete atoms. - - In the previous section we considered concrete atoms that can be used in - simple binders like \emph{@{text "\x. x"}}. Such concrete atoms do - not carry any information beyond their identities---comparing for equality - is really the only way to analyse ordinary concrete atoms. - However, in ``Church-style'' lambda-terms \cite{Church40} and in the terms - underlying HOL-systems \cite{PittsHOL4} binders and bound variables have a - more complicated structure. For example in the ``Church-style'' lambda-term - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}l} - @{text "\x\<^isub>\. x\<^isub>\ x\<^isub>\"} - \end{tabular}\hfill\numbered{church} - \end{isabelle} - - \noindent - both variables and binders include typing information indicated by @{text \} - and @{text \}. In this setting, we treat @{text "x\<^isub>\"} and @{text - "x\<^isub>\"} as distinct variables (assuming @{term "\\\"}) so that the - variable @{text "x\<^isub>\"} is bound by the lambda-abstraction, but not - @{text "x\<^isub>\"}. - - To illustrate how we can deal with this phenomenon, let us represent object - types like @{text \} and @{text \} by the datatype - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}l} - \isacommand{datatype}~~@{text "ty = TVar string | ty \ ty"} - \end{tabular} - \end{isabelle} - - \noindent - If we attempt to encode a variable naively as a pair of a @{text name} and a @{text ty}, we have the - problem that a swapping, say @{term "(x \ y)"}, applied to the pair @{text "((x, \), (x, \))"} - will always permute \emph{both} occurrences of @{text x}, even if the types - @{text "\"} and @{text "\"} are different. This is unwanted, because it will - eventually mean that both occurrences of @{text x} will become bound by a - corresponding binder. - - Another attempt might be to define variables as an instance of the concrete - atom type class, where a @{text ty} is somehow encoded within each variable. - Remember we defined atoms as the datatype: -*} - - datatype atom\\ = Atom\\ string nat - -text {* - \noindent - Considering our method of defining concrete atom types, the usage of a string - for the sort of atoms seems a natural choice. However, none of the results so - far depend on this choice and we are free to change it. - One possibility is to encode types or any other information by making the sort - argument parametric as follows: -*} - - datatype 'a \atom\\\ = \Atom\\ 'a nat - -text {* - \noindent - The problem with this possibility is that we are then back in the old - situation where our permutation operation is parametric in two types and - this would require to work around Isabelle/HOL's restriction on type - classes. Fortunately, encoding the types in a separate parameter is not - necessary for what we want to achieve, as we only have to know when two - types are equal or not. The solution is to use a different sort for each - object type. Then we can use the fact that permutations respect \emph{sorts} to - ensure that permutations also respect \emph{object types}. In order to do - this, we must define an injective function @{text "sort_ty"} mapping from - object types to sorts. For defining functions like @{text "sort_ty"}, it is - more convenient to use a tree datatype for sorts. Therefore we define -*} - - datatype sort = Sort string "(sort list)" - datatype atom\\\\ = Atom\\\\ sort nat - -text {* - \noindent - With this definition, - the sorts we considered so far can be encoded just as \mbox{@{text "Sort s []"}}. - The point, however, is that we can now define the function @{text sort_ty} simply as - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}l} - @{text "sort_ty (TVar s) = Sort ''TVar'' [Sort s []]"}\\ - @{text "sort_ty (\\<^isub>1 \ \\<^isub>2) = Sort ''Fun'' [sort_ty \\<^isub>1, sort_ty \\<^isub>2]"} - \end{tabular}\hfill\numbered{sortty} - \end{isabelle} - - \noindent - which can easily be shown to be injective. - - Having settled on what the sorts should be for ``Church-like'' atoms, we have to - give a subtype definition for concrete atoms. Previously we identified a subtype consisting - of atoms of only one specified sort. This must be generalised to all sorts the - function @{text "sort_ty"} might produce, i.e.~the - range of @{text "sort_ty"}. Therefore we define - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \isacommand{typedef}\ \ @{text var} = @{term "{a. sort a : range sort_ty}"} - \end{isabelle} - - \noindent - This command gives us again injective representation and abstraction - functions. We will write them also as \mbox{@{text "\_\ :: var \ atom"}} and - @{text "\_\ :: atom \ var"}, respectively. - - We can define the permutation operation for @{text var} as @{thm - permute_var_def[where p="\", THEN eq_reflection, no_vars]} and the - injective function to type @{typ atom} as @{thm atom_var_def[THEN - eq_reflection, no_vars]}. Finally, we can define a constructor function that - makes a @{text var} from a variable name and an object type: - - @{thm [display,indent=10] Var_def[where t="\", THEN eq_reflection, no_vars]} - - \noindent - With these definitions we can verify all the properties for concrete atom - types except Property \ref{atomprops}@{text ".iii)"}, which requires every - atom to have the same sort. This last property is clearly not true for type - @{text "var"}. - This fact is slightly unfortunate since this - property allowed us to use the type-checker in order to shield the user from - all sort-constraints. But this failure is expected here, because we cannot - burden the type-system of Isabelle/HOL with the task of deciding when two - object types are equal. This means we sometimes need to explicitly state sort - constraints or explicitly discharge them, but as we will see in the lemma - below this seems a natural price to pay in these circumstances. - - To sum up this section, the encoding of type-information into atoms allows us - to form the swapping @{term "(Var x \ \ Var y \)"} and to prove the following - lemma -*} - - lemma - assumes asm: "\ \ \" - shows "(Var x \ \ Var y \) \ (Var x \, Var x \) = (Var y \, Var x \)" - using asm by simp - -text {* - \noindent - As we expect, the atom @{term "Var x \"} is left unchanged by the - swapping. With this we can faithfully represent bindings in languages - involving ``Church-style'' terms and bindings as shown in \eqref{church}. We - expect that the creation of such atoms can be easily automated so that the - user just needs to specify \isacommand{atom\_decl}~~@{text "var (ty)"} - where the argument, or arguments, are datatypes for which we can automatically - define an injective function like @{text "sort_ty"} (see \eqref{sortty}). - Our hope is that with this approach Benzmueller and Paulson can make - headway with formalising their results - about simple type theory \cite{PaulsonBenzmueller}. - Because of its limitations, they did not attempt this with the old version - of Nominal Isabelle. We also hope we can make progress with formalisations of - HOL-based languages. -*} section {* Related Work *} text {* Add here comparison with old work. - The main point is that the above reasoning blends smoothly with the reasoning infrastructure of Isabelle/HOL; no custom ML-code is necessary and a single type class suffices. + + With this + design one can represent permutations as lists of pairs of atoms and the + operation of applying a permutation to an object as the function + + + @{text [display,indent=10] "_ \ _ :: (\ \ \) list \ \ \ \"} + + \noindent + where @{text "\"} stands for a type of atoms and @{text "\"} for the type + of the objects on which the permutation acts. For atoms + the permutation operation is defined over the length of lists as follows + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} + @{text "[] \ c"} & @{text "="} & @{text c}\\ + @{text "(a b)::\ \ c"} & @{text "="} & + $\begin{cases} @{text a} & \textrm{if}~@{text "\ \ c = b"}\\ + @{text b} & \textrm{if}~@{text "\ \ c = a"}\\ + @{text "\ \ c"} & \textrm{otherwise}\end{cases}$ + \end{tabular}\hfill\numbered{atomperm} + \end{isabelle} + + \noindent + where we write @{text "(a b)"} for a swapping of atoms @{text "a"} and + @{text "b"}. For atoms with different type than the permutation, we + define @{text "\ \ c \ c"}. + + With the separate atom types and the list representation of permutations it + is impossible in systems like Isabelle/HOL to state an ``ill-sorted'' + permutation, since the type system excludes lists containing atoms of + different type. However, a disadvantage is that whenever we need to + generalise induction hypotheses by quantifying over permutations, we have to + build quantifications like + + @{text [display,indent=10] "\\\<^isub>1 \ \\\<^isub>n. \"} + + \noindent + where the @{text "\\<^isub>i"} are of type @{text "(\\<^isub>i \ \\<^isub>i) list"}. + The reason is that the permutation operation behaves differently for + every @{text "\\<^isub>i"} and the type system does not allow use to have a + single quantification to stand for all permutations. Similarly, the + notion of support + + @{text [display,indent=10] "supp _ :: \ \ \ set"} + + \noindent + which we will define later, cannot be + used to express the support of an object over \emph{all} atoms. The reason + is that support can behave differently for each @{text + "\\<^isub>i"}. This problem is annoying, because if we need to know in + a statement that an object, say @{text "x"}, is finitely supported we end up + with having to state premises of the form + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + \begin{tabular}{@ {}l} + @{text "finite ((supp x) :: \\<^isub>1 set) , \, finite ((supp x) :: \\<^isub>n set)"} + \end{tabular}\hfill\numbered{fssequence} + \end{isabelle} + + \noindent + Because of these disadvantages, we will use in this paper a single unified atom type to + represent atoms of different sorts. Consequently, we have to deal with the + case that a swapping of two atoms is ill-sorted: we cannot rely anymore on + the type systems to exclude them. + + We also will not represent permutations as lists of pairs of atoms (as done in + \cite{Urban08}). Although an + advantage of this representation is that the basic operations on + permutations are already defined in Isabelle's list library: composition of + two permutations (written @{text "_ @ _"}) is just list append, and + inversion of a permutation (written @{text "_\<^sup>-\<^sup>1"}) is just + list reversal, and another advantage is that there is a well-understood + induction principle for lists, a disadvantage is that permutations + do not have unique representations as lists. We have to explicitly identify + them according to the relation + + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + \begin{tabular}{@ {}l} + @{text "\\<^isub>1 \ \\<^isub>2 \ \a. \\<^isub>1 \ a = \\<^isub>2 \ a"} + \end{tabular}\hfill\numbered{permequ} + \end{isabelle} + + \noindent + This is a problem when lifting the permutation operation to other types, for + example sets, functions and so on. For this we need to ensure that every definition + is well-behaved in the sense that it satisfies some + \emph{permutation properties}. In the list representation we need + to state these properties as follows: + + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}} + i) & @{text "[] \ x = x"}\\ + ii) & @{text "(\\<^isub>1 @ \\<^isub>2) \ x = \\<^isub>1 \ (\\<^isub>2 \ x)"}\\ + iii) & if @{text "\\<^isub>1 \ \\<^isub>2"} then @{text "\\<^isub>1 \ x = \\<^isub>2 \ x"} + \end{tabular}\hfill\numbered{permprops} + \end{isabelle} + + \noindent + where the last clause explicitly states that the permutation operation has + to produce the same result for related permutations. Moreover, + ``permutations-as-lists'' do not satisfy the group properties. This means by + using this representation we will not be able to reuse the extensive + reasoning infrastructure in Isabelle about groups. Because of this, we will represent + in this paper permutations as functions from atoms to atoms. This representation + is unique and satisfies the laws of non-commutative groups. *} diff -r d97e04126a3d -r 61d30863e5d1 Pearl-jv/ROOT.ML --- a/Pearl-jv/ROOT.ML Tue Mar 01 00:14:02 2011 +0000 +++ b/Pearl-jv/ROOT.ML Wed Mar 02 00:06:28 2011 +0000 @@ -1,5 +1,4 @@ no_document use_thys ["../Nominal/Nominal2_Base", - "../Nominal/Nominal2_Eqvt", "../Nominal/Atoms", "../Nominal/Nominal2_Abs", "LaTeXsugar"]; diff -r d97e04126a3d -r 61d30863e5d1 Pearl-jv/document/root.bib --- a/Pearl-jv/document/root.bib Tue Mar 01 00:14:02 2011 +0000 +++ b/Pearl-jv/document/root.bib Wed Mar 02 00:06:28 2011 +0000 @@ -8,6 +8,17 @@ year = "2008" } +@InProceedings{norrish04, + author = {M.~Norrish}, + title = {{R}ecursive {F}unction {D}efinition for {T}ypes with {B}inders}, + booktitle = {Proc.~of the 17th International Conference Theorem Proving in + Higher Order Logics (TPHOLs)}, + pages = {241--256}, + year = {2004}, + volume = {3223}, + series = {LNCS} +} + @InProceedings{GunterOsbornPopescu09, author = {E.L.~Gunter and C.J.~Osborn and A.~Popescu}, title = {{T}heory {S}upport for {W}eak {H}igher {O}rder {A}bstract {S}yntax in @@ -19,6 +30,16 @@ series = {ENTCS} } +@InProceedings{AydemirBohannonWeirich07, + author = {B.~Aydemir and A.~Bohannon and S.~Weihrich}, + title = {{N}ominal {R}easoning {T}echniques in {C}oq ({E}xtended {A}bstract)}, + booktitle = {Proc.~of the 1st International Workshop on Logical Frameworks and Meta-Languages: + Theory and Practice (LFMTP)}, + pages = {69--77}, + year = {2007}, + series = {ENTCS} +} + @Unpublished{SatoPollack10, author = {M.~Sato and R.~Pollack}, title = {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus}, diff -r d97e04126a3d -r 61d30863e5d1 Pearl-jv/document/root.tex --- a/Pearl-jv/document/root.tex Tue Mar 01 00:14:02 2011 +0000 +++ b/Pearl-jv/document/root.tex Wed Mar 02 00:06:28 2011 +0000 @@ -36,12 +36,12 @@ Pitts et al introduced a beautiful theory about names and binding based on the notions of atoms, permutations and support. The engineering challenge is to smoothly adapt this theory to a theorem prover environment, in our case -Isabelle/HOL. For this we have to make the theory compatible with choice -principles, which the work by Pitts is not. We present a formalisation of -this work that is based on a unified atom type and that represents -permutations by bijective functions from atoms to atoms. Interestingly, we -allow swappings, which are permutations build from two atoms, to be -ill-sorted. We extend the nominal logic work with a formalisation of an +Isabelle/HOL. For this we have to formulate the theory so that it is +compatible with choice principles, which the work by Pitts is not. We +present a formalisation of this work that is based on a unified atom type +and that represents permutations by bijective functions from atoms to atoms. +Interestingly, we allow swappings, which are permutations build from two +atoms, to be ill-sorted. We also describe a formalisation of an abstraction operator that binds sets of names. \end{abstract} diff -r d97e04126a3d -r 61d30863e5d1 Pearl/Paper.thy --- a/Pearl/Paper.thy Tue Mar 01 00:14:02 2011 +0000 +++ b/Pearl/Paper.thy Wed Mar 02 00:06:28 2011 +0000 @@ -1,7 +1,6 @@ (*<*) theory Paper imports "../Nominal/Nominal2_Base" - "../Nominal/Nominal2_Eqvt" "../Nominal/Atoms" "LaTeXsugar" begin @@ -346,7 +345,7 @@ @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm} @{thm plus_perm_def[where p="\\<^isub>1" and q="\\<^isub>2", THEN eq_reflection]} \hspace{4mm} @{thm uminus_perm_def[where p="\", THEN eq_reflection]} \hspace{4mm} - @{thm diff_def[where a="\\<^isub>1" and b="\\<^isub>2"]} + @{thm minus_perm_def[where ?p1.0="\\<^isub>1" and ?p2.0="\\<^isub>2"]} \end{tabular} \end{isabelle} diff -r d97e04126a3d -r 61d30863e5d1 Pearl/ROOT.ML --- a/Pearl/ROOT.ML Tue Mar 01 00:14:02 2011 +0000 +++ b/Pearl/ROOT.ML Wed Mar 02 00:06:28 2011 +0000 @@ -1,5 +1,4 @@ no_document use_thys ["../Nominal/Nominal2_Base", - "../Nominal/Nominal2_Eqvt", "../Nominal/Atoms", "LaTeXsugar"];