248 apply(tactic {* procedure_tac @{context} @{thm lam_tst} 1 *}) |
248 apply(tactic {* procedure_tac @{context} @{thm lam_tst} 1 *}) |
249 (*apply(tactic {* regularize_tac @{context} 1 *}) *) |
249 (*apply(tactic {* regularize_tac @{context} 1 *}) *) |
250 defer |
250 defer |
251 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
251 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
252 apply(tactic {* clean_tac @{context} 1 *}) |
252 apply(tactic {* clean_tac @{context} 1 *}) |
253 apply(simp add: prod_fun_def) (* Should be pair_prs *) |
253 apply(simp add: pair_prs) |
254 sorry |
254 sorry |
255 |
255 |
256 lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)" |
256 lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)" |
257 by simp |
257 by simp |
258 |
258 |
259 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
259 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
260 apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) |
260 apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) |
261 apply(tactic {* gen_frees_tac @{context} 1 *}) |
261 apply(tactic {* gen_frees_tac @{context} 1 *}) |
|
262 ML_prf {* regularize_trm @{context} (prop_of @{thm lam_tst2}) @{prop "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"} *} |
|
263 ML_prf {* print_depth 50 *} |
|
264 ML_prf {* Syntax.check_term @{context} it *} |
262 ML_prf {* procedure_inst @{context} (prop_of @{thm lam_tst2}) @{prop "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"} *} |
265 ML_prf {* procedure_inst @{context} (prop_of @{thm lam_tst2}) @{prop "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"} *} |
263 |
266 |
264 apply(tactic {* procedure_tac @{context} @{thm lam_tst2} 1 *}) |
267 apply(tactic {* procedure_tac @{context} @{thm lam_tst2} 1 *}) |
265 apply(tactic {* regularize_tac @{context} 1 *}) |
268 apply(tactic {* regularize_tac @{context} 1 *}) |
266 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
269 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |