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