--- a/Quot/quotient_term.ML Fri Jan 08 19:46:22 2010 +0100
+++ b/Quot/quotient_term.ML Sat Jan 09 08:52:06 2010 +0100
@@ -7,9 +7,6 @@
val absrep_fun: flag -> Proof.context -> (typ * typ) -> term
val absrep_fun_chk: flag -> Proof.context -> (typ * typ) -> term
- val new_equiv_relation: Proof.context -> (typ * typ) -> term
- val new_equiv_relation_chk: Proof.context -> (typ * typ) -> term
-
val equiv_relation: Proof.context -> (typ * typ) -> term
val equiv_relation_chk: Proof.context -> (typ * typ) -> term
@@ -187,7 +184,8 @@
val map_fun = mk_mapfun ctxt vs rty_pat
val result = list_comb (map_fun, args)
in
- if tys' = [] orelse tys' = tys then absrep_const flag ctxt s'
+ if tys' = [] orelse tys' = tys
+ then absrep_const flag ctxt s'
else mk_fun_compose flag (absrep_const flag ctxt s', result)
end
| (TFree x, TFree x') =>
@@ -262,43 +260,6 @@
(* builds the aggregate equivalence relation *)
(* that will be the argument of Respects *)
-fun new_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 (new_equiv_relation ctxt) (tys ~~ tys')
- in
- list_comb (get_relmap ctxt s, args)
- end
- else
- let
- val thy = ProofContext.theory_of ctxt
- val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
- val rtyenv = Sign.typ_match thy (rty_pat, rty) Vartab.empty
- handle MATCH_TYPE => equiv_match_err ctxt rty_pat rty
- val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty
- handle MATCH_TYPE => equiv_match_err ctxt qty_pat qty
- val args_aux = map (double_lookup rtyenv qtyenv) vs
- val args = map (new_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 tys' = [] orelse tys' = tys then eqv_rel'
- else mk_rel_compose (result, eqv_rel')
- end
- | _ => HOLogic.eq_const rty
-
-fun new_equiv_relation_chk ctxt (rty, qty) =
- new_equiv_relation ctxt (rty, qty)
- |> Syntax.check_term ctxt
-
fun equiv_relation ctxt (rty, qty) =
if rty = qty
then HOLogic.eq_const rty
@@ -314,9 +275,22 @@
end
else
let
+ val thy = ProofContext.theory_of ctxt
+ val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
+ val rtyenv = Sign.typ_match thy (rty_pat, rty) Vartab.empty
+ handle MATCH_TYPE => equiv_match_err ctxt rty_pat rty
+ val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty
+ handle MATCH_TYPE => equiv_match_err ctxt 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
- force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
+ if tys' = [] orelse tys' = tys
+ then eqv_rel'
+ else mk_rel_compose (result, eqv_rel')
end
| _ => HOLogic.eq_const rty
@@ -388,7 +362,7 @@
val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
in
if ty = ty' then subtrm
- else mk_babs $ (mk_resp $ new_equiv_relation 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') =>
@@ -396,7 +370,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 $ new_equiv_relation 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') =>
@@ -404,13 +378,13 @@
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 $ new_equiv_relation 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 new_equiv_relation 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')) =>
@@ -421,7 +395,7 @@
Syntax.string_of_term ctxt rel' ^ " :: " ^
Syntax.string_of_typ ctxt (fastype_of rel') ^ "]")
val rel_ty = fastype_of rel
- val rel' = new_equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
+ val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
in
if rel' aconv rel then rtrm else raise (exc rel rel')
end