# HG changeset patch
# User wenzelm
# Date 1518810265 -3600
# Node ID 9a1212f4393e4692a79a57b55c3c95297ad5fa48
# Parent  3b94553353ae628202d3d3d2cae4df857e02a2d5
clarified data operations, with trim_context and transfer;

diff -r 3b94553353ae -r 9a1212f4393e src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Fri Feb 16 19:58:42 2018 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Fri Feb 16 20:44:25 2018 +0100
@@ -9,6 +9,7 @@
   type quotmaps = {relmap: string, quot_thm: thm}
   val lookup_quotmaps: Proof.context -> string -> quotmaps option
   val lookup_quotmaps_global: theory -> string -> quotmaps option
+  val update_quotmaps: string * quotmaps -> Context.generic -> Context.generic
   val print_quotmaps: Proof.context -> unit
 
   type abs_rep = {abs : term, rep : term}
@@ -30,10 +31,10 @@
   val transform_quotconsts: morphism -> quotconsts -> quotconsts
   val lookup_quotconsts_global: theory -> term -> quotconsts option
   val update_quotconsts: string * quotconsts -> Context.generic -> Context.generic
+  val dest_quotconsts: Proof.context -> quotconsts list
   val dest_quotconsts_global: theory -> quotconsts list
-  val dest_quotconsts: Proof.context -> quotconsts list
   val print_quotconsts: Proof.context -> unit
-end;
+end
 
 structure Quotient_Info: QUOTIENT_INFO =
 struct
@@ -42,20 +43,23 @@
 
 (*info about map- and rel-functions for a type*)
 type quotmaps = {relmap: string, quot_thm: thm}
+fun transform_quotmaps phi : quotmaps -> quotmaps =
+  fn {relmap, quot_thm} => {relmap = relmap, quot_thm = Morphism.thm phi quot_thm}
 
 (*info about abs/rep terms*)
 type abs_rep = {abs : term, rep : term}
-fun transform_abs_rep phi {abs, rep} : abs_rep =
-  {abs = Morphism.term phi abs, rep = Morphism.term phi rep}
+fun transform_abs_rep phi : abs_rep -> abs_rep =
+  fn {abs, rep} => {abs = Morphism.term phi abs, rep = Morphism.term phi rep}
 
 (*info about quotient types*)
 type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm, quot_thm: thm}
-fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} : quotients =
-  {qtyp = Morphism.typ phi qtyp,
-   rtyp = Morphism.typ phi rtyp,
-   equiv_rel = Morphism.term phi equiv_rel,
-   equiv_thm = Morphism.thm phi equiv_thm,
-   quot_thm = Morphism.thm phi quot_thm}
+fun transform_quotients phi : quotients -> quotients =
+  fn {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} =>
+    {qtyp = Morphism.typ phi qtyp,
+     rtyp = Morphism.typ phi rtyp,
+     equiv_rel = Morphism.term phi equiv_rel,
+     equiv_thm = Morphism.thm phi equiv_thm,
+     quot_thm = Morphism.thm phi quot_thm}
 
 (*info about quotient constants*)
 (*We need to be able to lookup instances of lifted constants,
@@ -63,10 +67,11 @@
   but overloaded constants share the same name.*)
 type quotconsts = {qconst: term, rconst: term, def: thm}
 fun eq_quotconsts (x: quotconsts, y: quotconsts) = #qconst x = #qconst y
-fun transform_quotconsts phi {qconst, rconst, def} : quotconsts =
-  {qconst = Morphism.term phi qconst,
-   rconst = Morphism.term phi rconst,
-   def = Morphism.thm phi def}
+fun transform_quotconsts phi : quotconsts -> quotconsts =
+  fn {qconst, rconst, def} =>
+    {qconst = Morphism.term phi qconst,
+     rconst = Morphism.term phi rconst,
+     def = Morphism.thm phi def}
 
 structure Data = Generic_Data
 (
@@ -99,10 +104,15 @@
 
 (* quotmaps *)
 
-val lookup_quotmaps = Symtab.lookup o get_quotmaps o Context.Proof
-val lookup_quotmaps_global = Symtab.lookup o get_quotmaps o Context.Theory
+fun lookup_quotmaps_generic context name =
+  Symtab.lookup (get_quotmaps context) name
+  |> Option.map (transform_quotmaps (Morphism.transfer_morphism (Context.theory_of context)))
 
-(* FIXME export proper internal update operation!? *)
+val lookup_quotmaps = lookup_quotmaps_generic o Context.Proof
+val lookup_quotmaps_global = lookup_quotmaps_generic o Context.Theory
+
+val update_quotmaps =
+  map_quotmaps o Symtab.update o apsnd (transform_quotmaps Morphism.trim_context_morphism)
 
 val _ =
   Theory.setup
@@ -112,8 +122,8 @@
           Args.const {proper = true, strict = true} --| Scan.lift @{keyword ","} --
           Attrib.thm --| Scan.lift @{keyword ")"}) >>
         (fn (tyname, (relmap, quot_thm)) =>
-          let val minfo = {relmap = relmap, quot_thm = quot_thm}
-          in Thm.declaration_attribute (K (map_quotmaps (Symtab.update (tyname, minfo)))) end))
+          Thm.declaration_attribute
+            (K (update_quotmaps (tyname, {relmap = relmap, quot_thm = quot_thm})))))
       "declaration of map information")
 
 fun print_quotmaps ctxt =
