--- 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 ("\<allatoms>")
+where
+ "UNIV_atom \<equiv> UNIV::atom set"
+
notation (latex output)
sort_of ("sort _" [1000] 100) and
Abs_perm ("_") and
@@ -22,7 +27,7 @@
Abs_name ("\<lceil>_\<rceil>") and
Rep_var ("\<lfloor>_\<rfloor>") and
Abs_var ("\<lceil>_\<rceil>") 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 \<equiv> sort_of"
-abbreviation
- "sort_ty \<equiv> sort_of_ty"
+lemma infinite_collect:
+ assumes "\<forall>x \<in> S. P x" "infinite S"
+ shows "infinite {x \<in> S. P x}"
+using assms
+apply(subgoal_tac "infinite {x. x \<in> 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 "\<lambda>x. t \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. \<tau>"}
- \hfill\numbered{atomperm}
+ @{text "\<lambda>x. t \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. \<tau>"}
\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 "_ \<bullet> _"}, 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 "_ \<bullet> _"}, 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 "\<Gamma>"} 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 \<Gamma>} is valid then so is @{text "\<pi> \<bullet> \<Gamma>"} for
- all permutations @{text "\<pi>"}. This is \emph{not} the case for arbitrary
- renaming substitutions, as they might identify some variables in @{text \<Gamma>}.
- Permutations fit well with HOL's definitions. For example
+ all permutations @{text "\<pi>"}. This is again \emph{not} the case for arbitrary
+ renaming substitutions, as they might identify some of the @{text "x\<^isub>i"} in @{text \<Gamma>}.
+
+ 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 "\<pi> \<bullet> (A \<and> B)"} & if and only if & @{text "(\<pi> \<bullet> A) \<and> (\<pi> \<bullet> B)"}\\
+ @{term "\<pi> \<bullet> (A \<longrightarrow> B)"} & if and only if & @{text "(\<pi> \<bullet> A) \<longrightarrow> (\<pi> \<bullet> 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 "\<forall>\<pi>. \<pi> \<bullet> 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 "\<pi> \<bullet> x = x"}
+ for all @{text "\<pi>"}. 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
- "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^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 "\<equiv>"} & @{thm (rhs) sort_of.simps[no_vars]}\\
+ @{thm (lhs) nat_of.simps[no_vars]} & @{text "\<equiv>"} & @{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 \<pi>} as follows:
+ in Isabelle/HOL for a function @{text \<pi>} 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) \<equiv> \<lambda>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 "\<equiv>"} & @{thm (rhs) zero_perm_def[no_vars]} &
+ @{thm (lhs) plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2"]} & @{text "\<equiv>"} &
+ @{thm (rhs) plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2"]}\\
+ @{thm (lhs) uminus_perm_def[where p="\<pi>"]} & @{text "\<equiv>"} & @{thm (rhs) uminus_perm_def[where p="\<pi>"]} &
+ @{thm (lhs) minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]} & @{text "\<equiv>"} &
+ @{thm (rhs) minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^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="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{5mm}
- @{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{5mm}
- @{thm minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]}
- \end{tabular}
- \end{isabelle}
-
- \noindent
- and verify the simple properties
-
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \begin{tabular}{@ {}l}
- @{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]} \hspace{5mm}
- @{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{5mm}
- @{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{5mm}
+ @{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]}\\
+ @{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{9mm}
+ @{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{9mm}
@{thm group_add_class.left_minus[where a="\<pi>::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 "\<beta>"} is a \emph{permutation type} if the permutation
properties in \eqref{newpermprops} are satisfied for every @{text "x"} of type
@{text "\<beta>"}.
\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 "\<pi> \<bullet> _"}~~is bijective,
which in turn implies the property
@@ -337,43 +366,23 @@
@{thm (rhs) permute_eq_iff[where p="\<pi>", 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 "\<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x) = (\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}.
- \end{lemma}
-
- \begin{proof} The proof is as follows:
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \begin{tabular}[b]{@ {}rcl@ {\hspace{8mm}}l}
- @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> x"}
- & @{text "="} & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> (-\<pi>\<^isub>1) \<bullet> \<pi>\<^isub>1 \<bullet> x"} & by \eqref{cancel}\\
- & @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2 - \<pi>\<^isub>1) \<bullet> \<pi>\<^isub>1 \<bullet> x"} & by {\rm(\ref{newpermprops}.@{text "ii"})}\\
- & @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> 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="\<pi>",no_vars, THEN eq_reflection]}\\
- b) & functions: & @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\
- c) & permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\
- d) & sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
- e) & booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
- f) & lists: & @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
- & & @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
- g) & products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\
- h) & nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
- \end{tabular}}
- \end{equation}
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}}
+ atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\
+ functions: & @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\
+ permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\
+ sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+ booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+ lists: & @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+ & @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+ products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+ nats: & @{thm permute_nat_def[where p="\<pi>", 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 "\<pi> \<bullet> (f x) ="}
+ @{thm (rhs) permute_fun_app_eq[where p="\<pi>", 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 "\<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x) = (\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}.
+ \end{lemma}
+
+ \begin{proof} The proof is as follows:
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{tabular}[b]{@ {}c@ {\hspace{2mm}}l@ {\hspace{8mm}}l}
+ & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> x"}\\
+ @{text "="} & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> (-\<pi>\<^isub>1) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"} & by \eqref{cancel}\\
+ @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2 - \<pi>\<^isub>1) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"} & by {\rm(\ref{newpermprops}.@{text "ii"})}\\
+ @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> 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 "\<forall>\<pi>. \<pi> \<bullet> 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 "\<pi> \<bullet> (f x) = (\<pi> \<bullet> f) (\<pi> \<bullet> 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 \<bullet> 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 "\<and>"}, @{text "\<or>"} and @{text "\<longrightarrow>"} are all equivariant. Furthermore
+ @{text "\<and>"}, @{text "\<or>"}, @{text "\<not>"} and @{text "\<longrightarrow>"} 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 \<pi>}.
+
+ 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 "\<pi> \<bullet> 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="\<pi>",no_vars]} @{text "\<equiv>"}
- @{term "finite {b. (\<pi> \<bullet> a \<rightleftharpoons> b) \<bullet> \<pi> \<bullet> x \<noteq> \<pi> \<bullet> x}"}}\\
+ & @{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> \<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}\\
+ & by Lemma~\ref{permutecompose} and \eqref{swapeqvt}\\
@{text "\<Leftrightarrow>"}
- & @{term "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"} @{text "\<equiv>"}
- @{thm (rhs) fresh_permute_iff[where p="\<pi>",no_vars]}
+ & @{term "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"}
& by \eqref{permuteequ}\\
+ @{text "\<equiv>"}
+ & @{thm (rhs) fresh_permute_iff[where p="\<pi>",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 \<rightleftharpoons> b) \<bullet> 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 "\<alpha> set"} as an abbreviation
- of @{text "\<alpha> \<Rightarrow> 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) \<equiv> i"}
-
- \noindent
- This function's support is the set of \emph{all} atoms. To establish this we show @{term "\<not> a \<sharp> nat_of"}.
- This is equivalent to assuming the set @{term "{b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"} is finite
- and deriving a contradiction. From the assumption we also know that
- @{term "{a} \<union> {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"} is finite. Then we can use
- Proposition~\ref{choosefresh} to choose an atom @{text c} such that
- @{term "c \<noteq> a"}, @{term "sort_of c = sort_of a"} and @{term "(a \<rightleftharpoons> c) \<bullet> 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 "\<not> a \<sharp> nat_of"}. This is equivalent to assuming the set @{term
+ "{b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"} is finite and deriving a
+ contradiction. From the assumption we also know that @{term "{a} \<union> {b. (a \<rightleftharpoons>
+ b) \<bullet> nat_of \<noteq> nat_of}"} is finite. Then we can use
+ Proposition~\ref{choosefresh} to choose an atom @{text c} such that @{term
+ "c \<noteq> a"}, @{term "sort_of c = sort_of a"} and @{term "(a \<rightleftharpoons> c) \<bullet> 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 \<noteq> a"} about how we chose @{text c}.
- Cheney \cite{Cheney06} gives similar examples for constructions that have infinite support.
+ assumption @{term "c \<noteq> 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 "\<Union>x\<in>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 "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"}. Taking @{text "f"} to be
+ \mbox{@{text "\<lambda>S. \<Union> (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) \<subseteq> 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.