--- a/FSet.thy	Tue Nov 03 16:17:19 2009 +0100
+++ b/FSet.thy	Tue Nov 03 16:51:33 2009 +0100
@@ -34,7 +34,7 @@
 thm "Rep_fset"
 thm "ABS_fset_def"
 
-quotient_def (for "'a fset")
+quotient_def 
   EMPTY :: "'a fset"
 where
   "EMPTY \<equiv> ([]::'a list)"
@@ -43,7 +43,7 @@
 term EMPTY
 thm EMPTY_def
 
-quotient_def (for "'a fset")
+quotient_def 
   INSERT :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 where
   "INSERT \<equiv> op #"
@@ -52,7 +52,7 @@
 term INSERT
 thm INSERT_def
 
-quotient_def (for "'a fset")
+quotient_def 
   FUNION :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 where
   "FUNION \<equiv> (op @)"
@@ -78,7 +78,7 @@
   card1_nil: "(card1 []) = 0"
 | card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))"
 
-quotient_def (for "'a fset")
+quotient_def 
   CARD :: "'a fset \<Rightarrow> nat"
 where
   "CARD \<equiv> card1"
@@ -144,7 +144,7 @@
   apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons m1)
   done
 
-quotient_def (for "'a fset")
+quotient_def 
   IN :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool"
 where
   "IN \<equiv> membship"
@@ -168,7 +168,7 @@
 thm fold_def
 
 (* FIXME: does not work yet for all types*)
-quotient_def (for "'a fset" "'b fset")
+quotient_def 
   fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
 where
   "fmap \<equiv> map"

--- a/IntEx.thy	Tue Nov 03 16:17:19 2009 +0100
+++ b/IntEx.thy	Tue Nov 03 16:51:33 2009 +0100
@@ -14,13 +14,15 @@
 
 print_theorems
 
-quotient_def (for my_int)
+quotient_def 
   ZERO::"my_int"
 where
   "ZERO \<equiv> (0::nat, 0::nat)"
 
+term ZERO
+thm ZERO_def
 
-quotient_def (for my_int)
+quotient_def 
   ONE::"my_int"
 where
   "ONE \<equiv> (1::nat, 0::nat)"
@@ -33,7 +35,7 @@
 where
   "my_plus (x, y) (u, v) = (x + u, y + v)"
 
-quotient_def (for my_int)
+quotient_def 
   PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
 where
   "PLUS \<equiv> my_plus"
@@ -48,13 +50,12 @@
 thm MPLUS_def
 thm MPLUS_def_raw
 
-
 fun
   my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 where
   "my_neg (x, y) = (y, x)"
 
-quotient_def (for my_int)
+quotient_def 
   NEG::"my_int \<Rightarrow> my_int"
 where
   "NEG \<equiv> my_neg"
@@ -72,7 +73,7 @@
 where
   "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
-quotient_def (for my_int)
+quotient_def 
   MULT::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
 where
   "MULT \<equiv> my_mult"
@@ -86,7 +87,7 @@
 where
   "my_le (x, y) (u, v) = (x+v \<le> u+y)"
 
-quotient_def (for my_int)
+quotient_def 
   LE :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"
 where
   "LE \<equiv> my_le"

--- a/LamEx.thy	Tue Nov 03 16:17:19 2009 +0100
+++ b/LamEx.thy	Tue Nov 03 16:51:33 2009 +0100
@@ -37,17 +37,17 @@
 
 print_quotients
 
-quotient_def (for lam)
+quotient_def 
   Var :: "name \<Rightarrow> lam"
 where
   "Var \<equiv> rVar"
 
-quotient_def (for lam)
+quotient_def 
   App :: "lam \<Rightarrow> lam \<Rightarrow> lam"
 where
   "App \<equiv> rApp"
 
-quotient_def (for lam)
+quotient_def 
   Lam :: "name \<Rightarrow> lam \<Rightarrow> lam"
 where
   "Lam \<equiv> rLam"
@@ -56,7 +56,7 @@
 thm App_def
 thm Lam_def
 
-quotient_def (for lam)
+quotient_def 
   fv :: "lam \<Rightarrow> name set"
 where
   "fv \<equiv> rfv"
@@ -66,10 +66,10 @@
 (* definition of overloaded permutation function *)
 (* for the lifted type lam                       *)
 overloading
-  perm_lam    \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"   (unchecked)
+  perm_lam \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"   (unchecked)
 begin
 
-quotient_def (for lam)
+quotient_def 
   perm_lam :: "'x prm \<Rightarrow> lam \<Rightarrow> lam"
 where
   "perm_lam \<equiv> (perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam)"
@@ -308,14 +308,11 @@
 thm alpha.induct
 
 lemma rvar_inject: "rVar a \<approx> rVar b \<Longrightarrow> (a = b)"
-apply (rule alpha.cases)
-apply (assumption)
-apply (assumption)
-apply (simp_all)
-apply (cases "a = b")
-apply (simp_all)
-apply (cases "ba = b")
-apply (simp_all)
+apply (erule alpha.cases)
+apply (simp add: rlam.inject)
+apply (simp)
+apply (simp)
+done
 
 
 lemma var_inject_test:

