equal
deleted
inserted
replaced
1 signature QUOTIENT_INFO = |
1 signature QUOTIENT_INFO = |
2 sig |
2 sig |
|
3 exception NotFound |
|
4 |
3 type maps_info = {mapfun: string, relfun: string} |
5 type maps_info = {mapfun: string, relfun: string} |
4 val maps_lookup: theory -> string -> maps_info option |
6 val maps_lookup: theory -> string -> maps_info option |
5 val maps_update_thy: string -> maps_info -> theory -> theory |
7 val maps_update_thy: string -> maps_info -> theory -> theory |
6 val maps_update: string -> maps_info -> Proof.context -> Proof.context |
8 val maps_update: string -> maps_info -> Proof.context -> Proof.context |
7 |
9 |
13 val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context |
15 val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context |
14 val quotdata_dest: theory -> quotient_info list |
16 val quotdata_dest: theory -> quotient_info list |
15 |
17 |
16 type qconsts_info = {qconst: term, rconst: term, def: thm} |
18 type qconsts_info = {qconst: term, rconst: term, def: thm} |
17 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
19 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
18 val qconsts_lookup: theory -> string -> qconsts_info option |
20 val qconsts_lookup: theory -> string -> qconsts_info |
19 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
21 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
20 val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
22 val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
21 val qconsts_dest: theory -> qconsts_info list |
23 val qconsts_dest: theory -> qconsts_info list |
22 val print_qconstinfo: Proof.context -> unit |
24 val print_qconstinfo: Proof.context -> unit |
23 |
25 |
27 end; |
29 end; |
28 |
30 |
29 structure Quotient_Info: QUOTIENT_INFO = |
31 structure Quotient_Info: QUOTIENT_INFO = |
30 struct |
32 struct |
31 |
33 |
|
34 exception NotFound |
32 |
35 |
33 (* data containers *) |
36 (* data containers *) |
34 (*******************) |
37 (*******************) |
35 |
38 |
36 (* info about map- and rel-functions *) |
39 (* info about map- and rel-functions *) |
132 fun qconsts_transfer phi {qconst, rconst, def} = |
135 fun qconsts_transfer phi {qconst, rconst, def} = |
133 {qconst = Morphism.term phi qconst, |
136 {qconst = Morphism.term phi qconst, |
134 rconst = Morphism.term phi rconst, |
137 rconst = Morphism.term phi rconst, |
135 def = Morphism.thm phi def} |
138 def = Morphism.thm phi def} |
136 |
139 |
137 val qconsts_lookup = Symtab.lookup o QConstsData.get |
140 fun qconsts_lookup thy str = |
|
141 case Symtab.lookup (QConstsData.get thy) str of |
|
142 SOME info => info |
|
143 | NONE => raise NotFound |
138 |
144 |
139 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo)) |
145 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo)) |
140 fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I |
146 fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I |
141 |
147 |
142 fun qconsts_dest thy = |
148 fun qconsts_dest thy = |