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, 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
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 true --| Scan.lift (@{keyword "="})) -- Args.const_proper true >>
75 (fn (tyname, relname) =>
76 let val minfo = {relmap = relname}
77 in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end))
78 "declaration of map information"
80 fun print_quotmaps ctxt =
82 fun prt_map (ty_name, {relmap}) =
83 Pretty.block (separate (Pretty.brk 2)
86 "relation map:", relmap]))
88 map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt)))
89 |> Pretty.big_list "maps for type constructors:"
93 (* info about abs/rep terms *)
94 type abs_rep = {abs : term, rep : term}
96 structure Abs_Rep = Generic_Data
98 type T = abs_rep Symtab.table
99 val empty = Symtab.empty
101 fun merge data = Symtab.merge (K true) data
104 fun transform_abs_rep phi {abs, rep} = {abs = Morphism.term phi abs, rep = Morphism.term phi rep}
106 val lookup_abs_rep = Symtab.lookup o Abs_Rep.get o Context.Proof
107 val lookup_abs_rep_global = Symtab.lookup o Abs_Rep.get o Context.Theory
109 fun update_abs_rep str data = Abs_Rep.map (Symtab.update (str, data))
111 fun print_abs_rep ctxt =
113 fun prt_abs_rep (s, {abs, rep}) =
114 Pretty.block (separate (Pretty.brk 2)
115 [Pretty.str "type constructor:",
117 Pretty.str "abs term:",
118 Syntax.pretty_term ctxt abs,
119 Pretty.str "rep term:",
120 Syntax.pretty_term ctxt rep])
122 map prt_abs_rep (Symtab.dest (Abs_Rep.get (Context.Proof ctxt)))
123 |> Pretty.big_list "abs/rep terms:"
127 (* info about quotient types *)
128 type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm, quot_thm: thm}
130 structure Quotients = Generic_Data
132 type T = quotients Symtab.table
133 val empty = Symtab.empty
135 fun merge data = Symtab.merge (K true) data
138 fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} =
139 {qtyp = Morphism.typ phi qtyp,
140 rtyp = Morphism.typ phi rtyp,
141 equiv_rel = Morphism.term phi equiv_rel,
142 equiv_thm = Morphism.thm phi equiv_thm,
143 quot_thm = Morphism.thm phi quot_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, quot_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),
165 Pretty.str "quot. thm:",
166 Syntax.pretty_term ctxt (prop_of quot_thm)])
168 map (prt_quot o snd) (Symtab.dest (Quotients.get (Context.Proof ctxt)))
169 |> Pretty.big_list "quotients:"
174 (* info about quotient constants *)
175 type quotconsts = {qconst: term, rconst: term, def: thm}
177 fun eq_quotconsts (x : quotconsts, y : quotconsts) = #qconst x = #qconst y
179 (* We need to be able to lookup instances of lifted constants,
180 for example given "nat fset" we need to find "'a fset";
181 but overloaded constants share the same name *)
182 structure Quotconsts = Generic_Data
184 type T = quotconsts list Symtab.table
185 val empty = Symtab.empty
187 val merge = Symtab.merge_list eq_quotconsts
190 fun transform_quotconsts phi {qconst, rconst, def} =
191 {qconst = Morphism.term phi qconst,
192 rconst = Morphism.term phi rconst,
193 def = Morphism.thm phi def}
195 fun update_quotconsts name qcinfo = Quotconsts.map (Symtab.cons_list (name, qcinfo))
197 fun dest_quotconsts ctxt =
198 flat (map snd (Symtab.dest (Quotconsts.get (Context.Proof ctxt))))
200 fun dest_quotconsts_global thy =
201 flat (map snd (Symtab.dest (Quotconsts.get (Context.Theory thy))))
205 fun lookup_quotconsts_global thy t =
207 val (name, qty) = dest_Const t
208 fun matches (x: quotconsts) =
209 let val (name', qty') = dest_Const (#qconst x);
210 in name = name' andalso Sign.typ_instance thy (qty, qty') end
212 (case Symtab.lookup (Quotconsts.get (Context.Theory thy)) name of
214 | SOME l => find_first matches l)
217 fun print_quotconsts ctxt =
219 fun prt_qconst {qconst, rconst, def} =
220 Pretty.block (separate (Pretty.brk 1)
221 [Syntax.pretty_term ctxt qconst,
223 Syntax.pretty_term ctxt rconst,
225 Syntax.pretty_term ctxt (prop_of def)])
227 map prt_qconst (maps snd (Symtab.dest (Quotconsts.get (Context.Proof ctxt))))
228 |> Pretty.big_list "quotient constants:"
232 (* equivalence relation theorems *)
233 structure Equiv_Rules = Named_Thms
235 val name = @{binding quot_equiv}
236 val description = "equivalence relation theorems"
239 val equiv_rules = Equiv_Rules.get
240 val equiv_rules_add = Equiv_Rules.add
242 (* respectfulness theorems *)
243 structure Rsp_Rules = Named_Thms
245 val name = @{binding quot_respect}
246 val description = "respectfulness theorems"
249 val rsp_rules = Rsp_Rules.get
250 val rsp_rules_add = Rsp_Rules.add
252 (* preservation theorems *)
253 structure Prs_Rules = Named_Thms
255 val name = @{binding quot_preserve}
256 val description = "preservation theorems"
259 val prs_rules = Prs_Rules.get
260 val prs_rules_add = Prs_Rules.add
262 (* id simplification theorems *)
263 structure Id_Simps = Named_Thms
265 val name = @{binding id_simps}
266 val description = "identity simp rules for maps"
269 val id_simps = Id_Simps.get
271 (* quotient theorems *)
272 structure Quotient_Rules = Named_Thms
274 val name = @{binding quot_thm}
275 val description = "quotient theorems"
278 val quotient_rules = Quotient_Rules.get
279 val quotient_rules_add = Quotient_Rules.add
285 quotmaps_attribute_setup #>
293 (* outer syntax commands *)
296 Outer_Syntax.improper_command @{command_spec "print_quotmaps"} "print quotient map functions"
297 (Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of)))
300 Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients"
301 (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
304 Outer_Syntax.improper_command @{command_spec "print_quotconsts"} "print quotient constants"
305 (Scan.succeed (Toplevel.keep (print_quotconsts o Toplevel.context_of)))