247 

   247 

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

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

   249 apply(lifting lam_tst3a)

   249 apply(lifting lam_tst3a)

   250 apply(rule impI)

   250 apply(rule impI)

   251 apply(rule lam_tst3a_reg)

   251 apply(rule lam_tst3a_reg)

   253 

   256 

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

   255 by auto

   258 by auto

   256 

   259 

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

   258 apply(lifting lam_tst3b)

   261 apply(lifting lam_tst3b)

   259 apply(rule impI)

   262 apply(rule impI)

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

   261 apply(simp add: id_rsp)

   264 apply(simp add: id_rsp)

   263 

   269 

   264 term map

   270 term map

   265 

   271 

   266 lemma lam_tst4: "map (\<lambda>x. my_plus x (0,0)) l = l"

   272 lemma lam_tst4: "map (\<lambda>x. my_plus x (0,0)) l = l"

   267 apply (induct l)

   273 apply (induct l)