signature QUOTIENT_DEF =

sig

  datatype flag = absF | repF

  val make_def: binding -> typ -> mixfix -> Attrib.binding -> term ->

    Proof.context -> (term * thm) * local_theory

  val quotdef: (binding * typ * mixfix) * (Attrib.binding * term) ->

    local_theory -> (term * thm) * local_theory

  val quotdef_cmd: (binding * string * mixfix) * (Attrib.binding * string) ->

    local_theory -> local_theory

end;

structure Quotient_Def: QUOTIENT_DEF =

struct

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

(* calculates the aggregate abs and rep functions for a given type; 

   repF is for constants' arguments; absF is for constants;

   function types need to be treated specially, since repF and absF

   change *)

datatype flag = absF | repF

fun negF absF = repF

  | negF repF = absF

in

end

  val thy = ProofContext.theory_of lthy

fun make_def nconst_bname qty mx attr rhs lthy =

let

  val rty = fastype_of rhs

  fun mk_fun_map t s =  

        Const (@{const_name "fun_map"}, dummyT) $ t $ s

  val absrep_trm = (fold_rev mk_fun_map rep_fns abs_fn $ rhs)

                   |> Syntax.check_term lthy 

  val ((trm, thm), lthy') = define nconst_bname mx attr absrep_trm lthy

  val nconst_str = Binding.name_of nconst_bname

  val lthy'' = Local_Theory.declaration true

in

  ((trm, thm), lthy'')

end

(* interface and syntax setup *)

(* the ML-interface takes a 5-tuple consisting of  *)

(*                                                 *)

(* - the name of the constant to be lifted         *)

(* - its type                                      *)

(* - its mixfix annotation                         *)

(* - a meta-equation defining the constant,        *)

(*   and the attributes of for this meta-equality  *)

fun quotdef ((bind, qty, mx), (attr, prop)) lthy =

let   

  val (_, prop') = LocalDefs.cert_def lthy prop

  val (_, rhs) = Primitive_Defs.abs_def prop'

in

  make_def bind qty mx attr rhs lthy 

end

fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy = 

let

  val qty  = Syntax.read_typ lthy qtystr

  val prop = Syntax.read_prop lthy propstr

in

  quotdef ((bind, qty, mx), (attr, prop)) lthy |> snd

end

val quotdef_parser =

  (OuterParse.binding --

    (OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.typ -- 

      OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) -- 

       (SpecParse.opt_thm_name ":" -- OuterParse.prop)

val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"

  OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)

end; (* structure *)

open Quotient_Def;