1.1 --- a/src/ZF/AC.ML Fri Aug 14 13:52:42 1998 +0200
1.2 +++ b/src/ZF/AC.ML Fri Aug 14 18:37:28 1998 +0200
1.3 @@ -61,3 +61,9 @@
1.4 by (REPEAT (ares_tac [non_empty_family] 1));
1.5 qed "AC_Pi0";
1.6
1.7 +(*Used in Zorn.ML*)
1.8 +Goal "[| ch : (PROD X:Pow(S) - {0}. X); X<=S; X~=S |] ==> ch ` (S-X) : S-X";
1.9 +by (etac apply_type 1);
1.10 +by (blast_tac (claset() addSEs [equalityE]) 1);
1.11 +qed "choice_Diff";
1.12 +
2.1 --- a/src/ZF/Fixedpt.ML Fri Aug 14 13:52:42 1998 +0200
2.2 +++ b/src/ZF/Fixedpt.ML Fri Aug 14 18:37:28 1998 +0200
2.3 @@ -3,7 +3,7 @@
2.4 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
2.5 Copyright 1992 University of Cambridge
2.6
2.7 -For fixedpt.thy. Least and greatest fixed points; the Knaster-Tarski Theorem
2.8 +Least and greatest fixed points; the Knaster-Tarski Theorem
2.9
2.10 Proved in the lattice of subsets of D, namely Pow(D), with Inter as glb
2.11 *)
2.12 @@ -12,7 +12,7 @@
2.13
2.14 (*** Monotone operators ***)
2.15
2.16 -val prems = goalw Fixedpt.thy [bnd_mono_def]
2.17 +val prems = Goalw [bnd_mono_def]
2.18 "[| h(D)<=D; \
2.19 \ !!W X. [| W<=D; X<=D; W<=X |] ==> h(W) <= h(X) \
2.20 \ |] ==> bnd_mono(D,h)";
2.21 @@ -20,14 +20,12 @@
2.22 ORELSE etac subset_trans 1));
2.23 qed "bnd_monoI";
2.24
2.25 -val [major] = goalw Fixedpt.thy [bnd_mono_def] "bnd_mono(D,h) ==> h(D) <= D";
2.26 -by (rtac (major RS conjunct1) 1);
2.27 +Goalw [bnd_mono_def] "bnd_mono(D,h) ==> h(D) <= D";
2.28 +by (etac conjunct1 1);
2.29 qed "bnd_monoD1";
2.30
2.31 -val major::prems = goalw Fixedpt.thy [bnd_mono_def]
2.32 - "[| bnd_mono(D,h); W<=X; X<=D |] ==> h(W) <= h(X)";
2.33 -by (rtac (major RS conjunct2 RS spec RS spec RS mp RS mp) 1);
2.34 -by (REPEAT (resolve_tac prems 1));
2.35 +Goalw [bnd_mono_def] "[| bnd_mono(D,h); W<=X; X<=D |] ==> h(W) <= h(X)";
2.36 +by (Blast_tac 1);
2.37 qed "bnd_monoD2";
2.38
2.39 val [major,minor] = goal Fixedpt.thy
2.40 @@ -71,7 +69,7 @@
2.41 by (rtac lfp_subset 1);
2.42 qed "def_lfp_subset";
2.43
2.44 -val prems = goalw Fixedpt.thy [lfp_def]
2.45 +val prems = Goalw [lfp_def]
2.46 "[| h(D) <= D; !!X. [| h(X) <= X; X<=D |] ==> A<=X |] ==> \
2.47 \ A <= lfp(D,h)";
2.48 by (rtac (Pow_top RS CollectI RS Inter_greatest) 1);
2.49 @@ -85,11 +83,10 @@
2.50 by (REPEAT (resolve_tac prems 1));
2.51 qed "lfp_lemma1";
2.52
2.53 -val [hmono] = goal Fixedpt.thy
2.54 - "bnd_mono(D,h) ==> h(lfp(D,h)) <= lfp(D,h)";
2.55 +Goal "bnd_mono(D,h) ==> h(lfp(D,h)) <= lfp(D,h)";
2.56 by (rtac (bnd_monoD1 RS lfp_greatest) 1);
2.57 by (rtac lfp_lemma1 2);
2.58 -by (REPEAT (ares_tac [hmono] 1));
2.59 +by (REPEAT (assume_tac 1));
2.60 qed "lfp_lemma2";
2.61
2.62 val [hmono] = goal Fixedpt.thy
2.63 @@ -101,9 +98,8 @@
2.64 by (REPEAT (rtac lfp_subset 1));
2.65 qed "lfp_lemma3";
2.66
2.67 -val prems = goal Fixedpt.thy
2.68 - "bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))";
2.69 -by (REPEAT (resolve_tac (prems@[equalityI,lfp_lemma2,lfp_lemma3]) 1));
2.70 +Goal "bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))";
2.71 +by (REPEAT (ares_tac [equalityI,lfp_lemma2,lfp_lemma3] 1));
2.72 qed "lfp_Tarski";
2.73
2.74 (*Definition form, to control unfolding*)
2.75 @@ -115,7 +111,7 @@
2.76
2.77 (*** General induction rule for least fixedpoints ***)
2.78
2.79 -val [hmono,indstep] = goal Fixedpt.thy
2.80 +val [hmono,indstep] = Goal
2.81 "[| bnd_mono(D,h); !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) \
2.82 \ |] ==> h(Collect(lfp(D,h),P)) <= Collect(lfp(D,h),P)";
2.83 by (rtac subsetI 1);
2.84 @@ -128,7 +124,7 @@
2.85
2.86 (*This rule yields an induction hypothesis in which the components of a
2.87 data structure may be assumed to be elements of lfp(D,h)*)
2.88 -val prems = goal Fixedpt.thy
2.89 +val prems = Goal
2.90 "[| bnd_mono(D,h); a : lfp(D,h); \
2.91 \ !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) \
2.92 \ |] ==> P(a)";
2.93 @@ -138,7 +134,7 @@
2.94 qed "induct";
2.95
2.96 (*Definition form, to control unfolding*)
2.97 -val rew::prems = goal Fixedpt.thy
2.98 +val rew::prems = Goal
2.99 "[| A == lfp(D,h); bnd_mono(D,h); a:A; \
2.100 \ !!x. x : h(Collect(A,P)) ==> P(x) \
2.101 \ |] ==> P(a)";
2.102 @@ -157,7 +153,7 @@
2.103
2.104 (*Monotonicity of lfp, where h precedes i under a domain-like partial order
2.105 monotonicity of h is not strictly necessary; h must be bounded by D*)
2.106 -val [hmono,imono,subhi] = goal Fixedpt.thy
2.107 +val [hmono,imono,subhi] = Goal
2.108 "[| bnd_mono(D,h); bnd_mono(E,i); \
2.109 \ !!X. X<=D ==> h(X) <= i(X) |] ==> lfp(D,h) <= lfp(E,i)";
2.110 by (rtac (bnd_monoD1 RS lfp_greatest) 1);
2.111 @@ -170,7 +166,7 @@
2.112
2.113 (*This (unused) version illustrates that monotonicity is not really needed,
2.114 but both lfp's must be over the SAME set D; Inter is anti-monotonic!*)
2.115 -val [isubD,subhi] = goal Fixedpt.thy
2.116 +val [isubD,subhi] = Goal
2.117 "[| i(D) <= D; !!X. X<=D ==> h(X) <= i(X) |] ==> lfp(D,h) <= lfp(D,i)";
2.118 by (rtac lfp_greatest 1);
2.119 by (rtac isubD 1);
2.120 @@ -183,10 +179,9 @@
2.121 (**** Proof of Knaster-Tarski Theorem for the gfp ****)
2.122
2.123 (*gfp contains each post-fixedpoint that is contained in D*)
2.124 -val prems = goalw Fixedpt.thy [gfp_def]
2.125 - "[| A <= h(A); A<=D |] ==> A <= gfp(D,h)";
2.126 +Goalw [gfp_def] "[| A <= h(A); A<=D |] ==> A <= gfp(D,h)";
2.127 by (rtac (PowI RS CollectI RS Union_upper) 1);
2.128 -by (REPEAT (resolve_tac prems 1));
2.129 +by (REPEAT (assume_tac 1));
2.130 qed "gfp_upperbound";
2.131
2.132 Goalw [gfp_def] "gfp(D,h) <= D";
2.133 @@ -199,7 +194,7 @@
2.134 by (rtac gfp_subset 1);
2.135 qed "def_gfp_subset";
2.136
2.137 -val hmono::prems = goalw Fixedpt.thy [gfp_def]
2.138 +val hmono::prems = Goalw [gfp_def]
2.139 "[| bnd_mono(D,h); !!X. [| X <= h(X); X<=D |] ==> X<=A |] ==> \
2.140 \ gfp(D,h) <= A";
2.141 by (fast_tac (subset_cs addIs ((hmono RS bnd_monoD1)::prems)) 1);
2.142 @@ -213,11 +208,10 @@
2.143 by (REPEAT (resolve_tac prems 1));
2.144 qed "gfp_lemma1";
2.145
2.146 -val [hmono] = goal Fixedpt.thy
2.147 - "bnd_mono(D,h) ==> gfp(D,h) <= h(gfp(D,h))";
2.148 +Goal "bnd_mono(D,h) ==> gfp(D,h) <= h(gfp(D,h))";
2.149 by (rtac gfp_least 1);
2.150 by (rtac gfp_lemma1 2);
2.151 -by (REPEAT (ares_tac [hmono] 1));
2.152 +by (REPEAT (assume_tac 1));
2.153 qed "gfp_lemma2";
2.154
2.155 val [hmono] = goal Fixedpt.thy
2.156 @@ -228,9 +222,8 @@
2.157 by (REPEAT (rtac ([hmono, gfp_subset] MRS bnd_mono_subset) 1));
2.158 qed "gfp_lemma3";
2.159
2.160 -val prems = goal Fixedpt.thy
2.161 - "bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))";
2.162 -by (REPEAT (resolve_tac (prems@[equalityI,gfp_lemma2,gfp_lemma3]) 1));
2.163 +Goal "bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))";
2.164 +by (REPEAT (ares_tac [equalityI,gfp_lemma2,gfp_lemma3] 1));
2.165 qed "gfp_Tarski";
2.166
2.167 (*Definition form, to control unfolding*)
2.168 @@ -275,7 +268,7 @@
2.169 qed "def_coinduct";
2.170
2.171 (*Lemma used immediately below!*)
2.172 -val [subsA,XimpP] = goal ZF.thy
2.173 +val [subsA,XimpP] = Goal
2.174 "[| X <= A; !!z. z:X ==> P(z) |] ==> X <= Collect(A,P)";
2.175 by (rtac (subsA RS subsetD RS CollectI RS subsetI) 1);
2.176 by (assume_tac 1);
2.177 @@ -283,7 +276,7 @@
2.178 qed "subset_Collect";
2.179
2.180 (*The version used in the induction/coinduction package*)
2.181 -val prems = goal Fixedpt.thy
2.182 +val prems = Goal
2.183 "[| A == gfp(D, %w. Collect(D,P(w))); bnd_mono(D, %w. Collect(D,P(w))); \
2.184 \ a: X; X <= D; !!z. z: X ==> P(X Un A, z) |] ==> \
2.185 \ a : A";
2.186 @@ -292,7 +285,7 @@
2.187 qed "def_Collect_coinduct";
2.188
2.189 (*Monotonicity of gfp!*)
2.190 -val [hmono,subde,subhi] = goal Fixedpt.thy
2.191 +val [hmono,subde,subhi] = Goal
2.192 "[| bnd_mono(D,h); D <= E; \
2.193 \ !!X. X<=D ==> h(X) <= i(X) |] ==> gfp(D,h) <= gfp(E,i)";
2.194 by (rtac gfp_upperbound 1);
3.1 --- a/src/ZF/List.ML Fri Aug 14 13:52:42 1998 +0200
3.2 +++ b/src/ZF/List.ML Fri Aug 14 18:37:28 1998 +0200
3.3 @@ -55,7 +55,7 @@
3.4 by (REPEAT (ares_tac [list_subset_univ RS subsetD] 1));
3.5 qed "list_into_univ";
3.6
3.7 -val major::prems = goal List.thy
3.8 +val major::prems = Goal
3.9 "[| l: list(A); \
3.10 \ c: C(Nil); \
3.11 \ !!x y. [| x: A; y: list(A) |] ==> h(x,y): C(Cons(x,y)) \
3.12 @@ -142,7 +142,7 @@
3.13
3.14
3.15 (*Type checking -- proved by induction, as usual*)
3.16 -val prems = goal List.thy
3.17 +val prems = Goal
3.18 "[| l: list(A); \
3.19 \ c: C(Nil); \
3.20 \ !!x y r. [| x:A; y: list(A); r: C(y) |] ==> h(x,y,r): C(Cons(x,y)) \
3.21 @@ -153,14 +153,12 @@
3.22
3.23 (** Versions for use with definitions **)
3.24
3.25 -val [rew] = goal List.thy
3.26 - "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Nil) = c";
3.27 +val [rew] = Goal "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Nil) = c";
3.28 by (rewtac rew);
3.29 by (rtac list_rec_Nil 1);
3.30 qed "def_list_rec_Nil";
3.31
3.32 -val [rew] = goal List.thy
3.33 - "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Cons(a,l)) = h(a,l,j(l))";
3.34 +val [rew] = Goal "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Cons(a,l)) = h(a,l,j(l))";
3.35 by (rewtac rew);
3.36 by (rtac list_rec_Cons 1);
3.37 qed "def_list_rec_Cons";
3.38 @@ -173,13 +171,13 @@
3.39 val [map_Nil,map_Cons] = list_recs map_def;
3.40 Addsimps [map_Nil, map_Cons];
3.41
3.42 -val prems = goalw List.thy [map_def]
3.43 +val prems = Goalw [map_def]
3.44 "[| l: list(A); !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)";
3.45 by (REPEAT (ares_tac (prems @ list.intrs @ [list_rec_type]) 1));
3.46 qed "map_type";
3.47
3.48 -val [major] = goal List.thy "l: list(A) ==> map(h,l) : list({h(u). u:A})";
3.49 -by (rtac (major RS map_type) 1);
3.50 +Goal "l: list(A) ==> map(h,l) : list({h(u). u:A})";
3.51 +by (etac map_type 1);
3.52 by (etac RepFunI 1);
3.53 qed "map_type2";
3.54
3.55 @@ -263,35 +261,30 @@
3.56
3.57 (*** theorems about map ***)
3.58
3.59 -val prems = goal List.thy
3.60 - "l: list(A) ==> map(%u. u, l) = l";
3.61 -by (list_ind_tac "l" prems 1);
3.62 +Goal "l: list(A) ==> map(%u. u, l) = l";
3.63 +by (list_ind_tac "l" [] 1);
3.64 by (ALLGOALS Asm_simp_tac);
3.65 qed "map_ident";
3.66
3.67 -val prems = goal List.thy
3.68 - "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)";
3.69 -by (list_ind_tac "l" prems 1);
3.70 +Goal "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)";
3.71 +by (list_ind_tac "l" [] 1);
3.72 by (ALLGOALS Asm_simp_tac);
3.73 qed "map_compose";
3.74
3.75 -val prems = goal List.thy
3.76 - "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";
3.77 -by (list_ind_tac "xs" prems 1);
3.78 +Goal "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";
3.79 +by (list_ind_tac "xs" [] 1);
3.80 by (ALLGOALS Asm_simp_tac);
3.81 qed "map_app_distrib";
3.82
3.83 -val prems = goal List.thy
3.84 - "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))";
3.85 -by (list_ind_tac "ls" prems 1);
3.86 +Goal "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))";
3.87 +by (list_ind_tac "ls" [] 1);
3.88 by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib])));
3.89 qed "map_flat";
3.90
3.91 -val prems = goal List.thy
3.92 - "l: list(A) ==> \
3.93 +Goal "l: list(A) ==> \
3.94 \ list_rec(map(h,l), c, d) = \
3.95 \ list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))";
3.96 -by (list_ind_tac "l" prems 1);
3.97 +by (list_ind_tac "l" [] 1);
3.98 by (ALLGOALS Asm_simp_tac);
3.99 qed "list_rec_map";
3.100
3.101 @@ -300,23 +293,20 @@
3.102 (* c : list(Collect(B,P)) ==> c : list(B) *)
3.103 bind_thm ("list_CollectD", (Collect_subset RS list_mono RS subsetD));
3.104
3.105 -val prems = goal List.thy
3.106 - "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
3.107 -by (list_ind_tac "l" prems 1);
3.108 +Goal "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
3.109 +by (list_ind_tac "l" [] 1);
3.110 by (ALLGOALS Asm_simp_tac);
3.111 qed "map_list_Collect";
3.112
3.113 (*** theorems about length ***)
3.114
3.115 -val prems = goal List.thy
3.116 - "xs: list(A) ==> length(map(h,xs)) = length(xs)";
3.117 -by (list_ind_tac "xs" prems 1);
3.118 +Goal "xs: list(A) ==> length(map(h,xs)) = length(xs)";
3.119 +by (list_ind_tac "xs" [] 1);
3.120 by (ALLGOALS Asm_simp_tac);
3.121 qed "length_map";
3.122
3.123 -val prems = goal List.thy
3.124 - "xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)";
3.125 -by (list_ind_tac "xs" prems 1);
3.126 +Goal "xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)";
3.127 +by (list_ind_tac "xs" [] 1);
3.128 by (ALLGOALS Asm_simp_tac);
3.129 qed "length_app";
3.130
3.131 @@ -324,15 +314,13 @@
3.132 Used for rewriting below*)
3.133 val add_commute_succ = nat_succI RSN (2,add_commute);
3.134
3.135 -val prems = goal List.thy
3.136 - "xs: list(A) ==> length(rev(xs)) = length(xs)";
3.137 -by (list_ind_tac "xs" prems 1);
3.138 +Goal "xs: list(A) ==> length(rev(xs)) = length(xs)";
3.139 +by (list_ind_tac "xs" [] 1);
3.140 by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app, add_commute_succ])));
3.141 qed "length_rev";
3.142
3.143 -val prems = goal List.thy
3.144 - "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
3.145 -by (list_ind_tac "ls" prems 1);
3.146 +Goal "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
3.147 +by (list_ind_tac "ls" [] 1);
3.148 by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app])));
3.149 qed "length_flat";
3.150
3.151 @@ -364,26 +352,25 @@
3.152
3.153 (*** theorems about app ***)
3.154
3.155 -val [major] = goal List.thy "xs: list(A) ==> xs@Nil=xs";
3.156 -by (rtac (major RS list.induct) 1);
3.157 +Goal "xs: list(A) ==> xs@Nil=xs";
3.158 +by (etac list.induct 1);
3.159 by (ALLGOALS Asm_simp_tac);
3.160 qed "app_right_Nil";
3.161
3.162 -val prems = goal List.thy "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
3.163 -by (list_ind_tac "xs" prems 1);
3.164 +Goal "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
3.165 +by (list_ind_tac "xs" [] 1);
3.166 by (ALLGOALS Asm_simp_tac);
3.167 qed "app_assoc";
3.168
3.169 -val prems = goal List.thy
3.170 - "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)";
3.171 -by (list_ind_tac "ls" prems 1);
3.172 +Goal "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)";
3.173 +by (list_ind_tac "ls" [] 1);
3.174 by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_assoc])));
3.175 qed "flat_app_distrib";
3.176
3.177 (*** theorems about rev ***)
3.178
3.179 -val prems = goal List.thy "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))";
3.180 -by (list_ind_tac "l" prems 1);
3.181 +Goal "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))";
3.182 +by (list_ind_tac "l" [] 1);
3.183 by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib])));
3.184 qed "rev_map_distrib";
3.185
3.186 @@ -396,14 +383,13 @@
3.187 by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_right_Nil,app_assoc])));
3.188 qed "rev_app_distrib";
3.189
3.190 -val prems = goal List.thy "l: list(A) ==> rev(rev(l))=l";
3.191 -by (list_ind_tac "l" prems 1);
3.192 +Goal "l: list(A) ==> rev(rev(l))=l";
3.193 +by (list_ind_tac "l" [] 1);
3.194 by (ALLGOALS (asm_simp_tac (simpset() addsimps [rev_app_distrib])));
3.195 qed "rev_rev_ident";
3.196
3.197 -val prems = goal List.thy
3.198 - "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
3.199 -by (list_ind_tac "ls" prems 1);
3.200 +Goal "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
3.201 +by (list_ind_tac "ls" [] 1);
3.202 by (ALLGOALS (asm_simp_tac (simpset() addsimps
3.203 [map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil])));
3.204 qed "rev_flat";
3.205 @@ -411,34 +397,30 @@
3.206
3.207 (*** theorems about list_add ***)
3.208
3.209 -val prems = goal List.thy
3.210 - "[| xs: list(nat); ys: list(nat) |] ==> \
3.211 +Goal "[| xs: list(nat); ys: list(nat) |] ==> \
3.212 \ list_add(xs@ys) = list_add(ys) #+ list_add(xs)";
3.213 -by (cut_facts_tac prems 1);
3.214 -by (list_ind_tac "xs" prems 1);
3.215 +by (list_ind_tac "xs" [] 1);
3.216 by (ALLGOALS
3.217 (asm_simp_tac (simpset() addsimps [add_0_right, add_assoc RS sym])));
3.218 by (rtac (add_commute RS subst_context) 1);
3.219 by (REPEAT (ares_tac [refl, list_add_type] 1));
3.220 qed "list_add_app";
3.221
3.222 -val prems = goal List.thy
3.223 - "l: list(nat) ==> list_add(rev(l)) = list_add(l)";
3.224 -by (list_ind_tac "l" prems 1);
3.225 +Goal "l: list(nat) ==> list_add(rev(l)) = list_add(l)";
3.226 +by (list_ind_tac "l" [] 1);
3.227 by (ALLGOALS
3.228 (asm_simp_tac (simpset() addsimps [list_add_app, add_0_right])));
3.229 qed "list_add_rev";
3.230
3.231 -val prems = goal List.thy
3.232 - "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))";
3.233 -by (list_ind_tac "ls" prems 1);
3.234 +Goal "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))";
3.235 +by (list_ind_tac "ls" [] 1);
3.236 by (ALLGOALS (asm_simp_tac (simpset() addsimps [list_add_app])));
3.237 by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1));
3.238 qed "list_add_flat";
3.239
3.240 (** New induction rule **)
3.241
3.242 -val major::prems = goal List.thy
3.243 +val major::prems = Goal
3.244 "[| l: list(A); \
3.245 \ P(Nil); \
3.246 \ !!x y. [| x: A; y: list(A); P(y) |] ==> P(y @ [x]) \
4.1 --- a/src/ZF/Ordinal.ML Fri Aug 14 13:52:42 1998 +0200
4.2 +++ b/src/ZF/Ordinal.ML Fri Aug 14 18:37:28 1998 +0200
4.3 @@ -3,7 +3,7 @@
4.4 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4.5 Copyright 1993 University of Cambridge
4.6
4.7 -For Ordinal.thy. Ordinals in Zermelo-Fraenkel Set Theory
4.8 +Ordinals in Zermelo-Fraenkel Set Theory
4.9 *)
4.10
4.11 open Ordinal;
4.12 @@ -73,12 +73,12 @@
4.13 by (Blast_tac 1);
4.14 qed "Transset_Union";
4.15
4.16 -val [Transprem] = goalw Ordinal.thy [Transset_def]
4.17 +val [Transprem] = Goalw [Transset_def]
4.18 "[| !!i. i:A ==> Transset(i) |] ==> Transset(Union(A))";
4.19 by (blast_tac (claset() addDs [Transprem RS bspec RS subsetD]) 1);
4.20 qed "Transset_Union_family";
4.21
4.22 -val [prem,Transprem] = goalw Ordinal.thy [Transset_def]
4.23 +val [prem,Transprem] = Goalw [Transset_def]
4.24 "[| j:A; !!i. i:A ==> Transset(i) |] ==> Transset(Inter(A))";
4.25 by (cut_facts_tac [prem] 1);
4.26 by (blast_tac (claset() addDs [Transprem RS bspec RS subsetD]) 1);
4.27 @@ -86,19 +86,18 @@
4.28
4.29 (*** Natural Deduction rules for Ord ***)
4.30
4.31 -val prems = goalw Ordinal.thy [Ord_def]
4.32 +val prems = Goalw [Ord_def]
4.33 "[| Transset(i); !!x. x:i ==> Transset(x) |] ==> Ord(i)";
4.34 by (REPEAT (ares_tac (prems@[ballI,conjI]) 1));
4.35 qed "OrdI";
4.36
4.37 -val [major] = goalw Ordinal.thy [Ord_def]
4.38 - "Ord(i) ==> Transset(i)";
4.39 -by (rtac (major RS conjunct1) 1);
4.40 +Goalw [Ord_def] "Ord(i) ==> Transset(i)";
4.41 +by (Blast_tac 1);
4.42 qed "Ord_is_Transset";
4.43
4.44 -val [major,minor] = goalw Ordinal.thy [Ord_def]
4.45 +Goalw [Ord_def]
4.46 "[| Ord(i); j:i |] ==> Transset(j) ";
4.47 -by (rtac (minor RS (major RS conjunct2 RS bspec)) 1);
4.48 +by (Blast_tac 1);
4.49 qed "Ord_contains_Transset";
4.50
4.51 (*** Lemmas for ordinals ***)
4.52 @@ -159,7 +158,7 @@
4.53 by (blast_tac (claset() addSIs [Transset_Int]) 1);
4.54 qed "Ord_Int";
4.55
4.56 -val nonempty::prems = goal Ordinal.thy
4.57 +val nonempty::prems = Goal
4.58 "[| j:A; !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))";
4.59 by (rtac (nonempty RS Transset_Inter_family RS OrdI) 1);
4.60 by (rtac Ord_is_Transset 1);
4.61 @@ -167,7 +166,7 @@
4.62 ORELSE etac InterD 1));
4.63 qed "Ord_Inter";
4.64
4.65 -val jmemA::prems = goal Ordinal.thy
4.66 +val jmemA::prems = Goal
4.67 "[| j:A; !!x. x:A ==> Ord(B(x)) |] ==> Ord(INT x:A. B(x))";
4.68 by (rtac (jmemA RS RepFunI RS Ord_Inter) 1);
4.69 by (etac RepFunE 1);
4.70 @@ -194,7 +193,7 @@
4.71 by (REPEAT (ares_tac [conjI] 1));
4.72 qed "ltI";
4.73
4.74 -val major::prems = goalw Ordinal.thy [lt_def]
4.75 +val major::prems = Goalw [lt_def]
4.76 "[| i<j; [| i:j; Ord(i); Ord(j) |] ==> P |] ==> P";
4.77 by (rtac (major RS conjE) 1);
4.78 by (REPEAT (ares_tac (prems@[Ord_in_Ord]) 1));
4.79 @@ -258,12 +257,12 @@
4.80
4.81 val le_refl = refl RS le_eqI;
4.82
4.83 -val [prem] = goal Ordinal.thy "(~ (i=j & Ord(j)) ==> i<j) ==> i le j";
4.84 +val [prem] = Goal "(~ (i=j & Ord(j)) ==> i<j) ==> i le j";
4.85 by (rtac (disjCI RS (le_iff RS iffD2)) 1);
4.86 by (etac prem 1);
4.87 qed "leCI";
4.88
4.89 -val major::prems = goal Ordinal.thy
4.90 +val major::prems = Goal
4.91 "[| i le j; i<j ==> P; [| i=j; Ord(j) |] ==> P |] ==> P";
4.92 by (rtac (major RS (le_iff RS iffD1 RS disjE)) 1);
4.93 by (DEPTH_SOLVE (ares_tac prems 1 ORELSE etac conjE 1));
4.94 @@ -298,7 +297,7 @@
4.95 by (REPEAT (ares_tac [conjI, Memrel_iff RS iffD2] 1));
4.96 qed "MemrelI";
4.97
4.98 -val [major,minor] = goal Ordinal.thy
4.99 +val [major,minor] = Goal
4.100 "[| <a,b> : Memrel(A); \
4.101 \ [| a: A; b: A; a:b |] ==> P \
4.102 \ |] ==> P";
4.103 @@ -357,7 +356,7 @@
4.104 (*** Transfinite induction ***)
4.105
4.106 (*Epsilon induction over a transitive set*)
4.107 -val major::prems = goalw Ordinal.thy [Transset_def]
4.108 +val major::prems = Goalw [Transset_def]
4.109 "[| i: k; Transset(k); \
4.110 \ !!x.[| x: k; ALL y:x. P(y) |] ==> P(x) \
4.111 \ |] ==> P(i)";
4.112 @@ -373,7 +372,7 @@
4.113 val Ord_induct = Ord_is_Transset RSN (2, Transset_induct);
4.114
4.115 (*Induction over the class of ordinals -- a useful corollary of Ord_induct*)
4.116 -val [major,indhyp] = goal Ordinal.thy
4.117 +val [major,indhyp] = Goal
4.118 "[| Ord(i); \
4.119 \ !!x.[| Ord(x); ALL y:x. P(y) |] ==> P(x) \
4.120 \ |] ==> P(i)";
4.121 @@ -397,29 +396,28 @@
4.122
4.123 (** Proving that < is a linear ordering on the ordinals **)
4.124
4.125 -val prems = goal Ordinal.thy
4.126 - "Ord(i) ==> (ALL j. Ord(j) --> i:j | i=j | j:i)";
4.127 -by (trans_ind_tac "i" prems 1);
4.128 +Goal "Ord(i) ==> (ALL j. Ord(j) --> i:j | i=j | j:i)";
4.129 +by (etac trans_induct 1);
4.130 by (rtac (impI RS allI) 1);
4.131 by (trans_ind_tac "j" [] 1);
4.132 by (DEPTH_SOLVE (Step_tac 1 ORELSE Ord_trans_tac 1));
4.133 qed_spec_mp "Ord_linear";
4.134
4.135 (*The trichotomy law for ordinals!*)
4.136 -val ordi::ordj::prems = goalw Ordinal.thy [lt_def]
4.137 +val ordi::ordj::prems = Goalw [lt_def]
4.138 "[| Ord(i); Ord(j); i<j ==> P; i=j ==> P; j<i ==> P |] ==> P";
4.139 by (rtac ([ordi,ordj] MRS Ord_linear RS disjE) 1);
4.140 by (etac disjE 2);
4.141 by (DEPTH_SOLVE (ares_tac ([ordi,ordj,conjI] @ prems) 1));
4.142 qed "Ord_linear_lt";
4.143
4.144 -val prems = goal Ordinal.thy
4.145 +val prems = Goal
4.146 "[| Ord(i); Ord(j); i<j ==> P; j le i ==> P |] ==> P";
4.147 by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1);
4.148 by (DEPTH_SOLVE (ares_tac ([leI, sym RS le_eqI] @ prems) 1));
4.149 qed "Ord_linear2";
4.150
4.151 -val prems = goal Ordinal.thy
4.152 +val prems = Goal
4.153 "[| Ord(i); Ord(j); i le j ==> P; j le i ==> P |] ==> P";
4.154 by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1);
4.155 by (DEPTH_SOLVE (ares_tac ([leI,le_eqI] @ prems) 1));
4.156 @@ -489,7 +487,7 @@
4.157 qed "le_succ_iff";
4.158
4.159 (*Just a variant of subset_imp_le*)
4.160 -val [ordi,ordj,minor] = goal Ordinal.thy
4.161 +val [ordi,ordj,minor] = Goal
4.162 "[| Ord(i); Ord(j); !!x. x<j ==> x<i |] ==> j le i";
4.163 by (REPEAT_FIRST (ares_tac [notI RS not_lt_imp_le, ordi, ordj]));
4.164 by (etac (minor RS lt_irrefl) 1);
4.165 @@ -581,12 +579,12 @@
4.166
4.167 (*** Results about limits ***)
4.168
4.169 -val prems = goal Ordinal.thy "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))";
4.170 +val prems = Goal "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))";
4.171 by (rtac (Ord_is_Transset RS Transset_Union_family RS OrdI) 1);
4.172 by (REPEAT (etac UnionE 1 ORELSE ares_tac ([Ord_contains_Transset]@prems) 1));
4.173 qed "Ord_Union";
4.174
4.175 -val prems = goal Ordinal.thy
4.176 +val prems = Goal
4.177 "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(UN x:A. B(x))";
4.178 by (rtac Ord_Union 1);
4.179 by (etac RepFunE 1);
4.180 @@ -595,27 +593,27 @@
4.181 qed "Ord_UN";
4.182
4.183 (* No < version; consider (UN i:nat.i)=nat *)
4.184 -val [ordi,limit] = goal Ordinal.thy
4.185 +val [ordi,limit] = Goal
4.186 "[| Ord(i); !!x. x:A ==> b(x) le i |] ==> (UN x:A. b(x)) le i";
4.187 by (rtac (le_imp_subset RS UN_least RS subset_imp_le) 1);
4.188 by (REPEAT (ares_tac [ordi, Ord_UN, limit] 1 ORELSE etac (limit RS ltE) 1));
4.189 qed "UN_least_le";
4.190
4.191 -val [jlti,limit] = goal Ordinal.thy
4.192 +val [jlti,limit] = Goal
4.193 "[| j<i; !!x. x:A ==> b(x)<j |] ==> (UN x:A. succ(b(x))) < i";
4.194 by (rtac (jlti RS ltE) 1);
4.195 by (rtac (UN_least_le RS lt_trans2) 1);
4.196 by (REPEAT (ares_tac [jlti, succ_leI, limit] 1));
4.197 qed "UN_succ_least_lt";
4.198
4.199 -val prems = goal Ordinal.thy
4.200 +val prems = Goal
4.201 "[| a: A; i le b(a); !!x. x:A ==> Ord(b(x)) |] ==> i le (UN x:A. b(x))";
4.202 by (resolve_tac (prems RL [ltE]) 1);
4.203 by (rtac (le_imp_subset RS subset_trans RS subset_imp_le) 1);
4.204 by (REPEAT (ares_tac (prems @ [UN_upper, Ord_UN]) 1));
4.205 qed "UN_upper_le";
4.206
4.207 -val [leprem] = goal Ordinal.thy
4.208 +val [leprem] = Goal
4.209 "[| !!x. x:A ==> c(x) le d(x) |] ==> (UN x:A. c(x)) le (UN x:A. d(x))";
4.210 by (rtac UN_least_le 1);
4.211 by (rtac UN_upper_le 2);
4.212 @@ -679,7 +677,7 @@
4.213 addSDs [Ord_succD]) 1);
4.214 qed "Ord_cases_disj";
4.215
4.216 -val major::prems = goal Ordinal.thy
4.217 +val major::prems = Goal
4.218 "[| Ord(i); \
4.219 \ i=0 ==> P; \
4.220 \ !!j. [| Ord(j); i=succ(j) |] ==> P; \
4.221 @@ -689,7 +687,7 @@
4.222 by (REPEAT (eresolve_tac (prems@[asm_rl, disjE, exE, conjE]) 1));
4.223 qed "Ord_cases";
4.224
4.225 -val major::prems = goal Ordinal.thy
4.226 +val major::prems = Goal
4.227 "[| Ord(i); \
4.228 \ P(0); \
4.229 \ !!x. [| Ord(x); P(x) |] ==> P(succ(x)); \
5.1 --- a/src/ZF/Perm.ML Fri Aug 14 13:52:42 1998 +0200
5.2 +++ b/src/ZF/Perm.ML Fri Aug 14 18:37:28 1998 +0200
5.3 @@ -33,7 +33,7 @@
5.4 by (blast_tac (claset() addIs prems) 1);
5.5 qed "f_imp_surjective";
5.6
5.7 -val prems = goal Perm.thy
5.8 +val prems = Goal
5.9 "[| !!x. x:A ==> c(x): B; \
5.10 \ !!y. y:B ==> d(y): A; \
5.11 \ !!y. y:B ==> c(d(y)) = y \
5.12 @@ -74,7 +74,7 @@
5.13 by (deepen_tac (claset() addEs [subst_context RS box_equals]) 0 1);
5.14 bind_thm ("f_imp_injective", ballI RSN (2,result()));
5.15
5.16 -val prems = goal Perm.thy
5.17 +val prems = Goal
5.18 "[| !!x. x:A ==> c(x): B; \
5.19 \ !!x. x:A ==> d(c(x)) = x \
5.20 \ |] ==> (lam x:A. c(x)) : inj(A,B)";
5.21 @@ -185,10 +185,9 @@
5.22
5.23 val left_inverse_bij = bij_is_inj RS left_inverse;
5.24
5.25 -val prems = goal Perm.thy
5.26 - "[| f: A->B; converse(f): C->A; b: C |] ==> f`(converse(f)`b) = b";
5.27 +Goal "[| f: A->B; converse(f): C->A; b: C |] ==> f`(converse(f)`b) = b";
5.28 by (rtac (apply_Pair RS (converseD RS apply_equality)) 1);
5.29 -by (REPEAT (resolve_tac prems 1));
5.30 +by (REPEAT (assume_tac 1));
5.31 qed "right_inverse_lemma";
5.32
5.33 (*Should the premises be f:surj(A,B), b:B for symmetry with left_inverse?
5.34 @@ -337,7 +336,7 @@
5.35 Addsimps [comp_fun_apply];
5.36
5.37 (*Simplifies compositions of lambda-abstractions*)
5.38 -val [prem] = goal Perm.thy
5.39 +val [prem] = Goal
5.40 "[| !!x. x:A ==> b(x): B \
5.41 \ |] ==> (lam y:B. c(y)) O (lam x:A. b(x)) = (lam x:A. c(b(x)))";
5.42 by (rtac fun_extension 1);
5.43 @@ -513,11 +512,10 @@
5.44 box_equals, restrict] 1));
5.45 qed "restrict_inj";
5.46
5.47 -val prems = goal Perm.thy
5.48 - "[| f: Pi(A,B); C<=A |] ==> restrict(f,C): surj(C, f``C)";
5.49 +Goal "[| f: Pi(A,B); C<=A |] ==> restrict(f,C): surj(C, f``C)";
5.50 by (rtac (restrict_image RS subst) 1);
5.51 by (rtac (restrict_type2 RS surj_image) 3);
5.52 -by (REPEAT (resolve_tac prems 1));
5.53 +by (REPEAT (assume_tac 1));
5.54 qed "restrict_surj";
5.55
5.56 Goalw [inj_def,bij_def]
6.1 --- a/src/ZF/QUniv.ML Fri Aug 14 13:52:42 1998 +0200
6.2 +++ b/src/ZF/QUniv.ML Fri Aug 14 18:37:28 1998 +0200
6.3 @@ -160,42 +160,6 @@
6.4 bind_thm ("bool_into_quniv", bool_subset_quniv RS subsetD);
6.5
6.6
6.7 -(**** Properties of Vfrom analogous to the "take-lemma" ****)
6.8 -
6.9 -(*** Intersecting a*b with Vfrom... ***)
6.10 -
6.11 -(*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*)
6.12 -goal Univ.thy
6.13 - "!!X. [| {a,b} : Vfrom(X,succ(i)); Transset(X) |] ==> \
6.14 -\ a: Vfrom(X,i) & b: Vfrom(X,i)";
6.15 -by (dtac (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1);
6.16 -by (assume_tac 1);
6.17 -by (Fast_tac 1);
6.18 -qed "doubleton_in_Vfrom_D";
6.19 -
6.20 -(*This weaker version says a, b exist at the same level*)
6.21 -bind_thm ("Vfrom_doubleton_D", Transset_Vfrom RS Transset_doubleton_D);
6.22 -
6.23 -(** Using only the weaker theorem would prove <a,b> : Vfrom(X,i)
6.24 - implies a, b : Vfrom(X,i), which is useless for induction.
6.25 - Using only the stronger theorem would prove <a,b> : Vfrom(X,succ(succ(i)))
6.26 - implies a, b : Vfrom(X,i), leaving the succ(i) case untreated.
6.27 - The combination gives a reduction by precisely one level, which is
6.28 - most convenient for proofs.
6.29 -**)
6.30 -
6.31 -goalw Univ.thy [Pair_def]
6.32 - "!!X. [| <a,b> : Vfrom(X,succ(i)); Transset(X) |] ==> \
6.33 -\ a: Vfrom(X,i) & b: Vfrom(X,i)";
6.34 -by (blast_tac (claset() addSDs [doubleton_in_Vfrom_D, Vfrom_doubleton_D]) 1);
6.35 -qed "Pair_in_Vfrom_D";
6.36 -
6.37 -goal Univ.thy
6.38 - "!!X. Transset(X) ==> \
6.39 -\ (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))";
6.40 -by (blast_tac (claset() addSDs [Pair_in_Vfrom_D]) 1);
6.41 -qed "product_Int_Vfrom_subset";
6.42 -
6.43 (*** Intersecting <a;b> with Vfrom... ***)
6.44
6.45 Goalw [QPair_def,sum_def]
7.1 --- a/src/ZF/Rel.ML Fri Aug 14 13:52:42 1998 +0200
7.2 +++ b/src/ZF/Rel.ML Fri Aug 14 18:37:28 1998 +0200
7.3 @@ -12,19 +12,18 @@
7.4
7.5 (* irreflexivity *)
7.6
7.7 -val prems = goalw Rel.thy [irrefl_def]
7.8 +val prems = Goalw [irrefl_def]
7.9 "[| !!x. x:A ==> <x,x> ~: r |] ==> irrefl(A,r)";
7.10 by (REPEAT (ares_tac (prems @ [ballI]) 1));
7.11 qed "irreflI";
7.12
7.13 -val prems = goalw Rel.thy [irrefl_def]
7.14 - "[| irrefl(A,r); x:A |] ==> <x,x> ~: r";
7.15 -by (rtac (prems MRS bspec) 1);
7.16 +Goalw [irrefl_def] "[| irrefl(A,r); x:A |] ==> <x,x> ~: r";
7.17 +by (Blast_tac 1);
7.18 qed "irreflE";
7.19
7.20 (* symmetry *)
7.21
7.22 -val prems = goalw Rel.thy [sym_def]
7.23 +val prems = Goalw [sym_def]
7.24 "[| !!x y.<x,y>: r ==> <y,x>: r |] ==> sym(r)";
7.25 by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
7.26 qed "symI";
7.27 @@ -35,21 +34,19 @@
7.28
7.29 (* antisymmetry *)
7.30
7.31 -val prems = goalw Rel.thy [antisym_def]
7.32 +val prems = Goalw [antisym_def]
7.33 "[| !!x y.[| <x,y>: r; <y,x>: r |] ==> x=y |] ==> \
7.34 \ antisym(r)";
7.35 by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
7.36 qed "antisymI";
7.37
7.38 -val prems = goalw Rel.thy [antisym_def]
7.39 - "!!r. [| antisym(r); <x,y>: r; <y,x>: r |] ==> x=y";
7.40 +Goalw [antisym_def] "[| antisym(r); <x,y>: r; <y,x>: r |] ==> x=y";
7.41 by (Blast_tac 1);
7.42 qed "antisymE";
7.43
7.44 (* transitivity *)
7.45
7.46 -Goalw [trans_def]
7.47 - "[| trans(r); <a,b>:r; <b,c>:r |] ==> <a,c>:r";
7.48 +Goalw [trans_def] "[| trans(r); <a,b>:r; <b,c>:r |] ==> <a,c>:r";
7.49 by (Blast_tac 1);
7.50 qed "transD";
7.51
8.1 --- a/src/ZF/Sum.ML Fri Aug 14 13:52:42 1998 +0200
8.2 +++ b/src/ZF/Sum.ML Fri Aug 14 18:37:28 1998 +0200
8.3 @@ -22,7 +22,7 @@
8.4
8.5 val PartI = refl RSN (2,Part_eqI);
8.6
8.7 -val major::prems = goalw Sum.thy [Part_def]
8.8 +val major::prems = Goalw [Part_def]
8.9 "[| a : Part(A,h); !!z. [| a : A; a=h(z) |] ==> P \
8.10 \ |] ==> P";
8.11 by (rtac (major RS CollectE) 1);
8.12 @@ -58,7 +58,7 @@
8.13
8.14 (** Elimination rules **)
8.15
8.16 -val major::prems = goalw Sum.thy sum_defs
8.17 +val major::prems = Goalw sum_defs
8.18 "[| u: A+B; \
8.19 \ !!x. [| x:A; u=Inl(x) |] ==> P; \
8.20 \ !!y. [| y:B; u=Inr(y) |] ==> P \
8.21 @@ -141,7 +141,7 @@
8.22
8.23 Addsimps [case_Inl, case_Inr];
8.24
8.25 -val major::prems = goal Sum.thy
8.26 +val major::prems = Goal
8.27 "[| u: A+B; \
8.28 \ !!x. x: A ==> c(x): C(Inl(x)); \
8.29 \ !!y. y: B ==> d(y): C(Inr(y)) \
8.30 @@ -158,7 +158,7 @@
8.31 by Auto_tac;
8.32 qed "expand_case";
8.33
8.34 -val major::prems = goal Sum.thy
8.35 +val major::prems = Goal
8.36 "[| z: A+B; \
8.37 \ !!x. x:A ==> c(x)=c'(x); \
8.38 \ !!y. y:B ==> d(y)=d'(y) \
9.1 --- a/src/ZF/Trancl.ML Fri Aug 14 13:52:42 1998 +0200
9.2 +++ b/src/ZF/Trancl.ML Fri Aug 14 18:37:28 1998 +0200
9.3 @@ -14,9 +14,9 @@
9.4 by (Blast_tac 1);
9.5 qed "rtrancl_bnd_mono";
9.6
9.7 -val [prem] = goalw Trancl.thy [rtrancl_def] "r<=s ==> r^* <= s^*";
9.8 +Goalw [rtrancl_def] "r<=s ==> r^* <= s^*";
9.9 by (rtac lfp_mono 1);
9.10 -by (REPEAT (resolve_tac [rtrancl_bnd_mono, prem, subset_refl, id_mono,
9.11 +by (REPEAT (ares_tac [rtrancl_bnd_mono, subset_refl, id_mono,
9.12 comp_mono, Un_mono, field_mono, Sigma_mono] 1));
9.13 qed "rtrancl_mono";
9.14
9.15 @@ -28,29 +28,27 @@
9.16 bind_thm ("rtrancl_type", (rtrancl_def RS def_lfp_subset));
9.17
9.18 (*Reflexivity of rtrancl*)
9.19 -val [prem] = goal Trancl.thy "[| a: field(r) |] ==> <a,a> : r^*";
9.20 +Goal "[| a: field(r) |] ==> <a,a> : r^*";
9.21 by (resolve_tac [rtrancl_unfold RS ssubst] 1);
9.22 -by (rtac (prem RS idI RS UnI1) 1);
9.23 +by (etac (idI RS UnI1) 1);
9.24 qed "rtrancl_refl";
9.25
9.26 (*Closure under composition with r *)
9.27 -val prems = goal Trancl.thy
9.28 - "[| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^*";
9.29 +Goal "[| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^*";
9.30 by (resolve_tac [rtrancl_unfold RS ssubst] 1);
9.31 by (rtac (compI RS UnI2) 1);
9.32 -by (resolve_tac prems 1);
9.33 -by (resolve_tac prems 1);
9.34 +by (assume_tac 1);
9.35 +by (assume_tac 1);
9.36 qed "rtrancl_into_rtrancl";
9.37
9.38 (*rtrancl of r contains all pairs in r *)
9.39 -val prems = goal Trancl.thy "<a,b> : r ==> <a,b> : r^*";
9.40 +Goal "<a,b> : r ==> <a,b> : r^*";
9.41 by (resolve_tac [rtrancl_refl RS rtrancl_into_rtrancl] 1);
9.42 -by (REPEAT (resolve_tac (prems@[fieldI1]) 1));
9.43 +by (REPEAT (ares_tac [fieldI1] 1));
9.44 qed "r_into_rtrancl";
9.45
9.46 (*The premise ensures that r consists entirely of pairs*)
9.47 -val prems = goal Trancl.thy "r <= Sigma(A,B) ==> r <= r^*";
9.48 -by (cut_facts_tac prems 1);
9.49 +Goal "r <= Sigma(A,B) ==> r <= r^*";
9.50 by (blast_tac (claset() addIs [r_into_rtrancl]) 1);
9.51 qed "r_subset_rtrancl";
9.52
9.53 @@ -62,7 +60,7 @@
9.54
9.55 (** standard induction rule **)
9.56
9.57 -val major::prems = goal Trancl.thy
9.58 +val major::prems = Goal
9.59 "[| <a,b> : r^*; \
9.60 \ !!x. x: field(r) ==> P(<x,x>); \
9.61 \ !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |] ==> P(<x,z>) |] \
9.62 @@ -74,7 +72,7 @@
9.63 (*nice induction rule.
9.64 Tried adding the typing hypotheses y,z:field(r), but these
9.65 caused expensive case splits!*)
9.66 -val major::prems = goal Trancl.thy
9.67 +val major::prems = Goal
9.68 "[| <a,b> : r^*; \
9.69 \ P(a); \
9.70 \ !!y z.[| <a,y> : r^*; <y,z> : r; P(y) |] ==> P(z) \
9.71 @@ -96,7 +94,7 @@
9.72 qed "trans_rtrancl";
9.73
9.74 (*elimination of rtrancl -- by induction on a special formula*)
9.75 -val major::prems = goal Trancl.thy
9.76 +val major::prems = Goal
9.77 "[| <a,b> : r^*; (a=b) ==> P; \
9.78 \ !!y.[| <a,y> : r^*; <y,b> : r |] ==> P |] \
9.79 \ ==> P";
9.80 @@ -147,7 +145,7 @@
9.81 qed "rtrancl_into_trancl2";
9.82
9.83 (*Nice induction rule for trancl*)
9.84 -val major::prems = goal Trancl.thy
9.85 +val major::prems = Goal
9.86 "[| <a,b> : r^+; \
9.87 \ !!y. [| <a,y> : r |] ==> P(y); \
9.88 \ !!y z.[| <a,y> : r^+; <y,z> : r; P(y) |] ==> P(z) \
9.89 @@ -162,7 +160,7 @@
9.90 qed "trancl_induct";
9.91
9.92 (*elimination of r^+ -- NOT an induction rule*)
9.93 -val major::prems = goal Trancl.thy
9.94 +val major::prems = Goal
9.95 "[| <a,b> : r^+; \
9.96 \ <a,b> : r ==> P; \
9.97 \ !!y.[| <a,y> : r^+; <y,b> : r |] ==> P \
9.98 @@ -178,7 +176,7 @@
9.99 by (blast_tac (claset() addEs [rtrancl_type RS subsetD RS SigmaE2]) 1);
9.100 qed "trancl_type";
9.101
9.102 -val [prem] = goalw Trancl.thy [trancl_def] "r<=s ==> r^+ <= s^+";
9.103 -by (REPEAT (resolve_tac [prem, comp_mono, rtrancl_mono] 1));
9.104 +Goalw [trancl_def] "r<=s ==> r^+ <= s^+";
9.105 +by (REPEAT (ares_tac [comp_mono, rtrancl_mono] 1));
9.106 qed "trancl_mono";
9.107
10.1 --- a/src/ZF/Univ.ML Fri Aug 14 13:52:42 1998 +0200
10.2 +++ b/src/ZF/Univ.ML Fri Aug 14 18:37:28 1998 +0200
10.3 @@ -107,11 +107,10 @@
10.4 by (REPEAT (ares_tac [doubleton_in_Vfrom] 1));
10.5 qed "Pair_in_Vfrom";
10.6
10.7 -val [prem] = goal Univ.thy
10.8 - "a<=Vfrom(A,i) ==> succ(a) : Vfrom(A,succ(succ(i)))";
10.9 +Goal "a<=Vfrom(A,i) ==> succ(a) : Vfrom(A,succ(succ(i)))";
10.10 by (REPEAT (resolve_tac [subset_mem_Vfrom, succ_subsetI] 1));
10.11 by (rtac (Vfrom_mono RSN (2,subset_trans)) 2);
10.12 -by (REPEAT (resolve_tac [prem, subset_refl, subset_succI] 1));
10.13 +by (REPEAT (ares_tac [subset_refl, subset_succI] 1));
10.14 qed "succ_in_Vfrom";
10.15
10.16 (*** 0, successor and limit equations fof Vfrom ***)
10.17 @@ -140,12 +139,32 @@
10.18
10.19 (*The premise distinguishes this from Vfrom(A,0); allowing X=0 forces
10.20 the conclusion to be Vfrom(A,Union(X)) = A Un (UN y:X. Vfrom(A,y)) *)
10.21 +Goal "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))";
10.22 +by (stac Vfrom 1);
10.23 +by (rtac equalityI 1);
10.24 +(*first inclusion*)
10.25 +by (rtac Un_least 1);
10.26 +by (rtac (A_subset_Vfrom RS subset_trans) 1);
10.27 +by (rtac UN_upper 1);
10.28 +by (assume_tac 1);
10.29 +by (rtac UN_least 1);
10.30 +by (etac UnionE 1);
10.31 +by (rtac subset_trans 1);
10.32 +by (etac UN_upper 2 THEN stac Vfrom 1 THEN
10.33 + etac ([UN_upper, Un_upper2] MRS subset_trans) 1);
10.34 +(*opposite inclusion*)
10.35 +by (rtac UN_least 1);
10.36 +by (stac Vfrom 1);
10.37 +by (Blast_tac 1);
10.38 +qed "Vfrom_Union";
10.39 +
10.40 val [prem] = goal Univ.thy "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))";
10.41 by (stac Vfrom 1);
10.42 by (rtac equalityI 1);
10.43 (*first inclusion*)
10.44 by (rtac Un_least 1);
10.45 by (rtac (A_subset_Vfrom RS subset_trans) 1);
10.46 +
10.47 by (rtac (prem RS UN_upper) 1);
10.48 by (rtac UN_least 1);
10.49 by (etac UnionE 1);
10.50 @@ -175,7 +194,7 @@
10.51 by (REPEAT (ares_tac [ltD RS UN_I] 1));
10.52 qed "Limit_VfromI";
10.53
10.54 -val prems = goal Univ.thy
10.55 +val prems = Goal
10.56 "[| a: Vfrom(A,i); Limit(i); \
10.57 \ !!x. [| x<i; a: Vfrom(A,x) |] ==> R \
10.58 \ |] ==> R";
10.59 @@ -278,8 +297,7 @@
10.60 by (etac (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1);
10.61 qed "Transset_Vfrom_succ";
10.62
10.63 -goalw Ordinal.thy [Pair_def,Transset_def]
10.64 - "!!C. [| <a,b> <= C; Transset(C) |] ==> a: C & b: C";
10.65 +Goalw [Pair_def,Transset_def] "[| <a,b> <= C; Transset(C) |] ==> a: C & b: C";
10.66 by (Blast_tac 1);
10.67 qed "Transset_Pair_subset";
10.68
10.69 @@ -297,7 +315,7 @@
10.70 ***)
10.71
10.72 (*General theorem for membership in Vfrom(A,i) when i is a limit ordinal*)
10.73 -val [aprem,bprem,limiti,step] = goal Univ.thy
10.74 +val [aprem,bprem,limiti,step] = Goal
10.75 "[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); \
10.76 \ !!x y j. [| j<i; 1:j; x: Vfrom(A,j); y: Vfrom(A,j) \
10.77 \ |] ==> EX k. h(x,y): Vfrom(A,k) & k<i |] ==> \
10.78 @@ -377,8 +395,7 @@
10.79 qed "fun_in_VLimit";
10.80
10.81 Goalw [Pi_def]
10.82 - "[| a: Vfrom(A,j); Transset(A) |] ==> \
10.83 -\ Pow(a) : Vfrom(A, succ(succ(j)))";
10.84 + "[| a: Vfrom(A,j); Transset(A) |] ==> Pow(a) : Vfrom(A, succ(succ(j)))";
10.85 by (dtac Transset_Vfrom 1);
10.86 by (rtac subset_mem_Vfrom 1);
10.87 by (rewtac Transset_def);
10.88 @@ -406,8 +423,8 @@
10.89
10.90 (** Characterisation of the elements of Vset(i) **)
10.91
10.92 -val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) < i";
10.93 -by (rtac (ordi RS trans_induct) 1);
10.94 +Goal "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) < i";
10.95 +by (etac trans_induct 1);
10.96 by (stac Vset 1);
10.97 by Safe_tac;
10.98 by (stac rank 1);
10.99 @@ -416,8 +433,8 @@
10.100 by (REPEAT (ares_tac [ltI] 1));
10.101 qed_spec_mp "VsetD";
10.102
10.103 -val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)";
10.104 -by (rtac (ordi RS trans_induct) 1);
10.105 +Goal "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)";
10.106 +by (etac trans_induct 1);
10.107 by (rtac allI 1);
10.108 by (stac Vset 1);
10.109 by (blast_tac (claset() addSIs [rank_lt RS ltD]) 1);
10.110 @@ -458,7 +475,7 @@
10.111 by (etac (rank_lt RS VsetI) 1);
10.112 qed "arg_subset_Vset_rank";
10.113
10.114 -val [iprem] = goal Univ.thy
10.115 +val [iprem] = Goal
10.116 "[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b";
10.117 by (rtac ([subset_refl, arg_subset_Vset_rank] MRS
10.118 Int_greatest RS subset_trans) 1);
10.119 @@ -490,7 +507,7 @@
10.120 qed "Vrec";
10.121
10.122 (*This form avoids giant explosions in proofs. NOTE USE OF == *)
10.123 -val rew::prems = goal Univ.thy
10.124 +val rew::prems = Goal
10.125 "[| !!x. h(x)==Vrec(x,H) |] ==> \
10.126 \ h(a) = H(a, lam x: Vset(rank(a)). h(x))";
10.127 by (rewtac rew);
10.128 @@ -520,7 +537,7 @@
10.129 by (etac (univ_eq_UN RS subst) 1);
10.130 qed "subset_univ_eq_Int";
10.131
10.132 -val [aprem, iprem] = goal Univ.thy
10.133 +val [aprem, iprem] = Goal
10.134 "[| a <= univ(X); \
10.135 \ !!i. i:nat ==> a Int Vfrom(X,i) <= b \
10.136 \ |] ==> a <= b";
10.137 @@ -529,7 +546,7 @@
10.138 by (etac iprem 1);
10.139 qed "univ_Int_Vfrom_subset";
10.140
10.141 -val prems = goal Univ.thy
10.142 +val prems = Goal
10.143 "[| a <= univ(X); b <= univ(X); \
10.144 \ !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i) \
10.145 \ |] ==> a = b";
10.146 @@ -696,3 +713,37 @@
10.147 val FiniteFun_in_univ' = subsetI RSN (2, FiniteFun_in_univ);
10.148
10.149
10.150 +(**** For QUniv. Properties of Vfrom analogous to the "take-lemma" ****)
10.151 +
10.152 +(*** Intersecting a*b with Vfrom... ***)
10.153 +
10.154 +(*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*)
10.155 +Goal "[| {a,b} : Vfrom(X,succ(i)); Transset(X) |] \
10.156 +\ ==> a: Vfrom(X,i) & b: Vfrom(X,i)";
10.157 +by (dtac (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1);
10.158 +by (assume_tac 1);
10.159 +by (Fast_tac 1);
10.160 +qed "doubleton_in_Vfrom_D";
10.161 +
10.162 +(*This weaker version says a, b exist at the same level*)
10.163 +bind_thm ("Vfrom_doubleton_D", Transset_Vfrom RS Transset_doubleton_D);
10.164 +
10.165 +(** Using only the weaker theorem would prove <a,b> : Vfrom(X,i)
10.166 + implies a, b : Vfrom(X,i), which is useless for induction.
10.167 + Using only the stronger theorem would prove <a,b> : Vfrom(X,succ(succ(i)))
10.168 + implies a, b : Vfrom(X,i), leaving the succ(i) case untreated.
10.169 + The combination gives a reduction by precisely one level, which is
10.170 + most convenient for proofs.
10.171 +**)
10.172 +
10.173 +Goalw [Pair_def]
10.174 + "[| <a,b> : Vfrom(X,succ(i)); Transset(X) |] \
10.175 +\ ==> a: Vfrom(X,i) & b: Vfrom(X,i)";
10.176 +by (blast_tac (claset() addSDs [doubleton_in_Vfrom_D, Vfrom_doubleton_D]) 1);
10.177 +qed "Pair_in_Vfrom_D";
10.178 +
10.179 +Goal "Transset(X) ==> \
10.180 +\ (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))";
10.181 +by (blast_tac (claset() addSDs [Pair_in_Vfrom_D]) 1);
10.182 +qed "product_Int_Vfrom_subset";
10.183 +
11.1 --- a/src/ZF/WF.ML Fri Aug 14 13:52:42 1998 +0200
11.2 +++ b/src/ZF/WF.ML Fri Aug 14 18:37:28 1998 +0200
11.3 @@ -48,7 +48,7 @@
11.4 (** Introduction rules for wf_on **)
11.5
11.6 (*If every non-empty subset of A has an r-minimal element then wf[A](r).*)
11.7 -val [prem] = goalw WF.thy [wf_on_def, wf_def]
11.8 +val [prem] = Goalw [wf_on_def, wf_def]
11.9 "[| !!Z u. [| Z<=A; u:Z; ALL x:Z. EX y:Z. <y,x>:r |] ==> False |] \
11.10 \ ==> wf[A](r)";
11.11 by (rtac (equals0I RS disjCI RS allI) 1);
11.12 @@ -59,7 +59,7 @@
11.13 (*If r allows well-founded induction over A then wf[A](r)
11.14 Premise is equivalent to
11.15 !!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B *)
11.16 -val [prem] = goal WF.thy
11.17 +val [prem] = Goal
11.18 "[| !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B; y:A \
11.19 \ |] ==> y:B |] \
11.20 \ ==> wf[A](r)";
11.21 @@ -74,7 +74,7 @@
11.22 (** Well-founded Induction **)
11.23
11.24 (*Consider the least z in domain(r) Un {a} such that P(z) does not hold...*)
11.25 -val [major,minor] = goalw WF.thy [wf_def]
11.26 +val [major,minor] = Goalw [wf_def]
11.27 "[| wf(r); \
11.28 \ !!x.[| ALL y. <y,x>: r --> P(y) |] ==> P(x) \
11.29 \ |] ==> P(a)";
11.30 @@ -92,7 +92,7 @@
11.31 ares_tac prems i];
11.32
11.33 (*The form of this rule is designed to match wfI*)
11.34 -val wfr::amem::prems = goal WF.thy
11.35 +val wfr::amem::prems = Goal
11.36 "[| wf(r); a:A; field(r)<=A; \
11.37 \ !!x.[| x: A; ALL y. <y,x>: r --> P(y) |] ==> P(x) \
11.38 \ |] ==> P(a)";
11.39 @@ -103,11 +103,11 @@
11.40 by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
11.41 qed "wf_induct2";
11.42
11.43 -goal domrange.thy "!!r A. field(r Int A*A) <= A";
11.44 +Goal "!!r A. field(r Int A*A) <= A";
11.45 by (Blast_tac 1);
11.46 qed "field_Int_square";
11.47
11.48 -val wfr::amem::prems = goalw WF.thy [wf_on_def]
11.49 +val wfr::amem::prems = Goalw [wf_on_def]
11.50 "[| wf[A](r); a:A; \
11.51 \ !!x.[| x: A; ALL y:A. <y,x>: r --> P(y) |] ==> P(x) \
11.52 \ |] ==> P(a)";
11.53 @@ -122,7 +122,7 @@
11.54 REPEAT (ares_tac prems i)];
11.55
11.56 (*If r allows well-founded induction then wf(r)*)
11.57 -val [subs,indhyp] = goal WF.thy
11.58 +val [subs,indhyp] = Goal
11.59 "[| field(r)<=A; \
11.60 \ !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B; y:A \
11.61 \ |] ==> y:B |] \
11.62 @@ -197,9 +197,8 @@
11.63
11.64 (** is_recfun **)
11.65
11.66 -val [major] = goalw WF.thy [is_recfun_def]
11.67 - "is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)";
11.68 -by (stac major 1);
11.69 +Goalw [is_recfun_def] "is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)";
11.70 +by (etac ssubst 1);
11.71 by (rtac (lamI RS rangeI RS lam_type) 1);
11.72 by (assume_tac 1);
11.73 qed "is_recfun_type";
11.74 @@ -245,26 +244,22 @@
11.75
11.76 (*** Main Existence Lemma ***)
11.77
11.78 -val prems = goal WF.thy
11.79 - "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |] ==> f=g";
11.80 -by (cut_facts_tac prems 1);
11.81 +Goal "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |] ==> f=g";
11.82 by (rtac fun_extension 1);
11.83 by (REPEAT (ares_tac [is_recfun_equal] 1
11.84 ORELSE eresolve_tac [is_recfun_type,underD] 1));
11.85 qed "is_recfun_functional";
11.86
11.87 (*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *)
11.88 -val prems = goalw WF.thy [the_recfun_def]
11.89 +Goalw [the_recfun_def]
11.90 "[| is_recfun(r,a,H,f); wf(r); trans(r) |] \
11.91 \ ==> is_recfun(r, a, H, the_recfun(r,a,H))";
11.92 by (rtac (ex1I RS theI) 1);
11.93 -by (REPEAT (ares_tac (prems@[is_recfun_functional]) 1));
11.94 +by (REPEAT (ares_tac [is_recfun_functional] 1));
11.95 qed "is_the_recfun";
11.96
11.97 -val prems = goal WF.thy
11.98 - "[| wf(r); trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))";
11.99 -by (cut_facts_tac prems 1);
11.100 -by (wf_ind_tac "a" prems 1);
11.101 +Goal "[| wf(r); trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))";
11.102 +by (wf_ind_tac "a" [] 1);
11.103 by (res_inst_tac [("f", "lam y: r-``{a1}. wftrec(r,y,H)")] is_the_recfun 1);
11.104 by (REPEAT (assume_tac 2));
11.105 by (rewrite_goals_tac [is_recfun_def, wftrec_def]);
11.106 @@ -309,14 +304,14 @@
11.107 qed "wfrec";
11.108
11.109 (*This form avoids giant explosions in proofs. NOTE USE OF == *)
11.110 -val rew::prems = goal WF.thy
11.111 +val rew::prems = Goal
11.112 "[| !!x. h(x)==wfrec(r,x,H); wf(r) |] ==> \
11.113 \ h(a) = H(a, lam x: r-``{a}. h(x))";
11.114 by (rewtac rew);
11.115 by (REPEAT (resolve_tac (prems@[wfrec]) 1));
11.116 qed "def_wfrec";
11.117
11.118 -val prems = goal WF.thy
11.119 +val prems = Goal
11.120 "[| wf(r); a:A; field(r)<=A; \
11.121 \ !!x u. [| x: A; u: Pi(r-``{x}, B) |] ==> H(x,u) : B(x) \
11.122 \ |] ==> wfrec(r,a,H) : B(a)";
12.1 --- a/src/ZF/Zorn.ML Fri Aug 14 13:52:42 1998 +0200
12.2 +++ b/src/ZF/Zorn.ML Fri Aug 14 18:37:28 1998 +0200
12.3 @@ -13,11 +13,11 @@
12.4
12.5 (*** Section 1. Mathematical Preamble ***)
12.6
12.7 -goal ZF.thy "!!A B C. (ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)";
12.8 +Goal "!!A B C. (ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)";
12.9 by (Blast_tac 1);
12.10 qed "Union_lemma0";
12.11
12.12 -goal ZF.thy
12.13 +Goal
12.14 "!!A B C. [| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B";
12.15 by (Blast_tac 1);
12.16 qed "Inter_lemma0";
12.17 @@ -45,7 +45,7 @@
12.18
12.19 (** Structural induction on TFin(S,next) **)
12.20
12.21 -val major::prems = goal Zorn.thy
12.22 +val major::prems = Goal
12.23 "[| n: TFin(S,next); \
12.24 \ !!x. [| x : TFin(S,next); P(x); next: increasing(S) |] ==> P(next`x); \
12.25 \ !!Y. [| Y <= TFin(S,next); ALL y:Y. P(y) |] ==> P(Union(Y)) \
12.26 @@ -67,12 +67,10 @@
12.27 TFin_is_subset RSN (3, increasingD2 RSN (2,subset_trans)));
12.28
12.29 (*Lemma 1 of section 3.1*)
12.30 -val major::prems = goal Zorn.thy
12.31 - "[| n: TFin(S,next); m: TFin(S,next); \
12.32 -\ ALL x: TFin(S,next) . x<=m --> x=m | next`x<=m \
12.33 -\ |] ==> n<=m | next`m<=n";
12.34 -by (cut_facts_tac prems 1);
12.35 -by (rtac (major RS TFin_induct) 1);
12.36 +Goal "[| n: TFin(S,next); m: TFin(S,next); \
12.37 +\ ALL x: TFin(S,next) . x<=m --> x=m | next`x<=m \
12.38 +\ |] ==> n<=m | next`m<=n";
12.39 +by (etac TFin_induct 1);
12.40 by (etac Union_lemma0 2); (*or just Blast_tac*)
12.41 by (blast_tac (subset_cs addIs [increasing_trans]) 1);
12.42 qed "TFin_linear_lemma1";
12.43 @@ -123,10 +121,8 @@
12.44
12.45
12.46 (*Lemma 3 of section 3.3*)
12.47 -val major::prems = goal Zorn.thy
12.48 - "[| n: TFin(S,next); m: TFin(S,next); m = next`m |] ==> n<=m";
12.49 -by (cut_facts_tac prems 1);
12.50 -by (rtac (major RS TFin_induct) 1);
12.51 +Goal "[| n: TFin(S,next); m: TFin(S,next); m = next`m |] ==> n<=m";
12.52 +by (etac TFin_induct 1);
12.53 by (dtac TFin_subsetD 1);
12.54 by (REPEAT (assume_tac 1));
12.55 by (fast_tac (claset() addEs [ssubst]) 1);
12.56 @@ -276,11 +272,10 @@
12.57 (*** Section 6. Zermelo's Theorem: every set can be well-ordered ***)
12.58
12.59 (*Lemma 5*)
12.60 -val major::prems = goal Zorn.thy
12.61 +Goal
12.62 "[| n: TFin(S,next); Z <= TFin(S,next); z:Z; ~ Inter(Z) : Z \
12.63 \ |] ==> ALL m:Z. n<=m";
12.64 -by (cut_facts_tac prems 1);
12.65 -by (rtac (major RS TFin_induct) 1);
12.66 +by (etac TFin_induct 1);
12.67 by (Blast_tac 2); (*second induction step is easy*)
12.68 by (rtac ballI 1);
12.69 by (rtac (bspec RS TFin_subsetD RS disjE) 1);
12.70 @@ -324,13 +319,6 @@
12.71
12.72 (** Defining the "next" operation for Zermelo's Theorem **)
12.73
12.74 -goal AC.thy
12.75 - "!!S. [| ch : (PROD X:Pow(S) - {0}. X); X<=S; X~=S \
12.76 -\ |] ==> ch ` (S-X) : S-X";
12.77 -by (etac apply_type 1);
12.78 -by (blast_tac (claset() addSEs [equalityE]) 1);
12.79 -qed "choice_Diff";
12.80 -
12.81 (*This justifies Definition 6.1*)
12.82 Goal "ch: (PROD X: Pow(S)-{0}. X) ==> \
12.83 \ EX next: increasing(S). ALL X: Pow(S). \
13.1 --- a/src/ZF/equalities.ML Fri Aug 14 13:52:42 1998 +0200
13.2 +++ b/src/ZF/equalities.ML Fri Aug 14 18:37:28 1998 +0200
13.3 @@ -10,23 +10,23 @@
13.4 (** Finite Sets **)
13.5
13.6 (* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*)
13.7 -goal ZF.thy "{a} Un B = cons(a,B)";
13.8 +Goal "{a} Un B = cons(a,B)";
13.9 by (Blast_tac 1);
13.10 qed "cons_eq";
13.11
13.12 -goal ZF.thy "cons(a, cons(b, C)) = cons(b, cons(a, C))";
13.13 +Goal "cons(a, cons(b, C)) = cons(b, cons(a, C))";
13.14 by (Blast_tac 1);
13.15 qed "cons_commute";
13.16
13.17 -goal ZF.thy "!!B. a: B ==> cons(a,B) = B";
13.18 +Goal "a: B ==> cons(a,B) = B";
13.19 by (Blast_tac 1);
13.20 qed "cons_absorb";
13.21
13.22 -goal ZF.thy "!!B. a: B ==> cons(a, B-{a}) = B";
13.23 +Goal "a: B ==> cons(a, B-{a}) = B";
13.24 by (Blast_tac 1);
13.25 qed "cons_Diff";
13.26
13.27 -goal ZF.thy "!!C. [| a: C; ALL y:C. y=b |] ==> C = {b}";
13.28 +Goal "[| a: C; ALL y:C. y=b |] ==> C = {b}";
13.29 by (Blast_tac 1);
13.30 qed "equal_singleton_lemma";
13.31 val equal_singleton = ballI RSN (2,equal_singleton_lemma);
13.32 @@ -35,150 +35,150 @@
13.33 (** Binary Intersection **)
13.34
13.35 (*NOT an equality, but it seems to belong here...*)
13.36 -goal ZF.thy "cons(a,B) Int C <= cons(a, B Int C)";
13.37 +Goal "cons(a,B) Int C <= cons(a, B Int C)";
13.38 by (Blast_tac 1);
13.39 qed "Int_cons";
13.40
13.41 -goal ZF.thy "A Int A = A";
13.42 +Goal "A Int A = A";
13.43 by (Blast_tac 1);
13.44 qed "Int_absorb";
13.45
13.46 -goal ZF.thy "A Int B = B Int A";
13.47 +Goal "A Int B = B Int A";
13.48 by (Blast_tac 1);
13.49 qed "Int_commute";
13.50
13.51 -goal ZF.thy "(A Int B) Int C = A Int (B Int C)";
13.52 +Goal "(A Int B) Int C = A Int (B Int C)";
13.53 by (Blast_tac 1);
13.54 qed "Int_assoc";
13.55
13.56 -goal ZF.thy "(A Un B) Int C = (A Int C) Un (B Int C)";
13.57 +Goal "(A Un B) Int C = (A Int C) Un (B Int C)";
13.58 by (Blast_tac 1);
13.59 qed "Int_Un_distrib";
13.60
13.61 -goal ZF.thy "A<=B <-> A Int B = A";
13.62 +Goal "A<=B <-> A Int B = A";
13.63 by (blast_tac (claset() addSEs [equalityE]) 1);
13.64 qed "subset_Int_iff";
13.65
13.66 -goal ZF.thy "A<=B <-> B Int A = A";
13.67 +Goal "A<=B <-> B Int A = A";
13.68 by (blast_tac (claset() addSEs [equalityE]) 1);
13.69 qed "subset_Int_iff2";
13.70
13.71 -goal ZF.thy "!!A B C. C<=A ==> (A-B) Int C = C-B";
13.72 +Goal "C<=A ==> (A-B) Int C = C-B";
13.73 by (Blast_tac 1);
13.74 qed "Int_Diff_eq";
13.75
13.76 (** Binary Union **)
13.77
13.78 -goal ZF.thy "cons(a,B) Un C = cons(a, B Un C)";
13.79 +Goal "cons(a,B) Un C = cons(a, B Un C)";
13.80 by (Blast_tac 1);
13.81 qed "Un_cons";
13.82
13.83 -goal ZF.thy "A Un A = A";
13.84 +Goal "A Un A = A";
13.85 by (Blast_tac 1);
13.86 qed "Un_absorb";
13.87
13.88 -goal ZF.thy "A Un B = B Un A";
13.89 +Goal "A Un B = B Un A";
13.90 by (Blast_tac 1);
13.91 qed "Un_commute";
13.92
13.93 -goal ZF.thy "(A Un B) Un C = A Un (B Un C)";
13.94 +Goal "(A Un B) Un C = A Un (B Un C)";
13.95 by (Blast_tac 1);
13.96 qed "Un_assoc";
13.97
13.98 -goal ZF.thy "(A Int B) Un C = (A Un C) Int (B Un C)";
13.99 +Goal "(A Int B) Un C = (A Un C) Int (B Un C)";
13.100 by (Blast_tac 1);
13.101 qed "Un_Int_distrib";
13.102
13.103 -goal ZF.thy "A<=B <-> A Un B = B";
13.104 +Goal "A<=B <-> A Un B = B";
13.105 by (blast_tac (claset() addSEs [equalityE]) 1);
13.106 qed "subset_Un_iff";
13.107
13.108 -goal ZF.thy "A<=B <-> B Un A = B";
13.109 +Goal "A<=B <-> B Un A = B";
13.110 by (blast_tac (claset() addSEs [equalityE]) 1);
13.111 qed "subset_Un_iff2";
13.112
13.113 (** Simple properties of Diff -- set difference **)
13.114
13.115 -goal ZF.thy "A-A = 0";
13.116 +Goal "A-A = 0";
13.117 by (Blast_tac 1);
13.118 qed "Diff_cancel";
13.119
13.120 -goal ZF.thy "0-A = 0";
13.121 +Goal "0-A = 0";
13.122 by (Blast_tac 1);
13.123 qed "empty_Diff";
13.124
13.125 -goal ZF.thy "A-0 = A";
13.126 +Goal "A-0 = A";
13.127 by (Blast_tac 1);
13.128 qed "Diff_0";
13.129
13.130 -goal ZF.thy "A-B=0 <-> A<=B";
13.131 +Goal "A-B=0 <-> A<=B";
13.132 by (blast_tac (claset() addEs [equalityE]) 1);
13.133 qed "Diff_eq_0_iff";
13.134
13.135 (*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
13.136 -goal ZF.thy "A - cons(a,B) = A - B - {a}";
13.137 +Goal "A - cons(a,B) = A - B - {a}";
13.138 by (Blast_tac 1);
13.139 qed "Diff_cons";
13.140
13.141 (*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
13.142 -goal ZF.thy "A - cons(a,B) = A - {a} - B";
13.143 +Goal "A - cons(a,B) = A - {a} - B";
13.144 by (Blast_tac 1);
13.145 qed "Diff_cons2";
13.146
13.147 -goal ZF.thy "A Int (B-A) = 0";
13.148 +Goal "A Int (B-A) = 0";
13.149 by (Blast_tac 1);
13.150 qed "Diff_disjoint";
13.151
13.152 -goal ZF.thy "!!A B. A<=B ==> A Un (B-A) = B";
13.153 +Goal "A<=B ==> A Un (B-A) = B";
13.154 by (Blast_tac 1);
13.155 qed "Diff_partition";
13.156
13.157 -goal ZF.thy "A <= B Un (A - B)";
13.158 +Goal "A <= B Un (A - B)";
13.159 by (Blast_tac 1);
13.160 qed "subset_Un_Diff";
13.161
13.162 -goal ZF.thy "!!A B. [| A<=B; B<=C |] ==> B-(C-A) = A";
13.163 +Goal "[| A<=B; B<=C |] ==> B-(C-A) = A";
13.164 by (Blast_tac 1);
13.165 qed "double_complement";
13.166
13.167 -goal ZF.thy "(A Un B) - (B-A) = A";
13.168 +Goal "(A Un B) - (B-A) = A";
13.169 by (Blast_tac 1);
13.170 qed "double_complement_Un";
13.171
13.172 -goal ZF.thy
13.173 +Goal
13.174 "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
13.175 by (Blast_tac 1);
13.176 qed "Un_Int_crazy";
13.177
13.178 -goal ZF.thy "A - (B Un C) = (A-B) Int (A-C)";
13.179 +Goal "A - (B Un C) = (A-B) Int (A-C)";
13.180 by (Blast_tac 1);
13.181 qed "Diff_Un";
13.182
13.183 -goal ZF.thy "A - (B Int C) = (A-B) Un (A-C)";
13.184 +Goal "A - (B Int C) = (A-B) Un (A-C)";
13.185 by (Blast_tac 1);
13.186 qed "Diff_Int";
13.187
13.188 (*Halmos, Naive Set Theory, page 16.*)
13.189 -goal ZF.thy "(A Int B) Un C = A Int (B Un C) <-> C<=A";
13.190 +Goal "(A Int B) Un C = A Int (B Un C) <-> C<=A";
13.191 by (blast_tac (claset() addSEs [equalityE]) 1);
13.192 qed "Un_Int_assoc_iff";
13.193
13.194
13.195 (** Big Union and Intersection **)
13.196
13.197 -goal ZF.thy "Union(cons(a,B)) = a Un Union(B)";
13.198 +Goal "Union(cons(a,B)) = a Un Union(B)";
13.199 by (Blast_tac 1);
13.200 qed "Union_cons";
13.201
13.202 -goal ZF.thy "Union(A Un B) = Union(A) Un Union(B)";
13.203 +Goal "Union(A Un B) = Union(A) Un Union(B)";
13.204 by (Blast_tac 1);
13.205 qed "Union_Un_distrib";
13.206
13.207 -goal ZF.thy "Union(A Int B) <= Union(A) Int Union(B)";
13.208 +Goal "Union(A Int B) <= Union(A) Int Union(B)";
13.209 by (Blast_tac 1);
13.210 qed "Union_Int_subset";
13.211
13.212 -goal ZF.thy "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)";
13.213 +Goal "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)";
13.214 by (blast_tac (claset() addSEs [equalityE]) 1);
13.215 qed "Union_disjoint";
13.216
13.217 @@ -186,26 +186,26 @@
13.218 by (Blast_tac 1);
13.219 qed "Inter_0";
13.220
13.221 -goal ZF.thy "!!A B. [| z:A; z:B |] ==> Inter(A) Un Inter(B) <= Inter(A Int B)";
13.222 +Goal "[| z:A; z:B |] ==> Inter(A) Un Inter(B) <= Inter(A Int B)";
13.223 by (Blast_tac 1);
13.224 qed "Inter_Un_subset";
13.225
13.226 (* A good challenge: Inter is ill-behaved on the empty set *)
13.227 -goal ZF.thy "!!A B. [| a:A; b:B |] ==> Inter(A Un B) = Inter(A) Int Inter(B)";
13.228 +Goal "[| a:A; b:B |] ==> Inter(A Un B) = Inter(A) Int Inter(B)";
13.229 by (Blast_tac 1);
13.230 qed "Inter_Un_distrib";
13.231
13.232 -goal ZF.thy "Union({b}) = b";
13.233 +Goal "Union({b}) = b";
13.234 by (Blast_tac 1);
13.235 qed "Union_singleton";
13.236
13.237 -goal ZF.thy "Inter({b}) = b";
13.238 +Goal "Inter({b}) = b";
13.239 by (Blast_tac 1);
13.240 qed "Inter_singleton";
13.241
13.242 (** Unions and Intersections of Families **)
13.243
13.244 -goal ZF.thy "Union(A) = (UN x:A. x)";
13.245 +Goal "Union(A) = (UN x:A. x)";
13.246 by (Blast_tac 1);
13.247 qed "Union_eq_UN";
13.248
13.249 @@ -213,43 +213,41 @@
13.250 by (Blast_tac 1);
13.251 qed "Inter_eq_INT";
13.252
13.253 -goal ZF.thy "(UN i:0. A(i)) = 0";
13.254 +Goal "(UN i:0. A(i)) = 0";
13.255 by (Blast_tac 1);
13.256 qed "UN_0";
13.257
13.258 (*Halmos, Naive Set Theory, page 35.*)
13.259 -goal ZF.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
13.260 +Goal "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
13.261 by (Blast_tac 1);
13.262 qed "Int_UN_distrib";
13.263
13.264 -goal ZF.thy "!!A B. i:I ==> B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
13.265 +Goal "i:I ==> B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
13.266 by (Blast_tac 1);
13.267 qed "Un_INT_distrib";
13.268
13.269 -goal ZF.thy
13.270 - "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
13.271 +Goal "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
13.272 by (Blast_tac 1);
13.273 qed "Int_UN_distrib2";
13.274
13.275 -goal ZF.thy
13.276 - "!!I J. [| i:I; j:J |] ==> \
13.277 -\ (INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
13.278 +Goal "[| i:I; j:J |] ==> \
13.279 +\ (INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
13.280 by (Blast_tac 1);
13.281 qed "Un_INT_distrib2";
13.282
13.283 -goal ZF.thy "!!A. a: A ==> (UN y:A. c) = c";
13.284 +Goal "a: A ==> (UN y:A. c) = c";
13.285 by (Blast_tac 1);
13.286 qed "UN_constant";
13.287
13.288 -goal ZF.thy "!!A. a: A ==> (INT y:A. c) = c";
13.289 +Goal "a: A ==> (INT y:A. c) = c";
13.290 by (Blast_tac 1);
13.291 qed "INT_constant";
13.292
13.293 -goal ZF.thy "(UN y: RepFun(A,f). B(y)) = (UN x:A. B(f(x)))";
13.294 +Goal "(UN y: RepFun(A,f). B(y)) = (UN x:A. B(f(x)))";
13.295 by (Blast_tac 1);
13.296 qed "UN_RepFun";
13.297
13.298 -goal ZF.thy "!!x. x:A ==> (INT y: RepFun(A,f). B(y)) = (INT x:A. B(f(x)))";
13.299 +Goal "x:A ==> (INT y: RepFun(A,f). B(y)) = (INT x:A. B(f(x)))";
13.300 by (Blast_tac 1);
13.301 qed "INT_RepFun";
13.302
13.303 @@ -259,94 +257,92 @@
13.304 (** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:
13.305 Union of a family of unions **)
13.306
13.307 -goal ZF.thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i)) Un (UN i:I. B(i))";
13.308 +Goal "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i)) Un (UN i:I. B(i))";
13.309 by (Blast_tac 1);
13.310 qed "UN_Un_distrib";
13.311
13.312 -goal ZF.thy
13.313 - "!!A B. i:I ==> \
13.314 -\ (INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
13.315 +Goal "i:I ==> (INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
13.316 by (Blast_tac 1);
13.317 qed "INT_Int_distrib";
13.318
13.319 -goal ZF.thy "(UN z:I Int J. A(z)) <= (UN z:I. A(z)) Int (UN z:J. A(z))";
13.320 +Goal "(UN z:I Int J. A(z)) <= (UN z:I. A(z)) Int (UN z:J. A(z))";
13.321 by (Blast_tac 1);
13.322 qed "UN_Int_subset";
13.323
13.324 (** Devlin, page 12, exercise 5: Complements **)
13.325
13.326 -goal ZF.thy "!!A B. i:I ==> B - (UN i:I. A(i)) = (INT i:I. B - A(i))";
13.327 +Goal "i:I ==> B - (UN i:I. A(i)) = (INT i:I. B - A(i))";
13.328 by (Blast_tac 1);
13.329 qed "Diff_UN";
13.330
13.331 -goal ZF.thy "!!A B. i:I ==> B - (INT i:I. A(i)) = (UN i:I. B - A(i))";
13.332 +Goal "i:I ==> B - (INT i:I. A(i)) = (UN i:I. B - A(i))";
13.333 by (Blast_tac 1);
13.334 qed "Diff_INT";
13.335
13.336 (** Unions and Intersections with General Sum **)
13.337
13.338 (*Not suitable for rewriting: LOOPS!*)
13.339 -goal ZF.thy "Sigma(cons(a,B), C) = ({a}*C(a)) Un Sigma(B,C)";
13.340 +Goal "Sigma(cons(a,B), C) = ({a}*C(a)) Un Sigma(B,C)";
13.341 by (Blast_tac 1);
13.342 qed "Sigma_cons1";
13.343
13.344 (*Not suitable for rewriting: LOOPS!*)
13.345 -goal ZF.thy "A * cons(b,B) = A*{b} Un A*B";
13.346 +Goal "A * cons(b,B) = A*{b} Un A*B";
13.347 by (Blast_tac 1);
13.348 qed "Sigma_cons2";
13.349
13.350 -goal ZF.thy "Sigma(succ(A), B) = ({A}*B(A)) Un Sigma(A,B)";
13.351 +Goal "Sigma(succ(A), B) = ({A}*B(A)) Un Sigma(A,B)";
13.352 by (Blast_tac 1);
13.353 qed "Sigma_succ1";
13.354
13.355 -goal ZF.thy "A * succ(B) = A*{B} Un A*B";
13.356 +Goal "A * succ(B) = A*{B} Un A*B";
13.357 by (Blast_tac 1);
13.358 qed "Sigma_succ2";
13.359
13.360 -goal ZF.thy "(SUM x:(UN y:A. C(y)). B(x)) = (UN y:A. SUM x:C(y). B(x))";
13.361 +Goal "(SUM x:(UN y:A. C(y)). B(x)) = (UN y:A. SUM x:C(y). B(x))";
13.362 by (Blast_tac 1);
13.363 qed "SUM_UN_distrib1";
13.364
13.365 -goal ZF.thy "(SUM i:I. UN j:J. C(i,j)) = (UN j:J. SUM i:I. C(i,j))";
13.366 +Goal "(SUM i:I. UN j:J. C(i,j)) = (UN j:J. SUM i:I. C(i,j))";
13.367 by (Blast_tac 1);
13.368 qed "SUM_UN_distrib2";
13.369
13.370 -goal ZF.thy "(SUM i:I Un J. C(i)) = (SUM i:I. C(i)) Un (SUM j:J. C(j))";
13.371 +Goal "(SUM i:I Un J. C(i)) = (SUM i:I. C(i)) Un (SUM j:J. C(j))";
13.372 by (Blast_tac 1);
13.373 qed "SUM_Un_distrib1";
13.374
13.375 -goal ZF.thy "(SUM i:I. A(i) Un B(i)) = (SUM i:I. A(i)) Un (SUM i:I. B(i))";
13.376 +Goal "(SUM i:I. A(i) Un B(i)) = (SUM i:I. A(i)) Un (SUM i:I. B(i))";
13.377 by (Blast_tac 1);
13.378 qed "SUM_Un_distrib2";
13.379
13.380 (*First-order version of the above, for rewriting*)
13.381 -goal ZF.thy "I * (A Un B) = I*A Un I*B";
13.382 +Goal "I * (A Un B) = I*A Un I*B";
13.383 by (rtac SUM_Un_distrib2 1);
13.384 qed "prod_Un_distrib2";
13.385
13.386 -goal ZF.thy "(SUM i:I Int J. C(i)) = (SUM i:I. C(i)) Int (SUM j:J. C(j))";
13.387 +Goal "(SUM i:I Int J. C(i)) = (SUM i:I. C(i)) Int (SUM j:J. C(j))";
13.388 by (Blast_tac 1);
13.389 qed "SUM_Int_distrib1";
13.390
13.391 -goal ZF.thy
13.392 - "(SUM i:I. A(i) Int B(i)) = (SUM i:I. A(i)) Int (SUM i:I. B(i))";
13.393 +Goal "(SUM i:I. A(i) Int B(i)) = (SUM i:I. A(i)) Int (SUM i:I. B(i))";
13.394 by (Blast_tac 1);
13.395 qed "SUM_Int_distrib2";
13.396
13.397 (*First-order version of the above, for rewriting*)
13.398 -goal ZF.thy "I * (A Int B) = I*A Int I*B";
13.399 +Goal "I * (A Int B) = I*A Int I*B";
13.400 by (rtac SUM_Int_distrib2 1);
13.401 qed "prod_Int_distrib2";
13.402
13.403 (*Cf Aczel, Non-Well-Founded Sets, page 115*)
13.404 -goal ZF.thy "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))";
13.405 +Goal "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))";
13.406 by (Blast_tac 1);
13.407 qed "SUM_eq_UN";
13.408
13.409 (** Domain **)
13.410
13.411 -qed_goal "domain_of_prod" ZF.thy "!!A B. b:B ==> domain(A*B) = A"
13.412 - (fn _ => [ Blast_tac 1 ]);
13.413 +Goal "b:B ==> domain(A*B) = A";
13.414 +by (Blast_tac 1);
13.415 +qed "domain_of_prod";
13.416
13.417 qed_goal "domain_0" ZF.thy "domain(0) = 0"
13.418 (fn _ => [ Blast_tac 1 ]);
13.419 @@ -355,19 +351,19 @@
13.420 "domain(cons(<a,b>,r)) = cons(a, domain(r))"
13.421 (fn _ => [ Blast_tac 1 ]);
13.422
13.423 -goal ZF.thy "domain(A Un B) = domain(A) Un domain(B)";
13.424 +Goal "domain(A Un B) = domain(A) Un domain(B)";
13.425 by (Blast_tac 1);
13.426 qed "domain_Un_eq";
13.427
13.428 -goal ZF.thy "domain(A Int B) <= domain(A) Int domain(B)";
13.429 +Goal "domain(A Int B) <= domain(A) Int domain(B)";
13.430 by (Blast_tac 1);
13.431 qed "domain_Int_subset";
13.432
13.433 -goal ZF.thy "domain(A) - domain(B) <= domain(A - B)";
13.434 +Goal "domain(A) - domain(B) <= domain(A - B)";
13.435 by (Blast_tac 1);
13.436 qed "domain_Diff_subset";
13.437
13.438 -goal ZF.thy "domain(converse(r)) = range(r)";
13.439 +Goal "domain(converse(r)) = range(r)";
13.440 by (Blast_tac 1);
13.441 qed "domain_converse";
13.442
13.443 @@ -376,9 +372,9 @@
13.444
13.445 (** Range **)
13.446
13.447 -qed_goal "range_of_prod" ZF.thy
13.448 - "!!a A B. a:A ==> range(A*B) = B"
13.449 - (fn _ => [ Blast_tac 1 ]);
13.450 +Goal "a:A ==> range(A*B) = B";
13.451 +by (Blast_tac 1);
13.452 +qed "range_of_prod";
13.453
13.454 qed_goal "range_0" ZF.thy "range(0) = 0"
13.455 (fn _ => [ Blast_tac 1 ]);
13.456 @@ -387,19 +383,19 @@
13.457 "range(cons(<a,b>,r)) = cons(b, range(r))"
13.458 (fn _ => [ Blast_tac 1 ]);
13.459
13.460 -goal ZF.thy "range(A Un B) = range(A) Un range(B)";
13.461 +Goal "range(A Un B) = range(A) Un range(B)";
13.462 by (Blast_tac 1);
13.463 qed "range_Un_eq";
13.464
13.465 -goal ZF.thy "range(A Int B) <= range(A) Int range(B)";
13.466 +Goal "range(A Int B) <= range(A) Int range(B)";
13.467 by (Blast_tac 1);
13.468 qed "range_Int_subset";
13.469
13.470 -goal ZF.thy "range(A) - range(B) <= range(A - B)";
13.471 +Goal "range(A) - range(B) <= range(A - B)";
13.472 by (Blast_tac 1);
13.473 qed "range_Diff_subset";
13.474
13.475 -goal ZF.thy "range(converse(r)) = domain(r)";
13.476 +Goal "range(converse(r)) = domain(r)";
13.477 by (Blast_tac 1);
13.478 qed "range_converse";
13.479
13.480 @@ -418,19 +414,19 @@
13.481 "field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))"
13.482 (fn _ => [ rtac equalityI 1, ALLGOALS (Blast_tac) ]);
13.483
13.484 -goal ZF.thy "field(A Un B) = field(A) Un field(B)";
13.485 +Goal "field(A Un B) = field(A) Un field(B)";
13.486 by (Blast_tac 1);
13.487 qed "field_Un_eq";
13.488
13.489 -goal ZF.thy "field(A Int B) <= field(A) Int field(B)";
13.490 +Goal "field(A Int B) <= field(A) Int field(B)";
13.491 by (Blast_tac 1);
13.492 qed "field_Int_subset";
13.493
13.494 -goal ZF.thy "field(A) - field(B) <= field(A - B)";
13.495 +Goal "field(A) - field(B) <= field(A - B)";
13.496 by (Blast_tac 1);
13.497 qed "field_Diff_subset";
13.498
13.499 -goal ZF.thy "field(converse(r)) = field(r)";
13.500 +Goal "field(converse(r)) = field(r)";
13.501 by (Blast_tac 1);
13.502 qed "field_converse";
13.503
13.504 @@ -439,72 +435,74 @@
13.505
13.506 (** Image **)
13.507
13.508 -goal ZF.thy "r``0 = 0";
13.509 +Goal "r``0 = 0";
13.510 by (Blast_tac 1);
13.511 qed "image_0";
13.512
13.513 -goal ZF.thy "r``(A Un B) = (r``A) Un (r``B)";
13.514 +Goal "r``(A Un B) = (r``A) Un (r``B)";
13.515 by (Blast_tac 1);
13.516 qed "image_Un";
13.517
13.518 -goal ZF.thy "r``(A Int B) <= (r``A) Int (r``B)";
13.519 +Goal "r``(A Int B) <= (r``A) Int (r``B)";
13.520 by (Blast_tac 1);
13.521 qed "image_Int_subset";
13.522
13.523 -goal ZF.thy "(r Int A*A)``B <= (r``B) Int A";
13.524 +Goal "(r Int A*A)``B <= (r``B) Int A";
13.525 by (Blast_tac 1);
13.526 qed "image_Int_square_subset";
13.527
13.528 -goal ZF.thy "!!r. B<=A ==> (r Int A*A)``B = (r``B) Int A";
13.529 +Goal "B<=A ==> (r Int A*A)``B = (r``B) Int A";
13.530 by (Blast_tac 1);
13.531 qed "image_Int_square";
13.532
13.533 Addsimps [image_0, image_Un];
13.534
13.535 (*Image laws for special relations*)
13.536 -goal ZF.thy "0``A = 0";
13.537 +Goal "0``A = 0";
13.538 by (Blast_tac 1);
13.539 qed "image_0_left";
13.540 Addsimps [image_0_left];
13.541
13.542 -goal ZF.thy "(r Un s)``A = (r``A) Un (s``A)";
13.543 +Goal "(r Un s)``A = (r``A) Un (s``A)";
13.544 by (Blast_tac 1);
13.545 qed "image_Un_left";
13.546
13.547 -goal ZF.thy "(r Int s)``A <= (r``A) Int (s``A)";
13.548 +Goal "(r Int s)``A <= (r``A) Int (s``A)";
13.549 by (Blast_tac 1);
13.550 qed "image_Int_subset_left";
13.551
13.552
13.553 (** Inverse Image **)
13.554
13.555 -goal ZF.thy "r-``0 = 0";
13.556 +Goal "r-``0 = 0";
13.557 by (Blast_tac 1);
13.558 qed "vimage_0";
13.559
13.560 -goal ZF.thy "r-``(A Un B) = (r-``A) Un (r-``B)";
13.561 +Goal "r-``(A Un B) = (r-``A) Un (r-``B)";
13.562 by (Blast_tac 1);
13.563 qed "vimage_Un";
13.564
13.565 -goal ZF.thy "r-``(A Int B) <= (r-``A) Int (r-``B)";
13.566 +Goal "r-``(A Int B) <= (r-``A) Int (r-``B)";
13.567 by (Blast_tac 1);
13.568 qed "vimage_Int_subset";
13.569
13.570 -Goalw [function_def]
13.571 - "function(f) ==> f-``(A Int B) = (f-``A) Int (f-``B)";
13.572 +Goalw [function_def] "function(f) ==> f-``(A Int B) = (f-``A) Int (f-``B)";
13.573 by (Blast_tac 1);
13.574 qed "function_vimage_Int";
13.575
13.576 -Goalw [function_def]
13.577 - "function(f) ==> f-``(A-B) = (f-``A) - (f-``B)";
13.578 +Goalw [function_def] "function(f) ==> f-``(A-B) = (f-``A) - (f-``B)";
13.579 by (Blast_tac 1);
13.580 qed "function_vimage_Diff";
13.581
13.582 -goal ZF.thy "(r Int A*A)-``B <= (r-``B) Int A";
13.583 +Goalw [function_def] "function(f) ==> f `` (f-`` A) <= A";
13.584 +by (Blast_tac 1);
13.585 +qed "function_image_vimage";
13.586 +
13.587 +Goal "(r Int A*A)-``B <= (r-``B) Int A";
13.588 by (Blast_tac 1);
13.589 qed "vimage_Int_square_subset";
13.590
13.591 -goal ZF.thy "!!r. B<=A ==> (r Int A*A)-``B = (r-``B) Int A";
13.592 +Goal "B<=A ==> (r Int A*A)-``B = (r-``B) Int A";
13.593 by (Blast_tac 1);
13.594 qed "vimage_Int_square";
13.595
13.596 @@ -512,35 +510,35 @@
13.597
13.598
13.599 (*Invese image laws for special relations*)
13.600 -goal ZF.thy "0-``A = 0";
13.601 +Goal "0-``A = 0";
13.602 by (Blast_tac 1);
13.603 qed "vimage_0_left";
13.604 Addsimps [vimage_0_left];
13.605
13.606 -goal ZF.thy "(r Un s)-``A = (r-``A) Un (s-``A)";
13.607 +Goal "(r Un s)-``A = (r-``A) Un (s-``A)";
13.608 by (Blast_tac 1);
13.609 qed "vimage_Un_left";
13.610
13.611 -goal ZF.thy "(r Int s)-``A <= (r-``A) Int (s-``A)";
13.612 +Goal "(r Int s)-``A <= (r-``A) Int (s-``A)";
13.613 by (Blast_tac 1);
13.614 qed "vimage_Int_subset_left";
13.615
13.616
13.617 (** Converse **)
13.618
13.619 -goal ZF.thy "converse(A Un B) = converse(A) Un converse(B)";
13.620 +Goal "converse(A Un B) = converse(A) Un converse(B)";
13.621 by (Blast_tac 1);
13.622 qed "converse_Un";
13.623
13.624 -goal ZF.thy "converse(A Int B) = converse(A) Int converse(B)";
13.625 +Goal "converse(A Int B) = converse(A) Int converse(B)";
13.626 by (Blast_tac 1);
13.627 qed "converse_Int";
13.628
13.629 -goal ZF.thy "converse(A - B) = converse(A) - converse(B)";
13.630 +Goal "converse(A - B) = converse(A) - converse(B)";
13.631 by (Blast_tac 1);
13.632 qed "converse_Diff";
13.633
13.634 -goal ZF.thy "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))";
13.635 +Goal "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))";
13.636 by (Blast_tac 1);
13.637 qed "converse_UN";
13.638
13.639 @@ -553,27 +551,27 @@
13.640
13.641 (** Pow **)
13.642
13.643 -goal ZF.thy "Pow(A) Un Pow(B) <= Pow(A Un B)";
13.644 +Goal "Pow(A) Un Pow(B) <= Pow(A Un B)";
13.645 by (Blast_tac 1);
13.646 qed "Un_Pow_subset";
13.647
13.648 -goal ZF.thy "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))";
13.649 +Goal "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))";
13.650 by (Blast_tac 1);
13.651 qed "UN_Pow_subset";
13.652
13.653 -goal ZF.thy "A <= Pow(Union(A))";
13.654 +Goal "A <= Pow(Union(A))";
13.655 by (Blast_tac 1);
13.656 qed "subset_Pow_Union";
13.657
13.658 -goal ZF.thy "Union(Pow(A)) = A";
13.659 +Goal "Union(Pow(A)) = A";
13.660 by (Blast_tac 1);
13.661 qed "Union_Pow_eq";
13.662
13.663 -goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)";
13.664 +Goal "Pow(A Int B) = Pow(A) Int Pow(B)";
13.665 by (Blast_tac 1);
13.666 qed "Int_Pow_eq";
13.667
13.668 -goal ZF.thy "!!x A. x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))";
13.669 +Goal "x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))";
13.670 by (Blast_tac 1);
13.671 qed "INT_Pow_subset";
13.672
13.673 @@ -581,26 +579,26 @@
13.674
13.675 (** RepFun **)
13.676
13.677 -goal ZF.thy "{f(x).x:A}=0 <-> A=0";
13.678 +Goal "{f(x).x:A}=0 <-> A=0";
13.679 (*blast_tac takes too long to find a good depth*)
13.680 by (Blast.depth_tac (claset() addSEs [equalityE]) 10 1);
13.681 qed "RepFun_eq_0_iff";
13.682
13.683 (** Collect **)
13.684
13.685 -goal ZF.thy "Collect(A Un B, P) = Collect(A,P) Un Collect(B,P)";
13.686 +Goal "Collect(A Un B, P) = Collect(A,P) Un Collect(B,P)";
13.687 by (Blast_tac 1);
13.688 qed "Collect_Un";
13.689
13.690 -goal ZF.thy "Collect(A Int B, P) = Collect(A,P) Int Collect(B,P)";
13.691 +Goal "Collect(A Int B, P) = Collect(A,P) Int Collect(B,P)";
13.692 by (Blast_tac 1);
13.693 qed "Collect_Int";
13.694
13.695 -goal ZF.thy "Collect(A - B, P) = Collect(A,P) - Collect(B,P)";
13.696 +Goal "Collect(A - B, P) = Collect(A,P) - Collect(B,P)";
13.697 by (Blast_tac 1);
13.698 qed "Collect_Diff";
13.699
13.700 -goal ZF.thy "{x:cons(a,B). P(x)} = if(P(a), cons(a, {x:B. P(x)}), {x:B. P(x)})";
13.701 +Goal "{x:cons(a,B). P(x)} = if(P(a), cons(a, {x:B. P(x)}), {x:B. P(x)})";
13.702 by (simp_tac (simpset() addsplits [split_if]) 1);
13.703 by (Blast_tac 1);
13.704 qed "Collect_cons";
14.1 --- a/src/ZF/func.ML Fri Aug 14 13:52:42 1998 +0200
14.2 +++ b/src/ZF/func.ML Fri Aug 14 18:37:28 1998 +0200
14.3 @@ -389,25 +389,23 @@
14.4
14.5 (*** Extensions of functions ***)
14.6
14.7 -goal ZF.thy
14.8 - "!!f A B. [| f: A->B; c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)";
14.9 +Goal "[| f: A->B; c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)";
14.10 by (forward_tac [singleton_fun RS fun_disjoint_Un] 1);
14.11 by (asm_full_simp_tac (FOL_ss addsimps [cons_eq]) 2);
14.12 by (Blast_tac 1);
14.13 qed "fun_extend";
14.14
14.15 -goal ZF.thy
14.16 - "!!f A B. [| f: A->B; c~:A; b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B";
14.17 +Goal "[| f: A->B; c~:A; b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B";
14.18 by (blast_tac (claset() addIs [fun_extend RS fun_weaken_type]) 1);
14.19 qed "fun_extend3";
14.20
14.21 -goal ZF.thy "!!f A B. [| f: A->B; a:A; c~:A |] ==> cons(<c,b>,f)`a = f`a";
14.22 +Goal "[| f: A->B; a:A; c~:A |] ==> cons(<c,b>,f)`a = f`a";
14.23 by (rtac (apply_Pair RS consI2 RS apply_equality) 1);
14.24 by (rtac fun_extend 3);
14.25 by (REPEAT (assume_tac 1));
14.26 qed "fun_extend_apply1";
14.27
14.28 -goal ZF.thy "!!f A B. [| f: A->B; c~:A |] ==> cons(<c,b>,f)`c = b";
14.29 +Goal "[| f: A->B; c~:A |] ==> cons(<c,b>,f)`c = b";
14.30 by (rtac (consI1 RS apply_equality) 1);
14.31 by (rtac fun_extend 1);
14.32 by (REPEAT (assume_tac 1));
14.33 @@ -417,8 +415,7 @@
14.34 Addsimps [singleton_apply];
14.35
14.36 (*For Finite.ML. Inclusion of right into left is easy*)
14.37 -goal ZF.thy
14.38 - "!!c. c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})";
14.39 +Goal "c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})";
14.40 by (rtac equalityI 1);
14.41 by (safe_tac (claset() addSEs [fun_extend3]));
14.42 (*Inclusion of left into right*)