--- 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:
--- 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:
--- 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];
--- 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
--- 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!*)
--- 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 =
--- 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";
--- 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);
--- 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
--- 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";
--- 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))";