# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1255990325 -7200
# Node ID 8e8ba210f0f7d3779ee1bd24e70c5b5fa9464798
# Parent  89283c1dbba7e1df4c8fb95809f4121e9ef93fd4
moved the map-info and fun-info section to quotient.ML

diff -r 89283c1dbba7 -r 8e8ba210f0f7 QuotMain.thy
--- a/QuotMain.thy	Sun Oct 18 10:34:53 2009 +0200
+++ b/QuotMain.thy	Tue Oct 20 00:12:05 2009 +0200
@@ -147,7 +147,15 @@
 
 use "quotient.ML"
 
-term EQUIV
+(* mapfuns for some standard types *)
+setup {*
+  maps_update @{type_name "list"} {mapfun = @{const_name "map"},      relfun = @{const_name "LIST_REL"}} #>
+  maps_update @{type_name "*"}    {mapfun = @{const_name "prod_fun"}, relfun = @{const_name "prod_rel"}} #>
+  maps_update @{type_name "fun"}  {mapfun = @{const_name "fun_map"},  relfun = @{const_name "FUN_REL"}}
+*}
+
+
+ML {* maps_lookup @{theory} @{type_name list} *}
 
 ML {*
 val no_vars = Thm.rule_attribute (fn context => fn th =>
@@ -225,33 +233,6 @@
 
 section {* lifting of constants *}
 
-text {* information about map-functions for type-constructor *}
-ML {*
-type typ_info = {mapfun: string, relfun: string}
-
-local
-  structure Data = TheoryDataFun
-  (type T = typ_info Symtab.table
-   val empty = Symtab.empty
-   val copy = I
-   val extend = I
-   fun merge _ = Symtab.merge (K true))
-in
-  val lookup = Symtab.lookup o Data.get
-  fun update k v = Data.map (Symtab.update (k, v))
-end
-*}
-
-(* mapfuns for some standard types *)
-setup {*
-  update @{type_name "list"} {mapfun = @{const_name "map"},      relfun = @{const_name "LIST_REL"}} #>
-  update @{type_name "*"}    {mapfun = @{const_name "prod_fun"}, relfun = @{const_name "prod_rel"}} #>
-  update @{type_name "fun"}  {mapfun = @{const_name "fun_map"},  relfun = @{const_name "FUN_REL"}}
-*}
-
-
-ML {* lookup @{theory} @{type_name list} *}
-
 ML {*
 (* calculates the aggregate abs and rep functions for a given type; 
    repF is for constants' arguments; absF is for constants;
@@ -275,7 +256,7 @@
     val nty = Type (s, ntys)
     val ftys = map (op -->) tys
   in
-   (case (lookup (ProofContext.theory_of lthy) s) of
+   (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))
   end
@@ -1007,7 +988,7 @@
               val ty_out = ty --> ty --> @{typ bool};
               val tys_out = tys_rel ---> ty_out;
             in
-            (case (lookup (ProofContext.theory_of lthy) s) of
+            (case (maps_lookup (ProofContext.theory_of lthy) s) of
                SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys)
              | NONE  => HOLogic.eq_const ty
             )
diff -r 89283c1dbba7 -r 8e8ba210f0f7 quotient.ML
--- a/quotient.ML	Sun Oct 18 10:34:53 2009 +0200
+++ b/quotient.ML	Tue Oct 20 00:12:05 2009 +0200
@@ -1,14 +1,40 @@
 signature QUOTIENT =
 sig
+  type maps_info = {mapfun: string, relfun: string}
   val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state
   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_update: string -> maps_info -> theory -> theory                                  
+
 end;
 
 structure Quotient: QUOTIENT =
 struct
 
+(* data containers *)
+(*******************)
+
+(* map-functions and rel-functions *)
+type maps_info = {mapfun: string, relfun: string}
+
+local
+  structure Data = TheoryDataFun
+  (type T = maps_info Symtab.table
+   val empty = Symtab.empty
+   val copy = I
+   val extend = I
+   fun merge _ = Symtab.merge (K true))
+in
+  val maps_lookup = Symtab.lookup o Data.get
+  fun maps_update k v = Data.map (Symtab.update (k, v))
+end
+
+
+(* definition of the quotient type *)
+(***********************************)
+
 (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *)
 fun typedef_term rel rty lthy =
 let
@@ -167,6 +193,9 @@
       in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)
 end
 
+
+
+
 (* interface and syntax setup *)
 
 (* the ML-interface takes a list of 4-tuples consisting of  *)
@@ -175,7 +204,7 @@
 (* - its mixfix annotation                                  *)
 (* - the type to be quotient                                *)
 (* - the relation according to which the type is quotient   *)
-  
+
 fun mk_quotient_type quot_list lthy = 
 let
   fun get_goal (rty, rel) =