|
19203
|
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 |