--- a/IntEx.thy	Fri Dec 04 18:32:19 2009 +0100
+++ b/IntEx.thy	Fri Dec 04 21:42:55 2009 +0100
@@ -130,6 +130,10 @@
   apply(auto)
   done
 
+lemma list_equiv_rsp[quotient_rsp]:
+  shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
+by auto
+
 lemma ho_plus_rsp[quotient_rsp]:
   shows "(intrel ===> intrel ===> intrel) my_plus my_plus"
 by (simp)
@@ -149,8 +153,9 @@
 lemma "PLUS a b = PLUS b a"
 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
-prefer 2
-apply(tactic {* clean_tac @{context} 1 *})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
@@ -174,6 +179,7 @@
 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* clean_tac @{context} 1 *})
 done
 
 lemma plus_assoc_pre:
@@ -195,11 +201,6 @@
 apply simp
 done
 
-
-
-
-
-
 (* I believe it's true. *)
 lemma foldl_rsp[quotient_rsp]:
   "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> list_rel op \<approx> ===> op \<approx>) foldl foldl"
@@ -222,10 +223,12 @@
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(rule nil_rsp)
 apply(tactic {* quotient_tac @{context} 1*})
+apply(simp only: fun_map.simps id_simps)
+apply(simp only: Quotient_abs_rep[OF fun_quotient[OF Quotient_my_int fun_quotient[OF Quotient_my_int Quotient_my_int]]])
+apply(simp only: Quotient_abs_rep[OF list_quotient[OF Quotient_my_int]])
 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int])
-apply(simp only: nil_prs[OF Quotient_my_int])
 apply(tactic {* clean_tac @{context} 1 *})
-done
+sorry
 
 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"
 sorry
@@ -236,6 +239,9 @@
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(rule cons_rsp)
 apply(tactic {* quotient_tac @{context} 1 *})
+apply(simp only: fun_map.simps id_simps)
+apply(simp only: Quotient_abs_rep[OF fun_quotient[OF Quotient_my_int fun_quotient[OF Quotient_my_int Quotient_my_int]]])
+apply(simp only: Quotient_abs_rep[OF list_quotient[OF Quotient_my_int]])
 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 *})