theory Perm

imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs"

begin

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"

ML {*

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

*}

instantiation rtrm1 and bp :: pt

begin

ML {*

  val {descr, induct, ...} = Datatype.the_info @{theory} "Perm.rtrm1";

  val new_type_names = ["rtrm1", "bp"];

  (* 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_names = replicate (length new_type_names) @{const_name permute} @

    map (Sign.full_bname @{theory}) (List.drop (perm_names', length new_type_names));

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

  (* TODO: Next line only needed after instantiation *)

  val perm_names_types = perm_names ~~ perm_types;

  val perm_names_types' = perm_names' ~~ perm_types;

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

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

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

*}

ML {*

  val perm_eqs = maps (fn (i, (_, _, constrs)) =>

    let val T = nth_dtyp i

    in map (fn (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 ---> T);

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

    end) descr;

*}

local_setup {*

snd o (Primrec.add_primrec

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

*}

print_theorems

ML {*

   val perm_empty_thms =

     let

       val gl =

         HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj

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

               (Const (s, @{typ perm} --> T --> T) $

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

                Free (x, T)))

            (perm_names ~~

             map body_type perm_types ~~ perm_indnames)));

       fun tac _ =

         EVERY [indtac induct perm_indnames 1,

           ALLGOALS (asm_full_simp_tac @{simpset})];

     in

       map Drule.export_without_context (List.take (split_conj_thm

         (Goal.prove_global @{theory} [] [] gl tac),

       length new_type_names))

     end

*}

ML {*

   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 (map Drule.export_without_context (split_conj_thm

        (Goal.prove_global @{theory} [] []

           (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj

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

                  let

                    val perm = Const (s, @{typ perm} --> T --> T);

                    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_names ~~

                 map body_type perm_types ~~ perm_indnames))))

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

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

         length new_type_names)

*}

instance

apply(tactic {*

 (Class.intro_classes_tac []) THEN

 (ALLGOALS (simp_tac (@{simpset} addsimps (perm_empty_thms @ perm_append_thms)))) *})

done

end