1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/ZF/ZF-eg.txt Wed Jan 13 16:36:36 1999 +0100
1.3 @@ -0,0 +1,230 @@
1.4 +(**** ZF examples ****)
1.5 +
1.6 +Pretty.setmargin 72; (*existing macros just allow this margin*)
1.7 +print_depth 0;
1.8 +
1.9 +(*** Powerset example ***)
1.10 +
1.11 +val [prem] = goal ZF.thy "A<=B ==> Pow(A) <= Pow(B)";
1.12 +by (resolve_tac [subsetI] 1);
1.13 +by (resolve_tac [PowI] 1);
1.14 +by (dresolve_tac [PowD] 1);
1.15 +by (eresolve_tac [subset_trans] 1);
1.16 +by (resolve_tac [prem] 1);
1.17 +val Pow_mono = result();
1.18 +
1.19 +goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)";
1.20 +by (resolve_tac [equalityI] 1);
1.21 +by (resolve_tac [Int_greatest] 1);
1.22 +by (resolve_tac [Int_lower1 RS Pow_mono] 1);
1.23 +by (resolve_tac [Int_lower2 RS Pow_mono] 1);
1.24 +by (resolve_tac [subsetI] 1);
1.25 +by (eresolve_tac [IntE] 1);
1.26 +by (resolve_tac [PowI] 1);
1.27 +by (REPEAT (dresolve_tac [PowD] 1));
1.28 +by (resolve_tac [Int_greatest] 1);
1.29 +by (REPEAT (assume_tac 1));
1.30 +choplev 0;
1.31 +by (fast_tac (ZF_cs addIs [equalityI]) 1);
1.32 +
1.33 +Goal "C<=D ==> Union(C) <= Union(D)";
1.34 +by (resolve_tac [subsetI] 1);
1.35 +by (eresolve_tac [UnionE] 1);
1.36 +by (resolve_tac [UnionI] 1);
1.37 +by (eresolve_tac [subsetD] 1);
1.38 +by (assume_tac 1);
1.39 +by (assume_tac 1);
1.40 +choplev 0;
1.41 +by (resolve_tac [Union_least] 1);
1.42 +by (resolve_tac [Union_upper] 1);
1.43 +by (eresolve_tac [subsetD] 1);
1.44 +
1.45 +
1.46 +val prems = goal ZF.thy
1.47 + "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \
1.48 +\ (f Un g)`a = f`a";
1.49 +by (resolve_tac [apply_equality] 1);
1.50 +by (resolve_tac [UnI1] 1);
1.51 +by (resolve_tac [apply_Pair] 1);
1.52 +by (resolve_tac prems 1);
1.53 +by (resolve_tac prems 1);
1.54 +by (resolve_tac [fun_disjoint_Un] 1);
1.55 +by (resolve_tac prems 1);
1.56 +by (resolve_tac prems 1);
1.57 +by (resolve_tac prems 1);
1.58 +
1.59 +
1.60 +Goal "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \
1.61 +\ (f Un g)`a = f`a";
1.62 +by (resolve_tac [apply_equality] 1);
1.63 +by (resolve_tac [UnI1] 1);
1.64 +by (resolve_tac [apply_Pair] 1);
1.65 +by (assume_tac 1);
1.66 +by (assume_tac 1);
1.67 +by (resolve_tac [fun_disjoint_Un] 1);
1.68 +by (assume_tac 1);
1.69 +by (assume_tac 1);
1.70 +by (assume_tac 1);
1.71 +
1.72 +
1.73 +
1.74 +
1.75 +goal ZF.thy "f``(UN x:A. B(x)) = (UN x:A. f``B(x))";
1.76 +by (resolve_tac [equalityI] 1);
1.77 +by (resolve_tac [subsetI] 1);
1.78 +fe imageE;
1.79 +
1.80 +
1.81 +goal ZF.thy "(UN x:C. A(x) Int B) = (UN x:C. A(x)) Int B";
1.82 +by (resolve_tac [equalityI] 1);
1.83 +by (resolve_tac [Int_greatest] 1);
1.84 +fr UN_mono;
1.85 +by (resolve_tac [Int_lower1] 1);
1.86 +fr UN_least;
1.87 +????
1.88 +
1.89 +
1.90 +> goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)";
1.91 +Level 0
1.92 +Pow(A Int B) = Pow(A) Int Pow(B)
1.93 + 1. Pow(A Int B) = Pow(A) Int Pow(B)
1.94 +> by (resolve_tac [equalityI] 1);
1.95 +Level 1
1.96 +Pow(A Int B) = Pow(A) Int Pow(B)
1.97 + 1. Pow(A Int B) <= Pow(A) Int Pow(B)
1.98 + 2. Pow(A) Int Pow(B) <= Pow(A Int B)
1.99 +> by (resolve_tac [Int_greatest] 1);
1.100 +Level 2
1.101 +Pow(A Int B) = Pow(A) Int Pow(B)
1.102 + 1. Pow(A Int B) <= Pow(A)
1.103 + 2. Pow(A Int B) <= Pow(B)
1.104 + 3. Pow(A) Int Pow(B) <= Pow(A Int B)
1.105 +> by (resolve_tac [Int_lower1 RS Pow_mono] 1);
1.106 +Level 3
1.107 +Pow(A Int B) = Pow(A) Int Pow(B)
1.108 + 1. Pow(A Int B) <= Pow(B)
1.109 + 2. Pow(A) Int Pow(B) <= Pow(A Int B)
1.110 +> by (resolve_tac [Int_lower2 RS Pow_mono] 1);
1.111 +Level 4
1.112 +Pow(A Int B) = Pow(A) Int Pow(B)
1.113 + 1. Pow(A) Int Pow(B) <= Pow(A Int B)
1.114 +> by (resolve_tac [subsetI] 1);
1.115 +Level 5
1.116 +Pow(A Int B) = Pow(A) Int Pow(B)
1.117 + 1. !!x. x : Pow(A) Int Pow(B) ==> x : Pow(A Int B)
1.118 +> by (eresolve_tac [IntE] 1);
1.119 +Level 6
1.120 +Pow(A Int B) = Pow(A) Int Pow(B)
1.121 + 1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x : Pow(A Int B)
1.122 +> by (resolve_tac [PowI] 1);
1.123 +Level 7
1.124 +Pow(A Int B) = Pow(A) Int Pow(B)
1.125 + 1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x <= A Int B
1.126 +> by (REPEAT (dresolve_tac [PowD] 1));
1.127 +Level 8
1.128 +Pow(A Int B) = Pow(A) Int Pow(B)
1.129 + 1. !!x. [| x <= A; x <= B |] ==> x <= A Int B
1.130 +> by (resolve_tac [Int_greatest] 1);
1.131 +Level 9
1.132 +Pow(A Int B) = Pow(A) Int Pow(B)
1.133 + 1. !!x. [| x <= A; x <= B |] ==> x <= A
1.134 + 2. !!x. [| x <= A; x <= B |] ==> x <= B
1.135 +> by (REPEAT (assume_tac 1));
1.136 +Level 10
1.137 +Pow(A Int B) = Pow(A) Int Pow(B)
1.138 +No subgoals!
1.139 +> choplev 0;
1.140 +Level 0
1.141 +Pow(A Int B) = Pow(A) Int Pow(B)
1.142 + 1. Pow(A Int B) = Pow(A) Int Pow(B)
1.143 +> by (fast_tac (ZF_cs addIs [equalityI]) 1);
1.144 +Level 1
1.145 +Pow(A Int B) = Pow(A) Int Pow(B)
1.146 +No subgoals!
1.147 +
1.148 +
1.149 +
1.150 +
1.151 +> val [prem] = goal ZF.thy "C<=D ==> Union(C) <= Union(D)";
1.152 +Level 0
1.153 +Union(C) <= Union(D)
1.154 + 1. Union(C) <= Union(D)
1.155 +> by (resolve_tac [subsetI] 1);
1.156 +Level 1
1.157 +Union(C) <= Union(D)
1.158 + 1. !!x. x : Union(C) ==> x : Union(D)
1.159 +> by (eresolve_tac [UnionE] 1);
1.160 +Level 2
1.161 +Union(C) <= Union(D)
1.162 + 1. !!x B. [| x : B; B : C |] ==> x : Union(D)
1.163 +> by (resolve_tac [UnionI] 1);
1.164 +Level 3
1.165 +Union(C) <= Union(D)
1.166 + 1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : D
1.167 + 2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B)
1.168 +> by (resolve_tac [prem RS subsetD] 1);
1.169 +Level 4
1.170 +Union(C) <= Union(D)
1.171 + 1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : C
1.172 + 2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B)
1.173 +> by (assume_tac 1);
1.174 +Level 5
1.175 +Union(C) <= Union(D)
1.176 + 1. !!x B. [| x : B; B : C |] ==> x : B
1.177 +> by (assume_tac 1);
1.178 +Level 6
1.179 +Union(C) <= Union(D)
1.180 +No subgoals!
1.181 +
1.182 +
1.183 +
1.184 +> val prems = goal ZF.thy
1.185 +# "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \
1.186 +# \ (f Un g)`a = f`a";
1.187 +Level 0
1.188 +(f Un g) ` a = f ` a
1.189 + 1. (f Un g) ` a = f ` a
1.190 +> by (resolve_tac [apply_equality] 1);
1.191 +Level 1
1.192 +(f Un g) ` a = f ` a
1.193 + 1. <a,f ` a> : f Un g
1.194 + 2. f Un g : (PROD x:?A. ?B(x))
1.195 +> by (resolve_tac [UnI1] 1);
1.196 +Level 2
1.197 +(f Un g) ` a = f ` a
1.198 + 1. <a,f ` a> : f
1.199 + 2. f Un g : (PROD x:?A. ?B(x))
1.200 +> by (resolve_tac [apply_Pair] 1);
1.201 +Level 3
1.202 +(f Un g) ` a = f ` a
1.203 + 1. f : (PROD x:?A2. ?B2(x))
1.204 + 2. a : ?A2
1.205 + 3. f Un g : (PROD x:?A. ?B(x))
1.206 +> by (resolve_tac prems 1);
1.207 +Level 4
1.208 +(f Un g) ` a = f ` a
1.209 + 1. a : A
1.210 + 2. f Un g : (PROD x:?A. ?B(x))
1.211 +> by (resolve_tac prems 1);
1.212 +Level 5
1.213 +(f Un g) ` a = f ` a
1.214 + 1. f Un g : (PROD x:?A. ?B(x))
1.215 +> by (resolve_tac [fun_disjoint_Un] 1);
1.216 +Level 6
1.217 +(f Un g) ` a = f ` a
1.218 + 1. f : ?A3 -> ?B3
1.219 + 2. g : ?C3 -> ?D3
1.220 + 3. ?A3 Int ?C3 = 0
1.221 +> by (resolve_tac prems 1);
1.222 +Level 7
1.223 +(f Un g) ` a = f ` a
1.224 + 1. g : ?C3 -> ?D3
1.225 + 2. A Int ?C3 = 0
1.226 +> by (resolve_tac prems 1);
1.227 +Level 8
1.228 +(f Un g) ` a = f ` a
1.229 + 1. A Int C = 0
1.230 +> by (resolve_tac prems 1);
1.231 +Level 9
1.232 +(f Un g) ` a = f ` a
1.233 +No subgoals!