nominal2: comparison Pearl/Paper.thy

equal deleted inserted replaced

-:86122d793f32
+:0c958e385691
 atoms and sorts are used in the original formulation of the nominal logic work.
 Therefore it was decided in earlier versions of Nominal Isabelle to use a
 separate type for each sort of atoms and let the type system enforce the
 sort-respecting property of permutations. Inspired by the work on nominal
 unification \cite{UrbanPittsGabbay04}, it seemed best at the time to also
-implement permutations concretely as list of pairs of atoms. Thus Nominal
+implement permutations concretely as lists of pairs of atoms. Thus Nominal
 Isabelle used the two-place permutation operation with the generic type
 @{text [display,indent=10] "_ \<bullet> _  ::  (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
 \noindent
 the permutation operation is defined over the length of lists as follows
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
 @{text "[] \<bullet> c"} & @{text "="} & @{text c}\\
+\end{tabular}\hspace{12mm}
+\begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
 @{text "(a b)::\<pi> \<bullet> c"} & @{text "="} &
 $\begin{cases} @{text a} & \textrm{if}~@{text "\<pi> \<bullet> c = b"}\\
 @{text b} & \textrm{if}~@{text "\<pi> \<bullet> c = a"}\\
 @{text "\<pi> \<bullet> c"} & \textrm{otherwise}\end{cases}$
 \end{tabular}\hfill\numbered{atomperm}
 The major problem with Isabelle/HOL's type classes, however, is that they
 support operations with only a single type parameter and the permutation
 operations @{text "_ \<bullet> _"} used above in the permutation properties
 contain two! To work around this obstacle, Nominal Isabelle
-required from the user to
+required the user to
 declare up-front the collection of \emph{all} atom types, say @{text
 "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}. From this collection it used custom ML-code to
 generate @{text n} type classes corresponding to the permutation properties,
 whereby in these type classes the permutation operation is restricted to
 \noindent
 This operation has only a single type parameter @{text "\<beta>"} (the @{text "\<alpha>\<^isub>i"} are the
 atom types given by the user).
-While the representation of permutations-as-list solved the
+While the representation of permutations-as-lists solved the
 ``sort-respecting'' requirement and the declaration of all atom types
 up-front solved the problem with Isabelle/HOL's type classes, this setup
 caused several problems for formalising the nominal logic work: First,
 Nominal Isabelle had to generate @{text "n\<^sup>2"} definitions for the
 permutation operation over @{text "n"} types of atoms.  Second, whenever we
 with the large amounts of custom ML-code for generating multiple variants
 for some basic definitions. The result is that we can implement a pleasingly
 simple formalisation of the nominal logic work.\smallskip
 \noindent
-{\bf Contributions of the paper:} We use a single atom type for representing
+{\bf Contributions of the paper:} Our use of a single atom type for representing
-atoms of different sorts and use functions for representing
+atoms of different sorts and of functions for representing
-permutations. This drastically reduces the number of type classes to just
+permutations drastically reduces the number of type classes to just
-two (permutation types and finitely supported types), which we need in order
+two (permutation types and finitely supported types) that we need in order
 reason abstractly about properties from the nominal logic work. The novel
 technical contribution of this paper 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.
 text {*
 \noindent
 whereby the string argument specifies the sort of the atom.  (We use type
 \emph{string} merely for convenience; any countably infinite type would work
-as well.)  We have an auxiliary function @{text sort} that is defined as @{thm
+as well.)  A similar design choice was made by Gunter et al \cite{GunterOsbornPopescu09}
+for their variables.
+We have an auxiliary function @{text sort} that is defined as @{thm
 sort_of.simps[no_vars]}, and we clearly have for every finite set @{text X} of
 atoms and every sort @{text s} the property:
 \begin{proposition}\label{choosefresh}
 @{text "If finite X then there exists an atom a such that
 written  \mbox{@{text "_ \<circ> _"}}, and function inversion, given by Isabelle/HOL's
 inverse operator and written \mbox{@{text "inv _"}}, preserve the properties
 @{text "i"}-@{text "iii"}.
 However, a moment of thought is needed about how to construct non-trivial
-permutations? In the nominal logic work it turned out to be most convenient
+permutations. In the nominal logic work it turned out to be most convenient
 to work with swappings, written @{text "(a b)"}.  In our setting the
 type of swappings must be
 @{text [display,indent=10] "(_ _) :: atom \<Rightarrow> atom \<Rightarrow> perm"}
 \noindent
 and then establish:
 \begin{theorem}
 If @{text \<beta>}, @{text "\<beta>\<^isub>1"} and @{text "\<beta>\<^isub>2"} are permutation types,
-then so are: @{text "atom"}, @{text "\<beta>\<^isub>1 \<Rightarrow> \<beta>\<^isub>2"},
+then so are @{text "atom"}, @{text "\<beta>\<^isub>1 \<Rightarrow> \<beta>\<^isub>2"},
 @{text perm}, @{term "\<beta> set"}, @{term "\<beta> list"}, @{term "\<beta>\<^isub>1 \<times> \<beta>\<^isub>2"},
 @{text bool} and @{text "nat"}.
 \end{theorem}
 \begin{proof}
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \begin{tabular}[b]{@ {}rcl}
 @{text "0 \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "0 + \<pi>' - 0 = \<pi>'"}\\
 @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) + \<pi>' - (\<pi>\<^isub>1 + \<pi>\<^isub>2)"}\\
 & @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) + \<pi>' - \<pi>\<^isub>2 - \<pi>\<^isub>1"}\\
-& @{text "="} & @{text "\<pi>\<^isub>1 + (\<pi>\<^isub>2 + \<pi>' - \<pi>\<^isub>2) - \<pi>\<^isub>1"}\\
+& @{text "="} & @{text "\<pi>\<^isub>1 + (\<pi>\<^isub>2 + \<pi>' - \<pi>\<^isub>2) - \<pi>\<^isub>1"} @{text "\<equiv>"} @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> \<pi>'"}
-& @{text "\<equiv>"} & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> \<pi>'"}
 \end{tabular}\hfill\qed
 \end{isabelle}
 \end{proof}
 \noindent
 \end{lemma}
 \begin{proof}
 \begin{isabelle}
 \begin{tabular}[t]{c@ {\hspace{2mm}}l@ {\hspace{5mm}}l}
-& @{thm (lhs) fresh_permute_iff[where p="\<pi>",no_vars]}
+& \multicolumn{2}{@ {}l}{@{thm (lhs) fresh_permute_iff[where p="\<pi>",no_vars]} @{text "\<equiv>"}
-& \\
+@{term "finite {b. (\<pi> \<bullet> a \<rightleftharpoons> b) \<bullet> \<pi> \<bullet> x \<noteq> \<pi> \<bullet> x}"}}\\
-@{text "\<Leftrightarrow>"}
-& @{term "finite {b. (\<pi> \<bullet> a \<rightleftharpoons> b) \<bullet> \<pi> \<bullet> x \<noteq> \<pi> \<bullet> x}"}
-& by definition\\
 @{text "\<Leftrightarrow>"}
 & @{term "finite {b. (\<pi> \<bullet> a \<rightleftharpoons> \<pi> \<bullet> b) \<bullet> \<pi> \<bullet> x \<noteq> \<pi> \<bullet> x}"}
 & since @{text "\<pi> \<bullet> _"} is bijective\\
 @{text "\<Leftrightarrow>"}
 & @{term "finite {b. \<pi> \<bullet> (a \<rightleftharpoons> b) \<bullet> x \<noteq> \<pi> \<bullet> x}"}
 & by \eqref{permutecompose} and \eqref{swapeqvt}\\
 @{text "\<Leftrightarrow>"}
-& @{term "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"}
+& @{term "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"} @{text "\<equiv>"}
+@{thm (rhs) fresh_permute_iff[where p="\<pi>",no_vars]}
 & by \eqref{permuteequ}\\
-@{text "\<Leftrightarrow>"}
-& @{thm (rhs) fresh_permute_iff[where p="\<pi>",no_vars]}
-& by definition\\
 \end{tabular}
 \end{isabelle}\hfill\qed
 \end{proof}
 \noindent
 i)    & @{thm[mode=IfThen] supp_is_subset[no_vars]}\\
 ii)   & @{thm[mode=IfThen] supp_supports[no_vars]}\\
 iii)  & @{thm (concl) supp_is_least_supports[no_vars]}
 provided @{thm (prem 1) supp_is_least_supports[no_vars]},
 @{thm (prem 2) supp_is_least_supports[no_vars]}
