nominal2: comparison LMCS-Paper/Paper.thy

equal deleted inserted replaced

-:014f0ea2381c
+:65452cf6f5ae
 fa_trm2_al ("'(fa\<AL>\<^bsub>assn\<^esub>, fa\<AL>\<^bsub>trm\<^esub>')") and
 ast ("'(as, t')") and
 ast' ("'(as', t\<PRIME> ')") and
 equ2 ("'(=, =')") and
 supp2 ("'(supp, supp')") and
-bn_al ("bn\<^sup>\<alpha> _")
+bn_al ("bn\<^sup>\<alpha> _" [100] 100)
 (*>*)
 section {* Introduction *}
 corresponding alpha-equivalence will differ). We will show this later with
 an example.
 There are also some restrictions we need to impose on our binding clauses in
-comparison to the ones of Ott. The main idea behind these restrictions is
+comparison to Ott. The main idea behind these restrictions is
 that we obtain a notion of alpha-equivalence where it is ensured
 that within a given scope an atom occurrence cannot be both bound and free
 at the same time.  The first restriction is that a body can only occur in
 \emph{one} binding clause of a term constructor. So for example
 \end{tabular}}
 \]\smallskip
 \noindent
-In these specifications @{text "name"} refers to an atom type, and @{text
+In these specifications @{text "name"} refers to a (concrete) atom type, and @{text
 "fset"} to the type of finite sets.  Note that for @{text Lam} it does not
 matter which binding mode we use. The reason is that we bind only a single
 @{text name}, in which case all three binding modes coincide. However, having
 \isacommand{binds (set)} or just \isacommand{binds}
 in the second case makes a difference to the semantics of the specification
 \isacommand{nominal\_datatype} @{text trm} $=$\\
 \hspace{5mm}\phantom{$\mid$}~@{term "Var name"}\\
 \hspace{5mm}$\mid$~@{term "App trm trm"}\\
 \hspace{5mm}$\mid$~@{text "Lam x::name t::trm"}
 \;\;\isacommand{binds} @{text x} \isacommand{in} @{text t}\\
-\hspace{5mm}$\mid$~@{text "Let p::pat trm t::trm"}
+\hspace{5mm}$\mid$~@{text "Let_pat p::pat trm t::trm"}
 \;\;\isacommand{binds} @{text "bn(p)"} \isacommand{in} @{text t}\\
 \isacommand{and} @{text pat} $=$\\
 \hspace{5mm}\phantom{$\mid$}~@{text PNil}\\
 \hspace{5mm}$\mid$~@{text "PVar name"}\\
 \hspace{5mm}$\mid$~@{text "PTup pat pat"}\\
 \eqref{cases} and \eqref{induct} boil down to the following three inference
 rules (the cases lemmas are on the left-hand side; the induction principle
 on the right):
 \begin{equation}\label{inductex}\mbox{
-\begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {}}
+\begin{tabular}{c}
-\begin{tabular}{@ {}c@ {}}
+\multicolumn{1}{@ {\hspace{-5mm}}l}{cases lemmas:}\smallskip\\
 \infer{@{text "P\<^bsub>trm\<^esub>"}}
 {\begin{array}{@ {}l@ {}}
 @{text "\<forall>x. y = Var\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
 @{text "\<forall>x\<^isub>1 x\<^isub>2. y = App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
 @{text "\<forall>x\<^isub>1 x\<^isub>2. y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
-@{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. y = Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub>"}
+@{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. y = Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub>"}
-\end{array}}\medskip\\
+\end{array}}\hspace{10mm}
 \infer{@{text "P\<^bsub>pat\<^esub>"}}
 {\begin{array}{@ {}l@ {}}
 @{text "y = PNil\<^sup>\<alpha>  \<Rightarrow> P\<^bsub>pat\<^esub>"}\\
 @{text "\<forall>x. y = PVar\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>pat\<^esub>"}\\
 @{text "\<forall>x\<^isub>1 x\<^isub>2. y = PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub>"}
-\end{array}}
+\end{array}}\medskip\\
-\end{tabular}
-&
+\multicolumn{1}{@ {\hspace{-5mm}}l}{induction principle:}\smallskip\\
-\begin{tabular}{@ {}c@ {}}
 \infer{@{text "P\<^bsub>trm\<^esub> y\<^isub>1 \<and> P\<^bsub>pat\<^esub> y\<^isub>2"}}
 {\begin{array}{@ {}l@ {}}
 @{text "\<forall>x. P\<^bsub>trm\<^esub> (Var\<^sup>\<alpha> x)"}\\
 @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>trm\<^esub> x\<^isub>1 \<and> P\<^bsub>trm\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
 @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>trm\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
-@{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. P\<^bsub>pat\<^esub> x\<^isub>1 \<and> P\<^bsub>trm\<^esub> x\<^isub>2 \<and> P\<^bsub>trm\<^esub> x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub> (Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3)"}\\
+@{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. P\<^bsub>pat\<^esub> x\<^isub>1 \<and> P\<^bsub>trm\<^esub> x\<^isub>2 \<and> P\<^bsub>trm\<^esub> x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub> (Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3)"}\\
 @{text "P\<^bsub>pat\<^esub> (PNil\<^sup>\<alpha>)"}\\
 @{text "\<forall>x. P\<^bsub>pat\<^esub> (PVar\<^sup>\<alpha> x)"}\\
 @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>pat\<^esub> x\<^isub>1 \<and> P\<^bsub>pat\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub> (PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}
 \end{array}}
-\end{tabular}
 \end{tabular}}
 \end{equation}\smallskip
 By working now completely on the alpha-equated level, we
 can first show using \eqref{calphaeqvt} that the support of each term
 problem is to rename them. Unfortunately, this leads to very clunky proofs
 and makes formalisations grievous experiences (especially in the case for
 multiple bound atoms).
-For the older versions of Nominal Isabelle we introduced in
+For the older versions of Nominal Isabelle we described in
-\cite{UrbanTasson05} a method for automatically strengthening weak induction
+\cite{Urban08} a method for automatically strengthening weak induction
 principles. These stronger induction principles allow the user to make
 additional assumptions about bound atoms. The advantage of these assumptions
 is that they make in most cases any renaming of bound atoms unnecessary.  To
 explain how the strengthening works in the presence of multiple binders, we
 use as running example the lambda-calculus with @{text "Let"}-patterns shown
 {\begin{array}{l}
 @{text "\<forall>x c. P\<^bsub>trm\<^esub> c (Var\<^sup>\<alpha> x)"}\\
 @{text "\<forall>x\<^isub>1 x\<^isub>2 c. (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
 @{text "\<forall>x\<^isub>1 x\<^isub>2 c. atom x\<^isub>1 # c \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
 @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3 c. (set (bn\<^sup>\<alpha> x\<^isub>1)) #\<^sup>* c \<and>"}\\
-\hspace{10mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>3) \<Rightarrow> P\<^bsub>trm\<^esub> c (Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3)"}\\
+\hspace{10mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>3) \<Rightarrow> P\<^bsub>trm\<^esub> c (Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3)"}\\
 @{text "\<forall>c. P\<^bsub>pat\<^esub> c (PNil\<^sup>\<alpha>)"}\\
 @{text "\<forall>x c. P\<^bsub>pat\<^esub> c (PVar\<^sup>\<alpha> x)"}\\
 @{text "\<forall>x\<^isub>1 x\<^isub>2 c. (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>pat\<^esub> c (PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}
 \end{array}}
 \end{tabular}}
 stronger induction principle establishes the properties @{text "
 P\<^bsub>trm\<^esub> c y\<^isub>1 \<and> P\<^bsub>pat\<^esub> c y\<^isub>2"} in
 which the additional parameter @{text c} is assumed to be of finite
 support. The purpose of @{text "c"} is to ``control'' which freshness
 assumptions the binders should satisfy in the @{text "Lam\<^sup>\<alpha>"} and
-@{text "Let\<^sup>\<alpha>"} cases: for @{text "Lam\<^sup>\<alpha>"} we can assume the
+@{text "Let_pat\<^sup>\<alpha>"} cases: for @{text "Lam\<^sup>\<alpha>"} we can assume the
 bound atom @{text "x\<^isub>1"} is fresh for @{text "c"}; for @{text
-"Let\<^sup>\<alpha>"} we can assume all bound atoms from an assignment are fresh
+"Let_pat\<^sup>\<alpha>"} we can assume all bound atoms from an assignment are fresh
 for @{text "c"}. If @{text "c"} is instantiated appropriately, the user can
 mimic the ``pencil-and-paper'' reasoning employing the usual variable
-convention.
+convention \cite{Urban08}.
 In what follows we will show that the induction principle in
 \eqref{inductex} implies \eqref{stronginduct}. This fact was established for
-single binders in \cite{UrbanTasson05} by some quite involved, nevertheless
+single binders in \cite{Urban08} by some quite involved, nevertheless
 automated, induction proof. In this paper we simplify the proof by
 leveraging the automated proof methods from the function package of
 Isabelle/HOL \cite{Krauss09}. The reasoning principle behind these methods
 is well-founded induction. To use them in our setting, we have to discharge
 two proof obligations: one is that we have well-founded measures (one for
 each type @{text "ty"}$^\alpha_{1..n}$) that decrease in every induction
-step and the other is that we have covered all cases. Once these two
+step and the other is that we have covered all cases in the induction
-proof obligations are discharged, the reasoning infrastructure in
+principle. Once these two proof obligations are discharged, the reasoning
-the function package will automatically derive the stronger induction
+infrastructure in the function package will automatically derive the
-principle. This considerably simplifies the work we have to do.
+stronger induction principle. This considerably simplifies the work we have
+to do here.
 As measures we can use the size functions @{text "size_ty"}$^\alpha_{1..n}$,
 which we lifted in the previous section and which are all well-founded. It
 is straightforward to establish that the sizes decrease in every
 induction step. What is left to show is that we covered all cases.
 To do so, we have to derive stronger cases lemmas, which look in our
-running example as follows:
+running example are as follows:
 \[\mbox{
-\begin{tabular}{@ {}c@ {\hspace{6mm}}c@ {}}
+\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}
 \infer{@{text "P\<^bsub>trm\<^esub>"}}
 {\begin{array}{@ {}l@ {}}
 @{text "\<forall>x. y = Var\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
 @{text "\<forall>x\<^isub>1 x\<^isub>2. y = App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
 @{text "\<forall>x\<^isub>1 x\<^isub>2. atom x\<^isub>1 # c \<and> y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
-@{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. set (bn\<^sup>\<alpha> x\<^isub>1) #\<^sup>* c \<and> y = Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub>"}
+@{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. set (bn\<^sup>\<alpha> x\<^isub>1) #\<^sup>* c \<and> y = Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub>"}
 \end{array}} &
 \infer{@{text "P\<^bsub>pat\<^esub>"}}
 {\begin{array}{@ {}l@ {}}
 @{text "y = PNil\<^sup>\<alpha>  \<Rightarrow> P\<^bsub>pat\<^esub>"}\\
 \end{array}}
 \end{tabular}}
 \]\smallskip
 \noindent
-These stronger cases lemmas need to be derived from the `weak' cases lemmas given
+They are stronger in the sense that they allow us to assume that the bound
-in \eqref{inductex}. This is trivial in case of patterns (the one on the right-hand side)
+atoms avoid a context @{text "c"} (which is assumed to be finitely
-since weak and strong cases lemma coincide (there is no binding in patterns).
+supported). This is similar with the stronger induction principles.
-Interesting are only the cases for @{text "Lam\<^sup>\<alpha>"} and @{text "Let\<^sup>\<alpha>"}. There the
-stronger cases lemma allow us to assume that the bound atoms avoid the context @{text "c"}
+These stronger cases lemmas need to be derived from the `weak' cases lemmas
-(which is assumed to be finitely supported).
+given in \eqref{inductex}. This is trivial in case of patterns (the one on
+the right-hand side) since the weak and strong cases lemma coincide (there
-Let us show first establish the simpler case for @{text "Lam\<^sup>\<alpha>"}. By the weak cases lemma
+is no binding in patterns).  Interesting are only the cases for @{text
-\eqref{inductex} we can assume that
+"Lam\<^sup>\<alpha>"} and @{text "Let_pat\<^sup>\<alpha>"}, where we have some binders and
+therefore have an addition assumption.  Let us show first establish the case
+for @{text "Lam\<^sup>\<alpha>"}. By the weak cases lemma \eqref{inductex} we can
+assume that
 \begin{equation}\label{assm}
 @{text "y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2"}
 \end{equation}\smallskip
 \noindent
-holds and need to establish @{text "P\<^bsub>trm\<^esub>"}. The stronger cases lemma has the implication
+holds and need to establish @{text "P\<^bsub>trm\<^esub>"}. The stronger cases lemma has the
+corresponding implication
 \begin{equation}\label{imp}
 @{text "\<forall>x\<^isub>1 x\<^isub>2. atom x\<^isub>1 # c \<and> y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}
 \end{equation}\smallskip
 \noindent
 which we can use to infer @{text "P\<^bsub>trm\<^esub>"}. Clearly, we cannot
 use this implication directly, because we have no information whether @{text
 "x\<^isub>1"} is fresh for @{text "c"}.  However, we can use Properties
-\ref{supppermeq} and \ref{avoiding} to rename @{text "x\<^isub>1"}. We know
+\ref{supppermeq} and \ref{avoiding} to rename @{text "x\<^isub>1"}: We know
 by Theorem~\ref{suppfa} that @{text "{atom x\<^isub>1} #\<^sup>* Lam\<^sup>\<alpha>
 x\<^isub>1 x\<^isub>2"} (since its support is @{text "supp x\<^isub>2 -
 {atom x\<^isub>1}"}). Property \ref{avoiding} provides us therefore with a
 permutation @{text "\<pi>"}, such that @{text "{atom (\<pi> \<bullet> x\<^isub>1)} #\<^sup>*
 c"} and \mbox{@{text "supp (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2) #\<^sup>* \<pi>"}} hold.
 By using Property \ref{supppermeq}, we can infer from the latter that @{text
-"Lam\<^sup>\<alpha> (\<pi> \<bullet> x\<^isub>1) (\<pi> \<bullet> x\<^isub>2) = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2"}. We can use this in the assumption
+"Lam\<^sup>\<alpha> (\<pi> \<bullet> x\<^isub>1) (\<pi> \<bullet> x\<^isub>2) = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2"} holds. We can use this equation in
-\eqref{assm} and then use \eqref{imp} to conclude this case.
+the assumption \eqref{assm} and then use \eqref{imp} with the renamed @{text "\<pi> \<bullet> x\<^isub>1"}
+and @{text "\<pi> \<bullet> x\<^isub>2"} in order to conclude this case.
-The @{text "Let\<^sup>\<alpha>"}-case involving a (non-recursive) deep binder is more complicated.
+The @{text "Let_pat\<^sup>\<alpha>"}-case involving a deep binder is slightly more complicated.
 We have the assumption
-\begin{equation}\label{assm}
+\begin{equation}\label{assmtwo}
-@{text "y = Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3"}
+@{text "y = Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3"}
 \end{equation}\smallskip
 \noindent
-and as implication
+and the implication
 \[
+@{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. set (bn\<^sup>\<alpha> x\<^isub>1) #\<^sup>* c \<and> y = Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub>"}
 \]\smallskip
+\noindent
-The reason is that the we cannot apply Property \ref{avoiding} to the whole term @{text "Let p t"},
+The reason that this case is more complicated is that we cannot apply directly Property
+\ref{avoiding} for obtaining a renaming permutation. Property \ref{avoiding} requires
+that the binders are fresh for the term in which we want to perform the renaming. But
+this is not true in cases like (using informal notation)
+\[
+@{text "Let (x, y) := (x, y) in (x, y)"}
+\]\smallskip
+\noindent
+Although @{text x} and @{text y} are bound in this term, they are also free
+in the assignment. We can, however, obtain obtain such a renaming
+permutation, say @{text "\<pi>"}, for the abstraction @{term "Abs_lst (bn_al
+x\<^isub>1) x\<^isub>3"}. So we have \mbox{@{term "set (bn_al (\<pi> \<bullet>
+x\<^isub>1)) \<sharp>* c"}} and @{term "Abs_lst (bn_al (\<pi> \<bullet> x\<^isub>1)) (\<pi> \<bullet>
+x\<^isub>3) = Abs_lst (bn_al x\<^isub>1) x\<^isub>3"} (remember @{text "set"} and @{text "bn\<^sup>\<alpha>"} are equivariant).
+Now the quasi-injective property for @{text "Let_pat\<^sup>\<alpha>"} states
+\[
+\infer{@{text "Let_pat\<^sup>\<alpha> p t\<^isub>1 t\<^isub>2 = Let_pat\<^sup>\<alpha> p\<PRIME> t\<PRIME>\<^isub>1 t\<PRIME>\<^isub>2"}}
+{@{text "[bn\<^sup>\<alpha> p]\<^bsub>list\<^esub>. t\<^isub>2 = [bn\<^sup>\<alpha> p']\<^bsub>list\<^esub>. t\<PRIME>\<^isub>2"}\;\; &
+@{text "p \<approx>\<AL>\<^bsub>bn\<^esub> p\<PRIME>"}\;\; & @{text "t\<^isub>1 = t\<PRIME>\<^isub>1"}}
+\]\smallskip
+\noindent
+Since all atoms in a pattern are bound by @{text "Let_pat\<^sup>\<alpha>"}
+(hence @{text "(\<pi> \<bullet> x\<^isub>1) \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} holds for every @{text "\<pi>"}), we can infer the
+equation
+\[
+@{text "Let_pat\<^sup>\<alpha> (\<pi> \<bullet> x\<^isub>1) x\<^isub>2 (\<pi> \<bullet> x\<^isub>3) = Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3"}
+\]\smallskip
+\noindent
+Taking the left-hand side as our assumption in \eqref{assmtwo}, we can use
+the implication from the stronger cases lemma to infer @{text "P\<^bsub>trm\<^esub>"}, as needed.
+The remaining difficulty is when a deep binder contains atoms that are bound, but
+also that are free.
+to the whole term @{text "Let_pat x\<^isub>1 x\<^isub>2 x\<^isub>3"},
 because @{text p} might contain names bound by @{text bn}, but also some that are
 free. To solve this problem we have to introduce a permutation function that only
 permutes names bound by @{text bn} and leaves the other names unchanged. We do this again
 by lifting. For a
 clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, we define

changeset 3018	65452cf6f5ae
parent 3017	014f0ea2381c
child 3019	10fa937255da