nominal2: comparison Quot/quotient

equal deleted inserted replaced

-:f0a78fda343f
+:a28f805df355
 datatype flag = absF | repF
 val absrep_fun: flag -> Proof.context -> (typ * typ) -> term
 val absrep_fun_chk: flag -> Proof.context -> (typ * typ) -> 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
 end
 (* 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          *)
+(* correspond to the type variables in rty)         *)
 fun mk_mapfun ctxt vs ty =
 let
 val vs' = map (mk_Free) vs
 fun mk_mapfun_aux ty =
 val qdata = (quotdata_lookup thy s) handle NotFound => raise exc
 in
 (#rtyp qdata, #qtyp qdata)
 end
-(* receives two type-environments and looks *)
+(* takes two type-environments and looks    *)
-(* up in both of them the variable v        *)
+(* 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')))
 case flag of
 absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT)
 | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
 end
-(* produces the aggregate absrep function                          *)
+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 LIFT_MATCH (space_implode " "
+["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
+end
+(* produces an aggregate absrep function                           *)
 (*                                                                 *)
 (* - In case of function types and TFrees, we recurse, taking in   *)
 (*   the first case the polarity change into account.              *)
 (*                                                                 *)
 (* - If the type constructors are equal, we recurse for the        *)
 list_comb (get_mapfun ctxt s, args)
 end
 else
 let
 val thy = ProofContext.theory_of ctxt
-val exc = (LIFT_MATCH "absrep_fun (Types do not match.)")
 val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
-val (rtyenv, qtyenv) =
+val rtyenv = Sign.typ_match thy (rty_pat, rty) Vartab.empty
-(Sign.typ_match thy (rty_pat, rty) Vartab.empty,
+handle MATCH_TYPE => absrep_match_err ctxt rty_pat rty
-Sign.typ_match thy (qty_pat, qty) Vartab.empty)
+val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty
-handle MATCH_TYPE => raise exc
+handle MATCH_TYPE => absrep_match_err ctxt 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
 fun absrep_fun_chk flag ctxt (rty, qty) =
 absrep_fun flag ctxt (rty, qty)
 |> Syntax.check_term ctxt
-(* Regularizing an rtrm means:
+(**********************************)
+(* Aggregate Equivalence Relation *)
-- 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
-*)
 (* instantiates TVars so that the term is of type ty *)
 fun force_typ ctxt trm ty =
 let
 val thy = ProofContext.theory_of ctxt
 (* builds the aggregate equivalence relation *)
 (* that will be the argument of Respects     *)
 (* FIXME: check that the types correspond to each other? *)
-fun mk_resp_arg ctxt (rty, qty) =
+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 (mk_resp_arg ctxt) (tys ~~ tys')
+val args = map (equiv_relation ctxt) (tys ~~ tys')
 in
 list_comb (get_relmap ctxt s, args)
 end
 else
 let
 val eqv_rel = get_equiv_rel ctxt s'
 in
 force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
 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
+*)
 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_resp = Const (@{const_name Respects}, dummyT)
 (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 $ mk_resp_arg ctxt (ty, ty')) $ subtrm
+else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ 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 $ mk_resp_arg ctxt (qnt_typ ty, qnt_typ 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 $ mk_resp_arg ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
+else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ 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 mk_resp_arg ctxt (domain_type ty, domain_type ty')
+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 exc = LIFT_MATCH "regularise (relation mismatch)"
 val rel_ty = fastype_of rel
-val rel' = mk_resp_arg ctxt (domain_type rel_ty, domain_type ty')
+val rel' = equiv_relation ctxt (domain_type rel_ty, domain_type ty')
 in
 if rel' aconv rel then rtrm else raise exc
 end
 | (_, Const _) =>
 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
 :

changeset 795	a28f805df355
parent 792	a31cf260eeb3
child 796	64f9c76f70c7