114 in |
114 in |
115 maps_attribute_aux tyname {mapfun = mapname, relmap = relname} |
115 maps_attribute_aux tyname {mapfun = mapname, relmap = relname} |
116 end |
116 end |
117 |
117 |
118 val maps_attr_parser = |
118 val maps_attr_parser = |
119 Args.context -- Scan.lift |
119 Args.context -- Scan.lift |
120 ((Args.name --| OuterParse.$$$ "=") -- |
120 ((Args.name --| OuterParse.$$$ "=") -- |
121 (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," -- |
121 (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," -- |
122 Args.name --| OuterParse.$$$ ")")) |
122 Args.name --| OuterParse.$$$ ")")) |
123 |
123 |
124 val _ = Context.>> (Context.map_theory |
124 val _ = Context.>> (Context.map_theory |
125 (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) |
125 (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) |
126 "declaration of map information")) |
126 "declaration of map information")) |
127 |
127 |
128 fun print_mapsinfo ctxt = |
128 fun print_mapsinfo ctxt = |
129 let |
129 let |
130 fun prt_map (ty_name, {mapfun, relmap}) = |
130 fun prt_map (ty_name, {mapfun, relmap}) = |
131 Pretty.block (Library.separate (Pretty.brk 2) |
131 Pretty.block (Library.separate (Pretty.brk 2) |
132 (map Pretty.str |
132 (map Pretty.str |
133 ["type:", ty_name, |
133 ["type:", ty_name, |
134 "map:", mapfun, |
134 "map:", mapfun, |
135 "relation map:", relmap])) |
135 "relation map:", relmap])) |
136 in |
136 in |
137 MapsData.get (ProofContext.theory_of ctxt) |
137 MapsData.get (ProofContext.theory_of ctxt) |
138 |> Symtab.dest |
138 |> Symtab.dest |
139 |> map (prt_map) |
139 |> map (prt_map) |
140 |> Pretty.big_list "maps for type constructors:" |
140 |> Pretty.big_list "maps for type constructors:" |
150 val empty = Symtab.empty |
150 val empty = Symtab.empty |
151 val extend = I |
151 val extend = I |
152 val merge = Symtab.merge (K true)) |
152 val merge = Symtab.merge (K true)) |
153 |
153 |
154 fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} = |
154 fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} = |
155 {qtyp = Morphism.typ phi qtyp, |
155 {qtyp = Morphism.typ phi qtyp, |
156 rtyp = Morphism.typ phi rtyp, |
156 rtyp = Morphism.typ phi rtyp, |
157 equiv_rel = Morphism.term phi equiv_rel, |
157 equiv_rel = Morphism.term phi equiv_rel, |
158 equiv_thm = Morphism.thm phi equiv_thm} |
158 equiv_thm = Morphism.thm phi equiv_thm} |
159 |
159 |
160 fun quotdata_lookup_raw thy str = Symtab.lookup (QuotData.get thy) str |
160 fun quotdata_lookup_raw thy str = Symtab.lookup (QuotData.get thy) str |
161 |
161 |
162 fun quotdata_lookup thy str = |
162 fun quotdata_lookup thy str = |
163 case Symtab.lookup (QuotData.get thy) str of |
163 case Symtab.lookup (QuotData.get thy) str of |
170 fun quotdata_dest lthy = |
170 fun quotdata_dest lthy = |
171 map snd (Symtab.dest (QuotData.get (ProofContext.theory_of lthy))) |
171 map snd (Symtab.dest (QuotData.get (ProofContext.theory_of lthy))) |
172 |
172 |
173 fun print_quotinfo ctxt = |
173 fun print_quotinfo ctxt = |
174 let |
174 let |
175 fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} = |
175 fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} = |
176 Pretty.block (Library.separate (Pretty.brk 2) |
176 Pretty.block (Library.separate (Pretty.brk 2) |
177 [Pretty.str "quotient type:", |
177 [Pretty.str "quotient type:", |
178 Syntax.pretty_typ ctxt qtyp, |
178 Syntax.pretty_typ ctxt qtyp, |
179 Pretty.str "raw type:", |
179 Pretty.str "raw type:", |
180 Syntax.pretty_typ ctxt rtyp, |
180 Syntax.pretty_typ ctxt rtyp, |
181 Pretty.str "relation:", |
181 Pretty.str "relation:", |
182 Syntax.pretty_term ctxt equiv_rel, |
182 Syntax.pretty_term ctxt equiv_rel, |
183 Pretty.str "equiv. thm:", |
183 Pretty.str "equiv. thm:", |
184 Syntax.pretty_term ctxt (prop_of equiv_thm)]) |
184 Syntax.pretty_term ctxt (prop_of equiv_thm)]) |
185 in |
185 in |
186 QuotData.get (ProofContext.theory_of ctxt) |
186 QuotData.get (ProofContext.theory_of ctxt) |
187 |> Symtab.dest |
187 |> Symtab.dest |
188 |> map (prt_quot o snd) |
188 |> map (prt_quot o snd) |
189 |> Pretty.big_list "quotients:" |
189 |> Pretty.big_list "quotients:" |
204 val empty = Symtab.empty |
204 val empty = Symtab.empty |
205 val extend = I |
205 val extend = I |
206 val merge = Symtab.merge_list qconsts_info_eq) |
206 val merge = Symtab.merge_list qconsts_info_eq) |
207 |
207 |
208 fun transform_qconsts phi {qconst, rconst, def} = |
208 fun transform_qconsts phi {qconst, rconst, def} = |
209 {qconst = Morphism.term phi qconst, |
209 {qconst = Morphism.term phi qconst, |
210 rconst = Morphism.term phi rconst, |
210 rconst = Morphism.term phi rconst, |
211 def = Morphism.thm phi def} |
211 def = Morphism.thm phi def} |
212 |
212 |
213 fun qconsts_update_thy name qcinfo = QConstsData.map (Symtab.cons_list (name, qcinfo)) |
213 fun qconsts_update_thy name qcinfo = QConstsData.map (Symtab.cons_list (name, qcinfo)) |
214 fun qconsts_update_gen name qcinfo = Context.mapping (qconsts_update_thy name qcinfo) I |
214 fun qconsts_update_gen name qcinfo = Context.mapping (qconsts_update_thy name qcinfo) I |
215 |
215 |
216 fun qconsts_dest lthy = |
216 fun qconsts_dest lthy = |
235 end |
235 end |
236 |
236 |
237 fun print_qconstinfo ctxt = |
237 fun print_qconstinfo ctxt = |
238 let |
238 let |
239 fun prt_qconst {qconst, rconst, def} = |
239 fun prt_qconst {qconst, rconst, def} = |
240 Pretty.block (separate (Pretty.brk 1) |
240 Pretty.block (separate (Pretty.brk 1) |
241 [Syntax.pretty_term ctxt qconst, |
241 [Syntax.pretty_term ctxt qconst, |
242 Pretty.str ":=", |
242 Pretty.str ":=", |
243 Syntax.pretty_term ctxt rconst, |
243 Syntax.pretty_term ctxt rconst, |
244 Pretty.str "as", |
244 Pretty.str "as", |
245 Syntax.pretty_term ctxt (prop_of def)]) |
245 Syntax.pretty_term ctxt (prop_of def)]) |
246 in |
246 in |
247 QConstsData.get (ProofContext.theory_of ctxt) |
247 QConstsData.get (ProofContext.theory_of ctxt) |
248 |> Symtab.dest |
248 |> Symtab.dest |
249 |> map snd |
249 |> map snd |
250 |> flat |
250 |> flat |
251 |> map prt_qconst |
251 |> map prt_qconst |
252 |> Pretty.big_list "quotient constants:" |
252 |> Pretty.big_list "quotient constants:" |
253 |> Pretty.writeln |
253 |> Pretty.writeln |
254 end |
254 end |
255 |
255 |
256 (* FIXME/TODO: check the various lemmas conform *) |
|
257 (* with the required shape *) |
|
258 |
|
259 (* equivalence relation theorems *) |
256 (* equivalence relation theorems *) |
260 structure EquivRules = Named_Thms |
257 structure EquivRules = Named_Thms |
261 (val name = "quot_equiv" |
258 (val name = "quot_equiv" |
262 val description = "Equivalence relation theorems.") |
259 val description = "Equivalence relation theorems.") |
263 |
260 |
295 val quotient_rules_add = QuotientRules.add |
292 val quotient_rules_add = QuotientRules.add |
296 |
293 |
297 (* setup of the theorem lists *) |
294 (* setup of the theorem lists *) |
298 |
295 |
299 val _ = Context.>> (Context.map_theory |
296 val _ = Context.>> (Context.map_theory |
300 (EquivRules.setup #> |
297 (EquivRules.setup #> |
301 RspRules.setup #> |
298 RspRules.setup #> |
302 PrsRules.setup #> |
299 PrsRules.setup #> |
303 IdSimps.setup #> |
300 IdSimps.setup #> |
304 QuotientRules.setup)) |
301 QuotientRules.setup)) |
305 |
302 |
306 (* setup of the printing commands *) |
303 (* setup of the printing commands *) |
307 |
304 |
308 fun improper_command (pp_fn, cmd_name, descr_str) = |
305 fun improper_command (pp_fn, cmd_name, descr_str) = |
309 OuterSyntax.improper_command cmd_name descr_str |
306 OuterSyntax.improper_command cmd_name descr_str |
310 OuterKeyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of))) |
307 OuterKeyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of))) |
311 |
308 |
312 val _ = map improper_command |
309 val _ = map improper_command |
313 [(print_mapsinfo, "print_maps", "prints out all map functions"), |
310 [(print_mapsinfo, "print_maps", "prints out all map functions"), |
314 (print_quotinfo, "print_quotients", "prints out all quotients"), |
311 (print_quotinfo, "print_quotients", "prints out all quotients"), |
315 (print_qconstinfo, "print_quotconsts", "prints out all quotient constants")] |
312 (print_qconstinfo, "print_quotconsts", "prints out all quotient constants")] |
316 |
313 |
317 |
314 |
318 end; (* structure *) |
315 end; (* structure *) |
319 |
316 |