108 ML {*

   108 

   109 fun lifted ctxt qtys rthm =

   109 ML {*

   110 let

   110   val _ = timeit (fn () => map (lift_thm @{context} qtys []) @{thms distinct})

   111   (* When the theorem is atomized, eta redexes are contracted,

   112      so we do it both in the original theorem *)

   113   val rthm' = Drule.eta_contraction_rule rthm

   114   val ((_, [rthm'']), ctxt') = Variable.import false [rthm'] ctxt

   115   val goal = Quotient_Term.derive_qtrm ctxt' qtys (prop_of rthm'')

   116 in

   117   Goal.prove ctxt' [] [] goal (K (Quotient_Tacs.lift_tac ctxt' [rthm'] 1))

   118   |> singleton (ProofContext.export ctxt' ctxt)

   119 end

   120 *}

   121 

   122 ML {*

   123 fun lifted2 ctxt qtys rthms =

   124 let

   125   (* When the theorem is atomized, eta redexes are contracted,

   126      so we do it both in the original theorem *)

   127   val rthms' = map Drule.eta_contraction_rule rthms

   128   val ((_, rthms''), ctxt') = Variable.import false rthms' ctxt

   129   val goals = map (Quotient_Term.derive_qtrm ctxt' qtys o prop_of) rthms''

   130 in

   131   Goal.prove_multi ctxt' [] [] goals (K (Quotient_Tacs.lift_tac ctxt' rthms' 1))

   132   |> ProofContext.export ctxt' ctxt

   133 end

   134 *}

   135 

   136 ML {*

   137   val _ = timeit (fn () => map (lifted @{context} qtys) @{thms distinct})

   138 *}

   139 

   140 ML {*

   141   val _ = timeit (fn () => lifted2 @{context} qtys @{thms distinct})

   146   val thms_i = map (lift_thm @{context} qtys) @{thms tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.inducts}

   115   val _ = timeit (fn () => map (lift_thm @{context} qtys []) @{thms tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.induct})

   147 *}

   116 *}

   148 

   117 

   149 ML {*

   118 ML {*

   150   val thms_f = map (lift_thm @{context} qtys) @{thms fv_defs}

   119   val thms_f = map (lift_thm @{context} qtys []) @{thms fv_defs}

   154   val thms_i = map (lift_thm @{context} qtys) @{thms tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.size(50 - 98)}

   123   val thms_i = map (lift_thm @{context} qtys []) @{thms tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.size(50 - 98)}

   155 *}

   124 *}

   156 

   125 

   157 ML {*

   126 ML {*

   158   val thms_p = map (lift_thm @{context} qtys) @{thms perm_simps}

   127   val thms_p = map (lift_thm @{context} qtys []) @{thms perm_simps}

   159 *}

   128 *}

   160 

   129 

   161 ML {*

   130 ML {*

   162   val thms_f = map (lift_thm @{context} qtys) @{thms perm_laws}

   131   val thms_f = map (lift_thm @{context} qtys []) @{thms perm_laws}

   163 *}

   132 *}

   164 

   133 

   165 ML {*

   134 ML {*

   166  val thms_e = map (lift_thm @{context} qtys) 

   135   val simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps

   167    @{thms eq_iff[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps

   136     prod.cases}

   168     prod.cases]}

   137 *}

   169 *}

   138 

   170 

   139 ML {*

   171 ML {*

   140  val thms_e = map (lift_thm @{context} qtys simps) @{thms eq_iff}

   172   val thms_f = map (lift_thm @{context} qtys) @{thms bn_defs}

   141 *}

   173 *}

   142 

   174 

   143 ML {*

   175 ML {*

   144   val thms_f = map (lift_thm @{context} qtys []) @{thms bn_defs}

   176   val thms_f = map (lift_thm @{context} qtys) @{thms bn_eqvt}

   145 *}

   177 *}

   146 

   178 

   147 ML {*

   179 ML {*

   148   val thms_f = map (lift_thm @{context} qtys []) @{thms bn_eqvt}

   180   val thms_f = map (lift_thm @{context} qtys) @{thms fv_eqvt}

   149 *}

   181 *}

   150 

   182 

   151 ML {*

   183 ML {*

   152   val thms_f = map (lift_thm @{context} qtys []) @{thms fv_eqvt}

   184   val thms_f = map (lift_thm @{context} qtys) @{thms size_eqvt}

   153 *}

   154 

   155 ML {*

   156   val thms_f = map (lift_thm @{context} qtys []) @{thms size_eqvt}