author | paulson |
Mon, 17 Aug 1998 13:09:08 +0200 | |
changeset 5325 | f7a5e06adea1 |
parent 5321 | f8848433d240 |
child 5505 | b0856ff6fc69 |
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 |
|
2469 | 69 |
Addsimps [empty_fun, singleton_fun]; |
70 |
||
0 | 71 |
(*** Function Application ***) |
72 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
73 |
Goalw [Pi_def, function_def] |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
74 |
"[| <a,b>: f; <a,c>: f; f: Pi(A,B) |] ==> b=c"; |
2877 | 75 |
by (Blast_tac 1); |
760 | 76 |
qed "apply_equality2"; |
0 | 77 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
78 |
Goalw [apply_def, function_def] |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
79 |
"[| <a,b>: f; function(f) |] ==> f`a = b"; |
4829
aa5ea943f8e3
New proof of apply_equality and new thm Pi_image_cons
paulson
parents:
4512
diff
changeset
|
80 |
by (blast_tac (claset() addIs [the_equality]) 1); |
aa5ea943f8e3
New proof of apply_equality and new thm Pi_image_cons
paulson
parents:
4512
diff
changeset
|
81 |
qed "function_apply_equality"; |
aa5ea943f8e3
New proof of apply_equality and new thm Pi_image_cons
paulson
parents:
4512
diff
changeset
|
82 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
83 |
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
|
84 |
by (blast_tac (claset() addIs [function_apply_equality]) 1); |
760 | 85 |
qed "apply_equality"; |
0 | 86 |
|
517 | 87 |
(*Applying a function outside its domain yields 0*) |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
88 |
Goalw [apply_def] |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
89 |
"a ~: domain(f) ==> f`a = 0"; |
517 | 90 |
by (rtac the_0 1); |
2877 | 91 |
by (Blast_tac 1); |
760 | 92 |
qed "apply_0"; |
517 | 93 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
94 |
Goal "[| f: Pi(A,B); c: f |] ==> EX x:A. c = <x,f`x>"; |
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
95 |
by (forward_tac [fun_is_rel] 1); |
4091 | 96 |
by (blast_tac (claset() addDs [apply_equality]) 1); |
760 | 97 |
qed "Pi_memberD"; |
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
98 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
99 |
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
|
100 |
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
|
101 |
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
|
102 |
by (REPEAT (assume_tac 1)); |
760 | 103 |
qed "apply_Pair"; |
0 | 104 |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
105 |
(*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
|
106 |
Goal "[| f: Pi(A,B); a:A |] ==> f`a : B(a)"; |
0 | 107 |
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
|
108 |
by (REPEAT (ares_tac [apply_Pair] 1)); |
760 | 109 |
qed "apply_type"; |
0 | 110 |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
111 |
(*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
|
112 |
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
|
113 |
by (REPEAT (ares_tac [apply_type] 1)); |
760 | 114 |
qed "apply_funtype"; |
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
115 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
116 |
Goal "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b"; |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
117 |
by (forward_tac [fun_is_rel] 1); |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
118 |
by (blast_tac (claset() addSIs [apply_Pair, apply_equality]) 1); |
760 | 119 |
qed "apply_iff"; |
0 | 120 |
|
121 |
(*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
|
122 |
val pi_prem::prems = Goal |
0 | 123 |
"[| 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
|
124 |
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
|
125 |
by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff]) 1); |
4091 | 126 |
by (blast_tac (claset() addIs prems addSDs [pi_prem RS Pi_memberD]) 1); |
760 | 127 |
qed "Pi_type"; |
0 | 128 |
|
129 |
||
130 |
(** Elimination of membership in a function **) |
|
131 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
132 |
Goal "[| <a,b> : f; f: Pi(A,B) |] ==> a : A"; |
0 | 133 |
by (REPEAT (ares_tac [fun_is_rel RS subsetD RS SigmaD1] 1)); |
760 | 134 |
qed "domain_type"; |
0 | 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) |] ==> b : B(a)"; |
0 | 137 |
by (etac (fun_is_rel RS subsetD RS SigmaD2) 1); |
138 |
by (assume_tac 1); |
|
760 | 139 |
qed "range_type"; |
0 | 140 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
141 |
val prems = Goal |
0 | 142 |
"[| <a,b>: f; f: Pi(A,B); \ |
143 |
\ [| a:A; b:B(a); f`a = b |] ==> P \ |
|
144 |
\ |] ==> P"; |
|
145 |
by (cut_facts_tac prems 1); |
|
146 |
by (resolve_tac prems 1); |
|
147 |
by (REPEAT (eresolve_tac [asm_rl,domain_type,range_type,apply_equality] 1)); |
|
760 | 148 |
qed "Pair_mem_PiE"; |
0 | 149 |
|
150 |
(*** Lambda Abstraction ***) |
|
151 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
152 |
Goalw [lam_def] "a:A ==> <a,b(a)> : (lam x:A. b(x))"; |
0 | 153 |
by (etac RepFunI 1); |
760 | 154 |
qed "lamI"; |
0 | 155 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
156 |
val major::prems = Goalw [lam_def] |
0 | 157 |
"[| p: (lam x:A. b(x)); !!x.[| x:A; p=<x,b(x)> |] ==> P \ |
158 |
\ |] ==> P"; |
|
159 |
by (rtac (major RS RepFunE) 1); |
|
160 |
by (REPEAT (ares_tac prems 1)); |
|
760 | 161 |
qed "lamE"; |
0 | 162 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
163 |
Goal "[| <a,c>: (lam x:A. b(x)) |] ==> c = b(a)"; |
0 | 164 |
by (REPEAT (eresolve_tac [asm_rl,lamE,Pair_inject,ssubst] 1)); |
760 | 165 |
qed "lamD"; |
0 | 166 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
167 |
val prems = Goalw [lam_def, Pi_def, function_def] |
3840 | 168 |
"[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B)"; |
4091 | 169 |
by (blast_tac (claset() addIs prems) 1); |
760 | 170 |
qed "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*) |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
240 |
val fun_subset_eq = prove_goal thy |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
241 |
"!!f. [| f:Pi(A,B); g:Pi(A,C) |] ==> f <= g <-> (f = g)" |
5202 | 242 |
(fn _=> |
243 |
[ (rtac iffI 1), (asm_full_simp_tac ZF_ss 2), |
|
244 |
(rtac fun_extension 1), (REPEAT (atac 1)), |
|
245 |
(dtac (apply_Pair RSN (2,subsetD)) 1), (REPEAT (atac 1)), |
|
246 |
(rtac (apply_equality RS sym) 1), (REPEAT (atac 1)) ]); |
|
247 |
||
248 |
||
0 | 249 |
(*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
|
250 |
val prems = Goal |
0 | 251 |
"[| f: Pi(A,B); \ |
3840 | 252 |
\ !!b. [| ALL x:A. b(x):B(x); f = (lam x:A. b(x)) |] ==> P \ |
0 | 253 |
\ |] ==> P"; |
254 |
by (resolve_tac prems 1); |
|
255 |
by (rtac (eta RS sym) 2); |
|
256 |
by (REPEAT (ares_tac (prems@[ballI,apply_type]) 1)); |
|
760 | 257 |
qed "Pi_lamE"; |
0 | 258 |
|
259 |
||
435 | 260 |
(** Images of functions **) |
261 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
262 |
Goalw [lam_def] "C <= A ==> (lam x:A. b(x)) `` C = {b(x). x:C}"; |
2877 | 263 |
by (Blast_tac 1); |
760 | 264 |
qed "image_lam"; |
435 | 265 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
266 |
Goal "[| f : Pi(A,B); C <= A |] ==> f``C = {f`x. x:C}"; |
437 | 267 |
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
|
268 |
by (asm_full_simp_tac (simpset() addsimps [image_lam, subset_iff]) 1); |
760 | 269 |
qed "image_fun"; |
435 | 270 |
|
5137 | 271 |
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
|
272 |
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
|
273 |
qed "Pi_image_cons"; |
aa5ea943f8e3
New proof of apply_equality and new thm Pi_image_cons
paulson
parents:
4512
diff
changeset
|
274 |
|
435 | 275 |
|
0 | 276 |
(*** properties of "restrict" ***) |
277 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
278 |
Goalw [restrict_def,lam_def] |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
279 |
"[| f: Pi(C,B); A<=C |] ==> restrict(f,A) <= f"; |
4091 | 280 |
by (blast_tac (claset() addIs [apply_Pair]) 1); |
760 | 281 |
qed "restrict_subset"; |
0 | 282 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
283 |
val prems = Goalw [restrict_def] |
0 | 284 |
"[| !!x. x:A ==> f`x: B(x) |] ==> restrict(f,A) : Pi(A,B)"; |
285 |
by (rtac lam_type 1); |
|
286 |
by (eresolve_tac prems 1); |
|
760 | 287 |
qed "restrict_type"; |
0 | 288 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
289 |
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
|
290 |
by (blast_tac (claset() addIs [apply_type, restrict_type]) 1); |
760 | 291 |
qed "restrict_type2"; |
0 | 292 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
293 |
Goalw [restrict_def] "a : A ==> restrict(f,A) ` a = f`a"; |
0 | 294 |
by (etac beta 1); |
760 | 295 |
qed "restrict"; |
0 | 296 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
297 |
Goalw [restrict_def] "restrict(f,0) = 0"; |
2469 | 298 |
by (Simp_tac 1); |
299 |
qed "restrict_empty"; |
|
300 |
||
301 |
Addsimps [restrict, restrict_empty]; |
|
302 |
||
0 | 303 |
(*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
|
304 |
val prems = Goalw [restrict_def] |
0 | 305 |
"[| A=B; !!x. x:B ==> f`x=g`x |] ==> restrict(f,A) = restrict(g,B)"; |
306 |
by (REPEAT (ares_tac (prems@[lam_cong]) 1)); |
|
760 | 307 |
qed "restrict_eqI"; |
0 | 308 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
309 |
Goalw [restrict_def, lam_def] "domain(restrict(f,C)) = C"; |
2877 | 310 |
by (Blast_tac 1); |
760 | 311 |
qed "domain_restrict"; |
0 | 312 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
313 |
Goalw [restrict_def] |
0 | 314 |
"A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))"; |
315 |
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
|
316 |
by (set_mp_tac 1); |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
317 |
by (Asm_simp_tac 1); |
760 | 318 |
qed "restrict_lam_eq"; |
0 | 319 |
|
320 |
||
321 |
||
322 |
(*** Unions of functions ***) |
|
323 |
||
324 |
(** 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
|
325 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
326 |
Goalw [function_def] |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
327 |
"[| ALL x:S. function(x); \ |
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
328 |
\ 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
|
329 |
\ function(Union(S))"; |
2925 | 330 |
by (fast_tac (ZF_cs addSDs [bspec RS bspec]) 1); |
331 |
(*by (Blast_tac 1); takes too long...*) |
|
760 | 332 |
qed "function_Union"; |
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
333 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
334 |
Goalw [Pi_def] |
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
335 |
"[| 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
|
336 |
\ 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
|
337 |
\ Union(S) : domain(Union(S)) -> range(Union(S))"; |
2877 | 338 |
by (blast_tac (subset_cs addSIs [rel_Union, function_Union]) 1); |
760 | 339 |
qed "fun_Union"; |
0 | 340 |
|
341 |
||
342 |
(** The Union of 2 disjoint functions is a function **) |
|
343 |
||
691
b9fc536792bb
ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents:
538
diff
changeset
|
344 |
val Un_rls = [Un_subset_iff, domain_Un_eq, SUM_Un_distrib1, prod_Un_distrib2, |
1461 | 345 |
Un_upper1 RSN (2, subset_trans), |
346 |
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
|
347 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
348 |
Goal "[| f: A->B; g: C->D; A Int C = 0 |] \ |
2925 | 349 |
\ ==> (f Un g) : (A Un C) -> (B Un D)"; |
2877 | 350 |
(*Prove the product and domain subgoals using distributive laws*) |
4091 | 351 |
by (asm_full_simp_tac (simpset() addsimps [Pi_iff,extension]@Un_rls) 1); |
1461 | 352 |
by (rewtac function_def); |
4512
572440df6aa7
Changed required by new blast_tac (the one that squashes flex-flex pairs)
paulson
parents:
4091
diff
changeset
|
353 |
by (Blast_tac 1); |
760 | 354 |
qed "fun_disjoint_Un"; |
0 | 355 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
356 |
Goal "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \ |
0 | 357 |
\ (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
|
358 |
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
|
359 |
by (REPEAT (ares_tac [fun_disjoint_Un] 1)); |
760 | 360 |
qed "fun_disjoint_apply1"; |
0 | 361 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
362 |
Goal "[| c:C; f: A->B; g: C->D; A Int C = 0 |] ==> \ |
0 | 363 |
\ (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
|
364 |
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
|
365 |
by (REPEAT (ares_tac [fun_disjoint_Un] 1)); |
760 | 366 |
qed "fun_disjoint_apply2"; |
0 | 367 |
|
368 |
(** Domain and range of a function/relation **) |
|
369 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
370 |
Goalw [Pi_def] "f : Pi(A,B) ==> domain(f)=A"; |
2877 | 371 |
by (Blast_tac 1); |
760 | 372 |
qed "domain_of_fun"; |
0 | 373 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
374 |
Goal "[| f : Pi(A,B); a: A |] ==> f`a : range(f)"; |
517 | 375 |
by (etac (apply_Pair RS rangeI) 1); |
376 |
by (assume_tac 1); |
|
760 | 377 |
qed "apply_rangeI"; |
517 | 378 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset
|
379 |
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
|
380 |
by (REPEAT (ares_tac [Pi_type, apply_rangeI] 1)); |
760 | 381 |
qed "range_of_fun"; |
0 | 382 |
|
383 |
(*** Extensions of functions ***) |
|
384 |
||
5321 | 385 |
Goal "[| f: A->B; c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)"; |
857 | 386 |
by (forward_tac [singleton_fun RS fun_disjoint_Un] 1); |
519 | 387 |
by (asm_full_simp_tac (FOL_ss addsimps [cons_eq]) 2); |
2877 | 388 |
by (Blast_tac 1); |
760 | 389 |
qed "fun_extend"; |
0 | 390 |
|
5321 | 391 |
Goal "[| f: A->B; c~:A; b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B"; |
4091 | 392 |
by (blast_tac (claset() addIs [fun_extend RS fun_weaken_type]) 1); |
760 | 393 |
qed "fun_extend3"; |
538 | 394 |
|
5321 | 395 |
Goal "[| f: A->B; a:A; c~:A |] ==> cons(<c,b>,f)`a = f`a"; |
0 | 396 |
by (rtac (apply_Pair RS consI2 RS apply_equality) 1); |
397 |
by (rtac fun_extend 3); |
|
398 |
by (REPEAT (assume_tac 1)); |
|
760 | 399 |
qed "fun_extend_apply1"; |
0 | 400 |
|
5321 | 401 |
Goal "[| f: A->B; c~:A |] ==> cons(<c,b>,f)`c = b"; |
0 | 402 |
by (rtac (consI1 RS apply_equality) 1); |
403 |
by (rtac fun_extend 1); |
|
404 |
by (REPEAT (assume_tac 1)); |
|
760 | 405 |
qed "fun_extend_apply2"; |
0 | 406 |
|
2469 | 407 |
bind_thm ("singleton_apply", [singletonI, singleton_fun] MRS apply_equality); |
408 |
Addsimps [singleton_apply]; |
|
409 |
||
538 | 410 |
(*For Finite.ML. Inclusion of right into left is easy*) |
5321 | 411 |
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
|
412 |
by (rtac equalityI 1); |
4091 | 413 |
by (safe_tac (claset() addSEs [fun_extend3])); |
485 | 414 |
(*Inclusion of left into right*) |
415 |
by (subgoal_tac "restrict(x, A) : A -> B" 1); |
|
4091 | 416 |
by (blast_tac (claset() addIs [restrict_type2]) 2); |
485 | 417 |
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
|
418 |
by (rtac (apply_funtype RS UN_I) 1 THEN REPEAT (ares_tac [consI1] 1)); |
2469 | 419 |
by (Simp_tac 1); |
1461 | 420 |
by (rtac fun_extension 1 THEN REPEAT (ares_tac [fun_extend] 1)); |
485 | 421 |
by (etac consE 1); |
422 |
by (ALLGOALS |
|
4091 | 423 |
(asm_simp_tac (simpset() addsimps [restrict, fun_extend_apply1, |
2493 | 424 |
fun_extend_apply2]))); |
760 | 425 |
qed "cons_fun_eq"; |
485 | 426 |