(*  Title:      nominal_dt_alpha.ML
    Author:     Christian Urban
    Author:     Cezary Kaliszyk

  Performing quotient constructions
*)

signature NOMINAL_DT_QUOT =
sig
  val define_qtypes: (string list * binding * mixfix) list -> typ list -> term list -> 
    thm list -> local_theory -> Quotient_Info.quotdata_info list * local_theory

  val define_qconsts: typ list -> (string  * term * mixfix) list -> local_theory -> 
    Quotient_Info.qconsts_info list * local_theory

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

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

structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
struct

(* defines the quotient types *)
fun define_qtypes 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 define_qconsts 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 and proves pt-class *)
fun define_qperms qtys qfull_ty_names perm_specs raw_perm_laws lthy =
let
  val lthy' = 
    lthy
    |> Local_Theory.exit_global
    |> Class.instantiation (qfull_ty_names, [], @{sort pt}) 
  
  val (_, lthy'') = define_qconsts qtys perm_specs lthy'

  val lifted_perm_laws = map (Quotient_Tacs.lifted qtys lthy'') raw_perm_laws

  fun tac _ =
    Class.intro_classes_tac [] THEN
      (ALLGOALS (resolve_tac lifted_perm_laws))
in
  lthy''
  |> Class.prove_instantiation_exit tac 
  |> Named_Target.theory_init
end


(* defines the size functions and proves size-class *)
fun define_qsizes qtys qfull_ty_names size_specs lthy =
let
  fun tac _ = Class.intro_classes_tac []
in
  lthy
  |> Local_Theory.exit_global
  |> Class.instantiation (qfull_ty_names, [], @{sort size})
  |> snd o (define_qconsts qtys size_specs)
  |> Class.prove_instantiation_exit tac
  |> Named_Target.theory_init
end

end (* structure *)