23 val regularize_trm: Proof.context -> term * term -> term |
23 val regularize_trm: Proof.context -> term * term -> term |
24 val regularize_trm_chk: Proof.context -> term * term -> term |
24 val regularize_trm_chk: Proof.context -> term * term -> term |
25 |
25 |
26 val inj_repabs_trm: Proof.context -> term * term -> term |
26 val inj_repabs_trm: Proof.context -> term * term -> term |
27 val inj_repabs_trm_chk: Proof.context -> term * term -> term |
27 val inj_repabs_trm_chk: Proof.context -> term * term -> term |
|
28 |
|
29 val quotient_lift_all: Proof.context -> term -> term |
28 end; |
30 end; |
29 |
31 |
30 structure Quotient_Term: QUOTIENT_TERM = |
32 structure Quotient_Term: QUOTIENT_TERM = |
31 struct |
33 struct |
32 |
34 |
679 |
681 |
680 fun inj_repabs_trm_chk ctxt (rtrm, qtrm) = |
682 fun inj_repabs_trm_chk ctxt (rtrm, qtrm) = |
681 inj_repabs_trm ctxt (rtrm, qtrm) |
683 inj_repabs_trm ctxt (rtrm, qtrm) |
682 |> Syntax.check_term ctxt |
684 |> Syntax.check_term ctxt |
683 |
685 |
|
686 (* Finds subterms of a term that are lifted to constants and replaces |
|
687 those as well as occurrences of the equivalence relation and replaces |
|
688 those by equality. |
|
689 Currently types are not checked so because of the dummyTs it may |
|
690 not be complete *) |
|
691 fun quotient_lift_all ctxt t = |
|
692 let |
|
693 val thy = ProofContext.theory_of ctxt |
|
694 val const_infos = Quotient_Info.qconsts_dest ctxt |
|
695 val rel_infos = Quotient_Info.quotdata_dest ctxt |
|
696 fun treat_const_info t qc_info s = |
|
697 if s <> NONE then s else |
|
698 case try (Pattern.match thy (t, #rconst qc_info)) (Vartab.empty, Vartab.empty) of |
|
699 SOME inst => SOME (Envir.subst_term inst (#qconst qc_info)) |
|
700 | NONE => NONE; |
|
701 fun treat_const t = fold (treat_const_info t) const_infos NONE |
|
702 fun treat_rel_info t rel_info s = |
|
703 if s <> NONE then s else |
|
704 if Pattern.matches thy (t, #equiv_rel rel_info) then SOME (Const ("op =", dummyT)) |
|
705 else NONE |
|
706 fun treat_rel t = fold (treat_rel_info t) rel_infos NONE |
|
707 fun lift_aux t = |
|
708 case treat_const t of |
|
709 SOME x => x |
|
710 | NONE => |
|
711 (case treat_rel t of |
|
712 SOME x => x |
|
713 | NONE => |
|
714 (case t of |
|
715 a $ b => lift_aux a $ lift_aux b |
|
716 | Abs(a, T, s) => |
|
717 let val (y, s') = Term.dest_abs (a, T, s) in |
|
718 Abs(y, dummyT, abstract_over (Free (y, dummyT), (lift_aux s'))) |
|
719 end |
|
720 | Free(n, _) => Free(n, dummyT) |
|
721 | Var(n, _) => Var(n, dummyT) |
|
722 | Bound i => Bound i |
|
723 | Const(s, _) => Const(s, dummyT))) |
|
724 in |
|
725 lift_aux t |
|
726 end |
|
727 |
684 end; (* structure *) |
728 end; (* structure *) |
685 |
729 |
686 |
730 |
687 |
731 |