# HG changeset patch
# User paulson
# Date 1013771247 -3600
# Node ID 92af5c3a10fb7487ca0f398cc684f8dd66f9086e
# Parent  75b254b1c8bac19bb268d507edb56d92a9a83d9f
a new definition of "restrict"

diff -r 75b254b1c8ba -r 92af5c3a10fb src/ZF/AC/AC17_AC1.thy
--- a/src/ZF/AC/AC17_AC1.thy	Thu Feb 14 20:30:49 2002 +0100
+++ b/src/ZF/AC/AC17_AC1.thy	Fri Feb 15 12:07:27 2002 +0100
@@ -15,7 +15,7 @@
     AC0 comes from Suppes, AC1 from Rubin & Rubin **)
 
 lemma AC0_AC1_lemma: "[| f:(\<Pi>X \<in> A. X); D \<subseteq> A |] ==> \<exists>g. g:(\<Pi>X \<in> D. X)"
-by (fast intro!: restrict_type apply_type)
+by (fast intro!: lam_type apply_type)
 
 lemma AC0_AC1: "AC0 ==> AC1"
 apply (unfold AC0_def AC1_def)
@@ -75,7 +75,7 @@
 apply (rule allI)
 apply (erule swap)
 apply (rule_tac x = "Union (A)" in exI)
-apply (blast intro: restrict_type)
+apply (blast intro: lam_type)
 done
 
 lemma lemma1:
diff -r 75b254b1c8ba -r 92af5c3a10fb src/ZF/AC/DC.thy
--- a/src/ZF/AC/DC.thy	Thu Feb 14 20:30:49 2002 +0100
+++ b/src/ZF/AC/DC.thy	Fri Feb 15 12:07:27 2002 +0100
@@ -57,12 +57,8 @@
 by (simp add: domain_cons succ_def)
 
 lemma restrict_cons_eq: "g \<in> n->X ==> restrict(cons(<n,x>, g), n) = g"
-apply (unfold restrict_def)
-apply (rule fun_extension)
-apply (rule lam_type)
-apply (erule cons_fun_type [THEN apply_type])
-apply (erule succI2, assumption)
-apply (simp add: cons_val_k)
+apply (simp add: restrict_def Pi_iff)
+apply (blast intro: elim: mem_irrefl)  
 done
 
 lemma succ_in_succ: "[| Ord(k); i \<in> k |] ==> succ(i) \<in> succ(k)"
@@ -71,10 +67,9 @@
 done
 
 lemma restrict_eq_imp_val_eq: 
-      "[| restrict(f, domain(g)) = g; x \<in> domain(g) |] ==> f`x = g`x"
-apply (unfold restrict_def) 
-apply (erule subst, simp)
-done
+      "[|restrict(f, domain(g)) = g; x \<in> domain(g)|] 
+       ==> f`x = g`x" 
+by (erule subst, simp add: restrict)
 
 lemma domain_eq_imp_fun_type: "[| domain(f)=A; f \<in> B->C |] ==> f \<in> A->C"
 by (frule domain_of_fun, fast)
@@ -220,7 +215,7 @@
  apply (simp add: RR_def)
 apply (drule lemma2, assumption+)
 apply (blast dest!: domain_of_fun 
-             intro: nat_into_Ord OrdmemD [THEN subsetD])
+	     intro: nat_into_Ord OrdmemD [THEN subsetD])
 done
 
 lemma (in DC0_imp) lemma3:
@@ -370,11 +365,9 @@
      "[| restrict(h, domain(u))=u;  h \<in> n->X;  domain(u) \<subseteq> n |]   
       ==> restrict(cons(<n, y>, h), domain(u)) = u"
 apply (unfold restrict_def)
+apply (simp add: restrict_def Pi_iff)
 apply (erule sym [THEN trans, symmetric])
-apply (rule fun_extension)
-apply (fast intro!: lam_type)
-apply (fast intro!: lam_type)
-apply (simp add: subsetD [THEN cons_val_k])
+apply (blast elim: mem_irrefl)  
 done
 
 lemma (in imp_DC0) all_in_image_restrict_eq:
