1.1 --- a/src/ZF/AC/AC7_AC9.ML Mon Aug 17 13:06:29 1998 +0200
1.2 +++ b/src/ZF/AC/AC7_AC9.ML Mon Aug 17 13:09:08 1998 +0200
1.3 @@ -13,13 +13,10 @@
1.4 (* - Sigma_fun_space_eqpoll *)
1.5 (* ********************************************************************** *)
1.6
1.7 -goal ZF.thy "!!A. [| C~:A; B:A |] ==> B~=C";
1.8 -by (Fast_tac 1);
1.9 -qed "mem_not_eq_not_mem";
1.10 -
1.11 Goal "[| 0~:A; B:A |] ==> (nat->Union(A))*B ~= 0";
1.12 -by (blast_tac (claset() addSDs [Sigma_empty_iff RS iffD1]
1.13 - addDs [fun_space_emptyD, mem_not_eq_not_mem]) 1);
1.14 +by (blast_tac (claset() addSDs [Sigma_empty_iff RS iffD1,
1.15 + Union_empty_iff RS iffD1]
1.16 + addDs [fun_space_emptyD]) 1);
1.17 qed "Sigma_fun_space_not0";
1.18
1.19 Goal "(ALL B:A. B eqpoll C) ==> (ALL B1:A. ALL B2:A. B1 eqpoll B2)";
2.1 --- a/src/ZF/AC/AC_Equiv.ML Mon Aug 17 13:06:29 1998 +0200
2.2 +++ b/src/ZF/AC/AC_Equiv.ML Mon Aug 17 13:09:08 1998 +0200
2.3 @@ -44,8 +44,7 @@
2.4
2.5 (* used only in WO1_DC.ML *)
2.6 (*Note simpler proof*)
2.7 -goal ZF.thy "!!A f g. [| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg; \
2.8 -\ A<=Df; A<=Dg |] ==> f``A=g``A";
2.9 +Goal "[| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg; A<=Df; A<=Dg |] ==> f``A=g``A";
2.10 by (asm_simp_tac (simpset() addsimps [image_fun]) 1);
2.11 qed "images_eq";
2.12
3.1 --- a/src/ZF/AC/WO6_WO1.ML Mon Aug 17 13:06:29 1998 +0200
3.2 +++ b/src/ZF/AC/WO6_WO1.ML Mon Aug 17 13:09:08 1998 +0200
3.3 @@ -172,9 +172,8 @@
3.4 by (fast_tac (claset() addSEs [LeastI, lt_Ord]) 1);
3.5 qed "uu_not_empty";
3.6
3.7 -goal ZF.thy "!!r. [| r<=A*B; r~=0 |] ==> domain(r)~=0";
3.8 -by (REPEAT (eresolve_tac [asm_rl, not_emptyE, subsetD RS SigmaE,
3.9 - sym RSN (2, subst_elem) RS domainI RS not_emptyI] 1));
3.10 +Goal "[| r<=A*B; r~=0 |] ==> domain(r)~=0";
3.11 +by (Blast_tac 1);
3.12 qed "not_empty_rel_imp_domain";
3.13
3.14 Goal "[| b<a; g<a; f`b~=0; f`g~=0; \
3.15 @@ -186,7 +185,7 @@
3.16 THEN (REPEAT (ares_tac [lt_Ord] 1)));
3.17 qed "Least_uu_not_empty_lt_a";
3.18
3.19 -goal ZF.thy "!!B. [| B<=A; a~:B |] ==> B <= A-{a}";
3.20 +Goal "[| B<=A; a~:B |] ==> B <= A-{a}";
3.21 by (Blast_tac 1);
3.22 qed "subset_Diff_sing";
3.23
3.24 @@ -194,14 +193,11 @@
3.25 Goal "[| A lepoll m; m lepoll B; B <= A; m:nat |] ==> A=B";
3.26 by (etac natE 1);
3.27 by (fast_tac (claset() addSDs [lepoll_0_is_0] addSIs [equalityI]) 1);
3.28 -by (hyp_subst_tac 1);
3.29 -by (rtac equalityI 1);
3.30 -by (assume_tac 2);
3.31 -by (rtac subsetI 1);
3.32 -by (excluded_middle_tac "?P" 1 THEN (assume_tac 2));
3.33 -by (eresolve_tac [subset_Diff_sing RS subset_imp_lepoll RSN (2,
3.34 - Diff_sing_lepoll RSN (3, lepoll_trans RS lepoll_trans)) RS
3.35 - succ_lepoll_natE] 1
3.36 +by (safe_tac (claset() addSIs [equalityI]));
3.37 +by (rtac ccontr 1);
3.38 +by (etac (subset_Diff_sing RS subset_imp_lepoll
3.39 + RSN (2, Diff_sing_lepoll RSN (3, lepoll_trans RS lepoll_trans)) RS
3.40 + succ_lepoll_natE) 1
3.41 THEN REPEAT (assume_tac 1));
3.42 qed "supset_lepoll_imp_eq";
3.43
4.1 --- a/src/ZF/Arith.ML Mon Aug 17 13:06:29 1998 +0200
4.2 +++ b/src/ZF/Arith.ML Mon Aug 17 13:09:08 1998 +0200
4.3 @@ -34,7 +34,7 @@
4.4
4.5 Addsimps [rec_0, rec_succ];
4.6
4.7 -val major::prems = goal Arith.thy
4.8 +val major::prems = Goal
4.9 "[| n: nat; \
4.10 \ a: C(0); \
4.11 \ !!m z. [| m: nat; z: C(m) |] ==> b(m,z): C(succ(m)) \
4.12 @@ -467,7 +467,7 @@
4.13 qed "add_lt_mono";
4.14
4.15 (*A [clumsy] way of lifting < monotonicity to le monotonicity *)
4.16 -val lt_mono::ford::prems = goal Ordinal.thy
4.17 +val lt_mono::ford::prems = Goal
4.18 "[| !!i j. [| i<j; j:k |] ==> f(i) < f(j); \
4.19 \ !!i. i:k ==> Ord(f(i)); \
4.20 \ i le j; j:k \
5.1 --- a/src/ZF/Cardinal.ML Mon Aug 17 13:06:29 1998 +0200
5.2 +++ b/src/ZF/Cardinal.ML Mon Aug 17 13:09:08 1998 +0200
5.3 @@ -29,16 +29,15 @@
5.4 gfun RS fun_is_rel RS image_subset]) 1);
5.5 qed "Banach_last_equation";
5.6
5.7 -val prems = goal Cardinal.thy
5.8 - "[| f: X->Y; g: Y->X |] ==> \
5.9 -\ EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) & \
5.10 -\ (YA Int YB = 0) & (YA Un YB = Y) & \
5.11 -\ f``XA=YA & g``YB=XB";
5.12 +Goal "[| f: X->Y; g: Y->X |] ==> \
5.13 +\ EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) & \
5.14 +\ (YA Int YB = 0) & (YA Un YB = Y) & \
5.15 +\ f``XA=YA & g``YB=XB";
5.16 by (REPEAT
5.17 (FIRSTGOAL
5.18 (resolve_tac [refl, exI, conjI, Diff_disjoint, Diff_partition])));
5.19 by (rtac Banach_last_equation 3);
5.20 -by (REPEAT (resolve_tac (prems@[fun_is_rel, image_subset, lfp_subset]) 1));
5.21 +by (REPEAT (ares_tac [fun_is_rel, image_subset, lfp_subset] 1));
5.22 qed "decomposition";
5.23
5.24 val prems = goal Cardinal.thy
5.25 @@ -740,7 +739,7 @@
5.26 (*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered
5.27 set is well-ordered. Proofs simplified by lcp. *)
5.28
5.29 -goal Nat.thy "!!n. n:nat ==> wf[n](converse(Memrel(n)))";
5.30 +Goal "n:nat ==> wf[n](converse(Memrel(n)))";
5.31 by (etac nat_induct 1);
5.32 by (blast_tac (claset() addIs [wf_onI]) 1);
5.33 by (rtac wf_onI 1);
6.1 --- a/src/ZF/CardinalArith.ML Mon Aug 17 13:06:29 1998 +0200
6.2 +++ b/src/ZF/CardinalArith.ML Mon Aug 17 13:09:08 1998 +0200
6.3 @@ -380,8 +380,8 @@
6.4 (*** An infinite cardinal equals its square (Kunen, Thm 10.12, page 29) ***)
6.5
6.6 (*A general fact about ordermap*)
6.7 -goalw Cardinal.thy [eqpoll_def]
6.8 - "!!A. [| well_ord(A,r); x:A |] ==> ordermap(A,r)`x eqpoll pred(A,x,r)";
6.9 +Goalw [eqpoll_def]
6.10 + "[| well_ord(A,r); x:A |] ==> ordermap(A,r)`x eqpoll pred(A,x,r)";
6.11 by (rtac exI 1);
6.12 by (asm_simp_tac (simpset() addsimps [ordermap_eq_image, well_ord_is_wf]) 1);
6.13 by (etac (ordermap_bij RS bij_is_inj RS restrict_bij RS bij_converse_bij) 1);
6.14 @@ -808,7 +808,3 @@
6.15 addsimps [nat_cadd_eq_add RS sym, cadd_def, eqpoll_refl]) 1);
6.16 qed "nat_sum_eqpoll_sum";
6.17
6.18 -goal Nat.thy "!!m. [| m le n; n:nat |] ==> m:nat";
6.19 -by (blast_tac (claset() addSDs [lt_nat_in_nat]) 1);
6.20 -qed "le_in_nat";
6.21 -
7.1 --- a/src/ZF/Nat.ML Mon Aug 17 13:06:29 1998 +0200
7.2 +++ b/src/ZF/Nat.ML Mon Aug 17 13:09:08 1998 +0200
7.3 @@ -125,6 +125,10 @@
7.4 by (assume_tac 1);
7.5 qed "lt_nat_in_nat";
7.6
7.7 +Goal "[| m le n; n:nat |] ==> m:nat";
7.8 +by (blast_tac (claset() addSDs [lt_nat_in_nat]) 1);
7.9 +qed "le_in_nat";
7.10 +
7.11
7.12 (** Variations on mathematical induction **)
7.13
8.1 --- a/src/ZF/Sum.thy Mon Aug 17 13:06:29 1998 +0200
8.2 +++ b/src/ZF/Sum.thy Mon Aug 17 13:09:08 1998 +0200
8.3 @@ -7,7 +7,7 @@
8.4 "Part" primitive for simultaneous recursive type definitions
8.5 *)
8.6
8.7 -Sum = Bool + pair +
8.8 +Sum = Bool + equalities +
8.9
8.10 global
8.11
9.1 --- a/src/ZF/domrange.ML Mon Aug 17 13:06:29 1998 +0200
9.2 +++ b/src/ZF/domrange.ML Mon Aug 17 13:09:08 1998 +0200
9.3 @@ -8,19 +8,19 @@
9.4
9.5 (*** converse ***)
9.6
9.7 -qed_goalw "converse_iff" ZF.thy [converse_def]
9.8 +qed_goalw "converse_iff" thy [converse_def]
9.9 "<a,b>: converse(r) <-> <b,a>:r"
9.10 (fn _ => [ (Blast_tac 1) ]);
9.11
9.12 -qed_goalw "converseI" ZF.thy [converse_def]
9.13 +qed_goalw "converseI" thy [converse_def]
9.14 "!!a b r. <a,b>:r ==> <b,a>:converse(r)"
9.15 (fn _ => [ (Blast_tac 1) ]);
9.16
9.17 -qed_goalw "converseD" ZF.thy [converse_def]
9.18 +qed_goalw "converseD" thy [converse_def]
9.19 "!!a b r. <a,b> : converse(r) ==> <b,a> : r"
9.20 (fn _ => [ (Blast_tac 1) ]);
9.21
9.22 -qed_goalw "converseE" ZF.thy [converse_def]
9.23 +qed_goalw "converseE" thy [converse_def]
9.24 "[| yx : converse(r); \
9.25 \ !!x y. [| yx=<y,x>; <x,y>:r |] ==> P \
9.26 \ |] ==> P"
9.27 @@ -34,36 +34,36 @@
9.28 AddSIs [converseI];
9.29 AddSEs [converseD,converseE];
9.30
9.31 -qed_goal "converse_converse" ZF.thy
9.32 +qed_goal "converse_converse" thy
9.33 "!!A B r. r<=Sigma(A,B) ==> converse(converse(r)) = r"
9.34 (fn _ => [ (Blast_tac 1) ]);
9.35
9.36 -qed_goal "converse_type" ZF.thy "!!A B r. r<=A*B ==> converse(r)<=B*A"
9.37 +qed_goal "converse_type" thy "!!A B r. r<=A*B ==> converse(r)<=B*A"
9.38 (fn _ => [ (Blast_tac 1) ]);
9.39
9.40 -qed_goal "converse_prod" ZF.thy "converse(A*B) = B*A"
9.41 +qed_goal "converse_prod" thy "converse(A*B) = B*A"
9.42 (fn _ => [ (Blast_tac 1) ]);
9.43
9.44 -qed_goal "converse_empty" ZF.thy "converse(0) = 0"
9.45 +qed_goal "converse_empty" thy "converse(0) = 0"
9.46 (fn _ => [ (Blast_tac 1) ]);
9.47
9.48 Addsimps [converse_prod, converse_empty];
9.49
9.50 -val converse_subset_iff = prove_goal ZF.thy
9.51 +val converse_subset_iff = prove_goal thy
9.52 "!!z. A <= Sigma(X,Y) ==> converse(A) <= converse(B) <-> A <= B"
9.53 (fn _=> [ (Blast_tac 1) ]);
9.54
9.55
9.56 (*** domain ***)
9.57
9.58 -qed_goalw "domain_iff" ZF.thy [domain_def]
9.59 +qed_goalw "domain_iff" thy [domain_def]
9.60 "a: domain(r) <-> (EX y. <a,y>: r)"
9.61 (fn _=> [ (Blast_tac 1) ]);
9.62
9.63 -qed_goal "domainI" ZF.thy "!!a b r. <a,b>: r ==> a: domain(r)"
9.64 +qed_goal "domainI" thy "!!a b r. <a,b>: r ==> a: domain(r)"
9.65 (fn _=> [ (etac (exI RS (domain_iff RS iffD2)) 1) ]);
9.66
9.67 -qed_goal "domainE" ZF.thy
9.68 +qed_goal "domainE" thy
9.69 "[| a : domain(r); !!y. <a,y>: r ==> P |] ==> P"
9.70 (fn prems=>
9.71 [ (rtac (domain_iff RS iffD1 RS exE) 1),
9.72 @@ -72,15 +72,15 @@
9.73 AddIs [domainI];
9.74 AddSEs [domainE];
9.75
9.76 -qed_goal "domain_subset" ZF.thy "domain(Sigma(A,B)) <= A"
9.77 +qed_goal "domain_subset" thy "domain(Sigma(A,B)) <= A"
9.78 (fn _=> [ (Blast_tac 1) ]);
9.79
9.80 (*** range ***)
9.81
9.82 -qed_goalw "rangeI" ZF.thy [range_def] "!!a b r.<a,b>: r ==> b : range(r)"
9.83 +qed_goalw "rangeI" thy [range_def] "!!a b r.<a,b>: r ==> b : range(r)"
9.84 (fn _ => [ (etac (converseI RS domainI) 1) ]);
9.85
9.86 -qed_goalw "rangeE" ZF.thy [range_def]
9.87 +qed_goalw "rangeE" thy [range_def]
9.88 "[| b : range(r); !!x. <x,b>: r ==> P |] ==> P"
9.89 (fn major::prems=>
9.90 [ (rtac (major RS domainE) 1),
9.91 @@ -90,7 +90,7 @@
9.92 AddIs [rangeI];
9.93 AddSEs [rangeE];
9.94
9.95 -qed_goalw "range_subset" ZF.thy [range_def] "range(A*B) <= B"
9.96 +qed_goalw "range_subset" thy [range_def] "range(A*B) <= B"
9.97 (fn _ =>
9.98 [ (stac converse_prod 1),
9.99 (rtac domain_subset 1) ]);
9.100 @@ -98,17 +98,17 @@
9.101
9.102 (*** field ***)
9.103
9.104 -qed_goalw "fieldI1" ZF.thy [field_def] "!!r. <a,b>: r ==> a : field(r)"
9.105 +qed_goalw "fieldI1" thy [field_def] "!!r. <a,b>: r ==> a : field(r)"
9.106 (fn _ => [ (Blast_tac 1) ]);
9.107
9.108 -qed_goalw "fieldI2" ZF.thy [field_def] "!!r. <a,b>: r ==> b : field(r)"
9.109 +qed_goalw "fieldI2" thy [field_def] "!!r. <a,b>: r ==> b : field(r)"
9.110 (fn _ => [ (Blast_tac 1) ]);
9.111
9.112 -qed_goalw "fieldCI" ZF.thy [field_def]
9.113 +qed_goalw "fieldCI" thy [field_def]
9.114 "(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)"
9.115 (fn [prem]=> [ (blast_tac (claset() addIs [prem]) 1) ]);
9.116
9.117 -qed_goalw "fieldE" ZF.thy [field_def]
9.118 +qed_goalw "fieldE" thy [field_def]
9.119 "[| a : field(r); \
9.120 \ !!x. <a,x>: r ==> P; \
9.121 \ !!x. <x,a>: r ==> P |] ==> P"
9.122 @@ -119,40 +119,40 @@
9.123 AddIs [fieldCI];
9.124 AddSEs [fieldE];
9.125
9.126 -qed_goal "field_subset" ZF.thy "field(A*B) <= A Un B"
9.127 +qed_goal "field_subset" thy "field(A*B) <= A Un B"
9.128 (fn _ => [ (Blast_tac 1) ]);
9.129
9.130 -qed_goalw "domain_subset_field" ZF.thy [field_def]
9.131 +qed_goalw "domain_subset_field" thy [field_def]
9.132 "domain(r) <= field(r)"
9.133 (fn _ => [ (rtac Un_upper1 1) ]);
9.134
9.135 -qed_goalw "range_subset_field" ZF.thy [field_def]
9.136 +qed_goalw "range_subset_field" thy [field_def]
9.137 "range(r) <= field(r)"
9.138 (fn _ => [ (rtac Un_upper2 1) ]);
9.139
9.140 -qed_goal "domain_times_range" ZF.thy
9.141 +qed_goal "domain_times_range" thy
9.142 "!!A B r. r <= Sigma(A,B) ==> r <= domain(r)*range(r)"
9.143 (fn _ => [ (Blast_tac 1) ]);
9.144
9.145 -qed_goal "field_times_field" ZF.thy
9.146 +qed_goal "field_times_field" thy
9.147 "!!A B r. r <= Sigma(A,B) ==> r <= field(r)*field(r)"
9.148 (fn _ => [ (Blast_tac 1) ]);
9.149
9.150
9.151 (*** Image of a set under a function/relation ***)
9.152
9.153 -qed_goalw "image_iff" ZF.thy [image_def] "b : r``A <-> (EX x:A. <x,b>:r)"
9.154 +qed_goalw "image_iff" thy [image_def] "b : r``A <-> (EX x:A. <x,b>:r)"
9.155 (fn _ => [ (Blast_tac 1) ]);
9.156
9.157 -qed_goal "image_singleton_iff" ZF.thy "b : r``{a} <-> <a,b>:r"
9.158 +qed_goal "image_singleton_iff" thy "b : r``{a} <-> <a,b>:r"
9.159 (fn _ => [ rtac (image_iff RS iff_trans) 1,
9.160 Blast_tac 1 ]);
9.161
9.162 -qed_goalw "imageI" ZF.thy [image_def]
9.163 +qed_goalw "imageI" thy [image_def]
9.164 "!!a b r. [| <a,b>: r; a:A |] ==> b : r``A"
9.165 (fn _ => [ (Blast_tac 1) ]);
9.166
9.167 -qed_goalw "imageE" ZF.thy [image_def]
9.168 +qed_goalw "imageE" thy [image_def]
9.169 "[| b: r``A; !!x.[| <x,b>: r; x:A |] ==> P |] ==> P"
9.170 (fn major::prems=>
9.171 [ (rtac (major RS CollectE) 1),
9.172 @@ -161,32 +161,32 @@
9.173 AddIs [imageI];
9.174 AddSEs [imageE];
9.175
9.176 -qed_goal "image_subset" ZF.thy "!!A B r. r <= A*B ==> r``C <= B"
9.177 +qed_goal "image_subset" thy "!!A B r. r <= A*B ==> r``C <= B"
9.178 (fn _ => [ (Blast_tac 1) ]);
9.179
9.180
9.181 (*** Inverse image of a set under a function/relation ***)
9.182
9.183 -qed_goalw "vimage_iff" ZF.thy [vimage_def,image_def,converse_def]
9.184 +qed_goalw "vimage_iff" thy [vimage_def,image_def,converse_def]
9.185 "a : r-``B <-> (EX y:B. <a,y>:r)"
9.186 (fn _ => [ (Blast_tac 1) ]);
9.187
9.188 -qed_goal "vimage_singleton_iff" ZF.thy
9.189 +qed_goal "vimage_singleton_iff" thy
9.190 "a : r-``{b} <-> <a,b>:r"
9.191 (fn _ => [ rtac (vimage_iff RS iff_trans) 1,
9.192 Blast_tac 1 ]);
9.193
9.194 -qed_goalw "vimageI" ZF.thy [vimage_def]
9.195 +qed_goalw "vimageI" thy [vimage_def]
9.196 "!!A B r. [| <a,b>: r; b:B |] ==> a : r-``B"
9.197 (fn _ => [ (Blast_tac 1) ]);
9.198
9.199 -qed_goalw "vimageE" ZF.thy [vimage_def]
9.200 +qed_goalw "vimageE" thy [vimage_def]
9.201 "[| a: r-``B; !!x.[| <a,x>: r; x:B |] ==> P |] ==> P"
9.202 (fn major::prems=>
9.203 [ (rtac (major RS imageE) 1),
9.204 (REPEAT (etac converseD 1 ORELSE ares_tac prems 1)) ]);
9.205
9.206 -qed_goalw "vimage_subset" ZF.thy [vimage_def]
9.207 +qed_goalw "vimage_subset" thy [vimage_def]
9.208 "!!A B r. r <= A*B ==> r-``C <= A"
9.209 (fn _ => [ (etac (converse_type RS image_subset) 1) ]);
9.210
9.211 @@ -199,22 +199,22 @@
9.212 val ZF_cs = claset() delrules [equalityI];
9.213
9.214 (** The Union of a set of relations is a relation -- Lemma for fun_Union **)
9.215 -goal ZF.thy "!!S. (ALL x:S. EX A B. x <= A*B) ==> \
9.216 +Goal "(ALL x:S. EX A B. x <= A*B) ==> \
9.217 \ Union(S) <= domain(Union(S)) * range(Union(S))";
9.218 by (Blast_tac 1);
9.219 qed "rel_Union";
9.220
9.221 (** The Union of 2 relations is a relation (Lemma for fun_Un) **)
9.222 -qed_goal "rel_Un" ZF.thy
9.223 +qed_goal "rel_Un" thy
9.224 "!!r s. [| r <= A*B; s <= C*D |] ==> (r Un s) <= (A Un C) * (B Un D)"
9.225 (fn _ => [ (Blast_tac 1) ]);
9.226
9.227
9.228 -goal ZF.thy "!!r. [| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)";
9.229 +Goal "[| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)";
9.230 by (Blast_tac 1);
9.231 qed "domain_Diff_eq";
9.232
9.233 -goal ZF.thy "!!r. [| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)";
9.234 +Goal "[| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)";
9.235 by (Blast_tac 1);
9.236 qed "range_Diff_eq";
9.237
10.1 --- a/src/ZF/domrange.thy Mon Aug 17 13:06:29 1998 +0200
10.2 +++ b/src/ZF/domrange.thy Mon Aug 17 13:09:08 1998 +0200
10.3 @@ -1,4 +1,4 @@
10.4 (*Dummy theory to document dependencies *)
10.5
10.6 -domrange = pair + "subset"
10.7 +domrange = pair + subset
10.8
11.1 --- a/src/ZF/equalities.ML Mon Aug 17 13:06:29 1998 +0200
11.2 +++ b/src/ZF/equalities.ML Mon Aug 17 13:09:08 1998 +0200
11.3 @@ -182,7 +182,11 @@
11.4 by (blast_tac (claset() addSEs [equalityE]) 1);
11.5 qed "Union_disjoint";
11.6
11.7 -goalw ZF.thy [Inter_def] "Inter(0) = 0";
11.8 +Goal "Union(A) = 0 <-> (ALL B:A. B=0)";
11.9 +by (Blast_tac 1);
11.10 +qed "Union_empty_iff";
11.11 +
11.12 +Goalw [Inter_def] "Inter(0) = 0";
11.13 by (Blast_tac 1);
11.14 qed "Inter_0";
11.15
11.16 @@ -209,7 +213,7 @@
11.17 by (Blast_tac 1);
11.18 qed "Union_eq_UN";
11.19
11.20 -goalw ZF.thy [Inter_def] "Inter(A) = (INT x:A. x)";
11.21 +Goalw [Inter_def] "Inter(A) = (INT x:A. x)";
11.22 by (Blast_tac 1);
11.23 qed "Inter_eq_INT";
11.24
11.25 @@ -344,10 +348,10 @@
11.26 by (Blast_tac 1);
11.27 qed "domain_of_prod";
11.28
11.29 -qed_goal "domain_0" ZF.thy "domain(0) = 0"
11.30 +qed_goal "domain_0" thy "domain(0) = 0"
11.31 (fn _ => [ Blast_tac 1 ]);
11.32
11.33 -qed_goal "domain_cons" ZF.thy
11.34 +qed_goal "domain_cons" thy
11.35 "domain(cons(<a,b>,r)) = cons(a, domain(r))"
11.36 (fn _ => [ Blast_tac 1 ]);
11.37
11.38 @@ -376,10 +380,10 @@
11.39 by (Blast_tac 1);
11.40 qed "range_of_prod";
11.41
11.42 -qed_goal "range_0" ZF.thy "range(0) = 0"
11.43 +qed_goal "range_0" thy "range(0) = 0"
11.44 (fn _ => [ Blast_tac 1 ]);
11.45
11.46 -qed_goal "range_cons" ZF.thy
11.47 +qed_goal "range_cons" thy
11.48 "range(cons(<a,b>,r)) = cons(b, range(r))"
11.49 (fn _ => [ Blast_tac 1 ]);
11.50
11.51 @@ -404,13 +408,13 @@
11.52
11.53 (** Field **)
11.54
11.55 -qed_goal "field_of_prod" ZF.thy "field(A*A) = A"
11.56 +qed_goal "field_of_prod" thy "field(A*A) = A"
11.57 (fn _ => [ Blast_tac 1 ]);
11.58
11.59 -qed_goal "field_0" ZF.thy "field(0) = 0"
11.60 +qed_goal "field_0" thy "field(0) = 0"
11.61 (fn _ => [ Blast_tac 1 ]);
11.62
11.63 -qed_goal "field_cons" ZF.thy
11.64 +qed_goal "field_cons" thy
11.65 "field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))"
11.66 (fn _ => [ rtac equalityI 1, ALLGOALS (Blast_tac) ]);
11.67
11.68 @@ -543,7 +547,7 @@
11.69 qed "converse_UN";
11.70
11.71 (*Unfolding Inter avoids using excluded middle on A=0*)
11.72 -goalw ZF.thy [Inter_def] "converse(INT x:A. B(x)) = (INT x:A. converse(B(x)))";
11.73 +Goalw [Inter_def] "converse(INT x:A. B(x)) = (INT x:A. converse(B(x)))";
11.74 by (Blast_tac 1);
11.75 qed "converse_INT";
11.76
12.1 --- a/src/ZF/ex/PropLog.ML Mon Aug 17 13:06:29 1998 +0200
12.2 +++ b/src/ZF/ex/PropLog.ML Mon Aug 17 13:09:08 1998 +0200
12.3 @@ -3,7 +3,7 @@
12.4 Author: Tobias Nipkow & Lawrence C Paulson
12.5 Copyright 1992 University of Cambridge
12.6
12.7 -For ex/prop-log.thy. Inductive definition of propositional logic.
12.8 +Inductive definition of propositional logic.
12.9 Soundness and completeness w.r.t. truth-tables.
12.10
12.11 Prove: If H|=p then G|=p where G:Fin(H)
12.12 @@ -169,23 +169,20 @@
12.13 qed "Imp_Fls";
12.14
12.15 (*Typical example of strengthening the induction formula*)
12.16 -val [major] = goal PropLog.thy
12.17 - "p: prop ==> hyps(p,t) |- if(is_true(p,t), p, p=>Fls)";
12.18 +Goal "p: prop ==> hyps(p,t) |- if(is_true(p,t), p, p=>Fls)";
12.19 by (rtac (split_if RS iffD2) 1);
12.20 -by (rtac (major RS prop.induct) 1);
12.21 +by (etac prop.induct 1);
12.22 by (ALLGOALS (asm_simp_tac (simpset() addsimps [thms_I, thms.H])));
12.23 by (safe_tac (claset() addSEs [Fls_Imp RS weaken_left_Un1,
12.24 - Fls_Imp RS weaken_left_Un2]));
12.25 + Fls_Imp RS weaken_left_Un2]));
12.26 by (ALLGOALS (fast_tac (claset() addIs [weaken_left_Un1, weaken_left_Un2,
12.27 weaken_right, Imp_Fls])));
12.28 qed "hyps_thms_if";
12.29
12.30 (*Key lemma for completeness; yields a set of assumptions satisfying p*)
12.31 -val [premp,sat] = goalw PropLog.thy [logcon_def]
12.32 - "[| p: prop; 0 |= p |] ==> hyps(p,t) |- p";
12.33 -by (rtac (sat RS spec RS mp RS if_P RS subst) 1 THEN
12.34 - rtac (premp RS hyps_thms_if) 2);
12.35 -by (Fast_tac 1);
12.36 +Goalw [logcon_def] "[| p: prop; 0 |= p |] ==> hyps(p,t) |- p";
12.37 +by (dtac hyps_thms_if 1);
12.38 +by (Asm_full_simp_tac 1);
12.39 qed "logcon_thms_p";
12.40
12.41 (*For proving certain theorems in our new propositional logic*)
12.42 @@ -194,27 +191,24 @@
12.43 addIs [thms_in_pl, thms.H, thms.H RS thms_MP];
12.44
12.45 (*The excluded middle in the form of an elimination rule*)
12.46 -val prems = goal PropLog.thy
12.47 - "[| p: prop; q: prop |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q";
12.48 +Goal "[| p: prop; q: prop |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q";
12.49 by (rtac (deduction RS deduction) 1);
12.50 by (rtac (thms.DN RS thms_MP) 1);
12.51 -by (ALLGOALS (best_tac (thms_cs addSIs prems)));
12.52 +by (ALLGOALS (blast_tac thms_cs));
12.53 qed "thms_excluded_middle";
12.54
12.55 (*Hard to prove directly because it requires cuts*)
12.56 -val prems = goal PropLog.thy
12.57 - "[| cons(p,H) |- q; cons(p=>Fls,H) |- q; p: prop |] ==> H |- q";
12.58 +Goal "[| cons(p,H) |- q; cons(p=>Fls,H) |- q; p: prop |] ==> H |- q";
12.59 by (rtac (thms_excluded_middle RS thms_MP RS thms_MP) 1);
12.60 -by (REPEAT (resolve_tac (prems@prop.intrs@[deduction,thms_in_pl]) 1));
12.61 +by (REPEAT (ares_tac (prop.intrs@[deduction,thms_in_pl]) 1));
12.62 qed "thms_excluded_middle_rule";
12.63
12.64 (*** Completeness -- lemmas for reducing the set of assumptions ***)
12.65
12.66 (*For the case hyps(p,t)-cons(#v,Y) |- p;
12.67 we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
12.68 -val [major] = goal PropLog.thy
12.69 - "p: prop ==> hyps(p, t-{v}) <= cons(#v=>Fls, hyps(p,t)-{#v})";
12.70 -by (rtac (major RS prop.induct) 1);
12.71 +Goal "p: prop ==> hyps(p, t-{v}) <= cons(#v=>Fls, hyps(p,t)-{#v})";
12.72 +by (etac prop.induct 1);
12.73 by (Simp_tac 1);
12.74 by (asm_simp_tac (simpset() setloop (split_tac [split_if])) 1);
12.75 by (fast_tac (claset() addSEs prop.free_SEs) 1);
12.76 @@ -224,9 +218,8 @@
12.77
12.78 (*For the case hyps(p,t)-cons(#v => Fls,Y) |- p;
12.79 we also have hyps(p,t)-{#v=>Fls} <= hyps(p, cons(v,t)) *)
12.80 -val [major] = goal PropLog.thy
12.81 - "p: prop ==> hyps(p, cons(v,t)) <= cons(#v, hyps(p,t)-{#v=>Fls})";
12.82 -by (rtac (major RS prop.induct) 1);
12.83 +Goal "p: prop ==> hyps(p, cons(v,t)) <= cons(#v, hyps(p,t)-{#v=>Fls})";
12.84 +by (etac prop.induct 1);
12.85 by (Simp_tac 1);
12.86 by (asm_simp_tac (simpset() setloop (split_tac [split_if])) 1);
12.87 by (fast_tac (claset() addSEs prop.free_SEs) 1);
12.88 @@ -236,19 +229,18 @@
12.89
12.90 (** Two lemmas for use with weaken_left **)
12.91
12.92 -goal ZF.thy "B-C <= cons(a, B-cons(a,C))";
12.93 +Goal "B-C <= cons(a, B-cons(a,C))";
12.94 by (Fast_tac 1);
12.95 qed "cons_Diff_same";
12.96
12.97 -goal ZF.thy "cons(a, B-{c}) - D <= cons(a, B-cons(c,D))";
12.98 +Goal "cons(a, B-{c}) - D <= cons(a, B-cons(c,D))";
12.99 by (Fast_tac 1);
12.100 qed "cons_Diff_subset2";
12.101
12.102 (*The set hyps(p,t) is finite, and elements have the form #v or #v=>Fls;
12.103 could probably prove the stronger hyps(p,t) : Fin(hyps(p,0) Un hyps(p,nat))*)
12.104 -val [major] = goal PropLog.thy
12.105 - "p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})";
12.106 -by (rtac (major RS prop.induct) 1);
12.107 +Goal "p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})";
12.108 +by (etac prop.induct 1);
12.109 by (asm_simp_tac (simpset() addsimps [UN_I]
12.110 setloop (split_tac [split_if])) 2);
12.111 by (ALLGOALS Asm_simp_tac);
13.1 --- a/src/ZF/ex/misc.ML Mon Aug 17 13:06:29 1998 +0200
13.2 +++ b/src/ZF/ex/misc.ML Mon Aug 17 13:09:08 1998 +0200
13.3 @@ -10,12 +10,12 @@
13.4 writeln"ZF/ex/misc";
13.5
13.6 (*Nice Blast_tac benchmark. Proved in 0.3s; old tactics can't manage it!*)
13.7 -goal ZF.thy "!!S. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
13.8 +Goal "ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
13.9 by (Blast_tac 1);
13.10 result();
13.11
13.12 (*variant of the benchmark above*)
13.13 -goal ZF.thy "!!S. ALL x:S. Union(S) <= x ==> EX z. S <= {z}";
13.14 +Goal "ALL x:S. Union(S) <= x ==> EX z. S <= {z}";
13.15 by (Blast_tac 1);
13.16 result();
13.17
14.1 --- a/src/ZF/func.ML Mon Aug 17 13:06:29 1998 +0200
14.2 +++ b/src/ZF/func.ML Mon Aug 17 13:09:08 1998 +0200
14.3 @@ -8,32 +8,32 @@
14.4
14.5 (*** The Pi operator -- dependent function space ***)
14.6
14.7 -goalw ZF.thy [Pi_def]
14.8 +Goalw [Pi_def]
14.9 "f: Pi(A,B) <-> function(f) & f<=Sigma(A,B) & A<=domain(f)";
14.10 by (Blast_tac 1);
14.11 qed "Pi_iff";
14.12
14.13 (*For upward compatibility with the former definition*)
14.14 -goalw ZF.thy [Pi_def, function_def]
14.15 +Goalw [Pi_def, function_def]
14.16 "f: Pi(A,B) <-> f<=Sigma(A,B) & (ALL x:A. EX! y. <x,y>: f)";
14.17 by (Blast_tac 1);
14.18 qed "Pi_iff_old";
14.19
14.20 -goal ZF.thy "!!f. f: Pi(A,B) ==> function(f)";
14.21 +Goal "f: Pi(A,B) ==> function(f)";
14.22 by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff]) 1);
14.23 qed "fun_is_function";
14.24
14.25 (**Two "destruct" rules for Pi **)
14.26
14.27 -val [major] = goalw ZF.thy [Pi_def] "f: Pi(A,B) ==> f <= Sigma(A,B)";
14.28 -by (rtac (major RS CollectD1 RS PowD) 1);
14.29 +Goalw [Pi_def] "f: Pi(A,B) ==> f <= Sigma(A,B)";
14.30 +by (Blast_tac 1);
14.31 qed "fun_is_rel";
14.32
14.33 -goal ZF.thy "!!f. [| f: Pi(A,B); a:A |] ==> EX! y. <a,y>: f";
14.34 +Goal "[| f: Pi(A,B); a:A |] ==> EX! y. <a,y>: f";
14.35 by (blast_tac (claset() addSDs [Pi_iff_old RS iffD1]) 1);
14.36 qed "fun_unique_Pair";
14.37
14.38 -val prems = goalw ZF.thy [Pi_def]
14.39 +val prems = Goalw [Pi_def]
14.40 "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> Pi(A,B) = Pi(A',B')";
14.41 by (simp_tac (FOL_ss addsimps prems addcongs [Sigma_cong]) 1);
14.42 qed "Pi_cong";
14.43 @@ -43,26 +43,26 @@
14.44 Sigmas and Pis are abbreviated as * or -> *)
14.45
14.46 (*Weakening one function type to another; see also Pi_type*)
14.47 -goalw ZF.thy [Pi_def] "!!f. [| f: A->B; B<=D |] ==> f: A->D";
14.48 +Goalw [Pi_def] "[| f: A->B; B<=D |] ==> f: A->D";
14.49 by (Best_tac 1);
14.50 qed "fun_weaken_type";
14.51
14.52 (*Empty function spaces*)
14.53 -goalw ZF.thy [Pi_def, function_def] "Pi(0,A) = {0}";
14.54 +Goalw [Pi_def, function_def] "Pi(0,A) = {0}";
14.55 by (Blast_tac 1);
14.56 qed "Pi_empty1";
14.57
14.58 -goalw ZF.thy [Pi_def] "!!A a. a:A ==> A->0 = 0";
14.59 +Goalw [Pi_def] "a:A ==> A->0 = 0";
14.60 by (Blast_tac 1);
14.61 qed "Pi_empty2";
14.62
14.63 (*The empty function*)
14.64 -goalw ZF.thy [Pi_def, function_def] "0: Pi(0,B)";
14.65 +Goalw [Pi_def, function_def] "0: Pi(0,B)";
14.66 by (Blast_tac 1);
14.67 qed "empty_fun";
14.68
14.69 (*The singleton function*)
14.70 -goalw ZF.thy [Pi_def, function_def] "{<a,b>} : {a} -> {b}";
14.71 +Goalw [Pi_def, function_def] "{<a,b>} : {a} -> {b}";
14.72 by (Blast_tac 1);
14.73 qed "singleton_fun";
14.74
14.75 @@ -70,58 +70,56 @@
14.76
14.77 (*** Function Application ***)
14.78
14.79 -goalw ZF.thy [Pi_def, function_def]
14.80 - "!!a b f. [| <a,b>: f; <a,c>: f; f: Pi(A,B) |] ==> b=c";
14.81 +Goalw [Pi_def, function_def]
14.82 + "[| <a,b>: f; <a,c>: f; f: Pi(A,B) |] ==> b=c";
14.83 by (Blast_tac 1);
14.84 qed "apply_equality2";
14.85
14.86 -goalw ZF.thy [apply_def, function_def]
14.87 - "!!a b f. [| <a,b>: f; function(f) |] ==> f`a = b";
14.88 +Goalw [apply_def, function_def]
14.89 + "[| <a,b>: f; function(f) |] ==> f`a = b";
14.90 by (blast_tac (claset() addIs [the_equality]) 1);
14.91 qed "function_apply_equality";
14.92
14.93 -goalw ZF.thy [Pi_def] "!!a b f. [| <a,b>: f; f: Pi(A,B) |] ==> f`a = b";
14.94 +Goalw [Pi_def] "[| <a,b>: f; f: Pi(A,B) |] ==> f`a = b";
14.95 by (blast_tac (claset() addIs [function_apply_equality]) 1);
14.96 qed "apply_equality";
14.97
14.98 (*Applying a function outside its domain yields 0*)
14.99 -goalw ZF.thy [apply_def]
14.100 - "!!a. a ~: domain(f) ==> f`a = 0";
14.101 +Goalw [apply_def]
14.102 + "a ~: domain(f) ==> f`a = 0";
14.103 by (rtac the_0 1);
14.104 by (Blast_tac 1);
14.105 qed "apply_0";
14.106
14.107 -goal ZF.thy "!!f. [| f: Pi(A,B); c: f |] ==> EX x:A. c = <x,f`x>";
14.108 +Goal "[| f: Pi(A,B); c: f |] ==> EX x:A. c = <x,f`x>";
14.109 by (forward_tac [fun_is_rel] 1);
14.110 by (blast_tac (claset() addDs [apply_equality]) 1);
14.111 qed "Pi_memberD";
14.112
14.113 -goal ZF.thy "!!f. [| f: Pi(A,B); a:A |] ==> <a,f`a>: f";
14.114 +Goal "[| f: Pi(A,B); a:A |] ==> <a,f`a>: f";
14.115 by (rtac (fun_unique_Pair RS ex1E) 1);
14.116 by (resolve_tac [apply_equality RS ssubst] 3);
14.117 by (REPEAT (assume_tac 1));
14.118 qed "apply_Pair";
14.119
14.120 (*Conclusion is flexible -- use res_inst_tac or else apply_funtype below!*)
14.121 -goal ZF.thy "!!f. [| f: Pi(A,B); a:A |] ==> f`a : B(a)";
14.122 +Goal "[| f: Pi(A,B); a:A |] ==> f`a : B(a)";
14.123 by (rtac (fun_is_rel RS subsetD RS SigmaE2) 1);
14.124 by (REPEAT (ares_tac [apply_Pair] 1));
14.125 qed "apply_type";
14.126
14.127 (*This version is acceptable to the simplifier*)
14.128 -goal ZF.thy "!!f. [| f: A->B; a:A |] ==> f`a : B";
14.129 +Goal "[| f: A->B; a:A |] ==> f`a : B";
14.130 by (REPEAT (ares_tac [apply_type] 1));
14.131 qed "apply_funtype";
14.132
14.133 -val [major] = goal ZF.thy
14.134 - "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b";
14.135 -by (cut_facts_tac [major RS fun_is_rel] 1);
14.136 -by (blast_tac (claset() addSIs [major RS apply_Pair,
14.137 - major RSN (2,apply_equality)]) 1);
14.138 +Goal "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b";
14.139 +by (forward_tac [fun_is_rel] 1);
14.140 +by (blast_tac (claset() addSIs [apply_Pair, apply_equality]) 1);
14.141 qed "apply_iff";
14.142
14.143 (*Refining one Pi type to another*)
14.144 -val pi_prem::prems = goal ZF.thy
14.145 +val pi_prem::prems = Goal
14.146 "[| f: Pi(A,C); !!x. x:A ==> f`x : B(x) |] ==> f : Pi(A,B)";
14.147 by (cut_facts_tac [pi_prem] 1);
14.148 by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff]) 1);
14.149 @@ -131,16 +129,16 @@
14.150
14.151 (** Elimination of membership in a function **)
14.152
14.153 -goal ZF.thy "!!a A. [| <a,b> : f; f: Pi(A,B) |] ==> a : A";
14.154 +Goal "[| <a,b> : f; f: Pi(A,B) |] ==> a : A";
14.155 by (REPEAT (ares_tac [fun_is_rel RS subsetD RS SigmaD1] 1));
14.156 qed "domain_type";
14.157
14.158 -goal ZF.thy "!!b B a. [| <a,b> : f; f: Pi(A,B) |] ==> b : B(a)";
14.159 +Goal "[| <a,b> : f; f: Pi(A,B) |] ==> b : B(a)";
14.160 by (etac (fun_is_rel RS subsetD RS SigmaD2) 1);
14.161 by (assume_tac 1);
14.162 qed "range_type";
14.163
14.164 -val prems = goal ZF.thy
14.165 +val prems = Goal
14.166 "[| <a,b>: f; f: Pi(A,B); \
14.167 \ [| a:A; b:B(a); f`a = b |] ==> P \
14.168 \ |] ==> P";
14.169 @@ -151,35 +149,35 @@
14.170
14.171 (*** Lambda Abstraction ***)
14.172
14.173 -goalw ZF.thy [lam_def] "!!A b. a:A ==> <a,b(a)> : (lam x:A. b(x))";
14.174 +Goalw [lam_def] "a:A ==> <a,b(a)> : (lam x:A. b(x))";
14.175 by (etac RepFunI 1);
14.176 qed "lamI";
14.177
14.178 -val major::prems = goalw ZF.thy [lam_def]
14.179 +val major::prems = Goalw [lam_def]
14.180 "[| p: (lam x:A. b(x)); !!x.[| x:A; p=<x,b(x)> |] ==> P \
14.181 \ |] ==> P";
14.182 by (rtac (major RS RepFunE) 1);
14.183 by (REPEAT (ares_tac prems 1));
14.184 qed "lamE";
14.185
14.186 -goal ZF.thy "!!a b c. [| <a,c>: (lam x:A. b(x)) |] ==> c = b(a)";
14.187 +Goal "[| <a,c>: (lam x:A. b(x)) |] ==> c = b(a)";
14.188 by (REPEAT (eresolve_tac [asm_rl,lamE,Pair_inject,ssubst] 1));
14.189 qed "lamD";
14.190
14.191 -val prems = goalw ZF.thy [lam_def, Pi_def, function_def]
14.192 +val prems = Goalw [lam_def, Pi_def, function_def]
14.193 "[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B)";
14.194 by (blast_tac (claset() addIs prems) 1);
14.195 qed "lam_type";
14.196
14.197 -goal ZF.thy "(lam x:A. b(x)) : A -> {b(x). x:A}";
14.198 +Goal "(lam x:A. b(x)) : A -> {b(x). x:A}";
14.199 by (REPEAT (ares_tac [refl,lam_type,RepFunI] 1));
14.200 qed "lam_funtype";
14.201
14.202 -goal ZF.thy "!!a A. a : A ==> (lam x:A. b(x)) ` a = b(a)";
14.203 +Goal "a : A ==> (lam x:A. b(x)) ` a = b(a)";
14.204 by (REPEAT (ares_tac [apply_equality,lam_funtype,lamI] 1));
14.205 qed "beta";
14.206
14.207 -goalw ZF.thy [lam_def] "(lam x:0. b(x)) = 0";
14.208 +Goalw [lam_def] "(lam x:0. b(x)) = 0";
14.209 by (Simp_tac 1);
14.210 qed "lam_empty";
14.211
14.212 @@ -190,14 +188,14 @@
14.213 Addsimps [beta, lam_empty, domain_lam];
14.214
14.215 (*congruence rule for lambda abstraction*)
14.216 -val prems = goalw ZF.thy [lam_def]
14.217 +val prems = Goalw [lam_def]
14.218 "[| A=A'; !!x. x:A' ==> b(x)=b'(x) |] ==> Lambda(A,b) = Lambda(A',b')";
14.219 by (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1);
14.220 qed "lam_cong";
14.221
14.222 Addcongs [lam_cong];
14.223
14.224 -val [major] = goal ZF.thy
14.225 +val [major] = Goal
14.226 "(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)";
14.227 by (res_inst_tac [("x", "lam x: A. THE y. Q(x,y)")] exI 1);
14.228 by (rtac ballI 1);
14.229 @@ -210,7 +208,7 @@
14.230 (** Extensionality **)
14.231
14.232 (*Semi-extensionality!*)
14.233 -val prems = goal ZF.thy
14.234 +val prems = Goal
14.235 "[| f : Pi(A,B); g: Pi(C,D); A<=C; \
14.236 \ !!x. x:A ==> f`x = g`x |] ==> f<=g";
14.237 by (rtac subsetI 1);
14.238 @@ -220,27 +218,27 @@
14.239 by (REPEAT (ares_tac (prems@[apply_Pair,subsetD]) 1));
14.240 qed "fun_subset";
14.241
14.242 -val prems = goal ZF.thy
14.243 +val prems = Goal
14.244 "[| f : Pi(A,B); g: Pi(A,D); \
14.245 \ !!x. x:A ==> f`x = g`x |] ==> f=g";
14.246 by (REPEAT (ares_tac (prems @ (prems RL [sym]) @
14.247 [subset_refl,equalityI,fun_subset]) 1));
14.248 qed "fun_extension";
14.249
14.250 -goal ZF.thy "!!f A B. f : Pi(A,B) ==> (lam x:A. f`x) = f";
14.251 +Goal "f : Pi(A,B) ==> (lam x:A. f`x) = f";
14.252 by (rtac fun_extension 1);
14.253 by (REPEAT (ares_tac [lam_type,apply_type,beta] 1));
14.254 qed "eta";
14.255
14.256 Addsimps [eta];
14.257
14.258 -val fun_extension_iff = prove_goal ZF.thy
14.259 - "!!z. [| f:Pi(A,B); g:Pi(A,C) |] ==> (ALL a:A. f`a = g`a) <-> f=g"
14.260 - (fn _=> [ (blast_tac (claset() addIs [fun_extension]) 1) ]);
14.261 +Goal "[| f:Pi(A,B); g:Pi(A,C) |] ==> (ALL a:A. f`a = g`a) <-> f=g";
14.262 +by (blast_tac (claset() addIs [fun_extension]) 1);
14.263 +qed "fun_extension_iff";
14.264
14.265 (*thanks to Mark Staples*)
14.266 -val fun_subset_eq = prove_goal ZF.thy
14.267 - "!!z. [| f:Pi(A,B); g:Pi(A,C) |] ==> f <= g <-> (f = g)"
14.268 +val fun_subset_eq = prove_goal thy
14.269 + "!!f. [| f:Pi(A,B); g:Pi(A,C) |] ==> f <= g <-> (f = g)"
14.270 (fn _=>
14.271 [ (rtac iffI 1), (asm_full_simp_tac ZF_ss 2),
14.272 (rtac fun_extension 1), (REPEAT (atac 1)),
14.273 @@ -249,7 +247,7 @@
14.274
14.275
14.276 (*Every element of Pi(A,B) may be expressed as a lambda abstraction!*)
14.277 -val prems = goal ZF.thy
14.278 +val prems = Goal
14.279 "[| f: Pi(A,B); \
14.280 \ !!b. [| ALL x:A. b(x):B(x); f = (lam x:A. b(x)) |] ==> P \
14.281 \ |] ==> P";
14.282 @@ -261,14 +259,13 @@
14.283
14.284 (** Images of functions **)
14.285
14.286 -goalw ZF.thy [lam_def] "!!C A. C <= A ==> (lam x:A. b(x)) `` C = {b(x). x:C}";
14.287 +Goalw [lam_def] "C <= A ==> (lam x:A. b(x)) `` C = {b(x). x:C}";
14.288 by (Blast_tac 1);
14.289 qed "image_lam";
14.290
14.291 -goal ZF.thy "!!C A. [| f : Pi(A,B); C <= A |] ==> f``C = {f`x. x:C}";
14.292 +Goal "[| f : Pi(A,B); C <= A |] ==> f``C = {f`x. x:C}";
14.293 by (etac (eta RS subst) 1);
14.294 -by (asm_full_simp_tac (FOL_ss addsimps [beta, image_lam, subset_iff]
14.295 - addcongs [RepFun_cong]) 1);
14.296 +by (asm_full_simp_tac (simpset() addsimps [image_lam, subset_iff]) 1);
14.297 qed "image_fun";
14.298
14.299 Goal "[| f: Pi(A,B); x: A |] ==> f `` cons(x,y) = cons(f`x, f``y)";
14.300 @@ -278,47 +275,46 @@
14.301
14.302 (*** properties of "restrict" ***)
14.303
14.304 -goalw ZF.thy [restrict_def,lam_def]
14.305 - "!!f A. [| f: Pi(C,B); A<=C |] ==> restrict(f,A) <= f";
14.306 +Goalw [restrict_def,lam_def]
14.307 + "[| f: Pi(C,B); A<=C |] ==> restrict(f,A) <= f";
14.308 by (blast_tac (claset() addIs [apply_Pair]) 1);
14.309 qed "restrict_subset";
14.310
14.311 -val prems = goalw ZF.thy [restrict_def]
14.312 +val prems = Goalw [restrict_def]
14.313 "[| !!x. x:A ==> f`x: B(x) |] ==> restrict(f,A) : Pi(A,B)";
14.314 by (rtac lam_type 1);
14.315 by (eresolve_tac prems 1);
14.316 qed "restrict_type";
14.317
14.318 -val [pi,subs] = goal ZF.thy
14.319 - "[| f: Pi(C,B); A<=C |] ==> restrict(f,A) : Pi(A,B)";
14.320 -by (rtac (pi RS apply_type RS restrict_type) 1);
14.321 -by (etac (subs RS subsetD) 1);
14.322 +Goal "[| f: Pi(C,B); A<=C |] ==> restrict(f,A) : Pi(A,B)";
14.323 +by (blast_tac (claset() addIs [apply_type, restrict_type]) 1);
14.324 qed "restrict_type2";
14.325
14.326 -goalw ZF.thy [restrict_def] "!!a A. a : A ==> restrict(f,A) ` a = f`a";
14.327 +Goalw [restrict_def] "a : A ==> restrict(f,A) ` a = f`a";
14.328 by (etac beta 1);
14.329 qed "restrict";
14.330
14.331 -goalw ZF.thy [restrict_def] "restrict(f,0) = 0";
14.332 +Goalw [restrict_def] "restrict(f,0) = 0";
14.333 by (Simp_tac 1);
14.334 qed "restrict_empty";
14.335
14.336 Addsimps [restrict, restrict_empty];
14.337
14.338 (*NOT SAFE as a congruence rule for the simplifier! Can cause it to fail!*)
14.339 -val prems = goalw ZF.thy [restrict_def]
14.340 +val prems = Goalw [restrict_def]
14.341 "[| A=B; !!x. x:B ==> f`x=g`x |] ==> restrict(f,A) = restrict(g,B)";
14.342 by (REPEAT (ares_tac (prems@[lam_cong]) 1));
14.343 qed "restrict_eqI";
14.344
14.345 -goalw ZF.thy [restrict_def, lam_def] "domain(restrict(f,C)) = C";
14.346 +Goalw [restrict_def, lam_def] "domain(restrict(f,C)) = C";
14.347 by (Blast_tac 1);
14.348 qed "domain_restrict";
14.349
14.350 -val [prem] = goalw ZF.thy [restrict_def]
14.351 +Goalw [restrict_def]
14.352 "A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))";
14.353 by (rtac (refl RS lam_cong) 1);
14.354 -by (etac (prem RS subsetD RS beta) 1); (*easier than calling simp_tac*)
14.355 +by (set_mp_tac 1);
14.356 +by (Asm_simp_tac 1);
14.357 qed "restrict_lam_eq";
14.358
14.359
14.360 @@ -327,16 +323,16 @@
14.361
14.362 (** The Union of a set of COMPATIBLE functions is a function **)
14.363
14.364 -goalw ZF.thy [function_def]
14.365 - "!!S. [| ALL x:S. function(x); \
14.366 +Goalw [function_def]
14.367 + "[| ALL x:S. function(x); \
14.368 \ ALL x:S. ALL y:S. x<=y | y<=x |] ==> \
14.369 \ function(Union(S))";
14.370 by (fast_tac (ZF_cs addSDs [bspec RS bspec]) 1);
14.371 (*by (Blast_tac 1); takes too long...*)
14.372 qed "function_Union";
14.373
14.374 -goalw ZF.thy [Pi_def]
14.375 - "!!S. [| ALL f:S. EX C D. f:C->D; \
14.376 +Goalw [Pi_def]
14.377 + "[| ALL f:S. EX C D. f:C->D; \
14.378 \ ALL f:S. ALL y:S. f<=y | y<=f |] ==> \
14.379 \ Union(S) : domain(Union(S)) -> range(Union(S))";
14.380 by (blast_tac (subset_cs addSIs [rel_Union, function_Union]) 1);
14.381 @@ -349,7 +345,7 @@
14.382 Un_upper1 RSN (2, subset_trans),
14.383 Un_upper2 RSN (2, subset_trans)];
14.384
14.385 -goal ZF.thy "!!f. [| f: A->B; g: C->D; A Int C = 0 |] \
14.386 +Goal "[| f: A->B; g: C->D; A Int C = 0 |] \
14.387 \ ==> (f Un g) : (A Un C) -> (B Un D)";
14.388 (*Prove the product and domain subgoals using distributive laws*)
14.389 by (asm_full_simp_tac (simpset() addsimps [Pi_iff,extension]@Un_rls) 1);
14.390 @@ -357,15 +353,13 @@
14.391 by (Blast_tac 1);
14.392 qed "fun_disjoint_Un";
14.393
14.394 -goal ZF.thy
14.395 - "!!f g a. [| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \
14.396 +Goal "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \
14.397 \ (f Un g)`a = f`a";
14.398 by (rtac (apply_Pair RS UnI1 RS apply_equality) 1);
14.399 by (REPEAT (ares_tac [fun_disjoint_Un] 1));
14.400 qed "fun_disjoint_apply1";
14.401
14.402 -goal ZF.thy
14.403 - "!!f g c. [| c:C; f: A->B; g: C->D; A Int C = 0 |] ==> \
14.404 +Goal "[| c:C; f: A->B; g: C->D; A Int C = 0 |] ==> \
14.405 \ (f Un g)`c = g`c";
14.406 by (rtac (apply_Pair RS UnI2 RS apply_equality) 1);
14.407 by (REPEAT (ares_tac [fun_disjoint_Un] 1));
14.408 @@ -373,18 +367,17 @@
14.409
14.410 (** Domain and range of a function/relation **)
14.411
14.412 -goalw ZF.thy [Pi_def] "!!f. f : Pi(A,B) ==> domain(f)=A";
14.413 +Goalw [Pi_def] "f : Pi(A,B) ==> domain(f)=A";
14.414 by (Blast_tac 1);
14.415 qed "domain_of_fun";
14.416
14.417 -goal ZF.thy "!!f. [| f : Pi(A,B); a: A |] ==> f`a : range(f)";
14.418 +Goal "[| f : Pi(A,B); a: A |] ==> f`a : range(f)";
14.419 by (etac (apply_Pair RS rangeI) 1);
14.420 by (assume_tac 1);
14.421 qed "apply_rangeI";
14.422
14.423 -val [major] = goal ZF.thy "f : Pi(A,B) ==> f : A->range(f)";
14.424 -by (rtac (major RS Pi_type) 1);
14.425 -by (etac (major RS apply_rangeI) 1);
14.426 +Goal "f : Pi(A,B) ==> f : A->range(f)";
14.427 +by (REPEAT (ares_tac [Pi_type, apply_rangeI] 1));
14.428 qed "range_of_fun";
14.429
14.430 (*** Extensions of functions ***)
15.1 --- a/src/ZF/mono.ML Mon Aug 17 13:06:29 1998 +0200
15.2 +++ b/src/ZF/mono.ML Mon Aug 17 13:09:08 1998 +0200
15.3 @@ -28,7 +28,7 @@
15.4 by (Blast_tac 1);
15.5 qed "Union_mono";
15.6
15.7 -val prems = goal thy
15.8 +val prems = Goal
15.9 "[| A<=C; !!x. x:A ==> B(x)<=D(x) \
15.10 \ |] ==> (UN x:A. B(x)) <= (UN x:C. D(x))";
15.11 by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
15.12 @@ -57,8 +57,7 @@
15.13
15.14 (** Standard products, sums and function spaces **)
15.15
15.16 -Goal "[| A<=C; ALL x:A. B(x) <= D(x) |] ==> \
15.17 -\ Sigma(A,B) <= Sigma(C,D)";
15.18 +Goal "[| A<=C; ALL x:A. B(x) <= D(x) |] ==> Sigma(A,B) <= Sigma(C,D)";
15.19 by (Blast_tac 1);
15.20 qed "Sigma_mono_lemma";
15.21 val Sigma_mono = ballI RSN (2,Sigma_mono_lemma);
15.22 @@ -131,12 +130,12 @@
15.23
15.24 (** Images **)
15.25
15.26 -val [prem1,prem2] = goal thy
15.27 +val [prem1,prem2] = Goal
15.28 "[| !! x y. <x,y>:r ==> <x,y>:s; A<=B |] ==> r``A <= s``B";
15.29 by (blast_tac (claset() addIs [prem1, prem2 RS subsetD]) 1);
15.30 qed "image_pair_mono";
15.31
15.32 -val [prem1,prem2] = goal thy
15.33 +val [prem1,prem2] = Goal
15.34 "[| !! x y. <x,y>:r ==> <x,y>:s; A<=B |] ==> r-``A <= s-``B";
15.35 by (blast_tac (claset() addIs [prem1, prem2 RS subsetD]) 1);
15.36 qed "vimage_pair_mono";
15.37 @@ -149,7 +148,7 @@
15.38 by (Blast_tac 1);
15.39 qed "vimage_mono";
15.40
15.41 -val [sub,PQimp] = goal thy
15.42 +val [sub,PQimp] = Goal
15.43 "[| A<=B; !!x. x:A ==> P(x) --> Q(x) |] ==> Collect(A,P) <= Collect(B,Q)";
15.44 by (blast_tac (claset() addIs [sub RS subsetD, PQimp RS mp]) 1);
15.45 qed "Collect_mono";
16.1 --- a/src/ZF/mono.thy Mon Aug 17 13:06:29 1998 +0200
16.2 +++ b/src/ZF/mono.thy Mon Aug 17 13:09:08 1998 +0200
16.3 @@ -1,4 +1,2 @@
16.4 -(*Dummy theory to document dependencies *)
16.5 +mono = QPair + Sum + func
16.6
16.7 -mono = QPair + Sum + domrange
16.8 -
17.1 --- a/src/ZF/pair.ML Mon Aug 17 13:06:29 1998 +0200
17.2 +++ b/src/ZF/pair.ML Mon Aug 17 13:09:08 1998 +0200
17.3 @@ -8,17 +8,17 @@
17.4
17.5 (** Lemmas for showing that <a,b> uniquely determines a and b **)
17.6
17.7 -qed_goal "singleton_eq_iff" ZF.thy
17.8 +qed_goal "singleton_eq_iff" thy
17.9 "{a} = {b} <-> a=b"
17.10 (fn _=> [ (resolve_tac [extension RS iff_trans] 1),
17.11 (Blast_tac 1) ]);
17.12
17.13 -qed_goal "doubleton_eq_iff" ZF.thy
17.14 +qed_goal "doubleton_eq_iff" thy
17.15 "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)"
17.16 (fn _=> [ (resolve_tac [extension RS iff_trans] 1),
17.17 (Blast_tac 1) ]);
17.18
17.19 -qed_goalw "Pair_iff" ZF.thy [Pair_def]
17.20 +qed_goalw "Pair_iff" thy [Pair_def]
17.21 "<a,b> = <c,d> <-> a=c & b=d"
17.22 (fn _=> [ (simp_tac (simpset() addsimps [doubleton_eq_iff]) 1),
17.23 (Blast_tac 1) ]);
17.24 @@ -32,20 +32,20 @@
17.25 bind_thm ("Pair_inject1", Pair_iff RS iffD1 RS conjunct1);
17.26 bind_thm ("Pair_inject2", Pair_iff RS iffD1 RS conjunct2);
17.27
17.28 -qed_goalw "Pair_not_0" ZF.thy [Pair_def] "<a,b> ~= 0"
17.29 +qed_goalw "Pair_not_0" thy [Pair_def] "<a,b> ~= 0"
17.30 (fn _ => [ (blast_tac (claset() addEs [equalityE]) 1) ]);
17.31
17.32 bind_thm ("Pair_neq_0", Pair_not_0 RS notE);
17.33
17.34 AddSEs [Pair_neq_0, sym RS Pair_neq_0];
17.35
17.36 -qed_goalw "Pair_neq_fst" ZF.thy [Pair_def] "<a,b>=a ==> P"
17.37 +qed_goalw "Pair_neq_fst" thy [Pair_def] "<a,b>=a ==> P"
17.38 (fn [major]=>
17.39 [ (rtac (consI1 RS mem_asym RS FalseE) 1),
17.40 (rtac (major RS subst) 1),
17.41 (rtac consI1 1) ]);
17.42
17.43 -qed_goalw "Pair_neq_snd" ZF.thy [Pair_def] "<a,b>=b ==> P"
17.44 +qed_goalw "Pair_neq_snd" thy [Pair_def] "<a,b>=b ==> P"
17.45 (fn [major]=>
17.46 [ (rtac (consI1 RS consI2 RS mem_asym RS FalseE) 1),
17.47 (rtac (major RS subst) 1),
17.48 @@ -55,12 +55,12 @@
17.49 (*** Sigma: Disjoint union of a family of sets
17.50 Generalizes Cartesian product ***)
17.51
17.52 -qed_goalw "Sigma_iff" ZF.thy [Sigma_def] "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"
17.53 +qed_goalw "Sigma_iff" thy [Sigma_def] "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"
17.54 (fn _ => [ Blast_tac 1 ]);
17.55
17.56 Addsimps [Sigma_iff];
17.57
17.58 -qed_goal "SigmaI" ZF.thy
17.59 +qed_goal "SigmaI" thy
17.60 "!!a b. [| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B)"
17.61 (fn _ => [ Asm_simp_tac 1 ]);
17.62
17.63 @@ -68,7 +68,7 @@
17.64 bind_thm ("SigmaD2", Sigma_iff RS iffD1 RS conjunct2);
17.65
17.66 (*The general elimination rule*)
17.67 -qed_goalw "SigmaE" ZF.thy [Sigma_def]
17.68 +qed_goalw "SigmaE" thy [Sigma_def]
17.69 "[| c: Sigma(A,B); \
17.70 \ !!x y.[| x:A; y:B(x); c=<x,y> |] ==> P \
17.71 \ |] ==> P"
17.72 @@ -76,7 +76,7 @@
17.73 [ (cut_facts_tac [major] 1),
17.74 (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
17.75
17.76 -qed_goal "SigmaE2" ZF.thy
17.77 +qed_goal "SigmaE2" thy
17.78 "[| <a,b> : Sigma(A,B); \
17.79 \ [| a:A; b:B(a) |] ==> P \
17.80 \ |] ==> P"
17.81 @@ -85,7 +85,7 @@
17.82 (rtac (major RS SigmaD1) 1),
17.83 (rtac (major RS SigmaD2) 1) ]);
17.84
17.85 -qed_goalw "Sigma_cong" ZF.thy [Sigma_def]
17.86 +qed_goalw "Sigma_cong" thy [Sigma_def]
17.87 "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \
17.88 \ Sigma(A,B) = Sigma(A',B')"
17.89 (fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]);
17.90 @@ -98,10 +98,10 @@
17.91 AddSIs [SigmaI];
17.92 AddSEs [SigmaE2, SigmaE];
17.93
17.94 -qed_goal "Sigma_empty1" ZF.thy "Sigma(0,B) = 0"
17.95 +qed_goal "Sigma_empty1" thy "Sigma(0,B) = 0"
17.96 (fn _ => [ (Blast_tac 1) ]);
17.97
17.98 -qed_goal "Sigma_empty2" ZF.thy "A*0 = 0"
17.99 +qed_goal "Sigma_empty2" thy "A*0 = 0"
17.100 (fn _ => [ (Blast_tac 1) ]);
17.101
17.102 Addsimps [Sigma_empty1, Sigma_empty2];
17.103 @@ -113,21 +113,21 @@
17.104
17.105 (*** Projections: fst, snd ***)
17.106
17.107 -qed_goalw "fst_conv" ZF.thy [fst_def] "fst(<a,b>) = a"
17.108 +qed_goalw "fst_conv" thy [fst_def] "fst(<a,b>) = a"
17.109 (fn _=> [ (blast_tac (claset() addIs [the_equality]) 1) ]);
17.110
17.111 -qed_goalw "snd_conv" ZF.thy [snd_def] "snd(<a,b>) = b"
17.112 +qed_goalw "snd_conv" thy [snd_def] "snd(<a,b>) = b"
17.113 (fn _=> [ (blast_tac (claset() addIs [the_equality]) 1) ]);
17.114
17.115 Addsimps [fst_conv,snd_conv];
17.116
17.117 -qed_goal "fst_type" ZF.thy "!!p. p:Sigma(A,B) ==> fst(p) : A"
17.118 +qed_goal "fst_type" thy "!!p. p:Sigma(A,B) ==> fst(p) : A"
17.119 (fn _=> [ Auto_tac ]);
17.120
17.121 -qed_goal "snd_type" ZF.thy "!!p. p:Sigma(A,B) ==> snd(p) : B(fst(p))"
17.122 +qed_goal "snd_type" thy "!!p. p:Sigma(A,B) ==> snd(p) : B(fst(p))"
17.123 (fn _=> [ Auto_tac ]);
17.124
17.125 -qed_goal "Pair_fst_snd_eq" ZF.thy
17.126 +qed_goal "Pair_fst_snd_eq" thy
17.127 "!!a A B. a: Sigma(A,B) ==> <fst(a),snd(a)> = a"
17.128 (fn _=> [ Auto_tac ]);
17.129
17.130 @@ -135,13 +135,13 @@
17.131 (*** Eliminator - split ***)
17.132
17.133 (*A META-equality, so that it applies to higher types as well...*)
17.134 -qed_goalw "split" ZF.thy [split_def] "split(%x y. c(x,y), <a,b>) == c(a,b)"
17.135 +qed_goalw "split" thy [split_def] "split(%x y. c(x,y), <a,b>) == c(a,b)"
17.136 (fn _ => [ (Simp_tac 1),
17.137 (rtac reflexive_thm 1) ]);
17.138
17.139 Addsimps [split];
17.140
17.141 -qed_goal "split_type" ZF.thy
17.142 +qed_goal "split_type" thy
17.143 "[| p:Sigma(A,B); \
17.144 \ !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>) \
17.145 \ |] ==> split(%x y. c(x,y), p) : C(p)"
17.146 @@ -149,8 +149,8 @@
17.147 [ (rtac (major RS SigmaE) 1),
17.148 (asm_simp_tac (simpset() addsimps prems) 1) ]);
17.149
17.150 -goalw ZF.thy [split_def]
17.151 - "!!u. u: A*B ==> \
17.152 +Goalw [split_def]
17.153 + "u: A*B ==> \
17.154 \ R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))";
17.155 by Auto_tac;
17.156 qed "expand_split";
17.157 @@ -158,11 +158,11 @@
17.158
17.159 (*** split for predicates: result type o ***)
17.160
17.161 -goalw ZF.thy [split_def] "!!R a b. R(a,b) ==> split(R, <a,b>)";
17.162 +Goalw [split_def] "R(a,b) ==> split(R, <a,b>)";
17.163 by (Asm_simp_tac 1);
17.164 qed "splitI";
17.165
17.166 -val major::sigma::prems = goalw ZF.thy [split_def]
17.167 +val major::sigma::prems = Goalw [split_def]
17.168 "[| split(R,z); z:Sigma(A,B); \
17.169 \ !!x y. [| z = <x,y>; R(x,y) |] ==> P \
17.170 \ |] ==> P";
17.171 @@ -172,7 +172,7 @@
17.172 by (Asm_full_simp_tac 1);
17.173 qed "splitE";
17.174
17.175 -goalw ZF.thy [split_def] "!!R a b. split(R,<a,b>) ==> R(a,b)";
17.176 +Goalw [split_def] "split(R,<a,b>) ==> R(a,b)";
17.177 by (Full_simp_tac 1);
17.178 qed "splitD";
17.179
18.1 --- a/src/ZF/simpdata.ML Mon Aug 17 13:06:29 1998 +0200
18.2 +++ b/src/ZF/simpdata.ML Mon Aug 17 13:09:08 1998 +0200
18.3 @@ -10,7 +10,7 @@
18.4
18.5 local
18.6 (*For proving rewrite rules*)
18.7 - fun prover s = (prove_goal ZF.thy s (fn _ => [Blast_tac 1]));
18.8 + fun prover s = (prove_goal thy s (fn _ => [Blast_tac 1]));
18.9
18.10 in
18.11
19.1 --- a/src/ZF/subset.ML Mon Aug 17 13:06:29 1998 +0200
19.2 +++ b/src/ZF/subset.ML Mon Aug 17 13:09:08 1998 +0200
19.3 @@ -9,38 +9,38 @@
19.4
19.5 (*** cons ***)
19.6
19.7 -qed_goal "cons_subsetI" ZF.thy "!!a. [| a:C; B<=C |] ==> cons(a,B) <= C"
19.8 +qed_goal "cons_subsetI" thy "!!a. [| a:C; B<=C |] ==> cons(a,B) <= C"
19.9 (fn _ => [ Blast_tac 1 ]);
19.10
19.11 -qed_goal "subset_consI" ZF.thy "B <= cons(a,B)"
19.12 +qed_goal "subset_consI" thy "B <= cons(a,B)"
19.13 (fn _ => [ Blast_tac 1 ]);
19.14
19.15 -qed_goal "cons_subset_iff" ZF.thy "cons(a,B)<=C <-> a:C & B<=C"
19.16 +qed_goal "cons_subset_iff" thy "cons(a,B)<=C <-> a:C & B<=C"
19.17 (fn _ => [ Blast_tac 1 ]);
19.18
19.19 (*A safe special case of subset elimination, adding no new variables
19.20 [| cons(a,B) <= C; [| a : C; B <= C |] ==> R |] ==> R *)
19.21 bind_thm ("cons_subsetE", cons_subset_iff RS iffD1 RS conjE);
19.22
19.23 -qed_goal "subset_empty_iff" ZF.thy "A<=0 <-> A=0"
19.24 +qed_goal "subset_empty_iff" thy "A<=0 <-> A=0"
19.25 (fn _=> [ (Blast_tac 1) ]);
19.26
19.27 -qed_goal "subset_cons_iff" ZF.thy
19.28 +qed_goal "subset_cons_iff" thy
19.29 "C<=cons(a,B) <-> C<=B | (a:C & C-{a} <= B)"
19.30 (fn _=> [ (Blast_tac 1) ]);
19.31
19.32 (*** succ ***)
19.33
19.34 -qed_goal "subset_succI" ZF.thy "i <= succ(i)"
19.35 +qed_goal "subset_succI" thy "i <= succ(i)"
19.36 (fn _=> [ (Blast_tac 1) ]);
19.37
19.38 (*But if j is an ordinal or is transitive, then i:j implies i<=j!
19.39 See ordinal/Ord_succ_subsetI*)
19.40 -qed_goalw "succ_subsetI" ZF.thy [succ_def]
19.41 +qed_goalw "succ_subsetI" thy [succ_def]
19.42 "!!i j. [| i:j; i<=j |] ==> succ(i)<=j"
19.43 (fn _=> [ (Blast_tac 1) ]);
19.44
19.45 -qed_goalw "succ_subsetE" ZF.thy [succ_def]
19.46 +qed_goalw "succ_subsetE" thy [succ_def]
19.47 "[| succ(i) <= j; [| i:j; i<=j |] ==> P \
19.48 \ |] ==> P"
19.49 (fn major::prems=>
19.50 @@ -49,22 +49,22 @@
19.51
19.52 (*** singletons ***)
19.53
19.54 -qed_goal "singleton_subsetI" ZF.thy "!!a c. a:C ==> {a} <= C"
19.55 +qed_goal "singleton_subsetI" thy "!!a c. a:C ==> {a} <= C"
19.56 (fn _=> [ (Blast_tac 1) ]);
19.57
19.58 -qed_goal "singleton_subsetD" ZF.thy "!!a C. {a} <= C ==> a:C"
19.59 +qed_goal "singleton_subsetD" thy "!!a C. {a} <= C ==> a:C"
19.60 (fn _=> [ (Blast_tac 1) ]);
19.61
19.62 (*** Big Union -- least upper bound of a set ***)
19.63
19.64 -qed_goal "Union_subset_iff" ZF.thy "Union(A) <= C <-> (ALL x:A. x <= C)"
19.65 +qed_goal "Union_subset_iff" thy "Union(A) <= C <-> (ALL x:A. x <= C)"
19.66 (fn _ => [ Blast_tac 1 ]);
19.67
19.68 -qed_goal "Union_upper" ZF.thy
19.69 +qed_goal "Union_upper" thy
19.70 "!!B A. B:A ==> B <= Union(A)"
19.71 (fn _ => [ Blast_tac 1 ]);
19.72
19.73 -qed_goal "Union_least" ZF.thy
19.74 +qed_goal "Union_least" thy
19.75 "[| !!x. x:A ==> x<=C |] ==> Union(A) <= C"
19.76 (fn [prem]=>
19.77 [ (rtac (ballI RS (Union_subset_iff RS iffD2)) 1),
19.78 @@ -72,19 +72,19 @@
19.79
19.80 (*** Union of a family of sets ***)
19.81
19.82 -goal ZF.thy "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))";
19.83 +Goal "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))";
19.84 by (blast_tac (claset() addSEs [equalityE]) 1);
19.85 qed "subset_UN_iff_eq";
19.86
19.87 -qed_goal "UN_subset_iff" ZF.thy
19.88 +qed_goal "UN_subset_iff" thy
19.89 "(UN x:A. B(x)) <= C <-> (ALL x:A. B(x) <= C)"
19.90 (fn _ => [ Blast_tac 1 ]);
19.91
19.92 -qed_goal "UN_upper" ZF.thy
19.93 +qed_goal "UN_upper" thy
19.94 "!!x A. x:A ==> B(x) <= (UN x:A. B(x))"
19.95 (fn _ => [ etac (RepFunI RS Union_upper) 1 ]);
19.96
19.97 -qed_goal "UN_least" ZF.thy
19.98 +qed_goal "UN_least" thy
19.99 "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C"
19.100 (fn [prem]=>
19.101 [ (rtac (ballI RS (UN_subset_iff RS iffD2)) 1),
19.102 @@ -93,14 +93,14 @@
19.103
19.104 (*** Big Intersection -- greatest lower bound of a nonempty set ***)
19.105
19.106 -qed_goal "Inter_subset_iff" ZF.thy
19.107 +qed_goal "Inter_subset_iff" thy
19.108 "!!a A. a: A ==> C <= Inter(A) <-> (ALL x:A. C <= x)"
19.109 (fn _ => [ Blast_tac 1 ]);
19.110
19.111 -qed_goal "Inter_lower" ZF.thy "!!B A. B:A ==> Inter(A) <= B"
19.112 +qed_goal "Inter_lower" thy "!!B A. B:A ==> Inter(A) <= B"
19.113 (fn _ => [ Blast_tac 1 ]);
19.114
19.115 -qed_goal "Inter_greatest" ZF.thy
19.116 +qed_goal "Inter_greatest" thy
19.117 "[| a:A; !!x. x:A ==> C<=x |] ==> C <= Inter(A)"
19.118 (fn [prem1,prem2]=>
19.119 [ (rtac ([prem1, ballI] MRS (Inter_subset_iff RS iffD2)) 1),
19.120 @@ -108,11 +108,11 @@
19.121
19.122 (*** Intersection of a family of sets ***)
19.123
19.124 -qed_goal "INT_lower" ZF.thy
19.125 +qed_goal "INT_lower" thy
19.126 "!!x. x:A ==> (INT x:A. B(x)) <= B(x)"
19.127 (fn _ => [ Blast_tac 1 ]);
19.128
19.129 -qed_goal "INT_greatest" ZF.thy
19.130 +qed_goal "INT_greatest" thy
19.131 "[| a:A; !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))"
19.132 (fn [nonempty,prem] =>
19.133 [ rtac (nonempty RS RepFunI RS Inter_greatest) 1,
19.134 @@ -121,53 +121,58 @@
19.135
19.136 (*** Finite Union -- the least upper bound of 2 sets ***)
19.137
19.138 -qed_goal "Un_subset_iff" ZF.thy "A Un B <= C <-> A <= C & B <= C"
19.139 +qed_goal "Un_subset_iff" thy "A Un B <= C <-> A <= C & B <= C"
19.140 (fn _ => [ Blast_tac 1 ]);
19.141
19.142 -qed_goal "Un_upper1" ZF.thy "A <= A Un B"
19.143 +qed_goal "Un_upper1" thy "A <= A Un B"
19.144 (fn _ => [ Blast_tac 1 ]);
19.145
19.146 -qed_goal "Un_upper2" ZF.thy "B <= A Un B"
19.147 +qed_goal "Un_upper2" thy "B <= A Un B"
19.148 (fn _ => [ Blast_tac 1 ]);
19.149
19.150 -qed_goal "Un_least" ZF.thy "!!A B C. [| A<=C; B<=C |] ==> A Un B <= C"
19.151 +qed_goal "Un_least" thy "!!A B C. [| A<=C; B<=C |] ==> A Un B <= C"
19.152 (fn _ => [ Blast_tac 1 ]);
19.153
19.154
19.155 (*** Finite Intersection -- the greatest lower bound of 2 sets *)
19.156
19.157 -qed_goal "Int_subset_iff" ZF.thy "C <= A Int B <-> C <= A & C <= B"
19.158 +qed_goal "Int_subset_iff" thy "C <= A Int B <-> C <= A & C <= B"
19.159 (fn _ => [ Blast_tac 1 ]);
19.160
19.161 -qed_goal "Int_lower1" ZF.thy "A Int B <= A"
19.162 +qed_goal "Int_lower1" thy "A Int B <= A"
19.163 (fn _ => [ Blast_tac 1 ]);
19.164
19.165 -qed_goal "Int_lower2" ZF.thy "A Int B <= B"
19.166 +qed_goal "Int_lower2" thy "A Int B <= B"
19.167 (fn _ => [ Blast_tac 1 ]);
19.168
19.169 -qed_goal "Int_greatest" ZF.thy "!!A B C. [| C<=A; C<=B |] ==> C <= A Int B"
19.170 +qed_goal "Int_greatest" thy "!!A B C. [| C<=A; C<=B |] ==> C <= A Int B"
19.171 (fn _ => [ Blast_tac 1 ]);
19.172
19.173
19.174 (*** Set difference *)
19.175
19.176 -qed_goal "Diff_subset" ZF.thy "A-B <= A"
19.177 +qed_goal "Diff_subset" thy "A-B <= A"
19.178 (fn _ => [ Blast_tac 1 ]);
19.179
19.180 -qed_goal "Diff_contains" ZF.thy
19.181 +qed_goal "Diff_contains" thy
19.182 "!!C. [| C<=A; C Int B = 0 |] ==> C <= A-B"
19.183 - (fn _ => [ (blast_tac (claset() addSEs [equalityE]) 1) ]);
19.184 + (fn _ => [ Blast_tac 1 ]);
19.185 +
19.186 +Goal "B <= A - cons(c,C) <-> B<=A-C & c ~: B";
19.187 +by (Blast_tac 1);
19.188 +qed "subset_Diff_cons_iff";
19.189 +
19.190
19.191
19.192 (** Collect **)
19.193
19.194 -qed_goal "Collect_subset" ZF.thy "Collect(A,P) <= A"
19.195 +qed_goal "Collect_subset" thy "Collect(A,P) <= A"
19.196 (fn _ => [ Blast_tac 1 ]);
19.197
19.198
19.199 (** RepFun **)
19.200
19.201 -val prems = goal ZF.thy "[| !!x. x:A ==> f(x): B |] ==> {f(x). x:A} <= B";
19.202 +val prems = Goal "[| !!x. x:A ==> f(x): B |] ==> {f(x). x:A} <= B";
19.203 by (blast_tac (claset() addIs prems) 1);
19.204 qed "RepFun_subset";
19.205
20.1 --- a/src/ZF/upair.ML Mon Aug 17 13:06:29 1998 +0200
20.2 +++ b/src/ZF/upair.ML Mon Aug 17 13:09:08 1998 +0200
20.3 @@ -21,19 +21,19 @@
20.4
20.5 (*** Unordered pairs - Upair ***)
20.6
20.7 -qed_goalw "Upair_iff" ZF.thy [Upair_def]
20.8 +qed_goalw "Upair_iff" thy [Upair_def]
20.9 "c : Upair(a,b) <-> (c=a | c=b)"
20.10 (fn _ => [ (blast_tac (claset() addEs [Pow_neq_0, sym RS Pow_neq_0]) 1) ]);
20.11
20.12 Addsimps [Upair_iff];
20.13
20.14 -qed_goal "UpairI1" ZF.thy "a : Upair(a,b)"
20.15 +qed_goal "UpairI1" thy "a : Upair(a,b)"
20.16 (fn _ => [ Simp_tac 1 ]);
20.17
20.18 -qed_goal "UpairI2" ZF.thy "b : Upair(a,b)"
20.19 +qed_goal "UpairI2" thy "b : Upair(a,b)"
20.20 (fn _ => [ Simp_tac 1 ]);
20.21
20.22 -qed_goal "UpairE" ZF.thy
20.23 +qed_goal "UpairE" thy
20.24 "[| a : Upair(b,c); a=b ==> P; a=c ==> P |] ==> P"
20.25 (fn major::prems=>
20.26 [ (rtac (major RS (Upair_iff RS iffD1 RS disjE)) 1),
20.27 @@ -44,25 +44,25 @@
20.28
20.29 (*** Rules for binary union -- Un -- defined via Upair ***)
20.30
20.31 -qed_goalw "Un_iff" ZF.thy [Un_def] "c : A Un B <-> (c:A | c:B)"
20.32 +qed_goalw "Un_iff" thy [Un_def] "c : A Un B <-> (c:A | c:B)"
20.33 (fn _ => [ Blast_tac 1 ]);
20.34
20.35 Addsimps [Un_iff];
20.36
20.37 -qed_goal "UnI1" ZF.thy "!!c. c : A ==> c : A Un B"
20.38 +qed_goal "UnI1" thy "!!c. c : A ==> c : A Un B"
20.39 (fn _ => [ Asm_simp_tac 1 ]);
20.40
20.41 -qed_goal "UnI2" ZF.thy "!!c. c : B ==> c : A Un B"
20.42 +qed_goal "UnI2" thy "!!c. c : B ==> c : A Un B"
20.43 (fn _ => [ Asm_simp_tac 1 ]);
20.44
20.45 -qed_goal "UnE" ZF.thy
20.46 +qed_goal "UnE" thy
20.47 "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P"
20.48 (fn major::prems=>
20.49 [ (rtac (major RS (Un_iff RS iffD1 RS disjE)) 1),
20.50 (REPEAT (eresolve_tac prems 1)) ]);
20.51
20.52 (*Stronger version of the rule above*)
20.53 -qed_goal "UnE'" ZF.thy
20.54 +qed_goal "UnE'" thy
20.55 "[| c : A Un B; c:A ==> P; [| c:B; c~:A |] ==> P |] ==> P"
20.56 (fn major::prems =>
20.57 [(rtac (major RS UnE) 1),
20.58 @@ -73,7 +73,7 @@
20.59 (etac notnotD 1)]);
20.60
20.61 (*Classical introduction rule: no commitment to A vs B*)
20.62 -qed_goal "UnCI" ZF.thy "(c ~: B ==> c : A) ==> c : A Un B"
20.63 +qed_goal "UnCI" thy "(c ~: B ==> c : A) ==> c : A Un B"
20.64 (fn prems=>
20.65 [ Simp_tac 1, blast_tac (claset() addSIs prems) 1 ]);
20.66
20.67 @@ -83,21 +83,21 @@
20.68
20.69 (*** Rules for small intersection -- Int -- defined via Upair ***)
20.70
20.71 -qed_goalw "Int_iff" ZF.thy [Int_def] "c : A Int B <-> (c:A & c:B)"
20.72 +qed_goalw "Int_iff" thy [Int_def] "c : A Int B <-> (c:A & c:B)"
20.73 (fn _ => [ Blast_tac 1 ]);
20.74
20.75 Addsimps [Int_iff];
20.76
20.77 -qed_goal "IntI" ZF.thy "!!c. [| c : A; c : B |] ==> c : A Int B"
20.78 +qed_goal "IntI" thy "!!c. [| c : A; c : B |] ==> c : A Int B"
20.79 (fn _ => [ Asm_simp_tac 1 ]);
20.80
20.81 -qed_goal "IntD1" ZF.thy "!!c. c : A Int B ==> c : A"
20.82 +qed_goal "IntD1" thy "!!c. c : A Int B ==> c : A"
20.83 (fn _ => [ Asm_full_simp_tac 1 ]);
20.84
20.85 -qed_goal "IntD2" ZF.thy "!!c. c : A Int B ==> c : B"
20.86 +qed_goal "IntD2" thy "!!c. c : A Int B ==> c : B"
20.87 (fn _ => [ Asm_full_simp_tac 1 ]);
20.88
20.89 -qed_goal "IntE" ZF.thy
20.90 +qed_goal "IntE" thy
20.91 "[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P"
20.92 (fn prems=>
20.93 [ (resolve_tac prems 1),
20.94 @@ -108,21 +108,21 @@
20.95
20.96 (*** Rules for set difference -- defined via Upair ***)
20.97
20.98 -qed_goalw "Diff_iff" ZF.thy [Diff_def] "c : A-B <-> (c:A & c~:B)"
20.99 +qed_goalw "Diff_iff" thy [Diff_def] "c : A-B <-> (c:A & c~:B)"
20.100 (fn _ => [ Blast_tac 1 ]);
20.101
20.102 Addsimps [Diff_iff];
20.103
20.104 -qed_goal "DiffI" ZF.thy "!!c. [| c : A; c ~: B |] ==> c : A - B"
20.105 +qed_goal "DiffI" thy "!!c. [| c : A; c ~: B |] ==> c : A - B"
20.106 (fn _ => [ Asm_simp_tac 1 ]);
20.107
20.108 -qed_goal "DiffD1" ZF.thy "!!c. c : A - B ==> c : A"
20.109 +qed_goal "DiffD1" thy "!!c. c : A - B ==> c : A"
20.110 (fn _ => [ Asm_full_simp_tac 1 ]);
20.111
20.112 -qed_goal "DiffD2" ZF.thy "!!c. c : A - B ==> c ~: B"
20.113 +qed_goal "DiffD2" thy "!!c. c : A - B ==> c ~: B"
20.114 (fn _ => [ Asm_full_simp_tac 1 ]);
20.115
20.116 -qed_goal "DiffE" ZF.thy
20.117 +qed_goal "DiffE" thy
20.118 "[| c : A - B; [| c:A; c~:B |] ==> P |] ==> P"
20.119 (fn prems=>
20.120 [ (resolve_tac prems 1),
20.121 @@ -133,27 +133,27 @@
20.122
20.123 (*** Rules for cons -- defined via Un and Upair ***)
20.124
20.125 -qed_goalw "cons_iff" ZF.thy [cons_def] "a : cons(b,A) <-> (a=b | a:A)"
20.126 +qed_goalw "cons_iff" thy [cons_def] "a : cons(b,A) <-> (a=b | a:A)"
20.127 (fn _ => [ Blast_tac 1 ]);
20.128
20.129 Addsimps [cons_iff];
20.130
20.131 -qed_goal "consI1" ZF.thy "a : cons(a,B)"
20.132 +qed_goal "consI1" thy "a : cons(a,B)"
20.133 (fn _ => [ Simp_tac 1 ]);
20.134
20.135 Addsimps [consI1];
20.136
20.137 -qed_goal "consI2" ZF.thy "!!B. a : B ==> a : cons(b,B)"
20.138 +qed_goal "consI2" thy "!!B. a : B ==> a : cons(b,B)"
20.139 (fn _ => [ Asm_simp_tac 1 ]);
20.140
20.141 -qed_goal "consE" ZF.thy
20.142 +qed_goal "consE" thy
20.143 "[| a : cons(b,A); a=b ==> P; a:A ==> P |] ==> P"
20.144 (fn major::prems=>
20.145 [ (rtac (major RS (cons_iff RS iffD1 RS disjE)) 1),
20.146 (REPEAT (eresolve_tac (prems @ [UpairE]) 1)) ]);
20.147
20.148 (*Stronger version of the rule above*)
20.149 -qed_goal "consE'" ZF.thy
20.150 +qed_goal "consE'" thy
20.151 "[| a : cons(b,A); a=b ==> P; [| a:A; a~=b |] ==> P |] ==> P"
20.152 (fn major::prems =>
20.153 [(rtac (major RS consE) 1),
20.154 @@ -164,14 +164,14 @@
20.155 (etac notnotD 1)]);
20.156
20.157 (*Classical introduction rule*)
20.158 -qed_goal "consCI" ZF.thy "(a~:B ==> a=b) ==> a: cons(b,B)"
20.159 +qed_goal "consCI" thy "(a~:B ==> a=b) ==> a: cons(b,B)"
20.160 (fn prems=>
20.161 [ Simp_tac 1, blast_tac (claset() addSIs prems) 1 ]);
20.162
20.163 AddSIs [consCI];
20.164 AddSEs [consE];
20.165
20.166 -qed_goal "cons_not_0" ZF.thy "cons(a,B) ~= 0"
20.167 +qed_goal "cons_not_0" thy "cons(a,B) ~= 0"
20.168 (fn _ => [ (blast_tac (claset() addEs [equalityE]) 1) ]);
20.169
20.170 bind_thm ("cons_neq_0", cons_not_0 RS notE);
20.171 @@ -181,10 +181,10 @@
20.172
20.173 (*** Singletons - using cons ***)
20.174
20.175 -qed_goal "singleton_iff" ZF.thy "a : {b} <-> a=b"
20.176 +qed_goal "singleton_iff" thy "a : {b} <-> a=b"
20.177 (fn _ => [ Simp_tac 1 ]);
20.178
20.179 -qed_goal "singletonI" ZF.thy "a : {a}"
20.180 +qed_goal "singletonI" thy "a : {a}"
20.181 (fn _=> [ (rtac consI1 1) ]);
20.182
20.183 bind_thm ("singletonE", make_elim (singleton_iff RS iffD1));
20.184 @@ -194,25 +194,25 @@
20.185
20.186 (*** Rules for Descriptions ***)
20.187
20.188 -qed_goalw "the_equality" ZF.thy [the_def]
20.189 +qed_goalw "the_equality" thy [the_def]
20.190 "[| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"
20.191 (fn [pa,eq] =>
20.192 [ (fast_tac (claset() addSIs [pa] addEs [eq RS subst]) 1) ]);
20.193
20.194 (* Only use this if you already know EX!x. P(x) *)
20.195 -qed_goal "the_equality2" ZF.thy
20.196 +qed_goal "the_equality2" thy
20.197 "!!P. [| EX! x. P(x); P(a) |] ==> (THE x. P(x)) = a"
20.198 (fn _ =>
20.199 [ (deepen_tac (claset() addSIs [the_equality]) 1 1) ]);
20.200
20.201 -qed_goal "theI" ZF.thy "EX! x. P(x) ==> P(THE x. P(x))"
20.202 +qed_goal "theI" thy "EX! x. P(x) ==> P(THE x. P(x))"
20.203 (fn [major]=>
20.204 [ (rtac (major RS ex1E) 1),
20.205 (resolve_tac [major RS the_equality2 RS ssubst] 1),
20.206 (REPEAT (assume_tac 1)) ]);
20.207
20.208 (*Easier to apply than theI: conclusion has only one occurrence of P*)
20.209 -qed_goal "theI2" ZF.thy
20.210 +qed_goal "theI2" thy
20.211 "[| EX! x. P(x); !!x. P(x) ==> Q(x) |] ==> Q(THE x. P(x))"
20.212 (fn prems => [ resolve_tac prems 1,
20.213 rtac theI 1,
20.214 @@ -222,42 +222,42 @@
20.215 (THE x.P(x)) rewrites to (THE x. Q(x)) *)
20.216
20.217 (*If it's "undefined", it's zero!*)
20.218 -qed_goalw "the_0" ZF.thy [the_def]
20.219 +qed_goalw "the_0" thy [the_def]
20.220 "!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0"
20.221 (fn _ => [ (deepen_tac (claset() addSEs [ReplaceE]) 0 1) ]);
20.222
20.223
20.224 (*** if -- a conditional expression for formulae ***)
20.225
20.226 -goalw ZF.thy [if_def] "if(True,a,b) = a";
20.227 +Goalw [if_def] "if(True,a,b) = a";
20.228 by (blast_tac (claset() addSIs [the_equality]) 1);
20.229 qed "if_true";
20.230
20.231 -goalw ZF.thy [if_def] "if(False,a,b) = b";
20.232 +Goalw [if_def] "if(False,a,b) = b";
20.233 by (blast_tac (claset() addSIs [the_equality]) 1);
20.234 qed "if_false";
20.235
20.236 (*Never use with case splitting, or if P is known to be true or false*)
20.237 -val prems = goalw ZF.thy [if_def]
20.238 +val prems = Goalw [if_def]
20.239 "[| P<->Q; Q ==> a=c; ~Q ==> b=d |] ==> if(P,a,b) = if(Q,c,d)";
20.240 by (simp_tac (simpset() addsimps prems addcongs [conj_cong]) 1);
20.241 qed "if_cong";
20.242
20.243 (*Not needed for rewriting, since P would rewrite to True anyway*)
20.244 -goalw ZF.thy [if_def] "!!P. P ==> if(P,a,b) = a";
20.245 +Goalw [if_def] "P ==> if(P,a,b) = a";
20.246 by (blast_tac (claset() addSIs [the_equality]) 1);
20.247 qed "if_P";
20.248
20.249 (*Not needed for rewriting, since P would rewrite to False anyway*)
20.250 -goalw ZF.thy [if_def] "!!P. ~P ==> if(P,a,b) = b";
20.251 +Goalw [if_def] "~P ==> if(P,a,b) = b";
20.252 by (blast_tac (claset() addSIs [the_equality]) 1);
20.253 qed "if_not_P";
20.254
20.255 Addsimps [if_true, if_false];
20.256
20.257 -qed_goal "split_if" ZF.thy
20.258 +qed_goal "split_if" thy
20.259 "P(if(Q,x,y)) <-> ((Q --> P(x)) & (~Q --> P(y)))"
20.260 - (fn _=> [ (excluded_middle_tac "Q" 1),
20.261 + (fn _=> [ (case_tac "Q" 1),
20.262 (Asm_simp_tac 1),
20.263 (Asm_simp_tac 1) ]);
20.264
20.265 @@ -275,10 +275,10 @@
20.266 split_if_mem1, split_if_mem2];
20.267
20.268 (*Logically equivalent to split_if_mem2*)
20.269 -qed_goal "if_iff" ZF.thy "a: if(P,x,y) <-> P & a:x | ~P & a:y"
20.270 +qed_goal "if_iff" thy "a: if(P,x,y) <-> P & a:x | ~P & a:y"
20.271 (fn _=> [ (simp_tac (simpset() addsplits [split_if]) 1) ]);
20.272
20.273 -qed_goal "if_type" ZF.thy
20.274 +qed_goal "if_type" thy
20.275 "[| P ==> a: A; ~P ==> b: A |] ==> if(P,a,b): A"
20.276 (fn prems=> [ (simp_tac
20.277 (simpset() addsimps prems addsplits [split_if]) 1) ]);
20.278 @@ -287,48 +287,48 @@
20.279 (*** Foundation lemmas ***)
20.280
20.281 (*was called mem_anti_sym*)
20.282 -qed_goal "mem_asym" ZF.thy "[| a:b; ~P ==> b:a |] ==> P"
20.283 +qed_goal "mem_asym" thy "[| a:b; ~P ==> b:a |] ==> P"
20.284 (fn prems=>
20.285 [ (rtac classical 1),
20.286 (res_inst_tac [("A1","{a,b}")] (foundation RS disjE) 1),
20.287 REPEAT (blast_tac (claset() addIs prems addSEs [equalityE]) 1) ]);
20.288
20.289 (*was called mem_anti_refl*)
20.290 -qed_goal "mem_irrefl" ZF.thy "a:a ==> P"
20.291 +qed_goal "mem_irrefl" thy "a:a ==> P"
20.292 (fn [major]=> [ (rtac ([major,major] MRS mem_asym) 1) ]);
20.293
20.294 (*mem_irrefl should NOT be added to default databases:
20.295 it would be tried on most goals, making proofs slower!*)
20.296
20.297 -qed_goal "mem_not_refl" ZF.thy "a ~: a"
20.298 +qed_goal "mem_not_refl" thy "a ~: a"
20.299 (K [ (rtac notI 1), (etac mem_irrefl 1) ]);
20.300
20.301 (*Good for proving inequalities by rewriting*)
20.302 -qed_goal "mem_imp_not_eq" ZF.thy "!!a A. a:A ==> a ~= A"
20.303 +qed_goal "mem_imp_not_eq" thy "!!a A. a:A ==> a ~= A"
20.304 (fn _=> [ blast_tac (claset() addSEs [mem_irrefl]) 1 ]);
20.305
20.306 (*** Rules for succ ***)
20.307
20.308 -qed_goalw "succ_iff" ZF.thy [succ_def] "i : succ(j) <-> i=j | i:j"
20.309 +qed_goalw "succ_iff" thy [succ_def] "i : succ(j) <-> i=j | i:j"
20.310 (fn _ => [ Blast_tac 1 ]);
20.311
20.312 -qed_goalw "succI1" ZF.thy [succ_def] "i : succ(i)"
20.313 +qed_goalw "succI1" thy [succ_def] "i : succ(i)"
20.314 (fn _=> [ (rtac consI1 1) ]);
20.315
20.316 Addsimps [succI1];
20.317
20.318 -qed_goalw "succI2" ZF.thy [succ_def]
20.319 +qed_goalw "succI2" thy [succ_def]
20.320 "i : j ==> i : succ(j)"
20.321 (fn [prem]=> [ (rtac (prem RS consI2) 1) ]);
20.322
20.323 -qed_goalw "succE" ZF.thy [succ_def]
20.324 +qed_goalw "succE" thy [succ_def]
20.325 "[| i : succ(j); i=j ==> P; i:j ==> P |] ==> P"
20.326 (fn major::prems=>
20.327 [ (rtac (major RS consE) 1),
20.328 (REPEAT (eresolve_tac prems 1)) ]);
20.329
20.330 (*Classical introduction rule*)
20.331 -qed_goal "succCI" ZF.thy "(i~:j ==> i=j) ==> i: succ(j)"
20.332 +qed_goal "succCI" thy "(i~:j ==> i=j) ==> i: succ(j)"
20.333 (fn [prem]=>
20.334 [ (rtac (disjCI RS (succ_iff RS iffD2)) 1),
20.335 (etac prem 1) ]);
20.336 @@ -336,7 +336,7 @@
20.337 AddSIs [succCI];
20.338 AddSEs [succE];
20.339
20.340 -qed_goal "succ_not_0" ZF.thy "succ(n) ~= 0"
20.341 +qed_goal "succ_not_0" thy "succ(n) ~= 0"
20.342 (fn _=> [ (blast_tac (claset() addSEs [equalityE]) 1) ]);
20.343
20.344 bind_thm ("succ_neq_0", succ_not_0 RS notE);
20.345 @@ -352,7 +352,7 @@
20.346 bind_thm ("succ_neq_self", succI1 RS mem_imp_not_eq RS not_sym);
20.347
20.348
20.349 -qed_goal "succ_inject_iff" ZF.thy "succ(m) = succ(n) <-> m=n"
20.350 +qed_goal "succ_inject_iff" thy "succ(m) = succ(n) <-> m=n"
20.351 (fn _=> [ (blast_tac (claset() addEs [mem_asym] addSEs [equalityE]) 1) ]);
20.352
20.353 bind_thm ("succ_inject", succ_inject_iff RS iffD1);