src/HOL/ZF/Helper.thy

+(*  Title:      HOL/ZF/Helper.thy
+    ID:         $Id$
+    Author:     Steven Obua
+
+    Some helpful lemmas that probably will end up elsewhere. 
+*)
+
+theory Helper 
+imports Main
+begin
+
+lemma theI2' : "?! x. P x \<Longrightarrow> (!! x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (THE x. P x)"
+  apply auto
+  apply (subgoal_tac "P (THE x. P x)")
+  apply blast
+  apply (rule theI)
+  apply auto
+  done
+
+lemma in_range_superfluous: "(z \<in> range f & z \<in> (f ` x)) = (z \<in> f ` x)" 
+  by auto
+
+lemma f_x_in_range_f: "f x \<in> range f"
+  by (blast intro: image_eqI)
+
+lemma comp_inj: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (g o f)"
+  by (blast intro: comp_inj_on subset_inj_on)
+
+lemma comp_image_eq: "(g o f) ` x = g ` f ` x"
+  by auto
+  
+end