equal
deleted
inserted
replaced
24 val print_qconstinfo: Proof.context -> unit |
24 val print_qconstinfo: Proof.context -> unit |
25 |
25 |
26 val equiv_rules_get: Proof.context -> thm list |
26 val equiv_rules_get: Proof.context -> thm list |
27 val equiv_rules_add: attribute |
27 val equiv_rules_add: attribute |
28 val rsp_rules_get: Proof.context -> thm list |
28 val rsp_rules_get: Proof.context -> thm list |
|
29 val id_simps_get: Proof.context -> thm list |
29 val quotient_rules_get: Proof.context -> thm list |
30 val quotient_rules_get: Proof.context -> thm list |
30 val quotient_rules_add: attribute |
31 val quotient_rules_add: attribute |
31 end; |
32 end; |
32 |
33 |
33 structure Quotient_Info: QUOTIENT_INFO = |
34 structure Quotient_Info: QUOTIENT_INFO = |
60 let |
61 let |
61 val thy = ProofContext.theory_of ctxt |
62 val thy = ProofContext.theory_of ctxt |
62 val tyname = Sign.intern_type thy tystr |
63 val tyname = Sign.intern_type thy tystr |
63 val mapname = Sign.intern_const thy mapstr |
64 val mapname = Sign.intern_const thy mapstr |
64 val relname = Sign.intern_const thy relstr |
65 val relname = Sign.intern_const thy relstr |
|
66 |
|
67 fun check s = (Const (s, dummyT) |> Syntax.check_term ctxt) |
|
68 handle _ => error ("Constant " ^ s ^ " not declared.") |
|
69 val _ = map check [mapname, relname] |
65 in |
70 in |
66 maps_attribute_aux tyname {mapfun = mapname, relfun = relname} |
71 maps_attribute_aux tyname {mapfun = mapname, relfun = relname} |
67 end |
72 end |
68 |
73 |
69 val maps_attr_parser = |
74 val maps_attr_parser = |
168 |
173 |
169 val _ = |
174 val _ = |
170 OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" |
175 OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" |
171 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of))) |
176 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of))) |
172 |
177 |
|
178 (* FIXME/TODO: check the various lemmas conform *) |
|
179 (* with the required shape *) |
|
180 |
173 (* equivalence relation theorems *) |
181 (* equivalence relation theorems *) |
174 structure EquivRules = Named_Thms |
182 structure EquivRules = Named_Thms |
175 (val name = "quotient_equiv" |
183 (val name = "quotient_equiv" |
176 val description = "Equivalence relation theorems.") |
184 val description = "Equivalence relation theorems.") |
177 |
185 |
183 (val name = "quotient_rsp" |
191 (val name = "quotient_rsp" |
184 val description = "Respectfulness theorems.") |
192 val description = "Respectfulness theorems.") |
185 |
193 |
186 val rsp_rules_get = RspRules.get |
194 val rsp_rules_get = RspRules.get |
187 |
195 |
|
196 (* respectfulness theorems *) |
|
197 structure IdSimps = Named_Thms |
|
198 (val name = "id_simps" |
|
199 val description = "Identity simp rules for maps.") |
|
200 |
|
201 val id_simps_get = IdSimps.get |
|
202 |
188 (* quotient theorems *) |
203 (* quotient theorems *) |
189 structure QuotientRules = Named_Thms |
204 structure QuotientRules = Named_Thms |
190 (val name = "quotient_thm" |
205 (val name = "quotient_thm" |
191 val description = "Quotient theorems.") |
206 val description = "Quotient theorems.") |
192 |
207 |
195 |
210 |
196 (* setup of the theorem lists *) |
211 (* setup of the theorem lists *) |
197 val _ = Context.>> (Context.map_theory |
212 val _ = Context.>> (Context.map_theory |
198 (EquivRules.setup #> |
213 (EquivRules.setup #> |
199 RspRules.setup #> |
214 RspRules.setup #> |
|
215 IdSimps.setup #> |
200 QuotientRules.setup)) |
216 QuotientRules.setup)) |
201 |
217 |
202 end; (* structure *) |
218 end; (* structure *) |
203 |
219 |
204 open Quotient_Info |
220 open Quotient_Info |