# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1257497317 -3600
# Node ID 653460d3e8494078cad926893897737323c38506
# Parent  bd76f0398aa99e1fe47e74ca4a5cb8923576a9cc
tuned the code in quotient and quotient_def

diff -r bd76f0398aa9 -r 653460d3e849 QuotMain.thy
--- a/QuotMain.thy	Thu Nov 05 16:43:57 2009 +0100
+++ b/QuotMain.thy	Fri Nov 06 09:48:37 2009 +0100
@@ -1042,5 +1042,6 @@
 *}
 
 
+
 end
 
diff -r bd76f0398aa9 -r 653460d3e849 quotient.ML
--- a/quotient.ML	Thu Nov 05 16:43:57 2009 +0100
+++ b/quotient.ML	Fri Nov 06 09:48:37 2009 +0100
@@ -2,7 +2,7 @@
 sig
   val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state
   val 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
 end;
 
@@ -212,8 +212,8 @@
   fun parse_spec (((qty_str, mx), rty_str), rel_str) =
   let
     val qty_name = Binding.name qty_str
-    val rty = Syntax.parse_typ lthy rty_str |> Syntax.check_typ lthy
-    val rel = Syntax.parse_term lthy rel_str |> Syntax.check_term lthy
+    val rty = Syntax.read_typ lthy rty_str
+    val rel = Syntax.read_term lthy rel_str 
   in
     ((qty_name, mx), (rty, rel))
   end
diff -r bd76f0398aa9 -r 653460d3e849 quotient_def.ML
--- a/quotient_def.ML	Thu Nov 05 16:43:57 2009 +0100
+++ b/quotient_def.ML	Fri Nov 06 09:48:37 2009 +0100
@@ -3,7 +3,7 @@
 sig
   datatype flag = absF | repF
   val get_fun: flag -> (typ * typ) list -> Proof.context -> typ -> term
-  val make_def: binding -> term -> typ -> mixfix -> Attrib.binding -> (typ * typ) list ->
+  val make_def: binding -> typ -> mixfix -> Attrib.binding -> term ->
     Proof.context -> (term * thm) * local_theory
 
   val quotdef: (binding * typ * mixfix) * (Attrib.binding * term) ->
@@ -72,23 +72,6 @@
         | _ => error ("no type variables allowed"))
 end
 
-fun make_def nconst_bname rhs qty mx attr qenv lthy =
-let
-  val (arg_tys, res_ty) = strip_type qty
-
-  val rep_fns = map (get_fun repF qenv lthy) arg_tys
-  val abs_fn  = (get_fun absF qenv lthy) res_ty
-
-  fun mk_fun_map t s =  
-        Const (@{const_name "fun_map"}, dummyT) $ t $ s
-
-  val absrep_trm = (fold_rev mk_fun_map rep_fns abs_fn $ rhs)
-                   |> Syntax.check_term lthy 
-in
-  define nconst_bname mx attr absrep_trm lthy
-end
-
-
 (* returns all subterms where two types differ *)
 fun diff (T, S) Ds =
   case (T, S) of
@@ -104,19 +87,19 @@
 
 (* sanity check that the calculated quotient environment
    matches with the stored quotient environment. *)
-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
-  error (implode ["Quotient type ", qtystr, " does not match with ", rtystr])
-end
-
-fun sanity_chk lthy qenv =
+fun sanity_chk qenv lthy =
 let
   val global_qenv = Quotient_Info.mk_qenv lthy
   val thy = ProofContext.theory_of lthy
 
+  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
+    error (implode ["Quotient type ", qtystr, " does not match with ", rtystr])
+  end
+
   fun is_inst (qty, rty) (qty', rty') =
     if Sign.typ_instance thy (qty, qty')
     then let
@@ -134,17 +117,43 @@
   map chk_inst qenv
 end
 
+fun make_def nconst_bname qty mx attr rhs lthy =
+let
+  val (arg_tys, res_ty) = strip_type qty
+
+  val rty = fastype_of rhs
+  val qenv = distinct (op=) (diff (qty, rty) [])   
+
+  val _ = sanity_chk qenv lthy
+
+  val rep_fns = map (get_fun repF qenv lthy) arg_tys
+  val abs_fn  = (get_fun absF qenv lthy) res_ty
+
+  fun mk_fun_map t s =  
+        Const (@{const_name "fun_map"}, dummyT) $ t $ s
+
+  val absrep_trm = (fold_rev mk_fun_map rep_fns abs_fn $ rhs)
+                   |> Syntax.check_term lthy 
+in
+  define nconst_bname mx attr absrep_trm lthy
+end
+
+(* interface and syntax setup *)
+
+(* the ML-interface takes a 5-tuple consisting of  *)
+(*                                                 *)
+(* - the name of the constant to be lifted         *)
+(* - its type                                      *)
+(* - its mixfix annotation                         *)
+(* - a meta-equation defining the constant,        *)
+(*   and the attributes of for this meta-equality  *)
 
 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 attr qenv lthy 
+  make_def bind qty mx attr rhs lthy 
 end
 
 fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy =