# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1281504624 -28800
# Node ID cb8e2ac6397b1d7dd24686ffb9dfcc36b49419ea
# Parent  88e774d09fbcf98a059d25716ed934dc430e40b6
deleted duplicate lemma

diff -r 88e774d09fbc -r cb8e2ac6397b src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Tue Aug 10 22:26:23 2010 +0200
+++ b/src/HOL/Quotient.thy	Wed Aug 11 13:30:24 2010 +0800
@@ -136,16 +136,6 @@
   shows "((op =) ===> (op =)) = (op =)"
   by (simp add: expand_fun_eq)
 
-lemma fun_rel_id:
-  assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
-  shows "(R1 ===> R2) f g"
-  using a by simp
-
-lemma fun_rel_id_asm:
-  assumes a: "\<And>x y. R1 x y \<Longrightarrow> (A \<longrightarrow> R2 (f x) (g y))"
-  shows "A \<longrightarrow> (R1 ===> R2) f g"
-  using a by auto
-
 
 subsection {* Quotient Predicate *}
 
@@ -597,7 +587,7 @@
 lemma quot_rel_rsp:
   assumes a: "Quotient R Abs Rep"
   shows "(R ===> R ===> op =) R R"
-  apply(rule fun_rel_id)+
+  apply(rule fun_relI)+
   apply(rule equals_rsp[OF a])
   apply(assumption)+
   done
diff -r 88e774d09fbc -r cb8e2ac6397b src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Tue Aug 10 22:26:23 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Aug 11 13:30:24 2010 +0800
@@ -316,7 +316,7 @@
    The deterministic part:
     - remove lambdas from both sides
     - prove Ball/Bex/Babs equalities using ball_rsp, bex_rsp, babs_rsp
-    - prove Ball/Bex relations unfolding fun_rel_id
+    - prove Ball/Bex relations using fun_relI
     - reflexivity of equality
     - prove equality of relations using equals_rsp
     - use user-supplied RSP theorems
@@ -335,7 +335,7 @@
 (case (bare_concl goal) of
     (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)
   (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)
-      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
+      => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
 
     (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
 | (Const (@{const_name "op ="},_) $
@@ -347,7 +347,7 @@
 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
-      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
+      => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
 
     (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
 | Const (@{const_name "op ="},_) $
@@ -359,7 +359,7 @@
 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
-      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
+      => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
 
 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
     (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _)