parse term in auxiliary context augmented with variable;
pass through binding appropriately;
more standard syntax and ML interface
(* Title: HOL/Tools/Quotient/quotient_def.ML
Author: Cezary Kaliszyk and Christian Urban
Definitions for constants on quotient types.
*)
signature QUOTIENT_DEF =
sig
val quotient_def: (binding * typ option * mixfix) option * (Attrib.binding * (term * term)) ->
local_theory -> Quotient_Info.qconsts_info * local_theory
val quotdef_cmd: (binding * string option * mixfix) option * (Attrib.binding * (string * string)) ->
local_theory -> Quotient_Info.qconsts_info * local_theory
val lift_raw_const: typ list -> (string * term * mixfix) -> local_theory ->
Quotient_Info.qconsts_info * local_theory
end;
structure Quotient_Def: QUOTIENT_DEF =
struct
(** Interface and Syntax Setup **)
(* The ML-interface for a quotient definition takes
as argument:
- an optional binding and mixfix annotation
- attributes
- the new constant as term
- the rhs of the definition as term
It stores the qconst_info in the qconsts data slot.
Restriction: At the moment the left- and right-hand
side of the definition must be a constant.
*)
fun error_msg bind str =
let
val name = Binding.name_of bind
val pos = Position.str_of (Binding.pos_of bind)
in
error ("Head of quotient_definition " ^
quote str ^ " differs from declaration " ^ name ^ pos)
end
fun gen_quotient_def prep_vars prep_term (raw_var, (attr, (lhs_raw, rhs_raw))) lthy =
let
val (vars, ctxt) = prep_vars (the_list raw_var) lthy
val lhs = prep_term ctxt lhs_raw
val rhs = prep_term ctxt rhs_raw
val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
val _ = if is_Const rhs then () else warning "The definiens is not a constant"
val var =
(case vars of
[] => (Binding.name lhs_str, NoSyn)
| [(binding, _, mx)] =>
if Variable.check_name binding = lhs_str then (binding, mx)
else error_msg binding lhs_str
| _ => raise Match)
val absrep_trm = Quotient_Term.absrep_fun Quotient_Term.AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
val (_, prop') = Local_Defs.cert_def lthy prop
val (_, newrhs) = Local_Defs.abs_def prop'
val ((trm, (_ , thm)), lthy') = Local_Theory.define (var, (attr, newrhs)) lthy
(* data storage *)
val qconst_data = {qconst = trm, rconst = rhs, def = thm}
fun qcinfo phi = Quotient_Info.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 => Quotient_Info.qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
in
(qconst_data, lthy'')
end
val quotient_def = gen_quotient_def Proof_Context.cert_vars Syntax.check_term
val quotdef_cmd = gen_quotient_def Proof_Context.read_vars Syntax.read_term
(* a wrapper for automatically lifting a raw constant *)
fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt =
let
val rty = fastype_of rconst
val qty = Quotient_Term.derive_qtyp ctxt qtys rty
val lhs = Free (qconst_name, qty)
in
quotient_def (SOME (Binding.name qconst_name, NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
end
(* parser and command *)
val quotdef_parser =
Scan.option Parse_Spec.constdecl --
Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| Parse.$$$ "is" -- Parse.term))
val _ =
Outer_Syntax.local_theory "quotient_definition"
"definition for constants over the quotient type"
Keyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd))
end; (* structure *)