(*  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_thm: Proof.context -> typ list -> thm list -> thm -> thm

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 _ = tracing ("qtys:\n" ^ cat_lines (map @{make_string} qtys))

  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

  fun tac _ = 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" instances 

   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_thm ctxt qtys simps thm =

  |> unraw_bounds_thm

  |> unraw_vars_thm

  |> Drule.zero_var_indexes

end (* structure *)