445 | _ => false |
445 | _ => false |
446 |
446 |
447 *} |
447 *} |
448 |
448 |
449 ML {* |
449 ML {* |
450 (* trm \<Rightarrow> new_trm *) |
|
451 fun regularise trm rty rel lthy = |
|
452 case trm of |
|
453 Abs (x, T, t) => |
|
454 if (needs_lift rty T) then let |
|
455 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
|
456 val v = Free (x', T); |
|
457 val t' = subst_bound (v, t); |
|
458 val rec_term = regularise t' rty rel lthy2; |
|
459 val lam_term = Term.lambda_name (x, v) rec_term; |
|
460 val sub_res_term = tyRel T rty rel lthy; |
|
461 val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool}); |
|
462 val res_term = respects $ sub_res_term; |
|
463 val ty = fastype_of trm; |
|
464 val rabs = Const (@{const_name Babs}, (fastype_of res_term) --> ty --> ty); |
|
465 val rabs_term = (rabs $ res_term) $ lam_term; |
|
466 in |
|
467 rabs_term |
|
468 end else let |
|
469 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
|
470 val v = Free (x', T); |
|
471 val t' = subst_bound (v, t); |
|
472 val rec_term = regularise t' rty rel lthy2; |
|
473 in |
|
474 Term.lambda_name (x, v) rec_term |
|
475 end |
|
476 | ((Const (@{const_name "All"}, at)) $ (Abs (x, T, t))) => |
|
477 if (needs_lift rty T) then let |
|
478 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
|
479 val v = Free (x', T); |
|
480 val t' = subst_bound (v, t); |
|
481 val rec_term = regularise t' rty rel lthy2; |
|
482 val lam_term = Term.lambda_name (x, v) rec_term; |
|
483 val sub_res_term = tyRel T rty rel lthy; |
|
484 val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool}); |
|
485 val res_term = respects $ sub_res_term; |
|
486 val ty = fastype_of lam_term; |
|
487 val rall = Const (@{const_name Ball}, (fastype_of res_term) --> ty --> @{typ bool}); |
|
488 val rall_term = (rall $ res_term) $ lam_term; |
|
489 in |
|
490 rall_term |
|
491 end else let |
|
492 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
|
493 val v = Free (x', T); |
|
494 val t' = subst_bound (v, t); |
|
495 val rec_term = regularise t' rty rel lthy2; |
|
496 val lam_term = Term.lambda_name (x, v) rec_term |
|
497 in |
|
498 Const(@{const_name "All"}, at) $ lam_term |
|
499 end |
|
500 | ((Const (@{const_name "All"}, at)) $ P) => |
|
501 let |
|
502 val (_, [al, _]) = dest_Type (fastype_of P); |
|
503 val ([x], lthy2) = Variable.variant_fixes [""] lthy; |
|
504 val v = (Free (x, al)); |
|
505 val abs = Term.lambda_name (x, v) (P $ v); |
|
506 in regularise ((Const (@{const_name "All"}, at)) $ abs) rty rel lthy2 end |
|
507 | ((Const (@{const_name "Ex"}, at)) $ (Abs (x, T, t))) => |
|
508 if (needs_lift rty T) then let |
|
509 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
|
510 val v = Free (x', T); |
|
511 val t' = subst_bound (v, t); |
|
512 val rec_term = regularise t' rty rel lthy2; |
|
513 val lam_term = Term.lambda_name (x, v) rec_term; |
|
514 val sub_res_term = tyRel T rty rel lthy; |
|
515 val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool}); |
|
516 val res_term = respects $ sub_res_term; |
|
517 val ty = fastype_of lam_term; |
|
518 val rall = Const (@{const_name Bex}, (fastype_of res_term) --> ty --> @{typ bool}); |
|
519 val rall_term = (rall $ res_term) $ lam_term; |
|
520 in |
|
521 rall_term |
|
522 end else let |
|
523 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
|
524 val v = Free (x', T); |
|
525 val t' = subst_bound (v, t); |
|
526 val rec_term = regularise t' rty rel lthy2; |
|
527 val lam_term = Term.lambda_name (x, v) rec_term |
|
528 in |
|
529 Const(@{const_name "Ex"}, at) $ lam_term |
|
530 end |
|
531 | ((Const (@{const_name "Ex"}, at)) $ P) => |
|
532 let |
|
533 val (_, [al, _]) = dest_Type (fastype_of P); |
|
534 val ([x], lthy2) = Variable.variant_fixes [""] lthy; |
|
535 val v = (Free (x, al)); |
|
536 val abs = Term.lambda_name (x, v) (P $ v); |
|
537 in regularise ((Const (@{const_name "Ex"}, at)) $ abs) rty rel lthy2 end |
|
538 | a $ b => (regularise a rty rel lthy) $ (regularise b rty rel lthy) |
|
539 | _ => trm |
|
540 |
|
541 *} |
|
542 |
|
543 (* my version of regularise *) |
|
544 (****************************) |
|
545 |
|
546 (* some helper functions *) |
|
547 |
|
548 |
|
549 ML {* |
|
550 fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty) |
450 fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty) |
551 fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool}) |
451 fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool}) |
552 fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool}) |
452 fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool}) |
553 fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool}) |
453 fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool}) |
554 *} |
454 *} |
564 Term.absfree (x', T, f t') |
464 Term.absfree (x', T, f t') |
565 end |
465 end |
566 | _ => f trm |
466 | _ => f trm |
567 *} |
467 *} |
568 |
468 |
569 |
|
570 (* FIXME: assumes always the typ is qty! *) |
|
571 (* FIXME: if there are more than one quotient, then you have to look up the relation *) |
469 (* FIXME: if there are more than one quotient, then you have to look up the relation *) |
572 ML {* |
470 ML {* |
573 fun my_reg rel trm = |
471 fun my_reg lthy rel rty trm = |
574 case trm of |
472 case trm of |
575 Abs (x, T, t) => |
473 Abs (x, T, t) => |
576 let |
474 if (needs_lift rty T) then |
577 val ty1 = fastype_of trm |
475 let |
578 in |
476 val rrel = tyRel T rty rel lthy |
579 (mk_babs ty1 T) $ (mk_resp T $ rel) $ (apply_subt (my_reg rel) trm) |
477 in |
580 end |
478 (mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ (apply_subt (my_reg lthy rel rty) trm) |
581 | Const (@{const_name "All"}, ty) $ t => |
479 end |
582 let |
480 else |
|
481 Abs(x, T, (apply_subt (my_reg lthy rel rty) t)) |
|
482 | Const (@{const_name "All"}, ty) $ (t as Abs (x, T, _)) => |
|
483 let |
583 val ty1 = domain_type ty |
484 val ty1 = domain_type ty |
584 val ty2 = domain_type ty1 |
485 val ty2 = domain_type ty1 |
|
486 val rrel = tyRel T rty rel lthy |
585 in |
487 in |
586 (mk_ball ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t) |
488 if (needs_lift rty T) then |
|
489 (mk_ball ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t) |
|
490 else |
|
491 Const (@{const_name "All"}, ty) $ apply_subt (my_reg lthy rel rty) t |
587 end |
492 end |
588 | Const (@{const_name "Ex"}, ty) $ t => |
493 | Const (@{const_name "Ex"}, ty) $ (t as Abs (x, T, _)) => |
589 let |
494 let |
590 val ty1 = domain_type ty |
495 val ty1 = domain_type ty |
591 val ty2 = domain_type ty1 |
496 val ty2 = domain_type ty1 |
|
497 val rrel = tyRel T rty rel lthy |
592 in |
498 in |
593 (mk_bex ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t) |
499 if (needs_lift rty T) then |
|
500 (mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t) |
|
501 else |
|
502 Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t |
594 end |
503 end |
595 | t1 $ t2 => (my_reg rel t1) $ (my_reg rel t2) |
504 | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2) |
596 | _ => trm |
505 | _ => trm |
597 *} |
506 *} |
598 |
|
599 |
|
600 (*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this) |
|
601 trm == new_trm |
|
602 *) |
|
603 |
507 |
604 text {* Assumes that the given theorem is atomized *} |
508 text {* Assumes that the given theorem is atomized *} |
605 ML {* |
509 ML {* |
606 fun build_regularize_goal thm rty rel lthy = |
510 fun build_regularize_goal thm rty rel lthy = |
607 Logic.mk_implies |
511 Logic.mk_implies |
608 ((prop_of thm), |
512 ((prop_of thm), |
609 (regularise (prop_of thm) rty rel lthy)) |
513 (my_reg lthy rel rty (prop_of thm))) |
610 *} |
514 *} |
611 |
515 |
612 ML {* |
516 ML {* |
613 fun regularize thm rty rel rel_eqv lthy = |
517 fun regularize thm rty rel rel_eqv lthy = |
614 let |
518 let |