--- 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
--- 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"
--- 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) \<Rightarrow> True
--- 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 = (\<lambda>(a, b) (c, d). R1 a c \<and> 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) \<longleftrightarrow> R1 a c \<and> R2 b d"
--- 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) \<Rightarrow> R1 x y
--- 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 \<or> t = t2)"
+axiomatization catch_match :: "'a => 'a => 'a"
code_const catch_match
(Quickcheck "(_) handle Match => _")
@@ -157,9 +155,6 @@
no_notation fcomp (infixl "\<circ>>" 60)
no_notation scomp (infixl "\<circ>\<rightarrow>" 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 \<Rightarrow> 'b) \<Rightarrow> ('a randompred \<Rightarrow> '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
--- 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
--- /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 "\<rightarrow>" 55) = "'a \<Rightarrow> 'b" / "op ="
+ by (simp add: identity_equivp)
+
+quotient_definition "comp' :: ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'c" is
+ "comp :: ('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"
+
+quotient_definition "fcomp' :: ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" is
+ fcomp
+
+quotient_definition "map_fun' :: ('c \<rightarrow> 'a) \<rightarrow> ('b \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'c \<rightarrow> 'd"
+ is "map_fun::('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd"
+
+quotient_definition "inj_on' :: ('a \<rightarrow> 'b) \<rightarrow> 'a set \<rightarrow> bool" is inj_on
+
+quotient_definition "bij_betw' :: ('a \<rightarrow> 'b) \<rightarrow> 'a set \<rightarrow> 'b set \<rightarrow> 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 \<Rightarrow> 'a" / "op =" by (simp add: identity_equivp)
+
+definition map_endofun' :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> ('a => 'a) \<Rightarrow> ('b => 'b)"
+ where "map_endofun' f g e = map_fun g f e"
+
+quotient_definition "map_endofun :: ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a endofun \<Rightarrow> 'b endofun" is
+ map_endofun'
+
+text {* Registration of the map function for 'a endofun. *}
+
+enriched_type map_endofun : map_endofun
+proof -
+ have "\<forall> 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:"\<forall> x. rep_endofun (abs_endofun x) = x" using Quotient_endofun
+ Quotient_rep_abs[of "(op =)" abs_endofun rep_endofun] by blast
+ show "\<And>f g h i. map_endofun f g \<circ> map_endofun h i = map_endofun (f \<circ> h) (i \<circ> 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 \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> '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
--- 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"];
--- 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
--- 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'
--- 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)))
--- 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
--- 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