62   rbv5

    62   rbv5

    63 where

    63 where

    64   "rbv5 rLnil = {}"

    64   "rbv5 rLnil = {}"

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

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

    66 

    66 

    67 ML {*

    69 ML {*

    68 val thy1 = @{theory};

    70 val thy1 = @{theory};

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

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

    70 val number = 2;

    72 val number = 2;

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

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

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

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

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

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

    85 val induct = #induct info;

    87 val induct = #induct info;

    86 val inducts = #inducts info;

    88 val inducts = #inducts info;

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

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

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

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

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

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

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

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

    91 val lthy1 = Theory_Target.init NONE thy2

    95 val lthy1 = Theory_Target.init NONE thy2

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

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

    93 val alpha_ts_loc = #preds alpha

    97 val alpha_ts_loc = #preds alpha

    94 val alpha_intros = #intrs alpha

    98 val alpha_intros = #intrs alpha

    96 val alpha_induct_loc = #induct alpha

   100 val alpha_induct_loc = #induct alpha

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

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

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

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

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

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

   100 (*val alpha_inducts_loc = #inducts alpha

   105 (*val alpha_inducts_loc = #inducts alpha

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

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

   103 val alpha_inj = ProofContext.export lthy2 lthy1 alpha_inj_loc

   108 val alpha_inj = ProofContext.export lthy2 lthy1 alpha_inj_loc

   104 val fv_def = ProofContext.export lthy2 lthy1 fv_def_loc

   109 val fv_def = ProofContext.export lthy2 lthy1 fv_def_loc

   105 val morphism = ProofContext.export_morphism lthy2 lthy1

   110 val morphism = ProofContext.export_morphism lthy2 lthy1

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

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

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

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

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

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

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

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

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

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

   111 val alpha_eqvt = ProofContext.export lthy4 lthy1 alpha_eqvt_loc;

   116 val alpha_eqvt = ProofContext.export lthy4 lthy1 alpha_eqvt_loc;

   113 val alpha_equivp = ProofContext.export lthy4 lthy1 alpha_equivp_loc

   118 val alpha_equivp = ProofContext.export lthy4 lthy1 alpha_equivp_loc

   114 val lthy5 = define_quotient_type

   119 val lthy5 = define_quotient_type

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

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

   116   (ALLGOALS (resolve_tac alpha_equivp)) lthy4;

   121   (ALLGOALS (resolve_tac alpha_equivp)) lthy4;

   117 val consts =

   122 val consts =

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

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

   138   @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append}*)

   143   @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append}*)

   139 val lthy11 = Theory_Target.init NONE thy3;

   144 val lthy11 = Theory_Target.init NONE thy3;

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

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

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

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

   142 *}

   149 *}

   143 

   150 

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

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

   145 thm lift_induct

   152 thm lift_induct

   146 

   153 

   147 end

   155 end

   148 

   156