1.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Nov 17 06:04:59 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Nov 17 14:35:32 2011 +0100
     1.3 @@ -11,6 +11,13 @@
     1.4    val lookup_quotmaps_global: theory -> string -> quotmaps option
     1.5    val print_quotmaps: Proof.context -> unit
     1.6  
     1.7 +  type abs_rep = {abs : term, rep : term}
     1.8 +  val transform_abs_rep: morphism -> abs_rep -> abs_rep
     1.9 +  val lookup_abs_rep: Proof.context -> string -> abs_rep option
    1.10 +  val lookup_abs_rep_global: theory -> string -> abs_rep option
    1.11 +  val update_abs_rep: string -> abs_rep -> Context.generic -> Context.generic
    1.12 +  val print_abs_rep: Proof.context -> unit
    1.13 +  
    1.14    type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
    1.15    val transform_quotients: morphism -> quotients -> quotients
    1.16    val lookup_quotients: Proof.context -> string -> quotients option
    1.17 @@ -86,6 +93,39 @@
    1.18      |> Pretty.writeln
    1.19    end
    1.20  
    1.21 +(* info about abs/rep terms *)
    1.22 +type abs_rep = {abs : term, rep : term}
    1.23 +
    1.24 +structure Abs_Rep = Generic_Data
    1.25 +(
    1.26 +  type T = abs_rep Symtab.table
    1.27 +  val empty = Symtab.empty
    1.28 +  val extend = I
    1.29 +  fun merge data = Symtab.merge (K true) data
    1.30 +)
    1.31 +
    1.32 +fun transform_abs_rep phi {abs, rep} = {abs = Morphism.term phi abs, rep = Morphism.term phi rep}
    1.33 +
    1.34 +val lookup_abs_rep = Symtab.lookup o Abs_Rep.get o Context.Proof
    1.35 +val lookup_abs_rep_global = Symtab.lookup o Abs_Rep.get o Context.Theory
    1.36 +
    1.37 +fun update_abs_rep str data = Abs_Rep.map (Symtab.update (str, data))
    1.38 +
    1.39 +fun print_abs_rep ctxt =
    1.40 +  let
    1.41 +    fun prt_abs_rep (s, {abs, rep}) =
    1.42 +      Pretty.block (separate (Pretty.brk 2)
    1.43 +       [Pretty.str "type constructor:",
    1.44 +        Pretty.str s,
    1.45 +        Pretty.str "abs term:",
    1.46 +        Syntax.pretty_term ctxt abs,
    1.47 +        Pretty.str "rep term:",
    1.48 +        Syntax.pretty_term ctxt rep])
    1.49 +  in
    1.50 +    map prt_abs_rep (Symtab.dest (Abs_Rep.get (Context.Proof ctxt)))
    1.51 +    |> Pretty.big_list "abs/rep terms:"
    1.52 +    |> Pretty.writeln
    1.53 +  end
    1.54  
    1.55  (* info about quotient types *)
    1.56  type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}

     2.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Nov 17 06:04:59 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu Nov 17 14:35:32 2011 +0100
     2.3 @@ -123,14 +123,18 @@
     2.4  (* produces the rep or abs constant for a qty *)
     2.5  fun absrep_const flag ctxt qty_str =
     2.6    let
     2.7 -    val qty_name = Long_Name.base_name qty_str
     2.8 -    val qualifier = Long_Name.qualifier qty_str
     2.9 +    (* FIXME *)
    2.10 +    fun mk_dummyT (Const (c, _)) = Const (c, dummyT)
    2.11 +      | mk_dummyT _ = error "Expecting abs/rep term to be a constant"     
    2.12    in
    2.13 -    case flag of
    2.14 -      AbsF => Const (Long_Name.qualify qualifier ("abs_" ^ qty_name), dummyT)
    2.15 -    | RepF => Const (Long_Name.qualify qualifier ("rep_" ^ qty_name), dummyT)
    2.16 +    case Quotient_Info.lookup_abs_rep ctxt qty_str of
    2.17 +      SOME abs_rep => 
    2.18 +        mk_dummyT (case flag of
    2.19 +          AbsF => #abs abs_rep
    2.20 +        | RepF => #rep abs_rep)
    2.21 +      | NONE => error ("No abs/rep terms for " ^ quote qty_str)
    2.22    end
    2.23 -
    2.24 +  
    2.25  (* Lets Nitpick represent elements of quotient types as elements of the raw type *)
    2.26  fun absrep_const_chk flag ctxt qty_str =
    2.27    Syntax.check_term ctxt (absrep_const flag ctxt qty_str)

     3.1 --- a/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Nov 17 06:04:59 2011 +0100
     3.2 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Nov 17 14:35:32 2011 +0100
     3.3 @@ -116,9 +116,9 @@
     3.4      val abs_name = Binding.prefix_name "abs_" qty_name
     3.5      val rep_name = Binding.prefix_name "rep_" qty_name
     3.6  
     3.7 -    val ((_, (_, abs_def)), lthy2) = lthy1
     3.8 +    val ((abs_t, (_, abs_def)), lthy2) = lthy1
     3.9        |> Local_Theory.define ((abs_name, NoSyn), (Attrib.empty_binding, abs_trm))
    3.10 -    val ((_, (_, rep_def)), lthy3) = lthy2
    3.11 +    val ((rep_t, (_, rep_def)), lthy3) = lthy2
    3.12        |> Local_Theory.define ((rep_name, NoSyn), (Attrib.empty_binding, rep_trm))
    3.13  
    3.14      (* quot_type theorem *)
    3.15 @@ -137,10 +137,12 @@
    3.16      val quotients = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
    3.17  
    3.18      fun qinfo phi = Quotient_Info.transform_quotients phi quotients
    3.19 +    fun abs_rep phi = Quotient_Info.transform_abs_rep phi {abs = abs_t, rep = rep_t}
    3.20  
    3.21      val lthy4 = lthy3
    3.22        |> Local_Theory.declaration {syntax = false, pervasive = true}
    3.23 -        (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi))
    3.24 +        (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi)
    3.25 +           #> Quotient_Info.update_abs_rep qty_full_name (abs_rep phi))
    3.26        |> (snd oo Local_Theory.note)
    3.27          ((equiv_thm_name,
    3.28            if partial then [] else [Attrib.internal (K Quotient_Info.equiv_rules_add)]),