--- a/FSet.thy	Fri Oct 30 19:03:53 2009 +0100
+++ b/FSet.thy	Mon Nov 02 09:33:48 2009 +0100
@@ -44,7 +44,7 @@
 thm EMPTY_def
 
 quotient_def (for "'a fset")
-  INSERT :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fet"
+  INSERT :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 where
   "INSERT \<equiv> op #"
 
@@ -168,10 +168,10 @@
 thm fold_def
 
 (* FIXME: does not work yet for all types*)
-quotient_def (for "'a fset")
-  fmap::"('a \<Rightarrow> 'a) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+quotient_def (for "'a fset" "'b fset")
+  fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
 where
-  "fmap \<equiv> (map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list)"
+  "fmap \<equiv> map"
 
 term map
 term fmap
@@ -296,6 +296,9 @@
  by simp (rule list_eq_refl)
 
 
+print_quotients
+
+
 ML {* val qty = @{typ "'a fset"} *}
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "fset" *}

--- a/QuotMain.thy	Fri Oct 30 19:03:53 2009 +0100
+++ b/QuotMain.thy	Mon Nov 02 09:33:48 2009 +0100
@@ -159,17 +159,13 @@
 section {* lifting of constants *}
 
 ML {*
-(* whether ty1 is an instance of ty2 *)
-fun matches (ty1, ty2) =
-  Type.raw_instance (ty1, Logic.varifyT ty2)
-
 fun lookup_snd _ [] _ = NONE
   | lookup_snd eq ((value, key)::xs) key' =
       if eq (key', key) then SOME value
       else lookup_snd eq xs key';
 
 fun lookup_qenv qenv qty =
-  (case (AList.lookup matches qenv qty) of
+  (case (AList.lookup (op =) qenv qty) of
     SOME rty => SOME (qty, rty)
   | NONE => NONE)
 *}
@@ -225,7 +221,7 @@
   fun mk_identity ty = Abs ("", ty, Bound 0)
 
 in
-  if (AList.defined matches qenv ty)
+  if (AList.defined (op =) qenv ty)
   then (get_const flag (the (lookup_qenv qenv ty)))
   else (case ty of
           TFree _ => (mk_identity ty, (ty, ty))
@@ -259,11 +255,10 @@
 end
 *}
 
-ML {* lookup_snd *}
 
 ML {*
 fun exchange_ty qenv ty =
-  case (lookup_snd matches qenv ty) of
+  case (lookup_snd (op =) qenv ty) of
     SOME qty => qty
   | NONE =>
     (case ty of
@@ -272,6 +267,18 @@
     )
 *}
 
+ML {* 
+fun ppair lthy (ty1, ty2) =
+  "(" ^ (Syntax.string_of_typ lthy ty1) ^ "," ^ (Syntax.string_of_typ lthy ty2) ^ ")"
+*}
+
+ML {*
+fun print_env qenv lthy =
+  map (ppair lthy) qenv
+  |> commas
+  |> tracing
+*}
+
 ML {*
 fun make_const_def nconst_bname otrm mx qenv lthy =
 let
@@ -279,6 +286,11 @@
   val nconst_ty = exchange_ty qenv otrm_ty
   val nconst = Const (Binding.name_of nconst_bname, nconst_ty)
   val def_trm = get_const_def nconst otrm qenv lthy
+
+  val _ = print_env qenv lthy
+  val _ = Syntax.string_of_typ lthy otrm_ty |> tracing
+  val _ = Syntax.string_of_typ lthy nconst_ty |> tracing
+  val _ = Syntax.string_of_term lthy def_trm |> tracing
 in
   define (nconst_bname, mx, def_trm) lthy
 end
@@ -288,46 +300,37 @@
 fun build_qenv lthy qtys = 
 let
   val qenv = map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) (quotdata_lookup lthy)
-
-  fun find_assoc qty =
-    case (AList.lookup matches qenv qty) of
-      SOME rty => (qty, rty)
-    | NONE => error (implode 
-              ["Quotient type ",     
-               quote (Syntax.string_of_typ lthy qty), 
-               " does not exists"])
+  val tsig = Sign.tsig_of (ProofContext.theory_of lthy)
+  
+  fun find_assoc ((qty', rty')::rest) qty =
+        let 
+          val inst = Type.typ_match tsig (qty', qty) Vartab.empty
+        in
+           (Envir.norm_type inst qty, Envir.norm_type inst rty')
+        end
+    | find_assoc [] qty =
+        let 
+          val qtystr =  quote (Syntax.string_of_typ lthy qty)
+        in
+          error (implode ["Quotient type ", qtystr, " does not exists"])
+        end
 in
-  map find_assoc qtys
+  map (find_assoc qenv) qtys
 end
 *}
 
 ML {*
-(* taken from isar_syn.ML *)
-val constdecl =
-  OuterParse.binding --
-    (OuterParse.where_ >> K (NONE, NoSyn) ||
-      OuterParse.$$$ "::" |-- OuterParse.!!! ((OuterParse.typ >> SOME) -- 
-      OuterParse.opt_mixfix' --| OuterParse.where_) ||
-      Scan.ahead (OuterParse.$$$ "(") |-- 
-      OuterParse.!!! (OuterParse.mixfix' --| OuterParse.where_ >> pair NONE))
-*}
-
-ML {*
 val qd_parser = 
   (Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) --
-    (constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop))
-*}
-
-ML {* 
-fun pair lthy (ty1, ty2) =
-  "(" ^ (Syntax.string_of_typ lthy ty1) ^ "," ^ (Syntax.string_of_typ lthy ty2) ^ ")"
+    (SpecParse.constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop))
 *}
 
 ML {*
-fun parse_qd_spec (qtystrs, ((bind, (typstr__, mx)), (attr__, propstr))) lthy = 
+fun parse_qd_spec (qtystrs, ((bind, tystr, mx), (attr__, propstr))) lthy = 
 let
   val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystrs
   val qenv = build_qenv lthy qtys
+  val qty = Syntax.parse_typ lthy (the tystr) |> Syntax.check_typ lthy
   val prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy
   val (lhs, rhs) = Logic.dest_equals prop
 in
@@ -340,6 +343,8 @@
   OuterKeyword.thy_decl (qd_parser >> parse_qd_spec)
 *}
 
+(* ML {* show_all_types := true *} *)
+
 section {* ATOMIZE *}
 
 text {*
@@ -501,10 +506,6 @@
          else
            Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t
        end
-  | Const (@{const_name "op ="}, ty) $ t =>
-      if needs_lift rty (fastype_of t) then
-        (tyRel (fastype_of t) rty rel lthy) $ t
-      else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t)
   | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2)
   | _ => trm
 *}
@@ -517,31 +518,16 @@
        (my_reg lthy rel rty (prop_of thm)))
 *}
 
