simplified/standardized signatures;
authorwenzelm
Thu Oct 27 20:26:38 2011 +0200 (2011-10-27)
changeset 4527989a17197cb98
parent 45278 7c6c8e950636
child 45280 9fd6fce8a230
simplified/standardized signatures;
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Quotient/quotient_def.ML
src/HOL/Tools/Quotient/quotient_info.ML
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/Quotient/quotient_term.ML
src/HOL/Tools/Quotient/quotient_typ.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Oct 27 19:41:08 2011 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Oct 27 20:26:38 2011 +0200
     1.3 @@ -642,7 +642,7 @@
     1.4        |> Option.map snd |> these |> null |> not
     1.5    | is_codatatype _ _ = false
     1.6  fun is_real_quot_type thy (Type (s, _)) =
     1.7 -    is_some (Quotient_Info.quotdata_lookup thy s)
     1.8 +    is_some (Quotient_Info.lookup_quotients thy s)
     1.9    | is_real_quot_type _ _ = false
    1.10  fun is_quot_type ctxt T =
    1.11    let val thy = Proof_Context.theory_of ctxt in
    1.12 @@ -738,14 +738,14 @@
    1.13       | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
    1.14    | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
    1.15  fun rep_type_for_quot_type thy (T as Type (s, _)) =
    1.16 -    let val {qtyp, rtyp, ...} = the (Quotient_Info.quotdata_lookup thy s) in
    1.17 +    let val {qtyp, rtyp, ...} = the (Quotient_Info.lookup_quotients thy s) in
    1.18        instantiate_type thy qtyp T rtyp
    1.19      end
    1.20    | rep_type_for_quot_type _ T =
    1.21      raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], [])
    1.22  fun equiv_relation_for_quot_type thy (Type (s, Ts)) =
    1.23      let
    1.24 -      val {qtyp, equiv_rel, equiv_thm, ...} = the (Quotient_Info.quotdata_lookup thy s)
    1.25 +      val {qtyp, equiv_rel, equiv_thm, ...} = the (Quotient_Info.lookup_quotients thy s)
    1.26        val partial =
    1.27          case prop_of equiv_thm of
    1.28            @{const Trueprop} $ (Const (@{const_name equivp}, _) $ _) => false
     2.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Thu Oct 27 19:41:08 2011 +0200
     2.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Thu Oct 27 20:26:38 2011 +0200
     2.3 @@ -7,13 +7,13 @@
     2.4  signature QUOTIENT_DEF =
     2.5  sig
     2.6    val quotient_def: (binding * typ option * mixfix) option * (Attrib.binding * (term * term)) ->
     2.7 -    local_theory -> Quotient_Info.qconsts_info * local_theory
     2.8 +    local_theory -> Quotient_Info.quotconsts * local_theory
     2.9  
    2.10    val quotdef_cmd: (binding * string option * mixfix) option * (Attrib.binding * (string * string)) ->
    2.11 -    local_theory -> Quotient_Info.qconsts_info * local_theory
    2.12 +    local_theory -> Quotient_Info.quotconsts * local_theory
    2.13  
    2.14    val lift_raw_const: typ list -> (string * term * mixfix) -> local_theory ->
    2.15 -    Quotient_Info.qconsts_info * local_theory
    2.16 +    Quotient_Info.quotconsts * local_theory
    2.17  end;
    2.18  
    2.19  structure Quotient_Def: QUOTIENT_DEF =
    2.20 @@ -29,7 +29,7 @@
    2.21      - the new constant as term
    2.22      - the rhs of the definition as term
    2.23  
    2.24 -   It stores the qconst_info in the qconsts data slot.
    2.25 +   It stores the qconst_info in the quotconsts data slot.
    2.26  
    2.27     Restriction: At the moment the left- and right-hand
    2.28     side of the definition must be a constant.
    2.29 @@ -72,11 +72,11 @@
    2.30      (* data storage *)
    2.31      val qconst_data = {qconst = trm, rconst = rhs, def = thm}
    2.32  
    2.33 -    fun qcinfo phi = Quotient_Info.transform_qconsts phi qconst_data
    2.34 +    fun qcinfo phi = Quotient_Info.transform_quotconsts phi qconst_data
    2.35      fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
    2.36      val lthy'' =
    2.37        Local_Theory.declaration true
    2.38 -        (fn phi => Quotient_Info.qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
    2.39 +        (fn phi => Quotient_Info.update_quotconsts (trans_name phi) (qcinfo phi)) lthy'
    2.40    in
    2.41      (qconst_data, lthy'')
    2.42    end
     3.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Oct 27 19:41:08 2011 +0200
     3.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Oct 27 20:26:38 2011 +0200
     3.3 @@ -1,44 +1,41 @@
     3.4  (*  Title:      HOL/Tools/Quotient/quotient_info.ML
     3.5      Author:     Cezary Kaliszyk and Christian Urban
     3.6  
     3.7 -Data slots for the quotient package.
     3.8 +Context data for the quotient package.
     3.9  *)
    3.10  
    3.11 -(* FIXME odd names/signatures of data access operations *)
    3.12 -
    3.13  signature QUOTIENT_INFO =
    3.14  sig
    3.15 -
    3.16 -  type maps_info = {mapfun: string, relmap: string}
    3.17 -  val maps_lookup: theory -> string -> maps_info option
    3.18 -  val maps_update_thy: string -> maps_info -> theory -> theory
    3.19 -  val maps_update: string -> maps_info -> Proof.context -> Proof.context
    3.20 -  val print_mapsinfo: Proof.context -> unit
    3.21 +  type quotmaps = {mapfun: string, relmap: string}
    3.22 +  val lookup_quotmaps: theory -> string -> quotmaps option
    3.23 +  val update_quotmaps_global: string -> quotmaps -> theory -> theory
    3.24 +  val update_quotmaps: string -> quotmaps -> Proof.context -> Proof.context
    3.25 +  val print_quotmaps: Proof.context -> unit
    3.26  
    3.27 -  type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
    3.28 -  val transform_quotdata: morphism -> quotdata_info -> quotdata_info
    3.29 -  val quotdata_lookup: theory -> string -> quotdata_info option
    3.30 -  val quotdata_update_thy: string -> quotdata_info -> theory -> theory
    3.31 -  val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic
    3.32 -  val quotdata_dest: Proof.context -> quotdata_info list
    3.33 -  val print_quotinfo: Proof.context -> unit
    3.34 +  type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
    3.35 +  val transform_quotients: morphism -> quotients -> quotients
    3.36 +  val lookup_quotients: theory -> string -> quotients option
    3.37 +  val update_quotients_global: string -> quotients -> theory -> theory
    3.38 +  val update_quotients: string -> quotients -> Context.generic -> Context.generic
    3.39 +  val dest_quotients: Proof.context -> quotients list
    3.40 +  val print_quotients: Proof.context -> unit
    3.41  
    3.42 -  type qconsts_info = {qconst: term, rconst: term, def: thm}
    3.43 -  val transform_qconsts: morphism -> qconsts_info -> qconsts_info
    3.44 -  val qconsts_lookup: theory -> term -> qconsts_info option
    3.45 -  val qconsts_update_thy: string -> qconsts_info -> theory -> theory
    3.46 -  val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic
    3.47 -  val qconsts_dest: Proof.context -> qconsts_info list
    3.48 -  val print_qconstinfo: Proof.context -> unit
    3.49 +  type quotconsts = {qconst: term, rconst: term, def: thm}
    3.50 +  val transform_quotconsts: morphism -> quotconsts -> quotconsts
    3.51 +  val lookup_quotconsts: theory -> term -> quotconsts option
    3.52 +  val update_quotconsts_global: string -> quotconsts -> theory -> theory
    3.53 +  val update_quotconsts: string -> quotconsts -> Context.generic -> Context.generic
    3.54 +  val dest_quotconsts: Proof.context -> quotconsts list
    3.55 +  val print_quotconsts: Proof.context -> unit
    3.56  
    3.57 -  val equiv_rules_get: Proof.context -> thm list
    3.58 +  val equiv_rules: Proof.context -> thm list
    3.59    val equiv_rules_add: attribute
    3.60 -  val rsp_rules_get: Proof.context -> thm list
    3.61 +  val rsp_rules: Proof.context -> thm list
    3.62    val rsp_rules_add: attribute
    3.63 -  val prs_rules_get: Proof.context -> thm list
    3.64 +  val prs_rules: Proof.context -> thm list
    3.65    val prs_rules_add: attribute
    3.66 -  val id_simps_get: Proof.context -> thm list
    3.67 -  val quotient_rules_get: Proof.context -> thm list
    3.68 +  val id_simps: Proof.context -> thm list
    3.69 +  val quotient_rules: Proof.context -> thm list
    3.70    val quotient_rules_add: attribute
    3.71    val setup: theory -> theory
    3.72  end;
    3.73 @@ -51,29 +48,29 @@
    3.74  (* FIXME just one data slot (record) per program unit *)
    3.75  
    3.76  (* info about map- and rel-functions for a type *)
    3.77 -type maps_info = {mapfun: string, relmap: string}
    3.78 +type quotmaps = {mapfun: string, relmap: string}
    3.79  
    3.80 -structure MapsData = Theory_Data
    3.81 +structure Quotmaps = Theory_Data
    3.82  (
    3.83 -  type T = maps_info Symtab.table
    3.84 +  type T = quotmaps Symtab.table
    3.85    val empty = Symtab.empty
    3.86    val extend = I
    3.87    fun merge data = Symtab.merge (K true) data
    3.88  )
    3.89  
    3.90 -fun maps_lookup thy s = Symtab.lookup (MapsData.get thy) s
    3.91 +val lookup_quotmaps = Symtab.lookup o Quotmaps.get
    3.92  
    3.93 -fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
    3.94 -fun maps_update k minfo = Proof_Context.background_theory (maps_update_thy k minfo)  (* FIXME *)
    3.95 +fun update_quotmaps_global k minfo = Quotmaps.map (Symtab.update (k, minfo))
    3.96 +fun update_quotmaps k minfo = Proof_Context.background_theory (update_quotmaps_global k minfo)  (* FIXME !? *)
    3.97  
    3.98  fun maps_attribute_aux s minfo = Thm.declaration_attribute
    3.99 -  (fn _ => Context.mapping (maps_update_thy s minfo) (maps_update s minfo))
   3.100 +  (fn _ => Context.mapping (update_quotmaps_global s minfo) (update_quotmaps s minfo))
   3.101  
   3.102  (* attribute to be used in declare statements *)
   3.103  fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) =
   3.104    let
   3.105      val thy = Proof_Context.theory_of ctxt
   3.106 -    val tyname = Sign.intern_type thy tystr
   3.107 +    val tyname = Sign.intern_type thy tystr  (* FIXME pass proper internal names *)
   3.108      val mapname = Sign.intern_const thy mapstr
   3.109      val relname = Sign.intern_const thy relstr
   3.110  
   3.111 @@ -89,7 +86,7 @@
   3.112        (Parse.$$$ "(" |-- Args.name --| Parse.$$$ "," --
   3.113          Args.name --| Parse.$$$ ")"))
   3.114  
   3.115 -fun print_mapsinfo ctxt =
   3.116 +fun print_quotmaps ctxt =
   3.117    let
   3.118      fun prt_map (ty_name, {mapfun, relmap}) =
   3.119        Pretty.block (separate (Pretty.brk 2)
   3.120 @@ -98,7 +95,7 @@
   3.121            "map:", mapfun,
   3.122            "relation map:", relmap]))
   3.123    in
   3.124 -    MapsData.get (Proof_Context.theory_of ctxt)
   3.125 +    Quotmaps.get (Proof_Context.theory_of ctxt)
   3.126      |> Symtab.dest
   3.127      |> map (prt_map)
   3.128      |> Pretty.big_list "maps for type constructors:"
   3.129 @@ -107,31 +104,31 @@
   3.130  
   3.131  
   3.132  (* info about quotient types *)
   3.133 -type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
   3.134 +type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
   3.135  
   3.136 -structure QuotData = Theory_Data
   3.137 +structure Quotients = Theory_Data
   3.138  (
   3.139 -  type T = quotdata_info Symtab.table
   3.140 +  type T = quotients Symtab.table
   3.141    val empty = Symtab.empty
   3.142    val extend = I
   3.143    fun merge data = Symtab.merge (K true) data
   3.144  )
   3.145  
   3.146 -fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} =
   3.147 +fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm} =
   3.148    {qtyp = Morphism.typ phi qtyp,
   3.149     rtyp = Morphism.typ phi rtyp,
   3.150     equiv_rel = Morphism.term phi equiv_rel,
   3.151     equiv_thm = Morphism.thm phi equiv_thm}
   3.152  
   3.153 -fun quotdata_lookup thy str = Symtab.lookup (QuotData.get thy) str
   3.154 +val lookup_quotients = Symtab.lookup o Quotients.get
   3.155  
   3.156 -fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo))
   3.157 -fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I
   3.158 +fun update_quotients_global str qinfo = Quotients.map (Symtab.update (str, qinfo))
   3.159 +fun update_quotients str qinfo = Context.mapping (update_quotients_global str qinfo) I  (* FIXME !? *)
   3.160  
   3.161 -fun quotdata_dest lthy =
   3.162 -  map snd (Symtab.dest (QuotData.get (Proof_Context.theory_of lthy)))
   3.163 +fun dest_quotients lthy =  (* FIXME slightly expensive way to retrieve data *)
   3.164 +  map snd (Symtab.dest (Quotients.get (Proof_Context.theory_of lthy)))  (* FIXME !? *)
   3.165  
   3.166 -fun print_quotinfo ctxt =
   3.167 +fun print_quotients ctxt =
   3.168    let
   3.169      fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} =
   3.170        Pretty.block (separate (Pretty.brk 2)
   3.171 @@ -144,7 +141,7 @@
   3.172          Pretty.str "equiv. thm:",
   3.173          Syntax.pretty_term ctxt (prop_of equiv_thm)])
   3.174    in
   3.175 -    QuotData.get (Proof_Context.theory_of ctxt)
   3.176 +    Quotients.get (Proof_Context.theory_of ctxt)
   3.177      |> Symtab.dest
   3.178      |> map (prt_quot o snd)
   3.179      |> Pretty.big_list "quotients:"
   3.180 @@ -153,48 +150,48 @@
   3.181  
   3.182  
   3.183  (* info about quotient constants *)
   3.184 -type qconsts_info = {qconst: term, rconst: term, def: thm}
   3.185 +type quotconsts = {qconst: term, rconst: term, def: thm}
   3.186  
   3.187 -fun qconsts_info_eq (x : qconsts_info, y : qconsts_info) = #qconst x = #qconst y
   3.188 +fun eq_quotconsts (x : quotconsts, y : quotconsts) = #qconst x = #qconst y
   3.189  
   3.190  (* We need to be able to lookup instances of lifted constants,
   3.191     for example given "nat fset" we need to find "'a fset";
   3.192     but overloaded constants share the same name *)
   3.193 -structure QConstsData = Theory_Data
   3.194 +structure Quotconsts = Theory_Data
   3.195  (
   3.196 -  type T = qconsts_info list Symtab.table
   3.197 +  type T = quotconsts list Symtab.table
   3.198    val empty = Symtab.empty
   3.199    val extend = I
   3.200 -  val merge = Symtab.merge_list qconsts_info_eq
   3.201 +  val merge = Symtab.merge_list eq_quotconsts
   3.202  )
   3.203  
   3.204 -fun transform_qconsts phi {qconst, rconst, def} =
   3.205 +fun transform_quotconsts phi {qconst, rconst, def} =
   3.206    {qconst = Morphism.term phi qconst,
   3.207     rconst = Morphism.term phi rconst,
   3.208     def = Morphism.thm phi def}
   3.209  
   3.210 -fun qconsts_update_thy name qcinfo = QConstsData.map (Symtab.cons_list (name, qcinfo))
   3.211 -fun qconsts_update_gen name qcinfo = Context.mapping (qconsts_update_thy name qcinfo) I
   3.212 +fun update_quotconsts_global name qcinfo = Quotconsts.map (Symtab.cons_list (name, qcinfo))
   3.213 +fun update_quotconsts name qcinfo = Context.mapping (update_quotconsts_global name qcinfo) I  (* FIXME !? *)
   3.214  
   3.215 -fun qconsts_dest lthy =
   3.216 -  flat (map snd (Symtab.dest (QConstsData.get (Proof_Context.theory_of lthy))))
   3.217 +fun dest_quotconsts lthy =
   3.218 +  flat (map snd (Symtab.dest (Quotconsts.get (Proof_Context.theory_of lthy))))  (* FIXME !? *)
   3.219  
   3.220 -fun qconsts_lookup thy t =
   3.221 +fun lookup_quotconsts thy t =
   3.222    let
   3.223      val (name, qty) = dest_Const t
   3.224 -    fun matches (x: qconsts_info) =
   3.225 +    fun matches (x: quotconsts) =
   3.226        let
   3.227          val (name', qty') = dest_Const (#qconst x);
   3.228        in
   3.229          name = name' andalso Sign.typ_instance thy (qty, qty')
   3.230        end
   3.231    in
   3.232 -    (case Symtab.lookup (QConstsData.get thy) name of
   3.233 +    (case Symtab.lookup (Quotconsts.get thy) name of
   3.234        NONE => NONE
   3.235      | SOME l => find_first matches l)
   3.236    end
   3.237  
   3.238 -fun print_qconstinfo ctxt =
   3.239 +fun print_quotconsts ctxt =
   3.240    let
   3.241      fun prt_qconst {qconst, rconst, def} =
   3.242        Pretty.block (separate (Pretty.brk 1)
   3.243 @@ -204,7 +201,7 @@
   3.244          Pretty.str "as",
   3.245          Syntax.pretty_term ctxt (prop_of def)])
   3.246    in
   3.247 -    QConstsData.get (Proof_Context.theory_of ctxt)
   3.248 +    Quotconsts.get (Proof_Context.theory_of ctxt)
   3.249      |> Symtab.dest
   3.250      |> map snd
   3.251      |> flat
   3.252 @@ -214,80 +211,80 @@
   3.253    end
   3.254  
   3.255  (* equivalence relation theorems *)
   3.256 -structure EquivRules = Named_Thms
   3.257 +structure Equiv_Rules = Named_Thms
   3.258  (
   3.259    val name = "quot_equiv"
   3.260    val description = "equivalence relation theorems"
   3.261  )
   3.262  
   3.263 -val equiv_rules_get = EquivRules.get
   3.264 -val equiv_rules_add = EquivRules.add
   3.265 +val equiv_rules = Equiv_Rules.get
   3.266 +val equiv_rules_add = Equiv_Rules.add
   3.267  
   3.268  (* respectfulness theorems *)
   3.269 -structure RspRules = Named_Thms
   3.270 +structure Rsp_Rules = Named_Thms
   3.271  (
   3.272    val name = "quot_respect"
   3.273    val description = "respectfulness theorems"
   3.274  )
   3.275  
   3.276 -val rsp_rules_get = RspRules.get
   3.277 -val rsp_rules_add = RspRules.add
   3.278 +val rsp_rules = Rsp_Rules.get
   3.279 +val rsp_rules_add = Rsp_Rules.add
   3.280  
   3.281  (* preservation theorems *)
   3.282 -structure PrsRules = Named_Thms
   3.283 +structure Prs_Rules = Named_Thms
   3.284  (
   3.285    val name = "quot_preserve"
   3.286    val description = "preservation theorems"
   3.287  )
   3.288  
   3.289 -val prs_rules_get = PrsRules.get
   3.290 -val prs_rules_add = PrsRules.add
   3.291 +val prs_rules = Prs_Rules.get
   3.292 +val prs_rules_add = Prs_Rules.add
   3.293  
   3.294  (* id simplification theorems *)
   3.295 -structure IdSimps = Named_Thms
   3.296 +structure Id_Simps = Named_Thms
   3.297  (
   3.298    val name = "id_simps"
   3.299    val description = "identity simp rules for maps"
   3.300  )
   3.301  
   3.302 -val id_simps_get = IdSimps.get
   3.303 +val id_simps = Id_Simps.get
   3.304  
   3.305  (* quotient theorems *)
   3.306 -structure QuotientRules = Named_Thms
   3.307 +structure Quotient_Rules = Named_Thms
   3.308  (
   3.309    val name = "quot_thm"
   3.310    val description = "quotient theorems"
   3.311  )
   3.312  
   3.313 -val quotient_rules_get = QuotientRules.get
   3.314 -val quotient_rules_add = QuotientRules.add
   3.315 +val quotient_rules = Quotient_Rules.get
   3.316 +val quotient_rules_add = Quotient_Rules.add
   3.317  
   3.318  
   3.319  (* theory setup *)
   3.320  
   3.321  val setup =
   3.322 -  Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute)
   3.323 +  Attrib.setup @{binding map} (maps_attr_parser >> maps_attribute)
   3.324      "declaration of map information" #>
   3.325 -  EquivRules.setup #>
   3.326 -  RspRules.setup #>
   3.327 -  PrsRules.setup #>
   3.328 -  IdSimps.setup #>
   3.329 -  QuotientRules.setup
   3.330 +  Equiv_Rules.setup #>
   3.331 +  Rsp_Rules.setup #>
   3.332 +  Prs_Rules.setup #>
   3.333 +  Id_Simps.setup #>
   3.334 +  Quotient_Rules.setup
   3.335  
   3.336  
   3.337  (* outer syntax commands *)
   3.338  
   3.339  val _ =
   3.340    Outer_Syntax.improper_command "print_quotmaps" "print quotient map functions" Keyword.diag
   3.341 -    (Scan.succeed (Toplevel.keep (print_mapsinfo o Toplevel.context_of)))
   3.342 +    (Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of)))
   3.343  
   3.344  val _ =
   3.345    Outer_Syntax.improper_command "print_quotients" "print quotients" Keyword.diag
   3.346 -    (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of)))
   3.347 +    (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
   3.348  
   3.349  val _ =
   3.350    Outer_Syntax.improper_command "print_quotconsts" "print quotient constants" Keyword.diag
   3.351 -    (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of)))
   3.352 +    (Scan.succeed (Toplevel.keep (print_quotconsts o Toplevel.context_of)))
   3.353  
   3.354  
   3.355 -end; (* structure *)
   3.356 +end;
     4.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Oct 27 19:41:08 2011 +0200
     4.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Oct 27 20:26:38 2011 +0200
     4.3 @@ -52,7 +52,7 @@
     4.4  (** solvers for equivp and quotient assumptions **)
     4.5  
     4.6  fun equiv_tac ctxt =
     4.7 -  REPEAT_ALL_NEW (resolve_tac (Quotient_Info.equiv_rules_get ctxt))
     4.8 +  REPEAT_ALL_NEW (resolve_tac (Quotient_Info.equiv_rules ctxt))
     4.9  
    4.10  fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
    4.11  val equiv_solver = mk_solver "Equivalence goal solver" equiv_solver_tac
    4.12 @@ -60,7 +60,7 @@
    4.13  fun quotient_tac ctxt =
    4.14    (REPEAT_ALL_NEW (FIRST'
    4.15      [rtac @{thm identity_quotient},
    4.16 -     resolve_tac (Quotient_Info.quotient_rules_get ctxt)]))
    4.17 +     resolve_tac (Quotient_Info.quotient_rules ctxt)]))
    4.18  
    4.19  fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
    4.20  val quotient_solver = mk_solver "Quotient goal solver" quotient_solver_tac
    4.21 @@ -147,11 +147,11 @@
    4.22  
    4.23  fun reflp_get ctxt =
    4.24    map_filter (fn th => if prems_of th = [] then SOME (OF1 @{thm equivp_reflp} th) else NONE
    4.25 -    handle THM _ => NONE) (Quotient_Info.equiv_rules_get ctxt)
    4.26 +    handle THM _ => NONE) (Quotient_Info.equiv_rules ctxt)
    4.27  
    4.28  val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)}
    4.29  
    4.30 -fun eq_imp_rel_get ctxt = map (OF1 eq_imp_rel) (Quotient_Info.equiv_rules_get ctxt)
    4.31 +fun eq_imp_rel_get ctxt = map (OF1 eq_imp_rel) (Quotient_Info.equiv_rules ctxt)
    4.32  
    4.33  fun regularize_tac ctxt =
    4.34    let
    4.35 @@ -373,7 +373,7 @@
    4.36  
    4.37       (* respectfulness of constants; in particular of a simple relation *)
    4.38    | _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)
    4.39 -      => resolve_tac (Quotient_Info.rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
    4.40 +      => resolve_tac (Quotient_Info.rsp_rules ctxt) THEN_ALL_NEW quotient_tac ctxt
    4.41  
    4.42        (* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
    4.43        (* observe map_fun *)
    4.44 @@ -521,9 +521,9 @@
    4.45  *)
    4.46  fun clean_tac lthy =
    4.47    let
    4.48 -    val defs = map (Thm.symmetric o #def) (Quotient_Info.qconsts_dest lthy)
    4.49 -    val prs = Quotient_Info.prs_rules_get lthy
    4.50 -    val ids = Quotient_Info.id_simps_get lthy
    4.51 +    val defs = map (Thm.symmetric o #def) (Quotient_Info.dest_quotconsts lthy)
    4.52 +    val prs = Quotient_Info.prs_rules lthy
    4.53 +    val ids = Quotient_Info.id_simps lthy
    4.54      val thms =
    4.55        @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
    4.56  
    4.57 @@ -632,7 +632,7 @@
    4.58      THEN' gen_frees_tac ctxt
    4.59      THEN' SUBGOAL (fn (goal, i) =>
    4.60        let
    4.61 -        val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
    4.62 +        val qtys = map #qtyp (Quotient_Info.dest_quotients ctxt)
    4.63          val rtrm = Quotient_Term.derive_rtrm ctxt qtys goal
    4.64          val rule = procedure_inst ctxt rtrm  goal
    4.65        in
    4.66 @@ -711,7 +711,7 @@
    4.67  val lifted_attrib = Thm.rule_attribute (fn context =>
    4.68    let
    4.69      val ctxt = Context.proof_of context
    4.70 -    val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
    4.71 +    val qtys = map #qtyp (Quotient_Info.dest_quotients ctxt)
    4.72    in
    4.73      lifted ctxt qtys []
    4.74    end)
     5.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Oct 27 19:41:08 2011 +0200
     5.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu Oct 27 20:26:38 2011 +0200
     5.3 @@ -63,9 +63,9 @@
     5.4    | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1
     5.5  
     5.6  fun get_mapfun ctxt s =
     5.7 -  case Quotient_Info.maps_lookup (Proof_Context.theory_of ctxt) s of
     5.8 +  (case Quotient_Info.lookup_quotmaps (Proof_Context.theory_of ctxt) s of
     5.9      SOME map_data => Const (#mapfun map_data, dummyT)
    5.10 -  | NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
    5.11 +  | NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found."))
    5.12  
    5.13  (* makes a Free out of a TVar *)
    5.14  fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
    5.15 @@ -96,7 +96,7 @@
    5.16     a quotient definition
    5.17  *)
    5.18  fun get_rty_qty ctxt s =
    5.19 -  case Quotient_Info.quotdata_lookup (Proof_Context.theory_of ctxt) s of
    5.20 +  case Quotient_Info.lookup_quotients (Proof_Context.theory_of ctxt) s of
    5.21      SOME qdata => (#rtyp qdata, #qtyp qdata)
    5.22    | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.");
    5.23  
    5.24 @@ -271,9 +271,9 @@
    5.25    Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
    5.26  
    5.27  fun get_relmap ctxt s =
    5.28 -  case Quotient_Info.maps_lookup (Proof_Context.theory_of ctxt) s of
    5.29 +  (case Quotient_Info.lookup_quotmaps (Proof_Context.theory_of ctxt) s of
    5.30      SOME map_data => Const (#relmap map_data, dummyT)
    5.31 -  | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
    5.32 +  | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")"))
    5.33  
    5.34  fun mk_relmap ctxt vs rty =
    5.35    let
    5.36 @@ -290,9 +290,9 @@
    5.37    end
    5.38  
    5.39  fun get_equiv_rel ctxt s =
    5.40 -  case Quotient_Info.quotdata_lookup (Proof_Context.theory_of ctxt) s of
    5.41 -      SOME qdata => #equiv_rel qdata
    5.42 -    | NONE => raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
    5.43 +  (case Quotient_Info.lookup_quotients (Proof_Context.theory_of ctxt) s of
    5.44 +    SOME qdata => #equiv_rel qdata
    5.45 +  | NONE => raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")"))
    5.46  
    5.47  fun equiv_match_err ctxt ty_pat ty =
    5.48    let
    5.49 @@ -427,7 +427,7 @@
    5.50            if length rtys <> length qtys then false
    5.51            else forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
    5.52          else
    5.53 -          (case Quotient_Info.quotdata_lookup thy qs of
    5.54 +          (case Quotient_Info.lookup_quotients thy qs of
    5.55              SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
    5.56            | NONE => false)
    5.57      | _ => false)
    5.58 @@ -553,9 +553,10 @@
    5.59          if same_const rtrm qtrm then rtrm
    5.60          else
    5.61            let
    5.62 -            val rtrm' = case Quotient_Info.qconsts_lookup thy qtrm of
    5.63 -              SOME qconst_info => #rconst qconst_info
    5.64 -            | NONE => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm
    5.65 +            val rtrm' =
    5.66 +              (case Quotient_Info.lookup_quotconsts thy qtrm of
    5.67 +                SOME qconst_info => #rconst qconst_info
    5.68 +              | NONE => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm)
    5.69            in
    5.70              if Pattern.matches thy (rtrm', rtrm)
    5.71              then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm
    5.72 @@ -743,7 +744,7 @@
    5.73    let
    5.74      val thy = Proof_Context.theory_of ctxt
    5.75    in
    5.76 -    Quotient_Info.quotdata_dest ctxt
    5.77 +    Quotient_Info.dest_quotients ctxt
    5.78      |> map (fn x => (#rtyp x, #qtyp x))
    5.79      |> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty)
    5.80      |> map (if direction then swap else I)
    5.81 @@ -755,12 +756,12 @@
    5.82      fun proper (t1, t2) = subst_typ' (fastype_of t1) = fastype_of t2
    5.83  
    5.84      val const_substs =
    5.85 -      Quotient_Info.qconsts_dest ctxt
    5.86 +      Quotient_Info.dest_quotconsts ctxt
    5.87        |> map (fn x => (#rconst x, #qconst x))
    5.88        |> map (if direction then swap else I)
    5.89  
    5.90      val rel_substs =
    5.91 -      Quotient_Info.quotdata_dest ctxt
    5.92 +      Quotient_Info.dest_quotients ctxt
    5.93        |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x)))
    5.94        |> map (if direction then swap else I)
    5.95    in
    5.96 @@ -787,4 +788,4 @@
    5.97    subst_trm ctxt (mk_ty_subst qtys true ctxt) (mk_trm_subst qtys true ctxt) qtrm
    5.98  
    5.99  
   5.100 -end; (* structure *)
   5.101 +end;
     6.1 --- a/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Oct 27 19:41:08 2011 +0200
     6.2 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Oct 27 20:26:38 2011 +0200
     6.3 @@ -2,13 +2,12 @@
     6.4      Author:     Cezary Kaliszyk and Christian Urban
     6.5  
     6.6  Definition of a quotient type.
     6.7 -
     6.8  *)
     6.9  
    6.10  signature QUOTIENT_TYPE =
    6.11  sig
    6.12    val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) * thm
    6.13 -    -> Proof.context -> Quotient_Info.quotdata_info * local_theory
    6.14 +    -> Proof.context -> Quotient_Info.quotients * local_theory
    6.15  
    6.16    val quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) list
    6.17      -> Proof.context -> Proof.state
    6.18 @@ -161,20 +160,20 @@
    6.19      (* name equivalence theorem *)
    6.20      val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
    6.21  
    6.22 -    (* storing the quotdata *)
    6.23 -    val quotdata = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
    6.24 +    (* storing the quotients *)
    6.25 +    val quotients = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
    6.26  
    6.27 -    fun qinfo phi = Quotient_Info.transform_quotdata phi quotdata
    6.28 +    fun qinfo phi = Quotient_Info.transform_quotients phi quotients
    6.29  
    6.30      val lthy4 = lthy3
    6.31        |> Local_Theory.declaration true
    6.32 -        (fn phi => Quotient_Info.quotdata_update_gen qty_full_name (qinfo phi))
    6.33 +        (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi))
    6.34        |> note
    6.35          (equiv_thm_name, equiv_thm,
    6.36            if partial then [] else [intern_attr Quotient_Info.equiv_rules_add])
    6.37        |> note (quotient_thm_name, quotient_thm, [intern_attr Quotient_Info.quotient_rules_add])
    6.38    in
    6.39 -    (quotdata, lthy4)
    6.40 +    (quotients, lthy4)
    6.41    end
    6.42  
    6.43  
    6.44 @@ -225,7 +224,7 @@
    6.45      fun map_check_aux rty warns =
    6.46        case rty of
    6.47          Type (_, []) => warns
    6.48 -      | Type (s, _) => if is_some (Quotient_Info.maps_lookup thy s) then warns else s :: warns
    6.49 +      | Type (s, _) => if is_some (Quotient_Info.lookup_quotmaps thy s) then warns else s :: warns
    6.50        | _ => warns
    6.51  
    6.52      val warns = map_check_aux rty []