--- a/Quot/Examples/AbsRepTest.thy	Sat Dec 26 20:45:37 2009 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Sat Dec 26 21:36:20 2009 +0100
@@ -4,142 +4,101 @@
 
 ML {* open Quotient_Term *}
 
-print_maps
-
+ML {*
+fun test_funs flag ctxt (rty, qty) =
+  (absrep_fun_chk flag ctxt (rty, qty)
+   |> Syntax.string_of_term ctxt
+   |> writeln;
+   equiv_relation_chk ctxt (rty, qty) 
+   |> Syntax.string_of_term ctxt
+   |> writeln)  
+*}
 
-quotient_type 
-  'a fset = "'a list" / "\<lambda>xs ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" 
-  apply(rule equivpI)
-  unfolding reflp_def symp_def transp_def
-  by auto
+definition
+  erel1 (infixl "\<approx>1" 50)
+where
+  "erel1 \<equiv> \<lambda>xs ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys"
 
 quotient_type 
-  'a foo = "('a * 'a) list" / "\<lambda>(xs::('a * 'a) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" 
+  'a fset = "'a list" / erel1
   apply(rule equivpI)
-  unfolding reflp_def symp_def transp_def
+  unfolding erel1_def reflp_def symp_def transp_def
   by auto
 
+definition
+  erel2 (infixl "\<approx>2" 50)
+where
+  "erel2 \<equiv> \<lambda>(xs::('a * 'a) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys"
+
 quotient_type 
-  'a bar = "('a * int) list" / "\<lambda>(xs::('a * int) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" 
+  'a foo = "('a * 'a) list" / erel2
   apply(rule equivpI)
-  unfolding reflp_def symp_def transp_def
+  unfolding erel2_def reflp_def symp_def transp_def
+  by auto
+
+definition
+  erel3 (infixl "\<approx>3" 50)
+where
+  "erel3 \<equiv> \<lambda>(xs::('a * int) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys"
+
+quotient_type 
+  'a bar = "('a * int) list" / "erel3"
+  apply(rule equivpI)
+  unfolding erel3_def reflp_def symp_def transp_def
   by auto
 
 fun
-  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" 
+  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infixl "\<approx>4" 50)
 where
   "intrel (x, y) (u, v) = (x + v = u + y)"
 
-quotient_type int = "nat \<times> nat" / intrel
+quotient_type myint = "nat \<times> nat" / intrel
   by (auto simp add: equivp_def expand_fun_eq)
 
-print_quotients
-
 ML {*
-absrep_fun_chk absF @{context} 
-     (@{typ "('a * 'a) list"}, 
-      @{typ "'a foo"})
-|> Syntax.string_of_term @{context}
-|> writeln
+test_funs absF @{context} 
+     (@{typ "nat \<times> nat"}, 
+      @{typ "myint"})
 *}
 
-(* PROBLEM
 ML {*
-absrep_fun_chk absF @{context} 
+test_funs absF @{context} 
+     (@{typ "('a * 'a) list"}, 
+      @{typ "'a foo"})
+*}
+
+ML {*
+test_funs absF @{context} 
      (@{typ "(('a list) * int) list"}, 
       @{typ "('a fset) bar"})
-|> Syntax.string_of_term @{context}
-|> writeln
-*}*)
-
-ML {*
-absrep_fun_chk absF @{context} 
-     (@{typ "('a list) list"}, 
-      @{typ "('a fset) fset"})
-|> Syntax.string_of_term @{context}
-|> writeln
 *}
 
 ML {*
-absrep_fun_chk absF @{context} 
-     (@{typ "nat \<times> nat"}, 
-      @{typ "int"})
-|> Syntax.string_of_term @{context}
-|> writeln
+test_funs absF @{context} 
+     (@{typ "('a list) list"}, 
+      @{typ "('a fset) fset"})
+*}
+
+ML {*
+test_funs absF @{context} 
+     (@{typ "(('a * 'a) list) list"}, 
+      @{typ "(('a * 'a) fset) fset"})
+*}
+
+ML {*
+test_funs absF @{context} 
+      (@{typ "(nat * nat) list"}, 
+       @{typ "myint fset"})
+*}
+
+ML {*
+test_funs absF @{context} 
+     (@{typ "('a list) list \<Rightarrow> 'a"}, 
+      @{typ "('a fset) fset \<Rightarrow> 'a"})
 *}
 
 
