--- a/src/HOL/Tools/Quotient/quotient_info.ML Fri Mar 23 20:32:43 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Mon Mar 26 10:56:56 2012 +0200
@@ -6,7 +6,7 @@
signature QUOTIENT_INFO =
sig
- type quotmaps = {relmap: string}
+ type quotmaps = {relmap: string, quot_thm: thm}
val lookup_quotmaps: Proof.context -> string -> quotmaps option
val lookup_quotmaps_global: theory -> string -> quotmaps option
val print_quotmaps: Proof.context -> unit
@@ -18,7 +18,7 @@
val update_abs_rep: string -> abs_rep -> Context.generic -> Context.generic
val print_abs_rep: Proof.context -> unit
- type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
+ type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm, quot_thm: thm}
val transform_quotients: morphism -> quotients -> quotients
val lookup_quotients: Proof.context -> string -> quotients option
val lookup_quotients_global: theory -> string -> quotients option
@@ -54,7 +54,7 @@
(* FIXME just one data slot (record) per program unit *)
(* info about map- and rel-functions for a type *)
-type quotmaps = {relmap: string}
+type quotmaps = {relmap: string, quot_thm: thm}
structure Quotmaps = Generic_Data
(
@@ -71,19 +71,24 @@
val quotmaps_attribute_setup =
Attrib.setup @{binding map}
- ((Args.type_name true --| Scan.lift @{keyword "="}) -- Args.const_proper true >>
- (fn (tyname, relname) =>
- let val minfo = {relmap = relname}
+ ((Args.type_name true --| Scan.lift @{keyword "="}) --
+ (Scan.lift @{keyword "("} |-- Args.const_proper true --| Scan.lift @{keyword ","} --
+ Attrib.thm --| Scan.lift @{keyword ")"}) >>
+ (fn (tyname, (relname, qthm)) =>
+ let val minfo = {relmap = relname, quot_thm = qthm}
in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end))
"declaration of map information"
fun print_quotmaps ctxt =
let
- fun prt_map (ty_name, {relmap}) =
+ fun prt_map (ty_name, {relmap, quot_thm}) =
Pretty.block (separate (Pretty.brk 2)
- (map Pretty.str
- ["type:", ty_name,
- "relation map:", relmap]))
+ [Pretty.str "type:",
+ Pretty.str ty_name,
+ Pretty.str "relation map:",
+ Pretty.str relmap,
+ Pretty.str "quot. theorem:",
+ Syntax.pretty_term ctxt (prop_of quot_thm)])
in
map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt)))
|> Pretty.big_list "maps for type constructors:"
@@ -125,7 +130,7 @@
end
(* info about quotient types *)
-type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
+type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm, quot_thm: thm}
structure Quotients = Generic_Data
(
@@ -135,11 +140,12 @@
fun merge data = Symtab.merge (K true) data
)
-fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm} =
+fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} =
{qtyp = Morphism.typ phi qtyp,
rtyp = Morphism.typ phi rtyp,
equiv_rel = Morphism.term phi equiv_rel,
- equiv_thm = Morphism.thm phi equiv_thm}
+ equiv_thm = Morphism.thm phi equiv_thm,
+ quot_thm = Morphism.thm phi quot_thm}
val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof
val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory
@@ -151,7 +157,7 @@
fun print_quotients ctxt =
let
- fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} =
+ fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} =
Pretty.block (separate (Pretty.brk 2)
[Pretty.str "quotient type:",
Syntax.pretty_typ ctxt qtyp,
@@ -160,7 +166,9 @@
Pretty.str "relation:",
Syntax.pretty_term ctxt equiv_rel,
Pretty.str "equiv. thm:",
- Syntax.pretty_term ctxt (prop_of equiv_thm)])
+ Syntax.pretty_term ctxt (prop_of equiv_thm),
+ Pretty.str "quot. thm:",
+ Syntax.pretty_term ctxt (prop_of quot_thm)])
in
map (prt_quot o snd) (Symtab.dest (Quotients.get (Context.Proof ctxt)))
|> Pretty.big_list "quotients:"