haftmann@37744: (* Title: HOL/Tools/Quotient/quotient_term.ML kaliszyk@35222: Author: Cezary Kaliszyk and Christian Urban kaliszyk@35222: wenzelm@35788: Constructs terms corresponding to goals from lifting theorems to wenzelm@35788: quotient types. kaliszyk@35222: *) kaliszyk@35222: kaliszyk@35222: signature QUOTIENT_TERM = kaliszyk@35222: sig kaliszyk@35222: exception LIFT_MATCH of string kaliszyk@35222: kaliszyk@35222: datatype flag = AbsF | RepF kaliszyk@35222: kuncar@45797: val absrep_fun: Proof.context -> flag -> typ * typ -> term kuncar@45797: val absrep_fun_chk: Proof.context -> flag -> typ * typ -> term kaliszyk@35222: kaliszyk@35222: (* Allows Nitpick to represent quotient types as single elements from raw type *) kuncar@45797: val absrep_const_chk: Proof.context -> flag -> string -> term kaliszyk@35222: kaliszyk@35222: val equiv_relation: Proof.context -> typ * typ -> term kaliszyk@35222: val equiv_relation_chk: Proof.context -> typ * typ -> term kaliszyk@35222: kuncar@47096: val get_rel_from_quot_thm: thm -> term kuncar@47504: val prove_quot_thm: Proof.context -> typ * typ -> thm kuncar@47096: kaliszyk@35222: val regularize_trm: Proof.context -> term * term -> term kaliszyk@35222: val regularize_trm_chk: Proof.context -> term * term -> term kaliszyk@35222: kaliszyk@35222: val inj_repabs_trm: Proof.context -> term * term -> term kaliszyk@35222: val inj_repabs_trm_chk: Proof.context -> term * term -> term kaliszyk@35222: urbanc@38624: val derive_qtyp: Proof.context -> typ list -> typ -> typ urbanc@38624: val derive_qtrm: Proof.context -> typ list -> term -> term urbanc@38624: val derive_rtyp: Proof.context -> typ list -> typ -> typ urbanc@38624: val derive_rtrm: Proof.context -> typ list -> term -> term kaliszyk@35222: end; kaliszyk@35222: kaliszyk@35222: structure Quotient_Term: QUOTIENT_TERM = kaliszyk@35222: struct kaliszyk@35222: kaliszyk@35222: exception LIFT_MATCH of string kaliszyk@35222: kaliszyk@35222: kaliszyk@35222: kaliszyk@35222: (*** Aggregate Rep/Abs Function ***) kaliszyk@35222: kaliszyk@35222: kaliszyk@35222: (* The flag RepF is for types in negative position; AbsF is for types kaliszyk@35222: in positive position. Because of this, function types need to be kaliszyk@35222: treated specially, since there the polarity changes. kaliszyk@35222: *) kaliszyk@35222: kaliszyk@35222: datatype flag = AbsF | RepF kaliszyk@35222: kaliszyk@35222: fun negF AbsF = RepF kaliszyk@35222: | negF RepF = AbsF kaliszyk@35222: haftmann@37677: fun is_identity (Const (@{const_name id}, _)) = true kaliszyk@35222: | is_identity _ = false kaliszyk@35222: haftmann@37677: fun mk_identity ty = Const (@{const_name id}, ty --> ty) kaliszyk@35222: kaliszyk@35222: fun mk_fun_compose flag (trm1, trm2) = kaliszyk@35222: case flag of haftmann@37677: AbsF => Const (@{const_name comp}, dummyT) $ trm1 $ trm2 haftmann@37677: | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1 kaliszyk@35222: kuncar@45796: fun get_mapfun_data ctxt s = kuncar@45796: (case Symtab.lookup (Enriched_Type.entries ctxt) s of kuncar@45795: SOME [map_data] => (case try dest_Const (#mapper map_data) of kuncar@45795: SOME (c, _) => (Const (c, dummyT), #variances map_data) kuncar@45795: | NONE => raise LIFT_MATCH ("map function for type " ^ quote s ^ " is not a constant.")) kuncar@45795: | SOME _ => raise LIFT_MATCH ("map function for type " ^ quote s ^ " is non-singleton entry.") kuncar@45795: | NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")) kaliszyk@35222: kuncar@45796: fun defined_mapfun_data ctxt s = kuncar@45796: Symtab.defined (Enriched_Type.entries ctxt) s kaliszyk@35222: kaliszyk@35222: (* looks up the (varified) rty and qty for kaliszyk@35222: a quotient definition kaliszyk@35222: *) kuncar@45796: fun get_rty_qty ctxt s = kuncar@45796: let kuncar@45796: val thy = Proof_Context.theory_of ctxt kuncar@45796: in kuncar@45796: (case Quotient_Info.lookup_quotients_global thy s of kuncar@45796: SOME qdata => (#rtyp qdata, #qtyp qdata) kuncar@45796: | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")) kuncar@45796: end kaliszyk@35222: kaliszyk@35222: (* matches a type pattern with a type *) kaliszyk@35222: fun match ctxt err ty_pat ty = wenzelm@41444: let wenzelm@42361: val thy = Proof_Context.theory_of ctxt wenzelm@41444: in wenzelm@41444: Sign.typ_match thy (ty_pat, ty) Vartab.empty wenzelm@41444: handle Type.TYPE_MATCH => err ctxt ty_pat ty wenzelm@41444: end kaliszyk@35222: kaliszyk@35222: (* produces the rep or abs constant for a qty *) kuncar@45797: fun absrep_const ctxt flag qty_str = wenzelm@41444: let bulwahn@45534: (* FIXME *) bulwahn@45534: fun mk_dummyT (Const (c, _)) = Const (c, dummyT) urbanc@45628: | mk_dummyT (Free (c, _)) = Free (c, dummyT) urbanc@45628: | mk_dummyT _ = error "Expecting abs/rep term to be a constant or a free variable" wenzelm@41444: in bulwahn@45534: case Quotient_Info.lookup_abs_rep ctxt qty_str of bulwahn@45534: SOME abs_rep => bulwahn@45534: mk_dummyT (case flag of bulwahn@45534: AbsF => #abs abs_rep bulwahn@45534: | RepF => #rep abs_rep) bulwahn@45534: | NONE => error ("No abs/rep terms for " ^ quote qty_str) wenzelm@41444: end bulwahn@45534: kaliszyk@35222: (* Lets Nitpick represent elements of quotient types as elements of the raw type *) kuncar@45797: fun absrep_const_chk ctxt flag qty_str = kuncar@45797: Syntax.check_term ctxt (absrep_const ctxt flag qty_str) kaliszyk@35222: kaliszyk@35222: fun absrep_match_err ctxt ty_pat ty = wenzelm@41444: let wenzelm@41444: val ty_pat_str = Syntax.string_of_typ ctxt ty_pat wenzelm@41444: val ty_str = Syntax.string_of_typ ctxt ty wenzelm@41444: in wenzelm@41444: raise LIFT_MATCH (space_implode " " wenzelm@41444: ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) wenzelm@41444: end kaliszyk@35222: kaliszyk@35222: kaliszyk@35222: (** generation of an aggregate absrep function **) kaliszyk@35222: kaliszyk@35222: (* - In case of equal types we just return the identity. kaliszyk@35222: kaliszyk@35222: - In case of TFrees we also return the identity. kaliszyk@35222: kaliszyk@35222: - In case of function types we recurse taking kaliszyk@35222: the polarity change into account. kaliszyk@35222: kaliszyk@35222: - If the type constructors are equal, we recurse for the kaliszyk@35222: arguments and build the appropriate map function. kaliszyk@35222: kaliszyk@35222: - If the type constructors are unequal, there must be an kaliszyk@35222: instance of quotient types: kaliszyk@35222: kaliszyk@35222: - we first look up the corresponding rty_pat and qty_pat kaliszyk@35222: from the quotient definition; the arguments of qty_pat kaliszyk@35222: must be some distinct TVars kaliszyk@35222: - we then match the rty_pat with rty and qty_pat with qty; kaliszyk@35222: if matching fails the types do not correspond -> error kaliszyk@35222: - the matching produces two environments; we look up the kaliszyk@35222: assignments for the qty_pat variables and recurse on the kaliszyk@35222: assignments kaliszyk@35222: - we prefix the aggregate map function for the rty_pat, kaliszyk@35222: which is an abstraction over all type variables kaliszyk@35222: - finally we compose the result with the appropriate kaliszyk@35222: absrep function in case at least one argument produced kaliszyk@35222: a non-identity function / kaliszyk@35222: otherwise we just return the appropriate absrep kaliszyk@35222: function kaliszyk@35222: kaliszyk@35222: The composition is necessary for types like kaliszyk@35222: kaliszyk@35222: ('a list) list / ('a foo) foo kaliszyk@35222: kaliszyk@35222: The matching is necessary for types like kaliszyk@35222: kaliszyk@35222: ('a * 'a) list / 'a bar kaliszyk@35222: kaliszyk@35222: The test is necessary in order to eliminate superfluous kaliszyk@35222: identity maps. kaliszyk@35222: *) kaliszyk@35222: kuncar@45797: fun absrep_fun ctxt flag (rty, qty) = wenzelm@45340: let kuncar@45795: fun absrep_args tys tys' variances = kuncar@45795: let kuncar@45795: fun absrep_arg (types, (_, variant)) = kuncar@45795: (case variant of kuncar@45795: (false, false) => [] kuncar@45797: | (true, false) => [(absrep_fun ctxt flag types)] kuncar@45797: | (false, true) => [(absrep_fun ctxt (negF flag) types)] kuncar@45797: | (true, true) => [(absrep_fun ctxt flag types),(absrep_fun ctxt (negF flag) types)]) kuncar@45795: in kuncar@45795: maps absrep_arg ((tys ~~ tys') ~~ variances) kuncar@45795: end kuncar@45795: fun test_identities tys rtys' s s' = kuncar@45795: let kuncar@45797: val args = map (absrep_fun ctxt flag) (tys ~~ rtys') kuncar@45795: in kuncar@45795: if forall is_identity args kuncar@45795: then kuncar@45797: absrep_const ctxt flag s' kuncar@45795: else kuncar@45795: raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.") kuncar@45795: end wenzelm@45340: in wenzelm@45340: if rty = qty wenzelm@45340: then mk_identity rty wenzelm@45340: else wenzelm@45340: case (rty, qty) of kuncar@45795: (Type (s, tys), Type (s', tys')) => wenzelm@45340: if s = s' wenzelm@45340: then wenzelm@45340: let kuncar@45796: val (map_fun, variances) = get_mapfun_data ctxt s kuncar@45795: val args = absrep_args tys tys' variances wenzelm@45340: in kuncar@45795: list_comb (map_fun, args) wenzelm@45340: end wenzelm@45340: else wenzelm@45340: let kuncar@45796: val (Type (_, rtys), qty_pat) = get_rty_qty ctxt s' wenzelm@45340: val qtyenv = match ctxt absrep_match_err qty_pat qty kuncar@45795: val rtys' = map (Envir.subst_type qtyenv) rtys wenzelm@45340: in kuncar@45796: if not (defined_mapfun_data ctxt s) kuncar@45795: then kuncar@45795: (* kuncar@45795: If we don't know a map function for the raw type, kuncar@45795: we are not necessarilly in troubles because kuncar@45795: it can still be the case we don't need the map kuncar@45795: function <=> all abs/rep functions are identities. kuncar@45795: *) kuncar@45795: test_identities tys rtys' s s' wenzelm@45340: else wenzelm@45340: let kuncar@45796: val (map_fun, variances) = get_mapfun_data ctxt s kuncar@45795: val args = absrep_args tys rtys' variances wenzelm@45340: in kuncar@45795: if forall is_identity args kuncar@45797: then absrep_const ctxt flag s' kuncar@45795: else kuncar@45795: let kuncar@45795: val result = list_comb (map_fun, args) kuncar@45795: in kuncar@45797: mk_fun_compose flag (absrep_const ctxt flag s', result) kuncar@45795: end wenzelm@45340: end wenzelm@45340: end wenzelm@45340: | (TFree x, TFree x') => wenzelm@45340: if x = x' wenzelm@45340: then mk_identity rty wenzelm@45340: else raise (LIFT_MATCH "absrep_fun (frees)") wenzelm@45340: | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)") wenzelm@45340: | _ => raise (LIFT_MATCH "absrep_fun (default)") wenzelm@45340: end kaliszyk@35222: kuncar@45797: fun absrep_fun_chk ctxt flag (rty, qty) = kuncar@45797: absrep_fun ctxt flag (rty, qty) kaliszyk@35222: |> Syntax.check_term ctxt kaliszyk@35222: kaliszyk@35222: kaliszyk@35222: kaliszyk@35222: (*** Aggregate Equivalence Relation ***) kaliszyk@35222: kaliszyk@35222: kaliszyk@35222: (* works very similar to the absrep generation, kaliszyk@35222: except there is no need for polarities kaliszyk@35222: *) kaliszyk@35222: kaliszyk@35222: (* instantiates TVars so that the term is of type ty *) kaliszyk@35222: fun force_typ ctxt trm ty = wenzelm@41444: let wenzelm@42361: val thy = Proof_Context.theory_of ctxt wenzelm@41444: val trm_ty = fastype_of trm wenzelm@41444: val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty wenzelm@41444: in wenzelm@41444: map_types (Envir.subst_type ty_inst) trm wenzelm@41444: end kaliszyk@35222: haftmann@38864: fun is_eq (Const (@{const_name HOL.eq}, _)) = true kaliszyk@35222: | is_eq _ = false kaliszyk@35222: kaliszyk@35222: fun mk_rel_compose (trm1, trm2) = wenzelm@35402: Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2 kaliszyk@35222: wenzelm@45340: fun get_relmap thy s = wenzelm@45340: (case Quotient_Info.lookup_quotmaps thy s of bulwahn@45273: SOME map_data => Const (#relmap map_data, dummyT) wenzelm@45279: | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")) kaliszyk@35222: wenzelm@45340: fun get_equiv_rel thy s = wenzelm@45340: (case Quotient_Info.lookup_quotients thy s of wenzelm@45279: SOME qdata => #equiv_rel qdata kuncar@47095: | NONE => raise LIFT_MATCH ("get_equiv_rel (no quotient found for type " ^ s ^ ")")) kaliszyk@35222: kaliszyk@35222: fun equiv_match_err ctxt ty_pat ty = wenzelm@41444: let wenzelm@41444: val ty_pat_str = Syntax.string_of_typ ctxt ty_pat wenzelm@41444: val ty_str = Syntax.string_of_typ ctxt ty wenzelm@41444: in wenzelm@41444: raise LIFT_MATCH (space_implode " " wenzelm@41444: ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) wenzelm@41444: end kaliszyk@35222: kaliszyk@35222: (* builds the aggregate equivalence relation kaliszyk@35222: that will be the argument of Respects kaliszyk@35222: *) kaliszyk@35222: fun equiv_relation ctxt (rty, qty) = kuncar@45796: if rty = qty kuncar@45796: then HOLogic.eq_const rty kuncar@45796: else kuncar@45796: case (rty, qty) of kuncar@45796: (Type (s, tys), Type (s', tys')) => kuncar@45796: if s = s' kuncar@45796: then kuncar@45796: let kuncar@45796: val args = map (equiv_relation ctxt) (tys ~~ tys') kuncar@45796: in kuncar@45796: list_comb (get_relmap ctxt s, args) kuncar@45796: end kuncar@45796: else kuncar@45796: let kuncar@47095: val (Type (_, rtys), qty_pat) = get_rty_qty ctxt s' kuncar@45796: val qtyenv = match ctxt equiv_match_err qty_pat qty kuncar@47095: val rtys' = map (Envir.subst_type qtyenv) rtys kuncar@47095: val args = map (equiv_relation ctxt) (tys ~~ rtys') kuncar@45796: val eqv_rel = get_equiv_rel ctxt s' kuncar@45796: val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) kuncar@45796: in kuncar@45796: if forall is_eq args kuncar@45796: then eqv_rel' kuncar@45796: else kuncar@45796: let kuncar@47095: val result = list_comb (get_relmap ctxt s, args) kuncar@45796: in kuncar@45796: mk_rel_compose (result, eqv_rel') kuncar@45796: end kuncar@45796: end kuncar@45796: | _ => HOLogic.eq_const rty kuncar@45796: kaliszyk@35222: kaliszyk@35222: fun equiv_relation_chk ctxt (rty, qty) = kaliszyk@35222: equiv_relation ctxt (rty, qty) kaliszyk@35222: |> Syntax.check_term ctxt kaliszyk@35222: kuncar@47096: (* generation of the Quotient theorem *) kuncar@47096: kuncar@47106: exception CODE_GEN of string kuncar@47106: kuncar@47096: fun get_quot_thm ctxt s = kuncar@47096: let kuncar@47096: val thy = Proof_Context.theory_of ctxt kuncar@47096: in kuncar@47106: (case Quotient_Info.lookup_quotients ctxt s of kuncar@47106: SOME qdata => Thm.transfer thy (#quot_thm qdata) kuncar@47106: | NONE => raise CODE_GEN ("No quotient type " ^ quote s ^ " found.")) kuncar@47096: end kuncar@47096: kuncar@47106: fun get_rel_quot_thm ctxt s = kuncar@47106: let kuncar@47106: val thy = Proof_Context.theory_of ctxt kuncar@47106: in kuncar@47106: (case Quotient_Info.lookup_quotmaps ctxt s of kuncar@47106: SOME map_data => Thm.transfer thy (#quot_thm map_data) kuncar@47106: | NONE => raise CODE_GEN ("get_relmap (no relation map function found for type " ^ s ^ ")")) kuncar@47106: end kuncar@47096: kuncar@47308: fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient3}) kuncar@47096: kuncar@47096: infix 0 MRSL kuncar@47096: kuncar@47096: fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm kuncar@47096: kuncar@47096: exception NOT_IMPL of string kuncar@47096: kuncar@47096: fun get_rel_from_quot_thm quot_thm = kuncar@47096: let kuncar@47096: val (_ $ rel $ _ $ _) = (HOLogic.dest_Trueprop o prop_of) quot_thm kuncar@47096: in kuncar@47096: rel kuncar@47096: end kuncar@47096: kuncar@47096: fun mk_quot_thm_compose (rel_quot_thm, quot_thm) = kuncar@47096: let kuncar@47096: val quot_thm_rel = get_rel_from_quot_thm quot_thm kuncar@47096: in kuncar@47308: if is_eq quot_thm_rel then [rel_quot_thm, quot_thm] MRSL @{thm OOO_eq_quotient3} kuncar@47096: else raise NOT_IMPL "nested quotients: not implemented yet" kuncar@47096: end kuncar@47096: kuncar@47504: fun prove_quot_thm ctxt (rty, qty) = kuncar@47096: if rty = qty kuncar@47308: then @{thm identity_quotient3} kuncar@47096: else kuncar@47096: case (rty, qty) of kuncar@47096: (Type (s, tys), Type (s', tys')) => kuncar@47096: if s = s' kuncar@47096: then kuncar@47096: let kuncar@47504: val args = map (prove_quot_thm ctxt) (tys ~~ tys') kuncar@47096: in kuncar@47096: args MRSL (get_rel_quot_thm ctxt s) kuncar@47096: end kuncar@47096: else kuncar@47096: let kuncar@47096: val (Type (_, rtys), qty_pat) = get_rty_qty ctxt s' kuncar@47096: val qtyenv = match ctxt equiv_match_err qty_pat qty kuncar@47096: val rtys' = map (Envir.subst_type qtyenv) rtys kuncar@47504: val args = map (prove_quot_thm ctxt) (tys ~~ rtys') kuncar@47096: val quot_thm = get_quot_thm ctxt s' kuncar@47096: in kuncar@47096: if forall is_id_quot args kuncar@47096: then kuncar@47096: quot_thm kuncar@47096: else kuncar@47096: let kuncar@47096: val rel_quot_thm = args MRSL (get_rel_quot_thm ctxt s) kuncar@47096: in kuncar@47096: mk_quot_thm_compose (rel_quot_thm, quot_thm) kuncar@47096: end kuncar@47096: end kuncar@47308: | _ => @{thm identity_quotient3} kuncar@47096: kaliszyk@35222: kaliszyk@35222: kaliszyk@35222: (*** Regularization ***) kaliszyk@35222: kaliszyk@35222: (* Regularizing an rtrm means: kaliszyk@35222: kaliszyk@35222: - Quantifiers over types that need lifting are replaced kaliszyk@35222: by bounded quantifiers, for example: kaliszyk@35222: kaliszyk@35222: All P ----> All (Respects R) P kaliszyk@35222: kaliszyk@35222: where the aggregate relation R is given by the rty and qty; kaliszyk@35222: kaliszyk@35222: - Abstractions over types that need lifting are replaced kaliszyk@35222: by bounded abstractions, for example: kaliszyk@35222: kaliszyk@35222: %x. P ----> Ball (Respects R) %x. P kaliszyk@35222: kaliszyk@35222: - Equalities over types that need lifting are replaced by kaliszyk@35222: corresponding equivalence relations, for example: kaliszyk@35222: kaliszyk@35222: A = B ----> R A B kaliszyk@35222: kaliszyk@35222: or kaliszyk@35222: kaliszyk@35222: A = B ----> (R ===> R) A B kaliszyk@35222: kaliszyk@35222: for more complicated types of A and B kaliszyk@35222: kaliszyk@35222: kaliszyk@35222: The regularize_trm accepts raw theorems in which equalities kaliszyk@35222: and quantifiers match exactly the ones in the lifted theorem kaliszyk@35222: but also accepts partially regularized terms. kaliszyk@35222: kaliszyk@35222: This means that the raw theorems can have: kaliszyk@35222: Ball (Respects R), Bex (Respects R), Bex1_rel (Respects R), Babs, R kaliszyk@35222: in the places where: kaliszyk@35222: All, Ex, Ex1, %, (op =) kaliszyk@35222: is required the lifted theorem. kaliszyk@35222: kaliszyk@35222: *) kaliszyk@35222: kaliszyk@35222: val mk_babs = Const (@{const_name Babs}, dummyT) kaliszyk@35222: val mk_ball = Const (@{const_name Ball}, dummyT) kaliszyk@35222: val mk_bex = Const (@{const_name Bex}, dummyT) kaliszyk@35222: val mk_bex1_rel = Const (@{const_name Bex1_rel}, dummyT) kaliszyk@35222: val mk_resp = Const (@{const_name Respects}, dummyT) kaliszyk@35222: kaliszyk@35222: (* - applies f to the subterm of an abstraction, kaliszyk@35222: otherwise to the given term, kaliszyk@35222: - used by regularize, therefore abstracted kaliszyk@35222: variables do not have to be treated specially kaliszyk@35222: *) kaliszyk@35222: fun apply_subt f (trm1, trm2) = kaliszyk@35222: case (trm1, trm2) of kaliszyk@35222: (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t')) kaliszyk@35222: | _ => f (trm1, trm2) kaliszyk@35222: kaliszyk@35222: fun term_mismatch str ctxt t1 t2 = wenzelm@41444: let wenzelm@41444: val t1_str = Syntax.string_of_term ctxt t1 wenzelm@41444: val t2_str = Syntax.string_of_term ctxt t2 wenzelm@41444: val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1) wenzelm@41444: val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2) wenzelm@41444: in wenzelm@41444: raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str]) wenzelm@41444: end kaliszyk@35222: kaliszyk@35222: (* the major type of All and Ex quantifiers *) kaliszyk@35222: fun qnt_typ ty = domain_type (domain_type ty) kaliszyk@35222: kaliszyk@35222: (* Checks that two types match, for example: kaliszyk@35222: rty -> rty matches qty -> qty *) wenzelm@45280: fun matches_typ ctxt rT qT = wenzelm@45340: let wenzelm@45340: val thy = Proof_Context.theory_of ctxt wenzelm@45340: in wenzelm@45340: if rT = qT then true wenzelm@45340: else wenzelm@45340: (case (rT, qT) of wenzelm@45340: (Type (rs, rtys), Type (qs, qtys)) => wenzelm@45340: if rs = qs then wenzelm@45340: if length rtys <> length qtys then false wenzelm@45340: else forall (fn x => x = true) (map2 (matches_typ ctxt) rtys qtys) wenzelm@45340: else wenzelm@45340: (case Quotient_Info.lookup_quotients_global thy qs of wenzelm@45340: SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo) wenzelm@45340: | NONE => false) wenzelm@45340: | _ => false) wenzelm@45340: end kaliszyk@35222: kaliszyk@35222: kaliszyk@35222: (* produces a regularized version of rtrm kaliszyk@35222: kaliszyk@35222: - the result might contain dummyTs kaliszyk@35222: urbanc@38718: - for regularization we do not need any kaliszyk@35222: special treatment of bound variables kaliszyk@35222: *) kaliszyk@35222: fun regularize_trm ctxt (rtrm, qtrm) = wenzelm@45280: (case (rtrm, qtrm) of kaliszyk@35222: (Abs (x, ty, t), Abs (_, ty', t')) => wenzelm@41444: let wenzelm@41444: val subtrm = Abs(x, ty, regularize_trm ctxt (t, t')) wenzelm@41444: in wenzelm@41444: if ty = ty' then subtrm wenzelm@41444: else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm wenzelm@41444: end wenzelm@45280: haftmann@37677: | (Const (@{const_name Babs}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) => wenzelm@41444: let wenzelm@41444: val subtrm = regularize_trm ctxt (t, t') wenzelm@41444: val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty') wenzelm@41444: in wenzelm@41444: if resrel <> needres wenzelm@41444: then term_mismatch "regularize (Babs)" ctxt resrel needres wenzelm@41444: else mk_babs $ resrel $ subtrm wenzelm@41444: end kaliszyk@35222: haftmann@37677: | (Const (@{const_name All}, ty) $ t, Const (@{const_name All}, ty') $ t') => wenzelm@41444: let wenzelm@41444: val subtrm = apply_subt (regularize_trm ctxt) (t, t') wenzelm@41444: in wenzelm@41444: if ty = ty' then Const (@{const_name All}, ty) $ subtrm wenzelm@41444: else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm wenzelm@41444: end kaliszyk@35222: haftmann@37677: | (Const (@{const_name Ex}, ty) $ t, Const (@{const_name Ex}, ty') $ t') => wenzelm@41444: let wenzelm@41444: val subtrm = apply_subt (regularize_trm ctxt) (t, t') wenzelm@41444: in wenzelm@41444: if ty = ty' then Const (@{const_name Ex}, ty) $ subtrm wenzelm@41444: else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm wenzelm@41444: end kaliszyk@35222: haftmann@37677: | (Const (@{const_name Ex1}, ty) $ (Abs (_, _, haftmann@38795: (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name Set.member}, _) $ _ $ haftmann@37677: (Const (@{const_name Respects}, _) $ resrel)) $ (t $ _)))), haftmann@37677: Const (@{const_name Ex1}, ty') $ t') => wenzelm@41444: let wenzelm@41444: val t_ = incr_boundvars (~1) t wenzelm@41444: val subtrm = apply_subt (regularize_trm ctxt) (t_, t') wenzelm@41444: val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') wenzelm@41444: in wenzelm@41444: if resrel <> needrel wenzelm@41444: then term_mismatch "regularize (Bex1)" ctxt resrel needrel wenzelm@41444: else mk_bex1_rel $ resrel $ subtrm wenzelm@41444: end kaliszyk@35222: haftmann@38558: | (Const (@{const_name Ex1}, ty) $ t, Const (@{const_name Ex1}, ty') $ t') => wenzelm@41444: let wenzelm@41444: val subtrm = apply_subt (regularize_trm ctxt) (t, t') wenzelm@41444: in wenzelm@41444: if ty = ty' then Const (@{const_name Ex1}, ty) $ subtrm wenzelm@41444: else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm wenzelm@41444: end kaliszyk@35222: urbanc@38624: | (Const (@{const_name Ball}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t, haftmann@38558: Const (@{const_name All}, ty') $ t') => wenzelm@41444: let wenzelm@41444: val subtrm = apply_subt (regularize_trm ctxt) (t, t') wenzelm@41444: val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') wenzelm@41444: in wenzelm@41444: if resrel <> needrel wenzelm@41444: then term_mismatch "regularize (Ball)" ctxt resrel needrel wenzelm@41444: else mk_ball $ (mk_resp $ resrel) $ subtrm wenzelm@41444: end kaliszyk@35222: urbanc@38624: | (Const (@{const_name Bex}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t, haftmann@38558: Const (@{const_name Ex}, ty') $ t') => wenzelm@41444: let wenzelm@41444: val subtrm = apply_subt (regularize_trm ctxt) (t, t') wenzelm@41444: val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') wenzelm@41444: in wenzelm@41444: if resrel <> needrel wenzelm@41444: then term_mismatch "regularize (Bex)" ctxt resrel needrel wenzelm@41444: else mk_bex $ (mk_resp $ resrel) $ subtrm wenzelm@41444: end kaliszyk@35222: urbanc@38624: | (Const (@{const_name Bex1_rel}, ty) $ resrel $ t, Const (@{const_name Ex1}, ty') $ t') => wenzelm@41444: let wenzelm@41444: val subtrm = apply_subt (regularize_trm ctxt) (t, t') wenzelm@41444: val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') wenzelm@41444: in wenzelm@41444: if resrel <> needrel wenzelm@41444: then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel wenzelm@41444: else mk_bex1_rel $ resrel $ subtrm wenzelm@41444: end kaliszyk@35222: kaliszyk@35222: | (* equalities need to be replaced by appropriate equivalence relations *) haftmann@38864: (Const (@{const_name HOL.eq}, ty), Const (@{const_name HOL.eq}, ty')) => wenzelm@41444: if ty = ty' then rtrm wenzelm@41444: else equiv_relation ctxt (domain_type ty, domain_type ty') kaliszyk@35222: kaliszyk@35222: | (* in this case we just check whether the given equivalence relation is correct *) haftmann@38864: (rel, Const (@{const_name HOL.eq}, ty')) => wenzelm@41444: let wenzelm@41444: val rel_ty = fastype_of rel wenzelm@41444: val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') wenzelm@41444: in wenzelm@41444: if rel' aconv rel then rtrm wenzelm@41444: else term_mismatch "regularize (relation mismatch)" ctxt rel rel' wenzelm@41444: end kaliszyk@35222: kaliszyk@35222: | (_, Const _) => wenzelm@41444: let wenzelm@42361: val thy = Proof_Context.theory_of ctxt wenzelm@45280: fun same_const (Const (s, T)) (Const (s', T')) = s = s' andalso matches_typ ctxt T T' wenzelm@41444: | same_const _ _ = false wenzelm@41444: in wenzelm@41444: if same_const rtrm qtrm then rtrm wenzelm@41444: else wenzelm@41444: let wenzelm@45279: val rtrm' = wenzelm@45340: (case Quotient_Info.lookup_quotconsts_global thy qtrm of wenzelm@45279: SOME qconst_info => #rconst qconst_info wenzelm@45279: | NONE => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm) wenzelm@41444: in wenzelm@41444: if Pattern.matches thy (rtrm', rtrm) wenzelm@41444: then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm wenzelm@41444: end wenzelm@41444: end kaliszyk@35222: haftmann@37591: | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))), haftmann@37591: ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) => kaliszyk@35222: regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2))) kaliszyk@35222: haftmann@37591: | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, s1)), haftmann@37591: ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , s2))) => kaliszyk@35222: regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2)) kaliszyk@35222: kaliszyk@35222: | (t1 $ t2, t1' $ t2') => kaliszyk@35222: regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2') kaliszyk@35222: kaliszyk@35222: | (Bound i, Bound i') => wenzelm@41444: if i = i' then rtrm wenzelm@41444: else raise (LIFT_MATCH "regularize (bounds mismatch)") kaliszyk@35222: kaliszyk@35222: | _ => wenzelm@41444: let wenzelm@41444: val rtrm_str = Syntax.string_of_term ctxt rtrm wenzelm@41444: val qtrm_str = Syntax.string_of_term ctxt qtrm wenzelm@41444: in wenzelm@41444: raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")")) wenzelm@45280: end) kaliszyk@35222: kaliszyk@35222: fun regularize_trm_chk ctxt (rtrm, qtrm) = kaliszyk@35222: regularize_trm ctxt (rtrm, qtrm) kaliszyk@35222: |> Syntax.check_term ctxt kaliszyk@35222: kaliszyk@35222: kaliszyk@35222: kaliszyk@35222: (*** Rep/Abs Injection ***) kaliszyk@35222: kaliszyk@35222: (* kaliszyk@35222: Injection of Rep/Abs means: kaliszyk@35222: kaliszyk@35222: For abstractions: kaliszyk@35222: kaliszyk@35222: * If the type of the abstraction needs lifting, then we add Rep/Abs kaliszyk@35222: around the abstraction; otherwise we leave it unchanged. kaliszyk@35222: kaliszyk@35222: For applications: kaliszyk@35222: kaliszyk@35222: * If the application involves a bounded quantifier, we recurse on kaliszyk@35222: the second argument. If the application is a bounded abstraction, kaliszyk@35222: we always put an Rep/Abs around it (since bounded abstractions kaliszyk@35222: are assumed to always need lifting). Otherwise we recurse on both kaliszyk@35222: arguments. kaliszyk@35222: kaliszyk@35222: For constants: kaliszyk@35222: kaliszyk@35222: * If the constant is (op =), we leave it always unchanged. kaliszyk@35222: Otherwise the type of the constant needs lifting, we put kaliszyk@35222: and Rep/Abs around it. kaliszyk@35222: kaliszyk@35222: For free variables: kaliszyk@35222: kaliszyk@35222: * We put a Rep/Abs around it if the type needs lifting. kaliszyk@35222: kaliszyk@35222: Vars case cannot occur. kaliszyk@35222: *) kaliszyk@35222: kaliszyk@35222: fun mk_repabs ctxt (T, T') trm = kuncar@45797: absrep_fun ctxt RepF (T, T') $ (absrep_fun ctxt AbsF (T, T') $ trm) kaliszyk@35222: kaliszyk@35222: fun inj_repabs_err ctxt msg rtrm qtrm = wenzelm@41444: let wenzelm@41444: val rtrm_str = Syntax.string_of_term ctxt rtrm wenzelm@41444: val qtrm_str = Syntax.string_of_term ctxt qtrm wenzelm@41444: in wenzelm@41444: raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str]) wenzelm@41444: end kaliszyk@35222: kaliszyk@35222: kaliszyk@35222: (* bound variables need to be treated properly, kaliszyk@35222: as the type of subterms needs to be calculated *) kaliszyk@35222: fun inj_repabs_trm ctxt (rtrm, qtrm) = kaliszyk@35222: case (rtrm, qtrm) of urbanc@38624: (Const (@{const_name Ball}, T) $ r $ t, Const (@{const_name All}, _) $ t') => urbanc@38624: Const (@{const_name Ball}, T) $ r $ (inj_repabs_trm ctxt (t, t')) kaliszyk@35222: urbanc@38624: | (Const (@{const_name Bex}, T) $ r $ t, Const (@{const_name Ex}, _) $ t') => urbanc@38624: Const (@{const_name Bex}, T) $ r $ (inj_repabs_trm ctxt (t, t')) kaliszyk@35222: urbanc@38624: | (Const (@{const_name Babs}, T) $ r $ t, t' as (Abs _)) => kaliszyk@35222: let kaliszyk@35222: val rty = fastype_of rtrm kaliszyk@35222: val qty = fastype_of qtrm kaliszyk@35222: in urbanc@38624: mk_repabs ctxt (rty, qty) (Const (@{const_name Babs}, T) $ r $ (inj_repabs_trm ctxt (t, t'))) kaliszyk@35222: end kaliszyk@35222: kaliszyk@35222: | (Abs (x, T, t), Abs (x', T', t')) => kaliszyk@35222: let kaliszyk@35222: val rty = fastype_of rtrm kaliszyk@35222: val qty = fastype_of qtrm kaliszyk@35222: val (y, s) = Term.dest_abs (x, T, t) kaliszyk@35222: val (_, s') = Term.dest_abs (x', T', t') kaliszyk@35222: val yvar = Free (y, T) kaliszyk@35222: val result = Term.lambda_name (y, yvar) (inj_repabs_trm ctxt (s, s')) kaliszyk@35222: in kaliszyk@35222: if rty = qty then result kaliszyk@35222: else mk_repabs ctxt (rty, qty) result kaliszyk@35222: end kaliszyk@35222: kaliszyk@35222: | (t $ s, t' $ s') => kaliszyk@35222: (inj_repabs_trm ctxt (t, t')) $ (inj_repabs_trm ctxt (s, s')) kaliszyk@35222: kaliszyk@35222: | (Free (_, T), Free (_, T')) => kaliszyk@35222: if T = T' then rtrm kaliszyk@35222: else mk_repabs ctxt (T, T') rtrm kaliszyk@35222: haftmann@38864: | (_, Const (@{const_name HOL.eq}, _)) => rtrm kaliszyk@35222: kaliszyk@35222: | (_, Const (_, T')) => kaliszyk@35222: let kaliszyk@35222: val rty = fastype_of rtrm kaliszyk@35222: in kaliszyk@35222: if rty = T' then rtrm kaliszyk@35222: else mk_repabs ctxt (rty, T') rtrm kaliszyk@35222: end kaliszyk@35222: kaliszyk@35222: | _ => inj_repabs_err ctxt "injection (default):" rtrm qtrm kaliszyk@35222: kaliszyk@35222: fun inj_repabs_trm_chk ctxt (rtrm, qtrm) = kaliszyk@35222: inj_repabs_trm ctxt (rtrm, qtrm) kaliszyk@35222: |> Syntax.check_term ctxt kaliszyk@35222: kaliszyk@35222: kaliszyk@35222: kaliszyk@35222: (*** Wrapper for automatically transforming an rthm into a qthm ***) kaliszyk@35222: urbanc@37592: (* substitutions functions for r/q-types and urbanc@37592: r/q-constants, respectively urbanc@37560: *) urbanc@37592: fun subst_typ ctxt ty_subst rty = urbanc@37560: case rty of urbanc@37560: Type (s, rtys) => urbanc@37560: let wenzelm@42361: val thy = Proof_Context.theory_of ctxt urbanc@37592: val rty' = Type (s, map (subst_typ ctxt ty_subst) rtys) urbanc@37560: urbanc@37560: fun matches [] = rty' urbanc@37560: | matches ((rty, qty)::tail) = wenzelm@45280: (case try (Sign.typ_match thy (rty, rty')) Vartab.empty of urbanc@37560: NONE => matches tail cezarykaliszyk@46416: | SOME inst => subst_typ ctxt ty_subst (Envir.subst_type inst qty)) urbanc@37560: in wenzelm@41444: matches ty_subst wenzelm@41444: end urbanc@37560: | _ => rty urbanc@37560: urbanc@37592: fun subst_trm ctxt ty_subst trm_subst rtrm = urbanc@37560: case rtrm of urbanc@37592: t1 $ t2 => (subst_trm ctxt ty_subst trm_subst t1) $ (subst_trm ctxt ty_subst trm_subst t2) urbanc@37592: | Abs (x, ty, t) => Abs (x, subst_typ ctxt ty_subst ty, subst_trm ctxt ty_subst trm_subst t) urbanc@37592: | Free(n, ty) => Free(n, subst_typ ctxt ty_subst ty) urbanc@37592: | Var(n, ty) => Var(n, subst_typ ctxt ty_subst ty) urbanc@37560: | Bound i => Bound i wenzelm@41444: | Const (a, ty) => urbanc@37560: let wenzelm@42361: val thy = Proof_Context.theory_of ctxt kaliszyk@35222: urbanc@37592: fun matches [] = Const (a, subst_typ ctxt ty_subst ty) urbanc@37560: | matches ((rconst, qconst)::tail) = wenzelm@45280: (case try (Pattern.match thy (rconst, rtrm)) (Vartab.empty, Vartab.empty) of urbanc@37560: NONE => matches tail cezarykaliszyk@46416: | SOME inst => subst_trm ctxt ty_subst trm_subst (Envir.subst_term inst qconst)) urbanc@37560: in urbanc@37560: matches trm_subst urbanc@37560: end urbanc@37560: urbanc@37592: (* generate type and term substitutions out of the wenzelm@41444: qtypes involved in a quotient; the direction flag wenzelm@41444: indicates in which direction the substitutions work: wenzelm@41444: urbanc@37592: true: quotient -> raw urbanc@37592: false: raw -> quotient urbanc@37560: *) urbanc@37592: fun mk_ty_subst qtys direction ctxt = wenzelm@41444: let wenzelm@42361: val thy = Proof_Context.theory_of ctxt wenzelm@41444: in wenzelm@45279: Quotient_Info.dest_quotients ctxt wenzelm@41444: |> map (fn x => (#rtyp x, #qtyp x)) wenzelm@41444: |> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty) wenzelm@41444: |> map (if direction then swap else I) wenzelm@41444: end kaliszyk@35222: urbanc@37592: fun mk_trm_subst qtys direction ctxt = wenzelm@41444: let wenzelm@41444: val subst_typ' = subst_typ ctxt (mk_ty_subst qtys direction ctxt) wenzelm@41444: fun proper (t1, t2) = subst_typ' (fastype_of t1) = fastype_of t2 kaliszyk@37563: wenzelm@41444: val const_substs = wenzelm@45279: Quotient_Info.dest_quotconsts ctxt wenzelm@41444: |> map (fn x => (#rconst x, #qconst x)) wenzelm@41444: |> map (if direction then swap else I) urbanc@37560: wenzelm@41444: val rel_substs = wenzelm@45279: Quotient_Info.dest_quotients ctxt wenzelm@41444: |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x))) wenzelm@41444: |> map (if direction then swap else I) wenzelm@41444: in wenzelm@41444: filter proper (const_substs @ rel_substs) wenzelm@41444: end kaliszyk@35222: urbanc@37592: urbanc@37560: (* derives a qtyp and qtrm out of a rtyp and rtrm, wenzelm@41444: respectively urbanc@37560: *) urbanc@38624: fun derive_qtyp ctxt qtys rty = urbanc@37592: subst_typ ctxt (mk_ty_subst qtys false ctxt) rty urbanc@37592: urbanc@38624: fun derive_qtrm ctxt qtys rtrm = urbanc@37592: subst_trm ctxt (mk_ty_subst qtys false ctxt) (mk_trm_subst qtys false ctxt) rtrm kaliszyk@35222: urbanc@37592: (* derives a rtyp and rtrm out of a qtyp and qtrm, wenzelm@41444: respectively urbanc@37592: *) urbanc@38624: fun derive_rtyp ctxt qtys qty = urbanc@37592: subst_typ ctxt (mk_ty_subst qtys true ctxt) qty urbanc@37592: urbanc@38624: fun derive_rtrm ctxt qtys qtrm = urbanc@37592: subst_trm ctxt (mk_ty_subst qtys true ctxt) (mk_trm_subst qtys true ctxt) qtrm urbanc@37560: kaliszyk@35222: wenzelm@45279: end;