(*  Title:      nominal_dt_alpha.ML

    Author:     Christian Urban

    Author:     Cezary Kaliszyk

  Performing quotient constructions

*)

signature NOMINAL_DT_QUOT =

sig

  val qtype_defs: (string list * binding * mixfix) list -> typ list -> term list -> 

    thm list -> local_theory -> Quotient_Info.quotdata_info list * local_theory

  val qconst_defs: typ list -> (string  * term * mixfix) list -> local_theory -> 

    Quotient_Info.qconsts_info list * local_theory

  val qperm_defs: typ list -> string list -> (string * term * mixfix) list -> 

    thm list -> theory -> theory

end

structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =

struct

(* defines the quotient types *)

fun qtype_defs qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy =

let

  val qty_args1 = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms

  val qty_args2 = (qtys_descr ~~ qty_args1) ~~ alpha_equivp_thms

in

  fold_map Quotient_Type.add_quotient_type qty_args2 lthy

end 

(* defines quotient constants *)

fun qconst_defs qtys consts_specs lthy =

let

  val (qconst_infos, lthy') = 

    fold_map (Quotient_Def.lift_raw_const qtys) consts_specs lthy

  val phi = ProofContext.export_morphism lthy' lthy

in

  (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy')

end

(* defines the quotient permutations *)

fun qperm_defs qtys full_tnames name_term_pairs thms thy =

let

  val lthy =

    Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;

  val (_, lthy') = qconst_defs qtys name_term_pairs lthy;

  val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms;

  fun tac _ =

    Class.intro_classes_tac [] THEN

    (ALLGOALS (resolve_tac lifted_thms))

  val lthy'' = Class.prove_instantiation_instance tac lthy'

in

  Local_Theory.exit_global lthy''

end

end (* structure *)