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")

     ("nominal_dt_quot.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 *}

use "nominal_dt_quot.ML"

ML {* open Nominal_Dt_Quot *}

(* permutations for quotient types *)

ML {*

fun quotient_lift_consts_export qtys spec ctxt =

let

  val (result, ctxt') = fold_map (Quotient_Def.lift_raw_const qtys) spec ctxt;

  val (ts_loc, defs_loc) = split_list (map (fn info => (#qconst info, #def info)) 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