author  lcp 
Fri, 17 Sep 1993 16:52:10 +0200  
changeset 7  268f93ab3bc4 
parent 0  a5a9c433f639 
child 16  0b033d50ca1c 
permissions  rwrr 
0  1 
(* Title: ZF/ex/misc 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1993 University of Cambridge 

5 

6 
Miscellaneous examples for ZermeloFraenkel Set Theory 

7 
Cantor's Theorem; SchroederBernstein Theorem; Composition of homomorphisms... 

8 
*) 

9 

10 
writeln"ZF/ex/misc"; 

11 

12 

13 
(*Example 12 (credited to Peter Andrews) from 

14 
W. Bledsoe. A Maximal Method for Set Variables in Automatic Theoremproving. 

15 
In: J. Hayes and D. Michie and L. Mikulich, eds. Machine Intelligence 9. 

16 
Ellis Horwood, 53100 (1979). *) 

17 
goal ZF.thy "(ALL F. {x}: F > {y}:F) > (ALL A. x:A > y:A)"; 

18 
by (best_tac ZF_cs 1); 

19 
result(); 

20 

21 

22 
(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***) 

23 

24 
val cantor_cs = FOL_cs (*precisely the rules needed for the proof*) 

25 
addSIs [ballI, CollectI, PowI, subsetI] addIs [bexI] 

26 
addSEs [CollectE, equalityCE]; 

27 

28 
(*The search is undirected and similar proof attempts fail*) 

29 
goal ZF.thy "ALL f: A>Pow(A). EX S: Pow(A). ALL x:A. ~ f`x = S"; 

30 
by (best_tac cantor_cs 1); 

31 
result(); 

32 

