--- a/Quot/quotient_term.ML Sat Dec 26 20:45:37 2009 +0100
+++ b/Quot/quotient_term.ML Sat Dec 26 21:36:20 2009 +0100
@@ -7,6 +7,9 @@
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
@@ -57,7 +60,7 @@
(* 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
@@ -83,8 +86,9 @@
(#rtyp qdata, #qtyp qdata)
end
-(* receives two type-environments and looks *)
-(* up in both of them the variable v *)
+(* 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)
@@ -103,7 +107,16 @@
| 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. *)
@@ -157,12 +170,11 @@
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) =
- (Sign.typ_match thy (rty_pat, rty) Vartab.empty,
- Sign.typ_match thy (qty_pat, qty) Vartab.empty)
- handle MATCH_TYPE => raise exc
+ val rtyenv = Sign.typ_match thy (rty_pat, rty) Vartab.empty
+ handle MATCH_TYPE => absrep_match_err ctxt rty_pat rty
+ val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty
+ 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
@@ -182,31 +194,9 @@
|> 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
-*)
+(**********************************)
+(* Aggregate Equivalence Relation *)
+(**********************************)
(* instantiates TVars so that the term is of type ty *)
fun force_typ ctxt trm ty =
@@ -239,7 +229,7 @@
(* 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
@@ -248,7 +238,7 @@
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
@@ -259,6 +249,42 @@
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)
@@ -292,7 +318,7 @@
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') =>
@@ -300,7 +326,7 @@
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') =>
@@ -308,20 +334,20 @@
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
@@ -376,6 +402,10 @@
regularize_trm ctxt (rtrm, qtrm)
|> Syntax.check_term ctxt
+(*********************)
+(* Rep/Abs Injection *)
+(*********************)
+
(*
Injection of Rep/Abs means: