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)

   256 

   257 

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

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

   258 by auto

   259 by auto

   259 

   260 

   260 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)"

   261 apply(lifting lam_tst3b)

   262 apply(lifting lam_tst3b)

   262 apply(rule impI)

   263 apply(rule impI)

   263 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]])

   264 apply(simp add: id_rsp)

   265 apply(simp add: id_rsp)

   266 

   268 

   267 term map

   269 term map

   268 

   270 

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

   270 apply (induct l)

   272 apply (induct l)