--- a/QuotMain.thy	Tue Nov 03 16:17:19 2009 +0100
+++ b/QuotMain.thy	Tue Nov 03 16:51:33 2009 +0100
@@ -140,8 +140,15 @@
 
 section {* type definition for the quotient type *}
 
+(* the auxiliary data for the quotient types *)
 use "quotient_info.ML"
-use "quotient.ML"
+
+ML {*
+fun error_msg pre post msg = 
+  msg |> quote
+      |> enclose (pre ^ " ") (" " ^ post) 
+      |> error  
+*}
 
 declare [[map list = (map, LIST_REL)]]
 declare [[map * = (prod_fun, prod_rel)]]
@@ -151,6 +158,11 @@
 ML {* maps_lookup @{theory} "*" *}
 ML {* maps_lookup @{theory} "fun" *}
 
+
+(* definition of the quotient types *)
+use "quotient.ML"
+
+
 text {* FIXME: auxiliary function *}
 ML {*
 val no_vars = Thm.rule_attribute (fn context => fn th =>
@@ -238,7 +250,6 @@
 end
 *}
 
-
 text {* produces the definition for a lifted constant *}
 
 ML {*
@@ -290,65 +301,56 @@
   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
 *}
 
 ML {*
-fun build_qenv lthy qtys = 
-let
-  val qenv = map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) (quotdata_lookup lthy)
-  val thy = ProofContext.theory_of lthy
-  
-  fun find_assoc ((qty', rty')::rest) qty =
-        let 
-          val inst = Sign.typ_match thy (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 qenv) qtys
-end
+(* difference of two types *)
+fun diff (T, S) Ds =
+  case (T, S) of
+    (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds 
+  | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds
+  | (Type (a, Ts), Type (b, Us)) => 
+      if a = b then diffs (Ts, Us) Ds else (T, S)::Ds
+  | _ => (T, S)::Ds
+and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds)
+  | diffs ([], []) Ds = Ds
+  | diffs _ _ = error "Unequal length of type arguments"
 *}
 
-
 ML {*
-fun quotdef_cmd qenv ((bind, qty_, mx), (attr, prop)) lthy =
+fun quotdef_cmd ((bind, qty, mx), (attr, prop)) lthy =
 let    
-  val (lhs_, rhs) = Logic.dest_equals prop
+  val (_, rhs) = Logic.dest_equals prop
+  val rty = fastype_of rhs
+  val qenv = distinct (op=) (diff (qty, rty) [])
 in
   make_const_def bind rhs mx qenv lthy
 end
 *}
 
 ML {*
-val quotdef_parser = 
-  Scan.option (Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) --
-    (SpecParse.constdecl -- (SpecParse.opt_thm_name ":" -- 
-       OuterParse.prop)) >> OuterParse.triple2
+val constdecl =
+  OuterParse.binding --
+    (OuterParse.$$$ "::" |-- OuterParse.!!! 
+      (OuterParse.typ -- OuterParse.opt_mixfix' --| OuterParse.where_))
+  >> OuterParse.triple2;
 *}
 
 ML {*
-fun quotdef (qtystrs, (bind, tystr, mx), (attr, propstr)) lthy = 
+val quotdef_parser = 
+  (constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop)) 
+*}
+
+ML {*
+fun quotdef ((bind, qtystr, mx), (attr, propstr)) lthy = 
 let
-  val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) (the qtystrs)
-  val qenv = build_qenv lthy qtys
-  val qty  = Option.map (Syntax.check_typ lthy o Syntax.parse_typ lthy) tystr
-  val prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy
+  val qty  = (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystr
+  val prop = (Syntax.check_prop lthy o Syntax.parse_prop lthy) propstr
 in
-  quotdef_cmd qenv ((bind, qty, mx), (attr, prop)) lthy |> snd
+  quotdef_cmd ((bind, qty, mx), (attr, prop)) lthy |> snd
 end
 *}
 

--- a/quotient_info.ML	Tue Nov 03 16:17:19 2009 +0100
+++ b/quotient_info.ML	Tue Nov 03 16:51:33 2009 +0100
@@ -11,11 +11,16 @@
   val quotdata_lookup: Proof.context -> quotient_info list
   val quotdata_update_thy: (typ * typ * term * thm) -> theory -> theory
   val quotdata_update: (typ * typ * term * thm) -> Proof.context -> Proof.context
+
+  type qenv = (typ * typ) list
+  val mk_qenv: Proof.context -> qenv
+  val lookup_qenv: ((typ * typ) -> bool) -> qenv -> typ -> (typ * typ) option
 end;
 
 structure Quotient_Info: QUOTIENT_INFO =
 struct
 
+
 (* data containers *)
 (*******************)
 
@@ -102,6 +107,22 @@
   OuterSyntax.improper_command "print_quotients" "print out all quotients" 
     OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotdata o Toplevel.context_of)))
 
+
+(* environments of quotient and raw types *)
+type qenv = (typ * typ) list
+
+fun mk_qenv ctxt =
+let
+  val qinfo = quotdata_lookup ctxt
+in
+  map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) qinfo
+end
+
+fun lookup_qenv _ [] _ = NONE
+  | lookup_qenv eq ((qty, rty)::xs) qty' =
+      if eq (qty', qty) then SOME (qty, rty)
+      else lookup_qenv eq xs qty'
+
 end; (* structure *)
 
 open Quotient_Info
\ No newline at end of file