theory Perm

imports "Nominal2_Atoms"

begin

ML {*

  open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *)

  fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty);

  val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm});

*}

ML {*

(* TODO: full_name can be obtained from new_type_names with Datatype *)

fun define_raw_perms new_type_names full_tnames thy =

let

  val {descr, induct, ...} = Datatype.the_info thy (hd full_tnames);

  (* TODO: [] should be the sorts that we'll take from the specification *)

  val sorts = [];

  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);

  val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) =>

    "permute_" ^ name_of_typ (nth_dtyp i)) descr);

  val perm_types = map (fn (i, _) =>

    let val T = nth_dtyp i

    in @{typ perm} --> T --> T end) descr;

  val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);

  val perm_names_types' = perm_names' ~~ perm_types;

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

  fun perm_eq_constr i (cname, dts) =

    let

      val Ts = map (typ_of_dtyp descr sorts) dts;

      val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);

      val args = map Free (names ~~ Ts);

      val c = Const (cname, Ts ---> (nth_dtyp i));

      fun perm_arg (dt, x) =

        let val T = type_of x

        in

          if is_rec_type dt then

            let val (Us, _) = strip_type T

            in list_abs (map (pair "x") Us,

              Free (nth perm_names_types' (body_index dt)) $ pi $

                list_comb (x, map (fn (i, U) =>

                  (permute U) $ (minus_perm $ pi) $ Bound i)

                  ((length Us - 1 downto 0) ~~ Us)))

            end

          else (permute T) $ pi $ x

        end;

    in

      (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq

        (Free (nth perm_names_types' i) $

           Free ("pi", @{typ perm}) $ list_comb (c, args),

         list_comb (c, map perm_arg (dts ~~ args)))))

    end;

    fun perm_eq (i, (_, _, constrs)) = map (perm_eq_constr i) constrs;

    val perm_eqs = maps perm_eq descr;

    val lthy =

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

    (* TODO: Use the version of prmrec that gives the names explicitely. *)

    val (perm_ldef, lthy') =

      Primrec.add_primrec

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

    val perm_frees =

      (distinct (op =)) (map (fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) perm_ldef);

    val perm_empty_thms =

      let

        val gl =

          HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj

            (map (fn ((perm, T), x) => HOLogic.mk_eq

                (perm $ @{term "0 :: perm"} $ Free (x, T),

                 Free (x, T)))

             (perm_frees ~~

              map body_type perm_types ~~ perm_indnames)));

        fun tac {context = ctxt, ...} =

          EVERY [

            indtac induct perm_indnames 1,

            ALLGOALS (asm_full_simp_tac (@{simpset} addsimps perm_ldef))

          ];

      in

        (List.take (split_conj_thm (Goal.prove lthy' perm_indnames [] gl tac), length new_type_names))

      end;

    val add_perm = @{term "op + :: (perm \<Rightarrow> perm \<Rightarrow> perm)"}

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

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

    val perm_append_thms =

       List.take ((split_conj_thm

         (Goal.prove lthy' ("pi1" :: "pi2" :: perm_indnames) []

            (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj

               (map (fn ((perm, T), x) =>

                   let

                     val lhs = perm $ (add_perm $ pi1 $ pi2) $ Free (x, T)

                     val rhs = perm $ pi1 $ (perm $ pi2 $ Free (x, T))

                   in HOLogic.mk_eq (lhs, rhs)

                   end)

                 (perm_frees ~~

                  map body_type perm_types ~~ perm_indnames))))

            (fn _ => EVERY [indtac induct perm_indnames 1,

               ALLGOALS (asm_full_simp_tac (@{simpset} addsimps perm_ldef))]))),

          length new_type_names);

    fun tac ctxt perm_thms =

      (Class.intro_classes_tac []) THEN (ALLGOALS (

        simp_tac (@{simpset} addsimps perm_thms

      )));

    fun morphism phi = map (Morphism.thm phi);

  in

    Class_Target.prove_instantiation_exit_result morphism tac (perm_empty_thms @ perm_append_thms) lthy'

  end

*}

(* Test

atom_decl name

datatype rtrm1 =

  rVr1 "name"

| rAp1 "rtrm1" "rtrm1 list"

| rLm1 "name" "rtrm1"

| rLt1 "bp" "rtrm1" "rtrm1"

and bp =

  BUnit

| BVr "name"

| BPr "bp" "bp"

setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Perm.rtrm1", "Perm.bp"] *}

print_theorems

*)

end