635 |
635 |
636 ML {* |
636 ML {* |
637 (* bound variables need to be treated properly, *) |
637 (* bound variables need to be treated properly, *) |
638 (* as the type of subterms need to be calculated *) |
638 (* as the type of subterms need to be calculated *) |
639 |
639 |
640 fun inj_REPABS lthy (rtrm, qtrm) = |
640 fun inj_repabs_trm lthy (rtrm, qtrm) = |
641 let |
641 let |
642 val rty = fastype_of rtrm |
642 val rty = fastype_of rtrm |
643 val qty = fastype_of qtrm |
643 val qty = fastype_of qtrm |
644 in |
644 in |
645 case (rtrm, qtrm) of |
645 case (rtrm, qtrm) of |
646 (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => |
646 (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => |
647 Const (@{const_name "Ball"}, T) $ r $ (inj_REPABS lthy (t, t')) |
647 Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
648 | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => |
648 | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => |
649 Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t')) |
649 Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
650 | (Const (@{const_name "Babs"}, T) $ r $ t, t') => |
650 | (Const (@{const_name "Babs"}, T) $ r $ t, t') => |
651 Const (@{const_name "Babs"}, T) $ r $ (inj_REPABS lthy (t, t')) |
651 Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
652 | (Abs (x, T, t), Abs (x', T', t')) => |
652 | (Abs (x, T, t), Abs (x', T', t')) => |
653 let |
653 let |
654 val (y, s) = Term.dest_abs (x, T, t) |
654 val (y, s) = Term.dest_abs (x, T, t) |
655 val (_, s') = Term.dest_abs (x', T', t') |
655 val (_, s') = Term.dest_abs (x', T', t') |
656 val yvar = Free (y, T) |
656 val yvar = Free (y, T) |
657 val result = lambda yvar (inj_REPABS lthy (s, s')) |
657 val result = lambda yvar (inj_repabs_trm lthy (s, s')) |
658 in |
658 in |
659 if rty = qty |
659 if rty = qty |
660 then result |
660 then result |
661 else mk_repabs lthy (rty, qty) result |
661 else mk_repabs lthy (rty, qty) result |
662 end |
662 end |
666 (* - constants only get a rep-abs on the outside of the application *) |
666 (* - constants only get a rep-abs on the outside of the application *) |
667 (* - applications get a rep-abs insde and outside an application *) |
667 (* - applications get a rep-abs insde and outside an application *) |
668 let |
668 let |
669 val (rhead, rargs) = strip_comb rtrm |
669 val (rhead, rargs) = strip_comb rtrm |
670 val (qhead, qargs) = strip_comb qtrm |
670 val (qhead, qargs) = strip_comb qtrm |
671 val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs) |
671 val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs) |
672 in |
672 in |
673 if rty = qty |
673 if rty = qty |
674 then |
674 then |
675 case (rhead, qhead) of |
675 case (rhead, qhead) of |
676 (Free (_, T), Free (_, T')) => |
676 (Free (_, T), Free (_, T')) => |
683 | (Free (_, T), Free (_, T'), 0) => mk_repabs lthy (T, T') rhead |
683 | (Free (_, T), Free (_, T'), 0) => mk_repabs lthy (T, T') rhead |
684 | (Const _, Const _, _) => mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) |
684 | (Const _, Const _, _) => mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) |
685 | (Free (x, T), Free (x', T'), _) => |
685 | (Free (x, T), Free (x', T'), _) => |
686 mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs')) |
686 mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs')) |
687 | (Abs _, Abs _, _ ) => |
687 | (Abs _, Abs _, _ ) => |
688 mk_repabs lthy (rty, qty) (list_comb (inj_REPABS lthy (rhead, qhead), rargs')) |
688 mk_repabs lthy (rty, qty) (list_comb (inj_repabs_trm lthy (rhead, qhead), rargs')) |
689 | _ => raise (LIFT_MATCH "injection") |
689 | _ => raise (LIFT_MATCH "injection") |
690 end |
690 end |
691 end |
691 end |
692 *} |
692 *} |
693 |
693 |
1121 val qtrm' = HOLogic.dest_Trueprop qtrm |
1121 val qtrm' = HOLogic.dest_Trueprop qtrm |
1122 val reg_goal = |
1122 val reg_goal = |
1123 Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm') |
1123 Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm') |
1124 handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm |
1124 handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm |
1125 val inj_goal = |
1125 val inj_goal = |
1126 Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm')) |
1126 Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) |
1127 handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm |
1127 handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm |
1128 in |
1128 in |
1129 Drule.instantiate' [] |
1129 Drule.instantiate' [] |
1130 [SOME (cterm_of thy rtrm'), |
1130 [SOME (cterm_of thy rtrm'), |
1131 SOME (cterm_of thy reg_goal), |
1131 SOME (cterm_of thy reg_goal), |