244 lemma lam_tst: "(\<lambda>x. (x, x)) y = (y, (y :: nat \<times> nat))" |
244 lemma lam_tst: "(\<lambda>x. (x, x)) y = (y, (y :: nat \<times> nat))" |
245 by simp |
245 by simp |
246 |
246 |
247 lemma "(\<lambda>x. (x, x)) (y::my_int) = (y, y)" |
247 lemma "(\<lambda>x. (x, x)) (y::my_int) = (y, y)" |
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 |
|
251 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
250 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
252 apply(tactic {* clean_tac @{context} 1 *}) |
251 apply(tactic {* clean_tac @{context} 1 *}) |
253 apply(simp add: pair_prs) |
252 apply(simp add: pair_prs) |
254 sorry |
253 done |
255 |
254 |
256 lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)" |
255 lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)" |
257 by simp |
256 by simp |
258 |
257 |
|
258 |
|
259 |
|
260 |
259 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
261 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
260 apply(tactic {* ObjectLogic.full_atomize_tac 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 *} |
|
265 ML_prf {* procedure_inst @{context} (prop_of @{thm lam_tst2}) @{prop "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"} *} |
|
266 |
|
267 apply(tactic {* procedure_tac @{context} @{thm lam_tst2} 1 *}) |
262 apply(tactic {* procedure_tac @{context} @{thm lam_tst2} 1 *}) |
268 apply(tactic {* regularize_tac @{context} 1 *}) |
263 defer |
269 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
264 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
270 apply(tactic {* clean_tac @{context} 1 *}) |
265 (*apply(tactic {* lambda_prs_tac @{context} 1 *})*) |
271 done |
266 sorry |
272 |
267 |
|
268 lemma lam_tst3: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)" |
|
269 by auto |
|
270 |
|
271 lemma "(\<lambda>(y :: my_int \<Rightarrow> my_int). y) = (\<lambda>(x :: my_int \<Rightarrow> my_int). x)" |
|
272 apply(tactic {* procedure_tac @{context} @{thm lam_tst3} 1 *}) |
|
273 defer |
|
274 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
|
275 apply(tactic {* lambda_prs_tac @{context} 1 *}) |
|
276 sorry |