+
−
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_theory+
−
end;+
−
+
−
structure Quotient_Def: QUOTIENT_DEF =+
−
struct+
−
+
−
open 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)) lthy+
−
in+
−
  ((rhs, thm), lthy')+
−
end+
−
+
−
+
−
(** interface and syntax setup **)+
−
+
−
(* the ML-interface takes+
−
+
−
  - 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 slot       +
−
*)+
−
fun quotient_def mx attr lhs rhs lthy =+
−
let+
−
  val (lhs_str, lhs_ty) =+
−
    dest_Free lhs+
−
    handle TERM _ => error "The name for the new constant has to be a Free; check that it is not defined yet."+
−
  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}+
−
  val lthy'' = Local_Theory.declaration true+
−
                 (fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy'+
−
in+
−
  ((trm, thm), lthy'')+
−
end+
−
+
−
fun 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+
−
in+
−
  quotient_def mx attr lhs rhs lthy |> snd+
−
end+
−
+
−
val _ = 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 *)+
−