# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260273683 -3600
# Node ID 5d6a2b5fb222442be41ee891e756cf58d15afbab
# Parent  c4299ce27e46318e59e5d57c32b907747c050e1e
Another lambda example theorem proved. Seems it starts working properly.

diff -r c4299ce27e46 -r 5d6a2b5fb222 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Tue Dec 08 13:00:36 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Tue Dec 08 13:01:23 2009 +0100
@@ -313,7 +313,7 @@
 apply(rule lam_tst3a_reg)
 apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac  @{context} 1 *})
-apply(simp add: babs_prs[OF Quotient_my_int Quotient_my_int])
+apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int])
 done
 
 lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)"
@@ -333,6 +333,26 @@
 apply(tactic {* quotient_tac @{context} 1 *})
 apply(tactic {* quotient_tac @{context} 1 *})
 apply(rule refl)
+done
 
+term map
+
+lemma lam_tst4: "map (\<lambda>x. my_plus x (0,0)) l = l"
+apply (induct l)
+apply simp
+apply (case_tac a)
+apply simp
+done
+
+lemma "map (\<lambda>x. PLUS x ZERO) l = l"
+apply(tactic {* procedure_tac @{context} @{thm lam_tst4} 1 *})
+apply(tactic {* regularize_tac @{context} 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
+apply(tactic {* clean_tac @{context} 1*})
+apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int])
+apply(simp only: map_prs[OF Quotient_my_int Quotient_my_int])
+apply(tactic {* lambda_prs_tac @{context} 1 *})
+apply(rule refl)
+done
 
 end