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

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 *)