theory Lift
imports "../Nominal-General/Nominal2_Atoms"
        "../Nominal-General/Nominal2_Eqvt"
        "../Nominal-General/Nominal2_Supp"
        "Abs" "Perm" "Rsp"
begin

ML {*
fun define_quotient_types binds tys alphas equivps ctxt =
let
  fun def_ty ((b, ty), (alpha, equivp)) ctxt =
    Quotient_Type.add_quotient_type ((([], b, NoSyn), (ty, alpha, false)), equivp) ctxt;
  val alpha_equivps = List.take (equivps, length alphas)
  val (qinfo, ctxt') = fold_map def_ty ((binds ~~ tys) ~~ (alphas ~~ alpha_equivps)) ctxt;
  val qtys = map #qtyp qinfo;
in
  (qtys, ctxt')
end
*}

(* Unrawifying schematic and bound variables *)

ML {*
fun unraw_str s = 
  unsuffix "_raw" s
  handle Fail _ => s

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

  val vars = Term.add_vars (prop_of thm) []
  val nvars = map (Var o unraw_var) vars
in
  Thm.certify_instantiate ([], (vars ~~ nvars))  thm
end
*}

ML {*
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
*}


ML {*
fun lift_thm qtys ctxt thm =
  Quotient_Tacs.lifted qtys ctxt thm
  |> unraw_bounds_thm
  |> unraw_vars_thm
*}


end