# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260460563 -3600
# Node ID aa157e957655b62812e709ab28bafd7848a269ff
# Parent  57944c1ef72817b0629f553c93f3d312d48cea9b
added maps-printout and tuned some comments

diff -r 57944c1ef728 -r aa157e957655 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Thu Dec 10 12:25:12 2009 +0100
+++ b/Quot/QuotMain.thy	Thu Dec 10 16:56:03 2009 +0100
@@ -91,6 +91,8 @@
 (* the auxiliary data for the quotient types *)
 use "quotient_info.ML"
 
+ML {* print_mapsinfo @{context} *}
+
 declare [[map "fun" = (fun_map, fun_rel)]]
 
 lemmas [quot_thm] = fun_quotient 
@@ -996,18 +998,18 @@
   end)  
 *}
 
-section {* General Shape of the Lifting Procedure *}
+section {* The General Shape of the Lifting Procedure *}
 
-(* - A is the original raw theorem                  *)
-(* - B is the regularized theorem                   *)
-(* - C is the rep/abs injected version of B         *) 
-(* - D is the lifted theorem                        *)
-(*                                                  *)
-(* - b is the regularization step                   *)
-(* - c is the rep/abs injection step                *)
-(* - d is the cleaning part                         *)
-(*                                                  *)
-(* the QUOT_TRUE premise records the lifted theorem *)
+(* - A is the original raw theorem                       *)
+(* - B is the regularized theorem                        *)
+(* - C is the rep/abs injected version of B              *) 
+(* - D is the lifted theorem                             *)
+(*                                                       *)
+(* - b is the regularization step                        *)
+(* - c is the rep/abs injection step                     *)
+(* - d is the cleaning part                              *)
+(*                                                       *)
+(* the QUOT_TRUE premise in c records the lifted theorem *)
 
 lemma lifting_procedure:
   assumes a: "A"
diff -r 57944c1ef728 -r aa157e957655 Quot/QuotProd.thy
--- a/Quot/QuotProd.thy	Thu Dec 10 12:25:12 2009 +0100
+++ b/Quot/QuotProd.thy	Thu Dec 10 16:56:03 2009 +0100
@@ -26,7 +26,8 @@
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "Quotient (prod_rel R1 R2) (prod_fun Abs1 Abs2) (prod_fun Rep1 Rep2)"
 unfolding Quotient_def
-apply (simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q1] Quotient_rel_rep[OF q2])
+using q1 q2
+apply (simp add: Quotient_abs_rep Quotient_abs_rep Quotient_rel_rep Quotient_rel_rep)
 using Quotient_rel[OF q1] Quotient_rel[OF q2] by blast
 
 lemma pair_rsp:
@@ -41,8 +42,6 @@
   shows "(prod_fun Abs1 Abs2) (Rep1 l, Rep2 r) \<equiv> (l, r)"
   by (simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
 
-term Pair
-
 lemma pair_prs[quot_preserve]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
diff -r 57944c1ef728 -r aa157e957655 Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Thu Dec 10 12:25:12 2009 +0100
+++ b/Quot/quotient_info.ML	Thu Dec 10 16:56:03 2009 +0100
@@ -6,14 +6,15 @@
   val maps_lookup: theory -> string -> maps_info option
   val maps_update_thy: string -> maps_info -> theory -> theory    
   val maps_update: string -> maps_info -> Proof.context -> Proof.context     
+  val print_mapsinfo: Proof.context -> unit
 
   type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
-  val print_quotinfo: Proof.context -> unit
   val quotdata_lookup_thy: theory -> string -> quotient_info option
   val quotdata_lookup: Proof.context -> string -> quotient_info option
   val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory
   val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context
   val quotdata_dest: theory -> quotient_info list
+  val print_quotinfo: Proof.context -> unit
 
   type qconsts_info = {qconst: term, rconst: term, def: thm}
   val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
@@ -81,6 +82,25 @@
          (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) 
            "declaration of map information"))
 
+fun print_mapsinfo ctxt =
+let
+  fun prt_map (ty_name, {mapfun, relfun}) = 
+      Pretty.block (Library.separate (Pretty.brk 2)
+          [Pretty.str "type:", 
+           Pretty.str ty_name,
+           Pretty.str "map fun:", 
+           Pretty.str mapfun,
+           Pretty.str "relation map:", 
+           Pretty.str relfun])
+in
+  MapsData.get (ProofContext.theory_of ctxt)
+  |> Symtab.dest
+  |> map (prt_map)
+  |> Pretty.big_list "maps:" 
+  |> Pretty.writeln
+end
+
+
 
 (* info about quotient types *)
 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}