--- a/Nominal-General/nominal_thmdecls.ML Mon Apr 26 10:01:13 2010 +0200
+++ b/Nominal-General/nominal_thmdecls.ML Mon Apr 26 20:19:42 2010 +0200
@@ -34,6 +34,7 @@
val get_eqvts_thms: Proof.context -> thm list
val get_eqvts_raw_thms: Proof.context -> thm list
val eqvt_transform: Proof.context -> thm -> thm
+ val is_eqvt: Proof.context -> term -> bool
(* TEMPORARY FIX *)
val add_thm: thm -> Context.generic -> Context.generic
@@ -43,44 +44,20 @@
structure Nominal_ThmDecls: NOMINAL_THMDECLS =
struct
-fun get_ps trm =
- case trm of
- Const (@{const_name permute}, _) $ p $ (Bound _) =>
- raise TERM ("get_ps called on bound", [trm])
- | Const (@{const_name permute}, _) $ p $ _ => [p]
- | t $ u => get_ps t @ get_ps u
- | Abs (_, _, t) => get_ps t
- | _ => []
-
-fun put_p p trm =
- case trm of
- Bound _ => trm
- | Const _ => trm
- | t $ u => put_p p t $ put_p p u
- | Abs (x, ty, t) => Abs (x, ty, put_p p t)
- | _ => mk_perm p trm
-
-(* tests whether there is a disagreement between the permutations,
- and that there is at least one permutation *)
-fun is_bad_list [] = true
- | is_bad_list [_] = false
- | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true
-
-
structure EqvtData = Generic_Data
( type T = thm Item_Net.T;
val empty = Thm.full_rules;
val extend = I;
- val merge = Item_Net.merge );
+ val merge = Item_Net.merge);
structure EqvtRawData = Generic_Data
-( type T = thm Item_Net.T;
- val empty = Thm.full_rules;
+( type T = thm Symtab.table;
+ val empty = Symtab.empty;
val extend = I;
- val merge = Item_Net.merge );
+ val merge = Symtab.merge (K true));
val eqvts = Item_Net.content o EqvtData.get;
-val eqvts_raw = Item_Net.content o EqvtRawData.get;
+val eqvts_raw = map snd o Symtab.dest o EqvtRawData.get;
val get_eqvts_thms = eqvts o Context.Proof;
val get_eqvts_raw_thms = eqvts_raw o Context.Proof;
@@ -90,14 +67,46 @@
fun add_raw_thm thm =
case prop_of thm of
- Const ("==", _) $ _ $ _ => (EqvtRawData.map o Item_Net.update) thm
- | _ => raise THM ("Theorem must be a meta-equality", 0, [thm])
+ Const ("==", _) $ _ $ Const (c, _) => EqvtRawData.map (Symtab.update (c, thm))
+ | _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm])
-val del_raw_thm = EqvtRawData.map o Item_Net.remove;
+fun del_raw_thm thm =
+ case prop_of thm of
+ Const ("==", _) $ _ $ Const (c, _) => EqvtRawData.map (Symtab.delete c)
+ | _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm])
+
+fun is_eqvt ctxt trm =
+ case trm of
+ Const (c, _) => Symtab.defined (EqvtRawData.get (Context.Proof ctxt)) c
+ | _ => raise TERM ("Term must be a constsnt.", [trm])
+
(** transformation of eqvt lemmas **)
+fun get_perms trm =
+ case trm of
+ Const (@{const_name permute}, _) $ _ $ (Bound _) =>
+ raise TERM ("get_perms called on bound", [trm])
+ | Const (@{const_name permute}, _) $ p $ _ => [p]
+ | t $ u => get_perms t @ get_perms u
+ | Abs (_, _, t) => get_perms t
+ | _ => []
+
+fun put_perm p trm =
+ case trm of
+ Bound _ => trm
+ | Const _ => trm
+ | t $ u => put_perm p t $ put_perm p u
+ | Abs (x, ty, t) => Abs (x, ty, put_perm p t)
+ | _ => mk_perm p trm
+
+(* tests whether there is a disagreement between the permutations,
+ and that there is at least one permutation *)
+fun is_bad_list [] = true
+ | is_bad_list [_] = false
+ | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true
+
(* transforms equations into the "p o c == c"-form
from p o (c x1 ...xn) = c (p o x1) ... (p o xn) *)
@@ -119,15 +128,15 @@
val (p, t) = dest_perm lhs
handle TERM _ => error "Equivariance lemma is not of the form p \<bullet> c... = c..."
- val ps = get_ps rhs handle TERM _ => []
+ val ps = get_perms rhs handle TERM _ => []
val (c, c') = (head_of t, head_of rhs)
val msg = "Equivariance lemma is not of the right form "
in
if c <> c'
then error (msg ^ "(constants do not agree).")
- else if is_bad_list (p::ps)
+ else if is_bad_list (p :: ps)
then error (msg ^ "(permutations do not agree).")
- else if not (rhs aconv (put_p p t))
+ else if not (rhs aconv (put_perm p t))
then error (msg ^ "(arguments do not agree).")
else if is_Const t
then safe_mk_equiv thm
@@ -162,7 +171,7 @@
let
val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm))
val (c, c') = (head_of prem, head_of concl)
- val ps = get_ps concl handle TERM _ => []
+ val ps = get_perms concl handle TERM _ => []
val p = try hd ps
val msg = "Equivariance lemma is not of the right form "
in
@@ -170,7 +179,7 @@
then error (msg ^ "(constants do not agree).")
else if is_bad_list ps
then error (msg ^ "(permutations do not agree).")
- else if not (concl aconv (put_p (the p) prem))
+ else if not (concl aconv (put_perm (the p) prem))
then error (msg ^ "(arguments do not agree).")
else
let
@@ -181,7 +190,6 @@
Goal.prove ctxt' [] [] goal'
(fn _ => eqvt_transform_imp_tac ctxt' (the p) p' thm 1)
|> singleton (ProofContext.export ctxt' ctxt)
- |> eqvt_transform_eq ctxt
end
end
@@ -191,7 +199,7 @@
(Const (@{const_name "permute"}, _) $ _ $ _) $ _) =>
eqvt_transform_eq ctxt thm
| @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) =>
- eqvt_transform_imp ctxt thm
+ eqvt_transform_imp ctxt thm |> eqvt_transform_eq ctxt
| _ => raise error "Only _ = _ and _ ==> _ cases are implemented."
@@ -210,7 +218,7 @@
let
val thm' = eqvt_transform (Context.proof_of context) thm
in
- context |> del_thm thm |> del_raw_thm thm'
+ context |> del_thm thm |> del_raw_thm thm'
end)
val eqvt_raw_add = Thm.declaration_attribute add_raw_thm;
--- a/Paper/Paper.thy Mon Apr 26 10:01:13 2010 +0200
+++ b/Paper/Paper.thy Mon Apr 26 20:19:42 2010 +0200
@@ -363,7 +363,7 @@
inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
proofs, we establish a reasoning infrastructure for alpha-equated
terms, including properties about support, freshness and equality
- conditions for alpha-equated terms. We are also able to derive, at the moment
+ conditions for alpha-equated terms. We are also able to derive, for the moment
only manually, strong induction principles that
have the variable convention already built in.
@@ -490,7 +490,7 @@
\end{center}
\noindent
- We also use for sets of atoms the abbreviation
+ We use for sets of atoms the abbreviation
@{thm (lhs) fresh_star_def[no_vars]}, defined as
@{thm (rhs) fresh_star_def[no_vars]}.
A striking consequence of these definitions is that we can prove
@@ -682,7 +682,7 @@
It might be useful to consider some examples for how these definitions of alpha-equivalence
pan out in practice.
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
+ We set @{text R} to be the usual equality @{text "="} and for @{text "fv(T)"} we define
\begin{center}
@{text "fv(x) = {x}"} \hspace{5mm} @{text "fv(T\<^isub>1 \<rightarrow> T\<^isub>2) = fv(T\<^isub>1) \<union> fv(T\<^isub>2)"}
@@ -764,13 +764,14 @@
\noindent
This lemma 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 alpha-equivalence classes of pairs. The elements in these types
- will be, respectively, written as:
+ representing alpha-equivalence classes of pairs of type
+ @{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}.
+ The elements in these types will be, respectively, written as:
\begin{center}
@{term "Abs as x"} \hspace{5mm}
- @{term "Abs_lst as x"} \hspace{5mm}
- @{term "Abs_res as x"}
+ @{term "Abs_res as x"} \hspace{5mm}
+ @{term "Abs_lst as x"}
\end{center}
\noindent
@@ -784,8 +785,8 @@
\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(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_abs(3)[where bs="as", no_vars]}\\
- @{thm (lhs) supp_abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_abs(2)[no_vars]}
+ @{thm (lhs) supp_abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_abs(2)[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}
@@ -851,7 +852,7 @@
\end{center}
\noindent
- using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set
+ using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set,
we further obtain
%
\begin{equation}\label{halftwo}
@@ -897,7 +898,7 @@
binding \mbox{function part} &
$\begin{cases}
\mbox{\begin{tabular}{l}
- \isacommand{with} @{text "bn\<AL>\<^isub>1"} \isacommand{and} \ldots \isacommand{and} @{text "bn\<AL>\<^isub>m"}\\
+ \isacommand{binder} @{text "bn\<AL>\<^isub>1"} \isacommand{and} \ldots \isacommand{and} @{text "bn\<AL>\<^isub>m"}\\
\isacommand{where}\\
$\ldots$\\
\end{tabular}}
@@ -943,8 +944,10 @@
the second is for sets of binders (the order does not matter, but the
cardinality does) and the last is for sets of binders (with vacuous binders
preserving alpha-equivalence). The ``\isacommand{in}-part'' of a binding
- clause will be called \emph{body}; the ``\isacommand{bind}-part'' will
- be called \emph{binder}.
+ clause will be called \emph{bodies} (there can be more than one); the
+ ``\isacommand{bind}-part'' will be called \emph{binders}. A body can only occur
+ in \emph{one} binding clause. A binder, in contrast, may occur in several binding
+ clauses, but cannot occur as a body.
In addition we distinguish between \emph{shallow} and \emph{deep}
binders. Shallow binders are of the form \isacommand{bind}\; {\it labels}\;
@@ -976,22 +979,16 @@
\noindent
Note that in this specification \emph{name} refers to an atom type.
- If we have shallow binders that ``share'' a body, for instance $t$ in
- the following term-constructor
+ Shallow binders may also ``share'' several bodies, for instance @{text t}
+ and @{text s} in the following term-constructor
\begin{center}
\begin{tabular}{ll}
- @{text "Foo x::name y::name t::lam"} &
- \isacommand{bind} @{text x} \isacommand{in} @{text t},\;
- \isacommand{bind} @{text y} \isacommand{in} @{text t}
+ @{text "Foo x::name y::name t::lam s::lam"} &
+ \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}
\end{tabular}
\end{center}
- \noindent
- then we have to make sure the modes of the binders agree. We cannot
- have, for instance, in the first binding clause the mode \isacommand{bind}
- and in the second \isacommand{bind\_set}.
-
A \emph{deep} binder uses an auxiliary binding function that ``picks'' out
the atoms in one argument of the term-constructor, which can be bound in
other arguments and also in the same argument (we will
@@ -1017,7 +1014,7 @@
\hspace{5mm}\phantom{$\mid$}~@{text PNil}\\
\hspace{5mm}$\mid$~@{text "PVar name"}\\
\hspace{5mm}$\mid$~@{text "PTup pat pat"}\\
- \isacommand{with}~@{text "bn::pat \<Rightarrow> atom list"}\\
+ \isacommand{binder}~@{text "bn::pat \<Rightarrow> atom list"}\\
\isacommand{where}~@{text "bn(PNil) = []"}\\
\hspace{5mm}$\mid$~@{text "bn(PVar x) = [atom x]"}\\
\hspace{5mm}$\mid$~@{text "bn(PTup p\<^isub>1 p\<^isub>2) = bn(p\<^isub>1) @ bn(p\<^isub>2)"}\\
@@ -1046,18 +1043,16 @@
\begin{center}
\begin{tabular}{ll}
- @{text "Foo p::pat q::pat t::trm"} &
- \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t},\;
- \isacommand{bind} @{text "bn(q)"} \isacommand{in} @{text t}\\
- @{text "Foo' x::name p::pat t::trm"} &
- \isacommand{bind} @{text x} \isacommand{in} @{text t},\;
- \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}
+ @{text "Foo\<^isub>1 p::pat q::pat t::trm"} &
+ \isacommand{bind} @{text "bn(p) bn(q)"} \isacommand{in} @{text t}\\
+ @{text "Foo\<^isub>2 x::name p::pat t::trm"} &
+ \isacommand{bind} @{text "x bn(p)"} \isacommand{in} @{text t}\\
\end{tabular}
\end{center}
\noindent
- In the first case we might bind all atoms from the pattern @{text p} in @{text t}
- and also all atoms from @{text q} in @{text t}. As a result we have no way
+ In the first case the intention is to bind all atoms from the pattern @{text p} in @{text t}
+ and also all atoms from @{text q} in @{text t}. Unfortunately, we have no way
to determine whether the binder came from the binding function @{text
"bn(p)"} or @{text "bn(q)"}. Similarly in the second case. The reason why
we must exclude such specifications is that they cannot be represent by
@@ -1066,19 +1061,17 @@
\begin{center}
\begin{tabular}{ll}
- @{text "Bar p::pat t::trm s::trm"} &
- \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t},\;
- \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text s}\\
- @{text "Bar' p::pat t::trm"} &
- \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text p},\;
- \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}\\
+ @{text "Bar\<^isub>1 p::pat t::trm s::trm"} &
+ \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "t s"}\\
+ @{text "Bar\<^isub>2 p::pat t::trm"} &
+ \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"}\\
\end{tabular}
\end{center}
\noindent
since there is no overlap of binders.
- Note that in the last example we wrote {\it\isacommand{bind}\;bn(p)\;\isacommand{in}\;p}.
+ Note that in the last example we wrote \isacommand{bind}~@{text "bn(p)"}~\isacommand{in}~@{text "p.."}.
Whenever such a binding clause is present, we will call the corresponding binder \emph{recursive}.
To see the purpose of such recursive binders, compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s
in the following specification:
@@ -1090,13 +1083,12 @@
\hspace{5mm}\phantom{$\mid$}\ldots\\
\hspace{5mm}$\mid$~@{text "Let as::assn t::trm"}
\;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t}\\
- \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}\\
- \hspace{20mm}\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t},
- \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text as}\\
- \isacommand{and} {\it assn} =\\
+ \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}
+ \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\
+ \isacommand{and} @{text "ass"} =\\
\hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\
\hspace{5mm}$\mid$~@{text "ACons name trm assn"}\\
- \isacommand{with} @{text "bn::assn \<Rightarrow> atom list"}\\
+ \isacommand{binder} @{text "bn::assn \<Rightarrow> atom list"}\\
\isacommand{where}~@{text "bn(ANil) = []"}\\
\hspace{5mm}$\mid$~@{text "bn(ACons a t as) = [atom a] @ bn(as)"}\\
\end{tabular}}
@@ -1109,14 +1101,39 @@
function and alpha-equivalence relation, which we are going to describe in the
rest of this section.
+ In order to simplify matters below, we shall assume specifications
+ of term-calculi are \emph{completed}. By this we mean that
+ for every argument of a term-constructor that is \emph{not}
+ already part of a binding clause, we add implicitly a special \emph{empty} binding
+ clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "\<dots>"}. In case
+ of the lambda-calculus, the comletion is as follows:
+
+ \begin{center}
+ \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
+ \isacommand{nominal\_datatype} @{text lam} =\\
+ \hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"}
+ \;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "x"}\\
+ \hspace{5mm}$\mid$~@{text "App t\<^isub>1::lam t\<^isub>2::lam"}
+ \;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>1"},
+ \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>2"}\\
+ \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}
+ \;\;\isacommand{bind}~@{text x} \isacommand{in} @{text t}\\
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ The point of completion is that we can make definitions over the binding
+ clauses, which defined purely over arguments, turned out to be unwieldy.
+
Having dealt with all syntax matters, the problem now is how we can turn
specifications into actual type definitions in Isabelle/HOL and then
establish a reasoning infrastructure for them. As
- Pottier and Cheney pointed out \cite{Pottier06,Cheney5}, we cannot in general
- re-arrange arguments of
+ Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, by just
+ re-arranging the arguments of
term-constructors so that binders and their bodies are next to each other, and
- then use the type constructors @{text "abs_set"}, @{text "abs_res"} and
- @{text "abs_list"} from Section \ref{sec:binders}. Therefore we will first
+ then use directly the type constructors @{text "abs_set"}, @{text "abs_res"} and
+ @{text "abs_list"} from Section \ref{sec:binders}, will result in an inadequate
+ representatation. Therefore we will first
extract datatype definitions from the specification and then define
expicitly an alpha-equivalence relation over them.
@@ -1152,8 +1169,24 @@
\end{equation}
The first non-trivial step we have to perform is the generation free-variable
- functions from the specifications. Given the raw types @{text "ty\<^isub>1 \<dots> ty\<^isub>n"}
- we need to define free-variable functions
+ functions from the specifications. For atomic types we define the auxilary
+ free variable functions:
+
+ \begin{center}
+ \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+ @{text "fv_atom a"} & @{text "="} & @{text "atom a"}\\
+ @{text "fv_atom_set as"} & @{text "="} & @{text "atoms as"}\\
+ @{text "fv_atom_list as"} & @{text "="} & @{text "atoms (set as)"}\\
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ Like the coercion function @{text atom} used earlier, @{text "atoms"} coerces
+ the set of atoms to a set of the generic atom type.
+ It is defined as @{text "atoms as \<equiv> {atom a | a \<in> as}"}.
+
+ Given the raw types @{text "ty\<^isub>1 \<dots> ty\<^isub>n"}
+ we define now free-variable functions
\begin{center}
@{text "fv_ty\<^isub>1, \<dots>, fv_ty\<^isub>n"}
@@ -1173,92 +1206,65 @@
bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function
that calculates those unbound atoms.
- While the idea behind these
- free-variable functions is clear (they just collect all atoms that are not bound),
- because of our rather complicated binding mechanisms their definitions are
- somewhat involved.
- Given a term-constructor @{text "C"} of type @{text ty} with argument types
- \mbox{@{text "ty\<^isub>1 \<dots> ty\<^isub>n"}}, the function
- @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be the union of the values, @{text v},
- calculated below for each argument.
- First we deal with the case that @{text "x\<^isub>i"} is a binder. From the binding clauses,
- we can determine whether the argument is a shallow or deep
- binder, and in the latter case also whether it is a recursive or
- non-recursive binder.
- %
+ While the idea behind these free-variable functions is clear (they just
+ collect all atoms that are not bound), because of our rather complicated
+ binding mechanisms their definitions are somewhat involved. Given a
+ term-constructor @{text "C"} of type @{text ty} and some associated binding
+ clauses, the function @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be
+ the union of the values, @{text v}, calculated below for each binding
+ clause.
+
\begin{equation}\label{deepbinder}
\mbox{%
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
- $\bullet$ & @{term "v = {}"} provided @{text "x\<^isub>i"} is a shallow binder\\
- $\bullet$ & @{text "v = fv_bn x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep
- non-recursive binder with the auxiliary binding function @{text "bn"}\\
- $\bullet$ & @{text "v = fv_ty\<^isub>i x\<^isub>i - bn x\<^isub>i"} provided @{text "x\<^isub>i"} is
- a deep recursive binder with the auxiliary binding function @{text "bn"}
+ \multicolumn{2}{@ {}l}{Empty binding clauses of the form
+ \isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\
+ $\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} is of type @{text "ty"}\smallskip\\
+ \multicolumn{2}{@ {}l}{Shallow binders of the form
+ \isacommand{bind\_set}~@{text "x\<^isub>1\<dots>x\<^isub>n"}~\isacommand{in}~@{text "y\<^isub>1\<dots>y\<^isub>m"}:}\\
+ $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> fv_ty\<^isub>m y\<^isub>m) - (x\<^isub>1 \<union> \<dots> \<union> x\<^isub>n)"}
+ provided the @{text "y\<^isub>i"} are of type @{text "ty\<^isub>i"}\smallskip\\
+ \multicolumn{2}{@ {}l}{Deep binders of the form
+ \isacommand{bind\_set}~@{text "bn x"}~\isacommand{in}~@{text "y\<^isub>1\<dots>y\<^isub>m"}:}\\
+ $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> fv_ty\<^isub>m y\<^isub>m) - (bn x) \<union> (fv_bn x)"}\\
+ $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> fv_ty\<^isub>m y\<^isub>m) - (bn x)"}\\
+ & provided the @{text "y\<^isub>i"} are of type @{text "ty\<^isub>i"}; the first
+ clause applies for @{text x} being a non-recursive deep binder, the
+ second for a recursive deep binder
\end{tabular}}
\end{equation}
\noindent
- The first clause states that shallow binders do not contribute to the
- free variables; in the second clause, we have to collect all
- variables that are left unbound by the binding function @{text "bn"}---this
- is done with function @{text "fv_bn"}; in the third clause, since the
- binder is recursive, we need to bind all variables specified by
- @{text "bn"}---therefore we subtract @{text "bn x\<^isub>i"} from the free
- variables of @{text "x\<^isub>i"}.
+ Similarly for the other binding modes. Note that in a non-recursive deep
+ binder, we have to add all atoms that are left unbound by the binding
+ function @{text "bn"}. For this we use the function @{text "fv_bn"}. Assume
+ for the constructor @{text "C"} the binding function equation is of the form @{text
+ "bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}. We again define a value
+ @{text v} which is exactly as in \eqref{deepbinder} for shallow and deep
+ binders. We only modify the clause for empty binding clauses as follows:
- In case the argument is \emph{not} a binder, we need to consider
- whether the @{text "x\<^isub>i"} is the body of one or more binding clauses.
- In this case we first calculate the set @{text "bnds"} as follows:
- either the corresponding binders are all shallow or there is a single deep binder.
- In the former case we take @{text bnds} to be the union of all shallow
- binders; in the latter case, we just take the set of atoms specified by the
- corresponding binding function. The value for @{text "x\<^isub>i"} is then given by:
- %
- \begin{equation}\label{deepbody}
+
+ \begin{equation}\label{bnemptybinder}
\mbox{%
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
- $\bullet$ & @{text "v = {atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\
- $\bullet$ & @{text "v = (atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\
- $\bullet$ & @{text "v = (atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\
- $\bullet$ & @{text "v = (fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is one of the raw datatypes
- corresponding to the types specified by the user\\
-% $\bullet$ & @{text "(fv\<^isup>\<alpha> x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a defined nominal datatype
-% with a free-variable function @{text "fv\<^isup>\<alpha>"}\\
- $\bullet$ & @{term "v = {}"} otherwise
+ \multicolumn{2}{@ {}l}{Empty binding clauses of the form
+ \isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\
+ $\bullet$ & @{term "v = fv_ty\<^isub>i y"} provided @{text "y"} does not occur in @{text "rhs"}
+ and the free-variable function for the type of @{text "y"} is @{text "fv_ty\<^isub>i"}\\
+ $\bullet$ & @{term "v = fv_bn\<^isub>i y"} provided @{text "y"} occurs in @{text "rhs"}
+ with a recursive call @{text "bn\<^isub>i y"}\\
+ $\bullet$ & @{term "v = {}"} provided @{text "y"} occurs in @{text "rhs"},
+ but without a recursive call\\
\end{tabular}}
\end{equation}
- \noindent
- Like the coercion function @{text atom} used earlier, @{text "atoms"} coerces
- the set of atoms to a set of the generic atom type.
- It is defined as @{text "atoms as \<equiv> {atom a | a \<in> as}"}.
-
- The last case we need to consider is when @{text "x\<^isub>i"} is neither
- a binder nor a body of an abstraction. In this case it is defined
- as in \eqref{deepbody}, except that we do not need to subtract the
- set @{text bnds}.
+ \noindent
+ The reason why we only have to treat the empty binding clauses specially in
+ the definition of @{text "fv_bn"} is that binding functions can only use arguments
+ that do not occur in binding clauses. Otherwise the @{text "bn"} function cannot
+ be lifted to alpha-equated terms.
- The definitions of the free-variable functions for binding
- functions are similar. For each binding function
- @{text "bn\<^isub>j"} we need to define a free-variable function
- @{text "fv_bn\<^isub>j"}. Given a term-constructor @{term "C"}, the
- function @{text "fv_bn\<^isub>j(C x\<^isub>1 \<dots> x\<^isub>n)"} is the union of the
- values calculated for the arguments. For each argument @{term "x\<^isub>i"}
- we know whether it appears in the @{term "rhs"} of the binding
- function equation @{text "bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}. If it does not
- appear in @{text "rhs"} we generate the premise according to the
- rules for @{text "fv_ty"} described above in (\ref{deepbinder}--\ref{deepbody}). Otherwise:
- \begin{center}
- \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
- $\bullet$ & @{text "v = fv_bn x\<^isub>i"} provided @{text "rhs"} contains the
- recursive call @{text "bn x\<^isub>i"}\medskip\\
- $\bullet$ & @{term "v = {}"} provided @{text "rhs"} contains
- @{term "x\<^isub>i"} and @{term "x\<^isub>i"} is of atom type.
- \end{tabular}
- \end{center}
-
- \noindent
To see how these definitions work in practice, let us reconsider the term-constructors
@{text "Let"} and @{text "Let_rec"} from the example shown in \eqref{letrecs}.
For this specification we need to define three free-variable functions, namely
@@ -1266,20 +1272,19 @@
%
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
- @{text "fv\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "fv\<^bsub>bn\<^esub> as \<union> (fv\<^bsub>trm\<^esub> t - set (bn as))"}\\
- @{text "fv\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} &\\
- \multicolumn{3}{r}{@{text "(fv\<^bsub>assn\<^esub> as - set (bn as)) \<union> (fv\<^bsub>trm\<^esub> t - set (bn as))"}}\\[1mm]
+ @{text "fv\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fv\<^bsub>trm\<^esub> t - set (bn as)) \<union> fv\<^bsub>bn\<^esub> as"}\\
+ @{text "fv\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fv\<^bsub>assn\<^esub> as \<union> fv\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm]
- @{text "fv\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{text "[]"}\\
+ @{text "fv\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
@{text "fv\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "{atom a} \<union> (fv\<^bsub>trm\<^esub> t) \<union> (fv\<^bsub>assn\<^esub> as)"}\\[1mm]
- @{text "fv\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{text "[]"}\\
+ @{text "fv\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
@{text "fv\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fv\<^bsub>trm\<^esub> t) \<union> (fv\<^bsub>bn\<^esub> as)"}
\end{tabular}
\end{center}
\noindent
- Since there are no binding clauses for the term-constructors @{text ANil}
+ Since there are only (implicit) empty binding clauses for the term-constructors @{text ANil}
and @{text "ACons"}, the corresponding free-variable function @{text
"fv\<^bsub>assn\<^esub>"} returns all atoms occuring in an assignment. The
binding only takes place in @{text Let} and @{text "Let_rec"}. In the @{text
@@ -1290,12 +1295,15 @@
"fv\<^bsub>bn\<^esub>"} is. In contrast, in @{text "Let_rec"} we have a
recursive binder where we want to also bind all occurrences of the atoms
in @{text "set (bn as)"} inside @{text "as"}. Therefore we have to subtract @{text
- "set (bn as)"} from @{text "fv\<^bsub>assn\<^esub> as"}, as well as from
- @{text "fv\<^bsub>trm\<^esub> t"}. An interesting point in this example is
+ "set (bn as)"} from @{text "fv\<^bsub>trm\<^esub> t"}, as well as from
+ @{text "fv\<^bsub>assn\<^esub> as"}. An interesting point in this example is
that an assignment ``alone'' does not have any bound variables. Only in the
context of a @{text Let} or @{text "Let_rec"} will some atoms become bound.
This is a phenomenon
- that has also been pointed out in \cite{ott-jfp}. We can also see that
+ that has also been pointed out in \cite{ott-jfp}. For us it is crucial, because
+ we would not be able to lift a @{text "bn"}-function that is defined over
+ arguments that are either binders or bodies. In that case @{text "bn"} would
+ not respect alpha-equivalence. We can also see that
%
\begin{equation}\label{bnprop}
@{text "fv_ty x = bn x \<union> fv_bn x"}.
@@ -1307,7 +1315,7 @@
Next we define alpha-equivalence relations for the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}. We call them
@{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}. Like with the free-variable functions,
we also need to define auxiliary alpha-equivalence relations for the binding functions.
- Say we have @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, then we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}.
+ Say we have binding functions @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, then we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}.
To simplify our definitions we will use the following abbreviations for
relations and free-variable acting on products.
%
@@ -1327,12 +1335,9 @@
\end{center}
\noindent
- For what follows, let us assume
- @{text C} is of type @{text ty} and its arguments are given by @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}.
- The task is to specify what the premises of these clauses are. For this we
- consider the pairs \mbox{@{text "(x\<^isub>i, y\<^isub>i)"}}, but instead of considering them in turn, it will
- be easier to analyse these pairs according to ``clusters'' of the binding clauses.
- Therefore we distinguish the following cases:
+ For what follows, let us assume @{text C} is of type @{text ty}. The task
+ is to specify what the premises of these clauses are. Again for this we
+ analyse the binding clauses and produce a corresponding premise.
*}
(*<*)
consts alpha_ty ::'a
@@ -1348,59 +1353,42 @@
fv_trm2 ("fv\<^bsub>assn\<^esub> \<oplus> fv\<^bsub>trm\<^esub>")
(*>*)
text {*
- \begin{itemize}
- \item The @{text "(x\<^isub>i, y\<^isub>i)"} is a body of shallow binder with type @{text "ty"}. We assume the
- \mbox{@{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"}} are the corresponding binders. For the binding mode
- \isacommand{bind\_set} we generate the premise
+ \begin{equation}\label{alpha}
+ \mbox{%
+ \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
+ \multicolumn{2}{@ {}l}{Empty binding clauses of the form
+ \isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "x\<^isub>i"}:}\\
+ $\bullet$ & @{text "x\<^isub>i \<approx>ty y\<^isub>i"} provided @{text "x\<^isub>i"} and @{text "y\<^isub>i"}
+ are recursive arguments of @{text "C"}\\
+ $\bullet$ & @{term "x\<^isub>i = y\<^isub>i"} provided @{text "x\<^isub>i"} and @{text "y\<^isub>i"} are
+ non-recursive arguments\smallskip\\
+ \multicolumn{2}{@ {}l}{Shallow binders of the form
+ \isacommand{bind\_set}~@{text "x\<^isub>1\<dots>x\<^isub>n"}~\isacommand{in}~@{text "x'\<^isub>1\<dots>x'\<^isub>m"}:}\\
+ $\bullet$ & Assume the bodies @{text "x'\<^isub>1\<dots>x'\<^isub>m"} are of type @{text "ty\<^isub>1\<dots>ty\<^isub>m"},
+ @{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is
+ @{text "fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}, then
\begin{center}
- @{term "\<exists>p. (u\<^isub>1 \<union> \<xi> \<union> u\<^isub>m, x\<^isub>i) \<approx>gen alpha_ty fv_ty p (v\<^isub>1 \<union> \<xi> \<union> v\<^isub>m, y\<^isub>i)"}
- \end{center}
-
- For the binding mode \isacommand{bind}, we use $\approx_{\textit{list}}$, and for
- binding mode \isacommand{bind\_res} we use $\approx_{\textit{res}}$ instead.
-
- \item The @{text "(x\<^isub>i, y\<^isub>i)"} is a deep non-recursive binder with type @{text "ty"}
- and @{text bn} is corresponding the binding function. We assume
- @{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"} are the corresponding bodies with types @{text "ty\<^isub>1,\<dots>, ty\<^isub>m"}.
- For the binding mode \isacommand{bind\_set} we generate two premises
- %
+ @{term "\<exists>p. (x\<^isub>1 \<union> \<xi> \<union> x\<^isub>n, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fv p (y\<^isub>1 \<union> \<xi> \<union> y\<^isub>n, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}
+ \end{center}\\
+ \multicolumn{2}{@ {}l}{Deep binders of the form
+ \isacommand{bind\_set}~@{text "bn x"}~\isacommand{in}~@{text "x'\<^isub>1\<dots>x'\<^isub>m"}:}\\
+ $\bullet$ & Assume the bodies @{text "x'\<^isub>1\<dots>x'\<^isub>m"} are of type @{text "ty\<^isub>1\<dots>ty\<^isub>m"},
+ @{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is
+ @{text "fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}, then for recursive deep binders
\begin{center}
- @{text "x\<^isub>i \<approx>bn y\<^isub>i"}\hfill
- @{term "\<exists>p. (bn x\<^isub>i, (u\<^isub>1,\<xi>,u\<^isub>m)) \<approx>gen R fv p (bn y\<^isub>i, (v\<^isub>1,\<xi>,v\<^isub>m))"}
- \end{center}
+ @{term "\<exists>p. (bn x, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fv p (bn y, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}
+ \end{center}\\
+ $\bullet$ & for non-recursive binders we generate in addition @{text "x \<approx>bn y"}\\
+ \end{tabular}}
+ \end{equation}
\noindent
- where @{text R} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is
- @{text "fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}. Similarly for the other binding modes.
-
- \item The @{text "(x\<^isub>i, y\<^isub>i)"} is a deep recursive binders with type @{text "ty"}
- and @{text bn} is the corresponding binding function. We assume
- @{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"} are the corresponding bodies with types @{text "ty\<^isub>1,\<dots>, ty\<^isub>m"}.
- For the binding mode \isacommand{bind\_set} we generate the premise
- %
- \begin{center}
- @{term "\<exists>p. (bn x\<^isub>i, (x\<^isub>i, u\<^isub>1,\<xi>,u\<^isub>m)) \<approx>gen R fv p (bn y\<^isub>i, (y\<^isub>i, v\<^isub>1,\<xi>,v\<^isub>m))"}
- \end{center}
-
- \noindent
- where @{text R} is @{text "\<approx>ty \<otimes> \<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is
- @{text "fv_ty \<oplus> fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}. Similarly for the other modes.
- \end{itemize}
-
- \noindent
- From this definition it is clear why we can only support one binding mode per binder
- and body, as we cannot mix the relations $\approx_{\textit{set}}$, $\approx_{\textit{list}}$
- and $\approx_{\textit{res}}$. It is also clear why we have to impose the restriction
- of excluding overlapping binders, as these would need to be translated into separate
+ Similarly for the other binding modes.
+ From this definition it is clear why we have to impose the restriction
+ of excluding overlapping deep binders, as these would need to be translated into separate
abstractions.
- The only cases that are not covered by the rules above are the cases where @{text "(x\<^isub>i, y\<^isub>i)"} is
- neither a binder nor a body in a binding clause. Then we just generate @{text "x\<^isub>i \<approx>ty y\<^isub>i"} provided
- the type of @{text "x\<^isub>i"} and @{text "y\<^isub>i"} is @{text ty} and the arguments are
- recursive arguments of the term-constructor. If they are non-recursive arguments,
- then we generate the premise @{text "x\<^isub>i = y\<^isub>i"}.
-
The alpha-equivalence relations @{text "\<approx>bn\<^isub>j"} for binding functions
are similar. We again have conclusions of the form \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>bn C y\<^isub>1 \<dots> y\<^isub>n"}}