diff -r 75b254b1c8ba -r 92af5c3a10fb src/ZF/Induct/Multiset.ML
--- a/src/ZF/Induct/Multiset.ML	Thu Feb 14 20:30:49 2002 +0100
+++ b/src/ZF/Induct/Multiset.ML	Fri Feb 15 12:07:27 2002 +0100
@@ -1,4 +1,4 @@
-(*  Title:      ZF/Induct/Multiset.thy
+(*  Title:      ZF/Induct/Multiset
     ID:         $Id$
     Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
 
@@ -9,6 +9,45 @@
 
 *)
 
+(* Properties of the original "restrict" from ZF.thy. *)
+
+Goalw [funrestrict_def,lam_def]
+    "[| f: Pi(C,B);  A<=C |] ==> funrestrict(f,A) <= f";
+by (blast_tac (claset() addIs [apply_Pair]) 1);
+qed "funrestrict_subset";
+
+val prems = Goalw [funrestrict_def]
+    "[| !!x. x:A ==> f`x: B(x) |] ==> funrestrict(f,A) : Pi(A,B)";  
+by (rtac lam_type 1);
+by (eresolve_tac prems 1);
+qed "funrestrict_type";
+
+Goal "[| f: Pi(C,B);  A<=C |] ==> funrestrict(f,A) : Pi(A,B)";  
+by (blast_tac (claset() addIs [apply_type, funrestrict_type]) 1);
+qed "funrestrict_type2";
+
+Goalw [funrestrict_def] "a : A ==> funrestrict(f,A) ` a = f`a";
+by (etac beta 1);
+qed "funrestrict";
+
+Goalw [funrestrict_def] "funrestrict(f,0) = 0";
+by (Simp_tac 1);
+qed "funrestrict_empty";
+
+Addsimps [funrestrict, funrestrict_empty];
+
+Goalw [funrestrict_def, lam_def] "domain(funrestrict(f,C)) = C";
+by (Blast_tac 1);
+qed "domain_funrestrict";
+Addsimps [domain_funrestrict];
+
+Goal "f : cons(a, b) -> B ==> f = cons(<a, f ` a>, funrestrict(f, b))";
+by (rtac equalityI 1);
+by (blast_tac (claset() addIs [apply_Pair, impOfSubs funrestrict_subset]) 2);
+by (auto_tac (claset() addSDs [Pi_memberD],
+	       simpset() addsimps [funrestrict_def, lam_def]));
+qed "fun_cons_funrestrict_eq";
+
 Addsimps [domain_of_fun];
 Delrules [domainE];
 
@@ -146,7 +185,7 @@
 
 (** normalize **)
 
-Goalw [normalize_def, restrict_def, mset_of_def]
+Goalw [normalize_def, funrestrict_def, mset_of_def]
  "normalize(normalize(f)) = normalize(f)";
 by Auto_tac;
 qed "normalize_idem";
@@ -156,7 +195,7 @@
  "multiset(M) ==> normalize(M) = M";
 by (rewrite_goals_tac [normalize_def, mset_of_def]);
 by (auto_tac (claset(), simpset() 
-          addsimps [restrict_def, multiset_fun_iff]));
+          addsimps [funrestrict_def, multiset_fun_iff]));
 qed "normalize_multiset";
 Addsimps [normalize_multiset];
 
@@ -166,7 +205,7 @@
 by Auto_tac;
 by (res_inst_tac [("x", "{x:A . 0<f`x}")] exI 1);
 by (auto_tac (claset() addIs [Collect_subset RS subset_Finite,
-                              restrict_type], simpset()));
+                              funrestrict_type], simpset()));
 qed "normalize_multiset";
 
 (** Typechecking rules for union and difference of multisets **)
@@ -243,7 +282,7 @@
 Goalw [multiset_def] "multiset(M) ==> M -# 0 = M & 0 -# M = 0";
 by (rewrite_goals_tac [mdiff_def, normalize_def]);
 by (auto_tac (claset(), simpset() 
-         addsimps [multiset_fun_iff, mset_of_def, restrict_def]));
+         addsimps [multiset_fun_iff, mset_of_def, funrestrict_def]));
 qed "mdiff_0";
 Addsimps [mdiff_0];
 
@@ -254,7 +293,7 @@
 by (rtac fun_extension 1);
 by Auto_tac;
 by (res_inst_tac [("P", "%x. ?u : Pi(x, ?v)")] subst 1);
-by (rtac restrict_type 2);
+by (rtac funrestrict_type 2);
 by (rtac equalityI 1);
 by (ALLGOALS(Clarify_tac));
 by Auto_tac;
