--- a/Paper/Paper.thy Fri Mar 26 18:44:47 2010 +0100
+++ b/Paper/Paper.thy Fri Mar 26 22:02:59 2010 +0100
@@ -6,8 +6,6 @@
consts
fv :: "'a \<Rightarrow> 'b"
abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
- Abs_lst :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
- Abs_res :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
definition
"equal \<equiv> (op =)"
@@ -19,9 +17,9 @@
supp ("supp _" [78] 73) and
uminus ("-_" [78] 73) and
If ("if _ then _ else _" 10) and
- alpha_gen ("_ \<approx>\<^raw:\makebox[0mm][l]{$\,_{\textit{set}}$}>\<^bsup>_,_,_\<^esup> _") and
- alpha_lst ("_ \<approx>\<^raw:\makebox[0mm][l]{$\,_{\textit{list}}$}>\<^bsup>_,_,_\<^esup> _") and
- alpha_res ("_ \<approx>\<^raw:\makebox[0mm][l]{$\,_{\textit{res}}$}>\<^bsup>_,_,_\<^esup> _") and
+ alpha_gen ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{set}}$}}>\<^bsup>_,_,_\<^esup> _") and
+ alpha_lst ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_,_,_\<^esup> _") and
+ alpha_res ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{res}}$}}>\<^bsup>_,_,_\<^esup> _") and
abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
fv ("fv'(_')" [100] 100) and
equal ("=") and
@@ -412,9 +410,9 @@
\noindent
For a proof see \cite{HuffmanUrban10}.
- \begin{property}
- @{thm[mode=IfThen] at_set_avoiding[no_vars]}
- \end{property}
+ %\begin{property}
+ %@{thm[mode=IfThen] at_set_avoiding[no_vars]}
+ %\end{property}
*}
@@ -444,8 +442,8 @@
variables; moreover there must be a permutation @{text p} such that {\it
ii)} it leaves the free variables of @{text x} and @{text y} unchanged, but
{\it iii)} ``moves'' their bound names so that we obtain modulo a relation,
- say \mbox{@{text "_ R _"}}, two equal terms. We also require {\it iv)} that
- @{text p} makes the abstracted sets @{text as} and @{text bs} equal. The
+ say \mbox{@{text "_ R _"}}, two equivalent terms. We also require {\it iv)} that
+ @{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
requirements {\it i)} to {\it iv)} can be stated formally as follows:
%
\begin{equation}\label{alphaset}
@@ -502,7 +500,8 @@
\end{equation}
\begin{exmple}\rm
- It might be useful to consider some examples for how these definitions pan out in practise.
+ It might be useful to consider some examples for how these definitions of alpha-equivalence
+ pan out in practise.
For this consider the case of abstracting a set of variables over types (as in type-schemes).
We set @{text R} to be the equality and for @{text "fv(T)"} we define
@@ -556,55 +555,53 @@
In the rest of this section we are going to introduce a type- and term-constructor
- for abstractions. For this we define
+ for abstractions. For this we define (similarly for $\approx_{\textit{abs\_list}}$
+ and $\approx_{\textit{abs\_res}}$)
%
\begin{equation}
@{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_gen (as, x) equal supp p (bs, x)"}
\end{equation}
\noindent
- Similarly for @{text "abs_list"} and @{text "abs_res"}. We can show that these
- relations are equivalence relations and equivariant
+ We can show that these relations are equivalence relations and equivariant
(we only show the $\approx_{\textit{abs\_set}}$-case).
- \begin{lemma}
+ \begin{lemma}\label{alphaeq}
$\approx_{\textit{abs\_set}}$ is an equivalence
- relations, and if @{term "abs_set (as, x) (bs, x)"} then also
- @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> x)"}.
+ relations, and if @{term "abs_set (as, x) (bs, y)"} then also
+ @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"}.
\end{lemma}
\begin{proof}
Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have
a permutation @{text p} and for the proof obligation take @{term "-p"}. In case
- of transitivity we have two permutations @{text p} and @{text q}, and for the
- proof obligation use @{text "q + p"}. All the conditions are then by simple
+ of transitivity, we have two permutations @{text p} and @{text q}, and for the
+ proof obligation use @{text "q + p"}. All conditions are then by simple
calculations.
\end{proof}
+ \noindent
+ We are also define the following two auxiliary functions taking a pair
+ as argument.
+ %
+ \begin{equation}\label{aux}
+ \begin{array}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+ @{text "aux (as, x)"} & @{text "\<equiv>"} & @{text "supp x - as"}\\
+ @{text "aux_list (bs, x)"} & @{text "\<equiv>"} & @{text "supp x - set bs"}
+ \end{array}
+ \end{equation}
+
\noindent
- The following lemma (and similar ones for $\approx_{\textit{abs\_list}}$ and
- $\approx_{\textit{abs\_res}}$) will be crucial below:
-
- \begin{lemma}
- @{thm[mode=IfThen] alpha_abs_swap[no_vars]}
- \end{lemma}
+ The point of these two functions is that they are preserved under
+ alpha-equivalence, that means for instance
+ %
+ \begin{equation}\label{auxpreserved}
+ @{term "abs_set (as, x) (bs, y)"} \;\;\text{implies}\;\;
+ @{term "aux (as, x) = aux (bs, y)"}
+ \end{equation}
- \begin{proof}
- This lemma is straightforward by observing that the assumptions give us
- @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - bs) = (supp x - bs)"} and that @{text supp}
- is equivariant.
- \end{proof}
-
- \noindent
- We are also define the following
-
- @{text "aux (as, x) \<equiv> supp x - as"}
-
-
-
- \noindent
- This allows us to use our quotient package and introduce new types
- @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}
+ Lemma \ref{alphaeq} allows us to use our quotient package and introduce
+ new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}
representing the alpha-equivalence classes. Elements in these types
we will, respectively, write as:
@@ -614,6 +611,28 @@
@{term "Abs_res as x"}
\end{center}
+ \noindent
+ By definition we have
+
+ \begin{center}
+ @{thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;iff\;
+ @{thm (rhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}
+ \end{center}
+
+
+ \noindent
+ The following lemma (and similar ones for $\approx_{\textit{abs\_list}}$ and
+ $\approx_{\textit{abs\_res}}$) will be crucial below:
+
+ \begin{lemma}
+ @{thm[mode=IfThen] abs_swap1(1)[no_vars]}
+ \end{lemma}
+
+ \begin{proof}
+ This lemma is straightforward by observing that the assumptions give us
+ @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - bs) = (supp x - bs)"} and that @{text supp}
+ is equivariant.
+ \end{proof}
\begin{lemma}
$supp ([as]set. x) = supp x - as$
@@ -1000,6 +1019,13 @@
text {*
Complication when the single scopedness restriction is lifted (two
overlapping permutations)
+
+
+ The formalisation presented here will eventually become part of the
+ Isabelle distribution, but for the moment it can be downloaded from
+ the Mercurial repository linked at
+ \href{http://isabelle.in.tum.de/nominal/download}
+ {http://isabelle.in.tum.de/nominal/download}.\medskip
*}
text {*