260 lemma ho_tst3: "foldl f (s::nat \<times> nat) ([]::(nat \<times> nat) list) = s"

   261 by simp

   262 

   263 lemma "foldl f (x::my_int) ([]::my_int list) = x"

   264 apply(tactic {* procedure_tac @{context} @{thm ho_tst3} 1 *})

   265 apply(tactic {* regularize_tac @{context} 1 *})

   266 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})

   267 (* TODO: does not work when this is added *)

   268 (* apply(tactic {* lambda_prs_tac @{context} 1 *})*)

   269 apply(tactic {* clean_tac @{context} 1 *})

   270 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])

   271 done

   272 

   273 lemma lam_tst: "(\<lambda>x. (x, x)) y = (y, (y :: nat \<times> nat))"

   274 by simp

   275 

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

   277 apply(tactic {* procedure_tac @{context} @{thm lam_tst} 1 *})

   278 defer

   279 apply(tactic {* inj_repabs_tac_intex @{context} 1*})

   280 apply(tactic {* inj_repabs_tac_intex @{context} 1*})

   281 apply(tactic {* inj_repabs_tac_intex @{context} 1*})

   282 apply(simp only: prod_rel.simps)

   283 defer

   284 apply(tactic {* clean_tac @{context} 1 *})

   285 apply(simp add: prod_rel.simps)

   286 apply(tactic {* clean_tac @{context} 1 *})

   287 apply(simp)

   288 (*apply(tactic {* regularize_tac @{context} 1 *})

   289 apply(tactic {* inj_repabs_tac_intex @{context} 1*})*)

   290 sorry

   291 

   292 lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"

   293 by simp

   294 

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

   296 apply(tactic {* ObjectLogic.full_atomize_tac 1 *})

   297 apply(tactic {* gen_frees_tac @{context} 1 *})

   298 ML_prf {* procedure_inst @{context} (prop_of @{thm lam_tst2}) @{prop "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"} *}

   299 

   300 apply(tactic {* procedure_tac @{context} @{thm lam_tst2} 1 *})

   301 apply(tactic {* regularize_tac @{context} 1 *})

   302 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})

   303 apply(tactic {* clean_tac @{context} 1 *})

   304 done

   305