author  paulson 
Fri, 03 Jan 1997 15:01:55 +0100  
changeset 2469  b50b8c0eec01 
parent 1782  ab45b881fa62 
child 2496  40efb87985b5 
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 

2469  12 
set_current_thy"Perm"; 
0  13 

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

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

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

17 
Ellis Horwood, 53100 (1979). *) 

2469  18 
goal thy "(ALL F. {x}: F > {y}:F) > (ALL A. x:A > y:A)"; 
19 
by (Best_tac 1); 

0  20 
result(); 
21 

22 

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

24 

25 
(*Given as a challenge problem in 

26 
R. Boyer et al., 

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

28 
JAR 2 (1986), 287327 

29 
*) 

30 

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

31 
(*collecting the relevant lemmas*) 
2469  32 
Addsimps [comp_fun, SigmaI, apply_funtype]; 
0  33 

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

36 
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

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

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

2469  43 
by (asm_simp_tac (!simpset setloop (K (safe_tac (!claset)))) 1); 
0  44 
val comp_homs = result(); 
45 

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

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

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

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

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

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

53 
by (rewtac hom_def); 

2469  54 
by (safe_tac (!claset)); 
55 
by (Asm_simp_tac 1); 

56 
by (Asm_simp_tac 1); 

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

57 
qed "comp_homs"; 
0  58 

59 

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

61 

2469  62 
goalw thy [Pi_def, function_def] 
0  63 
"r: domain(r)>B <> r <= domain(r)*B & (ALL X. r `` (r `` X) <= X)"; 
2469  64 
by (Best_tac 1); 
0  65 
result(); 
66 

67 

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

69 
Artificial Intelligence, 10:127, 1978. 

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

71 

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

73 
fun forw_typechk tyrls [] = [] 

74 
 forw_typechk tyrls clauses = 

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

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

77 
end; 

78 

79 
(*A crude form of forward reasoning*) 

80 
fun forw_iterate tyrls rls facts 0 = facts 

81 
 forw_iterate tyrls rls facts n = 

82 
let val facts' = 

1461  83 
gen_union eq_thm (forw_typechk (tyrls@facts) (facts RL rls), facts); 
0  84 
in forw_iterate tyrls rls facts' (n1) end; 
85 

86 
val pastre_rls = 

87 
[comp_mem_injD1, comp_mem_surjD1, comp_mem_injD2, comp_mem_surjD2]; 

88 

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

434  90 
forw_iterate (prems @ [comp_surj, comp_inj, comp_fun]) 
0  91 
pastre_rls [fact1,fact2,fact3] 4; 
92 

93 
val prems = goalw Perm.thy [bij_def] 

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

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

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

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

99 
qed "pastre1"; 
0  100 

101 
val prems = goalw Perm.thy [bij_def] 

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

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

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

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

107 
qed "pastre2"; 
0  108 

109 
val prems = goalw Perm.thy [bij_def] 

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

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

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

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

115 
qed "pastre3"; 
0  116 

117 
val prems = goalw Perm.thy [bij_def] 

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

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

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

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

123 
qed "pastre4"; 
0  124 

125 
val prems = goalw Perm.thy [bij_def] 

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

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

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

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

131 
qed "pastre5"; 
0  132 

133 
val prems = goalw Perm.thy [bij_def] 

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

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

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

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

139 
qed "pastre6"; 
0  140 

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

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

142 

2469  143 
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

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

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

146 
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

147 
lam_bijective 1); 
a1586fa1b755
ZF/ex/Ramsey,Rmap,misc.ML: modified for new definition of Pi(A,B)
lcp
parents:
434
diff
changeset

148 
by (TRYALL (etac SigmaE)); 
2469  149 
by (ALLGOALS Asm_simp_tac); 
150 
by (ALLGOALS (fast_tac (!claset addSIs [equalityI]))); 

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

151 
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

152 

0  153 
writeln"Reached end of file."; 