equal
deleted
inserted
replaced
254 |
254 |
255 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)" |
256 by simp |
256 by simp |
257 |
257 |
258 |
258 |
259 |
|
260 |
|
261 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
259 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
262 apply(tactic {* procedure_tac @{context} @{thm lam_tst2} 1 *}) |
260 apply(tactic {* procedure_tac @{context} @{thm lam_tst2} 1 *}) |
263 defer |
261 defer |
264 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
262 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
265 (*apply(tactic {* lambda_prs_tac @{context} 1 *})*) |
263 apply(tactic {* clean_tac @{context} 1 *}) |
266 sorry |
264 sorry |
267 |
265 |
268 lemma lam_tst3: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)" |
266 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 |
267 by auto |
270 |
268 |
271 lemma "(\<lambda>(y :: my_int \<Rightarrow> my_int). y) = (\<lambda>(x :: my_int \<Rightarrow> my_int). x)" |
269 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 *}) |
270 apply(tactic {* procedure_tac @{context} @{thm lam_tst3} 1 *}) |
273 defer |
271 defer |
274 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
272 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
275 apply(tactic {* lambda_prs_tac @{context} 1 *}) |
273 apply(tactic {* clean_tac @{context} 1 *}) |
276 sorry |
274 sorry |