-term abs_foo
-term rep_foo
-term "abs_foo o map (prod_fun id id)"
-term "map (prod_fun id id) o rep_foo"
-
-ML {*
-absrep_fun_chk absF @{context} 
-     (@{typ "('a * 'a) list"}, 
-      @{typ "'a foo"})
-|> Syntax.string_of_term @{context}
-|> writeln
-*}
-
-typ "('a fset) foo"
-
-print_quotients
-
-ML{*
-Quotient_Info.quotient_rules_get @{context}
-*}
-
-print_quotients
-
-ML {*
-open Quotient_Term;
-*}
-
-ML {*
-absrep_fun_chk absF @{context} 
-     (@{typ "(('a * 'a) list) list"}, 
-      @{typ "(('a * 'a) fset) fset"})
-|> Syntax.string_of_term @{context}
-|> writeln
-*}
-
-(*
-ML {*
-absrep_fun_chk absF @{context} 
-     (@{typ "('a * 'a) list"}, 
-      @{typ "'a foo"})
-|> Syntax.string_of_term @{context}
-|> writeln
-*}
-*)
-
-term "option_map (prod_fun (abs_fset \<circ> map abs_int) id)"
-term "option_map (prod_fun (map rep_int \<circ> rep_fset) id)"
-term "option_map (map rep_int \<circ> rep_fset)"
-term "option_map (abs_fset o (map abs_int))"
-term "abs_fset"
-
-ML {*
-absrep_fun_chk absF @{context} (@{typ "(nat * nat) list"}, @{typ "int fset"})
-|> Syntax.string_of_term @{context}
-|> writeln
-*}
-
-term "map abs_int"
-term "abs_fset o map abs_int"
 
 
-ML {*
-absrep_fun_chk absF @{context} (@{typ "('a list) list"}, @{typ "('a fset) fset"})
-|> Syntax.string_of_term @{context}
-|> writeln
-*}
-
-ML {*
-absrep_fun_chk absF @{context} (@{typ "('a list) list \<Rightarrow> 'a"}, @{typ "('a fset) fset \<Rightarrow> 'a"})
-|> Syntax.string_of_term @{context}
-|> writeln
-*}
 
 end
\ No newline at end of file

--- a/Quot/quotient_term.ML	Sat Dec 26 20:45:37 2009 +0100
+++ b/Quot/quotient_term.ML	Sat Dec 26 21:36:20 2009 +0100
@@ -7,6 +7,9 @@
    val absrep_fun: flag -> Proof.context -> (typ * typ) -> term
    val absrep_fun_chk: flag -> Proof.context -> (typ * typ) -> term
 
+   val equiv_relation: Proof.context -> (typ * typ) -> term
+   val equiv_relation_chk: Proof.context -> (typ * typ) -> term
+
    val regularize_trm: Proof.context -> (term * term) -> term
    val regularize_trm_chk: Proof.context -> (term * term) -> term
    
@@ -57,7 +60,7 @@
 (* 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          *)        
+(* correspond to the type variables in rty)         *)        
 fun mk_mapfun ctxt vs ty =
 let
   val vs' = map (mk_Free) vs
