signature QUOTIENT_DEF =

sig

  datatype flag = absF | repF

  val get_fun: flag -> Proof.context -> typ * typ -> term

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

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

  val quotdef: (binding * term * 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

datatype flag = absF | repF

fun negF absF = repF

  | negF repF = absF

fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)

fun get_fun_aux lthy s fs =

  case (maps_lookup (ProofContext.theory_of lthy) s) of

    SOME info => list_comb (Const (#mapfun info, dummyT), fs)

  | NONE      => raise 

        (LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."]))

fun get_const flag lthy _ qty =

(* FIXME: check here that _ and qty are related *)

let 

  val thy = ProofContext.theory_of lthy

  val qty_name = Long_Name.base_name (fst (dest_Type qty))

in

  case flag of

    absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT)

  | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)

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

fun get_fun flag lthy (rty, qty) =

  if rty = qty then mk_identity qty else

  case (rty, qty) of 

    (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>

     let

       val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1')

       val fs_ty2 = get_fun flag lthy (ty2, ty2')

     in  

       get_fun_aux lthy "fun" [fs_ty1, fs_ty2]

     end 

  | (Type (s, []), Type (s', [])) =>

     if s = s'

     then mk_identity qty 

     else get_const flag lthy rty qty

  | (Type (s, tys), Type (s', tys')) =>

     if s = s'

     then get_fun_aux lthy s' (map (get_fun flag lthy) (tys ~~ tys'))

     else get_const flag lthy rty qty

  | (TFree x, TFree x') =>

     if x = x'

     then mk_identity qty 

     else raise (LIFT_MATCH "get_fun")

  | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun")

  | _ => raise (LIFT_MATCH "get_fun")

fun make_def qconst_bname mx attr lhs rhs lthy =

let

  val absrep_trm = get_fun absF lthy (fastype_of rhs, fastype_of lhs) $ rhs

                   |> Syntax.check_term lthy

  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

  fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm}

  val lthy'' = Local_Theory.declaration true

                 (fn phi => 

                       let

                         val qconst_str = Binding.name_of qconst_bname

                       in                      

                         qconsts_update_gen qconst_str (qcinfo phi)

                       end) lthy'

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, lhs, mx), (attr, rhs)) lthy =

  make_def bind mx attr lhs rhs lthy

fun quotdef_cmd ((bind, lhsstr, mx), (attr, rhsstr)) lthy = 

let

  val lhs = Syntax.read_term lthy lhsstr

  val rhs = Syntax.read_term lthy rhsstr

in

  quotdef ((bind, lhs, mx), (attr, rhs)) lthy |> snd

end

val quotdef_parser =

  (OuterParse.binding --

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

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

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

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

  OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)

end; (* structure *)

open Quotient_Def;