author | paulson |
Fri, 30 Jun 2000 12:51:30 +0200 | |
changeset 9211 | 6236c5285bd8 |
parent 9173 | 422968aeed49 |
child 9683 | f87c8c449018 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/func |
0 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1991 University of Cambridge |
5 |
||
6 |
Functions in Zermelo-Fraenkel Set Theory |
|
7 |
*) |
|
8 |
||
9 |
(*** The Pi operator -- dependent function space ***) |
|
10 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
11 |
Goalw [Pi_def] |
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
12 |
"f: Pi(A,B) <-> function(f) & f<=Sigma(A,B) & A<=domain(f)"; |
2877 | 13 |
by (Blast_tac 1); |
760 | 14 |
qed "Pi_iff"; |
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
15 |
|
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
16 |
(*For upward compatibility with the former definition*) |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
17 |
Goalw [Pi_def, function_def] |
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
18 |
"f: Pi(A,B) <-> f<=Sigma(A,B) & (ALL x:A. EX! y. <x,y>: f)"; |
2877 | 19 |
by (Blast_tac 1); |
760 | 20 |
qed "Pi_iff_old"; |
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
21 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
22 |
Goal "f: Pi(A,B) ==> function(f)"; |
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
23 |
by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff]) 1); |
760 | 24 |
qed "fun_is_function"; |
0 | 25 |
|
26 |
(**Two "destruct" rules for Pi **) |
|
27 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
28 |
Goalw [Pi_def] "f: Pi(A,B) ==> f <= Sigma(A,B)"; |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
29 |
by (Blast_tac 1); |
760 | 30 |
qed "fun_is_rel"; |
0 | 31 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
32 |
Goal "[| f: Pi(A,B); a:A |] ==> EX! y. <a,y>: f"; |
4091 | 33 |
by (blast_tac (claset() addSDs [Pi_iff_old RS iffD1]) 1); |
760 | 34 |
qed "fun_unique_Pair"; |
0 | 35 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
36 |
val prems = Goalw [Pi_def] |
0 | 37 |
"[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> Pi(A,B) = Pi(A',B')"; |
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
38 |
by (simp_tac (FOL_ss addsimps prems addcongs [Sigma_cong]) 1); |
760 | 39 |
qed "Pi_cong"; |
0 | 40 |
|
2469 | 41 |
(*Sigma_cong, Pi_cong NOT given to Addcongs: they cause |
42 |
flex-flex pairs and the "Check your prover" error. Most |
|
43 |
Sigmas and Pis are abbreviated as * or -> *) |
|
44 |
||
485 | 45 |
(*Weakening one function type to another; see also Pi_type*) |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
46 |
Goalw [Pi_def] "[| f: A->B; B<=D |] ==> f: A->D"; |
2469 | 47 |
by (Best_tac 1); |
760 | 48 |
qed "fun_weaken_type"; |
0 | 49 |
|
50 |
(*Empty function spaces*) |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
51 |
Goalw [Pi_def, function_def] "Pi(0,A) = {0}"; |
2877 | 52 |
by (Blast_tac 1); |
760 | 53 |
qed "Pi_empty1"; |
0 | 54 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
55 |
Goalw [Pi_def] "a:A ==> A->0 = 0"; |
2877 | 56 |
by (Blast_tac 1); |
760 | 57 |
qed "Pi_empty2"; |
0 | 58 |
|
519 | 59 |
(*The empty function*) |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
60 |
Goalw [Pi_def, function_def] "0: Pi(0,B)"; |
2877 | 61 |
by (Blast_tac 1); |
760 | 62 |
qed "empty_fun"; |
519 | 63 |
|
64 |
(*The singleton function*) |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
65 |
Goalw [Pi_def, function_def] "{<a,b>} : {a} -> {b}"; |
2877 | 66 |
by (Blast_tac 1); |
857 | 67 |
qed "singleton_fun"; |
519 | 68 |
|
8172
988a7737e158
Pi_empty1 is a more general simprule than empty_fun
paulson
parents:
8127
diff
changeset
|
69 |
Addsimps [Pi_empty1, singleton_fun]; |
2469 | 70 |
|
0 | 71 |
(*** Function Application ***) |
72 |
||
5505 | 73 |
Goalw [Pi_def, function_def] "[| <a,b>: f; <a,c>: f; f: Pi(A,B) |] ==> b=c"; |
2877 | 74 |
by (Blast_tac 1); |
760 | 75 |
qed "apply_equality2"; |
0 | 76 |
|
5505 | 77 |
Goalw [apply_def, function_def] "[| <a,b>: f; function(f) |] ==> f`a = b"; |
78 |
by (Blast_tac 1); |
|
4829
aa5ea943f8e3
New proof of apply_equality and new thm Pi_image_cons
paulson
parents:
4512
diff
changeset
|
79 |
qed "function_apply_equality"; |
aa5ea943f8e3
New proof of apply_equality and new thm Pi_image_cons
paulson
parents:
4512
diff
changeset
|
80 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
81 |
Goalw [Pi_def] "[| <a,b>: f; f: Pi(A,B) |] ==> f`a = b"; |
4829
aa5ea943f8e3
New proof of apply_equality and new thm Pi_image_cons
paulson
parents:
4512
diff
changeset
|
82 |
by (blast_tac (claset() addIs [function_apply_equality]) 1); |
760 | 83 |
qed "apply_equality"; |
0 | 84 |
|
517 | 85 |
(*Applying a function outside its domain yields 0*) |
5505 | 86 |
Goalw [apply_def] "a ~: domain(f) ==> f`a = 0"; |
517 | 87 |
by (rtac the_0 1); |
2877 | 88 |
by (Blast_tac 1); |
760 | 89 |
qed "apply_0"; |
517 | 90 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
91 |
Goal "[| f: Pi(A,B); c: f |] ==> EX x:A. c = <x,f`x>"; |
7499 | 92 |
by (ftac fun_is_rel 1); |
4091 | 93 |
by (blast_tac (claset() addDs [apply_equality]) 1); |
760 | 94 |
qed "Pi_memberD"; |
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
95 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
96 |
Goal "[| f: Pi(A,B); a:A |] ==> <a,f`a>: f"; |
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
97 |
by (rtac (fun_unique_Pair RS ex1E) 1); |
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
98 |
by (resolve_tac [apply_equality RS ssubst] 3); |
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
99 |
by (REPEAT (assume_tac 1)); |
760 | 100 |
qed "apply_Pair"; |
0 | 101 |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
102 |
(*Conclusion is flexible -- use res_inst_tac or else apply_funtype below!*) |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
103 |
Goal "[| f: Pi(A,B); a:A |] ==> f`a : B(a)"; |
0 | 104 |
by (rtac (fun_is_rel RS subsetD RS SigmaE2) 1); |
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
105 |
by (REPEAT (ares_tac [apply_Pair] 1)); |
760 | 106 |
qed "apply_type"; |
6153 | 107 |
AddTCs [apply_type]; |
0 | 108 |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
109 |
(*This version is acceptable to the simplifier*) |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
110 |
Goal "[| f: A->B; a:A |] ==> f`a : B"; |
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
111 |
by (REPEAT (ares_tac [apply_type] 1)); |
760 | 112 |
qed "apply_funtype"; |
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
113 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
114 |
Goal "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b"; |
7499 | 115 |
by (ftac fun_is_rel 1); |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
116 |
by (blast_tac (claset() addSIs [apply_Pair, apply_equality]) 1); |
760 | 117 |
qed "apply_iff"; |
0 | 118 |
|
119 |
(*Refining one Pi type to another*) |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
120 |
val pi_prem::prems = Goal |
0 | 121 |
"[| f: Pi(A,C); !!x. x:A ==> f`x : B(x) |] ==> f : Pi(A,B)"; |
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
122 |
by (cut_facts_tac [pi_prem] 1); |
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
123 |
by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff]) 1); |
4091 | 124 |
by (blast_tac (claset() addIs prems addSDs [pi_prem RS Pi_memberD]) 1); |
760 | 125 |
qed "Pi_type"; |
0 | 126 |
|
8127
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
7499
diff
changeset
|
127 |
(*Such functions arise in non-standard datatypes, ZF/ex/Ntree for instance*) |
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
7499
diff
changeset
|
128 |
Goal "(f : Pi(A, %x. {y:B(x). P(x,y)})) \ |
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
7499
diff
changeset
|
129 |
\ <-> f : Pi(A,B) & (ALL x: A. P(x, f`x))"; |
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
7499
diff
changeset
|
130 |
by (blast_tac (claset() addIs [Pi_type] addDs [apply_type]) 1); |
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
7499
diff
changeset
|
131 |
qed "Pi_Collect_iff"; |
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
7499
diff
changeset
|
132 |
|
0 | 133 |
|
134 |
(** Elimination of membership in a function **) |
|
135 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
136 |
Goal "[| <a,b> : f; f: Pi(A,B) |] ==> a : A"; |
0 | 137 |
by (REPEAT (ares_tac [fun_is_rel RS subsetD RS SigmaD1] 1)); |
760 | 138 |
qed "domain_type"; |
0 | 139 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
140 |
Goal "[| <a,b> : f; f: Pi(A,B) |] ==> b : B(a)"; |
0 | 141 |
by (etac (fun_is_rel RS subsetD RS SigmaD2) 1); |
142 |
by (assume_tac 1); |
|
760 | 143 |
qed "range_type"; |
0 | 144 |
|
9173 | 145 |
Goal "[| <a,b>: f; f: Pi(A,B) |] ==> a:A & b:B(a) & f`a = b"; |
146 |
by (blast_tac (claset() addIs [domain_type, range_type, apply_equality]) 1); |
|
147 |
qed "Pair_mem_PiD"; |
|
0 | 148 |
|
149 |
(*** Lambda Abstraction ***) |
|
150 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
151 |
Goalw [lam_def] "a:A ==> <a,b(a)> : (lam x:A. b(x))"; |
0 | 152 |
by (etac RepFunI 1); |
760 | 153 |
qed "lamI"; |
0 | 154 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
155 |
val major::prems = Goalw [lam_def] |
0 | 156 |
"[| p: (lam x:A. b(x)); !!x.[| x:A; p=<x,b(x)> |] ==> P \ |
157 |
\ |] ==> P"; |
|
158 |
by (rtac (major RS RepFunE) 1); |
|
159 |
by (REPEAT (ares_tac prems 1)); |
|
760 | 160 |
qed "lamE"; |
0 | 161 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
162 |
Goal "[| <a,c>: (lam x:A. b(x)) |] ==> c = b(a)"; |
0 | 163 |
by (REPEAT (eresolve_tac [asm_rl,lamE,Pair_inject,ssubst] 1)); |
760 | 164 |
qed "lamD"; |
0 | 165 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
166 |
val prems = Goalw [lam_def, Pi_def, function_def] |
3840 | 167 |
"[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B)"; |
4091 | 168 |
by (blast_tac (claset() addIs prems) 1); |
760 | 169 |
qed "lam_type"; |
6153 | 170 |
AddTCs [lam_type]; |
0 | 171 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
172 |
Goal "(lam x:A. b(x)) : A -> {b(x). x:A}"; |
0 | 173 |
by (REPEAT (ares_tac [refl,lam_type,RepFunI] 1)); |
760 | 174 |
qed "lam_funtype"; |
0 | 175 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
176 |
Goal "a : A ==> (lam x:A. b(x)) ` a = b(a)"; |
0 | 177 |
by (REPEAT (ares_tac [apply_equality,lam_funtype,lamI] 1)); |
760 | 178 |
qed "beta"; |
0 | 179 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
180 |
Goalw [lam_def] "(lam x:0. b(x)) = 0"; |
2469 | 181 |
by (Simp_tac 1); |
182 |
qed "lam_empty"; |
|
183 |
||
5156 | 184 |
Goalw [lam_def] "domain(Lambda(A,b)) = A"; |
185 |
by (Blast_tac 1); |
|
186 |
qed "domain_lam"; |
|
187 |
||
188 |
Addsimps [beta, lam_empty, domain_lam]; |
|
2469 | 189 |
|
0 | 190 |
(*congruence rule for lambda abstraction*) |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
191 |
val prems = Goalw [lam_def] |
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
192 |
"[| A=A'; !!x. x:A' ==> b(x)=b'(x) |] ==> Lambda(A,b) = Lambda(A',b')"; |
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
193 |
by (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1); |
760 | 194 |
qed "lam_cong"; |
0 | 195 |
|
2469 | 196 |
Addcongs [lam_cong]; |
197 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
198 |
val [major] = Goal |
0 | 199 |
"(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)"; |
200 |
by (res_inst_tac [("x", "lam x: A. THE y. Q(x,y)")] exI 1); |
|
201 |
by (rtac ballI 1); |
|
2033 | 202 |
by (stac beta 1); |
0 | 203 |
by (assume_tac 1); |
204 |
by (etac (major RS theI) 1); |
|
760 | 205 |
qed "lam_theI"; |
0 | 206 |
|
207 |
||
208 |
(** Extensionality **) |
|
209 |
||
210 |
(*Semi-extensionality!*) |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
211 |
val prems = Goal |
0 | 212 |
"[| f : Pi(A,B); g: Pi(C,D); A<=C; \ |
213 |
\ !!x. x:A ==> f`x = g`x |] ==> f<=g"; |
|
214 |
by (rtac subsetI 1); |
|
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
215 |
by (eresolve_tac (prems RL [Pi_memberD RS bexE]) 1); |
0 | 216 |
by (etac ssubst 1); |
217 |
by (resolve_tac (prems RL [ssubst]) 1); |
|
218 |
by (REPEAT (ares_tac (prems@[apply_Pair,subsetD]) 1)); |
|
760 | 219 |
qed "fun_subset"; |
0 | 220 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
221 |
val prems = Goal |
0 | 222 |
"[| f : Pi(A,B); g: Pi(A,D); \ |
223 |
\ !!x. x:A ==> f`x = g`x |] ==> f=g"; |
|
224 |
by (REPEAT (ares_tac (prems @ (prems RL [sym]) @ |
|
1461 | 225 |
[subset_refl,equalityI,fun_subset]) 1)); |
760 | 226 |
qed "fun_extension"; |
0 | 227 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
228 |
Goal "f : Pi(A,B) ==> (lam x:A. f`x) = f"; |
0 | 229 |
by (rtac fun_extension 1); |
230 |
by (REPEAT (ares_tac [lam_type,apply_type,beta] 1)); |
|
760 | 231 |
qed "eta"; |
0 | 232 |
|
2469 | 233 |
Addsimps [eta]; |
234 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
235 |
Goal "[| f:Pi(A,B); g:Pi(A,C) |] ==> (ALL a:A. f`a = g`a) <-> f=g"; |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
236 |
by (blast_tac (claset() addIs [fun_extension]) 1); |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
237 |
qed "fun_extension_iff"; |
5202 | 238 |
|
239 |
(*thanks to Mark Staples*) |
|
9211 | 240 |
Goal "[| f:Pi(A,B); g:Pi(A,C) |] ==> f <= g <-> (f = g)"; |
241 |
by (rtac iffI 1); |
|
242 |
by (asm_full_simp_tac ZF_ss 2); |
|
243 |
by (rtac fun_extension 1); |
|
244 |
by (REPEAT (atac 1)); |
|
245 |
by (dtac (apply_Pair RSN (2,subsetD)) 1); |
|
246 |
by (REPEAT (atac 1)); |
|
247 |
by (rtac (apply_equality RS sym) 1); |
|
248 |
by (REPEAT (atac 1)) ; |
|
249 |
qed "fun_subset_eq"; |
|
5202 | 250 |
|
251 |
||
0 | 252 |
(*Every element of Pi(A,B) may be expressed as a lambda abstraction!*) |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
253 |
val prems = Goal |
0 | 254 |
"[| f: Pi(A,B); \ |
3840 | 255 |
\ !!b. [| ALL x:A. b(x):B(x); f = (lam x:A. b(x)) |] ==> P \ |
0 | 256 |
\ |] ==> P"; |
257 |
by (resolve_tac prems 1); |
|
258 |
by (rtac (eta RS sym) 2); |
|
259 |
by (REPEAT (ares_tac (prems@[ballI,apply_type]) 1)); |
|
760 | 260 |
qed "Pi_lamE"; |
0 | 261 |
|
262 |
||
435 | 263 |
(** Images of functions **) |
264 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
265 |
Goalw [lam_def] "C <= A ==> (lam x:A. b(x)) `` C = {b(x). x:C}"; |
2877 | 266 |
by (Blast_tac 1); |
760 | 267 |
qed "image_lam"; |
435 | 268 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
269 |
Goal "[| f : Pi(A,B); C <= A |] ==> f``C = {f`x. x:C}"; |
437 | 270 |
by (etac (eta RS subst) 1); |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
271 |
by (asm_full_simp_tac (simpset() addsimps [image_lam, subset_iff]) 1); |
760 | 272 |
qed "image_fun"; |
435 | 273 |
|
5137 | 274 |
Goal "[| f: Pi(A,B); x: A |] ==> f `` cons(x,y) = cons(f`x, f``y)"; |
4829
aa5ea943f8e3
New proof of apply_equality and new thm Pi_image_cons
paulson
parents:
4512
diff
changeset
|
275 |
by (blast_tac (claset() addDs [apply_equality, apply_Pair]) 1); |
aa5ea943f8e3
New proof of apply_equality and new thm Pi_image_cons
paulson
parents:
4512
diff
changeset
|
276 |
qed "Pi_image_cons"; |
aa5ea943f8e3
New proof of apply_equality and new thm Pi_image_cons
paulson
parents:
4512
diff
changeset
|
277 |
|
435 | 278 |
|
0 | 279 |
(*** properties of "restrict" ***) |
280 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
281 |
Goalw [restrict_def,lam_def] |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
282 |
"[| f: Pi(C,B); A<=C |] ==> restrict(f,A) <= f"; |
4091 | 283 |
by (blast_tac (claset() addIs [apply_Pair]) 1); |
760 | 284 |
qed "restrict_subset"; |
0 | 285 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
286 |
val prems = Goalw [restrict_def] |
0 | 287 |
"[| !!x. x:A ==> f`x: B(x) |] ==> restrict(f,A) : Pi(A,B)"; |
288 |
by (rtac lam_type 1); |
|
289 |
by (eresolve_tac prems 1); |
|
760 | 290 |
qed "restrict_type"; |
0 | 291 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
292 |
Goal "[| f: Pi(C,B); A<=C |] ==> restrict(f,A) : Pi(A,B)"; |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
293 |
by (blast_tac (claset() addIs [apply_type, restrict_type]) 1); |
760 | 294 |
qed "restrict_type2"; |
0 | 295 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
296 |
Goalw [restrict_def] "a : A ==> restrict(f,A) ` a = f`a"; |
0 | 297 |
by (etac beta 1); |
760 | 298 |
qed "restrict"; |
0 | 299 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
300 |
Goalw [restrict_def] "restrict(f,0) = 0"; |
2469 | 301 |
by (Simp_tac 1); |
302 |
qed "restrict_empty"; |
|
303 |
||
304 |
Addsimps [restrict, restrict_empty]; |
|
305 |
||
0 | 306 |
(*NOT SAFE as a congruence rule for the simplifier! Can cause it to fail!*) |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
307 |
val prems = Goalw [restrict_def] |
0 | 308 |
"[| A=B; !!x. x:B ==> f`x=g`x |] ==> restrict(f,A) = restrict(g,B)"; |
309 |
by (REPEAT (ares_tac (prems@[lam_cong]) 1)); |
|
760 | 310 |
qed "restrict_eqI"; |
0 | 311 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
312 |
Goalw [restrict_def, lam_def] "domain(restrict(f,C)) = C"; |
2877 | 313 |
by (Blast_tac 1); |
760 | 314 |
qed "domain_restrict"; |
8182 | 315 |
Addsimps [domain_restrict]; |
0 | 316 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
317 |
Goalw [restrict_def] |
0 | 318 |
"A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))"; |
319 |
by (rtac (refl RS lam_cong) 1); |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
320 |
by (set_mp_tac 1); |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
321 |
by (Asm_simp_tac 1); |
760 | 322 |
qed "restrict_lam_eq"; |
0 | 323 |
|
8182 | 324 |
Goal "f : cons(a, b) -> B ==> f = cons(<a, f ` a>, restrict(f, b))"; |
325 |
by (rtac equalityI 1); |
|
326 |
by (blast_tac (claset() addIs [apply_Pair, impOfSubs restrict_subset]) 2); |
|
327 |
by (auto_tac (claset() addSDs [Pi_memberD], |
|
328 |
simpset() addsimps [restrict_def, lam_def])); |
|
329 |
qed "fun_cons_restrict_eq"; |
|
0 | 330 |
|
331 |
||
332 |
(*** Unions of functions ***) |
|
333 |
||
334 |
(** The Union of a set of COMPATIBLE functions is a function **) |
|
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
335 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
336 |
Goalw [function_def] |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
337 |
"[| ALL x:S. function(x); \ |
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
338 |
\ ALL x:S. ALL y:S. x<=y | y<=x |] ==> \ |
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
339 |
\ function(Union(S))"; |
2925 | 340 |
by (fast_tac (ZF_cs addSDs [bspec RS bspec]) 1); |
341 |
(*by (Blast_tac 1); takes too long...*) |
|
760 | 342 |
qed "function_Union"; |
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
343 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
344 |
Goalw [Pi_def] |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
345 |
"[| ALL f:S. EX C D. f:C->D; \ |
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
346 |
\ ALL f:S. ALL y:S. f<=y | y<=f |] ==> \ |
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
347 |
\ Union(S) : domain(Union(S)) -> range(Union(S))"; |
2877 | 348 |
by (blast_tac (subset_cs addSIs [rel_Union, function_Union]) 1); |
760 | 349 |
qed "fun_Union"; |
0 | 350 |
|
351 |
||
352 |
(** The Union of 2 disjoint functions is a function **) |
|
353 |
||
8201 | 354 |
val Un_rls = [Un_subset_iff, SUM_Un_distrib1, prod_Un_distrib2, |
1461 | 355 |
Un_upper1 RSN (2, subset_trans), |
356 |
Un_upper2 RSN (2, subset_trans)]; |
|
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
357 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
358 |
Goal "[| f: A->B; g: C->D; A Int C = 0 |] \ |
2925 | 359 |
\ ==> (f Un g) : (A Un C) -> (B Un D)"; |
2877 | 360 |
(*Prove the product and domain subgoals using distributive laws*) |
4091 | 361 |
by (asm_full_simp_tac (simpset() addsimps [Pi_iff,extension]@Un_rls) 1); |
1461 | 362 |
by (rewtac function_def); |
4512
572440df6aa7
Changed required by new blast_tac (the one that squashes flex-flex pairs)
paulson
parents:
4091
diff
changeset
|
363 |
by (Blast_tac 1); |
760 | 364 |
qed "fun_disjoint_Un"; |
0 | 365 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
366 |
Goal "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \ |
0 | 367 |
\ (f Un g)`a = f`a"; |
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
368 |
by (rtac (apply_Pair RS UnI1 RS apply_equality) 1); |
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
369 |
by (REPEAT (ares_tac [fun_disjoint_Un] 1)); |
760 | 370 |
qed "fun_disjoint_apply1"; |
0 | 371 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
372 |
Goal "[| c:C; f: A->B; g: C->D; A Int C = 0 |] ==> \ |
0 | 373 |
\ (f Un g)`c = g`c"; |
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
374 |
by (rtac (apply_Pair RS UnI2 RS apply_equality) 1); |
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
375 |
by (REPEAT (ares_tac [fun_disjoint_Un] 1)); |
760 | 376 |
qed "fun_disjoint_apply2"; |
0 | 377 |
|
378 |
(** Domain and range of a function/relation **) |
|
379 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
380 |
Goalw [Pi_def] "f : Pi(A,B) ==> domain(f)=A"; |
2877 | 381 |
by (Blast_tac 1); |
760 | 382 |
qed "domain_of_fun"; |
0 | 383 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
384 |
Goal "[| f : Pi(A,B); a: A |] ==> f`a : range(f)"; |
517 | 385 |
by (etac (apply_Pair RS rangeI) 1); |
386 |
by (assume_tac 1); |
|
760 | 387 |
qed "apply_rangeI"; |
517 | 388 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
389 |
Goal "f : Pi(A,B) ==> f : A->range(f)"; |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
390 |
by (REPEAT (ares_tac [Pi_type, apply_rangeI] 1)); |
760 | 391 |
qed "range_of_fun"; |
0 | 392 |
|
393 |
(*** Extensions of functions ***) |
|
394 |
||
5321 | 395 |
Goal "[| f: A->B; c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)"; |
857 | 396 |
by (forward_tac [singleton_fun RS fun_disjoint_Un] 1); |
519 | 397 |
by (asm_full_simp_tac (FOL_ss addsimps [cons_eq]) 2); |
2877 | 398 |
by (Blast_tac 1); |
760 | 399 |
qed "fun_extend"; |
0 | 400 |
|
5321 | 401 |
Goal "[| f: A->B; c~:A; b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B"; |
4091 | 402 |
by (blast_tac (claset() addIs [fun_extend RS fun_weaken_type]) 1); |
760 | 403 |
qed "fun_extend3"; |
538 | 404 |
|
5321 | 405 |
Goal "[| f: A->B; a:A; c~:A |] ==> cons(<c,b>,f)`a = f`a"; |
0 | 406 |
by (rtac (apply_Pair RS consI2 RS apply_equality) 1); |
407 |
by (rtac fun_extend 3); |
|
408 |
by (REPEAT (assume_tac 1)); |
|
760 | 409 |
qed "fun_extend_apply1"; |
0 | 410 |
|
5321 | 411 |
Goal "[| f: A->B; c~:A |] ==> cons(<c,b>,f)`c = b"; |
0 | 412 |
by (rtac (consI1 RS apply_equality) 1); |
413 |
by (rtac fun_extend 1); |
|
414 |
by (REPEAT (assume_tac 1)); |
|
760 | 415 |
qed "fun_extend_apply2"; |
0 | 416 |
|
2469 | 417 |
bind_thm ("singleton_apply", [singletonI, singleton_fun] MRS apply_equality); |
418 |
Addsimps [singleton_apply]; |
|
419 |
||
538 | 420 |
(*For Finite.ML. Inclusion of right into left is easy*) |
5321 | 421 |
Goal "c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})"; |
737
436019ca97d7
cons_fun_eq: modified strange uses of classical reasoner
lcp
parents:
691
diff
changeset
|
422 |
by (rtac equalityI 1); |
4091 | 423 |
by (safe_tac (claset() addSEs [fun_extend3])); |
485 | 424 |
(*Inclusion of left into right*) |
425 |
by (subgoal_tac "restrict(x, A) : A -> B" 1); |
|
4091 | 426 |
by (blast_tac (claset() addIs [restrict_type2]) 2); |
485 | 427 |
by (rtac UN_I 1 THEN assume_tac 1); |
737
436019ca97d7
cons_fun_eq: modified strange uses of classical reasoner
lcp
parents:
691
diff
changeset
|
428 |
by (rtac (apply_funtype RS UN_I) 1 THEN REPEAT (ares_tac [consI1] 1)); |
2469 | 429 |
by (Simp_tac 1); |
1461 | 430 |
by (rtac fun_extension 1 THEN REPEAT (ares_tac [fun_extend] 1)); |
485 | 431 |
by (etac consE 1); |
432 |
by (ALLGOALS |
|
4091 | 433 |
(asm_simp_tac (simpset() addsimps [restrict, fun_extend_apply1, |
2493 | 434 |
fun_extend_apply2]))); |
760 | 435 |
qed "cons_fun_eq"; |
485 | 436 |