-and @{text "S"} is the least such set, that means formally:\\[2mm]
+and @{text "S"} is the least such set, that means formally,
+for all @{text "S'"}, if @{term "finite S'"} and
-& \multicolumn{1}{c}{for all @{text "S'"}, if @{term "finite S'"} and
+@{term "S' supports x"} then @{text "S \<subseteq> S'"}.
-@{term "S' supports x"} then @{text "S \<subseteq> S'"}.}
 \end{tabular}
 \end{isabelle}
 \end{lemma}
 \begin{proof}
 nominal logic work. However for establishing the support of atoms and
 permutations we found  the following ``optimised'' variant of @{text "iii)"}
 more useful:
 \begin{lemma}\label{optimised} Let @{text x} be of permutation type.
-Then @{thm (concl) finite_supp_unique[no_vars]}
+We have that @{thm (concl) finite_supp_unique[no_vars]}
 provided @{thm (prem 1) finite_supp_unique[no_vars]},
 @{thm (prem 2) finite_supp_unique[no_vars]}, and for
 all @{text "a \<in> S"} and all @{text "b \<notin> S"}, with @{text a}
-and @{text b} having the same sort, then @{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"}
+and @{text b} having the same sort, then \mbox{@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"}}
 \end{lemma}
 \begin{proof}
 By Lemma \ref{supports}@{text ".iii)"} we have to show that for every finite
 set @{text S'} that supports @{text x}, \mbox{@{text "S \<subseteq> S'"}} holds. We will
 \end{isabelle}
 \noindent
 holds by a simple calculation using the group properties of permutations.
 The proof-obligation can then be discharged by analysing the inequality
-between the permutations @{term "(p \<bullet> a \<rightleftharpoons> b)"} and @{term "(a \<rightleftharpoons> b)"}.
+between the permutations @{term "(\<pi> \<bullet> a \<rightleftharpoons> b)"} and @{term "(a \<rightleftharpoons> b)"}.
 The main point about support is that whenever an object @{text x} has finite
 support, then Proposition~\ref{choosefresh} allows us to choose for @{text x} a
 fresh atom with arbitrary sort. This is an important operation in Nominal
 Isabelle in situations where, for example, a bound variable needs to be
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \begin{tabular}[b]{@ {}rcl@ {\hspace{5mm}}l}
 @{text "nat_of a"} & @{text "="} & @{text "(a \<rightleftharpoons> c) \<bullet> (nat_of a)"} & by def.~of permutations on nats\\
 & @{text "="} & @{term "((a \<rightleftharpoons> c) \<bullet> nat_of) ((a \<rightleftharpoons> c) \<bullet> a)"} & by \eqref{permutefunapp}\\
 & @{text "="} & @{term "nat_of c"} & by assumptions on @{text c}\\
-\end{tabular}\hfill\qed
+\end{tabular}
 \end{isabelle}
 \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 \<noteq> a"} about how we chose @{text c}. Similar examples for
+assumption @{term "c \<noteq> a"} about how we chose @{text c}.
-constructions that have infinite support are given in~\cite{Cheney06}.
+Cheney \cite{Cheney06} gives similar examples for constructions that have infinite support.
 *}
 section {* Concrete Atom Types *}
 text {*
 generic atom type, which we will write @{text "|_|"}.  For each class
 instance, this function must be injective and equivariant, and its outputs
 must all have the same sort.
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-\begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
+i)   \hspace{1mm}if @{thm (lhs) atom_eq_iff [no_vars]} then @{thm (rhs) atom_eq_iff [no_vars]}\hspace{4mm}
-i) & if @{thm (lhs) atom_eq_iff [no_vars]} then @{thm (rhs) atom_eq_iff [no_vars]}\\
+ii)  \hspace{1mm}@{thm atom_eqvt[where p="\<pi>", no_vars]}\hspace{4mm}
-ii) & @{thm atom_eqvt[where p="\<pi>", no_vars]}\\
+iii) \hspace{1mm}@{thm sort_of_atom_eq [no_vars]}
-iii) & @{thm sort_of_atom_eq [no_vars]}
+\hfill\numbered{atomprops}
-\end{tabular}\hfill\numbered{atomprops}
 \end{isabelle}
 \noindent
 With the definition @{thm atom_name_def [THEN eq_reflection, no_vars]} we can
 show that @{typ name} satisfies all the above requirements of a concrete atom
 \end{isabelle}
 \noindent
 which can easily be shown to be injective.
