equal
deleted
inserted
replaced
311 apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *}) |
311 apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *}) |
312 apply(rule impI) |
312 apply(rule impI) |
313 apply(rule lam_tst3a_reg) |
313 apply(rule lam_tst3a_reg) |
314 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
314 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
315 apply(tactic {* clean_tac @{context} 1 *}) |
315 apply(tactic {* clean_tac @{context} 1 *}) |
316 apply(simp add: babs_prs[OF Quotient_my_int Quotient_my_int]) |
316 apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int]) |
317 done |
317 done |
318 |
318 |
319 lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)" |
319 lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)" |
320 by auto |
320 by auto |
321 |
321 |
331 apply(tactic {* quotient_tac @{context} 1 *}) |
331 apply(tactic {* quotient_tac @{context} 1 *}) |
332 apply(subst babs_prs) |
332 apply(subst babs_prs) |
333 apply(tactic {* quotient_tac @{context} 1 *}) |
333 apply(tactic {* quotient_tac @{context} 1 *}) |
334 apply(tactic {* quotient_tac @{context} 1 *}) |
334 apply(tactic {* quotient_tac @{context} 1 *}) |
335 apply(rule refl) |
335 apply(rule refl) |
336 |
336 done |
|
337 |
|
338 term map |
|
339 |
|
340 lemma lam_tst4: "map (\<lambda>x. my_plus x (0,0)) l = l" |
|
341 apply (induct l) |
|
342 apply simp |
|
343 apply (case_tac a) |
|
344 apply simp |
|
345 done |
|
346 |
|
347 lemma "map (\<lambda>x. PLUS x ZERO) l = l" |
|
348 apply(tactic {* procedure_tac @{context} @{thm lam_tst4} 1 *}) |
|
349 apply(tactic {* regularize_tac @{context} 1 *}) |
|
350 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
|
351 apply(tactic {* clean_tac @{context} 1*}) |
|
352 apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int]) |
|
353 apply(simp only: map_prs[OF Quotient_my_int Quotient_my_int]) |
|
354 apply(tactic {* lambda_prs_tac @{context} 1 *}) |
|
355 apply(rule refl) |
|
356 done |
337 |
357 |
338 end |
358 end |