# HG changeset patch # User wenzelm # Date 1319739998 -7200 # Node ID 89a17197cb9842b6c96432d507812d9e318c9a78 # Parent 7c6c8e950636cde74c18907e59a0b568050a2e1b simplified/standardized signatures; diff -r 7c6c8e950636 -r 89a17197cb98 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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 diff -r 7c6c8e950636 -r 89a17197cb98 src/HOL/Tools/Quotient/quotient_def.ML --- 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 diff -r 7c6c8e950636 -r 89a17197cb98 src/HOL/Tools/Quotient/quotient_info.ML --- 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; diff -r 7c6c8e950636 -r 89a17197cb98 src/HOL/Tools/Quotient/quotient_tacs.ML --- 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) diff -r 7c6c8e950636 -r 89a17197cb98 src/HOL/Tools/Quotient/quotient_term.ML --- 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; diff -r 7c6c8e950636 -r 89a17197cb98 src/HOL/Tools/Quotient/quotient_typ.ML --- 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 []