# HG changeset patch # User Christian Urban # Date 1269954462 -7200 # Node ID 1f613b24fff843ebefc6fbccefe0a8e89f1b2d60 # Parent 3d6df74fc934468a40f9fdf727d94a325ed1cc8e merged diff -r 3d6df74fc934 -r 1f613b24fff8 Paper/Paper.thy --- a/Paper/Paper.thy Tue Mar 30 13:58:07 2010 +0200 +++ b/Paper/Paper.thy Tue Mar 30 15:07:42 2010 +0200 @@ -28,7 +28,7 @@ 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) (*>*) @@ -556,17 +556,17 @@ \end{property} \begin{property} - For a finite set @{text xs} and a finitely supported @{text x} with - @{term "xs \* x"} and also a finitely supported @{text c}, there - exists a permutation @{text p} such that @{term "(p \ xs) \* c"} and + For a finite set @{text as} and a finitely supported @{text x} with + @{term "as \* x"} and also a finitely supported @{text c}, there + exists a permutation @{text p} such that @{term "(p \ as) \* c"} and @{term "supp x \* 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 \* x"}), then there exists a permutation @{text p} such that - the renamed binders @{term "p \ xs"} avoid the @{text c} (which can be arbitrarily chosen + assumption @{term "as \* x"}), then there exists a permutation @{text p} such that + the renamed binders @{term "p \ 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 \* p"}). The last fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders @@ -625,7 +625,7 @@ 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}. @@ -759,9 +759,10 @@ \end{center} \noindent - indicating that a set or list is abstracted in @{text x}. We will call the types - \emph{abstraction types} and their elements \emph{abstractions}. The important - property we need is a characterisation for the support of abstractions, namely + indicating that a set or list @{text as} is abstracted in @{text x}. We will + call the types \emph{abstraction types} and their elements + \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] @@ -769,13 +770,13 @@ \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 % @@ -792,34 +793,33 @@ \end{equation} \noindent - The last fact derives from the definition of permutations acting on pairs - (see \eqref{permute}) and alpha-equivalence being equivariant (see Lemma~\ref{alphaeq}). - - With these two facts at our disposal, we can show the following lemma - about swapping two atoms. + The second fact derives from the definition of permutations acting on pairs + (see \eqref{permute}) and alpha-equivalence being equivariant + (see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show + the following lemma 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 - @{term "(a \ b) \ (supp x - bs) = (supp x - bs)"} and that @{text supp} - and set difference are equivariant. + By using \eqref{abseqiff}, this lemma is straightforward when observing that + the assumptions give us @{term "(a \ b) \ (supp x - as) = (supp x - as)"} + and that @{text supp} 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 - Thm~\ref{suppabs}. The other half is a bit more involved. For this we use a - trick from \cite{Pitts04} and first define an auxiliary function + which by Property~\ref{supportsprop} gives us ``one half'' of + Thm~\ref{suppabs}. The ``other half'' is a bit more involved. To establish + 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]} @@ -827,32 +827,31 @@ \noindent Using the second equation in \eqref{equivariance}, we can show that - @{term "supp_gen"} is equivariant and therefore has empty support. This - in turn means + @{text "aux"} is equivariant (since @{term "p \ (supp x - as) = + (supp (p \ x)) - (p \ as)"}) and therefore has empty support. + This in turn means % \begin{center} - @{thm (prem 1) aux_fresh(1)[where bs="as", no_vars]} - \;\;implies\;\; - @{thm (concl) aux_fresh(1)[where bs="as", no_vars]} + @{term "supp (supp_gen (Abs as x)) \ supp (Abs as x)"} \end{center} \noindent - using \eqref{suppfun}. Since @{term "supp x"} is by definition equal - to @{term "{a. \ a \ x}"} we can establish that + using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set + we further obtain % \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 - that for a finite set of atoms, we have @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}). + since for finite sets, @{text "S"}, we have + @{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 - follows next when we have to deal with binding in specifications of term-calculi. + but also use them in what follows next when we deal with binding in specifications + of term-calculi. *} section {* Alpha-Equivalence and Free Variables *}