--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/quotient_info.ML Mon Dec 07 14:12:29 2009 +0100
@@ -0,0 +1,204 @@
+signature QUOTIENT_INFO =
+sig
+ exception NotFound
+
+ type maps_info = {mapfun: string, relfun: string}
+ 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
+
+ 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
+
+ type qconsts_info = {qconst: term, rconst: term, def: thm}
+ val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
+ val qconsts_lookup: theory -> string -> qconsts_info
+ val qconsts_update_thy: string -> qconsts_info -> theory -> theory
+ val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic
+ val qconsts_dest: theory -> qconsts_info list
+ val print_qconstinfo: Proof.context -> unit
+
+ val equiv_rules_get: Proof.context -> thm list
+ val equiv_rules_add: attribute
+ val rsp_rules_get: Proof.context -> thm list
+ val quotient_rules_get: Proof.context -> thm list
+ val quotient_rules_add: attribute
+end;
+
+structure Quotient_Info: QUOTIENT_INFO =
+struct
+
+exception NotFound
+
+(* data containers *)
+(*******************)
+
+(* info about map- and rel-functions *)
+type maps_info = {mapfun: string, relfun: string}
+
+structure MapsData = Theory_Data
+ (type T = maps_info Symtab.table
+ val empty = Symtab.empty
+ val extend = I
+ val merge = Symtab.merge (K true))
+
+val maps_lookup = Symtab.lookup o MapsData.get
+
+fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
+fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo)
+
+fun maps_attribute_aux s minfo = Thm.declaration_attribute
+ (fn thm => Context.mapping (maps_update_thy s minfo) (maps_update s minfo))
+
+(* attribute to be used in declare statements *)
+fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) =
+let
+ val thy = ProofContext.theory_of ctxt
+ val tyname = Sign.intern_type thy tystr
+ val mapname = Sign.intern_const thy mapstr
+ val relname = Sign.intern_const thy relstr
+in
+ maps_attribute_aux tyname {mapfun = mapname, relfun = relname}
+end
+
+val maps_attr_parser =
+ Args.context -- Scan.lift
+ ((Args.name --| OuterParse.$$$ "=") --
+ (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," --
+ Args.name --| OuterParse.$$$ ")"))
+
+val _ = Context.>> (Context.map_theory
+ (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute)
+ "declaration of map information"))
+
+
+(* info about quotient types *)
+type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
+
+structure QuotData = Theory_Data
+ (type T = quotient_info Symtab.table
+ val empty = Symtab.empty
+ val extend = I
+ val merge = Symtab.merge (K true))
+
+fun quotdata_lookup_thy thy str =
+ Symtab.lookup (QuotData.get thy) (Sign.intern_type thy str)
+
+val quotdata_lookup = quotdata_lookup_thy o ProofContext.theory_of
+
+fun quotdata_update_thy qty_name (qty, rty, rel, equiv_thm) =
+ QuotData.map (Symtab.update (qty_name, {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}))
+
+fun quotdata_update qty_name (qty, rty, rel, equiv_thm) =
+ ProofContext.theory (quotdata_update_thy qty_name (qty, rty, rel, equiv_thm))
+
+fun quotdata_dest thy =
+ map snd (Symtab.dest (QuotData.get thy))
+
+fun print_quotinfo ctxt =
+let
+ fun prt_quot {qtyp, rtyp, rel, equiv_thm} =
+ Pretty.block (Library.separate (Pretty.brk 2)
+ [Pretty.str "quotient type:",
+ Syntax.pretty_typ ctxt qtyp,
+ Pretty.str "raw type:",
+ Syntax.pretty_typ ctxt rtyp,
+ Pretty.str "relation:",
+ Syntax.pretty_term ctxt rel,
+ Pretty.str "equiv. thm:",
+ Syntax.pretty_term ctxt (prop_of equiv_thm)])
+in
+ QuotData.get (ProofContext.theory_of ctxt)
+ |> Symtab.dest
+ |> map (prt_quot o snd)
+ |> Pretty.big_list "quotients:"
+ |> Pretty.writeln
+end
+
+val _ =
+ OuterSyntax.improper_command "print_quotients" "print out all quotients"
+ OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of)))
+
+
+(* info about quotient constants *)
+type qconsts_info = {qconst: term, rconst: term, def: thm}
+
+structure QConstsData = Theory_Data
+ (type T = qconsts_info Symtab.table
+ val empty = Symtab.empty
+ val extend = I
+ val merge = Symtab.merge (K true))
+
+fun qconsts_transfer phi {qconst, rconst, def} =
+ {qconst = Morphism.term phi qconst,
+ rconst = Morphism.term phi rconst,
+ def = Morphism.thm phi def}
+
+fun qconsts_lookup thy str =
+ case Symtab.lookup (QConstsData.get thy) str of
+ SOME info => info
+ | NONE => raise NotFound
+
+fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo))
+fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I
+
+fun qconsts_dest thy =
+ map snd (Symtab.dest (QConstsData.get thy))
+
+(* We don't print the definition *)
+fun print_qconstinfo ctxt =
+let
+ fun prt_qconst {qconst, rconst, def} =
+ Pretty.block (separate (Pretty.brk 1)
+ [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)))
+
+(* equivalence relation theorems *)
+structure EquivRules = Named_Thms
+ (val name = "quotient_equiv"
+ val description = "Equivalence relation theorems.")
+
+val equiv_rules_get = EquivRules.get
+val equiv_rules_add = EquivRules.add
+
+(* respectfulness theorems *)
+structure RspRules = Named_Thms
+ (val name = "quotient_rsp"
+ val description = "Respectfulness theorems.")
+
+val rsp_rules_get = RspRules.get
+
+(* quotient theorems *)
+structure QuotientRules = Named_Thms
+ (val name = "quotient_thm"
+ val description = "Quotient theorems.")
+
+val quotient_rules_get = QuotientRules.get
+val quotient_rules_add = QuotientRules.add
+
+(* setup of the theorem lists *)
+val _ = Context.>> (Context.map_theory
+ (EquivRules.setup #>
+ RspRules.setup #>
+ QuotientRules.setup))
+
+end; (* structure *)
+
+open Quotient_Info