--- a/quotient_info.ML Mon Dec 07 14:09:50 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,204 +0,0 @@
-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