--- a/Quotient-Paper/Paper.thy	Wed May 26 17:55:42 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Thu May 27 11:21:37 2010 +0200
@@ -1,3 +1,4 @@
+
 (*<*)
 theory Paper
 imports "Quotient"
@@ -157,6 +158,26 @@
 
 *}
 
+subsection {* Higher Order Logic *}
+
+text {*
+
+  Types:
+  \begin{eqnarray}\nonumber
+  @{text "\<sigma> ::="} & @{text "\<alpha>"} & \textrm{(type variable)} \\ \nonumber
+      @{text "|"} & @{text "(\<sigma>,\<dots>,\<sigma>)\<kappa>"} & \textrm{(type construction)}
+  \end{eqnarray}
+
+  Terms:
+  \begin{eqnarray}\nonumber
+  @{text "t ::="} & @{text "x\<^isup>\<sigma>"} & \textrm{(variable)} \\ \nonumber
+      @{text "|"} & @{text "c\<^isup>\<sigma>"} & \textrm{(constant)} \\ \nonumber
+      @{text "|"} & @{text "t t"} & \textrm{(application)} \\ \nonumber
+      @{text "|"} & @{text "\<lambda>x\<^isup>\<sigma>. t"} & \textrm{(abstraction)} \\ \nonumber
+  \end{eqnarray}
+
+*}
+
 section {* Constants *}
 
 (* Say more about containers? *)
@@ -173,31 +194,26 @@
 
   The operation is additionally able to descend into types for which
   maps are known. Such maps for most common types (list, pair, sum,
-  option, \ldots) are described in Homeier, and our algorithm uses the
-  same kind of maps. Given the raw compound type and the quotient compound
-  type the Rep/Abs algorithm does:
+  option, \ldots) are described in Homeier, and we assume that @{text "map"}
+  is the function that returns a map for a given type. Then REP/ABS is defined
+  as follows:
 
   \begin{itemize}
-  \item For equal types or free type variables return identity.
-
-  \item For function types recurse, change the Rep/Abs flag to
-     the opposite one for the domain type and compose the
-     results with @{term "fun_map"}.
-
-  \item For equal type constructors use the appropriate map function
-     applied to the results for the arguments.
-
-  \item For unequal type constructors, look in the quotients information
-    for a quotient type that matches the type constructor, and instantiate
-    the raw type
-    appropriately getting back an instantiation environment. We apply
-    the environment to the arguments and recurse composing it with the
-    aggregate map function.
+  \item @{text "ABS(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "id"}
+  \item @{text "REP(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"}  =  @{text "id"}
+  \item @{text "ABS(\<sigma>, \<sigma>)"}  =  @{text "id"}
+  \item @{text "REP(\<sigma>, \<sigma>)"}  =  @{text "id"}
+  \item @{text "ABS(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"}  =  @{text "REP(\<sigma>\<^isub>1,\<tau>\<^isub>1) ---> ABS(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}
+  \item @{text "REP(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"}  =  @{text "ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1) ---> REP(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}
+  \item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"}  =  @{text "(map \<kappa>) (ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (ABS(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
+  \item @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"}  =  @{text "(map \<kappa>) (REP(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REP(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
+  \item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"}  =  @{text "Abs_\<kappa>\<^isub>2 \<circ> (map \<kappa>\<^isub>1) (ABS(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (ABS(\<rho>\<^isub>p,\<nu>\<^isub>p)"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}
+  \item @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"}  =  @{text "(map \<kappa>\<^isub>1) (REP(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REP(\<rho>\<^isub>p,\<nu>\<^isub>p) \<circ> Rep_\<kappa>\<^isub>2"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}
   \end{itemize}
 
-  The first three points above are identical to the algorithm present in
-  in Homeier's HOL implementation, below is the definition of @{term fconcat}
-  that shows the last step:
+  Apart from the last 2 points the definition is same as the one implemented in
+  in Homeier's HOL package, below is the definition of @{term fconcat}
+  that shows the last points:
 
   @{thm fconcat_def[no_vars]}