equal
deleted
inserted
replaced
261 lemma "(\<lambda>(y :: my_int => my_int). y) = (\<lambda>(x :: my_int => my_int). x)" |
261 lemma "(\<lambda>(y :: my_int => my_int). y) = (\<lambda>(x :: my_int => my_int). x)" |
262 apply(lifting lam_tst3b) |
262 apply(lifting lam_tst3b) |
263 apply(rule impI) |
263 apply(rule impI) |
264 apply(rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]]) |
264 apply(rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]]) |
265 apply(simp add: id_rsp) |
265 apply(simp add: id_rsp) |
266 (* INJECTION PROBLEM *) |
266 (* INJECTION PROBLEM --- possibly now id_def is part of id_simps again *) |
267 oops |
267 oops |
268 |
268 |
269 term map |
269 term map |
270 |
270 |
271 lemma lam_tst4: "map (\<lambda>x. my_plus x (0,0)) l = l" |
271 lemma lam_tst4: "map (\<lambda>x. my_plus x (0,0)) l = l" |