src/ZF/func.ML

--- a/src/ZF/func.ML	Fri Aug 12 12:51:34 1994 +0200
+++ b/src/ZF/func.ML	Fri Aug 12 18:45:33 1994 +0200
@@ -71,6 +71,13 @@
 by (REPEAT (assume_tac 1));
 val apply_equality = result();
 
+(*Applying a function outside its domain yields 0*)
+goalw ZF.thy [apply_def]
+    "!!a b f. [| a ~: domain(f);  f: Pi(A,B) |] ==> f`a = 0";
+by (rtac the_0 1);
+by (fast_tac ZF_cs 1);
+val apply_0 = result();
+
 val prems = goal ZF.thy
     "[| f: Pi(A,B);   c: f;   !!x. [| x:A;  c = <x,f`x> |] ==> P  \
 \    |] ==> P";
@@ -338,9 +345,14 @@
 by (fast_tac ZF_cs 1);
 val domain_of_fun = result();
 
+goal ZF.thy "!!f. [| f : Pi(A,B);  a: A |] ==> f`a : range(f)";
+by (etac (apply_Pair RS rangeI) 1);
+by (assume_tac 1);
+val apply_rangeI = result();
+
 val [major] = goal ZF.thy "f : Pi(A,B) ==> f : A->range(f)";
 by (rtac (major RS Pi_type) 1);
-by (etac (major RS apply_Pair RS rangeI) 1);
+by (etac (major RS apply_rangeI) 1);
 val range_of_fun = result();
 
 (*** Extensions of functions ***)