1 theory Lift

     2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp"

     3 begin

     4 

     5 atom_decl name

     6 atom_decl ident

     7 

     8 datatype rtrm2 =

     9   rVr2 "name"

    10 | rAp2 "rtrm2" "rtrm2"

    11 | rLt2 "ras" "rtrm2" --"bind (bv2 l) in (r)"

    12 and ras =

    13   rAs "name" "rtrm2"

    14 

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

    16 

    17 

    18 ML {*

    19 fun build_eqvts_ funs perms simps induct ctxt =

    20 let

    21   val pi = Free ("pi", @{typ perm});

    22   val types = map (domain_type o fastype_of) funs;

    23   val fv_indnames = Datatype_Prop.make_tnames (map body_type types);

    24   val args = map Free (fv_indnames ~~ types);

    25   val perm_at = Const (@{const_name permute}, @{typ "perm \<Rightarrow> atom set \<Rightarrow> atom set"})

    26   fun eqvtc (fv, (arg, perm)) =

    27     HOLogic.mk_eq ((perm_at $ pi $ (fv $ arg)), (fv $ (perm $ pi $ arg)))

    28   val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms))))

    29   fun tac _ = (indtac induct fv_indnames THEN_ALL_NEW

    30     (asm_full_simp_tac (HOL_ss addsimps 

    31       (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))) 1

    32 in

    33   Goal.prove ctxt ("pi" :: fv_indnames) [] gl tac

    34 end

    35 *}

    36 

    37 

    38 ML {*

    39 print_depth 500;

    40 val thy1 = @{theory};

    41 val tnames = ["rtrm2", "ras"];

    42 val ftname = "Lift.rtrm2"

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

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

    45 val bv_simps = @{thms rbv2.simps}

    46 val info = Datatype.the_info @{theory} ftname;

    47 val descr = #descr info;

    48 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;

    49 val full_tnames = List.take (all_full_tnames, length tnames);

    50 val induct = #induct info;

    51 val inducts = #inducts info;

    52 val infos = map (Datatype.the_info @{theory}) all_full_tnames;

    53 val inject = flat (map #inject infos);

    54 val distinct = flat (map #distinct infos);

    55 val ((raw_perm_def, raw_perm_simps, perms), thy2) = define_raw_perms tnames full_tnames thy1;

    56 val lthy1 = Theory_Target.init NONE thy2

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

    58 val alpha_ts = #preds alpha

    59 val alpha_intros = #intrs alpha

    60 val alpha_cases = #elims alpha

    61 val alpha_induct = #induct alpha

    62 val alpha_inj = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy2

    63 val fv_def = ProofContext.export lthy2 lthy1 fv_def_loc

    64 val morphism = ProofContext.export_morphism lthy2 lthy1

    65 val fv_ts = map (Morphism.term morphism) fv_ts_loc

    66 val (bv_eqvts, lthy3) = build_eqvts @{binding bv_eqvts} [@{term rbv2}] [hd (tl perms)] 

    67   (bv_simps @ raw_perm_def) @{thm rtrm2_ras.inducts(2)} lthy2;

    68 val (fv_eqvts, lthy4) = build_eqvts @{binding fv_eqvts} fv_ts_loc perms (fv_def_loc @ raw_perm_def) induct lthy3;

    69 val alpha_eqvt = build_alpha_eqvts alpha_ts perms (raw_perm_def @ alpha_inj) alpha_induct lthy4;

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

    71 

    72 *}

    73 

    74 

    75 

    76 ML {*

    77   val thyf = Local_Theory.exit_global lthy4

    78 *}

    79 setup {* fn _ => thyf *}

    80 print_theorems

    81 

    82 ML {*

    83 (*val thyn = @{theory}

    84 val lthy3 = Theory_Target.init NONE thyn;*)

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

    86 

    87 *}

    88 

    89