--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Oct 27 19:41:08 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Oct 27 20:26:38 2011 +0200
@@ -642,7 +642,7 @@
|> Option.map snd |> these |> null |> not
| is_codatatype _ _ = false
fun is_real_quot_type thy (Type (s, _)) =
- is_some (Quotient_Info.quotdata_lookup thy s)
+ is_some (Quotient_Info.lookup_quotients thy s)
| is_real_quot_type _ _ = false
fun is_quot_type ctxt T =
let val thy = Proof_Context.theory_of ctxt in
@@ -738,14 +738,14 @@
| NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
| mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
fun rep_type_for_quot_type thy (T as Type (s, _)) =
- let val {qtyp, rtyp, ...} = the (Quotient_Info.quotdata_lookup thy s) in
+ let val {qtyp, rtyp, ...} = the (Quotient_Info.lookup_quotients thy s) in
instantiate_type thy qtyp T rtyp
end
| rep_type_for_quot_type _ T =
raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], [])
fun equiv_relation_for_quot_type thy (Type (s, Ts)) =
let
- val {qtyp, equiv_rel, equiv_thm, ...} = the (Quotient_Info.quotdata_lookup thy s)
+ val {qtyp, equiv_rel, equiv_thm, ...} = the (Quotient_Info.lookup_quotients thy s)
val partial =
case prop_of equiv_thm of
@{const Trueprop} $ (Const (@{const_name equivp}, _) $ _) => false
--- a/src/HOL/Tools/Quotient/quotient_def.ML Thu Oct 27 19:41:08 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Thu Oct 27 20:26:38 2011 +0200
@@ -7,13 +7,13 @@
signature QUOTIENT_DEF =
sig
val quotient_def: (binding * typ option * mixfix) option * (Attrib.binding * (term * term)) ->
- local_theory -> Quotient_Info.qconsts_info * local_theory
+ local_theory -> Quotient_Info.quotconsts * local_theory
val quotdef_cmd: (binding * string option * mixfix) option * (Attrib.binding * (string * string)) ->
- local_theory -> Quotient_Info.qconsts_info * local_theory
+ local_theory -> Quotient_Info.quotconsts * local_theory
val lift_raw_const: typ list -> (string * term * mixfix) -> local_theory ->
- Quotient_Info.qconsts_info * local_theory
+ Quotient_Info.quotconsts * local_theory
end;
structure Quotient_Def: QUOTIENT_DEF =
@@ -29,7 +29,7 @@
- the new constant as term
- the rhs of the definition as term
- It stores the qconst_info in the qconsts data slot.
+ It stores the qconst_info in the quotconsts data slot.
Restriction: At the moment the left- and right-hand
side of the definition must be a constant.
@@ -72,11 +72,11 @@
(* data storage *)
val qconst_data = {qconst = trm, rconst = rhs, def = thm}
- fun qcinfo phi = Quotient_Info.transform_qconsts phi qconst_data
+ fun qcinfo phi = Quotient_Info.transform_quotconsts phi qconst_data
fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
val lthy'' =
Local_Theory.declaration true
- (fn phi => Quotient_Info.qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
+ (fn phi => Quotient_Info.update_quotconsts (trans_name phi) (qcinfo phi)) lthy'
in
(qconst_data, lthy'')
end
--- a/src/HOL/Tools/Quotient/quotient_info.ML Thu Oct 27 19:41:08 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Thu Oct 27 20:26:38 2011 +0200
@@ -1,44 +1,41 @@
(* Title: HOL/Tools/Quotient/quotient_info.ML
Author: Cezary Kaliszyk and Christian Urban
-Data slots for the quotient package.
+Context data for the quotient package.
*)
-(* FIXME odd names/signatures of data access operations *)
-
signature QUOTIENT_INFO =
sig
-
- type maps_info = {mapfun: string, relmap: string}
- val maps_lookup: theory -> string -> maps_info option
- val maps_update_thy: string -> maps_info -> theory -> theory
- val maps_update: string -> maps_info -> Proof.context -> Proof.context
- val print_mapsinfo: Proof.context -> unit
+ type quotmaps = {mapfun: string, relmap: string}
+ val lookup_quotmaps: theory -> string -> quotmaps option
+ val update_quotmaps_global: string -> quotmaps -> theory -> theory
+ val update_quotmaps: string -> quotmaps -> Proof.context -> Proof.context
+ val print_quotmaps: Proof.context -> unit
- type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
- val transform_quotdata: morphism -> quotdata_info -> quotdata_info
- val quotdata_lookup: theory -> string -> quotdata_info option
- val quotdata_update_thy: string -> quotdata_info -> theory -> theory
- val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic
- val quotdata_dest: Proof.context -> quotdata_info list
- val print_quotinfo: Proof.context -> unit
+ type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
+ val transform_quotients: morphism -> quotients -> quotients
+ val lookup_quotients: theory -> string -> quotients option
+ val update_quotients_global: string -> quotients -> theory -> theory
+ val update_quotients: string -> quotients -> Context.generic -> Context.generic
+ val dest_quotients: Proof.context -> quotients list
+ val print_quotients: Proof.context -> unit
- type qconsts_info = {qconst: term, rconst: term, def: thm}
- val transform_qconsts: morphism -> qconsts_info -> qconsts_info
- val qconsts_lookup: theory -> term -> qconsts_info option
- val qconsts_update_thy: string -> qconsts_info -> theory -> theory
- val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic
- val qconsts_dest: Proof.context -> qconsts_info list
- val print_qconstinfo: Proof.context -> unit
+ type quotconsts = {qconst: term, rconst: term, def: thm}
+ val transform_quotconsts: morphism -> quotconsts -> quotconsts
+ val lookup_quotconsts: theory -> term -> quotconsts option
+ val update_quotconsts_global: string -> quotconsts -> theory -> theory
+ val update_quotconsts: string -> quotconsts -> Context.generic -> Context.generic
+ val dest_quotconsts: Proof.context -> quotconsts list
+ val print_quotconsts: Proof.context -> unit
- val equiv_rules_get: Proof.context -> thm list
+ val equiv_rules: Proof.context -> thm list
val equiv_rules_add: attribute
- val rsp_rules_get: Proof.context -> thm list
+ val rsp_rules: Proof.context -> thm list
val rsp_rules_add: attribute
- val prs_rules_get: Proof.context -> thm list
+ val prs_rules: Proof.context -> thm list
val prs_rules_add: attribute
- val id_simps_get: Proof.context -> thm list
- val quotient_rules_get: Proof.context -> thm list
+ val id_simps: Proof.context -> thm list
+ val quotient_rules: Proof.context -> thm list
val quotient_rules_add: attribute
val setup: theory -> theory
end;
@@ -51,29 +48,29 @@
(* FIXME just one data slot (record) per program unit *)
(* info about map- and rel-functions for a type *)
-type maps_info = {mapfun: string, relmap: string}
+type quotmaps = {mapfun: string, relmap: string}
-structure MapsData = Theory_Data
+structure Quotmaps = Theory_Data
(
- type T = maps_info Symtab.table
+ type T = quotmaps Symtab.table
val empty = Symtab.empty
val extend = I
fun merge data = Symtab.merge (K true) data
)
-fun maps_lookup thy s = Symtab.lookup (MapsData.get thy) s
+val lookup_quotmaps = Symtab.lookup o Quotmaps.get
-fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
-fun maps_update k minfo = Proof_Context.background_theory (maps_update_thy k minfo) (* FIXME *)
+fun update_quotmaps_global k minfo = Quotmaps.map (Symtab.update (k, minfo))
+fun update_quotmaps k minfo = Proof_Context.background_theory (update_quotmaps_global k minfo) (* FIXME !? *)
fun maps_attribute_aux s minfo = Thm.declaration_attribute
- (fn _ => Context.mapping (maps_update_thy s minfo) (maps_update s minfo))
+ (fn _ => Context.mapping (update_quotmaps_global s minfo) (update_quotmaps s minfo))
(* attribute to be used in declare statements *)
fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) =
let
val thy = Proof_Context.theory_of ctxt
- val tyname = Sign.intern_type thy tystr
+ val tyname = Sign.intern_type thy tystr (* FIXME pass proper internal names *)
val mapname = Sign.intern_const thy mapstr
val relname = Sign.intern_const thy relstr
@@ -89,7 +86,7 @@
(Parse.$$$ "(" |-- Args.name --| Parse.$$$ "," --
Args.name --| Parse.$$$ ")"))
-fun print_mapsinfo ctxt =
+fun print_quotmaps ctxt =
let
fun prt_map (ty_name, {mapfun, relmap}) =
Pretty.block (separate (Pretty.brk 2)
@@ -98,7 +95,7 @@
"map:", mapfun,
"relation map:", relmap]))
in
- MapsData.get (Proof_Context.theory_of ctxt)
+ Quotmaps.get (Proof_Context.theory_of ctxt)
|> Symtab.dest
|> map (prt_map)
|> Pretty.big_list "maps for type constructors:"
@@ -107,31 +104,31 @@
(* info about quotient types *)
-type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
+type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
-structure QuotData = Theory_Data
+structure Quotients = Theory_Data
(
- type T = quotdata_info Symtab.table
+ type T = quotients Symtab.table
val empty = Symtab.empty
val extend = I
fun merge data = Symtab.merge (K true) data
)
-fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} =
+fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_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}
-fun quotdata_lookup thy str = Symtab.lookup (QuotData.get thy) str
+val lookup_quotients = Symtab.lookup o Quotients.get
-fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo))
-fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I
+fun update_quotients_global str qinfo = Quotients.map (Symtab.update (str, qinfo))
+fun update_quotients str qinfo = Context.mapping (update_quotients_global str qinfo) I (* FIXME !? *)
-fun quotdata_dest lthy =
- map snd (Symtab.dest (QuotData.get (Proof_Context.theory_of lthy)))
+fun dest_quotients lthy = (* FIXME slightly expensive way to retrieve data *)
+ map snd (Symtab.dest (Quotients.get (Proof_Context.theory_of lthy))) (* FIXME !? *)
-fun print_quotinfo ctxt =
+fun print_quotients ctxt =
let
fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} =
Pretty.block (separate (Pretty.brk 2)
@@ -144,7 +141,7 @@
Pretty.str "equiv. thm:",
Syntax.pretty_term ctxt (prop_of equiv_thm)])
in
- QuotData.get (Proof_Context.theory_of ctxt)
+ Quotients.get (Proof_Context.theory_of ctxt)
|> Symtab.dest
|> map (prt_quot o snd)
|> Pretty.big_list "quotients:"
@@ -153,48 +150,48 @@
(* info about quotient constants *)
-type qconsts_info = {qconst: term, rconst: term, def: thm}
+type quotconsts = {qconst: term, rconst: term, def: thm}
-fun qconsts_info_eq (x : qconsts_info, y : qconsts_info) = #qconst x = #qconst y
+fun eq_quotconsts (x : quotconsts, y : quotconsts) = #qconst x = #qconst y
(* We need to be able to lookup instances of lifted constants,
for example given "nat fset" we need to find "'a fset";
but overloaded constants share the same name *)
-structure QConstsData = Theory_Data
+structure Quotconsts = Theory_Data
(
- type T = qconsts_info list Symtab.table
+ type T = quotconsts list Symtab.table
val empty = Symtab.empty
val extend = I
- val merge = Symtab.merge_list qconsts_info_eq
+ val merge = Symtab.merge_list eq_quotconsts
)
-fun transform_qconsts phi {qconst, rconst, def} =
+fun transform_quotconsts phi {qconst, rconst, def} =
{qconst = Morphism.term phi qconst,
rconst = Morphism.term phi rconst,
def = Morphism.thm phi def}
-fun qconsts_update_thy name qcinfo = QConstsData.map (Symtab.cons_list (name, qcinfo))
-fun qconsts_update_gen name qcinfo = Context.mapping (qconsts_update_thy name qcinfo) I
+fun update_quotconsts_global name qcinfo = Quotconsts.map (Symtab.cons_list (name, qcinfo))
+fun update_quotconsts name qcinfo = Context.mapping (update_quotconsts_global name qcinfo) I (* FIXME !? *)
-fun qconsts_dest lthy =
- flat (map snd (Symtab.dest (QConstsData.get (Proof_Context.theory_of lthy))))
+fun dest_quotconsts lthy =
+ flat (map snd (Symtab.dest (Quotconsts.get (Proof_Context.theory_of lthy)))) (* FIXME !? *)
-fun qconsts_lookup thy t =
+fun lookup_quotconsts thy t =
let
val (name, qty) = dest_Const t
- fun matches (x: qconsts_info) =
+ fun matches (x: quotconsts) =
let
val (name', qty') = dest_Const (#qconst x);
in
name = name' andalso Sign.typ_instance thy (qty, qty')
end
in
- (case Symtab.lookup (QConstsData.get thy) name of
+ (case Symtab.lookup (Quotconsts.get thy) name of
NONE => NONE
| SOME l => find_first matches l)
end
-fun print_qconstinfo ctxt =
+fun print_quotconsts ctxt =
let
fun prt_qconst {qconst, rconst, def} =
Pretty.block (separate (Pretty.brk 1)
@@ -204,7 +201,7 @@
Pretty.str "as",
Syntax.pretty_term ctxt (prop_of def)])
in
- QConstsData.get (Proof_Context.theory_of ctxt)
+ Quotconsts.get (Proof_Context.theory_of ctxt)
|> Symtab.dest
|> map snd
|> flat
@@ -214,80 +211,80 @@
end
(* equivalence relation theorems *)
-structure EquivRules = Named_Thms
+structure Equiv_Rules = Named_Thms
(
val name = "quot_equiv"
val description = "equivalence relation theorems"
)
-val equiv_rules_get = EquivRules.get
-val equiv_rules_add = EquivRules.add
+val equiv_rules = Equiv_Rules.get
+val equiv_rules_add = Equiv_Rules.add
(* respectfulness theorems *)
-structure RspRules = Named_Thms
+structure Rsp_Rules = Named_Thms
(
val name = "quot_respect"
val description = "respectfulness theorems"
)
-val rsp_rules_get = RspRules.get
-val rsp_rules_add = RspRules.add
+val rsp_rules = Rsp_Rules.get
+val rsp_rules_add = Rsp_Rules.add
(* preservation theorems *)
-structure PrsRules = Named_Thms
+structure Prs_Rules = Named_Thms
(
val name = "quot_preserve"
val description = "preservation theorems"
)
-val prs_rules_get = PrsRules.get
-val prs_rules_add = PrsRules.add
+val prs_rules = Prs_Rules.get
+val prs_rules_add = Prs_Rules.add
(* id simplification theorems *)
-structure IdSimps = Named_Thms
+structure Id_Simps = Named_Thms
(
val name = "id_simps"
val description = "identity simp rules for maps"
)
-val id_simps_get = IdSimps.get
+val id_simps = Id_Simps.get
(* quotient theorems *)
-structure QuotientRules = Named_Thms
+structure Quotient_Rules = Named_Thms
(
val name = "quot_thm"
val description = "quotient theorems"
)
-val quotient_rules_get = QuotientRules.get
-val quotient_rules_add = QuotientRules.add
+val quotient_rules = Quotient_Rules.get
+val quotient_rules_add = Quotient_Rules.add
(* theory setup *)
val setup =
- Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute)
+ Attrib.setup @{binding map} (maps_attr_parser >> maps_attribute)
"declaration of map information" #>
- EquivRules.setup #>
- RspRules.setup #>
- PrsRules.setup #>
- IdSimps.setup #>
- QuotientRules.setup
+ Equiv_Rules.setup #>
+ Rsp_Rules.setup #>
+ Prs_Rules.setup #>
+ Id_Simps.setup #>
+ Quotient_Rules.setup
(* outer syntax commands *)
val _ =
Outer_Syntax.improper_command "print_quotmaps" "print quotient map functions" Keyword.diag
- (Scan.succeed (Toplevel.keep (print_mapsinfo o Toplevel.context_of)))
+ (Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of)))
val _ =
Outer_Syntax.improper_command "print_quotients" "print quotients" Keyword.diag
- (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of)))
+ (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
val _ =
Outer_Syntax.improper_command "print_quotconsts" "print quotient constants" Keyword.diag
- (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of)))
+ (Scan.succeed (Toplevel.keep (print_quotconsts o Toplevel.context_of)))
-end; (* structure *)
+end;
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Oct 27 19:41:08 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Oct 27 20:26:38 2011 +0200
@@ -52,7 +52,7 @@
(** solvers for equivp and quotient assumptions **)
fun equiv_tac ctxt =
- REPEAT_ALL_NEW (resolve_tac (Quotient_Info.equiv_rules_get ctxt))
+ REPEAT_ALL_NEW (resolve_tac (Quotient_Info.equiv_rules ctxt))
fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
val equiv_solver = mk_solver "Equivalence goal solver" equiv_solver_tac
@@ -60,7 +60,7 @@
fun quotient_tac ctxt =
(REPEAT_ALL_NEW (FIRST'
[rtac @{thm identity_quotient},
- resolve_tac (Quotient_Info.quotient_rules_get ctxt)]))
+ resolve_tac (Quotient_Info.quotient_rules ctxt)]))
fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
val quotient_solver = mk_solver "Quotient goal solver" quotient_solver_tac
@@ -147,11 +147,11 @@
fun reflp_get ctxt =
map_filter (fn th => if prems_of th = [] then SOME (OF1 @{thm equivp_reflp} th) else NONE
- handle THM _ => NONE) (Quotient_Info.equiv_rules_get ctxt)
+ handle THM _ => NONE) (Quotient_Info.equiv_rules ctxt)
val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)}
-fun eq_imp_rel_get ctxt = map (OF1 eq_imp_rel) (Quotient_Info.equiv_rules_get ctxt)
+fun eq_imp_rel_get ctxt = map (OF1 eq_imp_rel) (Quotient_Info.equiv_rules ctxt)
fun regularize_tac ctxt =
let
@@ -373,7 +373,7 @@
(* respectfulness of constants; in particular of a simple relation *)
| _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *)
- => resolve_tac (Quotient_Info.rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
+ => resolve_tac (Quotient_Info.rsp_rules ctxt) THEN_ALL_NEW quotient_tac ctxt
(* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
(* observe map_fun *)
@@ -521,9 +521,9 @@
*)
fun clean_tac lthy =
let
- val defs = map (Thm.symmetric o #def) (Quotient_Info.qconsts_dest lthy)
- val prs = Quotient_Info.prs_rules_get lthy
- val ids = Quotient_Info.id_simps_get lthy
+ val defs = map (Thm.symmetric o #def) (Quotient_Info.dest_quotconsts lthy)
+ val prs = Quotient_Info.prs_rules lthy
+ val ids = Quotient_Info.id_simps lthy
val thms =
@{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
@@ -632,7 +632,7 @@
THEN' gen_frees_tac ctxt
THEN' SUBGOAL (fn (goal, i) =>
let
- val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
+ val qtys = map #qtyp (Quotient_Info.dest_quotients ctxt)
val rtrm = Quotient_Term.derive_rtrm ctxt qtys goal
val rule = procedure_inst ctxt rtrm goal
in
@@ -711,7 +711,7 @@
val lifted_attrib = Thm.rule_attribute (fn context =>
let
val ctxt = Context.proof_of context
- val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
+ val qtys = map #qtyp (Quotient_Info.dest_quotients ctxt)
in
lifted ctxt qtys []
end)
--- a/src/HOL/Tools/Quotient/quotient_term.ML Thu Oct 27 19:41:08 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Thu Oct 27 20:26:38 2011 +0200
@@ -63,9 +63,9 @@
| RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1
fun get_mapfun ctxt s =
- case Quotient_Info.maps_lookup (Proof_Context.theory_of ctxt) s of
+ (case Quotient_Info.lookup_quotmaps (Proof_Context.theory_of ctxt) s of
SOME map_data => Const (#mapfun map_data, dummyT)
- | NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
+ | NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found."))
(* makes a Free out of a TVar *)
fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
@@ -96,7 +96,7 @@
a quotient definition
*)
fun get_rty_qty ctxt s =
- case Quotient_Info.quotdata_lookup (Proof_Context.theory_of ctxt) s of
+ case Quotient_Info.lookup_quotients (Proof_Context.theory_of ctxt) s of
SOME qdata => (#rtyp qdata, #qtyp qdata)
| NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.");
@@ -271,9 +271,9 @@
Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
fun get_relmap ctxt s =
- case Quotient_Info.maps_lookup (Proof_Context.theory_of ctxt) s of
+ (case Quotient_Info.lookup_quotmaps (Proof_Context.theory_of ctxt) s of
SOME map_data => Const (#relmap map_data, dummyT)
- | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
+ | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")"))
fun mk_relmap ctxt vs rty =
let
@@ -290,9 +290,9 @@
end
fun get_equiv_rel ctxt s =
- case Quotient_Info.quotdata_lookup (Proof_Context.theory_of ctxt) s of
- SOME qdata => #equiv_rel qdata
- | NONE => raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
+ (case Quotient_Info.lookup_quotients (Proof_Context.theory_of ctxt) s of
+ SOME qdata => #equiv_rel qdata
+ | NONE => raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")"))
fun equiv_match_err ctxt ty_pat ty =
let
@@ -427,7 +427,7 @@
if length rtys <> length qtys then false
else forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
else
- (case Quotient_Info.quotdata_lookup thy qs of
+ (case Quotient_Info.lookup_quotients thy qs of
SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
| NONE => false)
| _ => false)
@@ -553,9 +553,10 @@
if same_const rtrm qtrm then rtrm
else
let
- val rtrm' = case Quotient_Info.qconsts_lookup thy qtrm of
- SOME qconst_info => #rconst qconst_info
- | NONE => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm
+ val rtrm' =
+ (case Quotient_Info.lookup_quotconsts thy qtrm of
+ SOME qconst_info => #rconst qconst_info
+ | NONE => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm)
in
if Pattern.matches thy (rtrm', rtrm)
then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm
@@ -743,7 +744,7 @@
let
val thy = Proof_Context.theory_of ctxt
in
- Quotient_Info.quotdata_dest ctxt
+ Quotient_Info.dest_quotients ctxt
|> map (fn x => (#rtyp x, #qtyp x))
|> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty)
|> map (if direction then swap else I)
@@ -755,12 +756,12 @@
fun proper (t1, t2) = subst_typ' (fastype_of t1) = fastype_of t2
val const_substs =
- Quotient_Info.qconsts_dest ctxt
+ Quotient_Info.dest_quotconsts ctxt
|> map (fn x => (#rconst x, #qconst x))
|> map (if direction then swap else I)
val rel_substs =
- Quotient_Info.quotdata_dest ctxt
+ Quotient_Info.dest_quotients ctxt
|> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x)))
|> map (if direction then swap else I)
in
@@ -787,4 +788,4 @@
subst_trm ctxt (mk_ty_subst qtys true ctxt) (mk_trm_subst qtys true ctxt) qtrm
-end; (* structure *)
+end;
--- a/src/HOL/Tools/Quotient/quotient_typ.ML Thu Oct 27 19:41:08 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML Thu Oct 27 20:26:38 2011 +0200
@@ -2,13 +2,12 @@
Author: Cezary Kaliszyk and Christian Urban
Definition of a quotient type.
-
*)
signature QUOTIENT_TYPE =
sig
val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) * thm
- -> Proof.context -> Quotient_Info.quotdata_info * local_theory
+ -> Proof.context -> Quotient_Info.quotients * local_theory
val quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) list
-> Proof.context -> Proof.state
@@ -161,20 +160,20 @@
(* name equivalence theorem *)
val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
- (* storing the quotdata *)
- val quotdata = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
+ (* storing the quotients *)
+ val quotients = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
- fun qinfo phi = Quotient_Info.transform_quotdata phi quotdata
+ fun qinfo phi = Quotient_Info.transform_quotients phi quotients
val lthy4 = lthy3
|> Local_Theory.declaration true
- (fn phi => Quotient_Info.quotdata_update_gen qty_full_name (qinfo phi))
+ (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi))
|> note
(equiv_thm_name, equiv_thm,
if partial then [] else [intern_attr Quotient_Info.equiv_rules_add])
|> note (quotient_thm_name, quotient_thm, [intern_attr Quotient_Info.quotient_rules_add])
in
- (quotdata, lthy4)
+ (quotients, lthy4)
end
@@ -225,7 +224,7 @@
fun map_check_aux rty warns =
case rty of
Type (_, []) => warns
- | Type (s, _) => if is_some (Quotient_Info.maps_lookup thy s) then warns else s :: warns
+ | Type (s, _) => if is_some (Quotient_Info.lookup_quotmaps thy s) then warns else s :: warns
| _ => warns
val warns = map_check_aux rty []