--- a/LMCS-Paper/Paper.thy Wed Sep 14 22:44:28 2011 +0200
+++ b/LMCS-Paper/Paper.thy Thu Sep 15 01:01:43 2011 +0200
@@ -9,6 +9,7 @@
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"
@@ -54,18 +55,26 @@
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> _")
(*>*)
@@ -640,7 +649,7 @@
*}
-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
@@ -1680,7 +1689,7 @@
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')"} &
@@ -1703,7 +1712,7 @@
{@{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
@@ -1855,9 +1864,24 @@
\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}}$
- are replaced by $\approx_{\textit{set}}^{=, \textit{fa}}$ (similarly for the
- other binding modes).
+ in case of binders the relations @{text "\<approx>ty"}$_{1..n}$ are all replaced
+ by equality. Recall the alpha-equivalence rules for @{text "Let"} and @{text "Let_rec"}
+ 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
@@ -2009,10 +2033,57 @@
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
@@ -2060,7 +2131,7 @@
@{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)"}