104
|
1 |
(**** ZF examples ****)
|
|
2 |
|
|
3 |
Pretty.setmargin 72; (*existing macros just allow this margin*)
|
|
4 |
print_depth 0;
|
|
5 |
|
|
6 |
(*** Powerset example ***)
|
|
7 |
|
115
|
8 |
val [prem] = goal ZF.thy "A<=B ==> Pow(A) <= Pow(B)";
|
104
|
9 |
by (resolve_tac [subsetI] 1);
|
|
10 |
by (resolve_tac [PowI] 1);
|
|
11 |
by (dresolve_tac [PowD] 1);
|
|
12 |
by (eresolve_tac [subset_trans] 1);
|
|
13 |
by (resolve_tac [prem] 1);
|
|
14 |
val Pow_mono = result();
|
|
15 |
|
115
|
16 |
goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)";
|
104
|
17 |
by (resolve_tac [equalityI] 1);
|
|
18 |
by (resolve_tac [Int_greatest] 1);
|
|
19 |
by (resolve_tac [Int_lower1 RS Pow_mono] 1);
|
|
20 |
by (resolve_tac [Int_lower2 RS Pow_mono] 1);
|
|
21 |
by (resolve_tac [subsetI] 1);
|
|
22 |
by (eresolve_tac [IntE] 1);
|
|
23 |
by (resolve_tac [PowI] 1);
|
|
24 |
by (REPEAT (dresolve_tac [PowD] 1));
|
|
25 |
by (resolve_tac [Int_greatest] 1);
|
|
26 |
by (REPEAT (assume_tac 1));
|
|
27 |
choplev 0;
|
|
28 |
by (fast_tac (ZF_cs addIs [equalityI]) 1);
|
|
29 |
|
115
|
30 |
val [prem] = goal ZF.thy "C<=D ==> Union(C) <= Union(D)";
|
104
|
31 |
by (resolve_tac [subsetI] 1);
|
|
32 |
by (eresolve_tac [UnionE] 1);
|
|
33 |
by (resolve_tac [UnionI] 1);
|
|
34 |
by (resolve_tac [prem RS subsetD] 1);
|
|
35 |
by (assume_tac 1);
|
|
36 |
by (assume_tac 1);
|
|
37 |
choplev 0;
|
|
38 |
by (resolve_tac [Union_least] 1);
|
|
39 |
by (resolve_tac [Union_upper] 1);
|
|
40 |
by (eresolve_tac [prem RS subsetD] 1);
|
|
41 |
|
|
42 |
|
115
|
43 |
val prems = goal ZF.thy
|
104
|
44 |
"[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \
|
|
45 |
\ (f Un g)`a = f`a";
|
|
46 |
by (resolve_tac [apply_equality] 1);
|
|
47 |
by (resolve_tac [UnI1] 1);
|
|
48 |
by (resolve_tac [apply_Pair] 1);
|
|
49 |
by (resolve_tac prems 1);
|
|
50 |
by (resolve_tac prems 1);
|
|
51 |
by (resolve_tac [fun_disjoint_Un] 1);
|
|
52 |
by (resolve_tac prems 1);
|
|
53 |
by (resolve_tac prems 1);
|
|
54 |
by (resolve_tac prems 1);
|
|
55 |
|
|
56 |
|
|
57 |
|
|
58 |
|
115
|
59 |
goal ZF.thy "f``(UN x:A. B(x)) = (UN x:A. f``B(x))";
|
104
|
60 |
by (resolve_tac [equalityI] 1);
|
|
61 |
by (resolve_tac [subsetI] 1);
|
|
62 |
fe imageE;
|
|
63 |
|
|
64 |
|
115
|
65 |
goal ZF.thy "(UN x:C. A(x) Int B) = (UN x:C. A(x)) Int B";
|
104
|
66 |
by (resolve_tac [equalityI] 1);
|
|
67 |
by (resolve_tac [Int_greatest] 1);
|
|
68 |
fr UN_mono;
|
|
69 |
by (resolve_tac [Int_lower1] 1);
|
|
70 |
fr UN_least;
|
|
71 |
????
|
|
72 |
|
|
73 |
|
115
|
74 |
> goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)";
|
104
|
75 |
Level 0
|
|
76 |
Pow(A Int B) = Pow(A) Int Pow(B)
|
|
77 |
1. Pow(A Int B) = Pow(A) Int Pow(B)
|
|
78 |
> by (resolve_tac [equalityI] 1);
|
|
79 |
Level 1
|
|
80 |
Pow(A Int B) = Pow(A) Int Pow(B)
|
|
81 |
1. Pow(A Int B) <= Pow(A) Int Pow(B)
|
|
82 |
2. Pow(A) Int Pow(B) <= Pow(A Int B)
|
|
83 |
> by (resolve_tac [Int_greatest] 1);
|
|
84 |
Level 2
|
|
85 |
Pow(A Int B) = Pow(A) Int Pow(B)
|
|
86 |
1. Pow(A Int B) <= Pow(A)
|
|
87 |
2. Pow(A Int B) <= Pow(B)
|
|
88 |
3. Pow(A) Int Pow(B) <= Pow(A Int B)
|
|
89 |
> by (resolve_tac [Int_lower1 RS Pow_mono] 1);
|
|
90 |
Level 3
|
|
91 |
Pow(A Int B) = Pow(A) Int Pow(B)
|
|
92 |
1. Pow(A Int B) <= Pow(B)
|
|
93 |
2. Pow(A) Int Pow(B) <= Pow(A Int B)
|
|
94 |
> by (resolve_tac [Int_lower2 RS Pow_mono] 1);
|
|
95 |
Level 4
|
|
96 |
Pow(A Int B) = Pow(A) Int Pow(B)
|
|
97 |
1. Pow(A) Int Pow(B) <= Pow(A Int B)
|
|
98 |
> by (resolve_tac [subsetI] 1);
|
|
99 |
Level 5
|
|
100 |
Pow(A Int B) = Pow(A) Int Pow(B)
|
|
101 |
1. !!x. x : Pow(A) Int Pow(B) ==> x : Pow(A Int B)
|
|
102 |
> by (eresolve_tac [IntE] 1);
|
|
103 |
Level 6
|
|
104 |
Pow(A Int B) = Pow(A) Int Pow(B)
|
|
105 |
1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x : Pow(A Int B)
|
|
106 |
> by (resolve_tac [PowI] 1);
|
|
107 |
Level 7
|
|
108 |
Pow(A Int B) = Pow(A) Int Pow(B)
|
|
109 |
1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x <= A Int B
|
|
110 |
> by (REPEAT (dresolve_tac [PowD] 1));
|
|
111 |
Level 8
|
|
112 |
Pow(A Int B) = Pow(A) Int Pow(B)
|
|
113 |
1. !!x. [| x <= A; x <= B |] ==> x <= A Int B
|
|
114 |
> by (resolve_tac [Int_greatest] 1);
|
|
115 |
Level 9
|
|
116 |
Pow(A Int B) = Pow(A) Int Pow(B)
|
|
117 |
1. !!x. [| x <= A; x <= B |] ==> x <= A
|
|
118 |
2. !!x. [| x <= A; x <= B |] ==> x <= B
|
|
119 |
> by (REPEAT (assume_tac 1));
|
|
120 |
Level 10
|
|
121 |
Pow(A Int B) = Pow(A) Int Pow(B)
|
|
122 |
No subgoals!
|
|
123 |
> choplev 0;
|
|
124 |
Level 0
|
|
125 |
Pow(A Int B) = Pow(A) Int Pow(B)
|
|
126 |
1. Pow(A Int B) = Pow(A) Int Pow(B)
|
|
127 |
> by (fast_tac (ZF_cs addIs [equalityI]) 1);
|
|
128 |
Level 1
|
|
129 |
Pow(A Int B) = Pow(A) Int Pow(B)
|
|
130 |
No subgoals!
|
|
131 |
|
|
132 |
|
|
133 |
|
|
134 |
|
115
|
135 |
> val [prem] = goal ZF.thy "C<=D ==> Union(C) <= Union(D)";
|
104
|
136 |
Level 0
|
|
137 |
Union(C) <= Union(D)
|
|
138 |
1. Union(C) <= Union(D)
|
|
139 |
> by (resolve_tac [subsetI] 1);
|
|
140 |
Level 1
|
|
141 |
Union(C) <= Union(D)
|
|
142 |
1. !!x. x : Union(C) ==> x : Union(D)
|
|
143 |
> by (eresolve_tac [UnionE] 1);
|
|
144 |
Level 2
|
|
145 |
Union(C) <= Union(D)
|
|
146 |
1. !!x B. [| x : B; B : C |] ==> x : Union(D)
|
|
147 |
> by (resolve_tac [UnionI] 1);
|
|
148 |
Level 3
|
|
149 |
Union(C) <= Union(D)
|
|
150 |
1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : D
|
|
151 |
2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B)
|
|
152 |
> by (resolve_tac [prem RS subsetD] 1);
|
|
153 |
Level 4
|
|
154 |
Union(C) <= Union(D)
|
|
155 |
1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : C
|
|
156 |
2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B)
|
|
157 |
> by (assume_tac 1);
|
|
158 |
Level 5
|
|
159 |
Union(C) <= Union(D)
|
|
160 |
1. !!x B. [| x : B; B : C |] ==> x : B
|
|
161 |
> by (assume_tac 1);
|
|
162 |
Level 6
|
|
163 |
Union(C) <= Union(D)
|
|
164 |
No subgoals!
|
|
165 |
|
|
166 |
|
|
167 |
|
115
|
168 |
> val prems = goal ZF.thy
|
104
|
169 |
# "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \
|
|
170 |
# \ (f Un g)`a = f`a";
|
|
171 |
Level 0
|
|
172 |
(f Un g) ` a = f ` a
|
|
173 |
1. (f Un g) ` a = f ` a
|
|
174 |
> by (resolve_tac [apply_equality] 1);
|
|
175 |
Level 1
|
|
176 |
(f Un g) ` a = f ` a
|
|
177 |
1. <a,f ` a> : f Un g
|
|
178 |
2. f Un g : (PROD x:?A. ?B(x))
|
|
179 |
> by (resolve_tac [UnI1] 1);
|
|
180 |
Level 2
|
|
181 |
(f Un g) ` a = f ` a
|
|
182 |
1. <a,f ` a> : f
|
|
183 |
2. f Un g : (PROD x:?A. ?B(x))
|
|
184 |
> by (resolve_tac [apply_Pair] 1);
|
|
185 |
Level 3
|
|
186 |
(f Un g) ` a = f ` a
|
|
187 |
1. f : (PROD x:?A2. ?B2(x))
|
|
188 |
2. a : ?A2
|
|
189 |
3. f Un g : (PROD x:?A. ?B(x))
|
|
190 |
> by (resolve_tac prems 1);
|
|
191 |
Level 4
|
|
192 |
(f Un g) ` a = f ` a
|
|
193 |
1. a : A
|
|
194 |
2. f Un g : (PROD x:?A. ?B(x))
|
|
195 |
> by (resolve_tac prems 1);
|
|
196 |
Level 5
|
|
197 |
(f Un g) ` a = f ` a
|
|
198 |
1. f Un g : (PROD x:?A. ?B(x))
|
|
199 |
> by (resolve_tac [fun_disjoint_Un] 1);
|
|
200 |
Level 6
|
|
201 |
(f Un g) ` a = f ` a
|
|
202 |
1. f : ?A3 -> ?B3
|
|
203 |
2. g : ?C3 -> ?D3
|
|
204 |
3. ?A3 Int ?C3 = 0
|
|
205 |
> by (resolve_tac prems 1);
|
|
206 |
Level 7
|
|
207 |
(f Un g) ` a = f ` a
|
|
208 |
1. g : ?C3 -> ?D3
|
|
209 |
2. A Int ?C3 = 0
|
|
210 |
> by (resolve_tac prems 1);
|
|
211 |
Level 8
|
|
212 |
(f Un g) ` a = f ` a
|
|
213 |
1. A Int C = 0
|
|
214 |
> by (resolve_tac prems 1);
|
|
215 |
Level 9
|
|
216 |
(f Un g) ` a = f ` a
|
|
217 |
No subgoals!
|