|
1 signature QUOTIENT_INFO = |
|
2 sig |
|
3 exception NotFound |
|
4 |
|
5 type maps_info = {mapfun: string, relfun: string} |
|
6 val maps_lookup: theory -> string -> maps_info option |
|
7 val maps_update_thy: string -> maps_info -> theory -> theory |
|
8 val maps_update: string -> maps_info -> Proof.context -> Proof.context |
|
9 |
|
10 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
|
11 val print_quotinfo: Proof.context -> unit |
|
12 val quotdata_lookup_thy: theory -> string -> quotient_info option |
|
13 val quotdata_lookup: Proof.context -> string -> quotient_info option |
|
14 val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory |
|
15 val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context |
|
16 val quotdata_dest: theory -> quotient_info list |
|
17 |
|
18 type qconsts_info = {qconst: term, rconst: term, def: thm} |
|
19 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
|
20 val qconsts_lookup: theory -> string -> qconsts_info |
|
21 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
|
22 val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
|
23 val qconsts_dest: theory -> qconsts_info list |
|
24 val print_qconstinfo: Proof.context -> unit |
|
25 |
|
26 val equiv_rules_get: Proof.context -> thm list |
|
27 val equiv_rules_add: attribute |
|
28 val rsp_rules_get: Proof.context -> thm list |
|
29 val quotient_rules_get: Proof.context -> thm list |
|
30 val quotient_rules_add: attribute |
|
31 end; |
|
32 |
|
33 structure Quotient_Info: QUOTIENT_INFO = |
|
34 struct |
|
35 |
|
36 exception NotFound |
|
37 |
|
38 (* data containers *) |
|
39 (*******************) |
|
40 |
|
41 (* info about map- and rel-functions *) |
|
42 type maps_info = {mapfun: string, relfun: string} |
|
43 |
|
44 structure MapsData = Theory_Data |
|
45 (type T = maps_info Symtab.table |
|
46 val empty = Symtab.empty |
|
47 val extend = I |
|
48 val merge = Symtab.merge (K true)) |
|
49 |
|
50 val maps_lookup = Symtab.lookup o MapsData.get |
|
51 |
|
52 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) |
|
53 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) |
|
54 |
|
55 fun maps_attribute_aux s minfo = Thm.declaration_attribute |
|
56 (fn thm => Context.mapping (maps_update_thy s minfo) (maps_update s minfo)) |
|
57 |
|
58 (* attribute to be used in declare statements *) |
|
59 fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) = |
|
60 let |
|
61 val thy = ProofContext.theory_of ctxt |
|
62 val tyname = Sign.intern_type thy tystr |
|
63 val mapname = Sign.intern_const thy mapstr |
|
64 val relname = Sign.intern_const thy relstr |
|
65 in |
|
66 maps_attribute_aux tyname {mapfun = mapname, relfun = relname} |
|
67 end |
|
68 |
|
69 val maps_attr_parser = |
|
70 Args.context -- Scan.lift |
|
71 ((Args.name --| OuterParse.$$$ "=") -- |
|
72 (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," -- |
|
73 Args.name --| OuterParse.$$$ ")")) |
|
74 |
|
75 val _ = Context.>> (Context.map_theory |
|
76 (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) |
|
77 "declaration of map information")) |
|
78 |
|
79 |
|
80 (* info about quotient types *) |
|
81 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
|
82 |
|
83 structure QuotData = Theory_Data |
|
84 (type T = quotient_info Symtab.table |
|
85 val empty = Symtab.empty |
|
86 val extend = I |
|
87 val merge = Symtab.merge (K true)) |
|
88 |
|
89 fun quotdata_lookup_thy thy str = |
|
90 Symtab.lookup (QuotData.get thy) (Sign.intern_type thy str) |
|
91 |
|
92 val quotdata_lookup = quotdata_lookup_thy o ProofContext.theory_of |
|
93 |
|
94 fun quotdata_update_thy qty_name (qty, rty, rel, equiv_thm) = |
|
95 QuotData.map (Symtab.update (qty_name, {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm})) |
|
96 |
|
97 fun quotdata_update qty_name (qty, rty, rel, equiv_thm) = |
|
98 ProofContext.theory (quotdata_update_thy qty_name (qty, rty, rel, equiv_thm)) |
|
99 |
|
100 fun quotdata_dest thy = |
|
101 map snd (Symtab.dest (QuotData.get thy)) |
|
102 |
|
103 fun print_quotinfo ctxt = |
|
104 let |
|
105 fun prt_quot {qtyp, rtyp, rel, equiv_thm} = |
|
106 Pretty.block (Library.separate (Pretty.brk 2) |
|
107 [Pretty.str "quotient type:", |
|
108 Syntax.pretty_typ ctxt qtyp, |
|
109 Pretty.str "raw type:", |
|
110 Syntax.pretty_typ ctxt rtyp, |
|
111 Pretty.str "relation:", |
|
112 Syntax.pretty_term ctxt rel, |
|
113 Pretty.str "equiv. thm:", |
|
114 Syntax.pretty_term ctxt (prop_of equiv_thm)]) |
|
115 in |
|
116 QuotData.get (ProofContext.theory_of ctxt) |
|
117 |> Symtab.dest |
|
118 |> map (prt_quot o snd) |
|
119 |> Pretty.big_list "quotients:" |
|
120 |> Pretty.writeln |
|
121 end |
|
122 |
|
123 val _ = |
|
124 OuterSyntax.improper_command "print_quotients" "print out all quotients" |
|
125 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of))) |
|
126 |
|
127 |
|
128 (* info about quotient constants *) |
|
129 type qconsts_info = {qconst: term, rconst: term, def: thm} |
|
130 |
|
131 structure QConstsData = Theory_Data |
|
132 (type T = qconsts_info Symtab.table |
|
133 val empty = Symtab.empty |
|
134 val extend = I |
|
135 val merge = Symtab.merge (K true)) |
|
136 |
|
137 fun qconsts_transfer phi {qconst, rconst, def} = |
|
138 {qconst = Morphism.term phi qconst, |
|
139 rconst = Morphism.term phi rconst, |
|
140 def = Morphism.thm phi def} |
|
141 |
|
142 fun qconsts_lookup thy str = |
|
143 case Symtab.lookup (QConstsData.get thy) str of |
|
144 SOME info => info |
|
145 | NONE => raise NotFound |
|
146 |
|
147 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo)) |
|
148 fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I |
|
149 |
|
150 fun qconsts_dest thy = |
|
151 map snd (Symtab.dest (QConstsData.get thy)) |
|
152 |
|
153 (* We don't print the definition *) |
|
154 fun print_qconstinfo ctxt = |
|
155 let |
|
156 fun prt_qconst {qconst, rconst, def} = |
|
157 Pretty.block (separate (Pretty.brk 1) |
|
158 [Syntax.pretty_term ctxt qconst, |
|
159 Pretty.str ":=", |
|
160 Syntax.pretty_term ctxt rconst]) |
|
161 in |
|
162 QConstsData.get (ProofContext.theory_of ctxt) |
|
163 |> Symtab.dest |
|
164 |> map (prt_qconst o snd) |
|
165 |> Pretty.big_list "quotient constants:" |
|
166 |> Pretty.writeln |
|
167 end |
|
168 |
|
169 val _ = |
|
170 OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" |
|
171 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of))) |
|
172 |
|
173 (* equivalence relation theorems *) |
|
174 structure EquivRules = Named_Thms |
|
175 (val name = "quotient_equiv" |
|
176 val description = "Equivalence relation theorems.") |
|
177 |
|
178 val equiv_rules_get = EquivRules.get |
|
179 val equiv_rules_add = EquivRules.add |
|
180 |
|
181 (* respectfulness theorems *) |
|
182 structure RspRules = Named_Thms |
|
183 (val name = "quotient_rsp" |
|
184 val description = "Respectfulness theorems.") |
|
185 |
|
186 val rsp_rules_get = RspRules.get |
|
187 |
|
188 (* quotient theorems *) |
|
189 structure QuotientRules = Named_Thms |
|
190 (val name = "quotient_thm" |
|
191 val description = "Quotient theorems.") |
|
192 |
|
193 val quotient_rules_get = QuotientRules.get |
|
194 val quotient_rules_add = QuotientRules.add |
|
195 |
|
196 (* setup of the theorem lists *) |
|
197 val _ = Context.>> (Context.map_theory |
|
198 (EquivRules.setup #> |
|
199 RspRules.setup #> |
|
200 QuotientRules.setup)) |
|
201 |
|
202 end; (* structure *) |
|
203 |
|
204 open Quotient_Info |