-lemma universal_twice: "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))"
-apply (auto)
-done
-
-lemma implication_twice: "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
-apply (auto)
-done
-
 ML {*
-fun regularize thm rty rel rel_eqv rel_refl lthy =
+fun regularize thm rty rel rel_eqv lthy =
   let
     val g = build_regularize_goal thm rty rel lthy;
     fun tac ctxt =
-      (ObjectLogic.full_atomize_tac) THEN'
-     REPEAT_ALL_NEW (FIRST' [
-      rtac rel_refl,
-      atac,
-      rtac @{thm universal_twice},
-      rtac @{thm implication_twice},
-      (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
+       (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
         [(@{thm equiv_res_forall} OF [rel_eqv]),
-         (@{thm equiv_res_exists} OF [rel_eqv])]) i)),
-      (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl),
-      (rtac @{thm RIGHT_RES_FORALL_REGULAR})
-     ]);
+         (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW
+         (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN'
+         (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt []));
     val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1);
   in
     cthm OF [thm]
@@ -565,10 +551,14 @@
      )
 *}
 
+ML {* make_const_def *}
+
 ML {*
 fun old_get_fun flag rty qty lthy ty =
   get_fun flag [(qty, rty)] lthy ty 
+*}
 
+ML {*
 fun old_make_const_def nconst_bname otrm mx rty qty lthy =
   make_const_def nconst_bname otrm mx [(qty, rty)] lthy
 *}
@@ -926,7 +916,7 @@
   val (trans2, reps_same, quot) = lookup_quot_thms lthy qty_name;
   val consts = lookup_quot_consts defs;
   val t_a = atomize_thm t;
-  val t_r = regularize t_a rty rel rel_eqv rel_refl lthy;
+  val t_r = regularize t_a rty rel rel_eqv lthy;
   val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;
   val abs = findabs rty (prop_of t_a);
   val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs;

--- a/QuotTest.thy	Fri Oct 30 19:03:53 2009 +0100
+++ b/QuotTest.thy	Mon Nov 02 09:33:48 2009 +0100
@@ -2,6 +2,7 @@
 imports QuotMain
 begin
 
+
 section {* various tests for quotient types*}
 datatype trm =
   var  "nat"

--- a/quotient.ML	Fri Oct 30 19:03:53 2009 +0100
+++ b/quotient.ML	Mon Nov 02 09:33:48 2009 +0100
@@ -6,7 +6,7 @@
   val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state
   val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory
   val note: binding * thm -> local_theory -> thm * local_theory
-  val maps_lookup: theory -> string -> maps_info option
+  val maps_lookup_thy: theory -> string -> maps_info option
   val maps_update_thy: string -> maps_info -> theory -> theory    
   val maps_update: string -> maps_info -> Proof.context -> Proof.context                           
   val print_quotdata: Proof.context -> unit
@@ -32,7 +32,9 @@
    val extend = I
    fun merge _ = Symtab.merge (K true))
 
-val maps_lookup = Symtab.lookup o MapsData.get
+val maps_lookup_thy = Symtab.lookup o MapsData.get
+
+
 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo)
 
@@ -242,7 +244,7 @@
   val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
 
   (* storing the quot-info *)
-  val lthy3 = quotdata_update (abs_ty, rty, rel, equiv_thm) lthy2
+  val lthy3 = quotdata_update (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2
 
   (* interpretation *)
   val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))