theory Perm
imports 
  "../Nominal-General/Nominal2_Base"
  "../Nominal-General/Nominal2_Atoms" 
  "../Nominal-General/Nominal2_Eqvt" 
  "Nominal2_FSet"
  "Abs"
uses ("nominal_dt_rawperm.ML")
     ("nominal_dt_rawfuns.ML")
     ("nominal_dt_alpha.ML")
begin

use "nominal_dt_rawperm.ML"
ML {* open Nominal_Dt_RawPerm *}

use "nominal_dt_rawfuns.ML"
ML {* open Nominal_Dt_RawFuns *}

use "nominal_dt_alpha.ML"
ML {* open Nominal_Dt_Alpha *}

(* permutations for quotient types *)

ML {*
fun quotient_lift_consts_export qtys spec ctxt =
let
  val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt;
  val (ts_loc, defs_loc) = split_list result;
  val morphism = ProofContext.export_morphism ctxt' ctxt;
  val ts = map (Morphism.term morphism) ts_loc
  val defs = Morphism.fact morphism defs_loc
in
  (ts, defs, ctxt')
end
*}

ML {*
fun define_lifted_perms qtys full_tnames name_term_pairs thms thy =
let
  val lthy =
    Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
  val (_, _, lthy') = quotient_lift_consts_export qtys name_term_pairs lthy;
  val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms;
  fun tac _ =
    Class.intro_classes_tac [] THEN
    (ALLGOALS (resolve_tac lifted_thms))
  val lthy'' = Class.prove_instantiation_instance tac lthy'
in
  Local_Theory.exit_global lthy''
end
*}


end