# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1256422480 -7200
# Node ID c7eff9882bd8236662f35ff608054c83e9042826
# Parent  3e53081ad53a9b369df1ab1ac3331ff10e3e1a6f
added data-storage about the quotients

diff -r 3e53081ad53a -r c7eff9882bd8 QuotMain.thy
--- a/QuotMain.thy	Sat Oct 24 22:52:23 2009 +0200
+++ b/QuotMain.thy	Sun Oct 25 00:14:40 2009 +0200
@@ -164,15 +164,6 @@
   maps_update @{type_name "fun"}  {mapfun = @{const_name "fun_map"},  relfun = @{const_name "FUN_REL"}}
 *}
 
-
-ML {* quotdata_lookup @{theory} *}
-setup {* quotdata_update_thy (@{typ nat}, @{typ bool}, @{term "True"})*}
-ML {* quotdata_lookup @{theory} *}
-
-ML {* print_quotdata @{context} *}
-
-ML {* maps_lookup @{theory} @{type_name list} *}
-
 ML {*
 val no_vars = Thm.rule_attribute (fn context => fn th =>
   let
diff -r 3e53081ad53a -r c7eff9882bd8 quotient.ML
--- a/quotient.ML	Sat Oct 24 22:52:23 2009 +0200
+++ b/quotient.ML	Sun Oct 25 00:14:40 2009 +0200
@@ -45,10 +45,12 @@
    fun merge _ = (op @))
 
 val quotdata_lookup = QuotData.get
+
 fun quotdata_update_thy (qty, rty, rel) = 
       QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel}::ls)
 
-fun quotdata_update (qty, rty, rel) = ProofContext.theory (quotdata_update_thy (qty, rty, rel))
+fun quotdata_update (qty, rty, rel) = 
+      ProofContext.theory (quotdata_update_thy (qty, rty, rel))
 
 fun print_quotdata ctxt =
 let
@@ -179,9 +181,6 @@
   val abs = Const (abs_name, rep_ty --> abs_ty)
   val rep = Const (rep_name, abs_ty --> rep_ty)
 
-  (* storing the quot-info *)
-  (*val _ = quotdata_update (abs_ty, rty, rel) (ProofContext.theory_of lthy)*)
-
   (* ABS and REP definitions *)
   val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT )
   val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT )
@@ -201,14 +200,18 @@
   val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2
   val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
 
+					      
+  (* storing the quot-info *)
+  val lthy3 = quotdata_update (abs_ty, rty, rel) lthy2
+
   (* interpretation *)
   val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
-  val ((_, [eqn1pre]), lthy3) = Variable.import true [ABS_def] lthy2;
+  val ((_, [eqn1pre]), lthy4) = Variable.import true [ABS_def] lthy3;
   val eqn1i = Thm.prop_of (symmetric eqn1pre)
-  val ((_, [eqn2pre]), lthy4) = Variable.import true [REP_def] lthy3;
+  val ((_, [eqn2pre]), lthy5) = Variable.import true [REP_def] lthy4;
   val eqn2i = Thm.prop_of (symmetric eqn2pre)
 
-  val exp_morphism = ProofContext.export_morphism lthy4 (ProofContext.init (ProofContext.theory_of lthy4));
+  val exp_morphism = ProofContext.export_morphism lthy5 (ProofContext.init (ProofContext.theory_of lthy5));
   val exp_term = Morphism.term exp_morphism;
   val exp = Morphism.thm exp_morphism;
 
@@ -219,14 +222,14 @@
   val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true),
     Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))]
 in
-  lthy4
+  lthy5
   |> note (quot_thm_name, quot_thm)
   ||>> note (quotient_thm_name, quotient_thm)
   ||> LocalTheory.theory (fn thy =>
       let
         val global_eqns = map exp_term [eqn2i, eqn1i];
         (* Not sure if the following context should not be used *)
-        val (global_eqns2, lthy5) = Variable.import_terms true global_eqns lthy4;
+        val (global_eqns2, lthy6) = Variable.import_terms true global_eqns lthy5;
         val global_eqns3 = map (fn t => (bindd, t)) global_eqns2;
       in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)
 end