# HG changeset patch # User Christian Urban # Date 1277379231 -3600 # Node ID 70d03844b2f957f198e6e0b94ca009e8f6dd0bcd # Parent 0246a314b57d9f4ecd20615aa1f5d96f10e0e2e4 export of proper information in the ML-interface of the quotient package diff -r 0246a314b57d -r 70d03844b2f9 src/HOL/Tools/Quotient/quotient_def.ML --- a/src/HOL/Tools/Quotient/quotient_def.ML Thu Jun 24 11:08:21 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Thu Jun 24 12:33:51 2010 +0100 @@ -7,13 +7,13 @@ signature QUOTIENT_DEF = sig val quotient_def: (binding option * mixfix) * (Attrib.binding * (term * term)) -> - local_theory -> (term * thm) * local_theory + local_theory -> Quotient_Info.qconsts_info * local_theory val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) -> - local_theory -> (term * thm) * local_theory + local_theory -> Quotient_Info.qconsts_info * local_theory val quotient_lift_const: typ list -> string * term -> local_theory -> - (term * thm) * local_theory + Quotient_Info.qconsts_info * local_theory end; structure Quotient_Def: QUOTIENT_DEF = @@ -45,7 +45,7 @@ val pos = Position.str_of (Binding.pos_of bind) in error ("Head of quotient_definition " ^ - (quote str) ^ " differs from declaration " ^ name ^ pos) + quote str ^ " differs from declaration " ^ name ^ pos) end fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy = @@ -69,12 +69,14 @@ val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy (* data storage *) - fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm} + val qconst_data = {qconst = trm, rconst = rhs, def = thm} + + fun qcinfo phi = transform_qconsts phi qconst_data fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi) val lthy'' = Local_Theory.declaration true (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy' in - ((trm, thm), lthy'') + (qconst_data, lthy'') end fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy = diff -r 0246a314b57d -r 70d03844b2f9 src/HOL/Tools/Quotient/quotient_term.ML --- a/src/HOL/Tools/Quotient/quotient_term.ML Thu Jun 24 11:08:21 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Thu Jun 24 12:33:51 2010 +0100 @@ -84,7 +84,7 @@ *) fun mk_mapfun ctxt vs rty = let - val vs' = map (mk_Free) vs + val vs' = map mk_Free vs fun mk_mapfun_aux rty = case rty of @@ -103,7 +103,7 @@ let val thy = ProofContext.theory_of ctxt val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.") - val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn + val qdata = quotdata_lookup thy s handle Quotient_Info.NotFound => raise exn in (#rtyp qdata, #qtyp qdata) end diff -r 0246a314b57d -r 70d03844b2f9 src/HOL/Tools/Quotient/quotient_typ.ML --- a/src/HOL/Tools/Quotient/quotient_typ.ML Thu Jun 24 11:08:21 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML Thu Jun 24 12:33:51 2010 +0100 @@ -8,7 +8,7 @@ signature QUOTIENT_TYPE = sig val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) * thm - -> Proof.context -> (thm * thm) * local_theory + -> Proof.context -> Quotient_Info.quotdata_info * local_theory val quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) list -> Proof.context -> Proof.state @@ -32,11 +32,8 @@ end fun note (name, thm, attrs) lthy = -let - val ((_,[thm']), lthy') = Local_Theory.note ((name, attrs), [thm]) lthy -in - (thm', lthy') -end + Local_Theory.note ((name, attrs), [thm]) lthy |> snd + fun intern_attr at = Attrib.internal (K at) @@ -64,7 +61,7 @@ |> map Free in lambda c (HOLogic.exists_const rty $ - lambda x (HOLogic.mk_conj ((rel $ x $ x), (HOLogic.mk_eq (c, (rel $ x)))))) + lambda x (HOLogic.mk_conj (rel $ x $ x, HOLogic.mk_eq (c, rel $ x)))) end @@ -139,7 +136,10 @@ (* main function for constructing a quotient type *) fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial)), equiv_thm) lthy = let - val part_equiv = if partial then equiv_thm else equiv_thm RS @{thm equivp_implies_part_equivp} + val part_equiv = + if partial + then equiv_thm + else equiv_thm RS @{thm equivp_implies_part_equivp} (* generates the typedef *) val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy @@ -173,15 +173,17 @@ (* name equivalence theorem *) val equiv_thm_name = Binding.suffix_name "_equivp" qty_name - (* storing the quot-info *) - fun qinfo phi = transform_quotdata phi - {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm} - val lthy4 = Local_Theory.declaration true - (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) lthy3 + (* storing the quotdata *) + val quotdata = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm} + + fun qinfo phi = transform_quotdata phi quotdata + + val lthy4 = lthy3 + |> Local_Theory.declaration true (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) + |> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add]) + |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) in - lthy4 - |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) - ||>> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add]) + (quotdata, lthy4) end @@ -253,6 +255,7 @@ - its free type variables (first argument) - its mixfix annotation - the type to be quotient + - the partial flag (a boolean) - the relation according to which the type is quotient it opens a proof-state in which one has to show that the @@ -268,7 +271,8 @@ fun mk_goal (rty, rel, partial) = let val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} - val const = if partial then @{const_name part_equivp} else @{const_name equivp} + val const = + if partial then @{const_name part_equivp} else @{const_name equivp} in HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel) end