diff -r d641c32855f0 -r 41500cd131dc IntEx.thy
--- a/IntEx.thy	Sat Dec 05 21:50:31 2009 +0100
+++ b/IntEx.thy	Sat Dec 05 22:05:09 2009 +0100
@@ -130,17 +130,11 @@
   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]:
+lemma plus_rsp[quotient_rsp]:
   shows "(intrel ===> intrel ===> intrel) my_plus my_plus"
 by (simp)
 
 ML {* val qty = @{typ "my_int"} *}
-ML {* val ty_name = "my_int" *}
-ML {* val rsp_thms = @{thms ho_plus_rsp} *}
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *}
 
@@ -174,7 +168,7 @@
 lemma "PLUS a = PLUS a"
 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *})
 apply(rule ballI)
-apply(rule apply_rsp[OF Quotient_my_int ho_plus_rsp])
+apply(rule apply_rsp[OF Quotient_my_int plus_rsp])
 apply(simp only: in_respects)
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
@@ -186,7 +180,7 @@
 
 lemma "PLUS = PLUS"
 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *})
-apply(rule ho_plus_rsp)
+apply(rule plus_rsp)
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 done
@@ -238,14 +232,8 @@
 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: 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(tactic {* clean_tac @{context} 1 *})
-apply(simp) (* FIXME: why is this needed *)
+apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
 done
 
 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"
@@ -255,13 +243,7 @@
 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: 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 *})
+apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int])
 done