theory Lift
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp"
begin

atom_decl name
atom_decl ident

datatype rtrm2 =
  rVr2 "name"
| rAp2 "rtrm2" "rtrm2 list"
| rLt2 "ras" "rtrm2" --"bind (bv2 l) in (r)"
and ras =
  rAs "name" "rtrm2"

primrec rbv2 where "rbv2 (rAs x t) = {atom x}"


ML {*
fun build_eqvts_ funs perms simps induct ctxt =
let
  val pi = Free ("pi", @{typ perm});
  val types = map (domain_type o fastype_of) funs;
  val fv_indnames = Datatype_Prop.make_tnames (map body_type types);
  val args = map Free (fv_indnames ~~ types);
  val perm_at = Const (@{const_name permute}, @{typ "perm \<Rightarrow> atom set \<Rightarrow> atom set"})
  fun eqvtc (fv, (arg, perm)) =
    HOLogic.mk_eq ((perm_at $ pi $ (fv $ arg)), (fv $ (perm $ pi $ arg)))
  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms))))
  fun tac _ = (indtac induct fv_indnames THEN_ALL_NEW
    (asm_full_simp_tac (HOL_ss addsimps 
      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))) 1
in
  Goal.prove ctxt ("pi" :: fv_indnames) [] gl tac
end
*}


ML {*
print_depth 500;
val thy1 = @{theory};
val tnames = ["rtrm2", "ras"];
val ftname = "Lift.rtrm2"
val ntnames = [(@{binding trm2}, @{typ rtrm2}), (@{binding as}, @{typ ras})]
val binds = [[[[]], [[], []], [[], [(SOME @{term rbv2}, 0)]]], 
             [[[], []]]  (*, [[], [[], []]] *) ];
val bv_simps = @{thms rbv2.simps}
val info = Datatype.the_info @{theory} ftname;
*}

.
{*
val descr = #descr info;
val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
val full_tnames = List.take (all_full_tnames, length tnames);
val induct = #induct info;
val inducts = #inducts info;
val infos = map (Datatype.the_info @{theory}) all_full_tnames;
val inject = flat (map #inject infos);
val distinct = flat (map #distinct infos);
val ((raw_perm_def, raw_perm_simps, perms), thy2) = define_raw_perms tnames full_tnames thy1;
val lthy1 = Theory_Target.init NONE thy2
val (((fv_ts_loc, fv_def_loc), alpha), lthy2) = define_fv_alpha ftname binds lthy1;
val alpha_ts_loc = #preds alpha
val alpha_intros = #intrs alpha
val alpha_cases = #elims alpha
val alpha_induct = #induct alpha
val alpha_inj = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy2
val fv_def = ProofContext.export lthy2 lthy1 fv_def_loc
val morphism = ProofContext.export_morphism lthy2 lthy1
val fv_ts = map (Morphism.term morphism) fv_ts_loc
val alpha_ts = map (Morphism.term morphism) alpha_ts_loc
val (bv_eqvts, lthy3) = build_eqvts @{binding bv_eqvts} [@{term rbv2}] [hd (tl perms)] 
  (bv_simps @ raw_perm_def) @{thm rtrm2_ras.inducts(2)} lthy2;
val (fv_eqvts, lthy4) = build_eqvts @{binding fv_eqvts} fv_ts_loc perms (fv_def_loc @ raw_perm_def) induct lthy3;
val alpha_eqvt = build_alpha_eqvts alpha_ts_loc perms (raw_perm_def @ alpha_inj) alpha_induct lthy4;
val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct inject alpha_inj distinct alpha_cases alpha_eqvt lthy4;
val alpha_equivp = ProofContext.export lthy4 lthy1 alpha_equivp_loc
val lthy5 = define_quotient_type
  (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) (ntnames ~~ alpha_ts))
  (ALLGOALS (resolve_tac alpha_equivp)) lthy4;
val ((c, def), lthy6) = Quotient_Def.quotient_lift_const ("Vr2", @{term rVr2}) lthy5
*}

ML {*
val thyf = Local_Theory.exit_global lthy6;
*}
setup {* fn _ => thyf *}
print_theorems




ML {*
val lthy5 = define_quotient_type
  (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) (ntnames ~~ alpha_ts))
  (ALLGOALS (resolve_tac alpha_equivp)) lthy4
*}

ML {*

*}