# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1257988716 -3600
# Node ID fec6301a19899e86f69f9f4f0912fe2da31dd591
# Parent  20fa8dd8fb93102011a359e2cf1ba311016e53a8
added a container for quotient constants (does not work yet though)

diff -r 20fa8dd8fb93 -r fec6301a1989 IntEx.thy
--- a/IntEx.thy	Wed Nov 11 22:30:43 2009 +0100
+++ b/IntEx.thy	Thu Nov 12 02:18:36 2009 +0100
@@ -109,6 +109,10 @@
 where
  "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"
 
+ML {* print_qconstinfo @{context} *}
+
+ML {* print_qconstinfo @{context} *}
+
 lemma plus_sym_pre:
   shows "my_plus a b \<approx> my_plus b a"
   apply(cases a)
diff -r 20fa8dd8fb93 -r fec6301a1989 QuotMain.thy
--- a/QuotMain.thy	Wed Nov 11 22:30:43 2009 +0100
+++ b/QuotMain.thy	Thu Nov 12 02:18:36 2009 +0100
@@ -137,7 +137,6 @@
 
 end
 
-
 section {* type definition for the quotient type *}
 
 (* the auxiliary data for the quotient types *)
@@ -160,6 +159,8 @@
 (* lifting of constants *)
 use "quotient_def.ML"
 
+
+
 section {* ATOMIZE *}
 
 lemma atomize_eqv[atomize]: 
diff -r 20fa8dd8fb93 -r fec6301a1989 quotient_def.ML
--- a/quotient_def.ML	Wed Nov 11 22:30:43 2009 +0100
+++ b/quotient_def.ML	Thu Nov 12 02:18:36 2009 +0100
@@ -135,8 +135,14 @@
 
   val absrep_trm = (fold_rev mk_fun_map rep_fns abs_fn $ rhs)
                    |> Syntax.check_term lthy 
+
+  val ((trm, thm), lthy') = define nconst_bname mx attr absrep_trm lthy
+
+  val nconst_str = Binding.str_of nconst_bname
+  val qc_info = {qconst = trm, rconst = rhs}
+  val lthy'' = qconsts_update nconst_str qc_info lthy'
 in
-  define nconst_bname mx attr absrep_trm lthy
+  ((trm, thm), lthy'')
 end
 
 (* interface and syntax setup *)
diff -r 20fa8dd8fb93 -r fec6301a1989 quotient_info.ML
--- a/quotient_info.ML	Wed Nov 11 22:30:43 2009 +0100
+++ b/quotient_info.ML	Thu Nov 12 02:18:36 2009 +0100
@@ -6,7 +6,7 @@
   val maps_update: string -> maps_info -> Proof.context -> Proof.context     
 
   type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
-  val print_quotdata: Proof.context -> unit
+  val print_quotinfo: Proof.context -> unit
   val quotdata_lookup_thy: theory -> quotient_info list
   val quotdata_lookup: Proof.context -> quotient_info list
   val quotdata_update_thy: (typ * typ * term * thm) -> theory -> theory
@@ -15,6 +15,12 @@
   type qenv = (typ * typ) list
   val mk_qenv: Proof.context -> qenv
   val lookup_qenv: ((typ * typ) -> bool) -> qenv -> typ -> (typ * typ) option
+
+  type qconsts_info = {qconst: term, rconst: term}
+  val qconsts_lookup: theory -> string -> qconsts_info option
+  val qconsts_update_thy: string -> qconsts_info -> theory -> theory    
+  val qconsts_update: string -> qconsts_info -> Proof.context -> Proof.context 
+  val print_qconstinfo: Proof.context -> unit
 end;
 
 structure Quotient_Info: QUOTIENT_INFO =
@@ -82,7 +88,7 @@
 fun quotdata_update (qty, rty, rel, equiv_thm) ctxt = 
       ProofContext.theory (quotdata_update_thy (qty, rty, rel, equiv_thm)) ctxt
 
-fun print_quotdata ctxt =
+fun print_quotinfo ctxt =
 let
   fun prt_quot {qtyp, rtyp, rel, equiv_thm} = 
       Pretty.block (Library.separate (Pretty.brk 2)
@@ -103,7 +109,7 @@
 
 val _ = 
   OuterSyntax.improper_command "print_quotients" "print out all quotients" 
-    OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotdata o Toplevel.context_of)))
+    OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of)))
 
 
 (* environments of quotient and raw types *)
@@ -121,6 +127,40 @@
       if eq (qty', qty) then SOME (qty, rty)
       else lookup_qenv eq xs qty'
 
+(* information about quotient constants *)
+type qconsts_info = {qconst: term, rconst: term}
+
+structure QConstsData = Theory_Data
+  (type T = qconsts_info Symtab.table
+   val empty = Symtab.empty
+   val extend = I
+   val merge = Symtab.merge (K true))
+
+val qconsts_lookup = Symtab.lookup o QConstsData.get
+
+fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo))
+fun qconsts_update k qcinfo = ProofContext.theory (qconsts_update_thy k qcinfo)
+
+fun print_qconstinfo ctxt =
+let
+  fun prt_qconst {qconst, rconst} = 
+      Pretty.block (Library.separate (Pretty.brk 2)
+          [Syntax.pretty_term ctxt qconst,
+           Pretty.str (" := "),
+           Syntax.pretty_term ctxt rconst])
+in
+  QConstsData.get (ProofContext.theory_of ctxt)
+  |> Symtab.dest
+  |> map (prt_qconst o snd)
+  |> Pretty.big_list "quotient constants:" 
+  |> Pretty.writeln
+end
+
+val _ = 
+  OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" 
+    OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of)))
+
+
 end; (* structure *)
 
 open Quotient_Info
\ No newline at end of file