145 |
145 |
146 section {* type definition for the quotient type *} |
146 section {* type definition for the quotient type *} |
147 |
147 |
148 use "quotient.ML" |
148 use "quotient.ML" |
149 |
149 |
150 term EQUIV |
150 (* mapfuns for some standard types *) |
|
151 setup {* |
|
152 maps_update @{type_name "list"} {mapfun = @{const_name "map"}, relfun = @{const_name "LIST_REL"}} #> |
|
153 maps_update @{type_name "*"} {mapfun = @{const_name "prod_fun"}, relfun = @{const_name "prod_rel"}} #> |
|
154 maps_update @{type_name "fun"} {mapfun = @{const_name "fun_map"}, relfun = @{const_name "FUN_REL"}} |
|
155 *} |
|
156 |
|
157 |
|
158 ML {* maps_lookup @{theory} @{type_name list} *} |
151 |
159 |
152 ML {* |
160 ML {* |
153 val no_vars = Thm.rule_attribute (fn context => fn th => |
161 val no_vars = Thm.rule_attribute (fn context => fn th => |
154 let |
162 let |
155 val ctxt = Variable.set_body false (Context.proof_of context); |
163 val ctxt = Variable.set_body false (Context.proof_of context); |
223 quotient qt = "t" / "Rt" |
231 quotient qt = "t" / "Rt" |
224 by (rule t_eq) |
232 by (rule t_eq) |
225 |
233 |
226 section {* lifting of constants *} |
234 section {* lifting of constants *} |
227 |
235 |
228 text {* information about map-functions for type-constructor *} |
|
229 ML {* |
|
230 type typ_info = {mapfun: string, relfun: string} |
|
231 |
|
232 local |
|
233 structure Data = TheoryDataFun |
|
234 (type T = typ_info Symtab.table |
|
235 val empty = Symtab.empty |
|
236 val copy = I |
|
237 val extend = I |
|
238 fun merge _ = Symtab.merge (K true)) |
|
239 in |
|
240 val lookup = Symtab.lookup o Data.get |
|
241 fun update k v = Data.map (Symtab.update (k, v)) |
|
242 end |
|
243 *} |
|
244 |
|
245 (* mapfuns for some standard types *) |
|
246 setup {* |
|
247 update @{type_name "list"} {mapfun = @{const_name "map"}, relfun = @{const_name "LIST_REL"}} #> |
|
248 update @{type_name "*"} {mapfun = @{const_name "prod_fun"}, relfun = @{const_name "prod_rel"}} #> |
|
249 update @{type_name "fun"} {mapfun = @{const_name "fun_map"}, relfun = @{const_name "FUN_REL"}} |
|
250 *} |
|
251 |
|
252 |
|
253 ML {* lookup @{theory} @{type_name list} *} |
|
254 |
|
255 ML {* |
236 ML {* |
256 (* calculates the aggregate abs and rep functions for a given type; |
237 (* calculates the aggregate abs and rep functions for a given type; |
257 repF is for constants' arguments; absF is for constants; |
238 repF is for constants' arguments; absF is for constants; |
258 function types need to be treated specially, since repF and absF |
239 function types need to be treated specially, since repF and absF |
259 change |
240 change |
273 val (otys, ntys) = split_list tys |
254 val (otys, ntys) = split_list tys |
274 val oty = Type (s, otys) |
255 val oty = Type (s, otys) |
275 val nty = Type (s, ntys) |
256 val nty = Type (s, ntys) |
276 val ftys = map (op -->) tys |
257 val ftys = map (op -->) tys |
277 in |
258 in |
278 (case (lookup (ProofContext.theory_of lthy) s) of |
259 (case (maps_lookup (ProofContext.theory_of lthy) s) of |
279 SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty)) |
260 SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty)) |
280 | NONE => raise ERROR ("no map association for type " ^ s)) |
261 | NONE => raise ERROR ("no map association for type " ^ s)) |
281 end |
262 end |
282 |
263 |
283 fun get_fun_fun fs_tys = |
264 fun get_fun_fun fs_tys = |
1005 let |
986 let |
1006 val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys; |
987 val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys; |
1007 val ty_out = ty --> ty --> @{typ bool}; |
988 val ty_out = ty --> ty --> @{typ bool}; |
1008 val tys_out = tys_rel ---> ty_out; |
989 val tys_out = tys_rel ---> ty_out; |
1009 in |
990 in |
1010 (case (lookup (ProofContext.theory_of lthy) s) of |
991 (case (maps_lookup (ProofContext.theory_of lthy) s) of |
1011 SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys) |
992 SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys) |
1012 | NONE => HOLogic.eq_const ty |
993 | NONE => HOLogic.eq_const ty |
1013 ) |
994 ) |
1014 end |
995 end |
1015 | _ => HOLogic.eq_const ty) |
996 | _ => HOLogic.eq_const ty) |