-Having settled on what the the sorts should be for ``Church-like'' atoms, we have to
+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
 \end{isabelle}
 \noindent
 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 the authors of \cite{PaulsonBenzmueller}
+Our hope is that with this approach Benzmueller and Paulson the authors of
-can make headway with formalising their results about simple type theory.
+\cite{PaulsonBenzmueller} can make headway with formalising their results
+about simple type theory.
 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.
 *}
 @{text \<pi>}, then we only have to state @{term "\<forall>\<pi>. P (\<pi> \<bullet> t)"}. The reason is
 that permutations can now consist of multiple swapping each of which can
 swap different kinds of atoms. This simplifies considerably the reasoning
 involved in building Nominal Isabelle.
-Second, we represented permutation as functions so that the associated
+Second, we represented permutations as functions so that the associated
-permutation operation has only a single type parameter. From this we derive
+permutation operation has only a single type parameter. This is very convenient
-most benefits because the abstract reasoning about permutations fits cleanly
+because the abstract reasoning about permutations fits cleanly
 with Isabelle/HOL's type classes. No custom ML-code is required to work
 around rough edges. Moreover, by establishing that our permutations-as-functions
 representation satisfy the group properties, we were able to use extensively
 Isabelle/HOL's reasoning infrastructure for groups. This often reduced proofs
 to simple calculations over @{text "+"}, @{text "-"} and @{text "0"}.
 {http://isabelle.in.tum.de/nominal/download}.\medskip
 \noindent
 {\bf Acknowledgements:} We are very grateful to Jesper Bengtson, Stefan
 Berghofer and Cezary Kaliszyk for their comments on earlier versions
-of this paper.
+of this paper. We are also grateful to the anonymous referee who helped us to
+put the work into the right context.
 *}
 (*<*)
 end

changeset 1776	0c958e385691
parent 1774	c34347ec7ab3
child 1779	4c2e424cb858