equal
deleted
inserted
replaced
287 val _ = check_rty_type ctxt rty quot_thm |
287 val _ = check_rty_type ctxt rty quot_thm |
288 in |
288 in |
289 quot_thm |
289 quot_thm |
290 end |
290 end |
291 |
291 |
|
292 (* |
|
293 Computes the composed abstraction function for rty and qty. |
|
294 *) |
|
295 |
292 fun abs_fun ctxt (rty, qty) = |
296 fun abs_fun ctxt (rty, qty) = |
293 quot_thm_abs (prove_quot_thm ctxt (rty, qty)) |
297 quot_thm_abs (prove_quot_thm ctxt (rty, qty)) |
|
298 |
|
299 (* |
|
300 Computes the composed equivalence relation for rty and qty. |
|
301 *) |
294 |
302 |
295 fun equiv_relation ctxt (rty, qty) = |
303 fun equiv_relation ctxt (rty, qty) = |
296 quot_thm_rel (prove_quot_thm ctxt (rty, qty)) |
304 quot_thm_rel (prove_quot_thm ctxt (rty, qty)) |
297 |
305 |
298 val get_fresh_Q_t = |
306 val get_fresh_Q_t = |
321 val renamed_Q_t = rename_free_tvars tab_tfrees renamed_Q_t |
329 val renamed_Q_t = rename_free_tvars tab_tfrees renamed_Q_t |
322 in |
330 in |
323 (renamed_Q_t, ctxt) |
331 (renamed_Q_t, ctxt) |
324 end |
332 end |
325 end |
333 end |
|
334 |
|
335 (* |
|
336 For the given type, it proves a composed Quotient map theorem, where for each type variable |
|
337 extra Quotient assumption is generated. E.g., for 'a list it generates exactly |
|
338 the Quotient map theorem for the list type. The function generalizes this for the whole |
|
339 type universe. New fresh variables in the assumptions are fixed in the returned context. |
|
340 |
|
341 Returns: the composed Quotient map theorem and list mapping each type variable in ty |
|
342 to the corresponding assumption in the returned theorem. |
|
343 *) |
326 |
344 |
327 fun prove_param_quot_thm ctxt ty = |
345 fun prove_param_quot_thm ctxt ty = |
328 let |
346 let |
329 fun generate (ty as Type (s, tys)) (table_ctxt as (table, ctxt)) = |
347 fun generate (ty as Type (s, tys)) (table_ctxt as (table, ctxt)) = |
330 if null tys |
348 if null tys |
358 in |
376 in |
359 (param_quot_thm, rev table, ctxt) |
377 (param_quot_thm, rev table, ctxt) |
360 end |
378 end |
361 handle QUOT_THM_INTERNAL pretty_msg => raise PARAM_QUOT_THM (ty, pretty_msg) |
379 handle QUOT_THM_INTERNAL pretty_msg => raise PARAM_QUOT_THM (ty, pretty_msg) |
362 |
380 |
|
381 (* |
|
382 It computes a parametrized relator for the given type ty. E.g., for 'a dlist: |
|
383 list_all2 ?R OO cr_dlist with parameters [?R]. |
|
384 |
|
385 Returns: the definitional term and list of parameters (relations). |
|
386 *) |
|
387 |
363 fun generate_parametrized_relator ctxt ty = |
388 fun generate_parametrized_relator ctxt ty = |
364 let |
389 let |
365 val orig_ctxt = ctxt |
390 val orig_ctxt = ctxt |
366 val (quot_thm, table, ctxt) = prove_param_quot_thm ctxt ty |
391 val (quot_thm, table, ctxt) = prove_param_quot_thm ctxt ty |
367 val parametrized_relator = quot_thm_crel quot_thm |
392 val parametrized_relator = quot_thm_crel quot_thm |
410 | SOME v => map_interrupt' f xs (v::l)) |
435 | SOME v => map_interrupt' f xs (v::l)) |
411 in |
436 in |
412 map_interrupt' f l [] |
437 map_interrupt' f l [] |
413 end |
438 end |
414 in |
439 in |
|
440 |
|
441 (* |
|
442 ctm - of the form (par_R OO T) t f, where par_R is a parametricity transfer relation for t |
|
443 and T is a transfer relation between t and f. |
|
444 |
|
445 The function merges par_R OO T using definitions of parametrized correspondence relations |
|
446 (e.g., rel_T R OO cr_T == pcr_T R). |
|
447 *) |
|
448 |
415 fun merge_transfer_relations ctxt ctm = |
449 fun merge_transfer_relations ctxt ctm = |
416 let |
450 let |
417 val ctm = Thm.dest_arg ctm |
451 val ctm = Thm.dest_arg ctm |
418 val tm = term_of ctm |
452 val tm = term_of ctm |
419 val rel = (hd o get_args 2) tm |
453 val rel = (hd o get_args 2) tm |
486 end |
520 end |
487 end |
521 end |
488 handle QUOT_THM_INTERNAL pretty_msg => raise MERGE_TRANSFER_REL pretty_msg |
522 handle QUOT_THM_INTERNAL pretty_msg => raise MERGE_TRANSFER_REL pretty_msg |
489 end |
523 end |
490 |
524 |
|
525 (* |
|
526 It replaces cr_T by pcr_T op= in the transfer relation. For composed |
|
527 abstract types, it replaces T_rel R OO cr_T by pcr_T R. If the parametrized |
|
528 correspondce relation does not exist, the original relation is kept. |
|
529 |
|
530 thm - a transfer rule |
|
531 *) |
|
532 |
491 fun parametrize_transfer_rule ctxt thm = |
533 fun parametrize_transfer_rule ctxt thm = |
492 let |
534 let |
493 fun parametrize_relation_conv ctm = |
535 fun parametrize_relation_conv ctm = |
494 let |
536 let |
495 val (rty, qty) = (relation_types o fastype_of) (term_of ctm) |
537 val (rty, qty) = (relation_types o fastype_of) (term_of ctm) |