33 
(*This form displays the diagonal term, {x: A . ~ x: f`x} *) 

34 
val [prem] = goal ZF.thy 

35 
"f: A>Pow(A) ==> (ALL x:A. ~ f`x = ?S) & ?S: Pow(A)"; 

36 
by (best_tac cantor_cs 1); 

37 
result(); 

38 

39 
(*yet another version...*) 

40 
goalw Perm.thy [surj_def] "~ f : surj(A,Pow(A))"; 

41 
by (safe_tac ZF_cs); 

42 
by (etac ballE 1); 

43 
by (best_tac (cantor_cs addSEs [bexE]) 1); 

44 
by (fast_tac ZF_cs 1); 

45 
result(); 

46 

47 

48 
(**** The SchroederBernstein Theorem  see Davey & Priestly, page 106 ****) 

49 

50 
val SB_thy = merge_theories (Fixedpt.thy, Perm.thy); 

51 

52 
(** Lemma: Banach's Decomposition Theorem **) 

53 

54 
goal SB_thy "bnd_mono(X, %W. X  g``(Y  f``W))"; 

55 
by (rtac bnd_monoI 1); 

56 
by (REPEAT (ares_tac [Diff_subset, subset_refl, Diff_mono, image_mono] 1)); 

57 
val decomp_bnd_mono = result(); 

58 

59 
val [gfun] = goal SB_thy 

60 
"g: Y>X ==> \ 

61 
\ g``(Y  f`` lfp(X, %W. X  g``(Y  f``W))) = \ 

62 
\ X  lfp(X, %W. X  g``(Y  f``W)) "; 

63 
by (res_inst_tac [("P", "%u. ?v = Xu")] 

64 
(decomp_bnd_mono RS lfp_Tarski RS ssubst) 1); 

7
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

65 
by (simp_tac (ZF_ss addsimps [subset_refl, double_complement, Diff_subset, 
0  66 
gfun RS fun_is_rel RS image_subset]) 1); 
67 
val Banach_last_equation = result(); 

68 

69 
val prems = goal SB_thy 

70 
"[ f: X>Y; g: Y>X ] ==> \ 

71 
\ EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) & \ 

72 
\ (YA Int YB = 0) & (YA Un YB = Y) & \ 

73 
\ f``XA=YA & g``YB=XB"; 

74 
by (REPEAT 

75 
(FIRSTGOAL 

76 
(resolve_tac [refl, exI, conjI, Diff_disjoint, Diff_partition]))); 

77 
by (rtac Banach_last_equation 3); 

78 
by (REPEAT (resolve_tac (prems@[fun_is_rel, image_subset, lfp_subset]) 1)); 

79 
val decomposition = result(); 

80 

81 
val prems = goal SB_thy 

82 
"[ f: inj(X,Y); g: inj(Y,X) ] ==> EX h. h: bij(X,Y)"; 

83 
by (cut_facts_tac prems 1); 

84 
by (cut_facts_tac [(prems RL [inj_is_fun]) MRS decomposition] 1); 

85 
by (fast_tac (ZF_cs addSIs [restrict_bij,bij_disjoint_Un] 

86 
addIs [bij_converse_bij]) 1); 

87 
(* The instantiation of exI to "restrict(f,XA) Un converse(restrict(g,YB))" 

88 
is forced by the context!! *) 

89 
val schroeder_bernstein = result(); 

90 

91 

92 
(*** Composition of homomorphisms is a homomorphism ***) 

93 

94 
(*Given as a challenge problem in 

95 
R. Boyer et al., 

96 
Set Theory in FirstOrder Logic: Clauses for G\"odel's Axioms, 

97 
JAR 2 (1986), 287327 

98 
*) 

99 

7
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

100 
(*collecting the relevant lemmas*) 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

101 
val hom_ss = ZF_ss addsimps [comp_func,comp_func_apply,SigmaI,apply_funtype]; 
0  102 

7
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

103 
(*The problem below is proving conditions of rewrites such as comp_func_apply; 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

104 
rewriting does not instantiate Vars; we must prove the conditions 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

105 
explicitly.*) 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

106 
fun hom_tac hyps = 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

107 
resolve_tac (TrueI::refl::iff_refl::hyps) ORELSE' 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

108 
(cut_facts_tac hyps THEN' fast_tac prop_cs); 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

109 

268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

110 
(*This version uses a super application of simp_tac*) 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

111 
goal Perm.thy 
0  112 
"(ALL A f B g. hom(A,f,B,g) = \ 
113 
\ {H: A>B. f:A*A>A & g:B*B>B & \ 

7
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

114 
\ (ALL x:A. ALL y:A. H`(f`<x,y>) = g`<H`x,H`y>)}) > \ 
0  115 
\ J : hom(A,f,B,g) & K : hom(B,g,C,h) > \ 
116 
\ (K O J) : hom(A,f,C,h)"; 

7
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

117 
by (simp_tac (hom_ss setsolver hom_tac) 1); 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

118 
(*Also works but slower: 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

119 
by (asm_simp_tac (hom_ss setloop (K (safe_tac FOL_cs))) 1); *) 
0  120 
val comp_homs = result(); 
121 

7
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

122 
(*This version uses metalevel rewriting, safe_tac and asm_simp_tac*) 
0  123 
val [hom_def] = goal Perm.thy 
124 
"(!! A f B g. hom(A,f,B,g) == \ 

125 
\ {H: A>B. f:A*A>A & g:B*B>B & \ 

126 
\ (ALL x:A. ALL y:A. H`(f`<x,y>) = g`<H`x,H`y>)}) ==> \ 

127 
\ J : hom(A,f,B,g) & K : hom(B,g,C,h) > \ 

128 
\ (K O J) : hom(A,f,C,h)"; 

129 
by (rewtac hom_def); 

130 
by (safe_tac ZF_cs); 

7
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

131 
by (asm_simp_tac hom_ss 1); 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

132 
by (asm_simp_tac hom_ss 1); 
0  133 
val comp_homs = result(); 
134 

135 

136 
(** A characterization of functions, suggested by Tobias Nipkow **) 

137 

138 
goalw ZF.thy [Pi_def] 

139 
"r: domain(r)>B <> r <= domain(r)*B & (ALL X. r `` (r `` X) <= X)"; 

140 
by (safe_tac ZF_cs); 

141 
by (fast_tac (ZF_cs addSDs [bspec RS ex1_equalsE]) 1); 

142 
by (eres_inst_tac [("x", "{y}")] allE 1); 

143 
by (fast_tac ZF_cs 1); 

144 
result(); 

145 

146 

147 
(**** From D Pastre. Automatic theorem proving in set theory. 

148 
Artificial Intelligence, 10:127, 1978. 

149 
These examples require forward reasoning! ****) 

150 

151 
(*reduce the clauses to units by type checking  beware of nontermination*) 

152 
fun forw_typechk tyrls [] = [] 

153 
 forw_typechk tyrls clauses = 

154 
let val (units, others) = partition (has_fewer_prems 1) clauses 

155 
in gen_union eq_thm (units, forw_typechk tyrls (tyrls RL others)) 

156 
end; 

157 

158 
(*A crude form of forward reasoning*) 

159 
fun forw_iterate tyrls rls facts 0 = facts 

160 
 forw_iterate tyrls rls facts n = 

161 
let val facts' = 

162 
gen_union eq_thm (forw_typechk (tyrls@facts) (facts RL rls), facts); 

163 
in forw_iterate tyrls rls facts' (n1) end; 

164 

165 
val pastre_rls = 

166 
[comp_mem_injD1, comp_mem_surjD1, comp_mem_injD2, comp_mem_surjD2]; 

167 

168 
fun pastre_facts (fact1::fact2::fact3::prems) = 

169 
forw_iterate (prems @ [comp_surj, comp_inj, comp_func]) 

170 
pastre_rls [fact1,fact2,fact3] 4; 

171 

172 
val prems = goalw Perm.thy [bij_def] 

173 
"[ (h O g O f): inj(A,A); \ 

174 
\ (f O h O g): surj(B,B); \ 

175 
\ (g O f O h): surj(C,C); \ 

176 
\ f: A>B; g: B>C; h: C>A ] ==> h: bij(C,A)"; 

