692 (* Finds subterms of a term that are lifted to constants and replaces

   692 (*** Translating the goal automatically

   693    those as well as occurrences of the equivalence relation and replaces

   693 

   694    those by equality.

   694 Finds subterms of a term that can be lifted and:

   695    Currently types are not checked so because of the dummyTs it may

   695 * replaces subterms matching lifted constants by the lifted constants

   696    not be complete *)

   696 * replaces equivalence relations by equalities

   697 * In constants, frees and schematic variables replaces

   698   subtypes matching lifted types by those types *)

   699 

   700 fun subst_ty thy ty (rty, qty) r =

   701   if r <> NONE then r else

   702   case try (Sign.typ_match thy (ty, rty)) Vartab.empty of

   703     SOME inst => SOME (Envir.subst_type inst qty)

   704   | NONE => NONE

   705 fun subst_tys thy substs ty =

   706   case fold (subst_ty thy ty) substs NONE of

   707     SOME ty => ty

   708   | NONE =>

   709       (case ty of

   710         Type (s, tys) => Type (s, map (subst_tys thy substs) tys)

   711       | x => x)

   712 

   713 fun subst_trm thy t (rt, qt) s =

   714   if s <> NONE then s else

   715     case try (Pattern.match thy (t, rt)) (Vartab.empty, Vartab.empty) of

   716       SOME inst => SOME (Envir.subst_term inst qt)

   717     | NONE => NONE;

   718 fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE

   719 

   720 fun get_ty_trm_substs ctxt =

   721 let

   722   val thy = ProofContext.theory_of ctxt

   723   val quot_infos = Quotient_Info.quotdata_dest ctxt

   724   val ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos

   725   val const_infos = Quotient_Info.qconsts_dest ctxt

   726   val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos

   727   fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel)))

   728   val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos

   729 in

   730   (ty_substs, (const_substs @ rel_substs))

   731 end

   732 

   700   val const_infos = Quotient_Info.qconsts_dest ctxt

   736   val (ty_substs, substs) = get_ty_trm_substs ctxt

   701   val rel_infos = Quotient_Info.quotdata_dest ctxt

   702   fun treat_const_info t qc_info s =

   703     if s <> NONE then s else

   704       case try (Pattern.match thy (t, #rconst qc_info)) (Vartab.empty, Vartab.empty) of

   705         SOME inst => SOME (Envir.subst_term inst (#qconst qc_info))

   706       | NONE => NONE;

   707   fun treat_const t = fold (treat_const_info t) const_infos NONE

   708   fun treat_rel_info t rel_info s =

   709     if s <> NONE then s else

   710     if Pattern.matches thy (t, #equiv_rel rel_info) then SOME (Const ("op =", dummyT))

   711     else NONE

   712   fun treat_rel t = fold (treat_rel_info t) rel_infos NONE

   714     case treat_const t of

   738     case subst_trms thy substs t of

   717       (case treat_rel t of

   741       (case t of

   718         SOME x => x

   742         a $ b => lift_aux a $ lift_aux b

   719       | NONE =>

   743       | Abs(a, ty, s) =>

   720         (case t of

   744           let

   721           a $ b => lift_aux a $ lift_aux b

   745             val (y, s') = Term.dest_abs (a, ty, s)

   722         | Abs(a, T, s) =>

   746             val nty = subst_tys thy ty_substs ty

   723             let val (y, s') = Term.dest_abs (a, T, s) in

   747           in

   724             Abs(y, dummyT, abstract_over (Free (y, dummyT), (lift_aux s')))

   748           Abs(y, nty, abstract_over (Free (y, nty), (lift_aux s')))

   725             end

   749           end

   726         | Free(n, _) => Free(n, dummyT)

   750       | Free(n, ty) => Free(n, subst_tys thy ty_substs ty)

   727         | Var(n, _) => Var(n, dummyT)

   751       | Var(n, ty) => Var(n, subst_tys thy ty_substs ty)

   728         | Bound i => Bound i

   752       | Bound i => Bound i

   729         | Const(s, _) => Const(s, dummyT)))

   753       | Const(s, ty) => Const(s, subst_tys thy ty_substs ty))