(* Title: quotient_def.thy Author: Cezary Kaliszyk and Christian Urban Definitions for constants on quotient types.*)signature QUOTIENT_DEF =sig val quotient_def: (Attrib.binding * mixfix) option * (Attrib.binding * (term * term)) -> local_theory -> (term * thm) * local_theory val quotdef_cmd: (Attrib.binding * mixfix) option * (Attrib.binding * (string * string)) -> local_theory -> local_theoryend;structure Quotient_Def: QUOTIENT_DEF =structopen Quotient_Info;open Quotient_Term;(** 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 (bindmx, (attr, (lhs, rhs))) lthy =let val mx = case bindmx of SOME (_, mx) => mx | _ => NoSyn 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') = Local_Theory.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 (bindmx, (attr, (lhs_str, rhs_str))) lthy =let val lhs = Syntax.read_term lthy lhs_str val rhs = Syntax.read_term lthy rhs_str val lthy' = Variable.declare_term lhs lthy val lthy'' = Variable.declare_term rhs lthy'in quotient_def (bindmx, (attr, (lhs, rhs))) lthy'' |> sndendval binding_mixfix_parser = OuterParse.binding -- OuterParse.opt_mixfix' --| OuterParse.$$$ "where"val quotdef_parser = (Scan.option binding_mixfix_parser) -- OuterParse.!!! (SpecParse.opt_thm_name ":" -- ((OuterParse.term --| OuterParse.$$$ "is") -- OuterParse.term))val _ = OuterSyntax.local_theory "quotient_definition" "definition for constants over the quotient type" OuterKeyword.thy_decl (quotdef_parser >> (quotdef_cmd))end; (* structure *)