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!
