src/HOL/ZF/Helper.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 19203 778507520684
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
     1 (*  Title:      HOL/ZF/Helper.thy
     2     ID:         $Id$
     3     Author:     Steven Obua
     4 
     5     Some helpful lemmas that probably will end up elsewhere. 
     6 *)
     7 
     8 theory Helper 
     9 imports Main
    10 begin
    11 
    12 lemma theI2' : "?! x. P x \<Longrightarrow> (!! x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (THE x. P x)"
    13   apply auto
    14   apply (subgoal_tac "P (THE x. P x)")
    15   apply blast
    16   apply (rule theI)
    17   apply auto
    18   done
    19 
    20 lemma in_range_superfluous: "(z \<in> range f & z \<in> (f ` x)) = (z \<in> f ` x)" 
    21   by auto
    22 
    23 lemma f_x_in_range_f: "f x \<in> range f"
    24   by (blast intro: image_eqI)
    25 
    26 lemma comp_inj: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (g o f)"
    27   by (blast intro: comp_inj_on subset_inj_on)
    28 
    29 lemma comp_image_eq: "(g o f) ` x = g ` f ` x"
    30   by auto
    31   
    32 end