@@ -83,8 +86,9 @@
   (#rtyp qdata, #qtyp qdata)
 end
 
-(* receives two type-environments and looks *)
-(* up in both of them the variable v        *)
+(* 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)
@@ -103,7 +107,16 @@
   | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
 end
 
-(* produces the aggregate absrep function                          *)
+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
+
+(* produces an aggregate absrep function                           *)
 (*                                                                 *)
 (* - In case of function types and TFrees, we recurse, taking in   *) 
 (*   the first case the polarity change into account.              *)
@@ -157,12 +170,11 @@
         else
            let
              val thy = ProofContext.theory_of ctxt
-             val exc = (LIFT_MATCH "absrep_fun (Types do not match.)")
              val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
-             val (rtyenv, qtyenv) = 
-                     (Sign.typ_match thy (rty_pat, rty) Vartab.empty,
-                      Sign.typ_match thy (qty_pat, qty) Vartab.empty)
-                      handle MATCH_TYPE => raise exc
+             val rtyenv = Sign.typ_match thy (rty_pat, rty) Vartab.empty
+                          handle MATCH_TYPE => absrep_match_err ctxt rty_pat rty
+             val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty
+                          handle MATCH_TYPE => absrep_match_err ctxt 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       
@@ -182,31 +194,9 @@
   |> Syntax.check_term ctxt
 
 
-(* Regularizing an rtrm means:
- 
- - Quantifiers over types that need lifting are replaced 
-   by bounded quantifiers, for example:
-
-      All P  ----> All (Respects R) P
-
-   where the aggregate relation R is given by the rty and qty;
- 
- - Abstractions over types that need lifting are replaced
-   by bounded abstractions, for example:
-      
-      %x. P  ----> Ball (Respects R) %x. P
-
- - Equalities over types that need lifting are replaced by
-   corresponding equivalence relations, for example:
-
-      A = B  ----> R A B
-
-   or 
-
-      A = B  ----> (R ===> R) A B
- 
-   for more complicated types of A and B
-*)
+(**********************************)
+(* Aggregate Equivalence Relation *)
+(**********************************)
 
 (* instantiates TVars so that the term is of type ty *)
 fun force_typ ctxt trm ty =
@@ -239,7 +229,7 @@
 (* that will be the argument of Respects     *)
 
 (* FIXME: check that the types correspond to each other? *)
-fun mk_resp_arg ctxt (rty, qty) =
+fun equiv_relation ctxt (rty, qty) =
   if rty = qty
   then HOLogic.eq_const rty
   else
@@ -248,7 +238,7 @@
        if s = s' 
        then 
          let
-           val args = map (mk_resp_arg ctxt) (tys ~~ tys')
+           val args = map (equiv_relation ctxt) (tys ~~ tys')
          in
            list_comb (get_relmap ctxt s, args) 
          end  
@@ -259,6 +249,42 @@
            force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
          end
       | _ => HOLogic.eq_const rty
+
+fun equiv_relation_chk ctxt (rty, qty) =
+  equiv_relation ctxt (rty, qty)
+  |> Syntax.check_term ctxt
+
+
+(******************)
+(* Regularization *)
+(******************)
+
+(* Regularizing an rtrm means:
+ 
+ - Quantifiers over types that need lifting are replaced 
+   by bounded quantifiers, for example:
+
+      All P  ----> All (Respects R) P
+
+   where the aggregate relation R is given by the rty and qty;
+ 
+ - Abstractions over types that need lifting are replaced
+   by bounded abstractions, for example:
+      
+      %x. P  ----> Ball (Respects R) %x. P
+
+ - Equalities over types that need lifting are replaced by
+   corresponding equivalence relations, for example:
+
+      A = B  ----> R A B
+
+   or 
+
+      A = B  ----> (R ===> R) A B
+ 
+   for more complicated types of A and B
+*)
+
             
 val mk_babs = Const (@{const_name Babs}, dummyT)
 val mk_ball = Const (@{const_name Ball}, dummyT)
@@ -292,7 +318,7 @@
          val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
        in
          if ty = ty' then subtrm
-         else mk_babs $ (mk_resp $ mk_resp_arg ctxt (ty, ty')) $ subtrm
+         else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
        end
 
   | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
@@ -300,7 +326,7 @@
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
        in
          if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm
-         else mk_ball $ (mk_resp $ mk_resp_arg ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
+         else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
   | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
@@ -308,20 +334,20 @@
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
        in
          if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm
-         else mk_bex $ (mk_resp $ mk_resp_arg ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
+         else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
   | (* equalities need to be replaced by appropriate equivalence relations *) 
     (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
          if ty = ty' then rtrm
-         else mk_resp_arg ctxt (domain_type ty, domain_type ty') 
+         else equiv_relation ctxt (domain_type ty, domain_type ty') 
 
   | (* in this case we just check whether the given equivalence relation is correct *) 
     (rel, Const (@{const_name "op ="}, ty')) =>
        let 
          val exc = LIFT_MATCH "regularise (relation mismatch)"
          val rel_ty = fastype_of rel
-         val rel' = mk_resp_arg ctxt (domain_type rel_ty, domain_type ty') 
+         val rel' = equiv_relation ctxt (domain_type rel_ty, domain_type ty') 
        in 
          if rel' aconv rel then rtrm else raise exc
        end  
@@ -376,6 +402,10 @@
   regularize_trm ctxt (rtrm, qtrm) 
   |> Syntax.check_term ctxt
 
+(*********************)
+(* Rep/Abs Injection *)
+(*********************)
+
 (*
 Injection of Rep/Abs means: