1 (*  Title:      quotient_info.thy

     2     Author:     Cezary Kaliszyk and Christian Urban

     3 

     4     Data slots for the quotient package.

     5 

     6 *)

     7 

     8 

     9 signature QUOTIENT_INFO =

    10 sig

    11   exception NotFound

    12 

    13   type maps_info = {mapfun: string, relmap: string}

    14   val maps_defined: theory -> string -> bool

    15   val maps_lookup: theory -> string -> maps_info     (* raises NotFound *)

    16   val maps_update_thy: string -> maps_info -> theory -> theory

    17   val maps_update: string -> maps_info -> Proof.context -> Proof.context

    18   val print_mapsinfo: Proof.context -> unit

    19 

    20   type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}

    21   val transform_quotdata: morphism -> quotdata_info -> quotdata_info

    22   val quotdata_lookup_raw: theory -> string -> quotdata_info option

    23   val quotdata_lookup: theory -> string -> quotdata_info     (* raises NotFound *)

    24   val quotdata_update_thy: string -> quotdata_info -> theory -> theory

    25   val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic

    26   val quotdata_dest: Proof.context -> quotdata_info list

    27   val print_quotinfo: Proof.context -> unit

    28 

    29   type qconsts_info = {qconst: term, rconst: term, def: thm}

    30   val transform_qconsts: morphism -> qconsts_info -> qconsts_info

    31   val qconsts_lookup: theory -> term -> qconsts_info     (* raises NotFound *)

    32   val qconsts_update_thy: string -> qconsts_info -> theory -> theory

    33   val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic

    34   val qconsts_dest: Proof.context -> qconsts_info list

    35   val print_qconstinfo: Proof.context -> unit

    36 

    37   val equiv_rules_get: Proof.context -> thm list

    38   val equiv_rules_add: attribute

    39   val rsp_rules_get: Proof.context -> thm list

    40   val rsp_rules_add: attribute

    41   val prs_rules_get: Proof.context -> thm list

    42   val prs_rules_add: attribute

    43   val id_simps_get: Proof.context -> thm list

    44   val quotient_rules_get: Proof.context -> thm list

    45   val quotient_rules_add: attribute

    46 end;

    47 

    48 

    49 structure Quotient_Info: QUOTIENT_INFO =

    50 struct

    51 

    52 exception NotFound

    53 

    54 

    55 (** data containers **)

    56 

    57 (* info about map- and rel-functions for a type *)

    58 type maps_info = {mapfun: string, relmap: string}

    59 

    60 structure MapsData = Theory_Data

    61   (type T = maps_info Symtab.table

    62    val empty = Symtab.empty

    63    val extend = I

    64    val merge = Symtab.merge (K true))

    65 

    66 fun maps_defined thy s =

    67   Symtab.defined (MapsData.get thy) s

    68 

    69 fun maps_lookup thy s =

    70   case (Symtab.lookup (MapsData.get thy) s) of

    71     SOME map_fun => map_fun

    72   | NONE => raise NotFound

    73 

    74 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))

    75 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo)

    76 

    77 fun maps_attribute_aux s minfo = Thm.declaration_attribute

    78   (fn _ => Context.mapping (maps_update_thy s minfo) (maps_update s minfo))

    79 

    80 (* attribute to be used in declare statements *)

    81 fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) =

    82 let

    83   val thy = ProofContext.theory_of ctxt

    84   val tyname = Sign.intern_type thy tystr

    85   val mapname = Sign.intern_const thy mapstr

    86   val relname = Sign.intern_const thy relstr

    87 

    88   fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt; ())

    89   val _ = List.app sanity_check [mapname, relname]

    90 in

    91   maps_attribute_aux tyname {mapfun = mapname, relmap = relname}

    92 end

    93 

    94 val maps_attr_parser =

    95   Args.context -- Scan.lift

    96     ((Args.name --| OuterParse.$$$ "=") --

    97       (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," --

    98         Args.name --| OuterParse.$$$ ")"))

    99 

   100 val _ = Context.>> (Context.map_theory

   101   (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute)

   102     "declaration of map information"))

   103 

   104 fun print_mapsinfo ctxt =

   105 let

   106   fun prt_map (ty_name, {mapfun, relmap}) =

   107     Pretty.block (Library.separate (Pretty.brk 2)

   108       (map Pretty.str

   109         ["type:", ty_name,

   110         "map:", mapfun,

   111         "relation map:", relmap]))

   112 in

   113   MapsData.get (ProofContext.theory_of ctxt)

   114   |> Symtab.dest

   115   |> map (prt_map)

   116   |> Pretty.big_list "maps for type constructors:"

   117   |> Pretty.writeln

   118 end

   119 

   120 

   121 (* info about quotient types *)

   122 type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}

   123 

   124 structure QuotData = Theory_Data

   125   (type T = quotdata_info Symtab.table

   126    val empty = Symtab.empty

   127    val extend = I

   128    val merge = Symtab.merge (K true))

   129 

   130 fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} =

   131   {qtyp = Morphism.typ phi qtyp,

   132    rtyp = Morphism.typ phi rtyp,

   133    equiv_rel = Morphism.term phi equiv_rel,

   134    equiv_thm = Morphism.thm phi equiv_thm}

   135 

   136 fun quotdata_lookup_raw thy str = Symtab.lookup (QuotData.get thy) str

   137 

   138 fun quotdata_lookup thy str =

   139   case Symtab.lookup (QuotData.get thy) str of

   140     SOME qinfo => qinfo

   141   | NONE => raise NotFound

   142 

   143 fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo))

   144 fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I

   145 

   146 fun quotdata_dest lthy =

   147   map snd (Symtab.dest (QuotData.get (ProofContext.theory_of lthy)))

   148 

   149 fun print_quotinfo ctxt =

   150 let

   151   fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} =

   152     Pretty.block (Library.separate (Pretty.brk 2)

   153      [Pretty.str "quotient type:",

   154       Syntax.pretty_typ ctxt qtyp,

   155       Pretty.str "raw type:",

   156       Syntax.pretty_typ ctxt rtyp,

   157       Pretty.str "relation:",

   158       Syntax.pretty_term ctxt equiv_rel,

   159       Pretty.str "equiv. thm:",

   160       Syntax.pretty_term ctxt (prop_of equiv_thm)])

   161 in

   162   QuotData.get (ProofContext.theory_of ctxt)

   163   |> Symtab.dest

   164   |> map (prt_quot o snd)

   165   |> Pretty.big_list "quotients:"

   166   |> Pretty.writeln

   167 end

   168 

   169 

   170 (* info about quotient constants *)

   171 type qconsts_info = {qconst: term, rconst: term, def: thm}

   172 

   173 fun qconsts_info_eq (x : qconsts_info, y : qconsts_info) = #qconst x = #qconst y

   174 

   175 (* We need to be able to lookup instances of lifted constants,

   176    for example given "nat fset" we need to find "'a fset";

   177    but overloaded constants share the same name *)

   178 structure QConstsData = Theory_Data

   179   (type T = (qconsts_info list) Symtab.table

   180    val empty = Symtab.empty

   181    val extend = I

   182    val merge = Symtab.merge_list qconsts_info_eq)

   183 

   184 fun transform_qconsts phi {qconst, rconst, def} =

   185   {qconst = Morphism.term phi qconst,

   186    rconst = Morphism.term phi rconst,

   187    def = Morphism.thm phi def}

   188 

   189 fun qconsts_update_thy name qcinfo = QConstsData.map (Symtab.cons_list (name, qcinfo))

   190 fun qconsts_update_gen name qcinfo = Context.mapping (qconsts_update_thy name qcinfo) I

   191 

   192 fun qconsts_dest lthy =

   193   flat (map snd (Symtab.dest (QConstsData.get (ProofContext.theory_of lthy))))

   194 

   195 fun qconsts_lookup thy t =

   196   let

   197     val (name, qty) = dest_Const t

   198     fun matches x =

   199       let

   200         val (name', qty') = dest_Const (#qconst x);

   201       in

   202         name = name' andalso Sign.typ_instance thy (qty, qty')

   203       end

   204   in

   205     case Symtab.lookup (QConstsData.get thy) name of

   206       NONE => raise NotFound

   207     | SOME l =>

   208       (case (find_first matches l) of

   209         SOME x => x

   210       | NONE => raise NotFound)

   211   end

   212 

   213 fun print_qconstinfo ctxt =

   214 let

   215   fun prt_qconst {qconst, rconst, def} =

   216     Pretty.block (separate (Pretty.brk 1)

   217      [Syntax.pretty_term ctxt qconst,

   218       Pretty.str ":=",

   219       Syntax.pretty_term ctxt rconst,

   220       Pretty.str "as",

   221       Syntax.pretty_term ctxt (prop_of def)])

   222 in

   223   QConstsData.get (ProofContext.theory_of ctxt)

   224   |> Symtab.dest

   225   |> map snd

   226   |> flat

   227   |> map prt_qconst

   228   |> Pretty.big_list "quotient constants:"

   229   |> Pretty.writeln

   230 end

   231 

   232 (* equivalence relation theorems *)

   233 structure EquivRules = Named_Thms

   234   (val name = "quot_equiv"

   235    val description = "Equivalence relation theorems.")

   236 

   237 val equiv_rules_get = EquivRules.get

   238 val equiv_rules_add = EquivRules.add

   239 

   240 (* respectfulness theorems *)

   241 structure RspRules = Named_Thms

   242   (val name = "quot_respect"

   243    val description = "Respectfulness theorems.")

   244 

   245 val rsp_rules_get = RspRules.get

   246 val rsp_rules_add = RspRules.add

   247 

   248 (* preservation theorems *)

   249 structure PrsRules = Named_Thms

   250   (val name = "quot_preserve"

   251    val description = "Preservation theorems.")

   252 

   253 val prs_rules_get = PrsRules.get

   254 val prs_rules_add = PrsRules.add

   255 

   256 (* id simplification theorems *)

   257 structure IdSimps = Named_Thms

   258   (val name = "id_simps"

   259    val description = "Identity simp rules for maps.")

   260 

   261 val id_simps_get = IdSimps.get

   262 

   263 (* quotient theorems *)

   264 structure QuotientRules = Named_Thms

   265   (val name = "quot_thm"

   266    val description = "Quotient theorems.")

   267 

   268 val quotient_rules_get = QuotientRules.get

   269 val quotient_rules_add = QuotientRules.add

   270 

   271 (* setup of the theorem lists *)

   272 

   273 val _ = Context.>> (Context.map_theory

   274   (EquivRules.setup #>

   275    RspRules.setup #>

   276    PrsRules.setup #>

   277    IdSimps.setup #>

   278    QuotientRules.setup))

   279 

   280 (* setup of the printing commands *)

   281 

   282 fun improper_command (pp_fn, cmd_name, descr_str) =

   283   OuterSyntax.improper_command cmd_name descr_str

   284     OuterKeyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))

   285 

   286 val _ = map improper_command

   287   [(print_mapsinfo, "print_maps", "prints out all map functions"),

   288    (print_quotinfo, "print_quotients", "prints out all quotients"),

   289    (print_qconstinfo, "print_quotconsts", "prints out all quotient constants")]

   290 

   291 

   292 end; (* structure *)

   293