diff -r f89ee40fbb08 -r 78d828f43cdf Attic/Quot/quotient_term.ML --- a/Attic/Quot/quotient_term.ML Sat Dec 17 16:57:25 2011 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,780 +0,0 @@ -(* Title: HOL/Tools/Quotient/quotient_term.thy - Author: Cezary Kaliszyk and Christian Urban - -Constructs terms corresponding to goals from lifting theorems to -quotient types. -*) - -signature QUOTIENT_TERM = -sig - datatype flag = AbsF | RepF - - val absrep_fun: flag -> Proof.context -> typ * typ -> term - val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term - - (* Allows Nitpick to represent quotient types as single elements from raw type *) - val absrep_const_chk: flag -> Proof.context -> string -> term - - val equiv_relation: Proof.context -> typ * typ -> term - val equiv_relation_chk: Proof.context -> typ * typ -> term - - val regularize_trm: Proof.context -> term * term -> term - val regularize_trm_chk: Proof.context -> term * term -> term - - val inj_repabs_trm: Proof.context -> term * term -> term - val inj_repabs_trm_chk: Proof.context -> term * term -> term - - val quotient_lift_const: string * term -> local_theory -> term - val quotient_lift_all: Proof.context -> term -> term -end; - -structure Quotient_Term: QUOTIENT_TERM = -struct - -open Quotient_Info; - -exception LIFT_MATCH of string - - - -(*** Aggregate Rep/Abs Function ***) - - -(* The flag RepF is for types in negative position; AbsF is for types - in positive position. Because of this, function types need to be - treated specially, since there the polarity changes. -*) - -datatype flag = AbsF | RepF - -fun negF AbsF = RepF - | negF RepF = AbsF - -fun is_identity (Const (@{const_name "id"}, _)) = true - | is_identity _ = false - -fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) - -fun mk_fun_compose flag (trm1, trm2) = - case flag of - AbsF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 - | RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 - -fun get_mapfun ctxt s = -let - val thy = ProofContext.theory_of ctxt - val exn = error ("No map function for type " ^ quote s ^ " found.") - val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn -in - Const (mapfun, dummyT) -end - -(* makes a Free out of a TVar *) -fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT) - -(* produces an aggregate map function for the - rty-part of a quotient definition; abstracts - over all variables listed in vs (these variables - correspond to the type variables in rty) - - for example for: (?'a list * ?'b) - it produces: %a b. prod_map (map a) b -*) -fun mk_mapfun ctxt vs rty = -let - val vs' = map (mk_Free) vs - - fun mk_mapfun_aux rty = - case rty of - TVar _ => mk_Free rty - | Type (_, []) => mk_identity rty - | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys) - | _ => raise (error "mk_mapfun (default)") -in - fold_rev Term.lambda vs' (mk_mapfun_aux rty) -end - -(* looks up the (varified) rty and qty for - a quotient definition -*) -fun get_rty_qty ctxt s = -let - val thy = ProofContext.theory_of ctxt - val exn = error ("No quotient type " ^ quote s ^ " found.") - val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn -in - (#rtyp qdata, #qtyp qdata) -end - -(* takes two type-environments and looks - up in both of them the variable v, which - must be listed in the environment -*) -fun double_lookup rtyenv qtyenv v = -let - val v' = fst (dest_TVar v) -in - (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v'))) -end - -(* matches a type pattern with a type *) -fun match ctxt err ty_pat ty = -let - val thy = ProofContext.theory_of ctxt -in - Sign.typ_match thy (ty_pat, ty) Vartab.empty - handle MATCH_TYPE => err ctxt ty_pat ty -end - -(* produces the rep or abs constant for a qty *) -fun absrep_const flag ctxt qty_str = -let - val thy = ProofContext.theory_of ctxt - val qty_name = Long_Name.base_name qty_str -in - case flag of - AbsF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) - | RepF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) -end - -(* Lets Nitpick represent elements of quotient types as elements of the raw type *) -fun absrep_const_chk flag ctxt qty_str = - Syntax.check_term ctxt (absrep_const flag ctxt qty_str) - -fun absrep_match_err ctxt ty_pat ty = -let - val ty_pat_str = Syntax.string_of_typ ctxt ty_pat - val ty_str = Syntax.string_of_typ ctxt ty -in - raise error (cat_lines - ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) -end - - -(** generation of an aggregate absrep function **) - -(* - In case of equal types we just return the identity. - - - In case of TFrees we also return the identity. - - - In case of function types we recurse taking - the polarity change into account. - - - If the type constructors are equal, we recurse for the - arguments and build the appropriate map function. - - - If the type constructors are unequal, there must be an - instance of quotient types: - - - we first look up the corresponding rty_pat and qty_pat - from the quotient definition; the arguments of qty_pat - must be some distinct TVars - - we then match the rty_pat with rty and qty_pat with qty; - if matching fails the types do not correspond -> error - - the matching produces two environments; we look up the - assignments for the qty_pat variables and recurse on the - assignments - - we prefix the aggregate map function for the rty_pat, - which is an abstraction over all type variables - - finally we compose the result with the appropriate - absrep function in case at least one argument produced - a non-identity function / - otherwise we just return the appropriate absrep - function - - The composition is necessary for types like - - ('a list) list / ('a foo) foo - - The matching is necessary for types like - - ('a * 'a) list / 'a bar - - The test is necessary in order to eliminate superfluous - identity maps. -*) - -fun absrep_fun flag ctxt (rty, qty) = - if rty = qty - then mk_identity rty - else - case (rty, qty) of - (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => - let - val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1') - val arg2 = absrep_fun flag ctxt (ty2, ty2') - in - list_comb (get_mapfun ctxt "fun", [arg1, arg2]) - end - | (Type (s, tys), Type (s', tys')) => - if s = s' - then - let - val args = map (absrep_fun flag ctxt) (tys ~~ tys') - in - list_comb (get_mapfun ctxt s, args) - end - else - let - val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' - val rtyenv = match ctxt absrep_match_err rty_pat rty - val qtyenv = match ctxt absrep_match_err qty_pat qty - val args_aux = map (double_lookup rtyenv qtyenv) vs - val args = map (absrep_fun flag ctxt) args_aux - val map_fun = mk_mapfun ctxt vs rty_pat - val result = list_comb (map_fun, args) - in - (*if forall is_identity args - then absrep_const flag ctxt s' - else*) mk_fun_compose flag (absrep_const flag ctxt s', result) - end - | (TFree x, TFree x') => - if x = x' - then mk_identity rty - else raise (error "absrep_fun (frees)") - | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)") - | _ => raise (error "absrep_fun (default)") - -fun absrep_fun_chk flag ctxt (rty, qty) = - absrep_fun flag ctxt (rty, qty) - |> Syntax.check_term ctxt - - - - -(*** Aggregate Equivalence Relation ***) - - -(* works very similar to the absrep generation, - except there is no need for polarities -*) - -(* instantiates TVars so that the term is of type ty *) -fun force_typ ctxt trm ty = -let - val thy = ProofContext.theory_of ctxt - val trm_ty = fastype_of trm - val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty -in - map_types (Envir.subst_type ty_inst) trm -end - -fun is_eq (Const (@{const_name "op ="}, _)) = true - | is_eq _ = false - -fun mk_rel_compose (trm1, trm2) = - Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2 - -fun get_relmap ctxt s = -let - val thy = ProofContext.theory_of ctxt - val exn = error ("get_relmap (no relation map function found for type " ^ s ^ ")") - val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn -in - Const (relmap, dummyT) -end - -fun mk_relmap ctxt vs rty = -let - val vs' = map (mk_Free) vs - - fun mk_relmap_aux rty = - case rty of - TVar _ => mk_Free rty - | Type (_, []) => HOLogic.eq_const rty - | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys) - | _ => raise (error "mk_relmap (default)") -in - fold_rev Term.lambda vs' (mk_relmap_aux rty) -end - -fun get_equiv_rel ctxt s = -let - val thy = ProofContext.theory_of ctxt - val exn = error ("get_quotdata (no quotient found for type " ^ s ^ ")") -in - #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn -end - -fun equiv_match_err ctxt ty_pat ty = -let - val ty_pat_str = Syntax.string_of_typ ctxt ty_pat - val ty_str = Syntax.string_of_typ ctxt ty -in - raise error (space_implode " " - ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) -end - -(* builds the aggregate equivalence relation - that will be the argument of Respects -*) -fun equiv_relation ctxt (rty, qty) = - if rty = qty - then HOLogic.eq_const rty - else - case (rty, qty) of - (Type (s, tys), Type (s', tys')) => - if s = s' - then - let - val args = map (equiv_relation ctxt) (tys ~~ tys') - in - list_comb (get_relmap ctxt s, args) - end - else - let - val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' - val rtyenv = match ctxt equiv_match_err rty_pat rty - val qtyenv = match ctxt equiv_match_err qty_pat qty - val args_aux = map (double_lookup rtyenv qtyenv) vs - val args = map (equiv_relation ctxt) args_aux - val rel_map = mk_relmap ctxt vs rty_pat - val result = list_comb (rel_map, args) - val eqv_rel = get_equiv_rel ctxt s' - val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) - in - if forall is_eq args - then eqv_rel' - else mk_rel_compose (result, eqv_rel') - end - | _ => HOLogic.eq_const rty - -fun equiv_relation_chk ctxt (rty, qty) = - equiv_relation ctxt (rty, qty) - |> Syntax.check_term ctxt - - - -(*** Regularization ***) - -(* Regularizing an rtrm means: - - - Quantifiers over types that need lifting are replaced - by bounded quantifiers, for example: - - All P ----> All (Respects R) P - - where the aggregate relation R is given by the rty and qty; - - - Abstractions over types that need lifting are replaced - by bounded abstractions, for example: - - %x. P ----> Ball (Respects R) %x. P - - - Equalities over types that need lifting are replaced by - corresponding equivalence relations, for example: - - A = B ----> R A B - - or - - A = B ----> (R ===> R) A B - - for more complicated types of A and B - - - The regularize_trm accepts raw theorems in which equalities - and quantifiers match exactly the ones in the lifted theorem - but also accepts partially regularized terms. - - This means that the raw theorems can have: - Ball (Respects R), Bex (Respects R), Bex1_rel (Respects R), Babs, R - in the places where: - All, Ex, Ex1, %, (op =) - is required the lifted theorem. - -*) - -val mk_babs = Const (@{const_name Babs}, dummyT) -val mk_ball = Const (@{const_name Ball}, dummyT) -val mk_bex = Const (@{const_name Bex}, dummyT) -val mk_bex1_rel = Const (@{const_name Bex1_rel}, dummyT) -val mk_resp = Const (@{const_name Respects}, dummyT) - -(* - applies f to the subterm of an abstraction, - otherwise to the given term, - - used by regularize, therefore abstracted - variables do not have to be treated specially -*) -fun apply_subt f (trm1, trm2) = - case (trm1, trm2) of - (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t')) - | _ => f (trm1, trm2) - -fun term_mismatch str ctxt t1 t2 = -let - val t1_str = Syntax.string_of_term ctxt t1 - val t2_str = Syntax.string_of_term ctxt t2 - val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1) - val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2) -in - raise error (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str]) -end - -(* the major type of All and Ex quantifiers *) -fun qnt_typ ty = domain_type (domain_type ty) - -(* Checks that two types match, for example: - rty -> rty matches qty -> qty *) -fun matches_typ thy rT qT = - if rT = qT then true else - case (rT, qT) of - (Type (rs, rtys), Type (qs, qtys)) => - if rs = qs then - if length rtys <> length qtys then false else - forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys) - else - (case Quotient_Info.quotdata_lookup_raw thy qs of - SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo) - | NONE => false) - | _ => false - - -(* produces a regularized version of rtrm - - - the result might contain dummyTs - - - for regularisation we do not need any - special treatment of bound variables -*) -fun regularize_trm ctxt (rtrm, qtrm) = - case (rtrm, qtrm) of - (Abs (x, ty, t), Abs (_, ty', t')) => - let - val subtrm = Abs(x, ty, regularize_trm ctxt (t, t')) - in - if ty = ty' then subtrm - else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm - end - | (Const (@{const_name "Babs"}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) => - let - val subtrm = regularize_trm ctxt (t, t') - val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty') - in - if resrel <> needres - then term_mismatch "regularize (Babs)" ctxt resrel needres - else mk_babs $ resrel $ subtrm - end - - | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => - let - val subtrm = apply_subt (regularize_trm ctxt) (t, t') - in - if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm - else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm - end - - | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => - let - val subtrm = apply_subt (regularize_trm ctxt) (t, t') - in - if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm - else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm - end - - | (Const (@{const_name "Ex1"}, ty) $ (Abs (_, _, - (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op :"}, _) $ _ $ - (Const (@{const_name "Respects"}, _) $ resrel)) $ (t $ _)))), - Const (@{const_name "Ex1"}, ty') $ t') => - let - val t_ = incr_boundvars (~1) t - val subtrm = apply_subt (regularize_trm ctxt) (t_, t') - val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') - in - if resrel <> needrel - then term_mismatch "regularize (Bex1)" ctxt resrel needrel - else mk_bex1_rel $ resrel $ subtrm - end - - | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') => - let - val subtrm = apply_subt (regularize_trm ctxt) (t, t') - in - if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm - else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm - end - - | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, - Const (@{const_name "All"}, ty') $ t') => - let - val subtrm = apply_subt (regularize_trm ctxt) (t, t') - val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') - in - if resrel <> needrel - then term_mismatch "regularize (Ball)" ctxt resrel needrel - else mk_ball $ (mk_resp $ resrel) $ subtrm - end - - | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, - Const (@{const_name "Ex"}, ty') $ t') => - let - val subtrm = apply_subt (regularize_trm ctxt) (t, t') - val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') - in - if resrel <> needrel - then term_mismatch "regularize (Bex)" ctxt resrel needrel - else mk_bex $ (mk_resp $ resrel) $ subtrm - end - - | (Const (@{const_name "Bex1_rel"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') => - let - val subtrm = apply_subt (regularize_trm ctxt) (t, t') - val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') - in - if resrel <> needrel - then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel - else mk_bex1_rel $ resrel $ subtrm - end - - | (* equalities need to be replaced by appropriate equivalence relations *) - (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => - if ty = ty' then rtrm - else equiv_relation ctxt (domain_type ty, domain_type ty') - - | (* in this case we just check whether the given equivalence relation is correct *) - (rel, Const (@{const_name "op ="}, ty')) => - let - val rel_ty = fastype_of rel - val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') - in - if rel' aconv rel then rtrm - else term_mismatch "regularise (relation mismatch)" ctxt rel rel' - end - - | (_, Const _) => - let - val thy = ProofContext.theory_of ctxt - fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ thy T T' - | same_const _ _ = false - in - if same_const rtrm qtrm then rtrm - else - let - val rtrm' = #rconst (qconsts_lookup thy qtrm) - handle Quotient_Info.NotFound => term_mismatch "regularize(constant notfound)" ctxt rtrm qtrm - in - if Pattern.matches thy (rtrm', rtrm) - then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm - end - end - - | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))), - ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) => - regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2))) - - | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, s1)), - ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , s2))) => - regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2)) - - | (t1 $ t2, t1' $ t2') => - regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2') - - | (Bound i, Bound i') => - if i = i' then rtrm - else raise (error "regularize (bounds mismatch)") - - | _ => - let - val rtrm_str = Syntax.string_of_term ctxt rtrm - val qtrm_str = Syntax.string_of_term ctxt qtrm - in - raise (error ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")")) - end - -fun regularize_trm_chk ctxt (rtrm, qtrm) = - regularize_trm ctxt (rtrm, qtrm) - |> Syntax.check_term ctxt - - - -(*** Rep/Abs Injection ***) - -(* -Injection of Rep/Abs means: - - For abstractions: - - * If the type of the abstraction needs lifting, then we add Rep/Abs - around the abstraction; otherwise we leave it unchanged. - - For applications: - - * If the application involves a bounded quantifier, we recurse on - the second argument. If the application is a bounded abstraction, - we always put an Rep/Abs around it (since bounded abstractions - are assumed to always need lifting). Otherwise we recurse on both - arguments. - - For constants: - - * If the constant is (op =), we leave it always unchanged. - Otherwise the type of the constant needs lifting, we put - and Rep/Abs around it. - - For free variables: - - * We put a Rep/Abs around it if the type needs lifting. - - Vars case cannot occur. -*) - -fun mk_repabs ctxt (T, T') trm = - absrep_fun RepF ctxt (T, T') $ (absrep_fun AbsF ctxt (T, T') $ trm) - -fun inj_repabs_err ctxt msg rtrm qtrm = -let - val rtrm_str = Syntax.string_of_term ctxt rtrm - val qtrm_str = Syntax.string_of_term ctxt qtrm -in - raise error (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str]) -end - - -(* bound variables need to be treated properly, - as the type of subterms needs to be calculated *) -fun inj_repabs_trm ctxt (rtrm, qtrm) = - case (rtrm, qtrm) of - (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => - Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm ctxt (t, t')) - - | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => - Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm ctxt (t, t')) - - | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) => - let - val rty = fastype_of rtrm - val qty = fastype_of qtrm - in - mk_repabs ctxt (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))) - end - - | (Abs (x, T, t), Abs (x', T', t')) => - let - val rty = fastype_of rtrm - val qty = fastype_of qtrm - val (y, s) = Term.dest_abs (x, T, t) - val (_, s') = Term.dest_abs (x', T', t') - val yvar = Free (y, T) - val result = Term.lambda_name (y, yvar) (inj_repabs_trm ctxt (s, s')) - in - if rty = qty then result - else mk_repabs ctxt (rty, qty) result - end - - | (t $ s, t' $ s') => - (inj_repabs_trm ctxt (t, t')) $ (inj_repabs_trm ctxt (s, s')) - - | (Free (_, T), Free (_, T')) => - if T = T' then rtrm - else mk_repabs ctxt (T, T') rtrm - - | (_, Const (@{const_name "op ="}, _)) => rtrm - - | (_, Const (_, T')) => - let - val rty = fastype_of rtrm - in - if rty = T' then rtrm - else mk_repabs ctxt (rty, T') rtrm - end - - | _ => inj_repabs_err ctxt "injection (default):" rtrm qtrm - -fun inj_repabs_trm_chk ctxt (rtrm, qtrm) = - inj_repabs_trm ctxt (rtrm, qtrm) - |> Syntax.check_term ctxt - - - -(*** Wrapper for automatically transforming an rthm into a qthm ***) - -(* subst_tys takes a list of (rty, qty) substitution pairs - and replaces all occurences of rty in the given type - by appropriate qty, with substitution *) -fun subst_ty thy ty (rty, qty) r = - if r <> NONE then r else - case try (Sign.typ_match thy (rty, ty)) Vartab.empty of - SOME inst => SOME (Envir.subst_type inst qty) - | NONE => NONE -fun subst_tys thy substs ty = - case fold (subst_ty thy ty) substs NONE of - SOME ty => ty - | NONE => - (case ty of - Type (s, tys) => Type (s, map (subst_tys thy substs) tys) - | x => x) - -(* subst_trms takes a list of (rtrm, qtrm) substitution pairs - and if the given term matches any of the raw terms it - returns the appropriate qtrm instantiated. If none of - them matched it returns NONE. *) -fun subst_trm thy t (rtrm, qtrm) s = - if s <> NONE then s else - case try (Pattern.match thy (rtrm, t)) (Vartab.empty, Vartab.empty) of - SOME inst => SOME (Envir.subst_term inst qtrm) - | NONE => NONE; -fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE - -(* prepares type and term substitution pairs to be used by above - functions that let replace all raw constructs by appropriate - lifted counterparts. *) -fun get_ty_trm_substs ctxt = -let - val thy = ProofContext.theory_of ctxt - val quot_infos = Quotient_Info.quotdata_dest ctxt - val const_infos = Quotient_Info.qconsts_dest ctxt - val ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos - val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos - fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel))) - val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos -in - (ty_substs, const_substs @ rel_substs) -end - -fun quotient_lift_const (b, t) ctxt = -let - val thy = ProofContext.theory_of ctxt - val (ty_substs, _) = get_ty_trm_substs ctxt; - val (_, ty) = dest_Const t; - val nty = subst_tys thy ty_substs ty; -in - Free(b, nty) -end - -(* -Takes a term and - -* replaces raw constants by the quotient constants - -* replaces equivalence relations by equalities - -* replaces raw types by the quotient types - -*) - -fun quotient_lift_all ctxt t = -let - val thy = ProofContext.theory_of ctxt - val (ty_substs, substs) = get_ty_trm_substs ctxt - fun lift_aux t = - case subst_trms thy substs t of - SOME x => x - | NONE => - (case t of - a $ b => lift_aux a $ lift_aux b - | Abs(a, ty, s) => - let - val (y, s') = Term.dest_abs (a, ty, s) - val nty = subst_tys thy ty_substs ty - in - Abs(y, nty, abstract_over (Free (y, nty), lift_aux s')) - end - | Free(n, ty) => Free(n, subst_tys thy ty_substs ty) - | Var(n, ty) => Var(n, subst_tys thy ty_substs ty) - | Bound i => Bound i - | Const(s, ty) => Const(s, subst_tys thy ty_substs ty)) -in - lift_aux t -end - -end; (* structure *)