# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1270054022 -7200
# Node ID 8f9e2b02470a7241707ff7dde6162a41f49d4ea5
# Parent  6988077666dc20c4c84741e9795e4a02092368a1
added alpha-definition for ~~ty

diff -r 6988077666dc -r 8f9e2b02470a Paper/Paper.thy
--- 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
diff -r 6988077666dc -r 8f9e2b02470a Paper/document/root.tex
--- a/Paper/document/root.tex	Wed Mar 31 17:04:09 2010 +0200
+++ b/Paper/document/root.tex	Wed Mar 31 18:47:02 2010 +0200
@@ -23,6 +23,7 @@
 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
 \renewcommand{\isasymequiv}{$\dn$}
 %%\renewcommand{\isasymiota}{}
+\renewcommand{\isasymxi}{$\ldots$}
 \renewcommand{\isasymemptyset}{$\varnothing$}
 \newcommand{\isasymnotapprox}{$\not\approx$}
 \newcommand{\isasymLET}{$\mathtt{let}$}