imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"

| rAp2 "rtrm2" "rtrm2"

ML {*

val thy1 = @{theory};

val info = Datatype.the_info @{theory} "Lift.rtrm2"

val number = 2; (* Number of defined types, rest are unfoldings *)

val binds = [[[[]], [[], []], [[], [(SOME @{term rbv2}, 0)]]],

             [[[], []]]  (*, [[], [[], []]] *) ];

val bvs = [(@{term rbv2}, 1)] (* Which type it operates on *)

val bv_simps = @{thms rbv2.simps}

val ntnames = [@{binding trm2}, @{binding as}]

val ncnames = ["Vr2", "Ap2", "Lt2", "As"]

val sorts = #sorts info;

val nos = map fst descr

val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) nos

val typs = List.take (all_typs, number)

val full_tnames = List.take (all_full_tnames, number);

val infos = map (Datatype.the_info thy1) all_full_tnames;

val ((raw_perm_def, raw_perm_simps, perms), thy2) = define_raw_perms info number thy1;

val (((fv_ts_loc, fv_def_loc), alpha), lthy2) = define_fv_alpha info binds lthy1;

val alpha_induct_loc = #induct alpha

val [alpha_induct] = ProofContext.export lthy2 lthy1 [alpha_induct_loc]

(* TODO replace when inducts is provided by the 2 lines below: *)

val alpha_inducts = Project_Rule.projects lthy2 (1 upto number) alpha_induct

(*val alpha_inducts_loc = #inducts alpha

val alpha_inducts = ProofContext.export lthy2 lthy1 alpha_inducts_loc*)

val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy2

val alpha_inj = ProofContext.export lthy2 lthy1 alpha_inj_loc

fun build_bv_eqvt (t, n) =

  build_eqvts Binding.empty [t] [nth perms n]

    (bv_simps @ raw_perm_def) (nth inducts n)

val (bv_eqvts, lthy3) = fold_map build_bv_eqvt bvs lthy2;

val (fv_eqvts, lthy4) = build_eqvts Binding.empty fv_ts_loc perms (fv_def_loc @ raw_perm_def) induct lthy3;

val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy4;

val alpha_eqvt = ProofContext.export lthy4 lthy1 alpha_eqvt_loc

val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy4;

  (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((ntnames ~~ typs) ~~ alpha_ts))

val consts =

  flat (map (fn (i, (_, _, l)) =>

    map (fn (cname, dts) =>

      Const (cname, map (typ_of_dtyp descr sorts) dts --->

        typ_of_dtyp descr sorts (DtRec i))) l) descr);

val (csdefl, lthy6) = fold_map Quotient_Def.quotient_lift_const (ncnames ~~ consts) lthy5;

val (cs, def) = split_list csdefl;

val ((_, fv_rsp), lthy7) = prove_const_rsp Binding.empty fv_ts

  (fn _ => fvbv_rsp_tac alpha_induct fv_def 1) lthy6

val (bvs_rsp', lthy8) = fold_map (

  fn (bv_t, i) => prove_const_rsp Binding.empty [bv_t]

    (fn _ => fvbv_rsp_tac (nth alpha_inducts i) bv_simps 1)) bvs lthy7

val bvs_rsp = flat (map snd bvs_rsp')

val (const_rsps, lthy9) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]

  (fn _ => constr_rsp_tac alpha_inj (fv_rsp @ bvs_rsp) alpha_equivp 1)) consts lthy8

val (perms_rsp, lthy10) = prove_const_rsp Binding.empty perms

  (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy9;

val lift_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy1, induct));

val lthy11 = snd (Local_Theory.note ((@{binding lift_induct}, []), [lift_induct]) lthy10)

setup {* fn _ => Local_Theory.exit_global lthy11 *}

thm lift_induct

end