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

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

    17 val thy1 = @{theory};

     6 fun lift_thm ctxt thm =

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

     7 let

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

     8   fun un_raw name = unprefix "_raw" name handle Fail _ => name

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

     9   fun add_under names = hd names :: (map (prefix "_") (tl names))

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

    10   fun un_raws name = implode (map un_raw (add_under (space_explode "_" name)))

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

    11   val un_raw_names = rename_vars un_raws

    23 val bv_simps = @{thms rbv2.simps}

    12 in

    24 

    13   un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm)))

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

    14 end

    26 val ncnames = ["Vr2", "Ap2", "Lt2", "As"] *} *)

    15 *}

    27 

    28 (*datatype rkind =

    29     Type

    30   | KPi "rty" "name" "rkind"

    31 and rty =

    32     TConst "ident"

    33   | TApp "rty" "rtrm"

    34   | TPi "rty" "name" "rty"

    35 and rtrm =

    36     Const "ident"

    37   | Var "name"

    38   | App "rtrm" "rtrm"

    39   | Lam "rty" "name" "rtrm"

    40 ML {*

    41 val thy1 = @{theory};

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

    43 val number = 3;

    44 val binds = [[ [], [(NONE, 1, 2)]],

    45    [ [], [], [(NONE, 1, 2)] ],

    46    [ [], [], [], [(NONE, 1, 2)]]];

    47 val bvs = []

    48 val bv_simps = []

    49 

    50 val ntnames = [@{binding kind}, @{binding ty}, @{binding trm}]

    51 val ncnames = ["TYP", "KPI", "TCONST", "TAPP", "TPI", "CONST", "VAR", "APP", "LAM"]*}*)

    52 

    53 datatype rtrm5 =

    54   rVr5 "name"

    55 | rAp5 "rtrm5" "rtrm5"

    56 | rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"

    57 and rlts =

    58   rLnil

    59 | rLcons "name" "rtrm5" "rlts"

    60 

    61 primrec

    62   rbv5

    63 where

    64   "rbv5 rLnil = {}"

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

    66 

    67 

    70 val thy1 = @{theory};

    18 fun quotient_lift_consts_export spec ctxt =

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

    19 let

    72 val number = 2;

    20   val (result, ctxt') = fold_map Quotient_Def.quotient_lift_const spec ctxt;

    73 val binds = [ [[], [], [(SOME @{term rbv5}, 0, 1)]], [[], []]  ]

    21   val (ts_loc, defs_loc) = split_list result;

    74 val bvs = [(@{term rbv5}, 1)]

    22   val morphism = ProofContext.export_morphism ctxt' ctxt;

    75 val bv_simps = @{thms rbv5.simps}

    23   val ts = map (Morphism.term morphism) ts_loc

    76 

    24   val defs = Morphism.fact morphism defs_loc

    77 val ntnames = [@{binding trm5}, @{binding lts}]

    25 in

    78 val ncnames = ["Vr5", "Ap5", "Lt5", "Lnil", "Lcons"]

    26   (ts, defs, ctxt')

    79 

    27 end

    80 

    81 val descr = #descr info;

    82 val sorts = #sorts info;

    83 val nos = map fst descr

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

    85 val typs = List.take (all_typs, number)

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

    87 val induct = #induct info;

    88 val inducts = #inducts info;

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

    90 val rel_infos = List.take (infos, number);

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

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

    93 val rel_distinct = map #distinct rel_infos;

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

    95 val lthy1 = Theory_Target.init NONE thy2

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

    97 val alpha_ts_loc = #preds alpha

    98 val alpha_intros = #intrs alpha

    99 val alpha_cases_loc = #elims alpha

   100 val alpha_induct_loc = #induct alpha

   101 val alpha_cases = ProofContext.export lthy2 lthy1 alpha_cases_loc

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

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

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

   105 (*val alpha_inducts_loc = #inducts alpha

   106 val alpha_inducts = ProofContext.export lthy2 lthy1 alpha_inducts_loc*)

   107 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy2

   108 val alpha_inj = ProofContext.export lthy2 lthy1 alpha_inj_loc

   109 val fv_def = ProofContext.export lthy2 lthy1 fv_def_loc

   110 val morphism = ProofContext.export_morphism lthy2 lthy1

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

   112 val alpha_ts = map (Morphism.term morphism) alpha_ts_loc

   113 val (bv_eqvts, lthy3) = fold_map (build_bv_eqvt perms (bv_simps @ raw_perm_def) inducts)  bvs lthy2;

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

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

   116 val alpha_eqvt = ProofContext.export lthy4 lthy1 alpha_eqvt_loc;

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

   118 val alpha_equivp = ProofContext.export lthy4 lthy1 alpha_equivp_loc

   119 val lthy5 = define_quotient_type

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

   121   (ALLGOALS (resolve_tac alpha_equivp)) lthy4;

   122 val consts =

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

   124     map (fn (cname, dts) =>

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

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

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

   128 val (cs, def) = split_list csdefl;

   129 val (bvs_rsp', lthy7) = fold_map (

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

   131     (fn _ => fvbv_rsp_tac (nth alpha_inducts i) bv_simps 1)) bvs lthy6;

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

   133   (fn _ => fvbv_rsp_tac alpha_induct fv_def 1) lthy7;

   134 val bvs_rsp = flat (map snd bvs_rsp');

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

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

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

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

   139 val thy3 = Local_Theory.exit_global lthy10;

   140 (* TODO: fix this hack... *)

   141 (*val tinfo = #abs_type (Typedef.the_info thy3 "Lift.trm5");*)

   142 (*val thy4 = define_lifted_perms ["Term1.trm1"] [("permute_trm1", @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"})]

   143   @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append}*)

   144 val lthy11 = Theory_Target.init NONE thy3;

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

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

   147 val rel_dists = flat (map (distinct_rel lthy12 alpha_cases) (rel_distinct ~~ (List.take (alpha_ts, number))))

   148