author  paulson 
Mon, 21 Feb 2000 11:15:43 +0100  
changeset 8266  4bc79ed1233b 
parent 5431  d50c2783f941 
child 9061  144b06e6729e 
permissions  rwrr 
1461  1 
(* Title: ZF/ex/misc 
0  2 
ID: $Id$ 
1461  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1993 University of Cambridge 
5 

6 
Miscellaneous examples for ZermeloFraenkel Set Theory 

1646  7 
Composition of homomorphisms, Pastre's examples, ... 
0  8 
*) 
9 

10 
writeln"ZF/ex/misc"; 

11 

8266  12 
(*These two are cited in Benzmueller and Kohlhash's system description of LEO, 
13 
CADE15, 1998 (page 139143) as theorems LEO could not prove.*) 

14 

15 
Goal "(X = Y Un Z) <> (Y<=X & Z<=X & (ALL V. Y<=V & Z<=V > X<=V))"; 

16 
by (blast_tac (claset() addSIs [equalityI]) 1); 

17 
result(); 

18 

19 
(*the dual of the previous one*) 

20 
Goal "(X = Y Int Z) <> (X<=Y & X<=Z & (ALL V. V<=Y & V<=Z > V<=X))"; 

21 
by (blast_tac (claset() addSIs [equalityI]) 1); 

22 
result(); 

23 

5431  24 
(*trivial example of term synthesis: apparently hard for some provers!*) 
25 
Goal "a ~= b ==> a:?X & b ~: ?X"; 

26 
by (Blast_tac 1); 

27 
result(); 

28 

3000
7ecb8b6a3d7f
Moved blast_tac demo from ZF/func.ML to ZF/ex/misc.ML
paulson
parents:
2496
diff
changeset

29 
(*Nice Blast_tac benchmark. Proved in 0.3s; old tactics can't manage it!*) 
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5068
diff
changeset

30 
Goal "ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}"; 
3000
7ecb8b6a3d7f
Moved blast_tac demo from ZF/func.ML to ZF/ex/misc.ML
paulson
parents:
2496
diff
changeset

31 
by (Blast_tac 1); 
7ecb8b6a3d7f
Moved blast_tac demo from ZF/func.ML to ZF/ex/misc.ML
paulson
parents:
2496
diff
changeset

32 
result(); 
7ecb8b6a3d7f
Moved blast_tac demo from ZF/func.ML to ZF/ex/misc.ML
paulson
parents:
2496
diff
changeset

33 

4322  34 
(*variant of the benchmark above*) 
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5068
diff
changeset

35 
Goal "ALL x:S. Union(S) <= x ==> EX z. S <= {z}"; 
4322  36 
by (Blast_tac 1); 
37 
result(); 

38 

4109  39 
context Perm.thy; 
0  40 

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

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

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

44 
Ellis Horwood, 53100 (1979). *) 

5068  45 
Goal "(ALL F. {x}: F > {y}:F) > (ALL A. x:A > y:A)"; 
2469  46 
by (Best_tac 1); 
0  47 
result(); 
48 

49 

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

51 

52 
(*Given as a challenge problem in 

53 
R. Boyer et al., 

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

55 
JAR 2 (1986), 287327 

56 
*) 

57 

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

58 
(*collecting the relevant lemmas*) 
2469  59 
Addsimps [comp_fun, SigmaI, apply_funtype]; 
0  60 

736  61 
(*This version uses a super application of simp_tac. Needs setloop to help 
62 
proving conditions of rewrites such as comp_fun_apply; 

63 
rewriting does not instantiate Vars*) 

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

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

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

4152  70 
by (asm_simp_tac (simpset() setloop (K Safe_tac)) 1); 
0  71 
val comp_homs = result(); 
72 

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

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

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

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

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

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

80 
by (rewtac hom_def); 

4152  81 
by Safe_tac; 
2469  82 
by (Asm_simp_tac 1); 
83 
by (Asm_simp_tac 1); 

782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
736
diff
changeset

84 
qed "comp_homs"; 
0  85 

86 

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

88 

5068  89 
Goalw [Pi_def, function_def] 
0  90 
"r: domain(r)>B <> r <= domain(r)*B & (ALL X. r `` (r `` X) <= X)"; 
2469  91 
by (Best_tac 1); 
0  92 
result(); 
93 

94 

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

96 
Artificial Intelligence, 10:127, 1978. 

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

98 

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

100 
fun forw_typechk tyrls [] = [] 

101 
 forw_typechk tyrls clauses = 

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

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

104 
end; 

105 

106 
(*A crude form of forward reasoning*) 

107 
fun forw_iterate tyrls rls facts 0 = facts 

