equal
deleted
inserted
replaced
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 defer |
250 defer |
250 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
251 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
251 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
252 apply(tactic {* clean_tac @{context} 1 *}) |
252 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
253 apply(simp add: prod_fun_def) (* Should be pair_prs *) |
253 apply(simp only: prod_rel.simps) |
|
254 defer |
|
255 apply(tactic {* clean_tac @{context} 1 *}) |
|
256 apply(simp add: prod_rel.simps) |
|
257 apply(tactic {* clean_tac @{context} 1 *}) |
|
258 apply(simp) |
|
259 (*apply(tactic {* regularize_tac @{context} 1 *}) |
|
260 apply(tactic {* inj_repabs_tac_intex @{context} 1*})*) |
|
261 sorry |
254 sorry |
262 |
255 |
263 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)" |
264 by simp |
257 by simp |
265 |
258 |