# HG changeset patch # User huffman # Date 1323518458 -3600 # Node ID 0f1c049c147e5dcb12ddb8932ea4cba4ece77881 # Parent 3c609e8785f271f835eada9173a77daa09ad64f2# Parent b16f976db51519b759ed5a4511998922ff574b70 merged diff -r 3c609e8785f2 -r 0f1c049c147e src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sat Dec 10 08:29:19 2011 +0100 +++ b/src/HOL/IsaMakefile Sat Dec 10 13:00:58 2011 +0100 @@ -1508,7 +1508,8 @@ Quotient_Examples/DList.thy Quotient_Examples/Quotient_Cset.thy \ Quotient_Examples/FSet.thy Quotient_Examples/List_Quotient_Cset.thy \ Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy \ - Quotient_Examples/Lift_Set.thy Quotient_Examples/Lift_RBT.thy + Quotient_Examples/Lift_Set.thy Quotient_Examples/Lift_RBT.thy \ + Quotient_Examples/Lift_Fun.thy @$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples diff -r 3c609e8785f2 -r 0f1c049c147e src/HOL/Library/Quotient_List.thy --- a/src/HOL/Library/Quotient_List.thy Sat Dec 10 08:29:19 2011 +0100 +++ b/src/HOL/Library/Quotient_List.thy Sat Dec 10 13:00:58 2011 +0100 @@ -8,7 +8,7 @@ imports Main Quotient_Syntax begin -declare [[map list = (map, list_all2)]] +declare [[map list = list_all2]] lemma map_id [id_simps]: "map id = id" diff -r 3c609e8785f2 -r 0f1c049c147e src/HOL/Library/Quotient_Option.thy --- a/src/HOL/Library/Quotient_Option.thy Sat Dec 10 08:29:19 2011 +0100 +++ b/src/HOL/Library/Quotient_Option.thy Sat Dec 10 13:00:58 2011 +0100 @@ -16,7 +16,7 @@ | "option_rel R None (Some x) = False" | "option_rel R (Some x) (Some y) = R x y" -declare [[map option = (Option.map, option_rel)]] +declare [[map option = option_rel]] lemma option_rel_unfold: "option_rel R x y = (case (x, y) of (None, None) \ True diff -r 3c609e8785f2 -r 0f1c049c147e src/HOL/Library/Quotient_Product.thy --- a/src/HOL/Library/Quotient_Product.thy Sat Dec 10 08:29:19 2011 +0100 +++ b/src/HOL/Library/Quotient_Product.thy Sat Dec 10 13:00:58 2011 +0100 @@ -13,7 +13,7 @@ where "prod_rel R1 R2 = (\(a, b) (c, d). R1 a c \ R2 b d)" -declare [[map prod = (map_pair, prod_rel)]] +declare [[map prod = prod_rel]] lemma prod_rel_apply [simp]: "prod_rel R1 R2 (a, b) (c, d) \ R1 a c \ R2 b d" diff -r 3c609e8785f2 -r 0f1c049c147e src/HOL/Library/Quotient_Sum.thy --- a/src/HOL/Library/Quotient_Sum.thy Sat Dec 10 08:29:19 2011 +0100 +++ b/src/HOL/Library/Quotient_Sum.thy Sat Dec 10 13:00:58 2011 +0100 @@ -16,7 +16,7 @@ | "sum_rel R1 R2 (Inr a2) (Inl b1) = False" | "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2" -declare [[map sum = (sum_map, sum_rel)]] +declare [[map sum = sum_rel]] lemma sum_rel_unfold: "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \ R1 x y diff -r 3c609e8785f2 -r 0f1c049c147e src/HOL/Quickcheck.thy --- a/src/HOL/Quickcheck.thy Sat Dec 10 08:29:19 2011 +0100 +++ b/src/HOL/Quickcheck.thy Sat Dec 10 13:00:58 2011 +0100 @@ -16,9 +16,7 @@ subsection {* Catching Match exceptions *} -definition catch_match :: "'a => 'a => 'a" (* "(bool * term list) option => (bool * term list) option => (bool * term list) option"*) -where - [code del]: "catch_match t1 t2 = (SOME t. t = t1 \ t = t2)" +axiomatization catch_match :: "'a => 'a => 'a" code_const catch_match (Quickcheck "(_) handle Match => _") @@ -157,9 +155,6 @@ no_notation fcomp (infixl "\>" 60) no_notation scomp (infixl "\\" 60) -hide_fact catch_match_def -hide_const (open) catch_match - subsection {* The Random-Predicate Monad *} fun iter' :: @@ -220,9 +215,23 @@ definition map :: "('a \ 'b) \ ('a randompred \ 'b randompred)" where "map f P = bind P (single o f)" -hide_fact (open) iter'.simps iter_def empty_def single_def bind_def union_def if_randompred_def iterate_upto_def not_randompred_def Random_def map_def +hide_fact + random_bool_def random_bool_def_raw + random_itself_def random_itself_def_raw + random_char_def random_char_def_raw + random_literal_def random_literal_def_raw + random_nat_def random_nat_def_raw + random_int_def random_int_def_raw + random_fun_lift_def random_fun_lift_def_raw + random_fun_def random_fun_def_raw + collapse_def collapse_def_raw + beyond_def beyond_def_raw beyond_zero + random_aux_rec + +hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift + +hide_fact (open) iter'.simps iter_def empty_def single_def bind_def union_def if_randompred_def iterate_upto_def not_randompred_def Random_def map_def hide_type (open) randompred -hide_const (open) random collapse beyond random_fun_aux random_fun_lift - iter' iter empty single bind union if_randompred iterate_upto not_randompred Random map +hide_const (open) iter' iter empty single bind union if_randompred iterate_upto not_randompred Random map end diff -r 3c609e8785f2 -r 0f1c049c147e src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Sat Dec 10 08:29:19 2011 +0100 +++ b/src/HOL/Quotient.thy Sat Dec 10 13:00:58 2011 +0100 @@ -671,8 +671,8 @@ use "Tools/Quotient/quotient_info.ML" setup Quotient_Info.setup -declare [[map "fun" = (map_fun, fun_rel)]] -declare [[map set = (vimage, set_rel)]] +declare [[map "fun" = fun_rel]] +declare [[map set = set_rel]] lemmas [quot_thm] = fun_quotient lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp diff -r 3c609e8785f2 -r 0f1c049c147e src/HOL/Quotient_Examples/Lift_Fun.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Quotient_Examples/Lift_Fun.thy Sat Dec 10 13:00:58 2011 +0100 @@ -0,0 +1,82 @@ +(* Title: HOL/Quotient_Examples/Lift_Fun.thy + Author: Ondrej Kuncar +*) + +header {* Example of lifting definitions with contravariant or co/contravariant type variables *} + + +theory Lift_Fun +imports Main +begin + +text {* This file is meant as a test case for features introduced in the changeset 2d8949268303. + It contains examples of lifting definitions with quotients that have contravariant + type variables or type variables which are covariant and contravariant in the same time. *} + +subsection {* Contravariant type variables *} + +text {* 'a is a contravariant type variable and we are able to map over this variable + in the following four definitions. This example is based on HOL/Fun.thy. *} + +quotient_type +('a, 'b) fun' (infixr "\" 55) = "'a \ 'b" / "op =" + by (simp add: identity_equivp) + +quotient_definition "comp' :: ('b \ 'c) \ ('a \ 'b) \ 'a \ 'c" is + "comp :: ('b \ 'c) \ ('a \ 'b) \ 'a \ 'c" + +quotient_definition "fcomp' :: ('a \ 'b) \ ('b \ 'c) \ 'a \ 'c" is + fcomp + +quotient_definition "map_fun' :: ('c \ 'a) \ ('b \ 'd) \ ('a \ 'b) \ 'c \ 'd" + is "map_fun::('c \ 'a) \ ('b \ 'd) \ ('a \ 'b) \ 'c \ 'd" + +quotient_definition "inj_on' :: ('a \ 'b) \ 'a set \ bool" is inj_on + +quotient_definition "bij_betw' :: ('a \ 'b) \ 'a set \ 'b set \ bool" is bij_betw + + +subsection {* Co/Contravariant type variables *} + +text {* 'a is a covariant and contravariant type variable in the same time. + The following example is a bit artificial. We haven't had a natural one yet. *} + +quotient_type 'a endofun = "'a \ 'a" / "op =" by (simp add: identity_equivp) + +definition map_endofun' :: "('a \ 'b) \ ('b \ 'a) \ ('a => 'a) \ ('b => 'b)" + where "map_endofun' f g e = map_fun g f e" + +quotient_definition "map_endofun :: ('a \ 'b) \ ('b \ 'a) \ 'a endofun \ 'b endofun" is + map_endofun' + +text {* Registration of the map function for 'a endofun. *} + +enriched_type map_endofun : map_endofun +proof - + have "\ x. abs_endofun (rep_endofun x) = x" using Quotient_endofun by (auto simp: Quotient_def) + then show "map_endofun id id = id" + by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff) + + have a:"\ x. rep_endofun (abs_endofun x) = x" using Quotient_endofun + Quotient_rep_abs[of "(op =)" abs_endofun rep_endofun] by blast + show "\f g h i. map_endofun f g \ map_endofun h i = map_endofun (f \ h) (i \ g)" + by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff) (simp add: a o_assoc) +qed + +quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a \ 'a) \ ('a \ 'a)" + +term endofun_id_id +thm endofun_id_id_def + +quotient_type 'a endofun' = "'a endofun" / "op =" by (simp add: identity_equivp) + +text {* We have to map "'a endofun" to "('a endofun') endofun", i.e., mapping (lifting) + over a type variable which is a covariant and contravariant type variable. *} + +quotient_definition "endofun'_id_id :: ('a endofun') endofun'" is endofun_id_id + +term endofun'_id_id +thm endofun'_id_id_def + + +end diff -r 3c609e8785f2 -r 0f1c049c147e src/HOL/Quotient_Examples/ROOT.ML --- a/src/HOL/Quotient_Examples/ROOT.ML Sat Dec 10 08:29:19 2011 +0100 +++ b/src/HOL/Quotient_Examples/ROOT.ML Sat Dec 10 13:00:58 2011 +0100 @@ -5,5 +5,5 @@ *) use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Cset", - "List_Quotient_Cset", "Lift_Set", "Lift_RBT"]; + "List_Quotient_Cset", "Lift_Set", "Lift_RBT", "Lift_Fun"]; diff -r 3c609e8785f2 -r 0f1c049c147e src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Dec 10 08:29:19 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Dec 10 13:00:58 2011 +0100 @@ -720,12 +720,12 @@ | is_rep_fun _ _ = false fun is_quot_abs_fun ctxt (x as (_, Type (@{type_name fun}, [_, abs_T as Type (s', _)]))) = - try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s' + try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.AbsF) s' = SOME (Const x) andalso not (is_codatatype ctxt abs_T) | is_quot_abs_fun _ _ = false fun is_quot_rep_fun ctxt (x as (_, Type (@{type_name fun}, [abs_T as Type (s', _), _]))) = - try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s' + try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.RepF) s' = SOME (Const x) andalso not (is_codatatype ctxt abs_T) | is_quot_rep_fun _ _ = false diff -r 3c609e8785f2 -r 0f1c049c147e src/HOL/Tools/Quotient/quotient_def.ML --- a/src/HOL/Tools/Quotient/quotient_def.ML Sat Dec 10 08:29:19 2011 +0100 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Sat Dec 10 13:00:58 2011 +0100 @@ -64,7 +64,7 @@ else error_msg binding lhs_str | _ => raise Match) - val absrep_trm = Quotient_Term.absrep_fun Quotient_Term.AbsF lthy (fastype_of rhs, lhs_ty) $ rhs + val absrep_trm = Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (fastype_of rhs, lhs_ty) $ rhs val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) val (_, prop') = Local_Defs.cert_def lthy prop val (_, newrhs) = Local_Defs.abs_def prop' diff -r 3c609e8785f2 -r 0f1c049c147e src/HOL/Tools/Quotient/quotient_info.ML --- a/src/HOL/Tools/Quotient/quotient_info.ML Sat Dec 10 08:29:19 2011 +0100 +++ b/src/HOL/Tools/Quotient/quotient_info.ML Sat Dec 10 13:00:58 2011 +0100 @@ -6,7 +6,7 @@ signature QUOTIENT_INFO = sig - type quotmaps = {mapfun: string, relmap: string} + type quotmaps = {relmap: string} val lookup_quotmaps: Proof.context -> string -> quotmaps option val lookup_quotmaps_global: theory -> string -> quotmaps option val print_quotmaps: Proof.context -> unit @@ -54,7 +54,7 @@ (* FIXME just one data slot (record) per program unit *) (* info about map- and rel-functions for a type *) -type quotmaps = {mapfun: string, relmap: string} +type quotmaps = {relmap: string} structure Quotmaps = Generic_Data ( @@ -72,20 +72,18 @@ val quotmaps_attribute_setup = Attrib.setup @{binding map} ((Args.type_name false --| Scan.lift (Parse.$$$ "=")) -- (* FIXME Args.type_name true (requires "set" type) *) - (Scan.lift (Parse.$$$ "(") |-- Args.const_proper true --| Scan.lift (Parse.$$$ ",") -- - Args.const_proper true --| Scan.lift (Parse.$$$ ")")) >> - (fn (tyname, (mapname, relname)) => - let val minfo = {mapfun = mapname, relmap = relname} + Args.const_proper true >> + (fn (tyname, relname) => + let val minfo = {relmap = relname} in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end)) "declaration of map information" fun print_quotmaps ctxt = let - fun prt_map (ty_name, {mapfun, relmap}) = + fun prt_map (ty_name, {relmap}) = Pretty.block (separate (Pretty.brk 2) (map Pretty.str ["type:", ty_name, - "map:", mapfun, "relation map:", relmap])) in map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt))) diff -r 3c609e8785f2 -r 0f1c049c147e src/HOL/Tools/Quotient/quotient_term.ML --- a/src/HOL/Tools/Quotient/quotient_term.ML Sat Dec 10 08:29:19 2011 +0100 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Sat Dec 10 13:00:58 2011 +0100 @@ -11,11 +11,11 @@ datatype flag = AbsF | RepF - val absrep_fun: flag -> Proof.context -> typ * typ -> term - val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term + val absrep_fun: Proof.context -> flag -> typ * typ -> term + val absrep_fun_chk: Proof.context -> flag -> typ * typ -> term (* Allows Nitpick to represent quotient types as single elements from raw type *) - val absrep_const_chk: flag -> Proof.context -> string -> term + val absrep_const_chk: Proof.context -> flag -> string -> term val equiv_relation: Proof.context -> typ * typ -> term val equiv_relation_chk: Proof.context -> typ * typ -> term @@ -62,53 +62,30 @@ AbsF => Const (@{const_name comp}, dummyT) $ trm1 $ trm2 | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1 -fun get_mapfun thy s = - (case Quotient_Info.lookup_quotmaps_global thy s of - SOME map_data => Const (#mapfun map_data, dummyT) - | NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")) +fun get_mapfun_data ctxt s = + (case Symtab.lookup (Enriched_Type.entries ctxt) s of + SOME [map_data] => (case try dest_Const (#mapper map_data) of + SOME (c, _) => (Const (c, dummyT), #variances map_data) + | NONE => raise LIFT_MATCH ("map function for type " ^ quote s ^ " is not a constant.")) + | SOME _ => raise LIFT_MATCH ("map function for type " ^ quote s ^ " is non-singleton entry.") + | NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")) +fun defined_mapfun_data ctxt s = + Symtab.defined (Enriched_Type.entries ctxt) s + (* 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 -*) -fun mk_mapfun thy vs rty = - let - val vs' = map mk_Free vs - - fun mk_mapfun_aux rty = - case rty of - TVar _ => mk_Free rty - | Type (_, []) => mk_identity rty - | Type (s, tys) => list_comb (get_mapfun thy s, map mk_mapfun_aux tys) - | _ => raise LIFT_MATCH "mk_mapfun (default)" - in - fold_rev Term.lambda vs' (mk_mapfun_aux rty) - end - (* looks up the (varified) rty and qty for a quotient definition *) -fun get_rty_qty thy s = - (case Quotient_Info.lookup_quotients_global thy s of - SOME qdata => (#rtyp qdata, #qtyp qdata) - | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")) - -(* 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 = +fun get_rty_qty ctxt s = let - val v' = fst (dest_TVar v) + val thy = Proof_Context.theory_of ctxt in - (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v'))) + (case Quotient_Info.lookup_quotients_global thy s of + SOME qdata => (#rtyp qdata, #qtyp qdata) + | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")) end (* matches a type pattern with a type *) @@ -121,7 +98,7 @@ end (* produces the rep or abs constant for a qty *) -fun absrep_const flag ctxt qty_str = +fun absrep_const ctxt flag qty_str = let (* FIXME *) fun mk_dummyT (Const (c, _)) = Const (c, dummyT) @@ -137,8 +114,8 @@ end (* Lets Nitpick represent elements of quotient types as elements of the raw type *) -fun absrep_const_chk flag ctxt qty_str = - Syntax.check_term ctxt (absrep_const flag ctxt qty_str) +fun absrep_const_chk ctxt flag qty_str = + Syntax.check_term ctxt (absrep_const ctxt flag qty_str) fun absrep_match_err ctxt ty_pat ty = let @@ -193,52 +170,71 @@ identity maps. *) -fun absrep_fun flag ctxt (rty, qty) = +fun absrep_fun ctxt flag (rty, qty) = let - val thy = Proof_Context.theory_of ctxt + fun absrep_args tys tys' variances = + let + fun absrep_arg (types, (_, variant)) = + (case variant of + (false, false) => [] + | (true, false) => [(absrep_fun ctxt flag types)] + | (false, true) => [(absrep_fun ctxt (negF flag) types)] + | (true, true) => [(absrep_fun ctxt flag types),(absrep_fun ctxt (negF flag) types)]) + in + maps absrep_arg ((tys ~~ tys') ~~ variances) + end + fun test_identities tys rtys' s s' = + let + val args = map (absrep_fun ctxt flag) (tys ~~ rtys') + in + if forall is_identity args + then + absrep_const ctxt flag s' + else + raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.") + end in if rty = qty then mk_identity rty else case (rty, qty) of - (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => - let - val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1') - val arg2 = absrep_fun flag ctxt (ty2, ty2') - in - list_comb (get_mapfun thy "fun", [arg1, arg2]) - end - (* FIXME: use type_name antiquotation if set type becomes explicit *) - | (Type ("Set.set", [ty]), Type ("Set.set", [ty'])) => - let - val arg = absrep_fun (negF flag) ctxt (ty, ty') - in - get_mapfun thy "Set.set" $ arg - end - | (Type (s, tys), Type (s', tys')) => + (Type (s, tys), Type (s', tys')) => if s = s' then let - val args = map (absrep_fun flag ctxt) (tys ~~ tys') + val (map_fun, variances) = get_mapfun_data ctxt s + val args = absrep_args tys tys' variances in - list_comb (get_mapfun thy s, args) + list_comb (map_fun, args) end else let - val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty thy s' - val rtyenv = match ctxt absrep_match_err rty_pat rty + val (Type (_, rtys), qty_pat) = get_rty_qty ctxt s' val qtyenv = match ctxt absrep_match_err qty_pat qty - val args_aux = map (double_lookup rtyenv qtyenv) vs - val args = map (absrep_fun flag ctxt) args_aux + val rtys' = map (Envir.subst_type qtyenv) rtys in - if forall is_identity args - then absrep_const flag ctxt s' + if not (defined_mapfun_data ctxt s) + then + (* + If we don't know a map function for the raw type, + we are not necessarilly in troubles because + it can still be the case we don't need the map + function <=> all abs/rep functions are identities. + *) + test_identities tys rtys' s s' else let - val map_fun = mk_mapfun thy vs rty_pat - val result = list_comb (map_fun, args) + val (map_fun, variances) = get_mapfun_data ctxt s + val args = absrep_args tys rtys' variances in - mk_fun_compose flag (absrep_const flag ctxt s', result) + if forall is_identity args + then absrep_const ctxt flag s' + else + let + val result = list_comb (map_fun, args) + in + mk_fun_compose flag (absrep_const ctxt flag s', result) + end end end | (TFree x, TFree x') => @@ -249,13 +245,12 @@ | _ => raise (LIFT_MATCH "absrep_fun (default)") end -fun absrep_fun_chk flag ctxt (rty, qty) = - absrep_fun flag ctxt (rty, qty) +fun absrep_fun_chk ctxt flag (rty, qty) = + absrep_fun ctxt flag (rty, qty) |> Syntax.check_term ctxt - (*** Aggregate Equivalence Relation ***) @@ -284,6 +279,17 @@ SOME map_data => Const (#relmap map_data, dummyT) | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")) +(* 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) + in + (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v'))) + end + fun mk_relmap ctxt vs rty = let val vs' = map (mk_Free) vs @@ -316,43 +322,40 @@ that will be the argument of Respects *) fun equiv_relation ctxt (rty, qty) = - let - val thy = Proof_Context.theory_of ctxt - in - 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 (equiv_relation ctxt) (tys ~~ tys') - in - list_comb (get_relmap ctxt s, args) - end - else - let - val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty thy s' - val rtyenv = match ctxt equiv_match_err rty_pat rty - val qtyenv = match ctxt equiv_match_err qty_pat qty - val args_aux = map (double_lookup rtyenv qtyenv) vs - val args = map (equiv_relation ctxt) args_aux - val eqv_rel = get_equiv_rel ctxt s' - val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) - in - if forall is_eq args - then eqv_rel' - else - let - val rel_map = mk_relmap ctxt vs rty_pat - val result = list_comb (rel_map, args) - in - mk_rel_compose (result, eqv_rel') - end - end - | _ => HOLogic.eq_const rty - end + 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 (equiv_relation ctxt) (tys ~~ tys') + in + list_comb (get_relmap ctxt s, args) + end + else + let + val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' + val rtyenv = match ctxt equiv_match_err rty_pat rty + val qtyenv = match ctxt equiv_match_err qty_pat qty + val args_aux = map (double_lookup rtyenv qtyenv) vs + val args = map (equiv_relation ctxt) args_aux + val eqv_rel = get_equiv_rel ctxt s' + val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) + in + if forall is_eq args + then eqv_rel' + else + let + val rel_map = mk_relmap ctxt vs rty_pat + val result = list_comb (rel_map, args) + in + mk_rel_compose (result, eqv_rel') + end + end + | _ => HOLogic.eq_const rty + fun equiv_relation_chk ctxt (rty, qty) = equiv_relation ctxt (rty, qty) @@ -642,7 +645,7 @@ *) fun mk_repabs ctxt (T, T') trm = - absrep_fun RepF ctxt (T, T') $ (absrep_fun AbsF ctxt (T, T') $ trm) + absrep_fun ctxt RepF (T, T') $ (absrep_fun ctxt AbsF (T, T') $ trm) fun inj_repabs_err ctxt msg rtrm qtrm = let diff -r 3c609e8785f2 -r 0f1c049c147e src/HOL/Tools/Quotient/quotient_type.ML --- a/src/HOL/Tools/Quotient/quotient_type.ML Sat Dec 10 08:29:19 2011 +0100 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Sat Dec 10 13:00:58 2011 +0100 @@ -197,13 +197,13 @@ end (* check for existence of map functions *) -fun map_check thy (_, (rty, _, _), _) = +fun map_check ctxt (_, (rty, _, _), _) = let fun map_check_aux rty warns = (case rty of Type (_, []) => warns | Type (s, _) => - if is_some (Quotient_Info.lookup_quotmaps_global thy s) then warns else s :: warns + if Symtab.defined (Enriched_Type.entries ctxt) s then warns else s :: warns | _ => warns) val warns = map_check_aux rty [] @@ -234,7 +234,7 @@ let (* sanity check *) val _ = List.app sanity_check quot_list - val _ = List.app (map_check (Proof_Context.theory_of lthy)) quot_list + val _ = List.app (map_check lthy) quot_list fun mk_goal (rty, rel, partial) = let