1 (* Title: HOL/Tools/Quotient/quotient_info.ML
2 Author: Cezary Kaliszyk and Christian Urban
4 Context data for the quotient package.
7 signature QUOTIENT_INFO =
9 type quotmaps = {relmap: string}
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
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
21 type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_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
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
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
49 structure Quotient_Info: QUOTIENT_INFO =
52 (** data containers **)
54 (* FIXME just one data slot (record) per program unit *)
56 (* info about map- and rel-functions for a type *)
57 type quotmaps = {relmap: string}
59 structure Quotmaps = Generic_Data
61 type T = quotmaps Symtab.table
62 val empty = Symtab.empty
64 fun merge data = Symtab.merge (K true) data
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
70 (* FIXME export proper internal update operation!? *)
72 val quotmaps_attribute_setup =
73 Attrib.setup @{binding map}
74 ((Args.type_name false --| Scan.lift (@{keyword "="})) -- (* FIXME Args.type_name true (requires "set" type) *)
75 Args.const_proper true >>
76 (fn (tyname, relname) =>
77 let val minfo = {relmap = relname}
78 in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end))
79 "declaration of map information"
81 fun print_quotmaps ctxt =
83 fun prt_map (ty_name, {relmap}) =
84 Pretty.block (separate (Pretty.brk 2)
87 "relation map:", relmap]))
89 map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt)))
90 |> Pretty.big_list "maps for type constructors:"
94 (* info about abs/rep terms *)
95 type abs_rep = {abs : term, rep : term}
97 structure Abs_Rep = Generic_Data
99 type T = abs_rep Symtab.table
100 val empty = Symtab.empty
102 fun merge data = Symtab.merge (K true) data
105 fun transform_abs_rep phi {abs, rep} = {abs = Morphism.term phi abs, rep = Morphism.term phi rep}
107 val lookup_abs_rep = Symtab.lookup o Abs_Rep.get o Context.Proof
108 val lookup_abs_rep_global = Symtab.lookup o Abs_Rep.get o Context.Theory
110 fun update_abs_rep str data = Abs_Rep.map (Symtab.update (str, data))
112 fun print_abs_rep ctxt =
114 fun prt_abs_rep (s, {abs, rep}) =
115 Pretty.block (separate (Pretty.brk 2)
116 [Pretty.str "type constructor:",
118 Pretty.str "abs term:",
119 Syntax.pretty_term ctxt abs,
120 Pretty.str "rep term:",
121 Syntax.pretty_term ctxt rep])
123 map prt_abs_rep (Symtab.dest (Abs_Rep.get (Context.Proof ctxt)))
124 |> Pretty.big_list "abs/rep terms:"
128 (* info about quotient types *)
129 type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
131 structure Quotients = Generic_Data
133 type T = quotients Symtab.table
134 val empty = Symtab.empty
136 fun merge data = Symtab.merge (K true) data
139 fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm} =
140 {qtyp = Morphism.typ phi qtyp,
141 rtyp = Morphism.typ phi rtyp,
142 equiv_rel = Morphism.term phi equiv_rel,
143 equiv_thm = Morphism.thm phi equiv_thm}
145 val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof
146 val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory
148 fun update_quotients str qinfo = Quotients.map (Symtab.update (str, qinfo))
150 fun dest_quotients ctxt = (* FIXME slightly expensive way to retrieve data *)
151 map snd (Symtab.dest (Quotients.get (Context.Proof ctxt)))
153 fun print_quotients ctxt =
155 fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} =
156 Pretty.block (separate (Pretty.brk 2)
157 [Pretty.str "quotient type:",
158 Syntax.pretty_typ ctxt qtyp,
159 Pretty.str "raw type:",
160 Syntax.pretty_typ ctxt rtyp,
161 Pretty.str "relation:",
162 Syntax.pretty_term ctxt equiv_rel,
163 Pretty.str "equiv. thm:",
164 Syntax.pretty_term ctxt (prop_of equiv_thm)])
166 map (prt_quot o snd) (Symtab.dest (Quotients.get (Context.Proof ctxt)))
167 |> Pretty.big_list "quotients:"
172 (* info about quotient constants *)
173 type quotconsts = {qconst: term, rconst: term, def: thm}
175 fun eq_quotconsts (x : quotconsts, y : quotconsts) = #qconst x = #qconst y
177 (* We need to be able to lookup instances of lifted constants,
178 for example given "nat fset" we need to find "'a fset";
179 but overloaded constants share the same name *)
180 structure Quotconsts = Generic_Data
182 type T = quotconsts list Symtab.table
183 val empty = Symtab.empty
185 val merge = Symtab.merge_list eq_quotconsts
188 fun transform_quotconsts phi {qconst, rconst, def} =
189 {qconst = Morphism.term phi qconst,
190 rconst = Morphism.term phi rconst,
191 def = Morphism.thm phi def}
193 fun update_quotconsts name qcinfo = Quotconsts.map (Symtab.cons_list (name, qcinfo))
195 fun dest_quotconsts ctxt =
196 flat (map snd (Symtab.dest (Quotconsts.get (Context.Proof ctxt))))
198 fun dest_quotconsts_global thy =
199 flat (map snd (Symtab.dest (Quotconsts.get (Context.Theory thy))))
203 fun lookup_quotconsts_global thy t =
205 val (name, qty) = dest_Const t
206 fun matches (x: quotconsts) =
207 let val (name', qty') = dest_Const (#qconst x);
208 in name = name' andalso Sign.typ_instance thy (qty, qty') end
210 (case Symtab.lookup (Quotconsts.get (Context.Theory thy)) name of
212 | SOME l => find_first matches l)
215 fun print_quotconsts ctxt =
217 fun prt_qconst {qconst, rconst, def} =
218 Pretty.block (separate (Pretty.brk 1)
219 [Syntax.pretty_term ctxt qconst,
221 Syntax.pretty_term ctxt rconst,
223 Syntax.pretty_term ctxt (prop_of def)])
225 map prt_qconst (maps snd (Symtab.dest (Quotconsts.get (Context.Proof ctxt))))
226 |> Pretty.big_list "quotient constants:"
230 (* equivalence relation theorems *)
231 structure Equiv_Rules = Named_Thms
233 val name = @{binding quot_equiv}
234 val description = "equivalence relation theorems"
237 val equiv_rules = Equiv_Rules.get
238 val equiv_rules_add = Equiv_Rules.add
240 (* respectfulness theorems *)
241 structure Rsp_Rules = Named_Thms
243 val name = @{binding quot_respect}
244 val description = "respectfulness theorems"
247 val rsp_rules = Rsp_Rules.get
248 val rsp_rules_add = Rsp_Rules.add
250 (* preservation theorems *)
251 structure Prs_Rules = Named_Thms
253 val name = @{binding quot_preserve}
254 val description = "preservation theorems"
257 val prs_rules = Prs_Rules.get
258 val prs_rules_add = Prs_Rules.add
260 (* id simplification theorems *)
261 structure Id_Simps = Named_Thms
263 val name = @{binding id_simps}
264 val description = "identity simp rules for maps"
267 val id_simps = Id_Simps.get
269 (* quotient theorems *)
270 structure Quotient_Rules = Named_Thms
272 val name = @{binding quot_thm}
273 val description = "quotient theorems"
276 val quotient_rules = Quotient_Rules.get
277 val quotient_rules_add = Quotient_Rules.add
283 quotmaps_attribute_setup #>
291 (* outer syntax commands *)
294 Outer_Syntax.improper_command "print_quotmaps" "print quotient map functions" Keyword.diag
295 (Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of)))
298 Outer_Syntax.improper_command "print_quotients" "print quotients" Keyword.diag
299 (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
302 Outer_Syntax.improper_command "print_quotconsts" "print quotient constants" Keyword.diag
303 (Scan.succeed (Toplevel.keep (print_quotconsts o Toplevel.context_of)))