@@ -512,7 +551,7 @@
 Goalw [multiset_def]
      "Finite(A) \
 \     ==> ALL M. multiset(M) --> (ALL a:mset_of(M).            \
-\          setsum(%x'. $# mcount(restrict(M, mset_of(M)-{a}), x'), A) = \
+\          setsum(%x'. $# mcount(funrestrict(M, mset_of(M)-{a}), x'), A) = \
 \          (if a:A then setsum(%x'. $# mcount(M, x'), A) $- $# M`a     \
 \           else setsum(%x'. $# mcount(M, x'), A)))";
 by (etac Finite_induct 1);
@@ -522,11 +561,11 @@
 qed "setsum_decr2";
 
 Goal "[| Finite(A); multiset(M); a:mset_of(M) |] \
-\     ==> setsum(%x. $# mcount(restrict(M, mset_of(M)-{a}), x), A - {a}) = \
+\     ==> setsum(%x. $# mcount(funrestrict(M, mset_of(M)-{a}), x), A - {a}) = \
 \         (if a:A then setsum(%x. $# mcount(M, x), A) $- $# M`a\
 \          else setsum(%x. $# mcount(M, x), A))";
-by (subgoal_tac "setsum(%x. $# mcount(restrict(M, mset_of(M)-{a}),x),A-{a}) = \
-\                setsum(%x. $# mcount(restrict(M, mset_of(M)-{a}),x),A)" 1);
+by (subgoal_tac "setsum(%x. $# mcount(funrestrict(M, mset_of(M)-{a}),x),A-{a}) = \
+\                setsum(%x. $# mcount(funrestrict(M, mset_of(M)-{a}),x),A)" 1);
 by (rtac (setsum_Diff RS sym) 2);
 by (REPEAT(asm_simp_tac (simpset() addsimps [mcount_def, mset_of_def]) 2));
 by (rtac sym 1 THEN rtac ssubst 1);
@@ -599,34 +638,34 @@
 by (rotate_simp_tac "cons(a, A) = A" 1);
 by (rotate_simp_tac "ALL x:A. ?u(x)" 1);
 by (rotate_simp_tac "ALL x:A. ?u(x)" 2);
-by (subgoal_tac "M=cons(<a, M`a>, restrict(M, A-{a}))" 1);
-by (rtac  fun_cons_restrict_eq 2);
+by (subgoal_tac "M=cons(<a, M`a>, funrestrict(M, A-{a}))" 1);
+by (rtac  fun_cons_funrestrict_eq 2);
 by (subgoal_tac "cons(a, A-{a}) = A" 2);
 by (REPEAT(Force_tac 2));
-by (res_inst_tac [("a", "cons(<a, 1>, restrict(M, A - {a}))")] ssubst 1);
+by (res_inst_tac [("a", "cons(<a, 1>, funrestrict(M, A - {a}))")] ssubst 1);
 by (Asm_full_simp_tac 1);
-by (subgoal_tac "multiset(restrict(M, A - {a}))" 1);
+by (subgoal_tac "multiset(funrestrict(M, A - {a}))" 1);
 by (simp_tac (simpset() addsimps [multiset_def, multiset_fun_iff]) 2);
 by (res_inst_tac [("x", "A-{a}")] exI 2);
 by Safe_tac;
 by (res_inst_tac [("A", "A-{a}")] apply_type 3);
-by (asm_simp_tac (simpset() addsimps [restrict]) 5);
-by (REPEAT(blast_tac (claset() addIs [Finite_Diff, restrict_type]) 2));;
+by (asm_simp_tac (simpset() addsimps [funrestrict]) 5);
+by (REPEAT(blast_tac (claset() addIs [Finite_Diff, funrestrict_type]) 2));;
 by (resolve_tac prems 1);
 by (assume_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [mset_of_def]) 1);
-by (dres_inst_tac [("x", "restrict(M, A-{a})")] spec 1);
+by (dres_inst_tac [("x", "funrestrict(M, A-{a})")] spec 1);
 by (dtac mp 1);
 by (res_inst_tac [("x", "A-{a}")] exI 1);
-by (auto_tac (claset() addIs [Finite_Diff, restrict_type], 
-             simpset() addsimps [restrict]));
+by (auto_tac (claset() addIs [Finite_Diff, funrestrict_type], 
+             simpset() addsimps [funrestrict]));
 by (forw_inst_tac [("A", "A"), ("M", "M"), ("a", "a")] setsum_decr3 1);
 by (asm_simp_tac  (simpset() addsimps [multiset_def, multiset_fun_iff]) 1);
 by (Blast_tac 1);
 by (asm_simp_tac (simpset() addsimps [mset_of_def]) 1);
 by (dres_inst_tac [("b", "if ?u then ?v else ?w")] sym 1);
 by (ALLGOALS(rotate_simp_tac "ALL x:A. ?u(x)"));
