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 {*
fun prove_perm_empty lthy induct perm_def perm_frees =
let
  val perm_types = map fastype_of perm_frees;
  val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
  fun glc ((perm, T), x) =
    HOLogic.mk_eq (perm $ @{term "0 :: perm"} $ Free (x, T), Free (x, T))
  val gl =
    HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
      (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames)));
  fun tac _ =
    EVERY [
      indtac induct perm_indnames 1,
      ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_zero} :: perm_def)))
    ];
in
  split_conj_thm (Goal.prove lthy perm_indnames [] gl tac)
end;
*}

ML {*
fun prove_perm_append lthy induct perm_def perm_frees =
let
  val add_perm = @{term "op + :: (perm \<Rightarrow> perm \<Rightarrow> perm)"}
  val pi1 = Free ("pi1", @{typ perm});
  val pi2 = Free ("pi2", @{typ perm});
  val perm_types = map fastype_of perm_frees
  val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
  fun glc ((perm, T), x) =
    HOLogic.mk_eq (
      perm $ (add_perm $ pi1 $ pi2) $ Free (x, T),
      perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
  val gl =
    (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
      (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames))))
  fun tac _ =
    EVERY [
      indtac induct perm_indnames 1,
      ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_plus} :: perm_def)))
    ]
in
  split_conj_thm (Goal.prove lthy ("pi1" :: "pi2" :: perm_indnames) [] gl tac)
end;
*}

ML {*
fun define_raw_perms (dt_info : info) number thy =
let
  val {descr, induct, sorts, ...} = dt_info;
  val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
  val full_tnames = List.take (all_full_tnames, number);
  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_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;
    val ((perm_frees, perm_ldef), lthy') =
      Primrec.add_primrec
        (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy;
    val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, number);
    val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, number)
    val perms_name = space_implode "_" perm_names'
    val perms_zero_bind = Binding.name (perms_name ^ "_zero")
    val perms_append_bind = Binding.name (perms_name ^ "_append")
    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_empty_thms))
  |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms))
  |> Class_Target.prove_instantiation_exit_result morphism tac (perm_ldef, (perm_empty_thms @ perm_append_thms), perm_frees)
  end

*}

ML {*
fun define_lifted_perms full_tnames name_term_pairs thms thy =
let
  val lthy =
    Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
  val lthy' = fold (snd oo Quotient_Def.quotient_lift_const) name_term_pairs lthy
  val lifted_thms = map (fn x => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy', x))) 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 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