# HG changeset patch # User Christian Urban # Date 1263339928 -3600 # Node ID 5961edda27d762befac8d4e2e97e6185071b1c92 # Parent 2480fb2a5e4eea404f4ca9060e341331a87afb88 absrep_fun and equiv_relation do not produce anymore spurious maps; two problems arose in IntEx, which are marked with "INJECTION PROBLEM" diff -r 2480fb2a5e4e -r 5961edda27d7 Quot/Examples/FSet3.thy --- a/Quot/Examples/FSet3.thy Tue Jan 12 10:59:51 2010 +0100 +++ b/Quot/Examples/FSet3.thy Wed Jan 13 00:45:28 2010 +0100 @@ -369,8 +369,6 @@ apply(cleaning) apply (simp add: finsert_def fconcat_def comp_def) apply cleaning -(* ID PROBLEM *) -apply(simp add: id_def[symmetric] id_simps) done text {* raw section *} diff -r 2480fb2a5e4e -r 5961edda27d7 Quot/Examples/IntEx.thy --- a/Quot/Examples/IntEx.thy Tue Jan 12 10:59:51 2010 +0100 +++ b/Quot/Examples/IntEx.thy Wed Jan 13 00:45:28 2010 +0100 @@ -252,7 +252,8 @@ apply(lifting lam_tst3a) apply(rule impI) apply(rule lam_tst3a_reg) -done +(* INJECTION PROBLEM *) +oops lemma lam_tst3b: "(\(y :: nat \ nat \ nat \ nat). y) = (\(x :: nat \ nat \ nat \ nat). x)" by auto @@ -262,7 +263,8 @@ apply(rule impI) apply(rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]]) apply(simp add: id_rsp) -done +(* INJECTION PROBLEM *) +oops term map diff -r 2480fb2a5e4e -r 5961edda27d7 Quot/QuotMain.thy --- a/Quot/QuotMain.thy Tue Jan 12 10:59:51 2010 +0100 +++ b/Quot/QuotMain.thy Wed Jan 13 00:45:28 2010 +0100 @@ -108,6 +108,7 @@ fun_map_id[THEN eq_reflection] id_apply[THEN eq_reflection] id_o[THEN eq_reflection] + id_def[symmetric, THEN eq_reflection] o_id[THEN eq_reflection] eq_comp_r diff -r 2480fb2a5e4e -r 5961edda27d7 Quot/quotient_def.ML --- a/Quot/quotient_def.ML Tue Jan 12 10:59:51 2010 +0100 +++ b/Quot/quotient_def.ML Wed Jan 13 00:45:28 2010 +0100 @@ -40,8 +40,8 @@ let val Free (lhs_str, lhs_ty) = lhs; (* FIXME/TODO: this throws an excpt., if the const is already def.*) val qconst_bname = Binding.name lhs_str; - val absrep_trm = (absrep_fun_chk absF lthy (fastype_of rhs, lhs_ty)) $ rhs - val prop = Logic.mk_equals (lhs, absrep_trm) + val absrep_trm = absrep_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs + val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) val (_, prop') = LocalDefs.cert_def lthy prop val (_, newrhs) = Primitive_Defs.abs_def prop' diff -r 2480fb2a5e4e -r 5961edda27d7 Quot/quotient_term.ML --- a/Quot/quotient_term.ML Tue Jan 12 10:59:51 2010 +0100 +++ b/Quot/quotient_term.ML Wed Jan 13 00:45:28 2010 +0100 @@ -24,28 +24,24 @@ exception LIFT_MATCH of string -(* simplifies a term according to the id_rules *) -fun id_simplify ctxt trm = -let - val thy = ProofContext.theory_of ctxt - val id_thms = id_simps_get ctxt -in - MetaSimplifier.rewrite_term thy id_thms [] trm -end - -(******************************) -(* Aggregate Rep/Abs Function *) -(******************************) + + +(*** Aggregate Rep/Abs Function ***) + -(* The flag repF is for types in negative position; absF is for types *) -(* in positive position. Because of this, function types need to be *) -(* treated specially, since there the polarity changes. *) +(* The flag repF is for types in negative position; 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 is_identity (Const (@{const_name "id"}, _)) = true + | is_identity _ = false + fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) fun mk_fun_compose flag (trm1, trm2) = @@ -65,13 +61,14 @@ (* makes a Free out of a TVar *) fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT) -(* 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) *) -(* *) -(* for example for: (?'a list * ?'b) *) -(* it produces: %a b. prod_map (map a) b *) +(* 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) + + for example for: (?'a list * ?'b) + it produces: %a b. prod_map (map a) b +*) fun mk_mapfun ctxt vs rty = let val vs' = map (mk_Free) vs @@ -86,8 +83,9 @@ fold_rev Term.lambda vs' (mk_mapfun_aux rty) end -(* looks up the (varified) rty and qty for *) -(* a quotient definition *) +(* looks up the (varified) rty and qty for + a quotient definition +*) fun get_rty_qty ctxt s = let val thy = ProofContext.theory_of ctxt @@ -97,9 +95,10 @@ (#rtyp qdata, #qtyp qdata) end -(* takes two type-environments and looks *) -(* up in both of them the variable v, which *) -(* must be listed in the environment *) +(* 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) @@ -136,38 +135,49 @@ ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) end -(* produces an aggregate absrep function *) -(* *) -(* - In case of equal types we just return the identity. *) -(* *) -(* - 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 *) -(* arguments and build the appropriate map function. *) -(* *) -(* - If the type constructors are unequal, there must be an *) -(* instance of quotient types: *) -(* - we first look up the corresponding rty_pat and qty_pat *) -(* from the quotient definition; the arguments of qty_pat *) -(* must be some distinct TVars *) -(* - we then match the rty_pat with rty and qty_pat with qty; *) -(* if matching fails the types do not match *) -(* - the matching produces two environments; we look up the *) -(* assignments for the qty_pat variables and recurse on the *) -(* assignments *) -(* - we prefix the aggregate map function for the rty_pat, *) -(* which is an abstraction over all type variables *) -(* - finally we compose the result with the appropriate *) -(* absrep function *) -(* *) -(* The composition is necessary for types like *) -(* *) -(* ('a list) list / ('a foo) foo *) -(* *) -(* The matching is necessary for types like *) -(* *) -(* ('a * 'a) list / 'a bar *) + +(** generation of an aggregate absrep function **) + +(* - In case of equal types we just return the identity. + + - In case of TFrees we also return the identity. + + - In case of function types we recurse taking + the polarity change into account. + + - If the type constructors are equal, we recurse for the + arguments and build the appropriate map function. + + - If the type constructors are unequal, there must be an + instance of quotient types: + + - we first look up the corresponding rty_pat and qty_pat + from the quotient definition; the arguments of qty_pat + must be some distinct TVars + - we then match the rty_pat with rty and qty_pat with qty; + if matching fails the types do not correspond -> error + - the matching produces two environments; we look up the + assignments for the qty_pat variables and recurse on the + assignments + - we prefix the aggregate map function for the rty_pat, + which is an abstraction over all type variables + - finally we compose the result with the appropriate + absrep function in case at least one argument produced + a non-identity function / + otherwise we just return the appropriate absrep + function + + The composition is necessary for types like + + ('a list) list / ('a foo) foo + + The matching is necessary for types like + + ('a * 'a) list / 'a bar + + The test is necessary in order to eliminate superflous + identity maps. +*) fun absrep_fun flag ctxt (rty, qty) = if rty = qty @@ -194,12 +204,14 @@ val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' val rtyenv = match ctxt absrep_match_err rty_pat rty val qtyenv = match ctxt absrep_match_err qty_pat qty - val args_aux = map (double_lookup rtyenv qtyenv) vs + 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 - mk_fun_compose flag (absrep_const flag ctxt s', result) + if forall is_identity args + then absrep_const flag ctxt s' + else mk_fun_compose flag (absrep_const flag ctxt s', result) end | (TFree x, TFree x') => if x = x' @@ -211,11 +223,16 @@ fun absrep_fun_chk flag ctxt (rty, qty) = absrep_fun flag ctxt (rty, qty) |> Syntax.check_term ctxt - |> id_simplify ctxt + + + -(**********************************) -(* Aggregate Equivalence Relation *) -(**********************************) +(*** Aggregate Equivalence Relation ***) + + +(* works very similar to the absrep generation, + except there is no need for polarities +*) (* instantiates TVars so that the term is of type ty *) fun force_typ ctxt trm ty = @@ -227,9 +244,11 @@ map_types (Envir.subst_type ty_inst) trm end +fun is_eq (Const (@{const_name "op ="}, _)) = true + | is_eq _ = false + fun mk_rel_compose (trm1, trm2) = - Const (@{const_name "pred_comp"}, dummyT) $ trm1 $ - (Const (@{const_name "pred_comp"}, dummyT) $ trm2 $ trm1) + Const (@{const_name "rel_conj"}, dummyT) $ trm1 $ trm2 fun get_relmap ctxt s = let @@ -271,8 +290,9 @@ ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) end -(* builds the aggregate equivalence relation *) -(* that will be the argument of Respects *) +(* builds the aggregate equivalence relation + that will be the argument of Respects +*) fun equiv_relation ctxt (rty, qty) = if rty = qty then HOLogic.eq_const rty @@ -298,19 +318,19 @@ val eqv_rel = get_equiv_rel ctxt s' val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) in - mk_rel_compose (result, eqv_rel') + if forall is_eq args + then eqv_rel' + else mk_rel_compose (result, eqv_rel') end | _ => HOLogic.eq_const rty fun equiv_relation_chk ctxt (rty, qty) = equiv_relation ctxt (rty, qty) |> Syntax.check_term ctxt - |> id_simplify ctxt -(******************) -(* Regularization *) -(******************) + +(*** Regularization ***) (* Regularizing an rtrm means: @@ -344,10 +364,11 @@ 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 *) +(* - 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')) @@ -356,14 +377,13 @@ (* the major type of All and Ex quantifiers *) fun qnt_typ ty = domain_type (domain_type ty) +(* produces a regularized version of rtrm -(* produces a regularized version of rtrm *) -(* *) -(* - the result might contain dummyTs *) -(* *) -(* - for regularisation we do not need any *) -(* special treatment of bound variables *) + - the result might contain 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')) => @@ -465,7 +485,6 @@ fun regularize_trm_chk ctxt (rtrm, qtrm) = regularize_trm ctxt (rtrm, qtrm) |> Syntax.check_term ctxt - |> id_simplify ctxt (*********************) @@ -567,7 +586,6 @@ fun inj_repabs_trm_chk ctxt (rtrm, qtrm) = inj_repabs_trm ctxt (rtrm, qtrm) |> Syntax.check_term ctxt - |> id_simplify ctxt end; (* structure *)