src/HOL/Tools/Quotient/quotient_info.ML
author wenzelm
Thu Mar 06 13:44:01 2014 +0100 (2014-03-06)
changeset 55954 a29aefc88c8d
parent 55952 2f85cc6c27d4
child 57960 ee1ba4848896
permissions -rw-r--r--
more uniform check_const/read_const;
     1 (*  Title:      HOL/Tools/Quotient/quotient_info.ML
     2     Author:     Cezary Kaliszyk and Christian Urban
     3 
     4 Context data for the quotient package.
     5 *)
     6 
     7 signature QUOTIENT_INFO =
     8 sig
     9   type quotmaps = {relmap: string, quot_thm: thm}
    10   val lookup_quotmaps: Proof.context -> string -> quotmaps option
    11   val lookup_quotmaps_global: theory -> string -> quotmaps option
    12   val print_quotmaps: Proof.context -> unit
    13 
    14   type abs_rep = {abs : term, rep : term}
    15   val transform_abs_rep: morphism -> abs_rep -> abs_rep
    16   val lookup_abs_rep: Proof.context -> string -> abs_rep option
    17   val lookup_abs_rep_global: theory -> string -> abs_rep option
    18   val update_abs_rep: string -> abs_rep -> Context.generic -> Context.generic
    19   val print_abs_rep: Proof.context -> unit
    20   
    21   type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm, quot_thm: thm}
    22   val transform_quotients: morphism -> quotients -> quotients
    23   val lookup_quotients: Proof.context -> string -> quotients option
    24   val lookup_quotients_global: theory -> string -> quotients option
    25   val update_quotients: string -> quotients -> Context.generic -> Context.generic
    26   val dest_quotients: Proof.context -> quotients list
    27   val print_quotients: Proof.context -> unit
    28 
    29   type quotconsts = {qconst: term, rconst: term, def: thm}
    30   val transform_quotconsts: morphism -> quotconsts -> quotconsts
    31   val lookup_quotconsts_global: theory -> term -> quotconsts option
    32   val update_quotconsts: string -> quotconsts -> Context.generic -> Context.generic
    33   val dest_quotconsts_global: theory -> quotconsts list
    34   val dest_quotconsts: Proof.context -> quotconsts list
    35   val print_quotconsts: Proof.context -> unit
    36 
    37   val equiv_rules: Proof.context -> thm list
    38   val equiv_rules_add: attribute
    39   val rsp_rules: Proof.context -> thm list
    40   val rsp_rules_add: attribute
    41   val prs_rules: Proof.context -> thm list
    42   val prs_rules_add: attribute
    43   val id_simps: Proof.context -> thm list
    44   val quotient_rules: Proof.context -> thm list
    45   val quotient_rules_add: attribute
    46   val setup: theory -> theory
    47 end;
    48 
    49 structure Quotient_Info: QUOTIENT_INFO =
    50 struct
    51 
    52 (** data containers **)
    53 
    54 (* FIXME just one data slot (record) per program unit *)
    55 
    56 (* info about map- and rel-functions for a type *)
    57 type quotmaps = {relmap: string, quot_thm: thm}
    58 
    59 structure Quotmaps = Generic_Data
    60 (
    61   type T = quotmaps Symtab.table
    62   val empty = Symtab.empty
    63   val extend = I
    64   fun merge data = Symtab.merge (K true) data
    65 )
    66 
    67 val lookup_quotmaps = Symtab.lookup o Quotmaps.get o Context.Proof
    68 val lookup_quotmaps_global = Symtab.lookup o Quotmaps.get o Context.Theory
    69 
    70 (* FIXME export proper internal update operation!? *)
    71 
    72 val quotmaps_attribute_setup =
    73   Attrib.setup @{binding mapQ3}
    74     ((Args.type_name {proper = true, strict = true} --| Scan.lift @{keyword "="}) --
    75       (Scan.lift @{keyword "("} |--
    76         Args.const {proper = true, strict = true} --| Scan.lift @{keyword ","} --
    77         Attrib.thm --| Scan.lift @{keyword ")"}) >>
    78       (fn (tyname, (relname, qthm)) =>
    79         let val minfo = {relmap = relname, quot_thm = qthm}
    80         in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end))
    81     "declaration of map information"
    82 
    83 fun print_quotmaps ctxt =
    84   let
    85     fun prt_map (ty_name, {relmap, quot_thm}) =
    86       Pretty.block (separate (Pretty.brk 2)
    87          [Pretty.str "type:", 
    88           Pretty.str ty_name,
    89           Pretty.str "relation map:", 
    90           Pretty.str relmap,
    91           Pretty.str "quot. theorem:", 
    92           Syntax.pretty_term ctxt (prop_of quot_thm)])
    93   in
    94     map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt)))
    95     |> Pretty.big_list "maps for type constructors:"
    96     |> Pretty.writeln
    97   end
    98 
    99 (* info about abs/rep terms *)
   100 type abs_rep = {abs : term, rep : term}
   101 
   102 structure Abs_Rep = Generic_Data
   103 (
   104   type T = abs_rep Symtab.table
   105   val empty = Symtab.empty
   106   val extend = I
   107   fun merge data = Symtab.merge (K true) data
   108 )
   109 
   110 fun transform_abs_rep phi {abs, rep} = {abs = Morphism.term phi abs, rep = Morphism.term phi rep}
   111 
   112 val lookup_abs_rep = Symtab.lookup o Abs_Rep.get o Context.Proof
   113 val lookup_abs_rep_global = Symtab.lookup o Abs_Rep.get o Context.Theory
   114 
   115 fun update_abs_rep str data = Abs_Rep.map (Symtab.update (str, data))
   116 
   117 fun print_abs_rep ctxt =
   118   let
   119     fun prt_abs_rep (s, {abs, rep}) =
   120       Pretty.block (separate (Pretty.brk 2)
   121        [Pretty.str "type constructor:",
   122         Pretty.str s,
   123         Pretty.str "abs term:",
   124         Syntax.pretty_term ctxt abs,
   125         Pretty.str "rep term:",
   126         Syntax.pretty_term ctxt rep])
   127   in
   128     map prt_abs_rep (Symtab.dest (Abs_Rep.get (Context.Proof ctxt)))
   129     |> Pretty.big_list "abs/rep terms:"
   130     |> Pretty.writeln
   131   end
   132 
   133 (* info about quotient types *)
   134 type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm, quot_thm: thm}
   135 
   136 structure Quotients = Generic_Data
   137 (
   138   type T = quotients Symtab.table
   139   val empty = Symtab.empty
   140   val extend = I
   141   fun merge data = Symtab.merge (K true) data
   142 )
   143 
   144 fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} =
   145   {qtyp = Morphism.typ phi qtyp,
   146    rtyp = Morphism.typ phi rtyp,
   147    equiv_rel = Morphism.term phi equiv_rel,
   148    equiv_thm = Morphism.thm phi equiv_thm,
   149    quot_thm = Morphism.thm phi quot_thm}
   150 
   151 val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof
   152 val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory
   153 
   154 fun update_quotients str qinfo = Quotients.map (Symtab.update (str, qinfo))
   155 
   156 fun dest_quotients ctxt =  (* FIXME slightly expensive way to retrieve data *)
   157   map snd (Symtab.dest (Quotients.get (Context.Proof ctxt)))
   158 
   159 fun print_quotients ctxt =
   160   let
   161     fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} =
   162       Pretty.block (separate (Pretty.brk 2)
   163        [Pretty.str "quotient type:",
   164         Syntax.pretty_typ ctxt qtyp,
   165         Pretty.str "raw type:",
   166         Syntax.pretty_typ ctxt rtyp,
   167         Pretty.str "relation:",
   168         Syntax.pretty_term ctxt equiv_rel,
   169         Pretty.str "equiv. thm:",
   170         Syntax.pretty_term ctxt (prop_of equiv_thm),
   171         Pretty.str "quot. thm:",
   172         Syntax.pretty_term ctxt (prop_of quot_thm)])
   173   in
   174     map (prt_quot o snd) (Symtab.dest (Quotients.get (Context.Proof ctxt)))
   175     |> Pretty.big_list "quotients:"
   176     |> Pretty.writeln
   177   end
   178 
   179 
   180 (* info about quotient constants *)
   181 type quotconsts = {qconst: term, rconst: term, def: thm}
   182 
   183 fun eq_quotconsts (x : quotconsts, y : quotconsts) = #qconst x = #qconst y
   184 
   185 (* We need to be able to lookup instances of lifted constants,
   186    for example given "nat fset" we need to find "'a fset";
   187    but overloaded constants share the same name *)
   188 structure Quotconsts = Generic_Data
   189 (
   190   type T = quotconsts list Symtab.table
   191   val empty = Symtab.empty
   192   val extend = I
   193   val merge = Symtab.merge_list eq_quotconsts
   194 )
   195 
   196 fun transform_quotconsts phi {qconst, rconst, def} =
   197   {qconst = Morphism.term phi qconst,
   198    rconst = Morphism.term phi rconst,
   199    def = Morphism.thm phi def}
   200 
   201 fun update_quotconsts name qcinfo = Quotconsts.map (Symtab.cons_list (name, qcinfo))
   202 
   203 fun dest_quotconsts ctxt =
   204   flat (map snd (Symtab.dest (Quotconsts.get (Context.Proof ctxt))))
   205 
   206 fun dest_quotconsts_global thy =
   207   flat (map snd (Symtab.dest (Quotconsts.get (Context.Theory thy))))
   208 
   209 
   210 
   211 fun lookup_quotconsts_global thy t =
   212   let
   213     val (name, qty) = dest_Const t
   214     fun matches (x: quotconsts) =
   215       let val (name', qty') = dest_Const (#qconst x);
   216       in name = name' andalso Sign.typ_instance thy (qty, qty') end
   217   in
   218     (case Symtab.lookup (Quotconsts.get (Context.Theory thy)) name of
   219       NONE => NONE
   220     | SOME l => find_first matches l)
   221   end
   222 
   223 fun print_quotconsts ctxt =
   224   let
   225     fun prt_qconst {qconst, rconst, def} =
   226       Pretty.block (separate (Pretty.brk 1)
   227        [Syntax.pretty_term ctxt qconst,
   228         Pretty.str ":=",
   229         Syntax.pretty_term ctxt rconst,
   230         Pretty.str "as",
   231         Syntax.pretty_term ctxt (prop_of def)])
   232   in
   233     map prt_qconst (maps snd (Symtab.dest (Quotconsts.get (Context.Proof ctxt))))
   234     |> Pretty.big_list "quotient constants:"
   235     |> Pretty.writeln
   236   end
   237 
   238 (* equivalence relation theorems *)
   239 structure Equiv_Rules = Named_Thms
   240 (
   241   val name = @{binding quot_equiv}
   242   val description = "equivalence relation theorems"
   243 )
   244 
   245 val equiv_rules = Equiv_Rules.get
   246 val equiv_rules_add = Equiv_Rules.add
   247 
   248 (* respectfulness theorems *)
   249 structure Rsp_Rules = Named_Thms
   250 (
   251   val name = @{binding quot_respect}
   252   val description = "respectfulness theorems"
   253 )
   254 
   255 val rsp_rules = Rsp_Rules.get
   256 val rsp_rules_add = Rsp_Rules.add
   257 
   258 (* preservation theorems *)
   259 structure Prs_Rules = Named_Thms
   260 (
   261   val name = @{binding quot_preserve}
   262   val description = "preservation theorems"
   263 )
   264 
   265 val prs_rules = Prs_Rules.get
   266 val prs_rules_add = Prs_Rules.add
   267 
   268 (* id simplification theorems *)
   269 structure Id_Simps = Named_Thms
   270 (
   271   val name = @{binding id_simps}
   272   val description = "identity simp rules for maps"
   273 )
   274 
   275 val id_simps = Id_Simps.get
   276 
   277 (* quotient theorems *)
   278 structure Quotient_Rules = Named_Thms
   279 (
   280   val name = @{binding quot_thm}
   281   val description = "quotient theorems"
   282 )
   283 
   284 val quotient_rules = Quotient_Rules.get
   285 val quotient_rules_add = Quotient_Rules.add
   286 
   287 
   288 (* theory setup *)
   289 
   290 val setup =
   291   quotmaps_attribute_setup #>
   292   Equiv_Rules.setup #>
   293   Rsp_Rules.setup #>
   294   Prs_Rules.setup #>
   295   Id_Simps.setup #>
   296   Quotient_Rules.setup
   297 
   298 
   299 (* outer syntax commands *)
   300 
   301 val _ =
   302   Outer_Syntax.improper_command @{command_spec "print_quotmapsQ3"} "print quotient map functions"
   303     (Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of)))
   304 
   305 val _ =
   306   Outer_Syntax.improper_command @{command_spec "print_quotientsQ3"} "print quotients"
   307     (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
   308 
   309 val _ =
   310   Outer_Syntax.improper_command @{command_spec "print_quotconsts"} "print quotient constants"
   311     (Scan.succeed (Toplevel.keep (print_quotconsts o Toplevel.context_of)))
   312 
   313 end;