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

  Performing quotient constructions and lifting theorems
*)

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 * sort) list -> 
    (string * term * mixfix) list -> thm list -> local_theory -> local_theory

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

  val lift_thms: typ list -> thm list -> thm list -> Proof.context -> thm list * Proof.context

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 tvs perm_specs raw_perm_laws lthy =
  let
    val lthy1 = 
      lthy
      |> Local_Theory.exit_global
      |> Class.instantiation (qfull_ty_names, tvs, @{sort pt}) 
  
    val (qs, lthy2) = define_qconsts qtys perm_specs lthy1

    val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2

    val lifted_perm_laws = 
      map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws'
      |> Variable.exportT lthy3 lthy2

    fun tac _ =
      Class.intro_classes_tac [] THEN
        (ALLGOALS (resolve_tac lifted_perm_laws))
  in
    lthy2
    |> 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 tvs size_specs lthy =
  let
    val tac = K (Class.intro_classes_tac [])
  in
    lthy
    |> Local_Theory.exit_global
    |> Class.instantiation (qfull_ty_names, tvs, @{sort size})
    |> snd o (define_qconsts qtys size_specs)
    |> Class.prove_instantiation_exit tac
    |> Named_Target.theory_init
  end


(* lifts a theorem and cleans all "_raw" parts
   from variable names *)

local
  val any = Scan.one (Symbol.not_eof)
  val raw = Scan.this_string "_raw"
  val exclude =
    Scan.repeat (Scan.unless raw any) --| raw >> implode
  val parser = Scan.repeat (exclude || any)
in
  fun unraw_str s =
    s |> explode
      |> Scan.finite Symbol.stopper parser >> implode 
      |> fst
end

fun unraw_vars_thm thm =
  let
    fun unraw_var_str ((s, i), T) = ((unraw_str s, i), T)

    val vars = Term.add_vars (prop_of thm) []
    val vars' = map (Var o unraw_var_str) vars
  in
    Thm.certify_instantiate ([], (vars ~~ vars')) thm
  end

fun unraw_bounds_thm th =
  let
    val trm = Thm.prop_of th
    val trm' = Term.map_abs_vars unraw_str trm
  in
    Thm.rename_boundvars trm trm' th
  end

fun lift_thms qtys simps thms ctxt =
  (map (Quotient_Tacs.lifted ctxt qtys simps
        #> unraw_bounds_thm
        #> unraw_vars_thm
        #> Drule.zero_var_indexes) thms, ctxt)

end (* structure *)