--- a/Pearl-jv/Paper.thy Wed May 04 15:27:04 2011 +0800
+++ b/Pearl-jv/Paper.thy Mon May 09 04:46:43 2011 +0100
@@ -156,7 +156,8 @@
$\new$
-
+ Obstacles for Coq; no type-classes, difficulties with quotient types,
+ need for classical reasoning
Two binders
@@ -188,7 +189,7 @@
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
+ This can be implemented in Isabelle/HOL as the datatype
*}
@@ -221,6 +222,9 @@
sort a = s and a \<notin> S"}.
\end{proposition}
+ \noindent
+ This property will be used later on whenever we have to chose a `fresh' atom.
+
For implementing sort-respecting permutations, we use functions of type @{typ
"atom => atom"} that are bijective; are the
identity on all atoms, except a finite number of them; and map
@@ -352,10 +356,14 @@
\end{isabelle}
\noindent
- whereby @{text "\<beta>"} is a generic type for the object @{text x}. The definition of this operation will be
- given by in terms of `induction' over this generic type. The type-class mechanism
- of Isabelle/HOL \cite{Wenzel04} allows us to give a definition for
- `base' types, such as atoms, permutations, booleans and natural numbers:
+ whereby @{text "\<beta>"} is a generic type for the object @{text
+ x}.\footnote{We will use the standard notation @{text "((op \<bullet>) \<pi>)
+ x"} for this operation in the few cases where we need to indicate
+ that it is a function applied with two arguments.} The definition
+ of this operation will be given by in terms of `induction' over this
+ generic type. The type-class mechanism of Isabelle/HOL
+ \cite{Wenzel04} allows us to give a definition for `base' types,
+ such as atoms, permutations, booleans and natural numbers:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}}
@@ -444,21 +452,21 @@
\end{isabelle}
\noindent
- whenever the permutation properties hold for @{text x}. This equation can
+ provided the permutation properties hold for @{text x}. This equation can
be easily shown by unfolding the permutation operation for functions on
- the right-hand side, simplifying the beta-redex and eliminating the permutations
- in front of @{text x} using \eqref{cancel}.
+ the right-hand side of the equation, simplifying the resulting beta-redex
+ and eliminating the permutations in front of @{text x} using \eqref{cancel}.
The main benefit of the use of type classes is that it allows us to delegate
much of the routine resoning involved in determining whether the permutation properties
are satisfied to Isabelle/HOL's type system: we only have to
establish that base types satisfy them and that type-constructors
- preserve them. Isabelle/HOL will use this information and determine
+ preserve them. Then Isabelle/HOL will use this information and determine
whether an object @{text x} with a compound type, like @{typ "atom \<Rightarrow> (atom set * nat)"}, satisfies the
permutation properties. For this we define the notion of a
\emph{permutation type}:
- \begin{definition}[Permutation type]
+ \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>"}.
@@ -494,47 +502,29 @@
section {* Equivariance *}
text {*
- An important notion in the nominal logic work is
- \emph{equivariance}. This notion allows us to characterise how
- permutations act upon compound statements in HOL by analysing how
- these statements are constructed. To do so, let us first define
- \emph{HOL-terms}. They are given by the grammar
-
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- @{text "t ::= c | x | t\<^isub>1 t\<^isub>2 | \<lambda>x. t"}
- \hfill\numbered{holterms}
- \end{isabelle}
-
- \noindent
- where @{text c} stands for constants and @{text x} for variables.
- We assume HOL-terms are fully typed, but for the sake of greater
- legibility we leave the typing information implicit. We also assume
- the usual notions for free and bound variables of a HOL-term.
- Furthermore, HOL-terms are regarded as equal modulo alpha-, beta-
- and eta-equivalence. Statements in HOL are HOL-terms of type @{text
- "bool"}.
-
- An \emph{equivariant} HOL-term is one that is invariant under the
- permutation operation. This can be defined in Isabelle/HOL
- as follows:
+ Two important notions in the nominal logic work are what Pitts calls
+ \emph{equivariance} and the \emph{equivariance principle}. These
+ notions allows us to characterise how permutations act upon compound
+ statements in HOL by analysing how these statements are constructed.
+ The notion of equivariance can defined as follows:
\begin{definition}[Equivariance]\label{equivariance}
- A HOL-term @{text t} is \emph{equivariant} provided
- @{term "\<pi> \<bullet> t = t"} holds for all permutations @{text "\<pi>"}.
+ An object @{text "x"} of permutation type is \emph{equivariant} provided
+ for all permutations @{text "\<pi>"}, \mbox{@{term "\<pi> \<bullet> x = x"}} holds.
\end{definition}
\noindent
- In what follows we will primarily be interested in the cases where @{text t}
- is a constant, but of course there is no way in Isabelle/HOL to restrict
- this definition to just these cases.
+ In what follows we will primarily be interested in the cases where
+ @{text x} is a constant, but of course there is no way in
+ Isabelle/HOL to restrict this definition to just these cases.
There are a number of equivalent formulations for the equivariance
- property. For example, assuming @{text t} is of permutation type @{text "\<alpha> \<Rightarrow>
- \<beta>"}, then equivariance can also be stated as
+ property. For example, assuming @{text f} is a function of permutation
+ type @{text "\<alpha> \<Rightarrow> \<beta>"}, then equivariance can also be stated as
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}l}
- @{text "\<forall>\<pi> x. \<pi> \<bullet> (t x) = t (\<pi> \<bullet> x)"}
+ @{text "\<forall>\<pi> x. \<pi> \<bullet> (f x) = f (\<pi> \<bullet> x)"}
\end{tabular}\hfill\numbered{altequivariance}
\end{isabelle}
@@ -544,7 +534,7 @@
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
- \eqref{permutefunapp}. Similarly for HOL-terms that take more than
+ \eqref{permutefunapp}. Similarly for functions that take more than
one argument. The point to note is that equivariance and equivariance in fully
applied form are always interderivable (for permutation types).
@@ -581,7 +571,7 @@
@{const True} and @{const False} are equivariant by the definition
of the permutation operation for booleans. Given this definition, it
is also easy to see that the boolean operators, like @{text "\<and>"},
- @{text "\<or>"}, @{text "\<longrightarrow>"} and @{text "\<not>"} are equivariant too:
+ @{text "\<or>"}, @{text "\<longrightarrow>"} and @{text "\<not>"} are equivariant:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}lcl}
@@ -593,15 +583,31 @@
\end{isabelle}
In contrast, the advantage of Definition \ref{equivariance} is that
- it leads to rewrite system that allows us to
- `push' a permutation towards the leaves of a HOL-term
- (i.e.~constants and variables). Then the permutation disappears in
- cases where the constants are equivariant. This can be stated more
- formally as the following \emph{equivariance principle}:
+ it allows us to state a general principle how permutations act on
+ statements in HOL. For this we will define a rewrite system that
+ `pushes' a permutation towards the leaves of statements (i.e.~constants
+ and variables). Then the permutations disappear in cases where the
+ constants are equivariant. To do so, let us first define
+ \emph{HOL-terms}, which are the building blocks of statements in HOL.
+ They are given by the grammar
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ @{text "t ::= c | x | t\<^isub>1 t\<^isub>2 | \<lambda>x. t"}
+ \hfill\numbered{holterms}
+ \end{isabelle}
+
+ \noindent
+ where @{text c} stands for constants and @{text x} for variables.
+ We assume HOL-terms are fully typed, but for the sake of better
+ legibility we leave the typing information implicit. We also assume
+ the usual notions for free and bound variables of a HOL-term.
+ Furthermore, HOL-terms are regarded as equal modulo alpha-, beta-
+ and eta-equivalence. The equivariance principle can now be stated
+ formally as follows:
\begin{theorem}[Equivariance Principle]\label{eqvtprin}
Suppose a HOL-term @{text t} whose constants are all equivariant. For any
- permutation @{text \<pi>}, let @{text t'} be the HOL-term @{text t} except every
+ permutation @{text \<pi>}, let @{text t'} be @{text t} except every
free variable @{text x} in @{term t} is replaced by @{text "\<pi> \<bullet> x"}, then
@{text "\<pi> \<bullet> t = t'"}.
\end{theorem}
@@ -611,79 +617,89 @@
the equivariance of a constant for which equivariance is not yet
known. For this we only have to make sure that the definiens of this
constant is a HOL-term whose constants are all equivariant. For example
- the universal quantifier @{text "All"}, also written @{text "\<forall>"}, is
- of type @{text "(\<alpha> \<Rightarrow> bool) \<Rightarrow> bool"} and in HOL is definied as
+ the universal quantifier @{text "\<forall>"} is definied in HOL as
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- @{thm All_def[no_vars]}
+ @{text "\<forall>x. P x \<equiv> "}~@{thm (rhs) All_def[no_vars]}
\end{isabelle}
\noindent
- Now @{text All} must be equivariant, because by the equivariance
- principle we only have to test whether the contants in the HOL-term
- @{thm (rhs) All_def[no_vars]}, namely @{text "="} and @{text
- "True"}, are equivariant. We shown this above. Taking all equations
- together, we can establish
+ The constants in the definiens @{thm (rhs) All_def[no_vars]}, namely @{text "="}
+ and @{text "True"}, are equivariant (we shown this above). Therefore
+ the equivariance principle gives us
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- @{text "\<pi> \<bullet> (All P) \<equiv> \<pi> \<bullet> (P = (\<lambda>x. True)) = ((\<pi> \<bullet> P) = (\<lambda>x. True)) \<equiv> All (\<pi> \<bullet> P)"}
+ @{text "\<pi> \<bullet> (\<forall>x. P x) \<equiv> \<pi> \<bullet> (P = (\<lambda>x. True)) = ((\<pi> \<bullet> P) = (\<lambda>x. True)) \<equiv> \<forall>x. (\<pi> \<bullet> P) x"}
+ \end{isabelle}
+
+ \noindent
+ and consequently, the constant @{text "\<forall>"} must be equivariant. From this
+ we can deduce that the existential quantifier @{text "\<exists>"} is equivariant.
+ Its definition in HOL is
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ @{text "\<exists>x. P x \<equiv> "}~@{thm (rhs) Ex_def[no_vars]}
\end{isabelle}
\noindent
- where the equation in the `middle' is given by Theorem~\ref{eqvtprin}.
- As a consequence, the constant @{text "All"} is equivariant. Given this
- fact we can further show that the existential quantifier @{text Ex},
- written also as @{text "\<exists>"}, is equivariant, since it is defined as
+ where again the HOL-term on the right-hand side only contains equivariant constants
+ (namely @{text "\<forall>"} and @{text "\<longrightarrow>"}). Taking both facts together, we can deduce that
+ the unique existential quantifier @{text "\<exists>!"} is equivariant. Its definition
+ is
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- @{thm Ex_def[no_vars]}
+ @{text "\<exists>!x. P x \<equiv> "}~@{thm (rhs) Ex1_def[no_vars]}
\end{isabelle}
\noindent
- and the HOL-term on the right-hand side contains equivariant constants only
- (namely @{text "\<forall>"} and @{text "\<longrightarrow>"}). In this way we can establish step by step
- equivariance for constants in HOL.
+ with all constants on the right-hand side being equivariant. With this kind
+ of reasoning we can build up a database of equivariant constants.
- In order to establish Theorem~\ref{eqvtprin}, we use a rewrite system
- consisting of a series of equalities
+ Before we proceed, let us give a justification for the equivariance principle.
+ For this we will use a rewrite system consisting of a series of equalities
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- @{text "\<pi> \<cdot> t = ... = t'"}
+ @{text "\<pi> \<cdot> t = ... = t'"}
\end{isabelle}
- \noindent
- that establish the equality between @{term "\<pi> \<bullet> t"} and @{text
- "t'"}. We have implemented this rewrite system as a conversion
- tactic on the ML-level of Isabelle/HOL.
- We shall next specify this tactic and show that it terminates and is
- correct (in the sense of pushing a permutation @{text "\<pi>"} inside a
- term and the only remaining instances of @{text "\<pi>"} are in front of
- the term's free variables). The tactic applies four `oriented'
- equations. We will first give a naive version of this tactic, which
- however in some cornercases produces incorrect resolts or does not
- terminate. We then give a modification it in order to obtain the
- desired properties. A permutation @{text \<pi>} can be pushed into
- applications and abstractions as follows
+ \noindent
+ that establish the equality between @{term "\<pi> \<bullet> t"} and
+ @{text "t'"}. The idea of the rewrite system is to push the
+ permutation inside the term @{text t}. We have implemented this as a
+ conversion tactic on the ML-level of Isabelle/HOL. In what follows,
+ we will show that this tactic produces only finitely many equations
+ and also show that is correct (in the sense of pushing a permutation
+ @{text "\<pi>"} inside a term and the only remaining instances of @{text
+ "\<pi>"} are in front of the term's free variables). The tactic applies
+ four `oriented' equations. We will first give a naive version of
+ this tactic, which however in some cornercases produces incorrect
+ results or does not terminate. We then give a modification in order
+ to obtain the desired properties.
+ Consider the following oriented equations
+
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}lr@ {\hspace{3mm}}c@ {\hspace{3mm}}l}
i) & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & \rrh & @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\\
ii) & @{text "\<pi> \<bullet> (\<lambda>x. t)"} & \rrh & @{text "\<lambda>x. \<pi> \<bullet> (t[x := (-\<pi>) \<bullet> x])"}\\
+ iii) & @{term "\<pi> \<bullet> (- \<pi>) \<bullet> x"} & \rrh & @{term "x"}\\
+ iv) & @{term "\<pi> \<bullet> c"} & \rrh &
+ {\rm @{term "c"}\hspace{6mm}provided @{text c} is equivariant}\\
\end{tabular}\hfill\numbered{rewriteapplam}
\end{isabelle}
\noindent
+ A permutation @{text \<pi>} can be pushed into applications and abstractions as follows
+
The first equation we established in \eqref{permutefunapp};
the second follows from the definition of permutations acting on functions
and the fact that HOL-terms are equal modulo beta-equivalence.
- Once the permutations are pushed towards the leaves we need the
+ Once the permutations are pushed towards the leaves, we need the
following two equations
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}lr@ {\hspace{3mm}}c@ {\hspace{3mm}}l}
- iii) & @{term "\<pi> \<bullet> (- \<pi>) \<bullet> x"} & \rrh & @{term "x"}\\
- iv) & @{term "\<pi> \<bullet> c"} & \rrh &
- {\rm @{term "c"}\hspace{6mm}provided @{text c} is equivariant}\\
+
\end{tabular}\hfill\numbered{rewriteother}
\end{isabelle}
@@ -691,10 +707,10 @@
in order to remove permuations in front of bound variables and
equivariant constants. Unfortunately, we have to be careful with
the rules {\it i)} and {\it iv}): they can lead to a loop whenever
- \mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "((op \<bullet>) \<pi>') t"}. Note
- that we usually write this application using infix notation as
- @{text "\<pi> \<bullet> t"} and recall that by Lemma \ref{permutecompose} the
- constant @{text "(op \<bullet>)"} is equivariant. Now consider the infinite
+ \mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "((op \<bullet>) \<pi>') t"}, where
+ we do not write the permutation operation infix, as usual, but
+ as an application. Recall that we established in Lemma \ref{permutecompose} that the
+ constant @{text "(op \<bullet>)"} is equivariant and consider the infinite
reduction sequence
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -709,37 +725,36 @@
\end{isabelle}
\noindent
- where the last step is again an instance of the first term, but it
+ The last term is again an instance of rewrite rule {\it i}), but the term
is bigger. To avoid this loop we need to apply our rewrite rule
using an `outside to inside' strategy. This strategy is sufficient
since we are only interested of rewriting terms of the form @{term
"\<pi> \<bullet> t"}, where an outermost permutation needs to pushed inside a term.
- Another problem we have to avoid is that the rules {\it i)} and
- {\it iii)} can `overlap'. For this note that
- the term @{term "\<pi> \<bullet>(\<lambda>x. x)"} reduces by {\it ii)} to
- @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet> x"}, to which we can apply rule {\it iii)}
- in order to obtain @{term "\<lambda>x. x"}, as is desired---there is no
- free variable in the original term and so the permutation should completely
- vanish. However, the subterm @{text
- "(- \<pi>) \<bullet> x"} is also an application. Consequently, the term
- @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet>x"} can reduce to @{text "\<lambda>x. (- (\<pi> \<bullet> \<pi>)) \<bullet> (\<pi> \<bullet> x)"} using
- {\it i)}. Given our strategy we cannot apply rule {\it iii)} anymore and
- even worse the measure we will introduce shortly increased. On the
- other hand, if we had started with the term @{text "\<pi> \<bullet> ((- \<pi>) \<bullet> x)"}
- where @{text \<pi>} and @{text x} are free variables, then we \emph{do}
- want to apply rule {\it i)} and not rule {\it iii)}. The latter
- would eliminate @{text \<pi>} completely. The problem is that rule {\it iii)}
- should only apply to instances where the variable is to bound; for free variables
- we want to use {\it ii)}.
+ Another problem we have to avoid is that the rules {\it i)} and {\it
+ iii)} can `overlap'. For this note that the term @{term "\<pi>
+ \<bullet>(\<lambda>x. x)"} reduces by {\it ii)} to @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet> x"}, to
+ which we can apply rule {\it iii)} in order to obtain @{term
+ "\<lambda>x. x"}, as is desired---there is no free variable in the original
+ term and so the permutation should completely vanish. However, the
+ subterm @{text "(- \<pi>) \<bullet> x"} is also an application. Consequently,
+ the term @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet>x"} can reduce to @{text "\<lambda>x. (- (\<pi>
+ \<bullet> \<pi>)) \<bullet> (\<pi> \<bullet> x)"} using {\it i)}. Given our strategy we cannot
+ apply rule {\it iii)} anymore and even worse the measure we will
+ introduce shortly increased. On the other hand, if we had started
+ with the term @{text "\<pi> \<bullet> ((- \<pi>) \<bullet> x)"} where @{text \<pi>} and @{text
+ x} are free variables, then we \emph{do} want to apply rule {\it i)}
+ and not rule {\it iii)}. The latter would eliminate @{text \<pi>}
+ completely. The problem is that rule {\it iii)} should only apply to
+ instances where the variable is to bound; for free variables we want
+ to use {\it ii)}. In order to distinguish these cases we have to
+ maintain the information which variable is bound when inductively
+ taking a term `apart'. This, unfortunately, does not mesh well with
+ the way how conversion tactics are implemented in Isabelle/HOL.
- The problem is that in order to distinguish both cases when
- inductively taking a term `apart', we have to maintain the
- information which variable is bound. This, unfortunately, does not
- mesh well with the way how simplification tactics are implemented in
- Isabelle/HOL. Our remedy is to use a standard trick in HOL: we
- introduce a separate definition for terms of the form @{text "(- \<pi>)
- \<bullet> x"}, namely as
+ Our remedy is to use a standard trick in HOL: we introduce a
+ separate definition for terms of the form @{text "(- \<pi>) \<bullet> x"},
+ namely as
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@{term "unpermute \<pi> x \<equiv> (- \<pi>) \<bullet> x"}
@@ -771,37 +786,45 @@
leaves) and the second is the number of occurences of @{text
"unpermute \<pi> x"} and @{text "\<pi> \<bullet> c"}.
- With the definition of the simplification tactic in place, we can
- establish its correctness. The property we are after is that for for
- a HOL-term @{text t} whose constants are all equivariant, the
- HOL-term @{text "\<pi> \<bullet> t"} is equal to @{text "t'"} with @{text "t'"}
+ With the rules of the conversions tactic in place, we can
+ establish its correctness. The property we are after is that
+ for a HOL-term @{text t} whose constants are all equivariant the
+ term \mbox{@{text "\<pi> \<bullet> t"}} is equal to @{text "t'"} with @{text "t'"}
being equal to @{text t} except that every free variable @{text x}
- in @{text t} is replaced by @{text "\<pi> \<bullet> x"}. Pitts calls this
- property \emph{equivariance principle} (book ref ???). In our
- setting the precise statement of this property is a slightly more
- involved because of the fact that @{text unpermutes} needs to be
- treated specially.
-
-
-
+ in @{text t} is replaced by \mbox{@{text "\<pi> \<bullet> x"}}. Let us call
+ a variable @{text x} \emph{really free}, if it is free and not occuring
+ in an unpermute, such as @{text "unpermute _ x"} and @{text "unpermute x _"}.
+ We need the following technical notion characterising a \emph{@{text "\<pi>"}-proper} HOL-term
- With these definitions in place we can define the notion of an \emph{equivariant}
- HOL-term
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{tabular}{@ {}ll}
+ $\bullet$ & variables and constants are @{text \<pi>}-proper,\\
+ $\bullet$ & @{term "unpermute \<pi> x"} is @{text \<pi>}-proper,\\
+ $\bullet$ & @{term "\<lambda>x. t"} is @{text \<pi>}-proper, if @{text t} is @{text \<pi>}-proper and @{text x} is
+ really free in @{text t}, and\\
+ $\bullet$ & @{term "t\<^isub>1 t\<^isub>2"} is @{text \<pi>}-proper, if @{text "t\<^isub>1"} and @{text "t\<^isub>2"} are
+ @{text \<pi>}-proper.
+ \end{tabular}
+ \end{isabelle}
- \begin{definition}[Equivariant HOL-term]
- A HOL-term is \emph{equivariant}, provided it is closed and composed of applications,
- abstractions and equivariant constants only.
- \end{definition}
+ \begin{proof}[Theorem~\ref{eqvtprin}] We establish the property if @{text t}
+ is @{text \<pi>}-proper and only contains equivaraint constants, then
+ @{text "\<pi> \<bullet> t = t'"} where @{text "t'"} is equal to @{text "t"} except all really
+ free variables @{text x} are replaced by @{text "\<pi> \<bullet> x"}, and all semi-free variables
+ @{text "unpermute \<pi> x"} by @{text "x"}. We establish this property by induction
+ on the size of HOL-terms, counting terms like @{text "unpermuting \<pi> x"} as leafes,
+ like variables and constants. The cases for variables, constants and @{text unpermutes}
+ are routine. In the case of abstractions we have by induction hypothesis that
+ @{text "\<pi> \<bullet> (t[x := unpermute \<pi> x]) = t'"} with @{text "t'"} satisfying our
+ correctness property. This implies that @{text "\<lambda>x. \<pi> \<bullet> (t[x := unpermute \<pi> x]) = \<lambda>x. t'"}
+ and hence @{text "\<pi> \<bullet> (\<lambda>x. t) = \<lambda>x. t'"} as needed.\hfill\qed
+ \end{proof}
+
+ Pitts calls this property \emph{equivariance principle} (book ref ???).
- \noindent
- For equivariant terms we have
-
- \begin{lemma}
- For an equivariant HOL-term @{text "t"}, @{term "\<pi> \<bullet> t = t"} for all permutations @{term "\<pi>"}.
- \end{lemma}
-
- Let us now see how to use the equivariance principle. We have
-
+ Problems with @{text undefined}
+
+ Lines of code
*}
@@ -814,7 +837,8 @@
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
+ \begin{definition}[Support] \label{support}
+ Given @{text x} is of permutation type, then
@{thm [display,indent=10] supp_def[no_vars, THEN eq_reflection]}
\end{definition}
@@ -833,13 +857,49 @@
@{thm [display,indent=10] fresh_star_def[no_vars]}
+ \noindent
+ Using the equivariance principle, it can be easily checked that all three notions
+ are equivariant. A simple consequence of the definition of support and equivariance
+ is that if @{text x} is equivariant then we have
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{tabular}{@ {}l}
+ @{thm (concl) supp_fun_eqvt[where f="x", no_vars]}
+ \end{tabular}\hfill\numbered{suppeqvtfun}
+ \end{isabelle}
\noindent
- A striking consequence of these definitions is that we can prove
- without knowing anything about the structure of @{term x} that
- swapping two fresh atoms, say @{text a} and @{text b}, leave
- @{text x} unchanged. For the proof we use the following lemma
- about swappings applied to an @{text x}:
+ For function applications we can establish the following two properties.
+
+ \begin{lemma}\label{suppfunapp} Let @{text f} and @{text x} be of permutation type, then
+ \begin{isabelle}
+ \begin{tabular}{r@ {\hspace{4mm}}p{10cm}}
+ {\it i)} & @{thm[mode=IfThen] fresh_fun_app[no_vars]}\\
+ {\it ii)} & @{thm supp_fun_app[no_vars]}\\
+ \end{tabular}
+ \end{isabelle}
+ \end{lemma}
+
+ \begin{proof}
+ For the first property, we know from the assumption that @{term
+ "finite {b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f}"} and @{term "finite {b . (a \<rightleftharpoons> b) \<bullet> x \<noteq>
+ x}"} hold. That means for all, but finitely many @{text b} we have
+ @{term "(a \<rightleftharpoons> b) \<bullet> f = f"} and @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}. Similarly,
+ we have to show that for but, but finitely @{text b} the equation
+ @{term "(a \<rightleftharpoons> b) \<bullet> f x = f x"} holds. The left-hand side of this
+ equation is equal to @{term "((a \<rightleftharpoons> b) \<bullet> f) ((a \<rightleftharpoons> b) \<bullet> x)"} by
+ \eqref{permutefunapp}, which we know by the previous two facts for
+ @{text f} and @{text x} is equal to the right-hand side for all,
+ but finitely many @{text b}. This establishes the first
+ property. The second is a simple corollary of {\it i)} by
+ unfolding the definition of freshness.\qed
+ \end{proof}
+
+ A striking consequence of the definitions for support and freshness
+ is that we can prove without knowing anything about the structure of
+ @{term x} that swapping two fresh atoms, say @{text a} and @{text
+ b}, leave @{text x} unchanged. For the proof we use the following
+ lemma about swappings applied to an @{text x}:
\begin{lemma}\label{swaptriple}
Assuming @{text x} is of permutation type, and @{text a}, @{text b} and @{text c}
@@ -856,7 +916,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}.\qed
\end{proof}
\begin{theorem}\label{swapfreshfresh}
@@ -874,81 +934,10 @@
Now the theorem follows from Lemma~\ref{swaptriple}.\hfill\qed
\end{proof}
- \noindent
- Two important properties that need to be established for later calculations is
- that @{text "supp"} and freshness are equivariant. For this we first show that:
-
- \begin{lemma}\label{half}
- If @{term x} is a permutation type, then @{thm (lhs) fresh_permute_iff[where p="\<pi>",no_vars]}
- if and only if @{thm (rhs) fresh_permute_iff[where p="\<pi>",no_vars]}.
- \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]}\\
- @{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 Lemma~\ref{permutecompose} and \eqref{swapeqvt}\\
- @{text "\<Leftrightarrow>"}
- & @{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}
-
- \noindent
- Together with the definition of the permutation operation on booleans,
- we can immediately infer equivariance of freshness:
-
- @{thm [display,indent=10] fresh_eqvt[where p="\<pi>",no_vars]}
-
- \noindent
- Now equivariance of @{text "supp"}, namely
-
- @{thm [display,indent=10] supp_eqvt[where p="\<pi>",no_vars]}
-
- \noindent
- is by noting that @{thm supp_conv_fresh[no_vars]} and that freshness and
- 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:
+ one often has to calculate the support of concrete objects.
+ For booleans, nats, products and lists it is easy to check that
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}}
@@ -960,8 +949,8 @@
\end{tabular}
\end{isabelle}
- \noindent
- But establishing the support of atoms and permutations is a bit
+ \noindent
+ hold. 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}[Supporting Set]
@@ -989,21 +978,21 @@
\end{lemma}
\begin{proof}
- For @{text "i)"} we derive a contradiction by assuming there is an atom @{text a}
+ For {\it i)} we derive a contradiction by assuming there is an atom @{text a}
with @{term "a \<in> supp x"} and @{text "a \<notin> S"}. Using the second fact, the
assumption that @{term "S supports x"} gives us that @{text S} is a superset of
@{term "{b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"}, which is finite by the assumption of @{text S}
being finite. But this means @{term "a \<notin> supp x"}, contradicting our assumption.
- Property @{text "ii)"} is by a direct application of
- Theorem~\ref{swapfreshfresh}. For the last property, part @{text "i)"} proves
+ Property {\it ii)} is by a direct application of
+ Theorem~\ref{swapfreshfresh}. For the last property, part {\it i)} proves
one ``half'' of the claimed equation. The other ``half'' is by property
- @{text "ii)"} and the fact that @{term "supp x"} is finite by @{text "i)"}.\hfill\qed
+ {\it ii)} and the fact that @{term "supp x"} is finite by {\it i)}.\hfill\qed
\end{proof}
\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 {\it iii)}
more useful:
\begin{lemma}\label{optimised} Let @{text x} be of permutation type.
@@ -1079,27 +1068,56 @@
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
+ fresh atom with arbitrary sort. This is a crucial operation in Nominal
Isabelle in situations where, for example, a bound variable needs to be
renamed. To allow such a choice, we only have to assume that
@{text "finite (supp x)"} holds. For more convenience we
- can define a type class for types where every element has finite support, and
- prove that the types @{term "atom"}, @{term "perm"}, lists, products and
- booleans are instances of this type class.
+ can define a type class in Isabelle/HOL corresponding to the
+ property:
+
+ \begin{definition}[Finitely Supported Type]
+ A type @{text "\<beta>"} is \emph{finitely supported} if @{term "finite (supp x)"}
+ holds for all @{text x} of type @{text "\<beta>"}.
+ \end{definition}
+
+ \noindent
+ By the calculations above we can easily establish
+
+ \begin{theorem}\label{finsuptype}
+ The types @{type atom}, @{type perm}, @{type bool} and @{type nat}
+ are fintitely supported, and assuming @{text \<beta>}, @{text "\<beta>\<^isub>1"} and
+ @{text "\<beta>\<^isub>2"} are finitely supported types, then @{text "\<beta> list"} and
+ @{text "\<beta>\<^isub>1 \<times> \<beta>\<^isub>2"} are finitely supported.
+ \end{theorem}
- Unfortunately, this does not work for sets or Isabelle/HOL's function
- 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:
+ \noindent
+ The main benefit of using the finite support property for choosing a
+ fresh atom is that the reasoning is `compositional'. To see this,
+ assume we have a list of atoms and a method of choosing a fresh atom
+ that is not a member in this list---for example the maximum plus
+ one. Then if we enlarge this list \emph{after} the choice, then
+ obviously the fresh atom might not be fresh anymore. In contrast, by
+ the classical reasoning of Proposition~\ref{choosefresh} we know a
+ fresh atom exists for every list of atoms and no matter how we
+ extend this list of atoms, we always preserve the property of being
+ finitely supported. Consequently the existence of a fresh atom is
+ still guarantied by Proposition~\ref{choosefresh}. Using the method
+ of `maximum plus one' we might have to adapt the choice of a fresh
+ atom.
+
+ Unfortunately, Theorem~\ref{finsuptype} does not work in general for the
+ types of sets and functions. There are functions definable in 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}
@@ -1119,15 +1137,19 @@
section {* Support of Finite Sets *}
text {*
- Also the set type is one instance whose elements are not generally finitely
+ Also the set type is an 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:
+ supported. Their support can be characterised as:
- \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
+ \begin{lemma}\label{finatomsets}
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{tabular}[b]{@ {}rl}
+ {\it i)} & If @{text S} is a finite set of atoms, then @{thm (concl) supp_finite_atom_set[no_vars]}.\\
+ {\it ii)} & If @{term "UNIV - (S::atom set)"} is a finite set of atoms, then
@{thm (concl) supp_cofinite_atom_set[no_vars]}.
+ \end{tabular}
+ \end{isabelle}
\end{lemma}
\begin{proof}
@@ -1144,23 +1166,32 @@
@{term "supp (UNIV::atom set) = {}"}.
More difficult, however, is it to establish that finite sets of finitely
supported objects are finitely supported. For this we first show that
- the union of the suports of finitely many and finitely supported objects
+ the union of the supports 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]}.
+ If @{text S} is a finite set whose elements are all finitely supported, then
+ %
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{tabular}[b]{@ {}rl}
+ {\it i)} & @{thm (concl) Union_of_finite_supp_sets[no_vars]} and\\
+ {\it ii)} & @{thm (concl) Union_included_in_supp[no_vars]}.
+ \end{tabular}
+ \end{isabelle}
\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
+ 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}.{\it i)} that @{term "(\<Union>x\<in>S. supp
+ x) = supp (\<Union>x\<in>S. supp x)"}. Taking @{text "f"} to be the function
+ \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 (can be easily checked by the equivariance principle), we
+ have that @{text "supp (f S) \<subseteq> supp S"} by
+ Lemma~\ref{suppfunapp}.{\it ii)}. This completes the second
+ part.\hfill\qed
\end{proof}
\noindent
@@ -1171,26 +1202,50 @@
\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)"}
+ The right-to-left inclusion is proved in Lemma~\ref{unionsupp}.{\it ii)}. To show the inclusion
+ in the other direction we can use Lemma~\ref{supports}.{\it i)}. This means
+ for all @{text a} and @{text b} that are not in @{text S} we have to show that
+ @{term "(a \<rightleftharpoons> b) \<bullet> (\<Union>x \<in> S. supp x) = (\<Union>x \<in> S. supp x)"} holds. By the equivariance
+ principle, the left-hand side is equal to @{term "\<Union>x \<in> ((a \<rightleftharpoons> b) \<bullet> S). supp x"}. Now
+ the swapping in front of @{text S} disappears, since @{term "a \<sharp> S"} and @{term "b \<sharp> S"}
+ whenever @{text "a, b \<notin> S"}. Thus we are done.\hfill\qed
\end{proof}
+
+ \noindent
+ To sum up, every finite set of finitely supported elements has
+ finite support. Unfortunately, we cannot use
+ Theorem~\ref{finsuptype} to let Isabelle/HOL find this out
+ automatically. This would require to introduce a separate type of
+ finite sets, which however is not so convenient to reason about as
+ Isabelle's standard set type.
*}
-section {* Induction Principles *}
+section {* Induction Principles for Permutations *}
text {*
While the use of functions as permutation provides us with a unique
- representation for permutations (for example @{term "(a \<rightleftharpoons> b)"} and
- @{term "(b \<rightleftharpoons> a)"} are equal permutations), this representation has
- one draw back: it does not come readily with an induction principle.
- Such an induction principle is handy for deriving properties like
+ representation for permutations (for example @{term "(a \<rightleftharpoons> b)"} and
+ @{term "(b \<rightleftharpoons> a)"} are equal permutations), this representation does
+ not come automatically with an induction principle. Such an
+ induction principle is however handy for generalising
+ Lemma~\ref{swapfreshfresh} from swappings to permutations
- @{thm [display, indent=10] supp_perm_eq[no_vars]}
+ \begin{lemma}
+ @{thm [mode=IfThen] perm_supp_eq[no_vars]}
+ \end{lemma}
\noindent
- However, it is not too difficult to derive an induction principle,
- given the fact that we allow only permutations with a finite domain.
+ In this section we will establish an induction principle for permutations
+ with which this lemma can be easily proved. It is not too difficult to derive
+ an induction principle for permutations, given the fact that we allow only
+ permutations having a finite support.
+
+ Using a the property from \cite{???}
+
+ \begin{lemma}\label{smallersupp}
+ @{thm [mode=IfThen] smaller_supp[no_vars]}
+ \end{lemma}
*}
@@ -1414,14 +1469,13 @@
type. This design gives us the flexibility to define operations and prove
theorems that are generic with respect to atom sorts. For example, as
illustrated above the @{term supp} function returns a set that includes the
- free atoms of \emph{all} sorts together; the flexibility offered by the new
- atom type makes this possible.
+ free atoms of \emph{all} sorts together.
However, the single multi-sorted atom type does not make an ideal interface
for end-users of Nominal Isabelle. If sorts are not distinguished by
Isabelle's type system, users must reason about atom sorts manually. That
- means subgoals involving sorts must be discharged explicitly within proof
- scripts, instead of being inferred by Isabelle/HOL's type checker. In other
+ means for example that subgoals involving sorts must be discharged explicitly within proof
+ scripts, instead of being inferred automatically. In other
cases, lemmas might require additional side conditions about sorts to be true.
For example, swapping @{text a} and @{text b} in the pair \mbox{@{term "(a,
b)"}} will only produce the expected result if we state the lemma in
@@ -1477,10 +1531,10 @@
must all have the same sort, that is
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \begin{tabular}{r@ {\hspace{3mm}}l}
- i) if @{thm (lhs) atom_eq_iff [no_vars]} then @{thm (rhs) atom_eq_iff [no_vars]}\\
- ii) @{thm atom_eqvt[where p="\<pi>", no_vars]}\\
- iii) @{thm sort_of_atom_eq [no_vars]}
+ \begin{tabular}{@ {}r@ {\hspace{3mm}}l}
+ i) & if @{thm (lhs) atom_eq_iff [no_vars]} then @{thm (rhs) atom_eq_iff [no_vars]}\\
+ ii) & @{thm atom_eqvt[where p="\<pi>", no_vars]}\\
+ iii) & @{thm sort_of_atom_eq [no_vars]}
\end{tabular}\hfill\numbered{atomprops}
\end{isabelle}
@@ -1489,7 +1543,7 @@
show that @{typ name} satisfies all the above requirements of a concrete atom
type.
- The whole point of defining the concrete atom type class was to let users
+ The whole point of defining the concrete atom type class is to let users
avoid explicit reasoning about sorts. This benefit is realised by defining a
special swapping operation of type @{text "\<alpha> \<Rightarrow> \<alpha>
\<Rightarrow> perm"}, where @{text "\<alpha>"} is a concrete atom type:
@@ -1530,6 +1584,18 @@
\noindent
This command can be implemented using less than 100 lines of custom ML-code.
+
+*}
+
+
+
+section {* Related Work\label{related} *}
+
+text {*
+ Coq-tries, but failed
+
+ Add here comparison with old work.
+
In comparison, the old version of Nominal Isabelle included more than 1000
lines of ML-code for creating concrete atom types, and for defining various
type classes and instantiating generic lemmas for them. In addition to
@@ -1538,14 +1604,6 @@
theories that separately declare different atom types can be merged
together---it is no longer required to collect all atom declarations in one
place.
-*}
-
-
-
-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