# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1316041303 -7200
# Node ID 799769b40f0e9c8168510414fa5ce2fa46267276
# Parent  4fafa8d219dc28381bfd3240bd8a2fd5c49a1568
more on the paper

diff -r 4fafa8d219dc -r 799769b40f0e LMCS-Paper/Paper.thy
--- 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)"}