--- a/IntEx.thy	Fri Dec 04 16:12:40 2009 +0100
+++ b/IntEx.thy	Fri Dec 04 16:40:23 2009 +0100
@@ -196,48 +196,9 @@
 done
 
 
-lemma foldr_prs:
-  assumes a: "Quotient R1 abs1 rep1"
-  and     b: "Quotient R2 abs2 rep2"
-  shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e"
-apply (induct l)
-apply (simp add: Quotient_ABS_REP[OF b])
-apply (simp add: Quotient_ABS_REP[OF a] Quotient_ABS_REP[OF b])
-done
-
-lemma foldl_prs:
-  assumes a: "Quotient R1 abs1 rep1"
-  and     b: "Quotient R2 abs2 rep2"
-  shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l"
-apply (induct l arbitrary:e)
-apply (simp add: Quotient_ABS_REP[OF a])
-apply (simp add: Quotient_ABS_REP[OF a] Quotient_ABS_REP[OF b])
-done
-
-lemma map_prs:
-  assumes a: "Quotient R1 abs1 rep1"
-  and     b: "Quotient R2 abs2 rep2"
-  shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l"
-apply (induct l)
-apply (simp)
-apply (simp add: Quotient_ABS_REP[OF a] Quotient_ABS_REP[OF b])
-done
 
 
-(* Removed unneeded assumption: "QUOTIENT R abs1 rep1" *)
-lemma nil_prs:
-  shows "map abs1 [] = []"
-by simp
 
-lemma cons_prs:
-  assumes a: "Quotient R1 abs1 rep1"
-  shows "(map abs1) ((rep1 h) # (map rep1 t)) = h # t"
-  apply (induct t)
-by (simp_all add: Quotient_ABS_REP[OF a])
-
-lemma cons_rsp[quotient_rsp]:
-  "(op \<approx> ===> list_rel op \<approx> ===> list_rel op \<approx>) op # op #"
-by simp
 
 (* I believe it's true. *)
 lemma foldl_rsp[quotient_rsp]:
@@ -255,16 +216,14 @@
 apply (induct_tac xb yb rule: list_induct2) (* To finish I need to give it: arbitrary:xa ya *)
 sorry
 
-lemma nil_listrel_rsp[quotient_rsp]:
-  "(list_rel R) [] []"
-by simp
-
 lemma "foldl PLUS x [] = x"
 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(rule nil_rsp)
+apply(tactic {* quotient_tac @{context} 1*})
 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int])
-apply(simp only: nil_prs)
+apply(simp only: nil_prs[OF Quotient_my_int])
 apply(tactic {* clean_tac @{context} 1 *})
 done
 
@@ -275,6 +234,8 @@
 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(rule cons_rsp)
+apply(tactic {* quotient_tac @{context} 1 *})
 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int])
 apply(simp only: cons_prs[OF Quotient_my_int])
 apply(tactic {* clean_tac @{context} 1 *})