equal
deleted
inserted
replaced
250 |
250 |
251 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
251 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
252 apply(lifting lam_tst3a) |
252 apply(lifting lam_tst3a) |
253 apply(rule impI) |
253 apply(rule impI) |
254 apply(rule lam_tst3a_reg) |
254 apply(rule lam_tst3a_reg) |
255 (* INJECTION PROBLEM *) |
255 done |
256 oops |
|
257 |
256 |
258 lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)" |
257 lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)" |
259 by auto |
258 by auto |
260 |
259 |
261 lemma "(\<lambda>(y :: my_int => my_int). y) = (\<lambda>(x :: my_int => my_int). x)" |
260 lemma "(\<lambda>(y :: my_int => my_int). y) = (\<lambda>(x :: my_int => my_int). x)" |
262 apply(lifting lam_tst3b) |
261 apply(lifting lam_tst3b) |
263 apply(rule impI) |
262 apply(rule impI) |
264 apply(rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]]) |
263 apply(rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]]) |
265 apply(simp add: id_rsp) |
264 apply(simp add: id_rsp) |
266 (* INJECTION PROBLEM --- possibly now id_def is part of id_simps again *) |
265 done |
267 oops |
|
268 |
|
269 term map |
|
270 |
266 |
271 lemma lam_tst4: "map (\<lambda>x. my_plus x (0,0)) l = l" |
267 lemma lam_tst4: "map (\<lambda>x. my_plus x (0,0)) l = l" |
272 apply (induct l) |
268 apply (induct l) |
273 apply simp |
269 apply simp |
274 apply (case_tac a) |
270 apply (case_tac a) |