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

use "nominal_dt_rawperm.ML"
use "nominal_dt_rawfuns.ML"

ML {*
open Nominal_Dt_RawPerm
open Nominal_Dt_RawFuns
*}

ML {*
fun is_atom ctxt ty =
  Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})

fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t
  | is_atom_set _ _ = false;

fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t
  | is_atom_fset _ _ = false;

fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t
  | is_atom_list _ _ = false


(* functions for producing sets, fsets and lists of general atom type
   out from concrete atom types *)
fun mk_atom_set t =
let
  val ty = fastype_of t;
  val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"};
  val img_ty = atom_ty --> ty --> @{typ "atom set"};
in
  Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t
end

fun mk_atom_fset t =
let
  val ty = fastype_of t;
  val atom_ty = dest_fsetT ty --> @{typ "atom"};
  val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};
  val fset_to_set = @{term "fset_to_set :: atom fset => atom set"}
in
  fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
end
*}
(* permutations for quotient types *)

ML {* Class_Target.prove_instantiation_exit_result *}

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

ML {*
fun neq_to_rel r neq =
let
  val neq = HOLogic.dest_Trueprop (prop_of neq)
  val eq = HOLogic.dest_not neq
  val (lhs, rhs) = HOLogic.dest_eq eq
  val rel = r $ lhs $ rhs
  val nrel = HOLogic.mk_not rel
in
  HOLogic.mk_Trueprop nrel
end
*}

ML {*
fun neq_to_rel_tac cases distinct =
  rtac notI THEN' eresolve_tac cases THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct)
*}

ML {*
fun distinct_rel ctxt cases (dists, rel) =
let
  val ((_, thms), ctxt') = Variable.import false dists ctxt
  val terms = map (neq_to_rel rel) thms
  val nrels = map (fn t => Goal.prove ctxt' [] [] t (fn _ => neq_to_rel_tac cases dists 1)) terms
in
  Variable.export ctxt' ctxt nrels
end
*}



(* Test *)
(*
atom_decl name

datatype trm =
  Var "name"
| App "trm" "(trm list) list"
| Lam "name" "trm"
| Let "bp" "trm" "trm"
and bp =
  BUnit
| BVar "name"
| BPair "bp" "bp"

setup {* fn thy =>
let 
  val info = Datatype.the_info thy "Perm.trm"
in
  define_raw_perms info 2 thy |> snd
end
*}

print_theorems
*)

end