1 (*  Title:      nominal_dt_alpha.ML

     2     Author:     Christian Urban

     3     Author:     Cezary Kaliszyk

     4 

     5   Performing quotient constructions

     6 *)

     7 

     8 signature NOMINAL_DT_QUOT =

     9 sig

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

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

    12 

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

    14     Quotient_Info.qconsts_info list * local_theory

    15 end

    16 

    17 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =

    18 struct

    19 

    20 (* defines the quotient types *)

    21 fun qtype_defs qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy =

    22 let

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

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

    25 in

    26   fold_map Quotient_Type.add_quotient_type qty_args2 lthy

    27 end 

    28 

    29 (* defines quotient constants *)

    30 fun qconst_defs qtys const_spec lthy =

    31 let

    32   val (qconst_infos, lthy') = fold_map (Quotient_Def.lift_raw_const qtys) const_spec lthy

    33   val phi = ProofContext.export_morphism lthy' lthy

    34 in

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

    36 end

    37 

    38 

    39 

    40 end (* structure *)

    41