-by (subgoal_tac "{x:A - {a} . 0 < restrict(M, A - {x}) ` x} = A - {a}" 1);
+by (subgoal_tac "{x:A - {a} . 0 < funrestrict(M, A - {x}) ` x} = A - {a}" 1);
 by (auto_tac (claset() addSIs [setsum_cong], 
               simpset() addsimps [zdiff_eq_iff, 
                zadd_commute, multiset_def, multiset_fun_iff,mset_of_def]));
@@ -703,7 +742,7 @@
 by (res_inst_tac [("x", "{x:A. P(x)}")] exI 1);
 by (auto_tac (claset()  addDs [CollectD1 RSN (2,apply_type)]
                         addIs [Collect_subset RS subset_Finite,
-                               restrict_type],
+                               funrestrict_type],
               simpset()));
 qed "MCollect_multiset";
 Addsimps [MCollect_multiset];
@@ -711,7 +750,7 @@
 Goalw [mset_of_def, MCollect_def]
  "multiset(M) ==> mset_of({# x:M. P(x) #}) <= mset_of(M)";
 by (auto_tac (claset(), 
-              simpset() addsimps [multiset_def, restrict_def]));
+              simpset() addsimps [multiset_def, funrestrict_def]));
 qed "mset_of_MCollect";
 Addsimps [mset_of_MCollect];
 
diff -r 75b254b1c8ba -r 92af5c3a10fb src/ZF/Induct/Multiset.thy
--- a/src/ZF/Induct/Multiset.thy	Thu Feb 14 20:30:49 2002 +0100
+++ b/src/ZF/Induct/Multiset.thy	Fri Feb 15 12:07:27 2002 +0100
@@ -16,6 +16,14 @@
   "Mult(A)" => "A-||>nat-{0}"
   
 constdefs
+  
+  (* This is the original "restrict" from ZF.thy.
+     Restricts the function f to the domain A 
+     FIXME: adapt Multiset to the new "restrict". *)
+
+  funrestrict :: "[i,i] => i"
+  "funrestrict(f,A) == lam x:A. f`x"
+
   (* M is a multiset *)
   multiset :: i => o
   "multiset(M) == EX A. M:A->nat-{0} & Finite(A)"
