5 val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state |
5 val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state |
6 val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state |
6 val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state |
7 val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory |
7 val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory |
8 val note: binding * thm -> local_theory -> thm * local_theory |
8 val note: binding * thm -> local_theory -> thm * local_theory |
9 val maps_lookup: theory -> string -> maps_info option |
9 val maps_lookup: theory -> string -> maps_info option |
10 val maps_update: string -> maps_info -> theory -> theory |
10 val maps_update_thy: string -> maps_info -> theory -> theory |
|
11 val maps_update: string -> maps_info -> Proof.context -> Proof.context |
11 val print_quotdata: Proof.context -> unit |
12 val print_quotdata: Proof.context -> unit |
12 val quotdata_lookup: theory -> quotient_info list |
13 val quotdata_lookup: theory -> quotient_info list |
13 val quotdata_update_thy: (typ * typ * term) -> theory -> theory |
14 val quotdata_update_thy: (typ * typ * term) -> theory -> theory |
14 val quotdata_update: (typ * typ * term) -> Proof.context -> Proof.context |
15 val quotdata_update: (typ * typ * term) -> Proof.context -> Proof.context |
15 end; |
16 end; |
29 val copy = I |
30 val copy = I |
30 val extend = I |
31 val extend = I |
31 fun merge _ = Symtab.merge (K true)) |
32 fun merge _ = Symtab.merge (K true)) |
32 |
33 |
33 val maps_lookup = Symtab.lookup o MapsData.get |
34 val maps_lookup = Symtab.lookup o MapsData.get |
34 fun maps_update k v = MapsData.map (Symtab.update (k, v)) |
35 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) |
|
36 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) |
|
37 |
|
38 fun maps_attribute_aux s minfo = Thm.declaration_attribute |
|
39 (fn thm => Context.mapping (maps_update_thy s minfo) (maps_update s minfo)) |
|
40 |
|
41 (* attribute to be used in declare statements *) |
|
42 fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) = |
|
43 let |
|
44 val thy = ProofContext.theory_of ctxt |
|
45 val tyname = Sign.intern_type thy tystr |
|
46 val mapname = Sign.intern_const thy mapstr |
|
47 val relname = Sign.intern_const thy relstr |
|
48 in |
|
49 maps_attribute_aux tyname {mapfun = mapname, relfun = relname} |
|
50 end |
|
51 |
|
52 val maps_attr_parser = |
|
53 Args.context -- Scan.lift |
|
54 ((Args.name --| OuterParse.$$$ "=") -- |
|
55 (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," -- |
|
56 Args.name --| OuterParse.$$$ ")")) |
|
57 |
|
58 val _ = Context.>> (Context.map_theory |
|
59 (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) |
|
60 "declaration of map information")) |
35 |
61 |
36 |
62 |
37 (* info about the quotient types *) |
63 (* info about the quotient types *) |
38 type quotient_info = {qtyp: typ, rtyp: typ, rel: term} |
64 type quotient_info = {qtyp: typ, rtyp: typ, rel: term} |
39 |
65 |
40 structure QuotData = TheoryDataFun |
66 structure QuotData = TheoryDataFun |
41 (type T = quotient_info list |
67 (type T = quotient_info list |
42 val empty = [] |
68 val empty = [] |
43 val copy = I |
69 val copy = I |
44 val extend = I |
70 val extend = I |
45 fun merge _ = (op @)) |
71 fun merge _ = (op @)) (* FIXME: is this the correct merging function for the list? *) |
46 |
72 |
47 val quotdata_lookup = QuotData.get |
73 val quotdata_lookup = QuotData.get |
48 |
74 |
49 fun quotdata_update_thy (qty, rty, rel) = |
75 fun quotdata_update_thy (qty, rty, rel) thy = |
50 QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel}::ls) |
76 QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel}::ls) thy |
51 |
77 |
52 fun quotdata_update (qty, rty, rel) = |
78 fun quotdata_update (qty, rty, rel) ctxt = |
53 ProofContext.theory (quotdata_update_thy (qty, rty, rel)) |
79 ProofContext.theory (quotdata_update_thy (qty, rty, rel)) ctxt |
54 |
80 |
55 fun print_quotdata ctxt = |
81 fun print_quotdata ctxt = |
56 let |
82 let |
57 val quots = QuotData.get (ProofContext.theory_of ctxt) |
|
58 fun prt_quot {qtyp, rtyp, rel} = |
83 fun prt_quot {qtyp, rtyp, rel} = |
59 Pretty.block [Pretty.str ("quotient:"), |
84 Pretty.block (Library.separate (Pretty.brk 2) |
60 Pretty.brk 2, Syntax.pretty_typ ctxt qtyp, |
85 [Pretty.str ("quotient type:"), |
61 Pretty.brk 2, Syntax.pretty_typ ctxt rtyp, |
86 Syntax.pretty_typ ctxt qtyp, |
62 Pretty.brk 2, Syntax.pretty_term ctxt rel] |
87 Pretty.str ("raw type:"), |
63 in |
88 Syntax.pretty_typ ctxt rtyp, |
64 [Pretty.big_list "quotients:" (map prt_quot quots)] |
89 Pretty.str ("relation:"), |
65 |> Pretty.chunks |> Pretty.writeln |
90 Syntax.pretty_term ctxt rel]) |
|
91 in |
|
92 QuotData.get (ProofContext.theory_of ctxt) |
|
93 |> map prt_quot |
|
94 |> Pretty.big_list "quotients:" |
|
95 |> Pretty.writeln |
66 end |
96 end |
67 |
97 |
68 val _ = |
98 val _ = |
69 OuterSyntax.improper_command "print_quotients" "print quotient types of this theory" |
99 OuterSyntax.improper_command "print_quotients" "print out all quotients" |
70 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotdata o Toplevel.context_of))) |
100 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotdata o Toplevel.context_of))) |
71 |
101 |
72 |
102 |
73 |
103 |
74 (* wrappers for define and note *) |
104 (* wrappers for define and note *) |
198 |
228 |
199 (* quotient theorem *) |
229 (* quotient theorem *) |
200 val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2 |
230 val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2 |
201 val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name |
231 val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name |
202 |
232 |
203 |
|
204 (* storing the quot-info *) |
233 (* storing the quot-info *) |
205 val lthy3 = quotdata_update (abs_ty, rty, rel) lthy2 |
234 val lthy3 = quotdata_update (abs_ty, rty, rel) lthy2 |
206 |
235 |
207 (* interpretation *) |
236 (* interpretation *) |
208 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
237 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
246 (* - the type to be quotient *) |
275 (* - the type to be quotient *) |
247 (* - the relation according to which the type is quotient *) |
276 (* - the relation according to which the type is quotient *) |
248 |
277 |
249 fun mk_quotient_type quot_list lthy = |
278 fun mk_quotient_type quot_list lthy = |
250 let |
279 let |
251 fun get_goal (rty, rel) = |
280 fun mk_goal (rty, rel) = |
252 let |
281 let |
253 val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
282 val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
254 in |
283 in |
255 (HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel), []) |
284 (HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel), []) |
256 end |
285 end |
257 |
286 |
258 val goals = map (get_goal o snd) quot_list |
287 val goals = map (mk_goal o snd) quot_list |
259 |
288 |
260 fun after_qed thms lthy = |
289 fun after_qed thms lthy = |
261 fold_map mk_typedef_main (quot_list ~~ (flat thms)) lthy |> snd |
290 fold_map mk_typedef_main (quot_list ~~ (flat thms)) lthy |> snd |
262 in |
291 in |
263 Proof.theorem_i NONE after_qed [goals] lthy |
292 Proof.theorem_i NONE after_qed [goals] lthy |