explicit handling of mem_def, avoiding the use of the simplifier; this fixes some quotient_type definitions
signature QUOTIENT_TERM =+ −
sig+ −
exception LIFT_MATCH of string+ −
+ −
datatype flag = absF | repF+ −
+ −
val absrep_fun: flag -> Proof.context -> (typ * typ) -> term+ −
val absrep_fun_chk: flag -> 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;+ −
+ − structure Quotient_Term: QUOTIENT_TERM =+ −
struct+ −
+ − open Quotient_Info;+ −
+ − exception LIFT_MATCH of string+ −
+ − (*******************************)+ −
(* Aggregate Rep/Abs Functions *)+ −
(*******************************)+ −
+ − (* The flag repF is for types in negative position, while 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 mk_identity ty = Const (@{const_name "id"}, ty --> ty)+ −
+ − fun mk_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_map ctxt ty_str =+ −
let+ −
val thy = ProofContext.theory_of ctxt+ −
val exc = LIFT_MATCH (space_implode " " ["absrep_fun: no map for type", quote ty_str, "."])+ −
val info = maps_lookup thy ty_str handle NotFound => raise exc+ −
in+ −
Const (#mapfun info, dummyT)+ −
end+ −
+ − fun get_absrep_const flag ctxt _ qty =+ −
(* FIXME: check here that the type-constructors of _ and qty are related *)+ −
let+ −
val thy = ProofContext.theory_of ctxt+ −
val qty_name = Long_Name.base_name (fst (dest_Type qty))+ −
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+ −
+ − fun absrep_fun flag ctxt (rty, qty) =+ −
if rty = qty then mk_identity qty 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_map ctxt "fun", [arg1, arg2])+ −
end+ −
| (Type (s, _), Type (s', [])) =>+ −
if s = s'+ −
then mk_identity qty+ −
else get_absrep_const flag ctxt rty qty+ −
| (Type (s, tys), Type (s', tys')) =>+ −
let+ −
val args = map (absrep_fun flag ctxt) (tys ~~ tys')+ −
val result = list_comb (get_map ctxt s, args)+ −
in+ −
if s = s'+ −
then result+ −
else mk_compose flag (get_absrep_const flag ctxt rty qty, result)+ −
end+ −
| (TFree x, TFree x') =>+ −
if x = x'+ −
then mk_identity qty+ −
else raise (LIFT_MATCH "absrep_fun (frees)")+ −
| (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")+ −
| _ => raise (LIFT_MATCH "absrep_fun (default)")+ −
+ − fun absrep_fun_chk flag ctxt (rty, qty) =+ −
absrep_fun flag ctxt (rty, qty)+ −
|> Syntax.check_term ctxt+ −
+ − + − (* 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+ −
*)+ −
+ − (* builds the aggregate equivalence relation *)+ −
(* that will be the argument of Respects *)+ −
fun mk_resp_arg ctxt (rty, qty) =+ −
let+ −
val thy = ProofContext.theory_of ctxt+ −
in + −
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 exc = LIFT_MATCH ("mk_resp_arg (no map function found for type " ^ s) + −
val map_info = maps_lookup thy s handle NotFound => raise exc+ −
val args = map (mk_resp_arg ctxt) (tys ~~ tys')+ −
in+ −
list_comb (Const (#relfun map_info, dummyT), args) + −
end + −
else + −
let + −
val SOME qinfo = quotdata_lookup_thy thy s'+ −
(* FIXME: check in this case that the rty and qty *)+ −
(* FIXME: correspond to each other *)+ −
val (s, _) = dest_Const (#rel qinfo)+ −
(* FIXME: the relation should only be the string *)+ −
(* FIXME: and the type needs to be calculated as below; *)+ −
(* FIXME: maybe one should actually have a term *)+ −
(* FIXME: and one needs to force it to have this type *)+ −
in+ −
Const (s, rty --> rty --> @{typ bool})+ −
end+ −
| _ => HOLogic.eq_const dummyT + −
(* FIXME: check that the types correspond to each other? *)+ −
end+ −
+ − 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)+ −
+ − (* - 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)+ −
+ − (* the major type of All and Ex quantifiers *)+ −
fun qnt_typ ty = domain_type (domain_type ty) + −
+ − + − (* produces a regularized version of rtrm *)+ −
(* *)+ −
(* - the result still contains 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 $ mk_resp_arg 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+ −
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+ −
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') + −
+ − | (* 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) handle TERM _ => raise exc + −
val rel' = mk_resp_arg ctxt (domain_type rel_ty, domain_type ty') + −
in + −
if rel' aconv rel then rtrm else raise exc+ −
end + −
+ − | (_, Const _) =>+ −
let + −
fun same_name (Const (s, T)) (Const (s', T')) = (s = s') (*andalso (T = T')*)+ −
| same_name _ _ = false+ −
(* TODO/FIXME: This test is not enough. *) + −
(* Why? *)+ −
(* Because constants can have the same name but not be the same+ −
constant. All overloaded constants have the same name but because+ −
of different types they do differ.+ −
+ −
This code will let one write a theorem where plus on nat is+ −
matched to plus on int, even if the latter is defined differently.+ −
+ −
This would result in hard to understand failures in injection and+ −
cleaning. *)+ −
(* cu: if I also test the type, then something else breaks *)+ −
in+ −
if same_name rtrm qtrm then rtrm+ −
else + −
let + −
val thy = ProofContext.theory_of ctxt+ −
val qtrm_str = Syntax.string_of_term ctxt qtrm+ −
val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)")+ −
val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)")+ −
val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1+ −
in + −
if Pattern.matches thy (rtrm', rtrm) + −
then rtrm else raise exc2+ −
end+ −
end + −
+ − | (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 (LIFT_MATCH "regularize (bounds mismatch)")+ −
+ − | _ =>+ −
let + −
val rtrm_str = Syntax.string_of_term ctxt rtrm+ −
val qtrm_str = Syntax.string_of_term ctxt qtrm+ −
in+ −
raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))+ −
end+ −
+ − fun regularize_trm_chk ctxt (rtrm, qtrm) =+ −
regularize_trm ctxt (rtrm, qtrm) + −
|> Syntax.check_term ctxt+ −
+ − (*+ −
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 Re/Abs around it (since bounded abstractions+ −
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 aRep/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)+ −
+ − + − (* 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 + −
+ −
| _ => raise (LIFT_MATCH "injection (default)")+ −
+ − fun inj_repabs_trm_chk ctxt (rtrm, qtrm) =+ −
inj_repabs_trm ctxt (rtrm, qtrm) + −
|> Syntax.check_term ctxt+ −
+ − end; (* structure *)+ −
+ − + − + −