theory Perm
imports "../Nominal-General/Nominal2_Atoms"
begin

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 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 [
      Datatype_Aux.indtac induct perm_indnames 1,
      ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_zero} :: perm_def)))
    ];
in
  Datatype_Aux.split_conj_thm (Goal.prove lthy perm_indnames [] gl tac)
end;
*}

ML {*
fun prove_perm_append lthy induct perm_def perm_frees =
let
  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 $ (mk_plus pi1 pi2) $ Free (x, T),
      perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
  val goal =
    (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
      (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames))))
  fun tac _ =
    EVERY [
      Datatype_Aux.indtac induct perm_indnames 1,
      ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_plus} :: perm_def)))
    ]
in
  Datatype_Aux.split_conj_thm (Goal.prove lthy ("pi1" :: "pi2" :: perm_indnames) [] goal tac)
end;
*}


(* definitions of the permute function for a raw nominal datatype *)

ML {*
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 non-recursive it returns 

         p o arg

    - in case the argument is recursive it will build

         %x1..xn. permute_fn p (arg (-p o x1)..(-p o xn))

      the x1..xn depend whether the argument is of function
      type; normally it just returns permute_fn pi arg 
*)
fun perm_arg permute_fns pi (arg_dty, arg) =
  if Datatype_Aux.is_rec_type arg_dty 
  then 
    let 
      val T = type_of arg
      val (Us, _) = strip_type T
      val indxs_tys = (length Us - 1 downto 0) ~~ Us
      val permute_fn = Free (nth permute_fns (Datatype_Aux.body_index arg_dty))
    in 
      list_abs (map (pair "x") Us, permute_fn $ pi $ 
        list_comb (arg, map (fn (i, U) => (mk_perm_ty U (mk_minus pi) (Bound i))) indxs_tys))
    end
  else mk_perm pi arg
*}

ML {*
(* equation for permutation function for one constructor *)
fun perm_eq_constr thy 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 {*
(* defines the permutation functions for raw datatypes and
   proves that they are instances of pt
*)
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_fn_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
    "permute_" ^ Datatype_Aux.name_of_typ (nth_dtyp dt_descr sorts i)) dt_descr);

  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 thy 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_frees, perm_ldef), lthy') =
    Primrec.add_primrec
      (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy;
    
  val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, dt_nos);
  val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, dt_nos)
  val perms_name = space_implode "_" perm_fn_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
*}

(* Test *)
(*atom_decl name

datatype trm =
  Var "name"
| App "trm" "trm 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
*)

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"
| Lam "name" "trm"
| Let "bp" "trm" "trm"
and bp =
  BUnit
| BVar "name"
| BPair "bp" "bp"

setup {* fn thy =>
let 
  val inf = Datatype.the_info thy "Perm.trm"
in
  define_raw_perms inf 2 thy |> snd
end
*}

print_theorems
*)

end