681 |
681 |
682 fun inj_repabs_trm_chk ctxt (rtrm, qtrm) = |
682 fun inj_repabs_trm_chk ctxt (rtrm, qtrm) = |
683 inj_repabs_trm ctxt (rtrm, qtrm) |
683 inj_repabs_trm ctxt (rtrm, qtrm) |
684 |> Syntax.check_term ctxt |
684 |> Syntax.check_term ctxt |
685 |
685 |
686 (* Finds subterms of a term that are lifted to constants and replaces |
686 (*** Translating the goal automatically |
687 those as well as occurrences of the equivalence relation and replaces |
687 |
688 those by equality. |
688 Finds subterms of a term that can be lifted and: |
689 Currently types are not checked so because of the dummyTs it may |
689 * replaces subterms matching lifted constants by the lifted constants |
690 not be complete *) |
690 * replaces equivalence relations by equalities |
|
691 * In constants, frees and schematic variables replaces |
|
692 subtypes matching lifted types by those types *) |
|
693 |
691 fun subst_ty thy ty (rty, qty) r = |
694 fun subst_ty thy ty (rty, qty) r = |
692 if r <> NONE then r else |
695 if r <> NONE then r else |
693 case try (Sign.typ_match thy (ty, rty)) Vartab.empty of |
696 case try (Sign.typ_match thy (ty, rty)) Vartab.empty of |
694 SOME inst => SOME (Envir.subst_type inst qty) |
697 SOME inst => SOME (Envir.subst_type inst qty) |
695 | NONE => NONE |
698 | NONE => NONE |
719 val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos |
722 val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos |
720 in |
723 in |
721 (ty_substs, (const_substs @ rel_substs)) |
724 (ty_substs, (const_substs @ rel_substs)) |
722 end |
725 end |
723 |
726 |
724 |
|
725 fun quotient_lift_all ctxt t = |
727 fun quotient_lift_all ctxt t = |
726 let |
728 let |
727 val thy = ProofContext.theory_of ctxt |
729 val thy = ProofContext.theory_of ctxt |
728 val (ty_substs, substs) = get_ty_trm_substs ctxt |
730 val (ty_substs, substs) = get_ty_trm_substs ctxt |
729 fun lift_aux t = |
731 fun lift_aux t = |
730 case subst_trms thy substs t of |
732 case subst_trms thy substs t of |
731 SOME x => x |
733 SOME x => x |
732 | NONE => |
734 | NONE => |
733 (case t of |
735 (case t of |
734 a $ b => lift_aux a $ lift_aux b |
736 a $ b => lift_aux a $ lift_aux b |
735 | Abs(a, T, s) => |
737 | Abs(a, ty, s) => |
736 let val (y, s') = Term.dest_abs (a, T, s) in |
738 let |
737 Abs(y, dummyT, abstract_over (Free (y, dummyT), (lift_aux s'))) |
739 val (y, s') = Term.dest_abs (a, ty, s) |
|
740 val nty = subst_tys thy ty_substs ty |
|
741 in |
|
742 Abs(y, nty, abstract_over (Free (y, nty), (lift_aux s'))) |
738 end |
743 end |
739 | Free(n, _) => Free(n, dummyT) |
744 | Free(n, ty) => Free(n, subst_tys thy ty_substs ty) |
740 | Var(n, _) => Var(n, dummyT) |
745 | Var(n, ty) => Var(n, subst_tys thy ty_substs ty) |
741 | Bound i => Bound i |
746 | Bound i => Bound i |
742 | Const(s, _) => Const(s, dummyT)) |
747 | Const(s, ty) => Const(s, subst_tys thy ty_substs ty)) |
743 in |
748 in |
744 lift_aux t |
749 lift_aux t |
745 end |
750 end |
746 |
751 |
747 |
752 |
|
753 |
748 end; (* structure *) |
754 end; (* structure *) |
749 |
755 |
750 |
756 |
751 |
757 |