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"

| 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 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 = #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 (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 perms (raw_perm_def @ alpha_inj) alpha_induct lthy4;

val alpha_equivp = build_equivps alpha_ts induct alpha_induct inject alpha_inj distinct alpha_cases alpha_eqvt lthy4

*}

ML {*

  val thyf = Local_Theory.exit_global lthy4

*}

setup {* fn _ => thyf *}

print_theorems

ML {*

(*val thyn = @{theory}

val lthy3 = Theory_Target.init NONE thyn;*)

build_equivps alpha_ts induct alpha_induct inject alpha_inj distinct alpha_cases @{thms alpha2_eqvt} lthy2

*}