equal
deleted
inserted
replaced
638 |
638 |
639 (* applies f to the subterm of an abstractions, otherwise to the given term *) |
639 (* applies f to the subterm of an abstractions, otherwise to the given term *) |
640 ML {* |
640 ML {* |
641 fun apply_subt f trm = |
641 fun apply_subt f trm = |
642 case trm of |
642 case trm of |
643 Abs (x, T, t) => Abs (x, T, f t) |
643 Abs (x, T, t) => |
|
644 let |
|
645 val (x', t') = Term.dest_abs (x, T, t) |
|
646 in |
|
647 Term.absfree (x', T, f t') |
|
648 end |
644 | _ => f trm |
649 | _ => f trm |
645 *} |
650 *} |
646 |
651 |
647 |
652 |
648 (* FIXME: assumes always the typ is qty! *) |
653 (* FIXME: assumes always the typ is qty! *) |
652 case trm of |
657 case trm of |
653 Abs (x, T, t) => |
658 Abs (x, T, t) => |
654 let |
659 let |
655 val ty1 = fastype_of trm |
660 val ty1 = fastype_of trm |
656 in |
661 in |
657 (mk_babs ty1 T) $ (mk_resp T $ rel) $ (Abs (x, T, my_reg rel t)) |
662 (mk_babs ty1 T) $ (mk_resp T $ rel) $ (apply_subt (my_reg rel) (Abs (x, T, t))) |
658 end |
663 end |
659 | Const (@{const_name "All"}, ty) $ t => |
664 | Const (@{const_name "All"}, ty) $ t => |
660 let |
665 let |
661 val ty1 = domain_type ty |
666 val ty1 = domain_type ty |
662 val ty2 = domain_type ty1 |
667 val ty2 = domain_type ty1 |
670 in |
675 in |
671 (mk_bex ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t) |
676 (mk_bex ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t) |
672 end |
677 end |
673 | t1 $ t2 => (my_reg rel t1) $ (my_reg rel t2) |
678 | t1 $ t2 => (my_reg rel t1) $ (my_reg rel t2) |
674 | _ => trm |
679 | _ => trm |
|
680 *} |
|
681 |
|
682 ML {* |
|
683 cterm_of @{theory} (regularise @{term "\<exists>(y::trm). P (\<lambda>(x::trm). y)"} @{typ "trm"} |
|
684 @{term "RR"} @{context}); |
|
685 cterm_of @{theory} (my_reg @{term "RR"} @{term "\<exists>(y::trm). P (\<lambda>(x::trm). y)"}) |
675 *} |
686 *} |
676 |
687 |
677 ML {* |
688 ML {* |
678 cterm_of @{theory} (regularise @{term "\<lambda>x::trm. x"} @{typ "trm"} @{term "RR"} @{context}); |
689 cterm_of @{theory} (regularise @{term "\<lambda>x::trm. x"} @{typ "trm"} @{term "RR"} @{context}); |
679 cterm_of @{theory} (my_reg @{term "RR"} @{term "\<lambda>x::trm. x"}) |
690 cterm_of @{theory} (my_reg @{term "RR"} @{term "\<lambda>x::trm. x"}) |