177 
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); 

178 
val pastre1 = result(); 

179 

180 
val prems = goalw Perm.thy [bij_def] 

181 
"[ (h O g O f): surj(A,A); \ 

182 
\ (f O h O g): inj(B,B); \ 

183 
\ (g O f O h): surj(C,C); \ 

184 
\ f: A>B; g: B>C; h: C>A ] ==> h: bij(C,A)"; 

185 
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); 

186 
val pastre2 = result(); 

187 

188 
val prems = goalw Perm.thy [bij_def] 

189 
"[ (h O g O f): surj(A,A); \ 

190 
\ (f O h O g): surj(B,B); \ 

191 
\ (g O f O h): inj(C,C); \ 

192 
\ f: A>B; g: B>C; h: C>A ] ==> h: bij(C,A)"; 

193 
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); 

194 
val pastre3 = result(); 

195 

196 
val prems = goalw Perm.thy [bij_def] 

197 
"[ (h O g O f): surj(A,A); \ 

198 
\ (f O h O g): inj(B,B); \ 

199 
\ (g O f O h): inj(C,C); \ 

200 
\ f: A>B; g: B>C; h: C>A ] ==> h: bij(C,A)"; 

201 
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); 

202 
val pastre4 = result(); 

203 

204 
val prems = goalw Perm.thy [bij_def] 

205 
"[ (h O g O f): inj(A,A); \ 

206 
\ (f O h O g): surj(B,B); \ 

207 
\ (g O f O h): inj(C,C); \ 

208 
\ f: A>B; g: B>C; h: C>A ] ==> h: bij(C,A)"; 

209 
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); 

210 
val pastre5 = result(); 

211 

212 
val prems = goalw Perm.thy [bij_def] 

213 
"[ (h O g O f): inj(A,A); \ 

214 
\ (f O h O g): inj(B,B); \ 

215 
\ (g O f O h): surj(C,C); \ 

216 
\ f: A>B; g: B>C; h: C>A ] ==> h: bij(C,A)"; 

217 
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); 

218 
val pastre6 = result(); 

219 

7
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

220 
(** Yet another example... **) 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

221 

268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

222 
goalw (merge_theories(Sum.thy,Perm.thy)) [bij_def,inj_def,surj_def] 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

223 
"(lam Z:Pow(A+B). <{x:A. Inl(x):Z}, {y:B. Inr(y):Z}>) \ 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

224 
\ : bij(Pow(A+B), Pow(A)*Pow(B))"; 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

225 
by (DO_GOAL 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

226 
[rtac IntI, 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

227 
DO_GOAL 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

228 
[rtac CollectI, 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

229 
fast_tac (ZF_cs addSIs [lam_type]), 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

230 
simp_tac ZF_ss, 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

231 
fast_tac (eq_cs addSEs [sumE] 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

232 
addEs [equalityD1 RS subsetD RS CollectD2, 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

233 
equalityD2 RS subsetD RS CollectD2])], 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

234 
DO_GOAL 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

235 
[rtac CollectI, 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

236 
fast_tac (ZF_cs addSIs [lam_type]), 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

237 
simp_tac ZF_ss, 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

238 
K(safe_tac ZF_cs), 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

239 
res_inst_tac [("x", "{Inl(u). u: ?U} Un {Inr(v). v: ?V}")] bexI, 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

240 
DO_GOAL 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

241 
[res_inst_tac [("t", "Pair")] subst_context2, 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

242 
fast_tac (sum_cs addSIs [equalityI]), 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

243 
fast_tac (sum_cs addSIs [equalityI])], 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

244 
DO_GOAL [fast_tac sum_cs]]] 1); 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

245 
val Pow_bij = result(); 
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset

246 

0  247 
writeln"Reached end of file."; 