diff -r b82e765ca464 -r df225aa45770 QuotMain.thy
--- a/QuotMain.thy	Wed Nov 04 09:52:31 2009 +0100
+++ b/QuotMain.thy	Wed Nov 04 10:31:20 2009 +0100
@@ -143,12 +143,6 @@
 (* the auxiliary data for the quotient types *)
 use "quotient_info.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)]]
@@ -175,13 +169,9 @@
 section {* lifting of constants *}
 
 ML {*
-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 (op =) qenv qty) of
+  (case (AList.lookup (op=) qenv qty) of
     SOME rty => SOME (qty, rty)
   | NONE => NONE)
 *}
@@ -210,7 +200,7 @@
   in
    (case (maps_lookup (ProofContext.theory_of lthy) s) of
       SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty))
-    | NONE      => raise ERROR ("no map association for type " ^ s))
+    | NONE      => error ("no map association for type " ^ s))
   end
 
   fun get_fun_fun fs_tys =
@@ -237,7 +227,7 @@
   fun mk_identity ty = Abs ("", ty, Bound 0)
 
 in
-  if (AList.defined (op =) 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))
@@ -250,64 +240,26 @@
 end
 *}
 
-text {* produces the definition for a lifted constant *}
-
 ML {*
-fun get_const_def nconst otrm qenv lthy =
+fun make_def nconst_bname rhs qty mx qenv lthy =
 let
-  val ty = fastype_of nconst
-  val (arg_tys, res_ty) = strip_type ty
+  val (arg_tys, res_ty) = strip_type qty
 
   val rep_fns = map (fst o get_fun repF qenv lthy) arg_tys
   val abs_fn  = (fst o get_fun absF qenv lthy) res_ty
 
-  fun mk_fun_map (t1,t2) = Const (@{const_name "fun_map"}, dummyT) $ t1 $ t2
-
-  val fns = Library.foldr mk_fun_map (rep_fns, abs_fn)
-            |> Syntax.check_term lthy
-in
-  fns $ otrm
-end
-*}
-
-
-ML {*
-fun exchange_ty qenv ty =
-  case (lookup_snd (op =) qenv ty) of
-    SOME qty => qty
-  | NONE =>
-    (case ty of
-       Type (s, tys) => Type (s, map (exchange_ty qenv) tys)
-      | _ => ty
-    )
-*}
+  fun mk_fun_map t s = 
+        Const (@{const_name "fun_map"}, dummyT) $ t $ s
 
-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
-  val otrm_ty = fastype_of otrm
-  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 absrep_fn = fold_rev mk_fun_map rep_fns abs_fn
+                  |> Syntax.check_term lthy 
 in
-  define (nconst_bname, mx, def_trm) lthy
+  define (nconst_bname, mx, absrep_fn $ rhs) lthy
 end
 *}
 
 ML {*
-(* difference of two types *)
+(* returns all subterms where two types differ *)
 fun diff (T, S) Ds =
   case (T, S) of
     (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds 
@@ -321,42 +273,73 @@
 *}
 
 ML {*
-fun quotdef_cmd ((bind, qty, mx), (attr, prop)) lthy =
-let    
-  val (_, rhs) = Logic.dest_equals prop
-  val rty = fastype_of rhs
-  val qenv = distinct (op=) (diff (qty, rty) [])
+fun error_msg lthy (qty, rty) =
+let 
+  val qtystr = quote (Syntax.string_of_typ lthy qty)
+  val rtystr = quote (Syntax.string_of_typ lthy rty)
 in
-  make_const_def bind rhs mx qenv lthy
+  error (implode ["Quotient type ", qtystr, " does not match with ", rtystr])
+end
+
+
+fun sanity_chk lthy qenv =
+let
+   val qenv' = Quotient_Info.mk_qenv lthy
+   val thy = ProofContext.theory_of lthy
+
+   fun is_inst thy (qty, rty) (qty', rty') =
+   if Sign.typ_instance thy (qty, qty')
+   then let
+          val inst = Sign.typ_match thy (qty', qty) Vartab.empty
+        in
+          rty = Envir.subst_type inst rty'
+        end
+   else false
+
+   fun chk_inst (qty, rty) = 
+     if exists (is_inst thy (qty, rty)) qenv' then true
+     else error_msg lthy (qty, rty)
+in
+  forall chk_inst qenv
 end
 *}
 
 ML {*
-val constdecl =
-  OuterParse.binding --
-    (OuterParse.$$$ "::" |-- OuterParse.!!! 
-      (OuterParse.typ -- OuterParse.opt_mixfix' --| OuterParse.where_))
-  >> OuterParse.triple2;
+fun quotdef ((bind, qty, mx), (attr, prop)) lthy =
+let   
+  val (_, prop') = PrimitiveDefs.dest_def lthy (K true) (K false) (K false) prop
+  val (_, rhs) = PrimitiveDefs.abs_def prop'
+
+  val rty = fastype_of rhs
+  val qenv = distinct (op=) (diff (qty, rty) [])
+ 
+in
+  sanity_chk lthy qenv;
+  make_def bind rhs qty mx qenv lthy 
+end
 *}
 
 ML {*
-val quotdef_parser = 
-  (constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop)) 
+val quotdef_parser =
+  (OuterParse.binding --
+    (OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.typ -- 
+      OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) -- 
+       (SpecParse.opt_thm_name ":" -- OuterParse.prop)
 *}
 
 ML {*
-fun quotdef ((bind, qtystr, mx), (attr, propstr)) lthy = 
+fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy = 
 let
   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 ((bind, qty, mx), (attr, prop)) lthy |> snd
+  quotdef ((bind, qty, mx), (attr, prop)) lthy |> snd
 end
 *}
 
 ML {*
 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
-  OuterKeyword.thy_decl (quotdef_parser >> quotdef)
+  OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
 *}
 
 section {* ATOMIZE *}
@@ -595,7 +578,7 @@
   get_fun flag [(qty, rty)] lthy ty 
 
 fun old_make_const_def nconst_bname otrm mx rty qty lthy =
-  make_const_def nconst_bname otrm mx [(qty, rty)] lthy
+  make_def nconst_bname otrm qty mx [(qty, rty)] lthy
 *}
 
 text {* Does the same as 'subst' in a given prop or theorem *}