--- a/Nominal/FSet.thy	Sun Jun 13 14:39:55 2010 +0200
+++ b/Nominal/FSet.thy	Sun Jun 13 17:01:15 2010 +0200
@@ -1417,4 +1417,223 @@
 no_notation
   list_eq (infix "\<approx>" 50)
 
+ML {*
+open Quotient_Info;
+
+exception LIFT_MATCH of string
+
+
+
+(*** Aggregate Rep/Abs Function ***)
+
+
+(* The flag RepF is for types in negative position; AbsF is for types
+   in positive position. Because of this, function types need to be
+   treated specially, since there the polarity changes.
+*)
+
+datatype flag = AbsF | RepF
+
+fun negF AbsF = RepF
+  | negF RepF = AbsF
+
+fun is_identity (Const (@{const_name "id"}, _)) = true
+  | is_identity _ = false
+
+fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
+
+fun mk_fun_compose flag (trm1, trm2) =
+  case flag of
+    AbsF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
+  | RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1
+
+fun get_mapfun ctxt s =
+let
+  val thy = ProofContext.theory_of ctxt
+  val exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
+  val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
+in
+  Const (mapfun, dummyT)
 end
+
+(* makes a Free out of a TVar *)
+fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
+
+(* produces an aggregate map function for the
+   rty-part of a quotient definition; abstracts
+   over all variables listed in vs (these variables
+   correspond to the type variables in rty)
+
+   for example for: (?'a list * ?'b)
+   it produces:     %a b. prod_map (map a) b
+*)
+fun mk_mapfun ctxt vs rty =
+let
+  val vs' = map (mk_Free) vs
+
+  fun mk_mapfun_aux rty =
+    case rty of
+      TVar _ => mk_Free rty
+    | Type (_, []) => mk_identity rty
+    | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
+    | _ => raise LIFT_MATCH "mk_mapfun (default)"
+in
+  fold_rev Term.lambda vs' (mk_mapfun_aux rty)
+end
+
+(* looks up the (varified) rty and qty for
+   a quotient definition
+*)
+fun get_rty_qty ctxt s =
+let
+  val thy = ProofContext.theory_of ctxt
+  val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
+  val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
+in
+  (#rtyp qdata, #qtyp qdata)
+end
+
+(* takes two type-environments and looks
+   up in both of them the variable v, which
+   must be listed in the environment
+*)
+fun double_lookup rtyenv qtyenv v =
+let
+  val v' = fst (dest_TVar v)
+in
+  (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
+end
+
+(* matches a type pattern with a type *)
+fun match ctxt err ty_pat ty =
+let
+  val thy = ProofContext.theory_of ctxt
+in
+  Sign.typ_match thy (ty_pat, ty) Vartab.empty
+  handle MATCH_TYPE => err ctxt ty_pat ty
+end
+
+(* produces the rep or abs constant for a qty *)
+fun absrep_const flag ctxt qty_str =
+let
+  val qty_name = Long_Name.base_name qty_str
+  val qualifier = Long_Name.qualifier qty_str
+in
+  case flag of
+    AbsF => Const (Long_Name.qualify qualifier ("abs_" ^ qty_name), dummyT)
+  | RepF => Const (Long_Name.qualify qualifier ("rep_" ^ qty_name), dummyT)
+end
+
+(* Lets Nitpick represent elements of quotient types as elements of the raw type *)
+fun absrep_const_chk flag ctxt qty_str =
+  Syntax.check_term ctxt (absrep_const flag ctxt qty_str)
+
+fun absrep_match_err ctxt ty_pat ty =
+let
+  val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
+  val ty_str = Syntax.string_of_typ ctxt ty
+in
+  raise LIFT_MATCH (space_implode " "
+    ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
+end
+
+
+(** generation of an aggregate absrep function **)
+
+(* - In case of equal types we just return the identity.
+
+   - In case of TFrees we also return the identity.
+
+   - In case of function types we recurse taking
+     the polarity change into account.
+
+   - If the type constructors are equal, we recurse for the
+     arguments and build the appropriate map function.
+
+   - If the type constructors are unequal, there must be an
+     instance of quotient types:
+
+       - we first look up the corresponding rty_pat and qty_pat
+         from the quotient definition; the arguments of qty_pat
+         must be some distinct TVars
+       - we then match the rty_pat with rty and qty_pat with qty;
+         if matching fails the types do not correspond -> error
+       - the matching produces two environments; we look up the
+         assignments for the qty_pat variables and recurse on the
+         assignments
+       - we prefix the aggregate map function for the rty_pat,
+         which is an abstraction over all type variables
+       - finally we compose the result with the appropriate
+         absrep function in case at least one argument produced
+         a non-identity function /
+         otherwise we just return the appropriate absrep
+         function
+
+     The composition is necessary for types like
+
+        ('a list) list / ('a foo) foo
+
+     The matching is necessary for types like
+
+        ('a * 'a) list / 'a bar
+
+     The test is necessary in order to eliminate superfluous
+     identity maps.
+*)
+
+fun absrep_fun flag ctxt (rty, qty) =
+  if rty = qty
+  then mk_identity rty
+  else
+    case (rty, qty) of
+      (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
+        let
+          val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1')
+          val arg2 = absrep_fun flag ctxt (ty2, ty2')
+        in
+          list_comb (get_mapfun ctxt "fun", [arg1, arg2])
+        end
+    | (Type (s, tys), Type (s', tys')) =>
+        if s = s'
+        then
+           let
+             val args = map (absrep_fun flag ctxt) (tys ~~ tys')
+           in
+             list_comb (get_mapfun ctxt s, args)
+           end
+        else
+           let
+             val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
+             val rtyenv = match ctxt absrep_match_err rty_pat rty
+             val qtyenv = match ctxt absrep_match_err qty_pat qty
+             val args_aux = map (double_lookup rtyenv qtyenv) vs
+             val args = map (absrep_fun flag ctxt) args_aux
+             val map_fun = mk_mapfun ctxt vs rty_pat
+             val result = list_comb (map_fun, args)
+           in
+             (*if forall is_identity args
+             then absrep_const flag ctxt s'
+             else*) mk_fun_compose flag (absrep_const flag ctxt s', result)
+           end
+    | (TFree x, TFree x') =>
+        if x = x'
+        then mk_identity rty
+        else raise (LIFT_MATCH "absrep_fun (frees)")
+    | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
+    | _ => raise (LIFT_MATCH "absrep_fun (default)")
+
+
+*}
+
+ML {*
+  absrep_fun AbsF @{context} (@{typ "('a list) list \<Rightarrow> 'a list"}, @{typ "('a fset) fset \<Rightarrow> 'a fset"})
+  |> Syntax.string_of_term @{context}
+  |> writeln
+*}
+
+lemma "(\<lambda> (c::'s \<Rightarrow> bool). \<exists>(x::'s). c = rel x) = {c. \<exists>x. c = rel x}"
+apply(auto simp add: mem_def)
+done
+
+
+end

--- a/Quotient-Paper/Paper.thy	Sun Jun 13 14:39:55 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Sun Jun 13 17:01:15 2010 +0200
@@ -114,7 +114,7 @@
   The purpose of a \emph{quotient package} is to ease the lifting of theorems
   and automate the definitions and reasoning as much as possible. In the
   context of HOL, there have been a few quotient packages already
-  \cite{harrison-thesis,Slotosch97}. The most notable is the one by Homeier
+  \cite{harrison-thesis,Slotosch97}. The most notable one is by Homeier
   \cite{Homeier05} implemented in HOL4.  The fundamental construction these
   quotient packages perform can be illustrated by the following picture:
 
@@ -144,19 +144,19 @@
   \end{center}
 
   \noindent
-  The starting point is an existing type, often referred to as the
-  \emph{raw level}, over which an equivalence relation given by the user is
+  The starting point is an existing type, often referred to as the \emph{raw
+  type}, over which an equivalence relation given by the user is
   defined. With this input the package introduces a new type, to which we
-  refer as the \emph{quotient level}. This type comes with an
+  refer as the \emph{quotient type}. This type comes with an
   \emph{abstraction} and a \emph{representation} function, written @{text Abs}
-  and @{text Rep}. These functions relate elements in the existing type to
-  ones in the new type and vice versa; they can be uniquely identified by
-  their type. For example for the integer quotient construction the types of
-  @{text Abs} and @{text Rep} are
-
+  and @{text Rep}.\footnote{Actually they need to be derived from slightly
+  more basic functions. We will show the details later. } These functions
+  relate elements in the existing type to ones in the new type and vice versa;
+  they can be uniquely identified by their type. For example for the integer
+  quotient construction the types of @{text Abs} and @{text Rep} are
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  @{text "Abs::nat \<times> nat \<Rightarrow> int"}\hspace{10mm}@{text "Rep::int \<Rightarrow> nat \<times> nat"}
+  @{text "Abs :: nat \<times> nat \<Rightarrow> int"}\hspace{10mm}@{text "Rep :: int \<Rightarrow> nat \<times> nat"}
   \end{isabelle}
 
   \noindent
@@ -192,7 +192,7 @@
 
   \noindent
   We expect that the corresponding operator on finite sets, written @{term "fconcat"},
-  behaves as follows:
+  builds the union of finite sets of finite sets:
 
   @{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]}
 
@@ -205,7 +205,7 @@
   the abstraction of the result is \emph{not} enough. The reason is that case in case
   of @{text "\<Union>"} we obtain the incorrect definition
 
-  @{text [display, indent=10] "\<Union> S \<equiv> Abs (flat (Rep S))"}
+  @{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat (Rep_fset S))"}
 
   \noindent
   where the right-hand side is not even typable! This problem can be remedied in the
@@ -216,7 +216,7 @@
   representation and abstraction functions, which in case of @{text "\<Union>"}
   generate the following definition
 
-  @{text [display, indent=10] "\<Union> S \<equiv> Abs (flat ((map Rep \<circ> Rep) S))"}
+  @{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat ((map Rep_fset \<circ> Rep_fset) S))"}
 
   \noindent
   where @{term map} is the usual mapping function for lists. In this paper we
@@ -294,13 +294,52 @@
       @{text "|"} & @{text "\<lambda>x\<^isup>\<sigma>. t"} & \textrm{(abstraction)} \\ \nonumber
   \end{eqnarray}
 
+  {\it Say more about containers / maping functions }
+
 *}
 
 section {* Quotient Types and Lifting of Definitions *}
 
-(* Say more about containers? *)
+text {*
+  The first step in a quotient constructions is to take a name for the new
+  type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation defined over a
+  raw type, say @{text "\<sigma>"}. The equivalence relation for the quotient
+  construction, lets say @{text "R"}, must then be of type @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow>
+  bool"}. Given this data, we can automatically declare the quotient type as
+
+  
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \isacommand{typedef}~~@{text "\<alpha>s \<kappa>\<^isub>q = {c. \<exists>x. c = R x}"}
+  \end{isabelle}
+
+  \noindent
+  being the set of equivalence classes of @{text "R"}. The restriction in this declaration
+  is that the type variables in the raw type @{text "\<sigma>"} must be included in the 
+  type variables @{text "\<alpha>s"} declared for @{text "\<kappa>\<^isub>q"}. HOL will provide us 
+  with abstraction and representation functions having the type
 
-text {*
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{text "abs_\<kappa>\<^isub>q :: \<sigma> set \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"}\hspace{10mm}@{text "rep_\<kappa>\<^isub>q :: \<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma> set"}
+  \end{isabelle}
+
+  \noindent
+  relating the new quotient type and raw type. However, as Homeier noted, it is easier 
+  to work with the following derived definitions
+  
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{text "Abs_\<kappa>\<^isub>q x \<equiv> abs_\<kappa>\<^isub>q (R x)"}\hspace{10mm}@{text "Rep_\<kappa>\<^isub>q x \<equiv> \<epsilon> (rep_\<kappa>\<^isub>q x)"}
+  \end{isabelle}
+  
+  \noindent
+  on the expense of having to use Hilbert's choice operator @{text "\<epsilon>"}. With these
+  definitions the abstraction and representation functions relate directly the 
+  quotient and raw types (their type is  @{text "\<sigma> \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"} and @{text "\<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma>"}, 
+  respectively). We can show that the property
+
+  @{text [display, indent=10] "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}
+
+  \noindent
+  holds (for the proof see \cite{Homeier05}).
 
   To define a constant on the lifted type, an aggregate abstraction
   function is applied to the raw constant. Below we describe the operation
@@ -317,17 +356,9 @@
   as follows:
 
   {\it the first argument is the raw type and the second argument the quotient type}
-
-
+  %
   \begin{center}
-  \begin{tabular}{rcl}
-
-  % type variable case says that variables must be equal...therefore subsumed by the equal case below
-  %
-  %\multicolumn{3}{@ {\hspace{-4mm}}l}{type variables:}\\ 
-  %@{text "ABS (\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} & $\dn$ & @{text "id"}\\
-  %@{text "REP (\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} & $\dn$ & @{text "id"}\smallskip\\
-
+  \begin{longtable}{rcl}
   \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\ 
   @{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\\
   @{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\smallskip\\
@@ -338,19 +369,19 @@
   @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (ABS (\<sigma>s, \<tau>s))"}\\
   @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (REP (\<sigma>s, \<tau>s))"}\smallskip\\
   \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\\
-  @{text "ABS (\<sigma>s \<kappa>\<^isub>1, \<tau>s \<kappa>\<^isub>2)"} & $\dn$ & @{text "Abs_\<kappa>\<^isub>2 \<circ> (MAP(\<rho>s \<kappa>\<^isub>1) (ABS (\<sigma>s', \<tau>s')))"}\\
-  @{text "REP (\<sigma>s \<kappa>\<^isub>1, \<tau>s \<kappa>\<^isub>2)"} & $\dn$ & @{text "(MAP(\<rho>s \<kappa>\<^isub>1) (REP (\<sigma>s', \<tau>s'))) \<circ> Rep_\<kappa>\<^isub>2"}\\
-  \end{tabular}
+  @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "Abs_\<kappa>\<^isub>q \<circ> (MAP(\<rho>s \<kappa>) (ABS (\<sigma>s', \<tau>s')))"}\\
+  @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "(MAP(\<rho>s \<kappa>) (REP (\<sigma>s', \<tau>s'))) \<circ> Rep_\<kappa>\<^isub>q"}\\
+  \end{longtable}
   \end{center}
-
+  %
   \noindent
-  where in the last two clauses we have that the quotient type @{text "\<alpha>s \<kappa>\<^isub>2"} is a quotient of
-  the raw type @{text "\<rho>s \<kappa>\<^isub>1"} (for example @{text "\<alpha> fset"} and @{text "\<alpha> list"}). 
+  where in the last two clauses we have that the quotient type @{text "\<alpha>s \<kappa>\<^isub>q"} is a quotient of
+  the raw type @{text "\<rho>s \<kappa>"} (for example @{text "\<alpha> fset"} and @{text "\<alpha> list"}). 
   The quotient construction ensures that the type variables in @{text "\<rho>s"} 
   must be amongst the @{text "\<alpha>s"}. Now the @{text "\<sigma>s'"} are given by the matchers 
   for the @{text "\<alpha>s"} 
-  when matching  @{text "\<sigma>s \<kappa>\<^isub>2"} against @{text "\<alpha>s \<kappa>\<^isub>2"}; similarly the @{text "\<tau>s'"} are given by the 
-  same type-variables when matching @{text "\<tau>s \<kappa>\<^isub>1"} against @{text "\<rho>s \<kappa>\<^isub>1"}.
+  when matching  @{text "\<sigma>s \<kappa>\<^isub>q"} against @{text "\<alpha>s \<kappa>\<^isub>q"}; similarly the @{text "\<tau>s'"} are given by the 
+  same type-variables when matching @{text "\<tau>s \<kappa>"} against @{text "\<rho>s \<kappa>"}.
   The function @{text "MAP"} calculates an \emph{aggregate map-function} for a type 
   as follows:
 

--- a/Quotient-Paper/document/root.tex	Sun Jun 13 14:39:55 2010 +0200
+++ b/Quotient-Paper/document/root.tex	Sun Jun 13 17:01:15 2010 +0200
@@ -9,6 +9,7 @@
 \usepackage{tikz}
 \usepackage{pgf}
 \usepackage{verbdef}
+\usepackage{longtable}
 
 \urlstyle{rm}
 \isabellestyle{it}