--- a/src/ZF/func.ML Thu Aug 24 00:55:42 2000 +0200
+++ b/src/ZF/func.ML Thu Aug 24 11:05:20 2000 +0200
@@ -47,27 +47,6 @@
by (Best_tac 1);
qed "fun_weaken_type";
-(*Empty function spaces*)
-Goalw [Pi_def, function_def] "Pi(0,A) = {0}";
-by (Blast_tac 1);
-qed "Pi_empty1";
-
-Goalw [Pi_def] "a:A ==> A->0 = 0";
-by (Blast_tac 1);
-qed "Pi_empty2";
-
-(*The empty function*)
-Goalw [Pi_def, function_def] "0: Pi(0,B)";
-by (Blast_tac 1);
-qed "empty_fun";
-
-(*The singleton function*)
-Goalw [Pi_def, function_def] "{<a,b>} : {a} -> {b}";
-by (Blast_tac 1);
-qed "singleton_fun";
-
-Addsimps [Pi_empty1, singleton_fun];
-
(*** Function Application ***)
Goalw [Pi_def, function_def] "[| <a,b>: f; <a,c>: f; f: Pi(A,B) |] ==> b=c";
@@ -130,6 +109,12 @@
by (blast_tac (claset() addIs [Pi_type] addDs [apply_type]) 1);
qed "Pi_Collect_iff";
+val [major,minor] = Goal
+ "[| f : Pi(A,B); !!x. x:A ==> B(x)<=C(x) |] ==> f : Pi(A,C)";
+by (fast_tac (claset() addSIs [major RS Pi_type, minor RS subsetD,
+ major RS apply_type]) 1);
+qed "Pi_weaken_type";
+
(** Elimination of membership in a function **)
@@ -204,6 +189,34 @@
by (etac (major RS theI) 1);
qed "lam_theI";
+Goal "[| (lam x:A. f(x)) = (lam x:A. g(x)); a:A |] ==> f(a)=g(a)";
+by (fast_tac (claset() addSIs [lamI] addEs [equalityE, lamE]) 1);
+qed "lam_eqE";
+
+
+(*Empty function spaces*)
+Goalw [Pi_def, function_def] "Pi(0,A) = {0}";
+by (Blast_tac 1);
+qed "Pi_empty1";
+Addsimps [Pi_empty1];
+
+(*The singleton function*)
+Goalw [Pi_def, function_def] "{<a,b>} : {a} -> {b}";
+by (Blast_tac 1);
+qed "singleton_fun";
+Addsimps [singleton_fun];
+
+Goalw [Pi_def, function_def] "(A->0) = (if A=0 then {0} else 0)";
+by (Force_tac 1);
+qed "Pi_empty2";
+Addsimps [Pi_empty2];
+
+Goal "(A->X)=0 \\<longleftrightarrow> X=0 & (A \\<noteq> 0)";
+by Auto_tac;
+by (fast_tac (claset() addSIs [equals0I] addIs [lam_type]) 1);
+qed "fun_space_empty_iff";
+AddIffs [fun_space_empty_iff];
+
(** Extensionality **)