952
|
1 |
(* Title: quotient_info.thy
|
|
2 |
Author: Cezary Kaliszyk and Christian Urban
|
|
3 |
|
|
4 |
Data slots for the quotient package.
|
|
5 |
|
|
6 |
*)
|
|
7 |
|
|
8 |
|
264
|
9 |
signature QUOTIENT_INFO =
|
|
10 |
sig
|
549
|
11 |
exception NotFound
|
|
12 |
|
784
|
13 |
type maps_info = {mapfun: string, relmap: string}
|
866
|
14 |
val maps_defined: theory -> string -> bool
|
784
|
15 |
val maps_lookup: theory -> string -> maps_info (* raises NotFound *)
|
264
|
16 |
val maps_update_thy: string -> maps_info -> theory -> theory
|
|
17 |
val maps_update: string -> maps_info -> Proof.context -> Proof.context
|
699
|
18 |
val print_mapsinfo: Proof.context -> unit
|
264
|
19 |
|
786
|
20 |
type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
|
799
|
21 |
val transform_quotdata: morphism -> quotdata_info -> quotdata_info
|
875
|
22 |
val quotdata_lookup_raw: theory -> string -> quotdata_info option
|
786
|
23 |
val quotdata_lookup: theory -> string -> quotdata_info (* raises NotFound *)
|
|
24 |
val quotdata_update_thy: string -> quotdata_info -> theory -> theory
|
|
25 |
val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic
|
1064
|
26 |
val quotdata_dest: Proof.context -> quotdata_info list
|
699
|
27 |
val print_quotinfo: Proof.context -> unit
|
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
|
28 |
|
496
|
29 |
type qconsts_info = {qconst: term, rconst: term, def: thm}
|
799
|
30 |
val transform_qconsts: morphism -> qconsts_info -> qconsts_info
|
784
|
31 |
val qconsts_lookup: theory -> term -> qconsts_info (* raises NotFound *)
|
868
09d5b7f0e55d
Undid changes from symtab to termtab, since we need to lookup specialized types.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
32 |
val qconsts_update_thy: string -> qconsts_info -> theory -> theory
|
09d5b7f0e55d
Undid changes from symtab to termtab, since we need to lookup specialized types.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
33 |
val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic
|
871
|
34 |
val qconsts_dest: Proof.context -> qconsts_info list
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
35 |
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
|
36 |
|
582
|
37 |
val equiv_rules_get: Proof.context -> thm list
|
|
38 |
val equiv_rules_add: attribute
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
39 |
val rsp_rules_get: Proof.context -> thm list
|
636
|
40 |
val prs_rules_get: Proof.context -> thm list
|
614
|
41 |
val id_simps_get: Proof.context -> thm list
|
503
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
42 |
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
|
43 |
val quotient_rules_add: attribute
|
264
|
44 |
end;
|
|
45 |
|
798
|
46 |
|
|
47 |
functor Filtered_Named_Thms (val name: string val description: string val filter: thm -> thm): NAMED_THMS =
|
797
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
48 |
struct
|
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
49 |
|
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
50 |
structure Data = Generic_Data
|
798
|
51 |
( type T = thm Item_Net.T;
|
797
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
52 |
val empty = Thm.full_rules;
|
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
53 |
val extend = I;
|
798
|
54 |
val merge = Item_Net.merge);
|
797
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
55 |
|
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
56 |
val content = Item_Net.content o Data.get;
|
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
57 |
val get = content o Context.Proof;
|
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
58 |
|
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
59 |
val add_thm = Data.map o Item_Net.update o filter;
|
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
60 |
val del_thm = Data.map o Item_Net.remove;
|
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
61 |
|
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
62 |
val add = Thm.declaration_attribute add_thm;
|
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
63 |
val del = Thm.declaration_attribute del_thm;
|
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
64 |
|
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
65 |
val setup =
|
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
66 |
Attrib.setup (Binding.name name) (Attrib.add_del add del) ("declaration of " ^ description) #>
|
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
67 |
PureThy.add_thms_dynamic (Binding.name name, content);
|
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
68 |
|
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
69 |
end;
|
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
70 |
|
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
71 |
|
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
72 |
|
264
|
73 |
structure Quotient_Info: QUOTIENT_INFO =
|
|
74 |
struct
|
|
75 |
|
549
|
76 |
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
|
77 |
|
850
|
78 |
|
|
79 |
(** data containers **)
|
264
|
80 |
|
759
|
81 |
(* info about map- and rel-functions for a type *)
|
784
|
82 |
type maps_info = {mapfun: string, relmap: string}
|
264
|
83 |
|
306
|
84 |
structure MapsData = Theory_Data
|
264
|
85 |
(type T = maps_info Symtab.table
|
|
86 |
val empty = Symtab.empty
|
|
87 |
val extend = I
|
306
|
88 |
val merge = Symtab.merge (K true))
|
264
|
89 |
|
866
|
90 |
fun maps_defined thy s =
|
|
91 |
Symtab.defined (MapsData.get thy) s
|
805
d193e2111811
added a warning to the quotient_type definition, if a map function is missing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
92 |
|
760
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
93 |
fun maps_lookup thy s =
|
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
94 |
case (Symtab.lookup (MapsData.get thy) s) of
|
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
95 |
SOME map_fun => map_fun
|
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
96 |
| NONE => raise NotFound
|
264
|
97 |
|
|
98 |
fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
|
|
99 |
fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo)
|
|
100 |
|
|
101 |
fun maps_attribute_aux s minfo = Thm.declaration_attribute
|
786
|
102 |
(fn _ => Context.mapping (maps_update_thy s minfo) (maps_update s minfo))
|
264
|
103 |
|
|
104 |
(* attribute to be used in declare statements *)
|
|
105 |
fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) =
|
|
106 |
let
|
|
107 |
val thy = ProofContext.theory_of ctxt
|
|
108 |
val tyname = Sign.intern_type thy tystr
|
|
109 |
val mapname = Sign.intern_const thy mapstr
|
|
110 |
val relname = Sign.intern_const thy relstr
|
613
|
111 |
|
866
|
112 |
fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt; ())
|
|
113 |
val _ = List.app sanity_check [mapname, relname]
|
264
|
114 |
in
|
784
|
115 |
maps_attribute_aux tyname {mapfun = mapname, relmap = relname}
|
264
|
116 |
end
|
|
117 |
|
|
118 |
val maps_attr_parser =
|
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
119 |
Args.context -- Scan.lift
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
120 |
((Args.name --| OuterParse.$$$ "=") --
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
121 |
(OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," --
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
122 |
Args.name --| OuterParse.$$$ ")"))
|
264
|
123 |
|
|
124 |
val _ = Context.>> (Context.map_theory
|
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
125 |
(Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute)
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
126 |
"declaration of map information"))
|
264
|
127 |
|
699
|
128 |
fun print_mapsinfo ctxt =
|
|
129 |
let
|
784
|
130 |
fun prt_map (ty_name, {mapfun, relmap}) =
|
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
131 |
Pretty.block (Library.separate (Pretty.brk 2)
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
132 |
(map Pretty.str
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
133 |
["type:", ty_name,
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
134 |
"map:", mapfun,
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
135 |
"relation map:", relmap]))
|
699
|
136 |
in
|
|
137 |
MapsData.get (ProofContext.theory_of ctxt)
|
|
138 |
|> Symtab.dest
|
|
139 |
|> map (prt_map)
|
786
|
140 |
|> Pretty.big_list "maps for type constructors:"
|
699
|
141 |
|> Pretty.writeln
|
|
142 |
end
|
|
143 |
|
778
|
144 |
|
329
|
145 |
(* info about quotient types *)
|
786
|
146 |
type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
|
264
|
147 |
|
306
|
148 |
structure QuotData = Theory_Data
|
786
|
149 |
(type T = quotdata_info Symtab.table
|
311
|
150 |
val empty = Symtab.empty
|
264
|
151 |
val extend = I
|
311
|
152 |
val merge = Symtab.merge (K true))
|
264
|
153 |
|
799
|
154 |
fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} =
|
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
155 |
{qtyp = Morphism.typ phi qtyp,
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
156 |
rtyp = Morphism.typ phi rtyp,
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
157 |
equiv_rel = Morphism.term phi equiv_rel,
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
158 |
equiv_thm = Morphism.thm phi equiv_thm}
|
786
|
159 |
|
875
|
160 |
fun quotdata_lookup_raw thy str = Symtab.lookup (QuotData.get thy) str
|
|
161 |
|
|
162 |
fun quotdata_lookup thy str =
|
786
|
163 |
case Symtab.lookup (QuotData.get thy) str of
|
784
|
164 |
SOME qinfo => qinfo
|
|
165 |
| NONE => raise NotFound
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
166 |
|
786
|
167 |
fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo))
|
|
168 |
fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I
|
264
|
169 |
|
1064
|
170 |
fun quotdata_dest lthy =
|
|
171 |
map snd (Symtab.dest (QuotData.get (ProofContext.theory_of lthy)))
|
|
172 |
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
173 |
fun print_quotinfo ctxt =
|
264
|
174 |
let
|
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
175 |
fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} =
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
176 |
Pretty.block (Library.separate (Pretty.brk 2)
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
177 |
[Pretty.str "quotient type:",
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
178 |
Syntax.pretty_typ ctxt qtyp,
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
179 |
Pretty.str "raw type:",
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
180 |
Syntax.pretty_typ ctxt rtyp,
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
181 |
Pretty.str "relation:",
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
182 |
Syntax.pretty_term ctxt equiv_rel,
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
183 |
Pretty.str "equiv. thm:",
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
184 |
Syntax.pretty_term ctxt (prop_of equiv_thm)])
|
264
|
185 |
in
|
|
186 |
QuotData.get (ProofContext.theory_of ctxt)
|
311
|
187 |
|> Symtab.dest
|
|
188 |
|> map (prt_quot o snd)
|
264
|
189 |
|> Pretty.big_list "quotients:"
|
|
190 |
|> Pretty.writeln
|
|
191 |
end
|
|
192 |
|
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
|
193 |
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
194 |
(* info about quotient constants *)
|
496
|
195 |
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
|
196 |
|
869
ce5f78f0eac5
Finished organising an efficient datastructure for qconst_info.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
197 |
fun qconsts_info_eq (x : qconsts_info, y : qconsts_info) = #qconst x = #qconst y
|
ce5f78f0eac5
Finished organising an efficient datastructure for qconst_info.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
198 |
|
868
09d5b7f0e55d
Undid changes from symtab to termtab, since we need to lookup specialized types.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
199 |
(* We need to be able to lookup instances of lifted constants,
|
09d5b7f0e55d
Undid changes from symtab to termtab, since we need to lookup specialized types.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
200 |
for example given "nat fset" we need to find "'a fset";
|
09d5b7f0e55d
Undid changes from symtab to termtab, since we need to lookup specialized types.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
201 |
but overloaded constants share the same name *)
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
202 |
structure QConstsData = Theory_Data
|
869
ce5f78f0eac5
Finished organising an efficient datastructure for qconst_info.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
203 |
(type T = (qconsts_info list) Symtab.table
|
868
09d5b7f0e55d
Undid changes from symtab to termtab, since we need to lookup specialized types.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
204 |
val empty = Symtab.empty
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
205 |
val extend = I
|
869
ce5f78f0eac5
Finished organising an efficient datastructure for qconst_info.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
206 |
val merge = Symtab.merge_list qconsts_info_eq)
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
207 |
|
799
|
208 |
fun transform_qconsts phi {qconst, rconst, def} =
|
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
209 |
{qconst = Morphism.term phi qconst,
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
210 |
rconst = Morphism.term phi rconst,
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
211 |
def = Morphism.thm phi def}
|
318
|
212 |
|
869
ce5f78f0eac5
Finished organising an efficient datastructure for qconst_info.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
213 |
fun qconsts_update_thy name qcinfo = QConstsData.map (Symtab.cons_list (name, qcinfo))
|
868
09d5b7f0e55d
Undid changes from symtab to termtab, since we need to lookup specialized types.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
214 |
fun qconsts_update_gen name qcinfo = Context.mapping (qconsts_update_thy name qcinfo) I
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
215 |
|
871
|
216 |
fun qconsts_dest lthy =
|
|
217 |
flat (map snd (Symtab.dest (QConstsData.get (ProofContext.theory_of lthy))))
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
218 |
|
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
219 |
fun qconsts_lookup thy t =
|
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
220 |
let
|
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
221 |
val (name, qty) = dest_Const t
|
869
ce5f78f0eac5
Finished organising an efficient datastructure for qconst_info.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
222 |
fun matches x =
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
223 |
let
|
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
224 |
val (name', qty') = dest_Const (#qconst x);
|
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
225 |
in
|
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
226 |
name = name' andalso Sign.typ_instance thy (qty, qty')
|
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
227 |
end
|
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
228 |
in
|
869
ce5f78f0eac5
Finished organising an efficient datastructure for qconst_info.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
229 |
case Symtab.lookup (QConstsData.get thy) name of
|
ce5f78f0eac5
Finished organising an efficient datastructure for qconst_info.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
230 |
NONE => raise NotFound
|
ce5f78f0eac5
Finished organising an efficient datastructure for qconst_info.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
231 |
| SOME l =>
|
ce5f78f0eac5
Finished organising an efficient datastructure for qconst_info.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
232 |
(case (find_first matches l) of
|
ce5f78f0eac5
Finished organising an efficient datastructure for qconst_info.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
233 |
SOME x => x
|
886
|
234 |
| NONE => raise NotFound)
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
235 |
end
|
497
b663bc007d00
Added qoutient_consts dest for getting all the constant definitions in the cleaning step.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
236 |
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
237 |
fun print_qconstinfo ctxt =
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
238 |
let
|
496
|
239 |
fun prt_qconst {qconst, rconst, def} =
|
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
240 |
Pretty.block (separate (Pretty.brk 1)
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
241 |
[Syntax.pretty_term ctxt qconst,
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
242 |
Pretty.str ":=",
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
243 |
Syntax.pretty_term ctxt rconst,
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
244 |
Pretty.str "as",
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
245 |
Syntax.pretty_term ctxt (prop_of def)])
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
246 |
in
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
247 |
QConstsData.get (ProofContext.theory_of ctxt)
|
868
09d5b7f0e55d
Undid changes from symtab to termtab, since we need to lookup specialized types.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
248 |
|> Symtab.dest
|
869
ce5f78f0eac5
Finished organising an efficient datastructure for qconst_info.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
249 |
|> map snd
|
ce5f78f0eac5
Finished organising an efficient datastructure for qconst_info.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
250 |
|> flat
|
ce5f78f0eac5
Finished organising an efficient datastructure for qconst_info.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
251 |
|> map prt_qconst
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
252 |
|> 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
|
253 |
|> Pretty.writeln
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
254 |
end
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
255 |
|
582
|
256 |
(* equivalence relation theorems *)
|
|
257 |
structure EquivRules = Named_Thms
|
636
|
258 |
(val name = "quot_equiv"
|
582
|
259 |
val description = "Equivalence relation theorems.")
|
|
260 |
|
|
261 |
val equiv_rules_get = EquivRules.get
|
|
262 |
val equiv_rules_add = EquivRules.add
|
|
263 |
|
|
264 |
(* respectfulness theorems *)
|
798
|
265 |
structure RspRules = Filtered_Named_Thms
|
636
|
266 |
(val name = "quot_respect"
|
797
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
267 |
val description = "Respectfulness theorems."
|
798
|
268 |
val filter = I)
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
269 |
|
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
270 |
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
|
271 |
|
636
|
272 |
(* preservation theorems *)
|
|
273 |
structure PrsRules = Named_Thms
|
|
274 |
(val name = "quot_preserve"
|
777
2f72662d21f3
added a print_maps command; updated the keyword file accordingly
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
275 |
val description = "Preservation theorems.")
|
636
|
276 |
|
|
277 |
val prs_rules_get = PrsRules.get
|
|
278 |
|
759
|
279 |
(* id simplification theorems *)
|
614
|
280 |
structure IdSimps = Named_Thms
|
|
281 |
(val name = "id_simps"
|
|
282 |
val description = "Identity simp rules for maps.")
|
|
283 |
|
|
284 |
val id_simps_get = IdSimps.get
|
|
285 |
|
582
|
286 |
(* quotient theorems *)
|
503
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
287 |
structure QuotientRules = Named_Thms
|
636
|
288 |
(val name = "quot_thm"
|
503
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
289 |
val description = "Quotient theorems.")
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
290 |
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
291 |
val quotient_rules_get = QuotientRules.get
|
582
|
292 |
val quotient_rules_add = QuotientRules.add
|
503
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
293 |
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
294 |
(* setup of the theorem lists *)
|
778
|
295 |
|
503
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
296 |
val _ = Context.>> (Context.map_theory
|
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
297 |
(EquivRules.setup #>
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
298 |
RspRules.setup #>
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
299 |
PrsRules.setup #>
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
300 |
IdSimps.setup #>
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
301 |
QuotientRules.setup))
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
302 |
|
778
|
303 |
(* setup of the printing commands *)
|
|
304 |
|
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
305 |
fun improper_command (pp_fn, cmd_name, descr_str) =
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
306 |
OuterSyntax.improper_command cmd_name descr_str
|
778
|
307 |
OuterKeyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))
|
|
308 |
|
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
309 |
val _ = map improper_command
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
310 |
[(print_mapsinfo, "print_maps", "prints out all map functions"),
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
311 |
(print_quotinfo, "print_quotients", "prints out all quotients"),
|
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
312 |
(print_qconstinfo, "print_quotconsts", "prints out all quotient constants")]
|
778
|
313 |
|
|
314 |
|
264
|
315 |
end; (* structure *)
|
|
316 |
|