nominal2: comparison LMCS-Paper/Paper.thy

equal deleted inserted replaced

-:4fafa8d219dc
+:799769b40f0e
 consts
 fv :: "'a \<Rightarrow> 'b"
 abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
 alpha_bn :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 abs_set2 :: "'a \<Rightarrow> perm \<Rightarrow> 'b \<Rightarrow> 'c"
+equ2 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 Abs_dist :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
 Abs_print :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
 definition
 "equal \<equiv> (op =)"
 supp_set ("aux _" [1000] 10) and
 alpha_bn ("_ \<approx>bn _")
 consts alpha_trm ::'a
 consts fa_trm :: 'a
+consts fa_trm_al :: 'a
 consts alpha_trm2 ::'a
 consts fa_trm2 :: 'a
+consts fa_trm2_al :: 'a
+consts supp2 :: 'a
 consts ast :: 'a
 consts ast' :: 'a
+consts bn_al :: "'b \<Rightarrow> 'a"
 notation (latex output)
 alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and
 fa_trm ("fa\<^bsub>trm\<^esub>") and
+fa_trm_al ("fa\<AL>\<^bsub>trm\<^esub>") and
 alpha_trm2 ("'(\<approx>\<^bsub>assn\<^esub>, \<approx>\<^bsub>trm\<^esub>')") and
 fa_trm2 ("'(fa\<^bsub>assn\<^esub>, fa\<^bsub>trm\<^esub>')") and
+fa_trm2_al ("'(fa\<AL>\<^bsub>assn\<^esub>, fa\<AL>\<^bsub>trm\<^esub>')") and
 ast ("'(as, t')") and
-ast' ("'(as', t\<PRIME> ')")
+ast' ("'(as', t\<PRIME> ')") and
+equ2 ("'(=, =')") and
+supp2 ("'(supp, supp')") and
+bn_al ("bn\<^sup>\<alpha> _")
 (*>*)
 section {* Introduction *}
 use of these properties in order to define alpha-equivalence in
 the presence of multiple binders.
 *}
