# HG changeset patch # User Christian Urban # Date 1263370760 -3600 # Node ID 433f7c17255f6bd3936a4535faa578e6d3dc2e79 # Parent 017cb46b27bb67bd7dd754adb26f46c928bd5e1c# Parent 3fd1365f57295c58b66603a72799dc7fad3d9fea merged diff -r 3fd1365f5729 -r 433f7c17255f Quot/Examples/FSet3.thy --- a/Quot/Examples/FSet3.thy Tue Jan 12 17:46:35 2010 +0100 +++ b/Quot/Examples/FSet3.thy Wed Jan 13 09:19:20 2010 +0100 @@ -368,8 +368,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 3fd1365f5729 -r 433f7c17255f Quot/Examples/IntEx.thy --- a/Quot/Examples/IntEx.thy Tue Jan 12 17:46:35 2010 +0100 +++ b/Quot/Examples/IntEx.thy Wed Jan 13 09:19:20 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 --- possibly now id_def is part of id_simps again *) +oops term map diff -r 3fd1365f5729 -r 433f7c17255f Quot/QuotMain.thy --- a/Quot/QuotMain.thy Tue Jan 12 17:46:35 2010 +0100 +++ b/Quot/QuotMain.thy Wed Jan 13 09:19:20 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 3fd1365f5729 -r 433f7c17255f Quot/quotient_def.ML --- a/Quot/quotient_def.ML Tue Jan 12 17:46:35 2010 +0100 +++ b/Quot/quotient_def.ML Wed Jan 13 09:19:20 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 3fd1365f5729 -r 433f7c17255f Quot/quotient_term.ML --- a/Quot/quotient_term.ML Tue Jan 12 17:46:35 2010 +0100 +++ b/Quot/quotient_term.ML Wed Jan 13 09:19:20 2010 +0100 @@ -24,27 +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 ***) -(* 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) = @@ -64,12 +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 @@ -84,7 +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 @@ -94,8 +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) @@ -132,38 +135,50 @@ ["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. +(** generation of an aggregate absrep 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 +(* - 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 composition is necessary for types like - - ('a list) list / ('a foo) foo + The test is necessary in order to eliminate superflous + identity maps. +*) - The matching is necessary for types like - - ('a * 'a) list / 'a bar *) fun absrep_fun flag ctxt (rty, qty) = if rty = qty then mk_identity rty @@ -189,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' @@ -206,12 +223,17 @@ fun absrep_fun_chk flag ctxt (rty, qty) = absrep_fun flag ctxt (rty, qty) |> Syntax.check_term ctxt - |> id_simplify ctxt + (*** 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 = let @@ -222,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 @@ -266,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 @@ -293,31 +318,32 @@ 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 ***) (* Regularizing an rtrm means: - - - Quantifiers over types that need lifting are replaced + + - 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 @@ -338,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')) @@ -350,10 +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 to treat bound variables specially *) + - 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')) => @@ -455,7 +485,6 @@ fun regularize_trm_chk ctxt (rtrm, qtrm) = regularize_trm ctxt (rtrm, qtrm) |> Syntax.check_term ctxt - |> id_simplify ctxt @@ -555,7 +584,6 @@ fun inj_repabs_trm_chk ctxt (rtrm, qtrm) = inj_repabs_trm ctxt (rtrm, qtrm) |> Syntax.check_term ctxt - |> id_simplify ctxt end; (* structure *)