theory Perm

imports "../Nominal-General/Nominal2_Atoms"

begin

(* definitions of the permute function for raw nominal datatypes *)

ML {*

(* returns the type of the nth datatype *)

fun nth_dtyp dt_descr sorts i = 

  Datatype_Aux.typ_of_dtyp dt_descr sorts (Datatype_Aux.DtRec i);

*}

ML {*

(* permutation function for one argument 

    - in case the argument is recursive it returns 

         permute_fn p arg

    - in case the argument is non-recursive it will build

         p o arg

*)

fun perm_arg permute_fns pi (arg_dty, arg) =

  if Datatype_Aux.is_rec_type arg_dty 

  then Free (nth permute_fns (Datatype_Aux.body_index arg_dty)) $ pi $ arg

  else mk_perm pi arg

*}

ML {*

(* equation for permutation function for one constructor;

   i is the index of the correspodning datatype *)

fun perm_eq_constr dt_descr sorts permute_fns i (cnstr_name, dts) =

let

  val pi = Free ("p", @{typ perm})

  val arg_tys = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts

  val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys)

  val args = map Free (arg_names ~~ arg_tys)

  val cnstr = Const (cnstr_name, arg_tys ---> (nth_dtyp dt_descr sorts i))

  val lhs = Free (nth permute_fns i) $ pi $ list_comb (cnstr, args)

  val rhs = list_comb (cnstr, map (perm_arg permute_fns pi) (dts ~~ args))

  val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))

in

  (Attrib.empty_binding, eq)

end

*}

ML {*

fun prove_permute_zero lthy induct perm_defs perm_fns =

let

  val perm_types = map (body_type o fastype_of) perm_fns

  val perm_indnames = Datatype_Prop.make_tnames perm_types

  fun single_goal ((perm_fn, T), x) =

    HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T))

  val goals =

    HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj

      (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))

  val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs)

  val tac = (Datatype_Aux.indtac induct perm_indnames 

             THEN_ALL_NEW asm_simp_tac simps) 1

in

  Goal.prove lthy perm_indnames [] goals (K tac)

  |> Datatype_Aux.split_conj_thm

end

*}

ML {*

fun prove_permute_plus lthy induct perm_defs perm_fns =

let

  val pi1 = Free ("p", @{typ perm})

  val pi2 = Free ("q", @{typ perm})

  val perm_types = map (body_type o fastype_of) perm_fns

  val perm_indnames = Datatype_Prop.make_tnames perm_types

  fun single_goal ((perm, T), x) = HOLogic.mk_eq 

      (perm $ (mk_plus pi1 pi2) $ Free (x, T), perm $ pi1 $ (perm $ pi2 $ Free (x, T)))

  val goals =

    HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj

      (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))

  val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs)

  val tac = (Datatype_Aux.indtac induct perm_indnames

             THEN_ALL_NEW asm_simp_tac simps) 1

in

  Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac)

  |> Datatype_Aux.split_conj_thm 

end

*}

ML {*

(* defines the permutation functions for raw datatypes and

   proves that they are instances of pt

   dt_nos refers to the number of "un-unfolded" datatypes

   given by the user

*)

fun define_raw_perms (dt_info : Datatype_Aux.info) dt_nos thy =

let

  val {descr as dt_descr, induct, sorts, ...} = dt_info;

  val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr;

  val full_tnames = List.take (all_full_tnames, dt_nos);

  val perm_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr

  val permute_fns = perm_fn_names ~~ perm_types

  fun perm_eq (i, (_, _, constrs)) = 

    map (perm_eq_constr dt_descr sorts permute_fns i) constrs;

  val perm_eqs = maps perm_eq dt_descr;

  val lthy =

    Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;

  val ((perm_fns, perm_ldef), lthy') =

    Primrec.add_primrec

      (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy;

  val perm_zero_thms = prove_permute_zero lthy' induct perm_ldef perm_fns

  val perm_plus_thms = prove_permute_plus lthy' induct perm_ldef perm_fns

  val perm_zero_thms' = List.take (perm_zero_thms, dt_nos);

  val perm_plus_thms' = List.take (perm_plus_thms, dt_nos)

  val perms_name = space_implode "_" perm_fn_names

  val perms_zero_bind = Binding.name (perms_name ^ "_zero")

  val perms_plus_bind = Binding.name (perms_name ^ "_plus")

  fun tac _ (_, simps, _) =

    Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)

  fun morphism phi (dfs, simps, fvs) =

    (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs);

in

  lthy'

  |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms'))

  |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms'))

  |> Class_Target.prove_instantiation_exit_result morphism tac 

       (perm_ldef, perm_zero_thms' @ perm_plus_thms', perm_fns)

end

*}

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

*}

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