-section {* General Bindings\label{sec:binders} *}
+section {* Abstractions\label{sec:binders} *}
 text {*
 In Nominal Isabelle, the user is expected to write down a specification of a
 term-calculus and then a reasoning infrastructure is automatically derived
 from this specification (remember that Nominal Isabelle is a definitional
 Again let us take a look at a concrete example for these definitions. For
 the specification given in \eqref{letrecs}
 we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
 $\approx_{\textit{bn}}$ with the following clauses:
-\[\mbox{
+\begin{equation}\label{rawalpha}\mbox{
 \begin{tabular}{@ {}c @ {}}
 \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
 {@{term "alpha_lst_ex (bn as, t) alpha_trm fa_trm (bn as', t')"} &
 \hspace{5mm}@{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\\
 \\
 \infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\hspace{9mm}
 \infer{@{text "ACons a t as \<approx>\<^bsub>bn\<^esub> ACons a' t' as"}}
 {@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & \hspace{5mm}@{text "as \<approx>\<^bsub>bn\<^esub> as'"}}
 \end{tabular}
 \end{tabular}}
-\]\smallskip
+\end{equation}\smallskip
 \noindent
 Notice the difference between  $\approx_{\textit{assn}}$ and
 $\approx_{\textit{bn}}$: the latter only ``tracks'' alpha-equivalence of
 the components in an assignment that are \emph{not} bound. This is needed in the
 \]\smallskip
 \noindent
 We call these conditions as \emph{quasi-injectivity}. They correspond to
 the premises in our alpha-equiva\-lence relations, with the exception that
-in case of binders the relations $\approx_{\textit{set}}^{\textit{R}, \textit{fa}}$
+in case of binders the relations @{text "\<approx>ty"}$_{1..n}$ are all replaced
-are replaced by $\approx_{\textit{set}}^{=, \textit{fa}}$ (similarly for the
+by equality. Recall the alpha-equivalence rules for @{text "Let"} and @{text "Let_rec"}
-other binding modes).
+shown in \eqref{rawalpha}. For @{text "Let\<^sup>\<alpha>"} and @{text "Let_rec\<^sup>\<alpha>"} we have
+\begin{equation}\label{alphalift}\mbox{
+\begin{tabular}{@ {}c @ {}}
+\infer{@{text "Let\<^sup>\<alpha> as t = Let\<^sup>\<alpha> as' t'"}}
+{@{term "alpha_lst_ex (bn_al as, t) equal fa_trm_al (bn as', t')"} &
+\hspace{5mm}@{text "as \<approx>\<AL>\<^bsub>bn\<^esub> as'"}}\\
+\\
+\makebox[0mm]{\infer{@{text "Let_rec\<^sup>\<alpha> as t = Let_rec\<^sup>\<alpha> as' t'"}}
+{@{term "alpha_lst_ex (bn_al as, ast) equ2 fa_trm2_al (bn_al as', ast')"}}}\\
+\end{tabular}}
+\end{equation}\smallskip
+\noindent
+where @{text "\<approx>\<^bsub>trm\<^esub>"} and @{text "\<approx>\<^bsub>assn\<^esub>"} are replaced by @{text "="} (and similarly
+the free-atom and binding functions are replaced by their lifted counterparts).
 Next we can lift the permutation operations defined in \eqref{ceqvt}. In
 order to make this lifting to go through, we have to show that the
 permutation operations are respectful. This amounts to showing that the
 alpha-equivalence relations are equivariant, which
 The proof is by induction. In each case
 we unfold the definition of @{text "supp"}, move the swapping inside the
 term-constructors and then use the quasi-injectivity lemmas in order to complete the
 proof. For the abstraction cases we use then the facts derived in Theorem~\ref{suppabs},
 for which we have to know that every body of an abstraction is finitely supported.
-This we have proved earlier.
+This, we have proved earlier.
 \end{proof}
 \noindent
+Consequently we can simplify the quasi-injection lemmas, for example the ones
+given in \eqref{alphalift} for @{text "Let\<^sup>\<alpha>"} and @{text "Let_rec\<^sup>\<alpha>"} to
+\[\mbox{
+\begin{tabular}{@ {}c @ {}}
+\infer{@{text "Let\<^sup>\<alpha> as t = Let\<^sup>\<alpha> as' t'"}}
+{@{term "alpha_lst_ex (bn_al as, t) equal supp (bn_al as', t')"} &
+\hspace{5mm}@{text "as \<approx>\<AL>\<^bsub>bn\<^esub> as'"}}\\
+\\
+\makebox[0mm]{\infer{@{text "Let_rec\<^sup>\<alpha> as t = Let_rec\<^sup>\<alpha> as' t'"}}
+{@{term "alpha_lst_ex (bn_al as, ast) equ2 supp2 (bn_al as', ast')"}}}\\
+\end{tabular}}
+\]\smallskip
+\noindent
+Taking the fact into account that @{term "equ2"} and @{term "supp2"} are
+by definition equal to @{term "equal"} and @{term "supp"}, respectively,
+the above rules simplify even further to
+\[\mbox{
+\begin{tabular}{@ {}c @ {}}
+\infer{@{text "Let\<^sup>\<alpha> as t = Let\<^sup>\<alpha> as' t'"}}
+{@{term "Abs_lst (bn_al as) t = Abs_lst (bn_al as') t'"} &
+\hspace{5mm}@{text "as \<approx>\<AL>\<^bsub>bn\<^esub> as'"}}\\
+\\
+\makebox[0mm]{\infer{@{text "Let_rec\<^sup>\<alpha> as t = Let_rec\<^sup>\<alpha> as' t'"}}
+{@{term "Abs_lst (bn_al as) ast = Abs_lst (bn_al as') ast'"}}}\\
+\end{tabular}}
+\]\smallskip
+\noindent
+which means we can characterise equality between term-constructors in terms
+of equality between the abstractions defined in Section~\ref{sec:binders}. From this
+we can derive the support for @{text "Let\<^sup>\<alpha>"} and
+@{text "Let_rec\<^sup>\<alpha>"}, namely
+\[\mbox{
+\begin{tabular}{l@ {\hspace{2mm}}l@ {\hspace{2mm}}l}
+@{text "supp (Let\<^sup>\<alpha> as t)"} & @{text "="} & @{text "(supp t - set (bn\<^sup>\<alpha> as)) \<union> fa\<AL>\<^bsub>bn\<^esub> as"}\\
+@{text "supp (Let_rec\<^sup>\<alpha> as t)"} & @{text "="} & @{text "(supp t \<union> supp as) - set (bn\<^sup>\<alpha> as)"}\\
+\end{tabular}}
+\]\smallskip
+\noindent
+using the support of abstractions derived in Theorem~\ref{suppabs}.
 To sum up this section, we can establish a reasoning infrastructure for the
 types @{text "ty\<AL>"}$_{1..n}$ by first lifting definitions from the
 ``raw'' level to the quotient level and then by proving facts about
 these lifted definitions. All necessary proofs are generated automatically
 by custom ML-code.
 \infer{@{text "P\<^bsub>trm\<^esub> c y\<^isub>1 \<and> P\<^bsub>pat\<^esub> c y\<^isub>2"}}
 {\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} #\<^sup>* 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 c. (set (bn x\<^isub>1)) #\<^sup>* c \<and> (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
+@{text "\<forall>x\<^isub>1 x\<^isub>2 c. (set (bn\<^sup>\<alpha> x\<^isub>1)) #\<^sup>* c \<and> (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
 @{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}}

changeset 3016	799769b40f0e
parent 3015	4fafa8d219dc
child 3017	014f0ea2381c