1 (* Title: HOL/Tools/Quotient/quotient_info.thy |
|
2 Author: Cezary Kaliszyk and Christian Urban |
|
3 |
|
4 Data slots for the quotient package. |
|
5 *) |
|
6 |
|
7 signature QUOTIENT_INFO = |
|
8 sig |
|
9 exception NotFound |
|
10 |
|
11 type maps_info = {mapfun: string, relmap: string} |
|
12 val maps_defined: theory -> string -> bool |
|
13 val maps_lookup: theory -> string -> maps_info (* raises NotFound *) |
|
14 val maps_update_thy: string -> maps_info -> theory -> theory |
|
15 val maps_update: string -> maps_info -> Proof.context -> Proof.context |
|
16 val print_mapsinfo: Proof.context -> unit |
|
17 |
|
18 type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} |
|
19 val transform_quotdata: morphism -> quotdata_info -> quotdata_info |
|
20 val quotdata_lookup_raw: theory -> string -> quotdata_info option |
|
21 val quotdata_lookup: theory -> string -> quotdata_info (* raises NotFound *) |
|
22 val quotdata_update_thy: string -> quotdata_info -> theory -> theory |
|
23 val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic |
|
24 val quotdata_dest: Proof.context -> quotdata_info list |
|
25 val print_quotinfo: Proof.context -> unit |
|
26 |
|
27 type qconsts_info = {qconst: term, rconst: term, def: thm} |
|
28 val transform_qconsts: morphism -> qconsts_info -> qconsts_info |
|
29 val qconsts_lookup: theory -> term -> qconsts_info (* raises NotFound *) |
|
30 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
|
31 val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
|
32 val qconsts_dest: Proof.context -> qconsts_info list |
|
33 val print_qconstinfo: Proof.context -> unit |
|
34 |
|
35 val equiv_rules_get: Proof.context -> thm list |
|
36 val equiv_rules_add: attribute |
|
37 val rsp_rules_get: Proof.context -> thm list |
|
38 val rsp_rules_add: attribute |
|
39 val prs_rules_get: Proof.context -> thm list |
|
40 val prs_rules_add: attribute |
|
41 val id_simps_get: Proof.context -> thm list |
|
42 val quotient_rules_get: Proof.context -> thm list |
|
43 val quotient_rules_add: attribute |
|
44 end; |
|
45 |
|
46 |
|
47 structure Quotient_Info: QUOTIENT_INFO = |
|
48 struct |
|
49 |
|
50 exception NotFound |
|
51 |
|
52 |
|
53 (** data containers **) |
|
54 |
|
55 (* info about map- and rel-functions for a type *) |
|
56 type maps_info = {mapfun: string, relmap: string} |
|
57 |
|
58 structure MapsData = Theory_Data |
|
59 (type T = maps_info Symtab.table |
|
60 val empty = Symtab.empty |
|
61 val extend = I |
|
62 fun merge data = Symtab.merge (K true) data) |
|
63 |
|
64 fun maps_defined thy s = |
|
65 Symtab.defined (MapsData.get thy) s |
|
66 |
|
67 fun maps_lookup thy s = |
|
68 case (Symtab.lookup (MapsData.get thy) s) of |
|
69 SOME map_fun => map_fun |
|
70 | NONE => raise NotFound |
|
71 |
|
72 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) |
|
73 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) |
|
74 |
|
75 fun maps_attribute_aux s minfo = Thm.declaration_attribute |
|
76 (fn _ => Context.mapping (maps_update_thy s minfo) (maps_update s minfo)) |
|
77 |
|
78 (* attribute to be used in declare statements *) |
|
79 fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) = |
|
80 let |
|
81 val thy = ProofContext.theory_of ctxt |
|
82 val tyname = Sign.intern_type thy tystr |
|
83 val mapname = Sign.intern_const thy mapstr |
|
84 val relname = Sign.intern_const thy relstr |
|
85 |
|
86 fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt; ()) |
|
87 val _ = List.app sanity_check [mapname, relname] |
|
88 in |
|
89 maps_attribute_aux tyname {mapfun = mapname, relmap = relname} |
|
90 end |
|
91 |
|
92 val maps_attr_parser = |
|
93 Args.context -- Scan.lift |
|
94 ((Args.name --| OuterParse.$$$ "=") -- |
|
95 (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," -- |
|
96 Args.name --| OuterParse.$$$ ")")) |
|
97 |
|
98 val _ = Context.>> (Context.map_theory |
|
99 (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) |
|
100 "declaration of map information")) |
|
101 |
|
102 fun print_mapsinfo ctxt = |
|
103 let |
|
104 fun prt_map (ty_name, {mapfun, relmap}) = |
|
105 Pretty.block (Library.separate (Pretty.brk 2) |
|
106 (map Pretty.str |
|
107 ["type:", ty_name, |
|
108 "map:", mapfun, |
|
109 "relation map:", relmap])) |
|
110 in |
|
111 MapsData.get (ProofContext.theory_of ctxt) |
|
112 |> Symtab.dest |
|
113 |> map (prt_map) |
|
114 |> Pretty.big_list "maps for type constructors:" |
|
115 |> Pretty.writeln |
|
116 end |
|
117 |
|
118 |
|
119 (* info about quotient types *) |
|
120 type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} |
|
121 |
|
122 structure QuotData = Theory_Data |
|
123 (type T = quotdata_info Symtab.table |
|
124 val empty = Symtab.empty |
|
125 val extend = I |
|
126 fun merge data = Symtab.merge (K true) data) |
|
127 |
|
128 fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} = |
|
129 {qtyp = Morphism.typ phi qtyp, |
|
130 rtyp = Morphism.typ phi rtyp, |
|
131 equiv_rel = Morphism.term phi equiv_rel, |
|
132 equiv_thm = Morphism.thm phi equiv_thm} |
|
133 |
|
134 fun quotdata_lookup_raw thy str = Symtab.lookup (QuotData.get thy) str |
|
135 |
|
136 fun quotdata_lookup thy str = |
|
137 case Symtab.lookup (QuotData.get thy) str of |
|
138 SOME qinfo => qinfo |
|
139 | NONE => raise NotFound |
|
140 |
|
141 fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo)) |
|
142 fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I |
|
143 |
|
144 fun quotdata_dest lthy = |
|
145 map snd (Symtab.dest (QuotData.get (ProofContext.theory_of lthy))) |
|
146 |
|
147 fun print_quotinfo ctxt = |
|
148 let |
|
149 fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} = |
|
150 Pretty.block (Library.separate (Pretty.brk 2) |
|
151 [Pretty.str "quotient type:", |
|
152 Syntax.pretty_typ ctxt qtyp, |
|
153 Pretty.str "raw type:", |
|
154 Syntax.pretty_typ ctxt rtyp, |
|
155 Pretty.str "relation:", |
|
156 Syntax.pretty_term ctxt equiv_rel, |
|
157 Pretty.str "equiv. thm:", |
|
158 Syntax.pretty_term ctxt (prop_of equiv_thm)]) |
|
159 in |
|
160 QuotData.get (ProofContext.theory_of ctxt) |
|
161 |> Symtab.dest |
|
162 |> map (prt_quot o snd) |
|
163 |> Pretty.big_list "quotients:" |
|
164 |> Pretty.writeln |
|
165 end |
|
166 |
|
167 |
|
168 (* info about quotient constants *) |
|
169 type qconsts_info = {qconst: term, rconst: term, def: thm} |
|
170 |
|
171 fun qconsts_info_eq (x : qconsts_info, y : qconsts_info) = #qconst x = #qconst y |
|
172 |
|
173 (* We need to be able to lookup instances of lifted constants, |
|
174 for example given "nat fset" we need to find "'a fset"; |
|
175 but overloaded constants share the same name *) |
|
176 structure QConstsData = Theory_Data |
|
177 (type T = (qconsts_info list) Symtab.table |
|
178 val empty = Symtab.empty |
|
179 val extend = I |
|
180 val merge = Symtab.merge_list qconsts_info_eq) |
|
181 |
|
182 fun transform_qconsts phi {qconst, rconst, def} = |
|
183 {qconst = Morphism.term phi qconst, |
|
184 rconst = Morphism.term phi rconst, |
|
185 def = Morphism.thm phi def} |
|
186 |
|
187 fun qconsts_update_thy name qcinfo = QConstsData.map (Symtab.cons_list (name, qcinfo)) |
|
188 fun qconsts_update_gen name qcinfo = Context.mapping (qconsts_update_thy name qcinfo) I |
|
189 |
|
190 fun qconsts_dest lthy = |
|
191 flat (map snd (Symtab.dest (QConstsData.get (ProofContext.theory_of lthy)))) |
|
192 |
|
193 fun qconsts_lookup thy t = |
|
194 let |
|
195 val (name, qty) = dest_Const t |
|
196 fun matches (x: qconsts_info) = |
|
197 let |
|
198 val (name', qty') = dest_Const (#qconst x); |
|
199 in |
|
200 name = name' andalso Sign.typ_instance thy (qty, qty') |
|
201 end |
|
202 in |
|
203 case Symtab.lookup (QConstsData.get thy) name of |
|
204 NONE => raise NotFound |
|
205 | SOME l => |
|
206 (case (find_first matches l) of |
|
207 SOME x => x |
|
208 | NONE => raise NotFound) |
|
209 end |
|
210 |
|
211 fun print_qconstinfo ctxt = |
|
212 let |
|
213 fun prt_qconst {qconst, rconst, def} = |
|
214 Pretty.block (separate (Pretty.brk 1) |
|
215 [Syntax.pretty_term ctxt qconst, |
|
216 Pretty.str ":=", |
|
217 Syntax.pretty_term ctxt rconst, |
|
218 Pretty.str "as", |
|
219 Syntax.pretty_term ctxt (prop_of def)]) |
|
220 in |
|
221 QConstsData.get (ProofContext.theory_of ctxt) |
|
222 |> Symtab.dest |
|
223 |> map snd |
|
224 |> flat |
|
225 |> map prt_qconst |
|
226 |> Pretty.big_list "quotient constants:" |
|
227 |> Pretty.writeln |
|
228 end |
|
229 |
|
230 (* equivalence relation theorems *) |
|
231 structure EquivRules = Named_Thms |
|
232 (val name = "quot_equiv" |
|
233 val description = "Equivalence relation theorems.") |
|
234 |
|
235 val equiv_rules_get = EquivRules.get |
|
236 val equiv_rules_add = EquivRules.add |
|
237 |
|
238 (* respectfulness theorems *) |
|
239 structure RspRules = Named_Thms |
|
240 (val name = "quot_respect" |
|
241 val description = "Respectfulness theorems.") |
|
242 |
|
243 val rsp_rules_get = RspRules.get |
|
244 val rsp_rules_add = RspRules.add |
|
245 |
|
246 (* preservation theorems *) |
|
247 structure PrsRules = Named_Thms |
|
248 (val name = "quot_preserve" |
|
249 val description = "Preservation theorems.") |
|
250 |
|
251 val prs_rules_get = PrsRules.get |
|
252 val prs_rules_add = PrsRules.add |
|
253 |
|
254 (* id simplification theorems *) |
|
255 structure IdSimps = Named_Thms |
|
256 (val name = "id_simps" |
|
257 val description = "Identity simp rules for maps.") |
|
258 |
|
259 val id_simps_get = IdSimps.get |
|
260 |
|
261 (* quotient theorems *) |
|
262 structure QuotientRules = Named_Thms |
|
263 (val name = "quot_thm" |
|
264 val description = "Quotient theorems.") |
|
265 |
|
266 val quotient_rules_get = QuotientRules.get |
|
267 val quotient_rules_add = QuotientRules.add |
|
268 |
|
269 (* setup of the theorem lists *) |
|
270 |
|
271 val _ = Context.>> (Context.map_theory |
|
272 (EquivRules.setup #> |
|
273 RspRules.setup #> |
|
274 PrsRules.setup #> |
|
275 IdSimps.setup #> |
|
276 QuotientRules.setup)) |
|
277 |
|
278 (* setup of the printing commands *) |
|
279 |
|
280 fun improper_command (pp_fn, cmd_name, descr_str) = |
|
281 OuterSyntax.improper_command cmd_name descr_str |
|
282 OuterKeyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of))) |
|
283 |
|
284 val _ = map improper_command |
|
285 [(print_mapsinfo, "print_quotmaps", "prints out all map functions"), |
|
286 (print_quotinfo, "print_quotients", "prints out all quotients"), |
|
287 (print_qconstinfo, "print_quotconsts", "prints out all quotient constants")] |
|
288 |
|
289 |
|
290 end; (* structure *) |
|