--- a/Paper/Paper.thy Wed Mar 31 17:04:09 2010 +0200
+++ b/Paper/Paper.thy Wed Mar 31 18:47:02 2010 +0200
@@ -1244,9 +1244,10 @@
$\bullet$ & @{term "{}"} provided @{term "x\<^isub>i"} is a single atom,
atom list or atom set\\
$\bullet$ & @{text "fv_bn x\<^isub>i"} in case @{text "rhs"} contains the
- recursive call @{text "bn x\<^isub>i"}\\[1mm]
+ recursive call @{text "bn x\<^isub>i"}\medskip\\
%
- \multicolumn{2}{l}{@{text "x\<^isub>i"} does not occur in @{text "rhs"}:}\\
+ \multicolumn{2}{l}{@{text "x\<^isub>i"} does not occur in @{text "rhs"}:}\\
+ $\bullet$ & @{text "atom x\<^isub>i"} provided @{term "x\<^isub>i"} is an atom\\
$\bullet$ & @{text "atoms x\<^isub>i"} provided @{term "x\<^isub>i"} is a set of atoms\\
$\bullet$ & @{term "atoms (set x\<^isub>i)"} provided @{term "x\<^isub>i"} is a list of atoms\\
$\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i"} provided @{term "ty\<^isub>i"} is one of the raw
@@ -1310,68 +1311,70 @@
%
\begin{center}
\begin{tabular}{rcl}
- @{text "(x\<^isub>1, y\<^isub>1) R\<^isub>1 \<otimes> R\<^isub>2 (x\<^isub>2, y\<^isub>2)"} & @{text "\<equiv>"} & @{text "x\<^isub>1 R\<^isub>1 y\<^isub>1 \<and> x\<^isub>2 R\<^isub>2 y\<^isub>2"}\\
- @{text "fv\<^isub>1 \<oplus> fv\<^isub>2 (x, y)"} & @{text "\<equiv>"} & @{text "fv\<^isub>1 x \<union> fv\<^isub>2 y"}\\
+ @{text "(x\<^isub>1, y\<^isub>1) (R\<^isub>1 \<otimes> R\<^isub>2) (x\<^isub>2, y\<^isub>2)"} & @{text "\<equiv>"} & @{text "x\<^isub>1 R\<^isub>1 y\<^isub>1 \<and> x\<^isub>2 R\<^isub>2 y\<^isub>2"}\\
+ @{text "(fv\<^isub>1 \<oplus> fv\<^isub>2) (x, y)"} & @{text "\<equiv>"} & @{text "fv\<^isub>1 x \<union> fv\<^isub>2 y"}\\
\end{tabular}
\end{center}
- The relations are inductively defined predicates, whose clauses have
+ The relations for alpha-equivalence are inductively defined predicates, whose clauses have
conclusions of the form @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"} (let us assume
- @{text C} is of type @{text ty} and its arguments are specified as @{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 @{text "(x\<^isub>i, y\<^isub>i)"} which necesarily must have the same type, say
- @{text "ty\<^isub>i"}. For each of these pairs we calculate a premise as follows.
-
+ @{text C} is of type @{text ty} and its arguments are given by @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}).
+ The task now is to specify what the premises of these clauses are. For this we
+ consider the pairs @{text "(x\<^isub>i, y\<^isub>i)"}. We will analyse these pairs according to
+ ``clusters'' of the binding clauses. There are the following cases:
+*}
+(*<*)
+consts alpha_ty ::'a
+notation alpha_ty ("\<approx>ty")
+(*>*)
+text {*
+ \begin{itemize}
+ \item The @{text "(x\<^isub>i, y\<^isub>i)"} are bodies of shallow binders with type @{text "ty"}. We assume the
+ @{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{center}
- \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
- \multicolumn{2}{l}{@{text "x\<^isub>i"} is a binder:}\\
- $\bullet$ & none provided @{text "x\<^isub>i"} is a shallow binder\\
- $\bullet$ & @{text "x\<^isub>i \<approx>bn y\<^isub>i"} provided @{text "x\<^isub>i"} is a deep
- non-recursive binder with the auxiliary binding function @{text bn}\\
- $\bullet$ & @{text "True"} provided @{text "x\<^isub>i"} is a deep
- recursive binder\\
- \end{tabular}
+ @{term "\<exists>p. (u\<^isub>1 \<union> \<xi> \<union> u\<^isub>m, x\<^isub>i) \<approx>gen alpha_ty fv_ty\<^isub>i p (v\<^isub>1 \<union> \<xi> \<union> v\<^isub>m, y\<^isub>i)"}
\end{center}
- TODO BELOW
+ Similarly for the other modes.
+
+ \item The @{text "(x\<^isub>i, y\<^isub>i)"} are deep non-recursive binders with type @{text "ty"}
+ and with @{text bn} being the auxiliary 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 two premises
\begin{center}
- \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
- \multicolumn{2}{l}{@{text "x\<^isub>i"} is a body where the binding clause has mode \isacommand{bind}:}\\
- $\bullet$ & @{text "\<exists>p. (bnds_x\<^isub>i, x\<^isub>i) \<approx>lst (\<approx>ty\<^isub>i) fv_ty\<^isub>i p (bnds_y\<^isub>i, y\<^isub>j)"}
- provided @{text "x\<^isub>i"} has only shallow binders; in this case @{text "bnds_x\<^isub>i"} is the
- union of all these shallow binders (similarly for @{text "bnds_y\<^isub>i"}\\
- $\bullet$ & @{text "\<exists>p. (bn_ty\<^isub>j x\<^isub>j, x\<^isub>i) \<approx>lst (\<approx>ty\<^isub>i) fv_ty\<^isub>i p (bn_ty y\<^isub>j, y\<^isub>i)"}
- provided @{text "x\<^isub>i"} is a body with a deep non-recursive binder @{text x\<^isub>j}
- (similarly @{text "y\<^isub>j"} is the deep non-recursive binder for @{text "y\<^isub>i"})\\
- $\bullet$ & @{text "\<exists>p (bn_ty\<^isub>i x\<^isub>i, (x\<^isub>j, x\<^isub>n)) \<approx>lst R fvs \<pi> (bn\<^isub>m y\<^isub>j, (y\<^isub>j, y\<^isub>n))"}
- provided @{text "x\<^isub>j"} is a deep recursive binder with the auxiliary binding
- function @{text "bn\<^isub>m"} and permutation @{text "\<pi>"}, @{term "fvs"} is a compound
- free variable function returning the union of appropriate @{term "fv_ty\<^isub>x"} and
- @{term "R"} is the composition of equivalence relations @{text "\<approx>"} and @{text "\<approx>\<^isub>n"}\\
- $\bullet$ & @{text "x\<^isub>j"} has a deep recursive binding\\
- $\bullet$ & @{text "({x\<^isub>n}, x\<^isub>j) \<approx>gen R fv_ty \<pi> ({y\<^isub>n}, y\<^isub>j)"} provided @{text "x\<^isub>j"} has
- a shallow binder @{text "x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the
- alpha-equivalence for @{term "x\<^isub>j"}
- and @{term "fv_ty"} is the free-variable function for @{term "x\<^isub>j"}\\
- $\bullet$ & @{text "(bn\<^isub>m x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (bn\<^isub>m y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>j"}
- has a deep non-recursive binder @{text "bn\<^isub>m x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the
- alpha-equivalence for @{term "x\<^isub>j"}
- and @{term "fv_ty"} is the free-variable function for @{term "x\<^isub>j"}\\
- $\bullet$ & @{text "x\<^isub>j \<approx>\<^isub>j y\<^isub>j"} provided @{term "x\<^isub>j"} is one of the types being
- defined\\
- $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} otherwise\\
- \end{tabular}
+ @{text "x\<^isub>i \<approx>bn y\<^isub>i"}\\
+ @{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}
- , of a type @{text ty}, two instances
- of this constructor are alpha-equivalent @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx> C y\<^isub>1 \<dots> y\<^isub>n"} if there
- exist permutations @{text "\<pi>\<^isub>1 \<dots> \<pi>\<^isub>p"} (one for each bound argument) such that
- the conjunction of equivalences defined below for each argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} holds.
- For an argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} this holds if:
+ \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 modes.
+
+ \item The @{text "(x\<^isub>i, y\<^isub>i)"} are deep recursive binders with type @{text "ty"}
+ and with @{text bn} being the auxiliary 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
+ The only cases that are not covered by these rules is if @{text "(x\<^isub>i, y\<^isub>i)"} is
+ neither a binder nor a body. 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 @{text "x\<^isub>i = y\<^isub>i"}.
+
+ TODO
The alpha-equivalence relations for binding functions are similar to the alpha-equivalences
for their respective types, the difference is that they ommit checking the arguments that