# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260046231 -3600
# Node ID d641c32855f0e4dcf639ad9bddeb467cd1b9aca7
# Parent  114bb544ecb982380bd9c4177c2861fc096e7e51# Parent  b460565dbb58074913d98a7b70d13d6526323fee
merged

diff -r 114bb544ecb9 -r d641c32855f0 IntEx.thy
--- a/IntEx.thy	Sat Dec 05 21:47:48 2009 +0100
+++ b/IntEx.thy	Sat Dec 05 21:50:31 2009 +0100
@@ -176,24 +176,7 @@
 apply(rule ballI)
 apply(rule apply_rsp[OF Quotient_my_int ho_plus_rsp])
 apply(simp only: in_respects)
-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(rule quot_rel_rsp)
-apply(tactic {* quotient_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*})
-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(fold PLUS_def)
+apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 done
 
@@ -204,14 +187,7 @@
 lemma "PLUS = PLUS"
 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *})
 apply(rule ho_plus_rsp)
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(rule quot_rel_rsp)
-apply(tactic {* quotient_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 {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 done
 
@@ -219,32 +195,7 @@
 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 *})
-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*})
-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*})
-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*})
-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*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 done
 
diff -r 114bb544ecb9 -r d641c32855f0 QuotMain.thy
--- a/QuotMain.thy	Sat Dec 05 21:47:48 2009 +0100
+++ b/QuotMain.thy	Sat Dec 05 21:50:31 2009 +0100
@@ -148,6 +148,9 @@
 lemmas [quotient_thm] =
   fun_quotient list_quotient
 
+lemmas [quotient_rsp] =
+  quot_rel_rsp
+
 ML {* maps_lookup @{theory} "List.list" *}
 ML {* maps_lookup @{theory} "*" *}
 ML {* maps_lookup @{theory} "fun" *}
@@ -981,6 +984,13 @@
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
     (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
+| (Const (@{const_name fun_rel}, _) $ _ $ _) $
+    (Const (@{const_name fun_rel}, _) $ _ $ _) $
+    (Const (@{const_name fun_rel}, _) $ _ $ _)
+    => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt
+| (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Const _) $ (Const _) =>
+    (* respectfulness of constants; in particular of a simple relation *)
+    resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
 | Const (@{const_name "op ="},_) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
@@ -1020,9 +1030,7 @@
     NDT ctxt "E" (atac),
     (* reflexivity of the basic relations *)
     (* R \<dots> \<dots> *)
-    NDT ctxt "D" (resolve_tac rel_refl),
-    (* respectfulness of constants *)
-    NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt))
+    NDT ctxt "D" (resolve_tac rel_refl)
     ])
 *}