1.1 --- a/src/HOL/Library/Quotient_List.thy Fri Mar 23 14:18:43 2012 +0100
1.2 +++ b/src/HOL/Library/Quotient_List.thy Fri Mar 23 14:20:09 2012 +0100
1.3 @@ -8,8 +8,6 @@
1.4 imports Main Quotient_Syntax
1.5 begin
1.6
1.7 -declare [[map list = list_all2]]
1.8 -
1.9 lemma map_id [id_simps]:
1.10 "map id = id"
1.11 by (fact List.map.id)
1.12 @@ -75,6 +73,8 @@
1.13 by (induct xs ys rule: list_induct2') auto
1.14 qed
1.15
1.16 +declare [[map list = (list_all2, list_quotient)]]
1.17 +
1.18 lemma cons_prs [quot_preserve]:
1.19 assumes q: "Quotient R Abs Rep"
1.20 shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)"
2.1 --- a/src/HOL/Library/Quotient_Option.thy Fri Mar 23 14:18:43 2012 +0100
2.2 +++ b/src/HOL/Library/Quotient_Option.thy Fri Mar 23 14:20:09 2012 +0100
2.3 @@ -16,8 +16,6 @@
2.4 | "option_rel R None (Some x) = False"
2.5 | "option_rel R (Some x) (Some y) = R x y"
2.6
2.7 -declare [[map option = option_rel]]
2.8 -
2.9 lemma option_rel_unfold:
2.10 "option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True
2.11 | (Some x, Some y) \<Rightarrow> R x y
2.12 @@ -65,6 +63,8 @@
2.13 apply (simp add: option_rel_unfold split: option.split)
2.14 done
2.15
2.16 +declare [[map option = (option_rel, option_quotient)]]
2.17 +
2.18 lemma option_None_rsp [quot_respect]:
2.19 assumes q: "Quotient R Abs Rep"
2.20 shows "option_rel R None None"
3.1 --- a/src/HOL/Library/Quotient_Product.thy Fri Mar 23 14:18:43 2012 +0100
3.2 +++ b/src/HOL/Library/Quotient_Product.thy Fri Mar 23 14:20:09 2012 +0100
3.3 @@ -13,8 +13,6 @@
3.4 where
3.5 "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
3.6
3.7 -declare [[map prod = prod_rel]]
3.8 -
3.9 lemma prod_rel_apply [simp]:
3.10 "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
3.11 by (simp add: prod_rel_def)
3.12 @@ -45,6 +43,8 @@
3.13 apply (auto simp add: split_paired_all)
3.14 done
3.15
3.16 +declare [[map prod = (prod_rel, prod_quotient)]]
3.17 +
3.18 lemma Pair_rsp [quot_respect]:
3.19 assumes q1: "Quotient R1 Abs1 Rep1"
3.20 assumes q2: "Quotient R2 Abs2 Rep2"
4.1 --- a/src/HOL/Library/Quotient_Set.thy Fri Mar 23 14:18:43 2012 +0100
4.2 +++ b/src/HOL/Library/Quotient_Set.thy Fri Mar 23 14:20:09 2012 +0100
4.3 @@ -26,6 +26,8 @@
4.4 by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient_def])+
4.5 qed
4.6
4.7 +declare [[map set = (set_rel, set_quotient)]]
4.8 +
4.9 lemma empty_set_rsp[quot_respect]:
4.10 "set_rel R {} {}"
4.11 unfolding set_rel_def by simp
5.1 --- a/src/HOL/Library/Quotient_Sum.thy Fri Mar 23 14:18:43 2012 +0100
5.2 +++ b/src/HOL/Library/Quotient_Sum.thy Fri Mar 23 14:20:09 2012 +0100
5.3 @@ -16,8 +16,6 @@
5.4 | "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
5.5 | "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
5.6
5.7 -declare [[map sum = sum_rel]]
5.8 -
5.9 lemma sum_rel_unfold:
5.10 "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
5.11 | (Inr x, Inr y) \<Rightarrow> R2 x y
5.12 @@ -67,6 +65,8 @@
5.13 apply (simp add: sum_rel_unfold comp_def split: sum.split)
5.14 done
5.15
5.16 +declare [[map sum = (sum_rel, sum_quotient)]]
5.17 +
5.18 lemma sum_Inl_rsp [quot_respect]:
5.19 assumes q1: "Quotient R1 Abs1 Rep1"
5.20 assumes q2: "Quotient R2 Abs2 Rep2"
6.1 --- a/src/HOL/Quotient.thy Fri Mar 23 14:18:43 2012 +0100
6.2 +++ b/src/HOL/Quotient.thy Fri Mar 23 14:20:09 2012 +0100
6.3 @@ -686,8 +686,7 @@
6.4 use "Tools/Quotient/quotient_info.ML"
6.5 setup Quotient_Info.setup
6.6
6.7 -declare [[map "fun" = fun_rel]]
6.8 -declare [[map set = set_rel]]
6.9 +declare [[map "fun" = (fun_rel, fun_quotient)]]
6.10
6.11 lemmas [quot_thm] = fun_quotient
6.12 lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp
7.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML Fri Mar 23 14:18:43 2012 +0100
7.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML Fri Mar 23 14:20:09 2012 +0100
7.3 @@ -6,7 +6,7 @@
7.4
7.5 signature QUOTIENT_INFO =
7.6 sig
7.7 - type quotmaps = {relmap: string}
7.8 + type quotmaps = {relmap: string, quot_thm: thm}
7.9 val lookup_quotmaps: Proof.context -> string -> quotmaps option
7.10 val lookup_quotmaps_global: theory -> string -> quotmaps option
7.11 val print_quotmaps: Proof.context -> unit
7.12 @@ -54,7 +54,7 @@
7.13 (* FIXME just one data slot (record) per program unit *)
7.14
7.15 (* info about map- and rel-functions for a type *)
7.16 -type quotmaps = {relmap: string}
7.17 +type quotmaps = {relmap: string, quot_thm: thm}
7.18
7.19 structure Quotmaps = Generic_Data
7.20 (
7.21 @@ -71,19 +71,24 @@
7.22
7.23 val quotmaps_attribute_setup =
7.24 Attrib.setup @{binding map}
7.25 - ((Args.type_name true --| Scan.lift (@{keyword "="})) -- Args.const_proper true >>
7.26 - (fn (tyname, relname) =>
7.27 - let val minfo = {relmap = relname}
7.28 + ((Args.type_name true --| Scan.lift (@{keyword "="})) --
7.29 + (Scan.lift (@{keyword "("}) |-- Args.const_proper true --| Scan.lift (@{keyword ","}) --
7.30 + Attrib.thm --| Scan.lift (@{keyword ")"})) >>
7.31 + (fn (tyname, (relname, qthm)) =>
7.32 + let val minfo = {relmap = relname, quot_thm = qthm}
7.33 in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end))
7.34 "declaration of map information"
7.35
7.36 fun print_quotmaps ctxt =
7.37 let
7.38 - fun prt_map (ty_name, {relmap}) =
7.39 + fun prt_map (ty_name, {relmap, quot_thm}) =
7.40 Pretty.block (separate (Pretty.brk 2)
7.41 - (map Pretty.str
7.42 - ["type:", ty_name,
7.43 - "relation map:", relmap]))
7.44 + [Pretty.str "type:",
7.45 + Pretty.str ty_name,
7.46 + Pretty.str "relation map:",
7.47 + Pretty.str relmap,
7.48 + Pretty.str "quot. theorem:",
7.49 + Syntax.pretty_term ctxt (prop_of quot_thm)])
7.50 in
7.51 map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt)))
7.52 |> Pretty.big_list "maps for type constructors:"