--- a/Quot/quotient_info.ML Thu Feb 25 07:48:57 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,293 +0,0 @@
-(* Title: quotient_info.thy
- Author: Cezary Kaliszyk and Christian Urban
-
- Data slots for the quotient package.
-
-*)
-
-
-signature QUOTIENT_INFO =
-sig
- exception NotFound
-
- type maps_info = {mapfun: string, relmap: string}
- val maps_defined: theory -> string -> bool
- val maps_lookup: theory -> string -> maps_info (* raises NotFound *)
- 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 quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
- val transform_quotdata: morphism -> quotdata_info -> quotdata_info
- val quotdata_lookup_raw: theory -> string -> quotdata_info option
- val quotdata_lookup: theory -> string -> quotdata_info (* raises NotFound *)
- val quotdata_update_thy: string -> quotdata_info -> theory -> theory
- val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic
- val quotdata_dest: Proof.context -> quotdata_info list
- val print_quotinfo: Proof.context -> unit
-
- type qconsts_info = {qconst: term, rconst: term, def: thm}
- val transform_qconsts: morphism -> qconsts_info -> qconsts_info
- val qconsts_lookup: theory -> term -> qconsts_info (* raises NotFound *)
- val qconsts_update_thy: string -> qconsts_info -> theory -> theory
- val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic
- val qconsts_dest: Proof.context -> 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 rsp_rules_add: attribute
- val prs_rules_get: Proof.context -> thm list
- val prs_rules_add: attribute
- val id_simps_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 for a type *)
-type maps_info = {mapfun: string, relmap: string}
-
-structure MapsData = Theory_Data
- (type T = maps_info Symtab.table
- val empty = Symtab.empty
- val extend = I
- val merge = Symtab.merge (K true))
-
-fun maps_defined thy s =
- Symtab.defined (MapsData.get thy) s
-
-fun maps_lookup thy s =
- case (Symtab.lookup (MapsData.get thy) s) of
- SOME map_fun => map_fun
- | NONE => raise NotFound
-
-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 _ => 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
-
- fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt; ())
- val _ = List.app sanity_check [mapname, relname]
-in
- maps_attribute_aux tyname {mapfun = mapname, relmap = 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"))
-
-fun print_mapsinfo ctxt =
-let
- fun prt_map (ty_name, {mapfun, relmap}) =
- Pretty.block (Library.separate (Pretty.brk 2)
- (map Pretty.str
- ["type:", ty_name,
- "map:", mapfun,
- "relation map:", relmap]))
-in
- MapsData.get (ProofContext.theory_of ctxt)
- |> Symtab.dest
- |> map (prt_map)
- |> Pretty.big_list "maps for type constructors:"
- |> Pretty.writeln
-end
-
-
-(* info about quotient types *)
-type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
-
-structure QuotData = Theory_Data
- (type T = quotdata_info Symtab.table
- val empty = Symtab.empty
- val extend = I
- val merge = Symtab.merge (K true))
-
-fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_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}
-
-fun quotdata_lookup_raw thy str = Symtab.lookup (QuotData.get thy) str
-
-fun quotdata_lookup thy str =
- case Symtab.lookup (QuotData.get thy) str of
- SOME qinfo => qinfo
- | NONE => raise NotFound
-
-fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo))
-fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I
-
-fun quotdata_dest lthy =
- map snd (Symtab.dest (QuotData.get (ProofContext.theory_of lthy)))
-
-fun print_quotinfo ctxt =
-let
- fun prt_quot {qtyp, rtyp, equiv_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 equiv_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
-
-
-(* info about quotient constants *)
-type qconsts_info = {qconst: term, rconst: term, def: thm}
-
-fun qconsts_info_eq (x : qconsts_info, y : qconsts_info) = #qconst x = #qconst y
-
-(* We need to be able to lookup instances of lifted constants,
- for example given "nat fset" we need to find "'a fset";
- but overloaded constants share the same name *)
-structure QConstsData = Theory_Data
- (type T = (qconsts_info list) Symtab.table
- val empty = Symtab.empty
- val extend = I
- val merge = Symtab.merge_list qconsts_info_eq)
-
-fun transform_qconsts phi {qconst, rconst, def} =
- {qconst = Morphism.term phi qconst,
- rconst = Morphism.term phi rconst,
- def = Morphism.thm phi def}
-
-fun qconsts_update_thy name qcinfo = QConstsData.map (Symtab.cons_list (name, qcinfo))
-fun qconsts_update_gen name qcinfo = Context.mapping (qconsts_update_thy name qcinfo) I
-
-fun qconsts_dest lthy =
- flat (map snd (Symtab.dest (QConstsData.get (ProofContext.theory_of lthy))))
-
-fun qconsts_lookup thy t =
- let
- val (name, qty) = dest_Const t
- fun matches x =
- let
- val (name', qty') = dest_Const (#qconst x);
- in
- name = name' andalso Sign.typ_instance thy (qty, qty')
- end
- in
- case Symtab.lookup (QConstsData.get thy) name of
- NONE => raise NotFound
- | SOME l =>
- (case (find_first matches l) of
- SOME x => x
- | NONE => raise NotFound)
- end
-
-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,
- Pretty.str "as",
- Syntax.pretty_term ctxt (prop_of def)])
-in
- QConstsData.get (ProofContext.theory_of ctxt)
- |> Symtab.dest
- |> map snd
- |> flat
- |> map prt_qconst
- |> Pretty.big_list "quotient constants:"
- |> Pretty.writeln
-end
-
-(* equivalence relation theorems *)
-structure EquivRules = Named_Thms
- (val name = "quot_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 = "quot_respect"
- val description = "Respectfulness theorems.")
-
-val rsp_rules_get = RspRules.get
-val rsp_rules_add = RspRules.add
-
-(* preservation theorems *)
-structure PrsRules = Named_Thms
- (val name = "quot_preserve"
- val description = "Preservation theorems.")
-
-val prs_rules_get = PrsRules.get
-val prs_rules_add = PrsRules.add
-
-(* id simplification theorems *)
-structure IdSimps = Named_Thms
- (val name = "id_simps"
- val description = "Identity simp rules for maps.")
-
-val id_simps_get = IdSimps.get
-
-(* quotient theorems *)
-structure QuotientRules = Named_Thms
- (val name = "quot_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 #>
- PrsRules.setup #>
- IdSimps.setup #>
- QuotientRules.setup))
-
-(* setup of the printing commands *)
-
-fun improper_command (pp_fn, cmd_name, descr_str) =
- OuterSyntax.improper_command cmd_name descr_str
- OuterKeyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))
-
-val _ = map improper_command
- [(print_mapsinfo, "print_maps", "prints out all map functions"),
- (print_quotinfo, "print_quotients", "prints out all quotients"),
- (print_qconstinfo, "print_quotconsts", "prints out all quotient constants")]
-
-
-end; (* structure *)
-