# HG changeset patch # User Christian Urban # Date 1299833499 0 # Node ID f1192e3474e02eb2cf394aa29a7fb16c407080db # Parent 651355113eeec3339315396f7667ee19c889f4e2 more on the paper diff -r 651355113eee -r f1192e3474e0 IsaMakefile --- a/IsaMakefile Tue Mar 08 09:07:49 2011 +0000 +++ b/IsaMakefile Fri Mar 11 08:51:39 2011 +0000 @@ -44,13 +44,13 @@ ## Pearl Journal Paper -pearl-jv: $(LOG)/HOL-Pearl-jv.gz +$(LOG)/HOL-Pearl-jv.gz: Pearl-jv/ROOT.ML Nominal/*.thy + @cd Pearl-jv; $(USEDIR) -b -f ROOT.ML HOL HOL-Pearl-jv -$(LOG)/HOL-Pearl-jv.gz: Pearl-jv/ROOT.ML Pearl-jv/document/root.* Pearl-jv/*.thy - @$(USEDIR) -D generated HOL Pearl-jv - $(ISABELLE_TOOL) document -o pdf Pearl-jv/generated - @cp Pearl-jv/document.pdf pearl-jv.pdf - +pearl-jv: $(LOG)/HOL-Pearl-jv.gz Pearl-jv/ROOT2.ML Pearl-jv/document/root.* Pearl-jv/*.thy + @$(USEDIR) -f ROOT2.ML -D generated HOL-Pearl-jv Pearl-jv + @$(ISABELLE_TOOL) document -o pdf Pearl-jv/generated + @cp Pearl-jv/document.pdf pearl-jv.pdf ## Quotient Paper diff -r 651355113eee -r f1192e3474e0 Nominal/Nominal2_Base.thy --- a/Nominal/Nominal2_Base.thy Tue Mar 08 09:07:49 2011 +0000 +++ b/Nominal/Nominal2_Base.thy Fri Mar 11 08:51:39 2011 +0000 @@ -34,7 +34,7 @@ primrec sort_of :: "atom \ atom_sort" where - "sort_of (Atom s i) = s" + "sort_of (Atom s n) = s" primrec nat_of :: "atom \ nat" @@ -1121,9 +1121,7 @@ lemma supp_eqvt [eqvt]: shows "p \ (supp x) = supp (p \ x)" unfolding supp_conv_fresh - unfolding Collect_def - unfolding permute_fun_def - by (simp add: Not_eqvt fresh_eqvt) + by (perm_simp) (rule refl) lemma fresh_permute_left: shows "a \ p \ x \ - p \ a \ x" @@ -1720,6 +1718,18 @@ apply(simp add: swap_set_in) done +lemma supp_cofinite_atom_set: + fixes S::"atom set" + assumes "finite (UNIV - S)" + shows "supp S = (UNIV - S)" + apply(rule finite_supp_unique) + apply(simp add: supports_def) + apply(simp add: swap_set_both_in) + apply(rule assms) + apply(subst swap_commute) + apply(simp add: swap_set_in) +done + lemma fresh_finite_atom_set: fixes S::"atom set" assumes "finite S" diff -r 651355113eee -r f1192e3474e0 Paper/Paper.thy --- a/Paper/Paper.thy Tue Mar 08 09:07:49 2011 +0000 +++ b/Paper/Paper.thy Fri Mar 11 08:51:39 2011 +0000 @@ -2185,7 +2185,7 @@ *} -section {* Related Work *} +section {* Related Work\label{related} *} text {* To our knowledge the earliest usage of general binders in a theorem prover diff -r 651355113eee -r f1192e3474e0 Pearl-jv/Paper.thy --- a/Pearl-jv/Paper.thy Tue Mar 08 09:07:49 2011 +0000 +++ b/Pearl-jv/Paper.thy Fri Mar 11 08:51:39 2011 +0000 @@ -6,6 +6,11 @@ "LaTeXsugar" begin +abbreviation + UNIV_atom ("\") +where + "UNIV_atom \ UNIV::atom set" + notation (latex output) sort_of ("sort _" [1000] 100) and Abs_perm ("_") and @@ -22,7 +27,7 @@ Abs_name ("\_\") and Rep_var ("\_\") and Abs_var ("\_\") and - sort_of_ty ("sort'_ty _") + sort_of_ty ("sort'_ty _") (* BH: uncomment if you really prefer the dot notation syntax (latex output) @@ -35,8 +40,16 @@ abbreviation "sort \ sort_of" -abbreviation - "sort_ty \ sort_of_ty" +lemma infinite_collect: + assumes "\x \ S. P x" "infinite S" + shows "infinite {x \ S. P x}" +using assms +apply(subgoal_tac "infinite {x. x \ S}") +apply(simp only: Inf_many_def[symmetric]) +apply(erule INFM_mono) +apply(auto) +done + (*>*) @@ -47,8 +60,7 @@ about syntax involving binders, such as lambda terms or type schemes: \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - @{text "\x. t \{x\<^isub>1,\, x\<^isub>n}. \"} - \hfill\numbered{atomperm} + @{text "\x. t \{x\<^isub>1,\, x\<^isub>n}. \"} \end{isabelle} \noindent @@ -64,20 +76,21 @@ The nominal logic work has been the starting point for a number of proving infrastructures, most notable by Norrish \cite{norrish04} in HOL4, by - Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and teh work by Urban + Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and the work by Urban and Berghofer in Isabelle/HOL \cite{Urban08}. Its key attraction is a very general notion, called \emph{support}, for the `set of free variables, or - atoms' of an object that applies not just to lambda terms and type schemes, - but also to sets, products, lists and even functions. The notion of support - is derived from the permutation operation defined over atoms. This - permutation operation, written @{text "_ \ _"}, has proved to be very + atoms, of an object' that applies not just to lambda terms and type schemes, + but also to sets, products, lists, booleans and even functions. The notion of support + is derived from the permutation operation defined over the + hierarchy of types. This + permutation operation, written @{text "_ \ _"}, has proved to be much more convenient for reasoning about syntax, in comparison to, say, arbitrary - renaming substitutions of atoms. The reason is that permutations are + renaming substitutions of atoms. One reason is that permutations are bijective renamings of atoms and thus they can be easily `undone'---namely by applying the inverse permutation. A corresponding inverse substitution - might not exist in general, since renaming substitutions are only injective. - Permutations also preserve many constructions when reasoning about syntax. - For example validity of a typing context is preserved under permutations. + might not always exist, since renaming substitutions are in general only injective. + Another reason is that permutations preserve many constructions when reasoning about syntax. + For example the validity of a typing context is preserved under any permutation. Suppose a typing context @{text "\"} of the form \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% @@ -88,38 +101,54 @@ is said to be \emph{valid} provided none of its variables, or atoms, @{text "x\<^isub>i"} occur twice. Then validity is preserved under permutations in the sense that if @{text \} is valid then so is @{text "\ \ \"} for - all permutations @{text "\"}. This is \emph{not} the case for arbitrary - renaming substitutions, as they might identify some variables in @{text \}. - Permutations fit well with HOL's definitions. For example + all permutations @{text "\"}. This is again \emph{not} the case for arbitrary + renaming substitutions, as they might identify some of the @{text "x\<^isub>i"} in @{text \}. + + Permutations also behave uniformly with respect to HOL's logic connectives. + Applying a permutation to a formula gives, for example + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + \begin{tabular}{@ {}lcl} + @{term "\ \ (A \ B)"} & if and only if & @{text "(\ \ A) \ (\ \ B)"}\\ + @{term "\ \ (A \ B)"} & if and only if & @{text "(\ \ A) \ (\ \ B)"}\\ + \end{tabular} + \end{isabelle} - Because - of the good properties of permutations, we will be able to automate reasoning - steps determining when a construction in HOL is - \emph{equivariant}. By equivariance we mean the property that every - permutation leaves an object unchanged, that is @{term "\\. \ \ x = x"}. - This will often simplify arguments involving the notion of support. + \noindent + This uniform behaviour can also be extended to quantifiers and functions. + Because of these good properties of permutations, we are able to automate + reasoning to do with \emph{equivariance}. By equivariance we mean the property + that every permutation leaves an object unchanged, that is @{term "\ \ x = x"} + for all @{text "\"}. This will often simplify arguments involving support + and functions, since equivariant objects have empty support---or + `no free atoms'. + + There are a number of subtle differences between the nominal logic work by + Pitts and the formalisation we will present in this paper. One difference + is that our + formalisation is compatible with HOL, in the sense that we only extend + HOL by some definitions, withouth the introduction of any new axioms. + The reason why the original nominal logic work is + incompatible with HOL has to do with the way how the finite support property + is enforced: FM-set theory is defined in \cite{Pitts01b} so that every set + in the FM-set-universe has finite support. In nominal logic \cite{Pitts03}, + the axioms (E3) and (E4) imply that every function symbol and proposition + has finite support. However, there are notions in HOL that do \emph{not} + have finite support (we will give some examples). In our formalisation, we + will avoid the incompatibility of the original nominal logic work by not a + priory restricting our discourse to only finitely supported entities, rather + we will explicitly assume this property whenever it is needed in proofs. One + consequence is that we state our basic definitions not in terms of nominal + sets (as done for example in \cite{Pitts06}), but in terms of the weaker + notion of permutation types---essentially sets equipped with a ``sensible'' + notion of permutation operation. - There are a number of subtle differences between the nominal logic work by Pitts - and the one we will present in this paper. Nominal - In the nominal logic work, the `new quantifier' plays a prominent role. - + In the nominal logic woworkrk, the `new quantifier' plays a prominent role. + $\new$ - 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 - of this paper is to show an example of how to make better theorem proving - tools by choosing the right level of abstraction for the underlying - theory---our design choices take advantage of Isabelle's type system, type - classes and reasoning infrastructure. The novel technical contribution is a - mechanism for dealing with ``Church-style'' lambda-terms \cite{Church40} and - HOL-based languages \cite{PittsHOL4} where variables and variable binding - depend on type annotations. - - The paper is organised as follows\ldots Two binders @@ -128,21 +157,19 @@ section {* Sorted Atoms and Sort-Respecting Permutations *} text {* - The two most basic notions in the nominal logic work are - sort-respecting permutation operation defined over a countably infinite - collection of sorted 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"}. However, this does not blend well with the - resoning infrastructure of type-classes in Isabelle/HOL (see Section ??? - about related work). Therefore we use here a single unified atom type to - represent atoms of different sorts. A basic requirement is that there must - be a countably infinite number of atoms of each sort. This can be - implemented as the datatype + The two most basic notions in the nominal logic work are a countably + infinite collection of sorted atoms and sort-respecting permutations. + 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 sorts of + atoms. However, we found that this does not blend well with type-classes in + Isabelle/HOL (see Section~\ref{related} about related work). Therefore we use here a + single unified atom type to represent atoms of different sorts. A basic + requirement is that there must be a countably infinite number of atoms of + each sort. This can be implemented as the datatype *} @@ -153,15 +180,20 @@ whereby the string argument specifies the sort of the atom.\footnote{A similar design choice was made by Gunter et al \cite{GunterOsbornPopescu09} for their variables.} The use of type \emph{string} for sorts is merely for - convenience; any countably infinite type would work as well. We have an - auxiliary function @{text sort} that is defined as + convenience; any countably infinite type would work as well. + The set of all atoms we shall write as @{term "UNIV::atom set"}. + We have two + auxiliary functions @{text sort} and @{const nat_of} that are defined as \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - @{thm sort_of.simps[no_vars, THEN eq_reflection]} + \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} + @{thm (lhs) sort_of.simps[no_vars]} & @{text "\"} & @{thm (rhs) sort_of.simps[no_vars]}\\ + @{thm (lhs) nat_of.simps[no_vars]} & @{text "\"} & @{thm (rhs) nat_of.simps[no_vars]} + \end{tabular}\hfill\numbered{sortnatof} \end{isabelle} \noindent - and we clearly have for every finite set @{text S} + We clearly have for every finite set @{text S} of atoms and every sort @{text s} the property: \begin{proposition}\label{choosefresh}\mbox{}\\ @@ -173,7 +205,7 @@ "atom => atom"} that @{text "i)"} are bijective; @{text "ii)"} are the identity on all atoms, except a finite number of them; and @{text "iii)"} map each atom to one of the same sort. These properties can be conveniently stated - for a function @{text \} as follows: + in Isabelle/HOL for a function @{text \} as follows: \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{r@ {\hspace{4mm}}l} @@ -202,29 +234,27 @@ \noindent but since permutations are required to respect sorts, we must carefully consider what happens if a user states a swapping of atoms with different - sorts. In early versions of Nominal Isabelle, we avoided this problem by - using different types for different sorts; the type system prevented users - from stating ill-sorted swappings. Here, however, definitions such - as\footnote{To increase legibility, we omit here and in what follows the - @{term Rep_perm} and @{term "Abs_perm"} wrappers that are needed in our - implementation since we defined permutation not to be the full function space, - but only those functions of type @{typ perm} satisfying properties @{text - i}-@{text "iii"}.} + sorts. The following definition\footnote{To increase legibility, we omit + here and in what follows the @{term Rep_perm} and @{term "Abs_perm"} + wrappers that are needed in our implementation since we defined permutation + not to be the full function space, but only those functions of type @{typ + perm} satisfying properties @{text i}-@{text "iii"} in \eqref{permtype}.} + @{text [display,indent=10] "(a b) \ \c. if a = c then b else (if b = c then a else c)"} \noindent - do not work in general, because the type system does not prevent @{text a} - and @{text b} from having different sorts---in which case the function would - violate property @{text iii}. We could make the definition of swappings - partial by adding the precondition @{term "sort a = sort b"}, - which would mean that in case @{text a} and @{text b} have different sorts, - the value of @{text "(a b)"} is unspecified. However, this looked like a - cumbersome solution, since sort-related side conditions would be required - everywhere, even to unfold the definition. It turned out to be more - convenient to actually allow the user to state `ill-sorted' swappings but - limit their `damage' by defaulting to the identity permutation in the - ill-sorted case: + does not work in general, because @{text a} and @{text b} may have different + sorts---in which case the function would violate property @{text iii} in \eqref{permtype}. We + could make the definition of swappings partial by adding the precondition + @{term "sort a = sort b"}, which would mean that in case @{text a} and + @{text b} have different sorts, the value of @{text "(a b)"} is unspecified. + However, this looked like a cumbersome solution, since sort-related side + conditions would be required everywhere, even to unfold the definition. It + turned out to be more convenient to actually allow the user to state + `ill-sorted' swappings but limit their `damage' by defaulting to the + identity permutation in the ill-sorted case: + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}rl} @@ -240,7 +270,7 @@ a function in @{typ perm}. One advantage of using functions as a representation for - permutations is that for example the swappings + permutations is that it is unique. For example the swappings \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}l} @@ -250,29 +280,28 @@ \end{isabelle} \noindent - are \emph{equal}. Therfore we can use for permutations HOL's built-in - principle of `replacing equals by equals in any context'. Another advantage - of the function representation is that they form a (non-commutative) group - provided we define + are \emph{equal}. Another advantage of the function representation is that + they form a (non-com\-mu\-ta\-tive) group provided we define + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{10mm}}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} + @{thm (lhs) zero_perm_def[no_vars]} & @{text "\"} & @{thm (rhs) zero_perm_def[no_vars]} & + @{thm (lhs) plus_perm_def[where p="\\<^isub>1" and q="\\<^isub>2"]} & @{text "\"} & + @{thm (rhs) plus_perm_def[where p="\\<^isub>1" and q="\\<^isub>2"]}\\ + @{thm (lhs) uminus_perm_def[where p="\"]} & @{text "\"} & @{thm (rhs) uminus_perm_def[where p="\"]} & + @{thm (lhs) minus_perm_def[where ?p1.0="\\<^isub>1" and ?p2.0="\\<^isub>2"]} & @{text "\"} & + @{thm (rhs) minus_perm_def[where ?p1.0="\\<^isub>1" and ?p2.0="\\<^isub>2"]} + \end{tabular}\hfill\numbered{groupprops} + \end{isabelle} + + \noindent + and verify the four simple properties \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}l} - @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{5mm} - @{thm plus_perm_def[where p="\\<^isub>1" and q="\\<^isub>2", THEN eq_reflection]} \hspace{5mm} - @{thm uminus_perm_def[where p="\", THEN eq_reflection]} \hspace{5mm} - @{thm minus_perm_def[where ?p1.0="\\<^isub>1" and ?p2.0="\\<^isub>2"]} - \end{tabular} - \end{isabelle} - - \noindent - and verify the simple properties - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}l} - @{thm add_assoc[where a="\\<^isub>1" and b="\\<^isub>2" and c="\\<^isub>3"]} \hspace{5mm} - @{thm monoid_add_class.add_0_left[where a="\::perm"]} \hspace{5mm} - @{thm monoid_add_class.add_0_right[where a="\::perm"]} \hspace{5mm} + @{thm add_assoc[where a="\\<^isub>1" and b="\\<^isub>2" and c="\\<^isub>3"]}\\ + @{thm monoid_add_class.add_0_left[where a="\::perm"]} \hspace{9mm} + @{thm monoid_add_class.add_0_right[where a="\::perm"]} \hspace{9mm} @{thm group_add_class.left_minus[where a="\::perm"]} \end{tabular} \end{isabelle} @@ -288,8 +317,9 @@ nominal theory as smoothly as possible in Isabelle/HOL, we tolerate the non-standard notation in order to reuse the existing libraries. - In order to reason abstractly about permutations, we state the following two - \emph{permutation properties} + In order to reason abstractly about permutations, we use Isabelle/HOL's + type classes~\cite{Wenzel04} and state the following two + \emph{permutation properties}: \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}} @@ -299,20 +329,20 @@ \end{isabelle} \noindent - We state these properties in terms of Isabelle/HOL's type class - mechanism \cite{}. - This allows us to delegate much of the resoning involved in - determining whether these properties are satisfied to the type system. - For this we define + The use of type classes allows us to delegate much of the routine resoning involved in + determining whether these properties are satisfied to Isabelle/HOL's type system: + we only have to establish that `base' types, such as @{text booleans} and + @{text atoms}, satisfy them and that type-constructors, such as products and lists, + preserve them. For this we define - \begin{definition} + \begin{definition}[Permutation type] A type @{text "\"} is a \emph{permutation type} if the permutation properties in \eqref{newpermprops} are satisfied for every @{text "x"} of type @{text "\"}. \end{definition} \noindent - The type class also allows us to establish generic lemmas involving the + The type classes also allows us to establish generic lemmas involving the permutation operation. First, it follows from the laws governing groups that a permutation and its inverse cancel each other. That is, for any @{text "x"} of a permutation type: @@ -326,7 +356,6 @@ \end{isabelle} \noindent - ??? Proof Consequently, in a permutation type the permutation operation @{text "\ \ _"}~~is bijective, which in turn implies the property @@ -337,43 +366,23 @@ @{thm (rhs) permute_eq_iff[where p="\", no_vars]}. \end{tabular}\hfill\numbered{permuteequ} \end{isabelle} - - \noindent - We can also show that the following property holds for any permutation type. - - \begin{lemma}\label{permutecompose} - Given @{term x} is of permutation type, then - @{text "\\<^isub>1 \ (\\<^isub>2 \ x) = (\\<^isub>1 \ \\<^isub>2) \ (\\<^isub>1 \ x)"}. - \end{lemma} - - \begin{proof} The proof is as follows: - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}[b]{@ {}rcl@ {\hspace{8mm}}l} - @{text "\\<^isub>1 \ \\<^isub>2 \ x"} - & @{text "="} & @{text "\\<^isub>1 \ \\<^isub>2 \ (-\\<^isub>1) \ \\<^isub>1 \ x"} & by \eqref{cancel}\\ - & @{text "="} & @{text "(\\<^isub>1 + \\<^isub>2 - \\<^isub>1) \ \\<^isub>1 \ x"} & by {\rm(\ref{newpermprops}.@{text "ii"})}\\ - & @{text "\"} & @{text "(\\<^isub>1 \ \\<^isub>2) \ (\\<^isub>1 \ x)"}\\ - \end{tabular}\hfill\qed - \end{isabelle} - \end{proof} \noindent In order to lift the permutation operation to other types, we can define for: - \begin{equation}\label{permdefs} - \mbox{ - \begin{tabular}{@ {}ll@ {\hspace{4mm}}l@ {}} - a) & atoms: & @{thm permute_atom_def[where p="\",no_vars, THEN eq_reflection]}\\ - b) & functions: & @{text "\ \ f \ \x. \ \ (f ((-\) \ x))"}\\ - c) & permutations: & @{thm permute_perm_def[where p="\" and q="\'", THEN eq_reflection]}\\ - d) & sets: & @{thm permute_set_eq[where p="\", no_vars, THEN eq_reflection]}\\ - e) & booleans: & @{thm permute_bool_def[where p="\", no_vars, THEN eq_reflection]}\\ - f) & lists: & @{thm permute_list.simps(1)[where p="\", no_vars, THEN eq_reflection]}\\ - & & @{thm permute_list.simps(2)[where p="\", no_vars, THEN eq_reflection]}\\ - g) & products: & @{thm permute_prod.simps[where p="\", no_vars, THEN eq_reflection]}\\ - h) & nats: & @{thm permute_nat_def[where p="\", no_vars, THEN eq_reflection]}\\ - \end{tabular}} - \end{equation} + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + \begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}} + atoms: & @{thm permute_atom_def[where p="\",no_vars, THEN eq_reflection]}\\ + functions: & @{text "\ \ f \ \x. \ \ (f ((-\) \ x))"}\\ + permutations: & @{thm permute_perm_def[where p="\" and q="\'", THEN eq_reflection]}\\ + sets: & @{thm permute_set_eq[where p="\", no_vars, THEN eq_reflection]}\\ + booleans: & @{thm permute_bool_def[where p="\", no_vars, THEN eq_reflection]}\\ + lists: & @{thm permute_list.simps(1)[where p="\", no_vars, THEN eq_reflection]}\\ + & @{thm permute_list.simps(2)[where p="\", no_vars, THEN eq_reflection]}\\ + products: & @{thm permute_prod.simps[where p="\", no_vars, THEN eq_reflection]}\\ + nats: & @{thm permute_nat_def[where p="\", no_vars, THEN eq_reflection]}\\ + \end{tabular}\hfill\numbered{permdefs} + \end{isabelle} \noindent and then establish: @@ -399,18 +408,48 @@ \end{tabular}\hfill\qed \end{isabelle} \end{proof} + + \noindent + Note that the permutation operation for functions is defined so that we have the property + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + @{text "\ \ (f x) ="} + @{thm (rhs) permute_fun_app_eq[where p="\", no_vars]} + \hfill\numbered{permutefunapp} + \end{isabelle} + + \noindent + which is a simple consequence of the definition and the cancellation property in \eqref{cancel}. + We can also show that the following property holds for any permutation type. + + \begin{lemma}\label{permutecompose} + Given @{term x} is of permutation type, then + @{text "\\<^isub>1 \ (\\<^isub>2 \ x) = (\\<^isub>1 \ \\<^isub>2) \ (\\<^isub>1 \ x)"}. + \end{lemma} + + \begin{proof} The proof is as follows: + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + \begin{tabular}[b]{@ {}c@ {\hspace{2mm}}l@ {\hspace{8mm}}l} + & @{text "\\<^isub>1 \ \\<^isub>2 \ x"}\\ + @{text "="} & @{text "\\<^isub>1 \ \\<^isub>2 \ (-\\<^isub>1) \ (\\<^isub>1 \ x)"} & by \eqref{cancel}\\ + @{text "="} & @{text "(\\<^isub>1 + \\<^isub>2 - \\<^isub>1) \ (\\<^isub>1 \ x)"} & by {\rm(\ref{newpermprops}.@{text "ii"})}\\ + @{text "\"} & @{text "(\\<^isub>1 \ \\<^isub>2) \ (\\<^isub>1 \ x)"}\\ + \end{tabular}\hfill\qed + \end{isabelle} + \end{proof} + *} section {* Equivariance *} text {* An important notion in the nominal logic work is \emph{equivariance}. - An equivariant function or predicate is one that is invariant under - the swapping of atoms. This notion can be defined + An equivariant function is one that is invariant under + permutations of atoms. This notion can be defined uniformly as follows: - \begin{definition}\label{equivariance} + \begin{definition}[Equivariance]\label{equivariance} A function @{text f} is \emph{equivariant} if @{term "\\. \ \ f = f"}. \end{definition} @@ -429,28 +468,12 @@ To see that this formulation implies the definition, we just unfold the definition of the permutation operation for functions and simplify with the equation and the cancellation property shown in \eqref{cancel}. To see the other direction, we use - the fact - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}l} - @{text "\ \ (f x) = (\ \ f) (\ \ x)"} - \end{tabular}\hfill\numbered{permutefunapp} - \end{isabelle} - - \noindent - which follows again directly - from the definition of the permutation operation for functions and the cancellation - property. Similarly for functions with more than one argument. + \eqref{permutefunapp}. Similarly for functions with more than one argument. Both formulations of equivariance have their advantages and disadvantages: - the definition, \eqref{permutefunapp} and (\ref{permdefs}.2) lead to a simple - rewrite system that pushes permutations inside a term until they reach - either function constants or variables. The permutations in front of - equivariant functions disappear. Such a rewrite system is often very helpful - in determining whether @{text "p \ t = t"} holds for a compound term @{text t}. In contrast \eqref{altequivariance} is usually easier to establish, since statements are - commonly given in a form where functions are fully applied. For example we can - easily show that equality is equivariant + commonly given in a form where functions are fully applied. For example we + can easily show that equality is equivariant \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}l} @@ -462,7 +485,7 @@ using the permutation operation on booleans and property \eqref{permuteequ}. Lemma~\ref{permutecompose} establishes that the permutation operation is equivariant. It is also easy to see that the boolean operators, like - @{text "\"}, @{text "\"} and @{text "\"} are all equivariant. Furthermore + @{text "\"}, @{text "\"}, @{text "\"} and @{text "\"} are all equivariant. Furthermore a simple calculation will show that our swapping functions are equivariant, that is \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% @@ -473,26 +496,36 @@ \noindent for all @{text a}, @{text b} and @{text \}. + + In contrast, Definition~\ref{equivariance} together with the permutation + operation for functions and \eqref{permutefunapp} lead to a simple + rewrite system that pushes permutations inside a term until they reach + either function constants or variables. The permutations in front of + equivariant functions disappear. Such a rewrite system is often very helpful + in determining whether @{text "\ \ t = t"} holds for a compound term @{text t}. ??? + *} section {* Support and Freshness *} text {* - The most original aspect of the nominal logic work of Pitts et al is a general - definition for ``the set of free variables of an object @{text "x"}''. This - definition is general in the sense that it applies not only to lambda-terms, - but also to lists, products, sets and even functions. The definition depends - only on the permutation operation and on the notion of equality defined for - the type of @{text x}, namely: + The most original aspect of the nominal logic work of Pitts is a general + definition for `the set of free variables, or free atoms, of an object @{text "x"}'. This + definition is general in the sense that it applies not only to lambda terms, + but to any type for which a permutation operation is defined + (like lists, sets, functions and so on). + \begin{definition}[Support] Given @{text x} is of permutation type, then + @{thm [display,indent=10] supp_def[no_vars, THEN eq_reflection]} + \end{definition} \noindent (Note that due to the definition of swapping in \eqref{swapdef}, we do not need to explicitly restrict @{text a} and @{text b} to have the same sort.) There is also the derived notion for when an atom @{text a} is \emph{fresh} - for an @{text x}, defined as + for an @{text x} of permutation type, defined as @{thm [display,indent=10] fresh_def[no_vars]} @@ -502,6 +535,7 @@ @{thm [display,indent=10] fresh_star_def[no_vars]} + \noindent A striking consequence of these definitions is that we can prove without knowing anything about the structure of @{term x} that @@ -511,7 +545,7 @@ \begin{lemma}\label{swaptriple} Assuming @{text x} is of permutation type, and @{text a}, @{text b} and @{text c} - have the same sort, then @{thm (prem 3) swap_rel_trans[no_vars]} and + have the same sort, then \mbox{@{thm (prem 3) swap_rel_trans[no_vars]}} and @{thm (prem 4) swap_rel_trans[no_vars]} imply @{thm (concl) swap_rel_trans[no_vars]}. \end{lemma} @@ -524,7 +558,7 @@ \noindent are equal. The lemma is then by application of the second permutation - property shown in \eqref{newpermprops}.\hfill\qed + property shown in~\eqref{newpermprops}.\hfill\qed \end{proof} \begin{theorem}\label{swapfreshfresh} @@ -554,18 +588,20 @@ \begin{proof} \begin{isabelle} \begin{tabular}[t]{c@ {\hspace{2mm}}l@ {\hspace{5mm}}l} - & \multicolumn{2}{@ {}l}{@{thm (lhs) fresh_permute_iff[where p="\",no_vars]} @{text "\"} - @{term "finite {b. (\ \ a \ b) \ \ \ x \ \ \ x}"}}\\ + & @{thm (lhs) fresh_permute_iff[where p="\",no_vars]}\\ + @{text "\"} & + @{term "finite {b. (\ \ a \ b) \ \ \ x \ \ \ x}"}\\ @{text "\"} & @{term "finite {b. (\ \ a \ \ \ b) \ \ \ x \ \ \ x}"} & since @{text "\ \ _"} is bijective\\ @{text "\"} & @{term "finite {b. \ \ (a \ b) \ x \ \ \ x}"} - & by \eqref{permutecompose} and \eqref{swapeqvt}\\ + & by Lemma~\ref{permutecompose} and \eqref{swapeqvt}\\ @{text "\"} - & @{term "finite {b. (a \ b) \ x \ x}"} @{text "\"} - @{thm (rhs) fresh_permute_iff[where p="\",no_vars]} + & @{term "finite {b. (a \ b) \ x \ x}"} & by \eqref{permuteequ}\\ + @{text "\"} + & @{thm (rhs) fresh_permute_iff[where p="\",no_vars]} \end{tabular} \end{isabelle}\hfill\qed \end{proof} @@ -583,29 +619,54 @@ \noindent is by noting that @{thm supp_conv_fresh[no_vars]} and that freshness and - the logical connectives are equivariant. + the logical connectives are equivariant. ??? Equivariance + + A simple consequence of the definition of support and equivariance is that + if a function @{text f} is equivariant then we have + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + \begin{tabular}{@ {}l} + @{thm (concl) supp_fun_eqvt[no_vars]} + \end{tabular}\hfill\numbered{suppeqvtfun} + \end{isabelle} + + \noindent + For function applications we can establish the two following properties. + + \begin{lemma} Let @{text f} and @{text x} be of permutation type, then + \begin{isabelle} + \begin{tabular}{r@ {\hspace{4mm}}p{10cm}} + @{text "i)"} & @{thm[mode=IfThen] fresh_fun_app[no_vars]}\\ + @{text "ii)"} & @{thm supp_fun_app[no_vars]}\\ + \end{tabular} + \end{isabelle} + \end{lemma} + + \begin{proof} + ??? + \end{proof} + While the abstract properties of support and freshness, particularly Theorem~\ref{swapfreshfresh}, are useful for developing Nominal Isabelle, one often has to calculate the support of some concrete object. This is straightforward for example for booleans, nats, products and lists: - \begin{equation} - \mbox{ - \begin{tabular}{@ {}r@ {\hspace{2mm}}l} + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + \begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}} @{text "booleans"}: & @{term "supp b = {}"}\\ @{text "nats"}: & @{term "supp n = {}"}\\ @{text "products"}: & @{thm supp_Pair[no_vars]}\\ @{text "lists:"} & @{thm supp_Nil[no_vars]}\\ & @{thm supp_Cons[no_vars]}\\ - \end{tabular}} - \end{equation} + \end{tabular} + \end{isabelle} \noindent But establishing the support of atoms and permutations is a bit trickier. To do so we will use the following notion about a \emph{supporting set}. - \begin{definition} + \begin{definition}[Supporting Set] A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b} not in @{text S} we have @{term "(a \ b) \ x = x"}. \end{definition} @@ -644,7 +705,7 @@ \noindent These are all relatively straightforward proofs adapted from the existing nominal logic work. However for establishing the support of atoms and - permutations we found the following ``optimised'' variant of @{text "iii)"} + permutations we found the following `optimised' variant of @{text "iii)"} more useful: \begin{lemma}\label{optimised} Let @{text x} be of permutation type. @@ -729,22 +790,18 @@ booleans are instances of this type class. Unfortunately, this does not work for sets or Isabelle/HOL's function - type.\footnote{Isabelle/HOL takes the type @{text "\ set"} as an abbreviation - of @{text "\ \ bool"}.} There are functions and sets definable in - Isabelle/HOL for which the finite support property does not hold. A simple - example of a function with infinite support is the function that returns the - natural number of an atom - - @{text [display, indent=10] "nat_of (Atom s i) \ i"} - - \noindent - This function's support is the set of \emph{all} atoms. To establish this we show @{term "\ a \ nat_of"}. - This is equivalent to assuming the set @{term "{b. (a \ b) \ nat_of \ nat_of}"} is finite - and deriving a contradiction. From the assumption we also know that - @{term "{a} \ {b. (a \ b) \ nat_of \ nat_of}"} is finite. Then we can use - Proposition~\ref{choosefresh} to choose an atom @{text c} such that - @{term "c \ a"}, @{term "sort_of c = sort_of a"} and @{term "(a \ c) \ nat_of = nat_of"}. - Now we can reason as follows: + type. There are functions and sets definable in Isabelle/HOL for which the + finite support property does not hold. A simple example of a function with + infinite support is @{const nat_of} shown in \eqref{sortnatof}. This + function's support is the set of \emph{all} atoms @{term "UNIV::atom set"}. + To establish this we show + @{term "\ a \ nat_of"}. This is equivalent to assuming the set @{term + "{b. (a \ b) \ nat_of \ nat_of}"} is finite and deriving a + contradiction. From the assumption we also know that @{term "{a} \ {b. (a \ + b) \ nat_of \ nat_of}"} is finite. Then we can use + Proposition~\ref{choosefresh} to choose an atom @{text c} such that @{term + "c \ a"}, @{term "sort_of c = sort_of a"} and @{term "(a \ c) \ nat_of = + nat_of"}. Now we can reason as follows: \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}[b]{@ {}rcl@ {\hspace{5mm}}l} @@ -757,28 +814,68 @@ \noindent But this means we have that @{term "nat_of a = nat_of c"} and @{term "sort_of a = sort_of c"}. This implies that atoms @{term a} and @{term c} must be equal, which clashes with our - assumption @{term "c \ a"} about how we chose @{text c}. - Cheney \cite{Cheney06} gives similar examples for constructions that have infinite support. + assumption @{term "c \ a"} about how we chose @{text c}.\footnote{Cheney \cite{Cheney06} + gives similar examples for constructions that have infinite support.} *} section {* Support of Finite Sets *} text {* - As shown above, sets is one instance of a type that is not generally finitely supported. - However, we can easily show that finite sets of atoms are finitely + Also the set type is one instance whose elements are not generally finitely + supported (we will give an example in Section~\ref{concrete}). + However, we can easily show that finite sets and co-finite sets of atoms are finitely supported, because their support can be characterised as: - \begin{lemma}\label{finatomsets} - If @{text S} is a finite set of atoms, then @{thm (concl) supp_finite_atom_set[no_vars]}. + \begin{lemma}\label{finatomsets}\mbox{}\\ + @{text "i)"} If @{text S} is a finite set of atoms, then @{thm (concl) supp_finite_atom_set[no_vars]}.\\ + @{text "ii)"} If @{term "UNIV - (S::atom set)"} is a finite set of atoms, then + @{thm (concl) supp_cofinite_atom_set[no_vars]}. \end{lemma} \begin{proof} - finite-supp-unique + Both parts can be easily shown by Lemma~\ref{optimised}. We only have to observe + that a swapping @{text "(a b)"} leaves a set @{text S} unchanged provided both + @{text a} and @{text b} are elements in @{text S} or both are not in @{text S}. + However if the sorts of a @{text a} and @{text b} agree, then the swapping will + change @{text S} if either of them is an element in @{text S} and the other is + not.\hfill\qed \end{proof} \noindent + Note that a consequence of the second part of this lemma is that + @{term "supp (UNIV::atom set) = {}"}. More difficult, however, is it to establish that finite sets of finitely - supported objects are finitely supported. + supported objects are finitely supported. For this we first show that + the union of the suports of finitely many and finitely supported objects + is finite, namely + + \begin{lemma}\label{unionsupp} + If @{text S} is a finite set whose elements are all finitely supported, then\\ + @{text "i)"} @{thm (concl) Union_of_finite_supp_sets[no_vars]} and\\ + @{text "ii)"} @{thm (concl) Union_included_in_supp[no_vars]}. + \end{lemma} + + \begin{proof} + The first part is by a straightforward induction on the finiteness of @{text S}. + For the second part, we know that @{term "\x\S. supp x"} is a set of atoms, which + by the first part is finite. Therefore we know by Lemma~\ref{finatomsets}.@{text "i)"} + that @{term "(\x\S. supp x) = supp (\x\S. supp x)"}. Taking @{text "f"} to be + \mbox{@{text "\S. \ (supp ` S)"}}, we can write the right hand side as @{text "supp (f S)"}. + Since @{text "f"} is an equivariant function, we have that + @{text "supp (f S) \ supp S"} by ??? This completes the second part.\hfill\qed + \end{proof} + + \noindent + With this lemma in place we can establish that + + \begin{lemma} + @{thm[mode=IfThen] supp_of_finite_sets[no_vars]} + \end{lemma} + + \begin{proof} + The right-to-left inclusion is proved in Lemma~\ref{unionsupp}.@{text "ii)"}. To show the inclusion + in the other direction we have to show Lemma~\ref{supports}.@{text "i)"} + \end{proof} *} @@ -1011,7 +1108,7 @@ *} -section {* Concrete Atom Types *} +section {* Concrete Atom Types\label{concrete} *} text {* @@ -1147,11 +1244,25 @@ -section {* Related Work *} +section {* Related Work\label{related} *} text {* Add here comparison with old work. + 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 + of this paper is to show an example of how to make better theorem proving + tools by choosing the right level of abstraction for the underlying + theory---our design choices take advantage of Isabelle's type system, type + classes and reasoning infrastructure. The novel technical contribution is a + mechanism for dealing with ``Church-style'' lambda-terms \cite{Church40} and + HOL-based languages \cite{PittsHOL4} where variables and variable binding + depend on type annotations. + + The paper is organised as follows\ldots + + 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. diff -r 651355113eee -r f1192e3474e0 Pearl-jv/ROOT.ML --- a/Pearl-jv/ROOT.ML Tue Mar 08 09:07:49 2011 +0000 +++ b/Pearl-jv/ROOT.ML Fri Mar 11 08:51:39 2011 +0000 @@ -1,6 +1,5 @@ -no_document use_thys ["../Nominal/Nominal2_Base", - "../Nominal/Atoms", - "../Nominal/Nominal2_Abs", - "LaTeXsugar"]; -use_thys ["Paper"]; \ No newline at end of file +use_thys ["../Nominal/Nominal2_Base", + "../Nominal/Atoms", + "../Nominal/Nominal2_Abs", + "LaTeXsugar"]; diff -r 651355113eee -r f1192e3474e0 Pearl-jv/ROOT2.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Pearl-jv/ROOT2.ML Fri Mar 11 08:51:39 2011 +0000 @@ -0,0 +1,1 @@ +use_thys ["Paper"]; \ No newline at end of file diff -r 651355113eee -r f1192e3474e0 Pearl-jv/document/root.bib --- a/Pearl-jv/document/root.bib Tue Mar 08 09:07:49 2011 +0000 +++ b/Pearl-jv/document/root.bib Fri Mar 11 08:51:39 2011 +0000 @@ -164,3 +164,8 @@ pages = {299--320} } +@Manual{Wenzel04, + title = {{U}sing {A}xiomatic {T}ype {C}lasses in {I}sabelle}, + author = {M.~Wenzel}, + note = {Manual in the Isabelle distribution.} +} \ No newline at end of file diff -r 651355113eee -r f1192e3474e0 Pearl-jv/document/root.tex --- a/Pearl-jv/document/root.tex Tue Mar 08 09:07:49 2011 +0000 +++ b/Pearl-jv/document/root.tex Fri Mar 11 08:51:39 2011 +0000 @@ -5,9 +5,9 @@ \usepackage{amsmath} \usepackage{amssymb} \usepackage{longtable} - +\usepackage{graphics} +\usepackage{pdfsetup} -\usepackage{pdfsetup} \urlstyle{rm} \isabellestyle{it} \renewcommand{\isastyle}{\isastyleminor} @@ -18,9 +18,10 @@ \renewcommand{\isasymiota}{} \renewcommand{\isasymrightleftharpoons}{} \renewcommand{\isasymemptyset}{$\varnothing$} +\newcommand{\isasymallatoms}{\ensuremath{\mathbb{A}}} \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}} - +\newcommand\new[0]{\reflectbox{\ensuremath{\mathsf{N}}}} \begin{document} @@ -33,16 +34,17 @@ \maketitle \begin{abstract} -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 formulate the theory so that it is -compatible with HOL, which the original formulation by Pitts is not. We -present a formalisation 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 two -abstraction operators that bind sets of names. +In his nominal logic work, Pitts 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 formulate the +theory so that it is compatible with HOL, which the original formulation by +Pitts is not. We achieve this by not requiring that every object in our +discourse has finite support. We present a formalisation 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 +two abstraction operators that bind sets of names. \end{abstract} % generated text of all theories