1.1 --- a/doc-src/ZF/ZF-eg.txt Fri Aug 15 13:45:39 2003 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,230 +0,0 @@
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!