--- a/src/HOL/IsaMakefile Tue Mar 02 15:39:15 2010 +0100
+++ b/src/HOL/IsaMakefile Tue Mar 02 17:45:10 2010 +0100
@@ -756,7 +756,7 @@
HOL-ZF: HOL $(LOG)/HOL-ZF.gz
-$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/Helper.thy ZF/LProd.thy \
+$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/LProd.thy \
ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex
@$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF
--- a/src/HOL/ZF/HOLZF.thy Tue Mar 02 15:39:15 2010 +0100
+++ b/src/HOL/ZF/HOLZF.thy Tue Mar 02 17:45:10 2010 +0100
@@ -6,7 +6,7 @@
*)
theory HOLZF
-imports Helper
+imports Main
begin
typedecl ZF
@@ -298,7 +298,7 @@
apply (rule_tac x="Fst z" in exI)
apply (simp add: isOpair_def)
apply (auto simp add: Fst Snd Opair)
- apply (rule theI2')
+ apply (rule the1I2)
apply auto
apply (drule Fun_implies_PFun)
apply (drule_tac x="Opair x ya" and y="Opair x yb" in PFun_inj)
@@ -306,7 +306,7 @@
apply (drule Fun_implies_PFun)
apply (drule_tac x="Opair x y" and y="Opair x ya" in PFun_inj)
apply (auto simp add: Fst Snd)
- apply (rule theI2')
+ apply (rule the1I2)
apply (auto simp add: Fun_total)
apply (drule Fun_implies_PFun)
apply (drule_tac x="Opair a x" and y="Opair a y" in PFun_inj)
--- a/src/HOL/ZF/Helper.thy Tue Mar 02 15:39:15 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-(* 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
\ No newline at end of file
--- a/src/HOL/ZF/Zet.thy Tue Mar 02 15:39:15 2010 +0100
+++ b/src/HOL/ZF/Zet.thy Tue Mar 02 17:45:10 2010 +0100
@@ -35,7 +35,7 @@
apply (rule_tac x="Repl z (g o (inv_into A f))" in exI)
apply (simp add: explode_Repl_eq)
apply (subgoal_tac "explode z = f ` A")
- apply (simp_all add: comp_image_eq)
+ apply (simp_all add: image_compose)
done
lemma zet_image_mem:
@@ -56,7 +56,7 @@
apply (auto simp add: subset injf)
done
show ?thesis
- apply (simp add: zet_def' comp_image_eq[symmetric])
+ apply (simp add: zet_def' image_compose[symmetric])
apply (rule exI[where x="?w"])
apply (simp add: injw image_zet_rep Azet)
done
@@ -108,7 +108,7 @@
lemma comp_zimage_eq: "zimage g (zimage f A) = zimage (g o f) A"
apply (simp add: zimage_def)
apply (subst Abs_zet_inverse)
- apply (simp_all add: comp_image_eq zet_image_mem Rep_zet)
+ apply (simp_all add: image_compose zet_image_mem Rep_zet)
done
definition zunion :: "'a zet \<Rightarrow> 'a zet \<Rightarrow> 'a zet" where