# HG changeset patch
# User kuncar
# Date 1332508809 -3600
# Node ID 1a7ad2601cb53e9630ad21ac55c0646f76c71e5e
# Parent  0516a6c1ea590f9b7eaf60d58a2709621953f353
store the relational theorem for every relator

diff -r 0516a6c1ea59 -r 1a7ad2601cb5 src/HOL/Library/Quotient_List.thy
--- a/src/HOL/Library/Quotient_List.thy	Fri Mar 23 14:18:43 2012 +0100
+++ b/src/HOL/Library/Quotient_List.thy	Fri Mar 23 14:20:09 2012 +0100
@@ -8,8 +8,6 @@
 imports Main Quotient_Syntax
 begin
 
-declare [[map list = list_all2]]
-
 lemma map_id [id_simps]:
   "map id = id"
   by (fact List.map.id)
@@ -75,6 +73,8 @@
     by (induct xs ys rule: list_induct2') auto
 qed
 
+declare [[map list = (list_all2, list_quotient)]]
+
 lemma cons_prs [quot_preserve]:
   assumes q: "Quotient R Abs Rep"
   shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)"
diff -r 0516a6c1ea59 -r 1a7ad2601cb5 src/HOL/Library/Quotient_Option.thy
--- a/src/HOL/Library/Quotient_Option.thy	Fri Mar 23 14:18:43 2012 +0100
+++ b/src/HOL/Library/Quotient_Option.thy	Fri Mar 23 14:20:09 2012 +0100
@@ -16,8 +16,6 @@
 | "option_rel R None (Some x) = False"
 | "option_rel R (Some x) (Some y) = R x y"
 
-declare [[map option = option_rel]]
-
 lemma option_rel_unfold:
   "option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True
     | (Some x, Some y) \<Rightarrow> R x y
@@ -65,6 +63,8 @@
   apply (simp add: option_rel_unfold split: option.split)
   done
 
+declare [[map option = (option_rel, option_quotient)]]
+
 lemma option_None_rsp [quot_respect]:
   assumes q: "Quotient R Abs Rep"
   shows "option_rel R None None"
diff -r 0516a6c1ea59 -r 1a7ad2601cb5 src/HOL/Library/Quotient_Product.thy
--- a/src/HOL/Library/Quotient_Product.thy	Fri Mar 23 14:18:43 2012 +0100
+++ b/src/HOL/Library/Quotient_Product.thy	Fri Mar 23 14:20:09 2012 +0100
@@ -13,8 +13,6 @@
 where
   "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
 
-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"
   by (simp add: prod_rel_def)
@@ -45,6 +43,8 @@
   apply (auto simp add: split_paired_all)
   done
 
+declare [[map prod = (prod_rel, prod_quotient)]]
+
 lemma Pair_rsp [quot_respect]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
diff -r 0516a6c1ea59 -r 1a7ad2601cb5 src/HOL/Library/Quotient_Set.thy
--- a/src/HOL/Library/Quotient_Set.thy	Fri Mar 23 14:18:43 2012 +0100
+++ b/src/HOL/Library/Quotient_Set.thy	Fri Mar 23 14:20:09 2012 +0100
@@ -26,6 +26,8 @@
     by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient_def])+
 qed
 
+declare [[map set = (set_rel, set_quotient)]]
+
 lemma empty_set_rsp[quot_respect]:
   "set_rel R {} {}"
   unfolding set_rel_def by simp
diff -r 0516a6c1ea59 -r 1a7ad2601cb5 src/HOL/Library/Quotient_Sum.thy
--- a/src/HOL/Library/Quotient_Sum.thy	Fri Mar 23 14:18:43 2012 +0100
+++ b/src/HOL/Library/Quotient_Sum.thy	Fri Mar 23 14:20:09 2012 +0100
@@ -16,8 +16,6 @@
 | "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
 | "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
 
-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
     | (Inr x, Inr y) \<Rightarrow> R2 x y
@@ -67,6 +65,8 @@
   apply (simp add: sum_rel_unfold comp_def split: sum.split)
   done
 
+declare [[map sum = (sum_rel, sum_quotient)]]
+
 lemma sum_Inl_rsp [quot_respect]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
diff -r 0516a6c1ea59 -r 1a7ad2601cb5 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Fri Mar 23 14:18:43 2012 +0100
+++ b/src/HOL/Quotient.thy	Fri Mar 23 14:20:09 2012 +0100
@@ -686,8 +686,7 @@
 use "Tools/Quotient/quotient_info.ML"
 setup Quotient_Info.setup
 
-declare [[map "fun" = fun_rel]]
-declare [[map set = set_rel]]
+declare [[map "fun" = (fun_rel, fun_quotient)]]
 
 lemmas [quot_thm] = fun_quotient
 lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp
diff -r 0516a6c1ea59 -r 1a7ad2601cb5 src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Fri Mar 23 14:18:43 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Fri Mar 23 14:20:09 2012 +0100
@@ -6,7 +6,7 @@
 
 signature QUOTIENT_INFO =
 sig
-  type quotmaps = {relmap: string}
+  type quotmaps = {relmap: string, quot_thm: thm}
   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 = {relmap: string}
+type quotmaps = {relmap: string, quot_thm: thm}
 
 structure Quotmaps = Generic_Data
 (
@@ -71,19 +71,24 @@
 
 val quotmaps_attribute_setup =
   Attrib.setup @{binding map}
-    ((Args.type_name true --| Scan.lift (@{keyword "="})) -- Args.const_proper true >>
-      (fn (tyname, relname) =>
-        let val minfo = {relmap = relname}
+    ((Args.type_name true --| Scan.lift (@{keyword "="})) --
+      (Scan.lift (@{keyword "("}) |-- Args.const_proper true --| Scan.lift (@{keyword ","}) --
+        Attrib.thm --| Scan.lift (@{keyword ")"})) >>
+      (fn (tyname, (relname, qthm)) =>
+        let val minfo = {relmap = relname, quot_thm = qthm}
         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, {relmap}) =
+    fun prt_map (ty_name, {relmap, quot_thm}) =
       Pretty.block (separate (Pretty.brk 2)
-        (map Pretty.str
-         ["type:", ty_name,
-          "relation map:", relmap]))
+         [Pretty.str "type:", 
+          Pretty.str ty_name,
+          Pretty.str "relation map:", 
+          Pretty.str relmap,
+          Pretty.str "quot. theorem:", 
+          Syntax.pretty_term ctxt (prop_of quot_thm)])
   in
     map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt)))
     |> Pretty.big_list "maps for type constructors:"