1.1 --- a/src/ZF/AC/AC17_AC1.thy Thu Feb 14 20:30:49 2002 +0100
1.2 +++ b/src/ZF/AC/AC17_AC1.thy Fri Feb 15 12:07:27 2002 +0100
1.3 @@ -15,7 +15,7 @@
1.4 AC0 comes from Suppes, AC1 from Rubin & Rubin **)
1.5
1.6 lemma AC0_AC1_lemma: "[| f:(\<Pi>X \<in> A. X); D \<subseteq> A |] ==> \<exists>g. g:(\<Pi>X \<in> D. X)"
1.7 -by (fast intro!: restrict_type apply_type)
1.8 +by (fast intro!: lam_type apply_type)
1.9
1.10 lemma AC0_AC1: "AC0 ==> AC1"
1.11 apply (unfold AC0_def AC1_def)
1.12 @@ -75,7 +75,7 @@
1.13 apply (rule allI)
1.14 apply (erule swap)
1.15 apply (rule_tac x = "Union (A)" in exI)
1.16 -apply (blast intro: restrict_type)
1.17 +apply (blast intro: lam_type)
1.18 done
1.19
1.20 lemma lemma1:
2.1 --- a/src/ZF/AC/DC.thy Thu Feb 14 20:30:49 2002 +0100
2.2 +++ b/src/ZF/AC/DC.thy Fri Feb 15 12:07:27 2002 +0100
2.3 @@ -57,12 +57,8 @@
2.4 by (simp add: domain_cons succ_def)
2.5
2.6 lemma restrict_cons_eq: "g \<in> n->X ==> restrict(cons(<n,x>, g), n) = g"
2.7 -apply (unfold restrict_def)
2.8 -apply (rule fun_extension)
2.9 -apply (rule lam_type)
2.10 -apply (erule cons_fun_type [THEN apply_type])
2.11 -apply (erule succI2, assumption)
2.12 -apply (simp add: cons_val_k)
2.13 +apply (simp add: restrict_def Pi_iff)
2.14 +apply (blast intro: elim: mem_irrefl)
2.15 done
2.16
2.17 lemma succ_in_succ: "[| Ord(k); i \<in> k |] ==> succ(i) \<in> succ(k)"
2.18 @@ -71,10 +67,9 @@
2.19 done
2.20
2.21 lemma restrict_eq_imp_val_eq:
2.22 - "[| restrict(f, domain(g)) = g; x \<in> domain(g) |] ==> f`x = g`x"
2.23 -apply (unfold restrict_def)
2.24 -apply (erule subst, simp)
2.25 -done
2.26 + "[|restrict(f, domain(g)) = g; x \<in> domain(g)|]
2.27 + ==> f`x = g`x"
2.28 +by (erule subst, simp add: restrict)
2.29
2.30 lemma domain_eq_imp_fun_type: "[| domain(f)=A; f \<in> B->C |] ==> f \<in> A->C"
2.31 by (frule domain_of_fun, fast)
2.32 @@ -220,7 +215,7 @@
2.33 apply (simp add: RR_def)
2.34 apply (drule lemma2, assumption+)
2.35 apply (blast dest!: domain_of_fun
2.36 - intro: nat_into_Ord OrdmemD [THEN subsetD])
2.37 + intro: nat_into_Ord OrdmemD [THEN subsetD])
2.38 done
2.39
2.40 lemma (in DC0_imp) lemma3:
2.41 @@ -370,11 +365,9 @@
2.42 "[| restrict(h, domain(u))=u; h \<in> n->X; domain(u) \<subseteq> n |]
2.43 ==> restrict(cons(<n, y>, h), domain(u)) = u"
2.44 apply (unfold restrict_def)
2.45 +apply (simp add: restrict_def Pi_iff)
2.46 apply (erule sym [THEN trans, symmetric])
2.47 -apply (rule fun_extension)
2.48 -apply (fast intro!: lam_type)
2.49 -apply (fast intro!: lam_type)
2.50 -apply (simp add: subsetD [THEN cons_val_k])
2.51 +apply (blast elim: mem_irrefl)
2.52 done
2.53
2.54 lemma (in imp_DC0) all_in_image_restrict_eq:
3.1 --- a/src/ZF/Induct/Multiset.ML Thu Feb 14 20:30:49 2002 +0100
3.2 +++ b/src/ZF/Induct/Multiset.ML Fri Feb 15 12:07:27 2002 +0100
3.3 @@ -1,4 +1,4 @@
3.4 -(* Title: ZF/Induct/Multiset.thy
3.5 +(* Title: ZF/Induct/Multiset
3.6 ID: $Id$
3.7 Author: Sidi O Ehmety, Cambridge University Computer Laboratory
3.8
3.9 @@ -9,6 +9,45 @@
3.10
3.11 *)
3.12
3.13 +(* Properties of the original "restrict" from ZF.thy. *)
3.14 +
3.15 +Goalw [funrestrict_def,lam_def]
3.16 + "[| f: Pi(C,B); A<=C |] ==> funrestrict(f,A) <= f";
3.17 +by (blast_tac (claset() addIs [apply_Pair]) 1);
3.18 +qed "funrestrict_subset";
3.19 +
3.20 +val prems = Goalw [funrestrict_def]
3.21 + "[| !!x. x:A ==> f`x: B(x) |] ==> funrestrict(f,A) : Pi(A,B)";
3.22 +by (rtac lam_type 1);
3.23 +by (eresolve_tac prems 1);
3.24 +qed "funrestrict_type";
3.25 +
3.26 +Goal "[| f: Pi(C,B); A<=C |] ==> funrestrict(f,A) : Pi(A,B)";
3.27 +by (blast_tac (claset() addIs [apply_type, funrestrict_type]) 1);
3.28 +qed "funrestrict_type2";
3.29 +
3.30 +Goalw [funrestrict_def] "a : A ==> funrestrict(f,A) ` a = f`a";
3.31 +by (etac beta 1);
3.32 +qed "funrestrict";
3.33 +
3.34 +Goalw [funrestrict_def] "funrestrict(f,0) = 0";
3.35 +by (Simp_tac 1);
3.36 +qed "funrestrict_empty";
3.37 +
3.38 +Addsimps [funrestrict, funrestrict_empty];
3.39 +
3.40 +Goalw [funrestrict_def, lam_def] "domain(funrestrict(f,C)) = C";
3.41 +by (Blast_tac 1);
3.42 +qed "domain_funrestrict";
3.43 +Addsimps [domain_funrestrict];
3.44 +
3.45 +Goal "f : cons(a, b) -> B ==> f = cons(<a, f ` a>, funrestrict(f, b))";
3.46 +by (rtac equalityI 1);
3.47 +by (blast_tac (claset() addIs [apply_Pair, impOfSubs funrestrict_subset]) 2);
3.48 +by (auto_tac (claset() addSDs [Pi_memberD],
3.49 + simpset() addsimps [funrestrict_def, lam_def]));
3.50 +qed "fun_cons_funrestrict_eq";
3.51 +
3.52 Addsimps [domain_of_fun];
3.53 Delrules [domainE];
3.54
3.55 @@ -146,7 +185,7 @@
3.56
3.57 (** normalize **)
3.58
3.59 -Goalw [normalize_def, restrict_def, mset_of_def]
3.60 +Goalw [normalize_def, funrestrict_def, mset_of_def]
3.61 "normalize(normalize(f)) = normalize(f)";
3.62 by Auto_tac;
3.63 qed "normalize_idem";
3.64 @@ -156,7 +195,7 @@
3.65 "multiset(M) ==> normalize(M) = M";
3.66 by (rewrite_goals_tac [normalize_def, mset_of_def]);
3.67 by (auto_tac (claset(), simpset()
3.68 - addsimps [restrict_def, multiset_fun_iff]));
3.69 + addsimps [funrestrict_def, multiset_fun_iff]));
3.70 qed "normalize_multiset";
3.71 Addsimps [normalize_multiset];
3.72
3.73 @@ -166,7 +205,7 @@
3.74 by Auto_tac;
3.75 by (res_inst_tac [("x", "{x:A . 0<f`x}")] exI 1);
3.76 by (auto_tac (claset() addIs [Collect_subset RS subset_Finite,
3.77 - restrict_type], simpset()));
3.78 + funrestrict_type], simpset()));
3.79 qed "normalize_multiset";
3.80
3.81 (** Typechecking rules for union and difference of multisets **)
3.82 @@ -243,7 +282,7 @@
3.83 Goalw [multiset_def] "multiset(M) ==> M -# 0 = M & 0 -# M = 0";
3.84 by (rewrite_goals_tac [mdiff_def, normalize_def]);
3.85 by (auto_tac (claset(), simpset()
3.86 - addsimps [multiset_fun_iff, mset_of_def, restrict_def]));
3.87 + addsimps [multiset_fun_iff, mset_of_def, funrestrict_def]));
3.88 qed "mdiff_0";
3.89 Addsimps [mdiff_0];
3.90
3.91 @@ -254,7 +293,7 @@
3.92 by (rtac fun_extension 1);
3.93 by Auto_tac;
3.94 by (res_inst_tac [("P", "%x. ?u : Pi(x, ?v)")] subst 1);
3.95 -by (rtac restrict_type 2);
3.96 +by (rtac funrestrict_type 2);
3.97 by (rtac equalityI 1);
3.98 by (ALLGOALS(Clarify_tac));
3.99 by Auto_tac;
3.100 @@ -512,7 +551,7 @@
3.101 Goalw [multiset_def]
3.102 "Finite(A) \
3.103 \ ==> ALL M. multiset(M) --> (ALL a:mset_of(M). \
3.104 -\ setsum(%x'. $# mcount(restrict(M, mset_of(M)-{a}), x'), A) = \
3.105 +\ setsum(%x'. $# mcount(funrestrict(M, mset_of(M)-{a}), x'), A) = \
3.106 \ (if a:A then setsum(%x'. $# mcount(M, x'), A) $- $# M`a \
3.107 \ else setsum(%x'. $# mcount(M, x'), A)))";
3.108 by (etac Finite_induct 1);
3.109 @@ -522,11 +561,11 @@
3.110 qed "setsum_decr2";
3.111
3.112 Goal "[| Finite(A); multiset(M); a:mset_of(M) |] \
3.113 -\ ==> setsum(%x. $# mcount(restrict(M, mset_of(M)-{a}), x), A - {a}) = \
3.114 +\ ==> setsum(%x. $# mcount(funrestrict(M, mset_of(M)-{a}), x), A - {a}) = \
3.115 \ (if a:A then setsum(%x. $# mcount(M, x), A) $- $# M`a\
3.116 \ else setsum(%x. $# mcount(M, x), A))";
3.117 -by (subgoal_tac "setsum(%x. $# mcount(restrict(M, mset_of(M)-{a}),x),A-{a}) = \
3.118 -\ setsum(%x. $# mcount(restrict(M, mset_of(M)-{a}),x),A)" 1);
3.119 +by (subgoal_tac "setsum(%x. $# mcount(funrestrict(M, mset_of(M)-{a}),x),A-{a}) = \
3.120 +\ setsum(%x. $# mcount(funrestrict(M, mset_of(M)-{a}),x),A)" 1);
3.121 by (rtac (setsum_Diff RS sym) 2);
3.122 by (REPEAT(asm_simp_tac (simpset() addsimps [mcount_def, mset_of_def]) 2));
3.123 by (rtac sym 1 THEN rtac ssubst 1);
3.124 @@ -599,34 +638,34 @@
3.125 by (rotate_simp_tac "cons(a, A) = A" 1);
3.126 by (rotate_simp_tac "ALL x:A. ?u(x)" 1);
3.127 by (rotate_simp_tac "ALL x:A. ?u(x)" 2);
3.128 -by (subgoal_tac "M=cons(<a, M`a>, restrict(M, A-{a}))" 1);
3.129 -by (rtac fun_cons_restrict_eq 2);
3.130 +by (subgoal_tac "M=cons(<a, M`a>, funrestrict(M, A-{a}))" 1);
3.131 +by (rtac fun_cons_funrestrict_eq 2);
3.132 by (subgoal_tac "cons(a, A-{a}) = A" 2);
3.133 by (REPEAT(Force_tac 2));
3.134 -by (res_inst_tac [("a", "cons(<a, 1>, restrict(M, A - {a}))")] ssubst 1);
3.135 +by (res_inst_tac [("a", "cons(<a, 1>, funrestrict(M, A - {a}))")] ssubst 1);
3.136 by (Asm_full_simp_tac 1);
3.137 -by (subgoal_tac "multiset(restrict(M, A - {a}))" 1);
3.138 +by (subgoal_tac "multiset(funrestrict(M, A - {a}))" 1);
3.139 by (simp_tac (simpset() addsimps [multiset_def, multiset_fun_iff]) 2);
3.140 by (res_inst_tac [("x", "A-{a}")] exI 2);
3.141 by Safe_tac;
3.142 by (res_inst_tac [("A", "A-{a}")] apply_type 3);
3.143 -by (asm_simp_tac (simpset() addsimps [restrict]) 5);
3.144 -by (REPEAT(blast_tac (claset() addIs [Finite_Diff, restrict_type]) 2));;
3.145 +by (asm_simp_tac (simpset() addsimps [funrestrict]) 5);
3.146 +by (REPEAT(blast_tac (claset() addIs [Finite_Diff, funrestrict_type]) 2));;
3.147 by (resolve_tac prems 1);
3.148 by (assume_tac 1);
3.149 by (asm_full_simp_tac (simpset() addsimps [mset_of_def]) 1);
3.150 -by (dres_inst_tac [("x", "restrict(M, A-{a})")] spec 1);
3.151 +by (dres_inst_tac [("x", "funrestrict(M, A-{a})")] spec 1);
3.152 by (dtac mp 1);
3.153 by (res_inst_tac [("x", "A-{a}")] exI 1);
3.154 -by (auto_tac (claset() addIs [Finite_Diff, restrict_type],
3.155 - simpset() addsimps [restrict]));
3.156 +by (auto_tac (claset() addIs [Finite_Diff, funrestrict_type],
3.157 + simpset() addsimps [funrestrict]));
3.158 by (forw_inst_tac [("A", "A"), ("M", "M"), ("a", "a")] setsum_decr3 1);
3.159 by (asm_simp_tac (simpset() addsimps [multiset_def, multiset_fun_iff]) 1);
3.160 by (Blast_tac 1);
3.161 by (asm_simp_tac (simpset() addsimps [mset_of_def]) 1);
3.162 by (dres_inst_tac [("b", "if ?u then ?v else ?w")] sym 1);
3.163 by (ALLGOALS(rotate_simp_tac "ALL x:A. ?u(x)"));
3.164 -by (subgoal_tac "{x:A - {a} . 0 < restrict(M, A - {x}) ` x} = A - {a}" 1);
3.165 +by (subgoal_tac "{x:A - {a} . 0 < funrestrict(M, A - {x}) ` x} = A - {a}" 1);
3.166 by (auto_tac (claset() addSIs [setsum_cong],
3.167 simpset() addsimps [zdiff_eq_iff,
3.168 zadd_commute, multiset_def, multiset_fun_iff,mset_of_def]));
3.169 @@ -703,7 +742,7 @@
3.170 by (res_inst_tac [("x", "{x:A. P(x)}")] exI 1);
3.171 by (auto_tac (claset() addDs [CollectD1 RSN (2,apply_type)]
3.172 addIs [Collect_subset RS subset_Finite,
3.173 - restrict_type],
3.174 + funrestrict_type],
3.175 simpset()));
3.176 qed "MCollect_multiset";
3.177 Addsimps [MCollect_multiset];
3.178 @@ -711,7 +750,7 @@
3.179 Goalw [mset_of_def, MCollect_def]
3.180 "multiset(M) ==> mset_of({# x:M. P(x) #}) <= mset_of(M)";
3.181 by (auto_tac (claset(),
3.182 - simpset() addsimps [multiset_def, restrict_def]));
3.183 + simpset() addsimps [multiset_def, funrestrict_def]));
3.184 qed "mset_of_MCollect";
3.185 Addsimps [mset_of_MCollect];
3.186
4.1 --- a/src/ZF/Induct/Multiset.thy Thu Feb 14 20:30:49 2002 +0100
4.2 +++ b/src/ZF/Induct/Multiset.thy Fri Feb 15 12:07:27 2002 +0100
4.3 @@ -16,6 +16,14 @@
4.4 "Mult(A)" => "A-||>nat-{0}"
4.5
4.6 constdefs
4.7 +
4.8 + (* This is the original "restrict" from ZF.thy.
4.9 + Restricts the function f to the domain A
4.10 + FIXME: adapt Multiset to the new "restrict". *)
4.11 +
4.12 + funrestrict :: "[i,i] => i"
4.13 + "funrestrict(f,A) == lam x:A. f`x"
4.14 +
4.15 (* M is a multiset *)
4.16 multiset :: i => o
4.17 "multiset(M) == EX A. M:A->nat-{0} & Finite(A)"
4.18 @@ -30,7 +38,7 @@
4.19
4.20 (* eliminating 0's from a function *)
4.21 normalize :: i => i
4.22 - "normalize(M) == restrict(M, {x:mset_of(M). 0<M`x})"
4.23 + "normalize(M) == funrestrict(M, {x:mset_of(M). 0<M`x})"
4.24
4.25 mdiff :: "[i, i] => i" (infixl "-#" 65)
4.26 "M -# N == normalize(lam x:mset_of(M).
4.27 @@ -41,7 +49,7 @@
4.28 "{#a#} == {<a, 1>}"
4.29
4.30 MCollect :: [i, i=>o] => i (*comprehension*)
4.31 - "MCollect(M, P) == restrict(M, {x:mset_of(M). P(x)})"
4.32 + "MCollect(M, P) == funrestrict(M, {x:mset_of(M). P(x)})"
4.33
4.34 (* Counts the number of occurences of an element in a multiset *)
4.35 mcount :: [i, i] => i
5.1 --- a/src/ZF/Order.ML Thu Feb 14 20:30:49 2002 +0100
5.2 +++ b/src/ZF/Order.ML Fri Feb 15 12:07:27 2002 +0100
5.3 @@ -402,11 +402,12 @@
5.4 Goal "[| f : ord_iso(A,r,B,s); a:A |] ==> \
5.5 \ restrict(f, pred(A,a,r)) : ord_iso(pred(A,a,r), r, pred(B, f`a, s), s)";
5.6 by (asm_simp_tac (simpset() addsimps [ord_iso_image_pred RS sym]) 1);
5.7 -by (rewtac ord_iso_def);
5.8 +by (rewtac ord_iso_def);
5.9 by (etac CollectE 1);
5.10 by (rtac CollectI 1);
5.11 -by (asm_full_simp_tac (simpset() addsimps [pred_def]) 2);
5.12 by (eresolve_tac [[bij_is_inj, pred_subset] MRS restrict_bij] 1);
5.13 +by (ftac bij_is_fun 1);
5.14 +by (auto_tac (claset(), simpset() addsimps [pred_def]));
5.15 qed "ord_iso_restrict_pred";
5.16
5.17 (*Tricky; a lot of forward proof!*)
6.1 --- a/src/ZF/OrderType.ML Thu Feb 14 20:30:49 2002 +0100
6.2 +++ b/src/ZF/OrderType.ML Fri Feb 15 12:07:27 2002 +0100
6.3 @@ -89,6 +89,22 @@
6.4 (*pred-unfolded version. NOT suitable for rewriting -- loops!*)
6.5 bind_thm ("ordermap_unfold", rewrite_rule [pred_def] ordermap_pred_unfold);
6.6
6.7 +(*The theorem above is
6.8 +
6.9 +[| wf[A](r); x : A |]
6.10 +==> ordermap(A,r) ` x = {ordermap(A,r) ` y . y: {y: A . <y,x> : r}}
6.11 +
6.12 +NOTE: the definition of ordermap used here delivers ordinals only if r is
6.13 +transitive. If r is the predecessor relation on the naturals then
6.14 +ordermap(nat,predr) ` n equals {n-1} and not n. A more complicated definition,
6.15 +like
6.16 +
6.17 + ordermap(A,r) ` x = Union{succ(ordermap(A,r) ` y) . y: {y: A . <y,x> : r}},
6.18 +
6.19 +might eliminate the need for r to be transitive.
6.20 +*)
6.21 +
6.22 +
6.23 (*** Showing that ordermap, ordertype yield ordinals ***)
6.24
6.25 fun ordermap_elim_tac i =
7.1 --- a/src/ZF/Perm.ML Thu Feb 14 20:30:49 2002 +0100
7.2 +++ b/src/ZF/Perm.ML Fri Feb 15 12:07:27 2002 +0100
7.3 @@ -497,9 +497,8 @@
7.4
7.5 Goal "[| f: Pi(C,B); A<=C |] ==> restrict(f,A)``A = f``A";
7.6 by (rtac equalityI 1);
7.7 -by (SELECT_GOAL (rewtac restrict_def) 2);
7.8 -by (REPEAT (eresolve_tac [imageE, apply_equality RS subst] 2
7.9 - ORELSE ares_tac [subsetI,lamI,imageI] 2));
7.10 +by (asm_full_simp_tac (simpset() addsimps [restrict_def]) 2);
7.11 +by (blast_tac (claset() addIs [apply_Pair]) 2);
7.12 by (REPEAT (ares_tac [image_mono,restrict_subset,subset_refl] 1));
7.13 qed "restrict_image";
7.14
8.1 --- a/src/ZF/WF.ML Thu Feb 14 20:30:49 2002 +0100
8.2 +++ b/src/ZF/WF.ML Fri Feb 15 12:07:27 2002 +0100
8.3 @@ -212,23 +212,29 @@
8.4 by (rtac (rel RS underI RS beta) 1);
8.5 qed "apply_recfun";
8.6
8.7 -Goalw [is_recfun_def]
8.8 - "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,b,H,g) |] ==> \
8.9 -\ <x,a>:r --> <x,b>:r --> f`x=g`x";
8.10 +Goal "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,b,H,g) |] \
8.11 +\ ==> <x,a>:r --> <x,b>:r --> f`x=g`x";
8.12 +by (forw_inst_tac [("f","f")] is_recfun_type 1);
8.13 +by (forw_inst_tac [("f","g")] is_recfun_type 1);
8.14 +by (asm_full_simp_tac (simpset() addsimps [is_recfun_def]) 1);
8.15 by (wf_ind_tac "x" [] 1);
8.16 by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
8.17 by (asm_simp_tac (simpset() addsimps [vimage_singleton_iff, restrict_def]) 1);
8.18 -by (subgoal_tac "ALL y. y : r-``{x1} --> f`y = g`y" 1);
8.19 - by (Asm_simp_tac 1);
8.20 -by (blast_tac (claset() addDs [transD]) 1);
8.21 +by (res_inst_tac [("t","%z. H(?x,z)")] subst_context 1);
8.22 +by (subgoal_tac "ALL y : r-``{x1}. ALL z. <y,z>:f <-> <y,z>:g" 1);
8.23 + by (blast_tac (claset() addDs [transD]) 1);
8.24 +by (asm_full_simp_tac (simpset() addsimps [apply_iff]) 1);
8.25 +by (blast_tac (claset() addDs [transD] addIs [sym]) 1);
8.26 qed_spec_mp "is_recfun_equal";
8.27
8.28 Goal "[| wf(r); trans(r); \
8.29 \ is_recfun(r,a,H,f); is_recfun(r,b,H,g); <b,a>:r |] \
8.30 \ ==> restrict(f, r-``{b}) = g";
8.31 -by (rtac (consI1 RS restrict_type RS fun_extension) 1);
8.32 -by (etac is_recfun_type 1);
8.33 -by (asm_full_simp_tac (simpset() addsimps [vimage_singleton_iff]) 1);
8.34 +by (forw_inst_tac [("f","f")] is_recfun_type 1);
8.35 +by (rtac fun_extension 1);
8.36 + by (blast_tac (claset() addDs [transD] addIs [restrict_type2]) 1);
8.37 + by (etac is_recfun_type 1);
8.38 +by (Asm_full_simp_tac 1);
8.39 by (blast_tac (claset() addDs [transD]
8.40 addIs [is_recfun_equal]) 1);
8.41 qed "is_recfun_cut";
8.42 @@ -236,9 +242,8 @@
8.43 (*** Main Existence Lemma ***)
8.44
8.45 Goal "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |] ==> f=g";
8.46 -by (rtac fun_extension 1);
8.47 -by (REPEAT (ares_tac [is_recfun_equal] 1
8.48 - ORELSE eresolve_tac [is_recfun_type,underD] 1));
8.49 +by (blast_tac (claset() addIs [fun_extension, is_recfun_type,
8.50 + is_recfun_equal]) 1);
8.51 qed "is_recfun_functional";
8.52
8.53 (*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *)
8.54 @@ -257,8 +262,12 @@
8.55 (*Applying the substitution: must keep the quantified assumption!!*)
8.56 by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong] 1));
8.57 by (fold_tac [is_recfun_def]);
8.58 -by (rtac (consI1 RS restrict_type RSN (2,fun_extension) RS subst_context) 1);
8.59 - by (blast_tac (claset() addIs [is_recfun_type]) 1);
8.60 +by (res_inst_tac [("t","%z. H(?x,z)")] subst_context 1);
8.61 +by (rtac fun_extension 1);
8.62 + by (blast_tac (claset() addIs [is_recfun_type]) 1);
8.63 + by (rtac (lam_type RS restrict_type2) 1);
8.64 + by (Blast_tac 1);
8.65 + by (blast_tac (claset() addDs [transD]) 1);
8.66 by (ftac (spec RS mp) 1 THEN assume_tac 1);
8.67 by (subgoal_tac "<xa,a1> : r" 1);
8.68 by (dres_inst_tac [("x1","xa")] (spec RS mp) 1 THEN assume_tac 1);
9.1 --- a/src/ZF/ZF.thy Thu Feb 14 20:30:49 2002 +0100
9.2 +++ b/src/ZF/ZF.thy Fri Feb 15 12:07:27 2002 +0100
9.3 @@ -262,8 +262,8 @@
9.4 apply_def "f`a == THE y. <a,y> : f"
9.5 Pi_def "Pi(A,B) == {f: Pow(Sigma(A,B)). A<=domain(f) & function(f)}"
9.6
9.7 - (* Restrict the function f to the domain A *)
9.8 - restrict_def "restrict(f,A) == lam x:A. f`x"
9.9 + (* Restrict the relation r to the domain A *)
9.10 + restrict_def "restrict(r,A) == {z : r. EX x:A. EX y. z = <x,y>}"
9.11
9.12 end
9.13
10.1 --- a/src/ZF/equalities.ML Thu Feb 14 20:30:49 2002 +0100
10.2 +++ b/src/ZF/equalities.ML Fri Feb 15 12:07:27 2002 +0100
10.3 @@ -750,3 +750,16 @@
10.4 by (simp_tac (simpset() addsplits [split_if]) 1);
10.5 by (Blast_tac 1);
10.6 qed "Collect_cons";
10.7 +
10.8 +Goal "A Int Collect(A,P) = Collect(A,P)";
10.9 +by (Blast_tac 1);
10.10 +qed "Int_Collect_self_eq";
10.11 +
10.12 +Goal "Collect(Collect(A,P), Q) = Collect(A, %x. P(x) & Q(x))";
10.13 +by (Blast_tac 1);
10.14 +qed "Collect_Collect_eq";
10.15 +Addsimps [Collect_Collect_eq];
10.16 +
10.17 +Goal "Collect(A,P) Int Collect(A,Q) = Collect(A, %x. P(x) & Q(x))";
10.18 +by (Blast_tac 1);
10.19 +qed "Collect_Int_Collect_eq";
11.1 --- a/src/ZF/func.ML Thu Feb 14 20:30:49 2002 +0100
11.2 +++ b/src/ZF/func.ML Fri Feb 15 12:07:27 2002 +0100
11.3 @@ -291,47 +291,78 @@
11.4
11.5 (*** properties of "restrict" ***)
11.6
11.7 -Goalw [restrict_def,lam_def]
11.8 +Goalw [restrict_def]
11.9 "[| f: Pi(C,B); A<=C |] ==> restrict(f,A) <= f";
11.10 by (blast_tac (claset() addIs [apply_Pair]) 1);
11.11 qed "restrict_subset";
11.12
11.13 -val prems = Goalw [restrict_def]
11.14 - "[| !!x. x:A ==> f`x: B(x) |] ==> restrict(f,A) : Pi(A,B)";
11.15 -by (rtac lam_type 1);
11.16 -by (eresolve_tac prems 1);
11.17 -qed "restrict_type";
11.18 +Goalw [restrict_def, function_def]
11.19 + "function(f) ==> function(restrict(f,A))";
11.20 +by (Blast_tac 1);
11.21 +qed "function_restrictI";
11.22
11.23 Goal "[| f: Pi(C,B); A<=C |] ==> restrict(f,A) : Pi(A,B)";
11.24 -by (blast_tac (claset() addIs [apply_type, restrict_type]) 1);
11.25 +by (asm_full_simp_tac
11.26 + (simpset() addsimps [Pi_iff, function_def, restrict_def]) 1);
11.27 +by (Blast_tac 1);
11.28 qed "restrict_type2";
11.29
11.30 -Goalw [restrict_def] "a : A ==> restrict(f,A) ` a = f`a";
11.31 -by (etac beta 1);
11.32 +(*Fails with the new definition of restrict
11.33 + "[| !!x. x:A ==> f`x: B(x) |] ==> restrict(f,A) : Pi(A,B)";
11.34 +qed "restrict_type";
11.35 +*)
11.36 +
11.37 +(*FIXME: move to FOL?*)
11.38 +Goal "EX x. a = x";
11.39 +by Auto_tac;
11.40 +qed "ex_equals_triv";
11.41 +
11.42 +Goal "a : A ==> restrict(f,A) ` a = f`a";
11.43 +by (asm_full_simp_tac
11.44 + (simpset() addsimps [apply_def, restrict_def, ex_equals_triv]) 1);
11.45 qed "restrict";
11.46
11.47 Goalw [restrict_def] "restrict(f,0) = 0";
11.48 by (Simp_tac 1);
11.49 qed "restrict_empty";
11.50 +Addsimps [restrict_empty];
11.51
11.52 -Addsimps [restrict, restrict_empty];
11.53 +Goalw [restrict_def, lam_def] "domain(restrict(Lambda(A,f),C)) = A Int C";
11.54 +by (rtac equalityI 1);
11.55 +by (auto_tac (claset(), simpset() addsimps [domain_iff]));
11.56 +qed "domain_restrict_lam";
11.57 +Addsimps [domain_restrict_lam];
11.58
11.59 -(*NOT SAFE as a congruence rule for the simplifier! Can cause it to fail!*)
11.60 -val prems = Goalw [restrict_def]
11.61 - "[| A=B; !!x. x:B ==> f`x=g`x |] ==> restrict(f,A) = restrict(g,B)";
11.62 -by (REPEAT (ares_tac (prems@[lam_cong]) 1));
11.63 -qed "restrict_eqI";
11.64 +Goalw [restrict_def] "restrict(restrict(r,A),B) = restrict(r, A Int B)";
11.65 +by (Blast_tac 1);
11.66 +qed "restrict_restrict";
11.67 +Addsimps [restrict_restrict];
11.68
11.69 -Goalw [restrict_def, lam_def] "domain(restrict(f,C)) = C";
11.70 -by (Blast_tac 1);
11.71 +Goalw [restrict_def] "domain(restrict(f,C)) = domain(f) Int C";
11.72 +by (auto_tac (claset(), simpset() addsimps [domain_def]));
11.73 qed "domain_restrict";
11.74 Addsimps [domain_restrict];
11.75
11.76 -Goalw [restrict_def]
11.77 +Goal "f <= Sigma(A,B) ==> restrict(f,A) = f";
11.78 +by (asm_full_simp_tac (simpset() addsimps [restrict_def]) 1);
11.79 +by (Blast_tac 1);
11.80 +qed "restrict_idem";
11.81 +Addsimps [restrict_idem];
11.82 +
11.83 +Goal "restrict(f,A) ` a = (if a : A then f`a else 0)";
11.84 +by (asm_full_simp_tac (simpset() addsimps [restrict, apply_0]) 1);
11.85 +qed "restrict_if";
11.86 +Addsimps [restrict_if];
11.87 +
11.88 +(*No longer true and no longer needed
11.89 +val prems = Goalw [restrict_def]
11.90 + "[| A=B; !!x. x:B ==> f`x=g`x |] ==> restrict(f,A) = restrict(g,B)";
11.91 +qed "restrict_eqI";
11.92 +*)
11.93 +
11.94 +Goalw [restrict_def, lam_def]
11.95 "A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))";
11.96 -by (rtac (refl RS lam_cong) 1);
11.97 -by (set_mp_tac 1);
11.98 -by (Asm_simp_tac 1);
11.99 +by Auto_tac;
11.100 qed "restrict_lam_eq";
11.101
11.102 Goal "f : cons(a, b) -> B ==> f = cons(<a, f ` a>, restrict(f, b))";