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

atom_decl name
atom_decl ident

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

primrec rbv2 where "rbv2 (rAs x t) = {atom x}"
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"] *} *)

(* datatype rkind =
    Type
  | KPi "rty" "name" "rkind"
and rty =
    TConst "ident"
  | TApp "rty" "rtrm"
  | TPi "rty" "name" "rty"
and rtrm =
    Const "ident"
  | Var "name"
  | App "rtrm" "rtrm"
  | Lam "rty" "name" "rtrm"
ML {*
val thy1 = @{theory};
val info = Datatype.the_info @{theory} "Lift.rkind"
val number = 3;
val binds =  [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ],
   [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ],
   [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]];
val bvs = []
val bv_simps = []

val ntnames = [@{binding kind}, @{binding ty}, @{binding trm}]
val ncnames = ["TYP", "KPI", "TCONST", "TAPP", "TPI", "CONST", "VAR", "APP", "LAM"]*} *)

datatype rtrm5 =
  rVr5 "name"
| rAp5 "rtrm5" "rtrm5"
| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"
and rlts =
  rLnil
| rLcons "name" "rtrm5" "rlts"

primrec
  rbv5
where
  "rbv5 rLnil = {}"
| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"

ML Typedef.add_typedef

ML {*
val thy1 = @{theory};
val info = Datatype.the_info @{theory} "Lift.rtrm5"
val number = 2;
val binds = [ [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]]  ]
val bvs = [(@{term rbv5}, 1)]
val bv_simps = @{thms rbv5.simps}

val ntnames = [@{binding trm5}, @{binding lts}]
val ncnames = ["Vr5", "Ap5", "Lt5", "Lnil", "Lcons"]

val descr = #descr info;
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 all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
val full_tnames = List.take (all_full_tnames, number);
val induct = #induct info;
val inducts = #inducts info;
val infos = map (Datatype.the_info thy1) 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 info number thy1;
val lthy1 = Theory_Target.init NONE thy2
val (((fv_ts_loc, fv_def_loc), alpha), lthy2) = define_fv_alpha info binds lthy1;
val alpha_ts_loc = #preds alpha
val alpha_intros = #intrs alpha
val alpha_cases = #elims alpha
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
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
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;
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 ~~ typs) ~~ alpha_ts))
  (ALLGOALS (resolve_tac alpha_equivp)) lthy4;
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 thy3 = Local_Theory.exit_global lthy10;
(* TODO: fix this hack... *)
val tinfo = #abs_type (Typedef.the_info thy3 "Lift.trm5");
(*val thy4 = define_lifted_perms ["Term1.trm1"] [("permute_trm1", @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"})]
  @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append}*)
val lthy11 = Theory_Target.init NONE thy3;
val lift_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy11, induct));
val lthy12 = snd (Local_Theory.note ((@{binding lift_induct}, []), [lift_induct]) lthy11);
*}

setup {* fn _ => Local_Theory.exit_global lthy12 *}
thm lift_induct

end