264
|
1 |
signature QUOTIENT_INFO =
|
|
2 |
sig
|
549
|
3 |
exception NotFound
|
|
4 |
|
264
|
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}
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
11 |
val print_quotinfo: Proof.context -> unit
|
311
|
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
|
460
3f8c7183ddac
added facilities to get all stored quotient data (equiv thms etc)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
16 |
val quotdata_dest: theory -> quotient_info list
|
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
17 |
|
496
|
18 |
type qconsts_info = {qconst: term, rconst: term, def: thm}
|
318
|
19 |
val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
|
549
|
20 |
val qconsts_lookup: theory -> string -> qconsts_info
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
21 |
val qconsts_update_thy: string -> qconsts_info -> theory -> theory
|
497
b663bc007d00
Added qoutient_consts dest for getting all the constant definitions in the cleaning step.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
22 |
val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic
|
b663bc007d00
Added qoutient_consts dest for getting all the constant definitions in the cleaning step.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
23 |
val qconsts_dest: theory -> qconsts_info list
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
24 |
val print_qconstinfo: Proof.context -> unit
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
25 |
|
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
26 |
val rsp_rules_get: Proof.context -> thm list
|
503
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
27 |
val quotient_rules_get: Proof.context -> thm list
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
28 |
val quotient_rules_add: attribute
|
264
|
29 |
end;
|
|
30 |
|
|
31 |
structure Quotient_Info: QUOTIENT_INFO =
|
|
32 |
struct
|
|
33 |
|
549
|
34 |
exception NotFound
|
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
35 |
|
264
|
36 |
(* data containers *)
|
|
37 |
(*******************)
|
|
38 |
|
|
39 |
(* info about map- and rel-functions *)
|
|
40 |
type maps_info = {mapfun: string, relfun: string}
|
|
41 |
|
306
|
42 |
structure MapsData = Theory_Data
|
264
|
43 |
(type T = maps_info Symtab.table
|
|
44 |
val empty = Symtab.empty
|
|
45 |
val extend = I
|
306
|
46 |
val merge = Symtab.merge (K true))
|
264
|
47 |
|
|
48 |
val maps_lookup = Symtab.lookup o MapsData.get
|
|
49 |
|
|
50 |
fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
|
|
51 |
fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo)
|
|
52 |
|
|
53 |
fun maps_attribute_aux s minfo = Thm.declaration_attribute
|
|
54 |
(fn thm => Context.mapping (maps_update_thy s minfo) (maps_update s minfo))
|
|
55 |
|
|
56 |
(* attribute to be used in declare statements *)
|
|
57 |
fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) =
|
|
58 |
let
|
|
59 |
val thy = ProofContext.theory_of ctxt
|
|
60 |
val tyname = Sign.intern_type thy tystr
|
|
61 |
val mapname = Sign.intern_const thy mapstr
|
|
62 |
val relname = Sign.intern_const thy relstr
|
|
63 |
in
|
|
64 |
maps_attribute_aux tyname {mapfun = mapname, relfun = relname}
|
|
65 |
end
|
|
66 |
|
|
67 |
val maps_attr_parser =
|
|
68 |
Args.context -- Scan.lift
|
|
69 |
((Args.name --| OuterParse.$$$ "=") --
|
|
70 |
(OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," --
|
|
71 |
Args.name --| OuterParse.$$$ ")"))
|
|
72 |
|
|
73 |
val _ = Context.>> (Context.map_theory
|
|
74 |
(Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute)
|
|
75 |
"declaration of map information"))
|
|
76 |
|
|
77 |
|
329
|
78 |
(* info about quotient types *)
|
264
|
79 |
type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
|
|
80 |
|
306
|
81 |
structure QuotData = Theory_Data
|
311
|
82 |
(type T = quotient_info Symtab.table
|
|
83 |
val empty = Symtab.empty
|
264
|
84 |
val extend = I
|
311
|
85 |
val merge = Symtab.merge (K true))
|
264
|
86 |
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
87 |
fun quotdata_lookup_thy thy str =
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
88 |
Symtab.lookup (QuotData.get thy) (Sign.intern_type thy str)
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
89 |
|
311
|
90 |
val quotdata_lookup = quotdata_lookup_thy o ProofContext.theory_of
|
264
|
91 |
|
314
|
92 |
fun quotdata_update_thy qty_name (qty, rty, rel, equiv_thm) =
|
311
|
93 |
QuotData.map (Symtab.update (qty_name, {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}))
|
264
|
94 |
|
311
|
95 |
fun quotdata_update qty_name (qty, rty, rel, equiv_thm) =
|
|
96 |
ProofContext.theory (quotdata_update_thy qty_name (qty, rty, rel, equiv_thm))
|
264
|
97 |
|
460
3f8c7183ddac
added facilities to get all stored quotient data (equiv thms etc)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
98 |
fun quotdata_dest thy =
|
3f8c7183ddac
added facilities to get all stored quotient data (equiv thms etc)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
99 |
map snd (Symtab.dest (QuotData.get thy))
|
3f8c7183ddac
added facilities to get all stored quotient data (equiv thms etc)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
100 |
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
101 |
fun print_quotinfo ctxt =
|
264
|
102 |
let
|
|
103 |
fun prt_quot {qtyp, rtyp, rel, equiv_thm} =
|
|
104 |
Pretty.block (Library.separate (Pretty.brk 2)
|
324
|
105 |
[Pretty.str "quotient type:",
|
264
|
106 |
Syntax.pretty_typ ctxt qtyp,
|
324
|
107 |
Pretty.str "raw type:",
|
264
|
108 |
Syntax.pretty_typ ctxt rtyp,
|
324
|
109 |
Pretty.str "relation:",
|
264
|
110 |
Syntax.pretty_term ctxt rel,
|
324
|
111 |
Pretty.str "equiv. thm:",
|
264
|
112 |
Syntax.pretty_term ctxt (prop_of equiv_thm)])
|
|
113 |
in
|
|
114 |
QuotData.get (ProofContext.theory_of ctxt)
|
311
|
115 |
|> Symtab.dest
|
|
116 |
|> map (prt_quot o snd)
|
264
|
117 |
|> Pretty.big_list "quotients:"
|
|
118 |
|> Pretty.writeln
|
|
119 |
end
|
|
120 |
|
|
121 |
val _ =
|
|
122 |
OuterSyntax.improper_command "print_quotients" "print out all quotients"
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
123 |
OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of)))
|
264
|
124 |
|
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
125 |
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
126 |
(* info about quotient constants *)
|
496
|
127 |
type qconsts_info = {qconst: term, rconst: term, def: thm}
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
128 |
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
129 |
structure QConstsData = Theory_Data
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
130 |
(type T = qconsts_info Symtab.table
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
131 |
val empty = Symtab.empty
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
132 |
val extend = I
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
133 |
val merge = Symtab.merge (K true))
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
134 |
|
496
|
135 |
fun qconsts_transfer phi {qconst, rconst, def} =
|
318
|
136 |
{qconst = Morphism.term phi qconst,
|
496
|
137 |
rconst = Morphism.term phi rconst,
|
|
138 |
def = Morphism.thm phi def}
|
318
|
139 |
|
549
|
140 |
fun qconsts_lookup thy str =
|
|
141 |
case Symtab.lookup (QConstsData.get thy) str of
|
|
142 |
SOME info => info
|
|
143 |
| NONE => raise NotFound
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
144 |
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
145 |
fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo))
|
324
|
146 |
fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
147 |
|
497
b663bc007d00
Added qoutient_consts dest for getting all the constant definitions in the cleaning step.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
148 |
fun qconsts_dest thy =
|
b663bc007d00
Added qoutient_consts dest for getting all the constant definitions in the cleaning step.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
149 |
map snd (Symtab.dest (QConstsData.get thy))
|
b663bc007d00
Added qoutient_consts dest for getting all the constant definitions in the cleaning step.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
150 |
|
496
|
151 |
(* We don't print the definition *)
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
152 |
fun print_qconstinfo ctxt =
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
153 |
let
|
496
|
154 |
fun prt_qconst {qconst, rconst, def} =
|
318
|
155 |
Pretty.block (separate (Pretty.brk 1)
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
156 |
[Syntax.pretty_term ctxt qconst,
|
318
|
157 |
Pretty.str ":=",
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
158 |
Syntax.pretty_term ctxt rconst])
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
159 |
in
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
160 |
QConstsData.get (ProofContext.theory_of ctxt)
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
161 |
|> Symtab.dest
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
162 |
|> map (prt_qconst o snd)
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
163 |
|> Pretty.big_list "quotient constants:"
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
164 |
|> Pretty.writeln
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
165 |
end
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
166 |
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
167 |
val _ =
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
168 |
OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants"
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
169 |
OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of)))
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
170 |
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
171 |
(* respectfulness lemmas *)
|
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
172 |
structure RspRules = Named_Thms
|
506
|
173 |
(val name = "quotient_rsp"
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
174 |
val description = "Respectfulness theorems.")
|
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
175 |
|
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
176 |
val rsp_rules_get = RspRules.get
|
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
177 |
|
503
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
178 |
(* quotient lemmas *)
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
179 |
structure QuotientRules = Named_Thms
|
506
|
180 |
(val name = "quotient_thm"
|
503
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
181 |
val description = "Quotient theorems.")
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
182 |
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
183 |
val quotient_rules_get = QuotientRules.get
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
184 |
val quotient_rules_add = Thm.declaration_attribute QuotientRules.add_thm
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
185 |
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
186 |
(* setup of the theorem lists *)
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
187 |
val _ = Context.>> (Context.map_theory
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
188 |
(RspRules.setup #>
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
189 |
QuotientRules.setup))
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
190 |
|
264
|
191 |
end; (* structure *)
|
|
192 |
|
314
|
193 |
open Quotient_Info
|