theory Perm

begin

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