diff -r fe2a37cfecd3 -r 830b58c2fa94 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Tue Dec 08 22:02:14 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Tue Dec 08 22:24:24 2009 +0100
@@ -1,5 +1,5 @@
 theory IntEx
-imports "../QuotList" Nitpick
+imports "../QuotList" "../QuotProd" Nitpick
 begin
 
 fun
@@ -204,30 +204,23 @@
 
 lemma "foldl PLUS x [] = x"
 apply(lifting ho_tst)
-apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
-apply(tactic {* clean_tac @{context} 1 *})
 done
 
 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"
 sorry
 
 lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)"
-apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *})
-apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int])
-apply(tactic {* clean_tac @{context} 1 *})
+apply(lifting_setup ho_tst2)
+apply(regularize)
+apply(injection)
+apply(cleaning)
 done
 
 lemma ho_tst3: "foldl f (s::nat \<times> nat) ([]::(nat \<times> nat) list) = s"
 by simp
 
 lemma "foldl f (x::my_int) ([]::my_int list) = x"
-apply(tactic {* procedure_tac @{context} @{thm ho_tst3} 1 *})
-apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
-apply(tactic {* clean_tac @{context} 1 *})
+apply(lifting ho_tst3)
 done
 
 lemma lam_tst: "(\<lambda>x. (x, x)) y = (y, (y :: nat \<times> nat))"
@@ -235,11 +228,7 @@
 
 (* Don't know how to keep the goal non-contracted... *)
 lemma "(\<lambda>x. (x, x)) (y::my_int) = (y, y)"
-apply(tactic {* procedure_tac @{context} @{thm lam_tst} 1 *})
-apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(tactic {* clean_tac @{context} 1 *})
-apply(simp add: pair_prs)
+apply(lifting lam_tst)
 done
 
 lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"
@@ -308,7 +297,6 @@
 apply(rule impI)
 apply(rule lam_tst3a_reg)
 apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int])
 apply(tactic {* clean_tac  @{context} 1 *})
 done
 
@@ -316,19 +304,10 @@
 by auto
 
 lemma "(\<lambda>(y :: my_int => my_int). y) = (\<lambda>(x :: my_int => my_int). x)"
-apply(tactic {* procedure_tac @{context} @{thm lam_tst3b} 1 *})
+apply(lifting lam_tst3b)
 apply(rule impI)
-apply (rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]])
-apply (simp add: id_rsp)
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(tactic {* clean_tac  @{context} 1 *})
-apply(subst babs_prs)
-apply(tactic {* quotient_tac @{context} 1 *})
-apply(tactic {* quotient_tac @{context} 1 *})
-apply(subst babs_prs)
-apply(tactic {* quotient_tac @{context} 1 *})
-apply(tactic {* quotient_tac @{context} 1 *})
-apply(rule refl)
+apply(rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]])
+apply(simp add: id_rsp)
 done
 
 term map
@@ -342,9 +321,6 @@
 
 lemma "map (\<lambda>x. PLUS x ZERO) l = l"
 apply(lifting lam_tst4)
-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(cleaning)
 done
 
 end