nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:3d6df74fc934
+:1f613b24fff8
 alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
 Abs ("[_]\<^raw:$\!$>\<^bsub>set\<^esub>._" [20, 101] 999) and
 Abs_lst ("[_]\<^raw:$\!$>\<^bsub>list\<^esub>._") and
 Abs_res ("[_]\<^raw:$\!$>\<^bsub>res\<^esub>._") and
 Cons ("_::_" [78,77] 73) and
-supp_gen ("aux _" [1000] 100)
+supp_gen ("aux _" [1000] 10)
 (*>*)
 section {* Introduction *}
 \begin{property}\label{supppermeq}
 @{thm[mode=IfThen] supp_perm_eq[no_vars]}
 \end{property}
 \begin{property}
-For a finite set @{text xs} and a finitely supported @{text x} with
+For a finite set @{text as} and a finitely supported @{text x} with
-@{term "xs \<sharp>* x"} and also a finitely supported @{text c}, there
+@{term "as \<sharp>* x"} and also a finitely supported @{text c}, there
-exists a permutation @{text p} such that @{term "(p \<bullet> xs) \<sharp>* c"} and
+exists a permutation @{text p} such that @{term "(p \<bullet> as) \<sharp>* c"} and
 @{term "supp x \<sharp>* p"}.
 \end{property}
 \noindent
-The idea behind the second property is that given a finite set @{text xs}
+The idea behind the second property is that given a finite set @{text as}
 of binders (being bound in @{text x} which is ensured by the
-assumption @{term "xs \<sharp>* x"}), then there exists a permutation @{text p} such that
+assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text p} such that
-the renamed binders @{term "p \<bullet> xs"} avoid the @{text c} (which can be arbitrarily chosen
+the renamed binders @{term "p \<bullet> as"} avoid the @{text c} (which can be arbitrarily chosen
 as long as it is finitely supported) and also does not affect anything
 in the support of @{text x} (that is @{term "supp x \<sharp>* p"}). The last
 fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders
 in @{text x}, because @{term "p \<bullet> x = x"}.
 "p"}. Alpha-equivalence between two pairs is then the relation where we
 existentially quantify over this @{text "p"}. Also note that the relation is
 dependent on a free-variable function @{text "fv"} and a relation @{text
 "R"}. The reason for this extra generality is that we will use
 $\approx_{\textit{set}}$ for both ``raw'' terms and alpha-equated terms. In
-the latter case, $R$ will be replaced by equality @{text "="} and for raw terms we
+the latter case, $R$ will be replaced by equality @{text "="} and we
 will prove that @{text "fv"} is equal to the support of @{text
 x} and @{text y}.
 The definition in \eqref{alphaset} does not make any distinction between the
 order of abstracted variables. If we want this, then we can define alpha-equivalence
 @{term "Abs_lst as x"} \hspace{5mm}
 @{term "Abs_res as x"}
 \end{center}
 \noindent
-indicating that a set or list is abstracted in @{text x}. We will call the types
+indicating that a set or list @{text as} is abstracted in @{text x}. We will
-\emph{abstraction types} and their elements \emph{abstractions}. The important
+call the types \emph{abstraction types} and their elements
-property we need is a characterisation for the support of abstractions, namely
+\emph{abstractions}. The important property we need is a characterisation
+for the support of abstractions, namely:
 \begin{thm}[Support of Abstractions]\label{suppabs}
 Assuming @{text x} has finite support, then\\[-6mm]
 \begin{center}
 \begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
 @{thm (lhs) supp_abs(1)[no_vars]} & $=$ & @{thm (rhs) supp_abs(1)[no_vars]}\\
 @{thm (lhs) supp_abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_abs(2)[no_vars]}\\
