author  lcp 
Tue, 21 Jun 1994 16:26:34 +0200  
changeset 434  89d45187f04d 
parent 38  4433428596f9 
child 695  a1586fa1b755 
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*) 

38  29 
goal ZF.thy "ALL f: A>Pow(A). EX S: Pow(A). ALL x:A. f`x ~= S"; 
0  30 
by (best_tac cantor_cs 1); 
31 
result(); 

32 

38  33 
(*This form displays the diagonal term, {x: A . x ~: f`x} *) 
0  34 
val [prem] = goal ZF.thy 
38  35 
"f: A>Pow(A) ==> (ALL x:A. f`x ~= ?S) & ?S: Pow(A)"; 
0  36 
by (best_tac cantor_cs 1); 
37 
result(); 

38 

39 
(*yet another version...*) 

38  40 
goalw Perm.thy [surj_def] "f ~: surj(A,Pow(A))"; 
0  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 
(*** Composition of homomorphisms is a homomorphism ***) 

49 

50 
(*Given as a challenge problem in 

51 
R. Boyer et al., 

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

53 
JAR 2 (1986), 287327 

54 
*) 

55 

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

56 
(*collecting the relevant lemmas*) 
434  57 
val hom_ss = ZF_ss addsimps [comp_fun,comp_fun_apply,SigmaI,apply_funtype]; 
0  58 

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

60 
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

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

62 
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

63 
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

64 
(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

65 

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

66 
(*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

67 
goal Perm.thy 
0  68 
"(ALL A f B g. hom(A,f,B,g) = \ 
69 
\ {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

70 
\ (ALL x:A. ALL y:A. H`(f`<x,y>) = g`<H`x,H`y>)}) > \ 
0  71 
\ J : hom(A,f,B,g) & K : hom(B,g,C,h) > \ 
72 
\ (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

73 
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

74 
(*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

75 
by (asm_simp_tac (hom_ss setloop (K (safe_tac FOL_cs))) 1); *) 
0  76 
val comp_homs = result(); 
77 

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

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

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

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

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

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

85 
by (rewtac hom_def); 

86 
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

87 
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

88 
by (asm_simp_tac hom_ss 1); 
0  89 
val comp_homs = result(); 
90 

91 

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

93 

94 
goalw ZF.thy [Pi_def] 

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

96 
by (safe_tac ZF_cs); 

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

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

99 
by (fast_tac ZF_cs 1); 

100 
result(); 

101 

102 

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

104 
Artificial Intelligence, 10:127, 1978. 

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

106 

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

108 
fun forw_typechk tyrls [] = [] 

109 
 forw_typechk tyrls clauses = 

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

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

112 
end; 

113 

114 
(*A crude form of forward reasoning*) 

115 
fun forw_iterate tyrls rls facts 0 = facts 

116 
 forw_iterate tyrls rls facts n = 

117 
let val facts' = 

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

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

120 

121 
val pastre_rls = 

122 
[comp_mem_injD1, comp_mem_surjD1, comp_mem_injD2, comp_mem_surjD2]; 

123 

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

434  125 
forw_iterate (prems @ [comp_surj, comp_inj, comp_fun]) 
0  126 
pastre_rls [fact1,fact2,fact3] 4; 
127 

128 
val prems = goalw Perm.thy [bij_def] 

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

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

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

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

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

134 
val pastre1 = result(); 

135 

136 
val prems = goalw Perm.thy [bij_def] 

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

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

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

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

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

142 
val pastre2 = result(); 

143 

144 
val prems = goalw Perm.thy [bij_def] 

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

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

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

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

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

150 
val pastre3 = result(); 

151 

152 
val prems = goalw Perm.thy [bij_def] 

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

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

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

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

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

158 
val pastre4 = result(); 

159 

160 
val prems = goalw Perm.thy [bij_def] 

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

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

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

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

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

166 
val pastre5 = result(); 

167 

168 
val prems = goalw Perm.thy [bij_def] 

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

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

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

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

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

174 
val pastre6 = result(); 

175 

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

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

177 

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

178 
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

179 
"(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

180 
\ : 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

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

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

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

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

185 
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

186 
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

187 
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

188 
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

189 
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

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

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

192 
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

193 
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

194 
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

195 
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

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

197 
[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

198 
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

199 
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

200 
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

201 
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

202 

0  203 
writeln"Reached end of file."; 