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 a 4-tuple consisting of     *)
(*                                                    *)
(* - 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 Free (lhs_str, lhs_ty) = lhs; (* FIXME/TODO: this throws an excpt., if the const is already def.*)
  val qconst_bname = Binding.name lhs_str;
  val absrep_trm = (absrep_fun_chk absF lthy (fastype_of rhs, lhs_ty)) $ rhs
  val prop = Logic.mk_equals (lhs, 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 *)