248 

   248 

   249 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"

   249 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"

   250 apply(lifting lam_tst3a)

   250 apply(lifting lam_tst3a)

   251 apply(rule impI)

   251 apply(rule impI)

   252 apply(rule lam_tst3a_reg)

   252 apply(rule lam_tst3a_reg)

   257 

   254 

   258 lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)"

   255 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

   256 by auto

   260 

   257 

   261 lemma "(\<lambda>(y :: my_int => my_int). y) = (\<lambda>(x :: my_int => my_int). x)"

   258 lemma "(\<lambda>(y :: my_int => my_int). y) = (\<lambda>(x :: my_int => my_int). x)"

   262 apply(lifting lam_tst3b)

   259 apply(lifting lam_tst3b)

   263 apply(rule impI)

   260 apply(rule impI)

   264 apply(rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]])

   261 apply(rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]])

   265 apply(simp add: id_rsp)

   262 apply(simp add: id_rsp)

   270 

   264 

   271 term map

   265 term map

   272 

   266 

   273 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"

   274 apply (induct l)

   268 apply (induct l)