# HG changeset patch
# User haftmann
# Date 1261380723 -3600
# Node ID 22acb8b38639f3bf720b93481220a2aa1b33afde
# Parent  db1b90188fd1a70aebb1471d7b2d2db01e11edd9
moved lemmas o_eq_dest, o_eq_elim here

diff -r db1b90188fd1 -r 22acb8b38639 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Dec 17 23:44:48 2009 +0100
+++ b/src/HOL/Fun.thy	Mon Dec 21 08:32:03 2009 +0100
@@ -74,6 +74,14 @@
 lemma o_id [simp]: "f o id = f"
 by (simp add: comp_def)
 
+lemma o_eq_dest:
+  "a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
+  by (simp only: o_def) (fact fun_cong)
+
+lemma o_eq_elim:
+  "a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
+  by (erule meta_mp) (fact o_eq_dest) 
+
 lemma image_compose: "(f o g) ` r = f`(g`r)"
 by (simp add: comp_def, blast)