# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271930119 -7200
# Node ID 92011cc923f580111c5710a04559f4776d8e9fb9
# Parent  c6ca9e258269fdc7a7492cf15cc4c59c36db9759
fun_rel introduction and list_rel elimination for quotient package

diff -r c6ca9e258269 -r 92011cc923f5 src/HOL/Library/Quotient_List.thy
--- a/src/HOL/Library/Quotient_List.thy	Thu Apr 22 09:30:39 2010 +0200
+++ b/src/HOL/Library/Quotient_List.thy	Thu Apr 22 11:55:19 2010 +0200
@@ -271,6 +271,15 @@
   apply(simp_all)
   done
 
+lemma list_rel_find_element:
+  assumes a: "x \<in> set a"
+  and b: "list_rel R a b"
+  shows "\<exists>y. (y \<in> set b \<and> R x y)"
+proof -
+  have "length a = length b" using b by (rule list_rel_len)
+  then show ?thesis using a b by (induct a b rule: list_induct2) auto
+qed
+
 lemma list_rel_refl:
   assumes a: "\<And>x y. R x y = (R x = R y)"
   shows "list_rel R x x"
diff -r c6ca9e258269 -r 92011cc923f5 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Thu Apr 22 09:30:39 2010 +0200
+++ b/src/HOL/Quotient.thy	Thu Apr 22 11:55:19 2010 +0200
@@ -106,6 +106,10 @@
 where
 [simp]: "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
 
+lemma fun_relI [intro]:
+  assumes "\<And>a b. P a b \<Longrightarrow> Q (x a) (y b)"
+  shows "(P ===> Q) x y"
+  using assms by (simp add: fun_rel_def)
 
 lemma fun_map_id:
   shows "(id ---> id) = id"