@@ -30,7 +38,7 @@
 
   (* eliminating 0's from a function *)
   normalize :: i => i   
-  "normalize(M) == restrict(M, {x:mset_of(M). 0<M`x})"
+  "normalize(M) == funrestrict(M, {x:mset_of(M). 0<M`x})"
 
   mdiff  :: "[i, i] => i" (infixl "-#" 65)
   "M -# N ==  normalize(lam x:mset_of(M).
@@ -41,7 +49,7 @@
   "{#a#} == {<a, 1>}"
   
   MCollect :: [i, i=>o] => i (*comprehension*)
-  "MCollect(M, P) == restrict(M, {x:mset_of(M). P(x)})"
+  "MCollect(M, P) == funrestrict(M, {x:mset_of(M). P(x)})"
 
   (* Counts the number of occurences of an element in a multiset *)
   mcount :: [i, i] => i
diff -r 75b254b1c8ba -r 92af5c3a10fb src/ZF/Order.ML
--- a/src/ZF/Order.ML	Thu Feb 14 20:30:49 2002 +0100
+++ b/src/ZF/Order.ML	Fri Feb 15 12:07:27 2002 +0100
@@ -402,11 +402,12 @@
 Goal "[| f : ord_iso(A,r,B,s);   a:A |] ==>    \
 \      restrict(f, pred(A,a,r)) : ord_iso(pred(A,a,r), r, pred(B, f`a, s), s)";
 by (asm_simp_tac (simpset() addsimps [ord_iso_image_pred RS sym]) 1);
-by (rewtac ord_iso_def);
+by (rewtac ord_iso_def); 
 by (etac CollectE 1);
 by (rtac CollectI 1);
-by (asm_full_simp_tac (simpset() addsimps [pred_def]) 2);
 by (eresolve_tac [[bij_is_inj, pred_subset] MRS restrict_bij] 1);
+by (ftac bij_is_fun 1);
+by (auto_tac (claset(), simpset() addsimps [pred_def])); 
 qed "ord_iso_restrict_pred";
 
 (*Tricky; a lot of forward proof!*)
diff -r 75b254b1c8ba -r 92af5c3a10fb src/ZF/OrderType.ML
--- a/src/ZF/OrderType.ML	Thu Feb 14 20:30:49 2002 +0100
+++ b/src/ZF/OrderType.ML	Fri Feb 15 12:07:27 2002 +0100
@@ -89,6 +89,22 @@
 (*pred-unfolded version.  NOT suitable for rewriting -- loops!*)
 bind_thm ("ordermap_unfold", rewrite_rule [pred_def] ordermap_pred_unfold);
 
+(*The theorem above is 
+
+[| wf[A](r); x : A |]
+==> ordermap(A,r) ` x = {ordermap(A,r) ` y . y: {y: A . <y,x> : r}}
+
+NOTE: the definition of ordermap used here delivers ordinals only if r is
+transitive.  If r is the predecessor relation on the naturals then
+ordermap(nat,predr) ` n equals {n-1} and not n.  A more complicated definition,
+like
+
+  ordermap(A,r) ` x = Union{succ(ordermap(A,r) ` y) . y: {y: A . <y,x> : r}},
+
+might eliminate the need for r to be transitive.
+*)
+
+
 (*** Showing that ordermap, ordertype yield ordinals ***)
 
 fun ordermap_elim_tac i =
diff -r 75b254b1c8ba -r 92af5c3a10fb src/ZF/Perm.ML
--- a/src/ZF/Perm.ML	Thu Feb 14 20:30:49 2002 +0100
+++ b/src/ZF/Perm.ML	Fri Feb 15 12:07:27 2002 +0100
@@ -497,9 +497,8 @@
 
 Goal "[| f: Pi(C,B);  A<=C |] ==> restrict(f,A)``A = f``A";
 by (rtac equalityI 1);
-by (SELECT_GOAL (rewtac restrict_def) 2);
-by (REPEAT (eresolve_tac [imageE, apply_equality RS subst] 2
-     ORELSE ares_tac [subsetI,lamI,imageI] 2));
+by (asm_full_simp_tac (simpset() addsimps [restrict_def]) 2); 
+by (blast_tac (claset() addIs [apply_Pair]) 2); 
 by (REPEAT (ares_tac [image_mono,restrict_subset,subset_refl] 1));
 qed "restrict_image";
 
diff -r 75b254b1c8ba -r 92af5c3a10fb src/ZF/WF.ML
--- a/src/ZF/WF.ML	Thu Feb 14 20:30:49 2002 +0100
+++ b/src/ZF/WF.ML	Fri Feb 15 12:07:27 2002 +0100
@@ -212,23 +212,29 @@
 by (rtac (rel RS underI RS beta) 1);
 qed "apply_recfun";
 
-Goalw [is_recfun_def]
-    "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |] ==> \
-\    <x,a>:r --> <x,b>:r --> f`x=g`x";
+Goal "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |]  \
+\     ==> <x,a>:r --> <x,b>:r --> f`x=g`x";
+by (forw_inst_tac [("f","f")] is_recfun_type 1); 
+by (forw_inst_tac [("f","g")] is_recfun_type 1); 
+by (asm_full_simp_tac (simpset() addsimps [is_recfun_def]) 1); 
 by (wf_ind_tac "x" [] 1);
 by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
 by (asm_simp_tac (simpset() addsimps [vimage_singleton_iff, restrict_def]) 1); 
-by (subgoal_tac "ALL y. y : r-``{x1} --> f`y = g`y" 1);
- by (Asm_simp_tac 1);
-by (blast_tac (claset() addDs [transD]) 1); 
+by (res_inst_tac [("t","%z. H(?x,z)")] subst_context 1); 
+by (subgoal_tac "ALL y : r-``{x1}. ALL z. <y,z>:f <-> <y,z>:g" 1);
+ by (blast_tac (claset() addDs [transD]) 1); 
+by (asm_full_simp_tac (simpset() addsimps [apply_iff]) 1); 
+by (blast_tac (claset() addDs [transD] addIs [sym]) 1); 
 qed_spec_mp "is_recfun_equal";
 
 Goal "[| wf(r);  trans(r);       \
 \        is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  <b,a>:r |]  \
 \     ==> restrict(f, r-``{b}) = g";
-by (rtac (consI1 RS restrict_type RS fun_extension) 1);
-by (etac is_recfun_type 1);
-by (asm_full_simp_tac (simpset() addsimps [vimage_singleton_iff]) 1);
+by (forw_inst_tac [("f","f")] is_recfun_type 1); 
+by (rtac fun_extension 1);
+  by (blast_tac (claset() addDs [transD] addIs [restrict_type2]) 1); 
+ by (etac is_recfun_type 1);
+by (Asm_full_simp_tac 1);
 by (blast_tac (claset() addDs [transD]
 			addIs [is_recfun_equal]) 1);
 qed "is_recfun_cut";
@@ -236,9 +242,8 @@
 (*** Main Existence Lemma ***)
 
 Goal "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |]  ==>  f=g";
-by (rtac fun_extension 1);
-by (REPEAT (ares_tac [is_recfun_equal] 1
-     ORELSE eresolve_tac [is_recfun_type,underD] 1));
+by (blast_tac (claset() addIs [fun_extension, is_recfun_type, 
+                               is_recfun_equal]) 1); 
 qed "is_recfun_functional";
 
 (*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *)
@@ -257,8 +262,12 @@
 (*Applying the substitution: must keep the quantified assumption!!*)
 by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong] 1));
 by (fold_tac [is_recfun_def]);
-by (rtac (consI1 RS restrict_type RSN (2,fun_extension) RS subst_context) 1);
- by (blast_tac (claset() addIs [is_recfun_type]) 1);
+by (res_inst_tac [("t","%z. H(?x,z)")] subst_context 1); 
+by (rtac fun_extension 1);
+  by (blast_tac (claset() addIs [is_recfun_type]) 1);
+ by (rtac (lam_type RS restrict_type2) 1); 
+  by (Blast_tac 1); 
+ by (blast_tac (claset() addDs [transD]) 1); 
 by (ftac (spec RS mp) 1 THEN assume_tac 1);
 by (subgoal_tac "<xa,a1> : r" 1);
 by (dres_inst_tac [("x1","xa")] (spec RS mp) 1 THEN assume_tac 1);
diff -r 75b254b1c8ba -r 92af5c3a10fb src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Thu Feb 14 20:30:49 2002 +0100
+++ b/src/ZF/ZF.thy	Fri Feb 15 12:07:27 2002 +0100
@@ -262,8 +262,8 @@
   apply_def     "f`a == THE y. <a,y> : f"
   Pi_def        "Pi(A,B)  == {f: Pow(Sigma(A,B)). A<=domain(f) & function(f)}"
 
-  (* Restrict the function f to the domain A *)
-  restrict_def  "restrict(f,A) == lam x:A. f`x"
+  (* Restrict the relation r to the domain A *)
+  restrict_def  "restrict(r,A) == {z : r. EX x:A. EX y. z = <x,y>}"
 
 end
 
diff -r 75b254b1c8ba -r 92af5c3a10fb src/ZF/equalities.ML
--- a/src/ZF/equalities.ML	Thu Feb 14 20:30:49 2002 +0100
+++ b/src/ZF/equalities.ML	Fri Feb 15 12:07:27 2002 +0100
@@ -750,3 +750,16 @@
 by (simp_tac (simpset() addsplits [split_if]) 1);
 by (Blast_tac 1);
 qed "Collect_cons";
+
+Goal "A Int Collect(A,P) = Collect(A,P)";
+by (Blast_tac 1); 
+qed "Int_Collect_self_eq";
+
+Goal "Collect(Collect(A,P), Q) = Collect(A, %x. P(x) & Q(x))";
+by (Blast_tac 1); 
+qed "Collect_Collect_eq";
+Addsimps [Collect_Collect_eq];
+
+Goal "Collect(A,P) Int Collect(A,Q) = Collect(A, %x. P(x) & Q(x))";
+by (Blast_tac 1); 
+qed "Collect_Int_Collect_eq";
diff -r 75b254b1c8ba -r 92af5c3a10fb src/ZF/func.ML
--- a/src/ZF/func.ML	Thu Feb 14 20:30:49 2002 +0100
+++ b/src/ZF/func.ML	Fri Feb 15 12:07:27 2002 +0100
@@ -291,47 +291,78 @@
 
 (*** properties of "restrict" ***)
 
-Goalw [restrict_def,lam_def]
+Goalw [restrict_def]
     "[| f: Pi(C,B);  A<=C |] ==> restrict(f,A) <= f";
 by (blast_tac (claset() addIs [apply_Pair]) 1);
 qed "restrict_subset";
 
-val prems = Goalw [restrict_def]
-    "[| !!x. x:A ==> f`x: B(x) |] ==> restrict(f,A) : Pi(A,B)";  
-by (rtac lam_type 1);
-by (eresolve_tac prems 1);
-qed "restrict_type";
+Goalw [restrict_def, function_def]
+    "function(f) ==> function(restrict(f,A))";  
+by (Blast_tac 1); 
+qed "function_restrictI";
 
 Goal "[| f: Pi(C,B);  A<=C |] ==> restrict(f,A) : Pi(A,B)";  
-by (blast_tac (claset() addIs [apply_type, restrict_type]) 1);
+by (asm_full_simp_tac
+    (simpset() addsimps [Pi_iff, function_def, restrict_def]) 1); 
+by (Blast_tac 1); 
 qed "restrict_type2";
 
-Goalw [restrict_def] "a : A ==> restrict(f,A) ` a = f`a";
-by (etac beta 1);
+(*Fails with the new definition of restrict
+    "[| !!x. x:A ==> f`x: B(x) |] ==> restrict(f,A) : Pi(A,B)";  
+qed "restrict_type";
+*)
+
+(*FIXME: move to FOL?*)
+Goal "EX x. a = x";
+by Auto_tac;
+qed "ex_equals_triv"; 
+
+Goal "a : A ==> restrict(f,A) ` a = f`a";
+by (asm_full_simp_tac
+    (simpset() addsimps [apply_def, restrict_def, ex_equals_triv]) 1); 
 qed "restrict";
 
 Goalw [restrict_def] "restrict(f,0) = 0";
 by (Simp_tac 1);
 qed "restrict_empty";
+Addsimps [restrict_empty];
 
-Addsimps [restrict, restrict_empty];
+Goalw [restrict_def, lam_def] "domain(restrict(Lambda(A,f),C)) = A Int C";
+by (rtac equalityI 1);  
+by (auto_tac (claset(), simpset() addsimps [domain_iff])); 
+qed "domain_restrict_lam";
+Addsimps [domain_restrict_lam];
 
-(*NOT SAFE as a congruence rule for the simplifier!  Can cause it to fail!*)
-val prems = Goalw [restrict_def]
-    "[| A=B;  !!x. x:B ==> f`x=g`x |] ==> restrict(f,A) = restrict(g,B)";
-by (REPEAT (ares_tac (prems@[lam_cong]) 1));
-qed "restrict_eqI";
+Goalw [restrict_def] "restrict(restrict(r,A),B) = restrict(r, A Int B)";
+by (Blast_tac 1); 
+qed "restrict_restrict";
+Addsimps [restrict_restrict];
 
-Goalw [restrict_def, lam_def] "domain(restrict(f,C)) = C";
-by (Blast_tac 1);
+Goalw [restrict_def] "domain(restrict(f,C)) = domain(f) Int C"; 
+by (auto_tac (claset(), simpset() addsimps [domain_def])); 
 qed "domain_restrict";
 Addsimps [domain_restrict];
 
-Goalw [restrict_def]
+Goal "f <= Sigma(A,B) ==> restrict(f,A) = f"; 
+by (asm_full_simp_tac (simpset() addsimps [restrict_def]) 1);  
+by (Blast_tac 1); 
+qed "restrict_idem";
+Addsimps [restrict_idem];
+
+Goal "restrict(f,A) ` a = (if a : A then f`a else 0)";
+by (asm_full_simp_tac (simpset() addsimps [restrict, apply_0]) 1); 
+qed "restrict_if";
+Addsimps [restrict_if];
+
+(*No longer true and no longer needed
+val prems = Goalw [restrict_def]
+    "[| A=B;  !!x. x:B ==> f`x=g`x |] ==> restrict(f,A) = restrict(g,B)";
+qed "restrict_eqI";
+*)
+
+Goalw [restrict_def, lam_def]
     "A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))";
-by (rtac (refl RS lam_cong) 1);
-by (set_mp_tac 1);
-by (Asm_simp_tac 1);
+by Auto_tac; 
 qed "restrict_lam_eq";
 
 Goal "f : cons(a, b) -> B ==> f = cons(<a, f ` a>, restrict(f, b))";