# HG changeset patch # User Christian Urban # Date 1263023526 -3600 # Node ID 224909b9399f20d2db6ebe27eea59b19c3bacc55 # Parent 89d772dae4d40b97780f2a23072a413897ad454c removed obsolete equiv_relation and rnamed new_equiv_relation diff -r 89d772dae4d4 -r 224909b9399f Quot/Examples/AbsRepTest.thy --- a/Quot/Examples/AbsRepTest.thy Fri Jan 08 19:46:22 2010 +0100 +++ b/Quot/Examples/AbsRepTest.thy Sat Jan 09 08:52:06 2010 +0100 @@ -11,9 +11,6 @@ |> writeln; equiv_relation_chk ctxt (rty, qty) |> Syntax.string_of_term ctxt - |> writeln; - new_equiv_relation_chk ctxt (rty, qty) - |> Syntax.string_of_term ctxt |> writeln) *} diff -r 89d772dae4d4 -r 224909b9399f Quot/quotient_term.ML --- 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