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