@@ -138,7 +148,8 @@
 val lookup_abs_rep = Symtab.lookup o get_abs_rep o Context.Proof
 val lookup_abs_rep_global = Symtab.lookup o get_abs_rep o Context.Theory
 
-val update_abs_rep = map_abs_rep o Symtab.update
+val update_abs_rep =
+  map_abs_rep o Symtab.update o apsnd (transform_abs_rep Morphism.trim_context_morphism)
 
 fun print_abs_rep ctxt =
   let
@@ -159,10 +170,15 @@
 
 (* quotients *)
 
-val lookup_quotients = Symtab.lookup o get_quotients o Context.Proof
-val lookup_quotients_global = Symtab.lookup o get_quotients o Context.Theory
+fun lookup_quotients_generic context name =
+  Symtab.lookup (get_quotients context) name
+  |> Option.map (transform_quotients (Morphism.transfer_morphism (Context.theory_of context)))
 
-val update_quotients = map_quotients o Symtab.update
+val lookup_quotients = lookup_quotients_generic o Context.Proof
+val lookup_quotients_global = lookup_quotients_generic o Context.Theory
+
+val update_quotients =
+  map_quotients o Symtab.update o apsnd (transform_quotients Morphism.trim_context_morphism)
 
 fun dest_quotients ctxt =
   map snd (Symtab.dest (get_quotients (Context.Proof ctxt)))
@@ -190,24 +206,25 @@
 
 (* quotconsts *)
 
-val update_quotconsts = map_quotconsts o Symtab.cons_list
+val update_quotconsts =
+  map_quotconsts o Symtab.cons_list o apsnd (transform_quotconsts Morphism.trim_context_morphism)
 
-fun dest_quotconsts ctxt =
-  maps snd (Symtab.dest (get_quotconsts (Context.Proof ctxt)))
+fun dest_quotconsts_generic context =
+  maps #2 (Symtab.dest (get_quotconsts context))
+  |> map (transform_quotconsts (Morphism.transfer_morphism (Context.theory_of context)))
 
-fun dest_quotconsts_global thy =
-  maps snd (Symtab.dest (get_quotconsts (Context.Theory thy)))
+val dest_quotconsts = dest_quotconsts_generic o Context.Proof
+val dest_quotconsts_global = dest_quotconsts_generic o Context.Theory
 
 fun lookup_quotconsts_global thy t =
   let
     val (name, qty) = dest_Const t
-    fun matches ({qconst, ...}: quotconsts) =
-      let val (name', qty') = dest_Const qconst;
-      in name = name' andalso Sign.typ_instance thy (qty, qty') end
   in
-    (case Symtab.lookup (get_quotconsts (Context.Theory thy)) name of
-      NONE => NONE
-    | SOME l => find_first matches l)
+    Symtab.lookup_list (get_quotconsts (Context.Theory thy)) name
+    |> find_first (fn {qconst, ...} =>
+        let val (name', qty') = dest_Const qconst
+        in name = name' andalso Sign.typ_instance thy (qty, qty') end)
+    |> Option.map (transform_quotconsts (Morphism.transfer_morphism thy))
   end
 
 fun print_quotconsts ctxt =
@@ -220,7 +237,7 @@
         Pretty.str "as",
         Syntax.pretty_term ctxt (Thm.prop_of def)])
   in
-    map prt_qconst (maps snd (Symtab.dest (get_quotconsts (Context.Proof ctxt))))
+    map prt_qconst (dest_quotconsts ctxt)
     |> Pretty.big_list "quotient constants:"
     |> Pretty.writeln
   end
@@ -240,4 +257,4 @@
   Outer_Syntax.command @{command_keyword print_quotconsts} "print quotient constants"
     (Scan.succeed (Toplevel.keep (print_quotconsts o Toplevel.context_of)))
 
-end;
+end
diff -r 3b94553353ae -r 9a1212f4393e src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Fri Feb 16 19:58:42 2018 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Fri Feb 16 20:44:25 2018 +0100
@@ -335,22 +335,14 @@
 exception CODE_GEN of string
 
 fun get_quot_thm ctxt s =
-  let
-    val thy = Proof_Context.theory_of ctxt
-  in
-    (case Quotient_Info.lookup_quotients ctxt s of
-      SOME {quot_thm, ...} => Thm.transfer thy quot_thm
-    | NONE => raise CODE_GEN ("No quotient type " ^ quote s ^ " found."))
-  end
+  (case Quotient_Info.lookup_quotients ctxt s of
+    SOME {quot_thm, ...} => quot_thm
+  | NONE => raise CODE_GEN ("No quotient type " ^ quote s ^ " found."));
 
 fun get_rel_quot_thm ctxt s =
-   let
-    val thy = Proof_Context.theory_of ctxt
-  in
-    (case Quotient_Info.lookup_quotmaps ctxt s of
-      SOME {quot_thm, ...} => Thm.transfer thy quot_thm
-    | NONE => raise CODE_GEN ("get_relmap (no relation map function found for type " ^ s ^ ")"))
-  end
+  (case Quotient_Info.lookup_quotmaps ctxt s of
+    SOME {quot_thm, ...} => quot_thm
+  | NONE => raise CODE_GEN ("get_relmap (no relation map function found for type " ^ s ^ ")"));
 
 fun is_id_quot thm = Thm.eq_thm_prop (thm, @{thm identity_quotient3})