-@{thm (lhs) supp_abs(3)[no_vars]} & $=$ & @{thm (rhs) supp_abs(3)[no_vars]}
+@{thm (lhs) supp_abs(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_abs(3)[where bs="as", no_vars]}
 \end{tabular}
 \end{center}
 \end{thm}
 \noindent
-We will only show the first equation as the others
+We will show below the first equation as the others
 follow similar arguments. By definition of the abstraction type @{text "abs_set"}
 we have
 %
 \begin{equation}\label{abseqiff}
 @{thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\;
 \begin{equation}
 @{thm permute_Abs[no_vars]}
 \end{equation}
 \noindent
-The last fact derives from the definition of permutations acting on pairs
+The second fact derives from the definition of permutations acting on pairs
-(see \eqref{permute}) and alpha-equivalence being equivariant (see Lemma~\ref{alphaeq}).
+(see \eqref{permute}) and alpha-equivalence being equivariant
+(see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show
-With these two facts at our disposal, we can show the following lemma
+the following lemma about swapping two atoms.
-about swapping two atoms.
 \begin{lemma}
-@{thm[mode=IfThen] abs_swap1(1)[no_vars]}
+@{thm[mode=IfThen] abs_swap1(1)[where bs="as", no_vars]}
 \end{lemma}
 \begin{proof}
 By using \eqref{abseqiff}, this lemma is straightforward when observing that
-the assumptions give us
+the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}
-@{term "(a \<rightleftharpoons> b) \<bullet> (supp x - bs) = (supp x - bs)"} and that @{text supp}
+and that @{text supp} and set difference are equivariant.
-and set difference are equivariant.
 \end{proof}
 \noindent
-This lemma gives us
+This lemma allows us to show
 %
 \begin{equation}\label{halfone}
 @{thm abs_supports(1)[no_vars]}
 \end{equation}
 \noindent
-which with Property~\ref{supportsprop} gives us one half of
+which by Property~\ref{supportsprop} gives us ``one half'' of
-Thm~\ref{suppabs}. The other half is a bit more involved. For this we use a
+Thm~\ref{suppabs}. The ``other half'' is a bit more involved. To establish
-trick from \cite{Pitts04} and first define an auxiliary function
+it, we use a trick from \cite{Pitts04} and first define an auxiliary
+function taking an abstraction as argument
 %
 \begin{center}
 @{thm supp_gen.simps[THEN eq_reflection, no_vars]}
 \end{center}
 \noindent
 Using the second equation in \eqref{equivariance}, we can show that
-@{term "supp_gen"} is equivariant and therefore has empty support. This
+@{text "aux"} is equivariant (since @{term "p \<bullet> (supp x - as) =
-in turn means
+(supp (p \<bullet> x)) - (p \<bullet> as)"}) and therefore has empty support.
-%
+This in turn means
-\begin{center}
+%
-@{thm (prem 1) aux_fresh(1)[where bs="as", no_vars]}
+\begin{center}
-\;\;implies\;\;
+@{term "supp (supp_gen (Abs as x)) \<subseteq> supp (Abs as x)"}
-@{thm (concl) aux_fresh(1)[where bs="as", no_vars]}
+\end{center}
-\end{center}
+\noindent
-\noindent
+using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set
-using \eqref{suppfun}. Since @{term "supp x"} is by definition equal
+we further obtain
-to @{term "{a. \<not> a \<sharp> x}"} we can establish that
 %
 \begin{equation}\label{halftwo}
 @{thm (concl) supp_abs_subset1(1)[no_vars]}
 \end{equation}
 \noindent
-provided @{text x} has finite support (the precondition we need in order to show
+since for finite sets, @{text "S"}, we have
-that for a finite set of atoms, we have @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}).
+@{thm (concl) supp_finite_atom_set[no_vars]}).
 Finally taking \eqref{halfone} and \eqref{halftwo} provides us with a proof
 of Theorem~\ref{suppabs}. The point of these general lemmas about abstractions is that we
 can define and prove properties about them conveniently on the Isabelle/HOL level,
-and in addition can use them in what
+but also use them in what follows next when we deal with binding in specifications
-follows next when we have to deal with binding in specifications of term-calculi.
+of term-calculi.
 *}
 section {* Alpha-Equivalence and Free Variables *}
 text {*

changeset 1716	1f613b24fff8
parent 1715	3d6df74fc934
child 1717	a3ef7fba983f