108 
 forw_iterate tyrls rls facts n = 

109 
let val facts' = 

1461  110 
gen_union eq_thm (forw_typechk (tyrls@facts) (facts RL rls), facts); 
0  111 
in forw_iterate tyrls rls facts' (n1) end; 
112 

113 
val pastre_rls = 

114 
[comp_mem_injD1, comp_mem_surjD1, comp_mem_injD2, comp_mem_surjD2]; 

115 

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

434  117 
forw_iterate (prems @ [comp_surj, comp_inj, comp_fun]) 
0  118 
pastre_rls [fact1,fact2,fact3] 4; 
119 

120 
val prems = goalw Perm.thy [bij_def] 

1461  121 
"[ (h O g O f): inj(A,A); \ 
122 
\ (f O h O g): surj(B,B); \ 

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

0  124 
\ f: A>B; g: B>C; h: C>A ] ==> h: bij(C,A)"; 
125 
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); 

782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
736
diff
changeset

126 
qed "pastre1"; 
0  127 

128 
val prems = goalw Perm.thy [bij_def] 

1461  129 
"[ (h O g O f): surj(A,A); \ 
130 
\ (f O h O g): inj(B,B); \ 

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

0  132 
\ f: A>B; g: B>C; h: C>A ] ==> h: bij(C,A)"; 
133 
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); 

782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
736
diff
changeset

134 
qed "pastre2"; 
0  135 

136 
val prems = goalw Perm.thy [bij_def] 

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

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

0  140 
\ f: A>B; g: B>C; h: C>A ] ==> h: bij(C,A)"; 
141 
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); 

782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
736
diff
changeset

142 
qed "pastre3"; 
0  143 

144 
val prems = goalw Perm.thy [bij_def] 

1461  145 
"[ (h O g O f): surj(A,A); \ 
146 
\ (f O h O g): inj(B,B); \ 

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

0  148 
\ f: A>B; g: B>C; h: C>A ] ==> h: bij(C,A)"; 
149 
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); 

782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
736
diff
changeset

150 
qed "pastre4"; 
0  151 

152 
val prems = goalw Perm.thy [bij_def] 

1461  153 
"[ (h O g O f): inj(A,A); \ 
154 
\ (f O h O g): surj(B,B); \ 

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

0  156 
\ f: A>B; g: B>C; h: C>A ] ==> h: bij(C,A)"; 
157 
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); 

782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
736
diff
changeset

158 
qed "pastre5"; 
0  159 

160 
val prems = goalw Perm.thy [bij_def] 

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

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

0  164 
\ f: A>B; g: B>C; h: C>A ] ==> h: bij(C,A)"; 
165 
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); 

782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
736
diff
changeset

166 
qed "pastre6"; 
0  167 

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

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

169 

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

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

172 
\ : bij(Pow(A+B), Pow(A)*Pow(B))"; 
1110
756aa2e81f6e
Changed some definitions and proofs to use patternmatching.
lcp
parents:
782
diff
changeset

173 
by (res_inst_tac [("d", "%<X,Y>.{Inl(x).x:X} Un {Inr(y).y:Y}")] 
695
a1586fa1b755
ZF/ex/Ramsey,Rmap,misc.ML: modified for new definition of Pi(A,B)
lcp
parents:
434
diff
changeset

174 
lam_bijective 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4322
diff
changeset

175 
(*Auto_tac no longer proves it*) 
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4322
diff
changeset

176 
by (REPEAT (fast_tac (claset() addss (simpset())) 1)); 
4595  177 
qed "Pow_sum_bij"; 
178 

179 
(*As a special case, we have bij(Pow(A*B), A > Pow B) *) 

180 
goal Perm.thy 

181 
"(lam r:Pow(Sigma(A,B)). lam x:A. r``{x}) \ 

182 
\ : bij(Pow(Sigma(A,B)), PROD x:A. Pow(B(x)))"; 

183 
by (res_inst_tac [("d", "%f. UN x:A. UN y:f`x. {<x,y>}")] lam_bijective 1); 

184 
by (blast_tac (claset() addDs [apply_type]) 2); 

185 
by (blast_tac (claset() addIs [lam_type]) 1); 

186 
by (ALLGOALS Asm_simp_tac); 

187 
by (Fast_tac 1); 

188 
by (rtac fun_extension 1); 

189 
by (assume_tac 2); 

190 
by (rtac (singletonI RS lam_type) 1); 

191 
by (Asm_simp_tac 1); 

192 
by (Blast_tac 1); 

193 
qed "Pow_Sigma_bij"; 

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

194 

0  195 
writeln"Reached end of file."; 