15 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 |
16 val quotdata_dest: theory -> quotient_info list |
16 val quotdata_dest: theory -> quotient_info list |
17 |
17 |
18 type qconsts_info = {qconst: term, rconst: term, def: thm} |
18 type qconsts_info = {qconst: term, rconst: term, def: thm} |
19 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
19 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
20 val qconsts_lookup: theory -> string -> qconsts_info |
20 val qconsts_lookup: theory -> term -> qconsts_info |
21 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
21 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
22 val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
22 val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
23 val qconsts_dest: theory -> qconsts_info list |
23 val qconsts_dest: theory -> qconsts_info list |
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 |
143 fun qconsts_transfer phi {qconst, rconst, def} = |
143 fun qconsts_transfer phi {qconst, rconst, def} = |
144 {qconst = Morphism.term phi qconst, |
144 {qconst = Morphism.term phi qconst, |
145 rconst = Morphism.term phi rconst, |
145 rconst = Morphism.term phi rconst, |
146 def = Morphism.thm phi def} |
146 def = Morphism.thm phi def} |
147 |
147 |
148 fun qconsts_lookup thy str = |
148 fun qconsts_update_thy id qcinfo = QConstsData.map (Symtab.update (id, qcinfo)) |
149 case Symtab.lookup (QConstsData.get thy) str of |
149 fun qconsts_update_gen id qcinfo = Context.mapping (qconsts_update_thy id qcinfo) I |
150 SOME info => info |
|
151 | NONE => raise NotFound |
|
152 |
|
153 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo)) |
|
154 fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I |
|
155 |
150 |
156 fun qconsts_dest thy = |
151 fun qconsts_dest thy = |
157 map snd (Symtab.dest (QConstsData.get thy)) |
152 map snd (Symtab.dest (QConstsData.get thy)) |
|
153 |
|
154 fun qconsts_lookup thy t = |
|
155 let |
|
156 val smt = Symtab.dest (QConstsData.get thy); |
|
157 val (name, qty) = dest_Const t |
|
158 fun matches (_, x) = |
|
159 let |
|
160 val (name', qty') = dest_Const (#qconst x); |
|
161 in |
|
162 name = name' andalso Sign.typ_instance thy (qty, qty') |
|
163 end |
|
164 in |
|
165 case (find_first matches smt) of |
|
166 SOME (_, x) => x |
|
167 | _ => raise NotFound |
|
168 end |
158 |
169 |
159 (* We don't print the definition *) |
170 (* We don't print the definition *) |
160 fun print_qconstinfo ctxt = |
171 fun print_qconstinfo ctxt = |
161 let |
172 let |
162 fun prt_qconst {qconst, rconst, def} = |
173 fun prt_qconst {qconst, rconst, def} = |