(* Title: quotient_def.thy Author: Cezary Kaliszyk and Christian Urban Definitions for constants on quotient types.*)signature QUOTIENT_DEF =sig val quotient_def: mixfix -> Attrib.binding -> term -> term -> local_theory -> (term * thm) * local_theory val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) -> local_theory -> local_theoryend;structure Quotient_Def: QUOTIENT_DEF =structopen Quotient_Info;open Quotient_Term;(* wrapper for define *)fun define name mx attr rhs lthy =let val ((rhs, (_ , thm)), lthy') = Local_Theory.define ((name, mx), (attr, rhs)) lthyin ((rhs, thm), lthy')end(** Interface and Syntax Setup **)(* The ML-interface for a quotient definition takes as argument: - the mixfix annotation - name and attributes - the new constant as term - the rhs of the definition as term It returns the defined constant and its definition theorem; stores the data in the qconsts data slot. Restriction: At the moment the right-hand side must be a terms composed of constant. Similarly the left-hand side must be a single constant. *)fun quotient_def mx attr lhs rhs lthy =let 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 qconst_bname = Binding.name lhs_str val absrep_trm = absrep_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) val (_, prop') = LocalDefs.cert_def lthy prop val (_, newrhs) = Primitive_Defs.abs_def prop' val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy (* data storage *) fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm} 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'')endfun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy =let val lhs = Syntax.read_term lthy lhs_str val rhs = Syntax.read_term lthy rhs_str (* FIXME: Relating the reads will cause errors. *) in quotient_def mx attr lhs rhs lthy |> sndendval _ = OuterKeyword.keyword "as";val quotdef_parser = (SpecParse.opt_thm_name ":" -- OuterParse.term) -- (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" -- OuterParse.term)val _ = OuterSyntax.local_theory "quotient_definition" "definition for constants over the quotient type" OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)end; (* structure *)