44 |
44 |
45 (*Weakening one function type to another; see also Pi_type*) |
45 (*Weakening one function type to another; see also Pi_type*) |
46 Goalw [Pi_def] "[| f: A->B; B<=D |] ==> f: A->D"; |
46 Goalw [Pi_def] "[| f: A->B; B<=D |] ==> f: A->D"; |
47 by (Best_tac 1); |
47 by (Best_tac 1); |
48 qed "fun_weaken_type"; |
48 qed "fun_weaken_type"; |
49 |
|
50 (*Empty function spaces*) |
|
51 Goalw [Pi_def, function_def] "Pi(0,A) = {0}"; |
|
52 by (Blast_tac 1); |
|
53 qed "Pi_empty1"; |
|
54 |
|
55 Goalw [Pi_def] "a:A ==> A->0 = 0"; |
|
56 by (Blast_tac 1); |
|
57 qed "Pi_empty2"; |
|
58 |
|
59 (*The empty function*) |
|
60 Goalw [Pi_def, function_def] "0: Pi(0,B)"; |
|
61 by (Blast_tac 1); |
|
62 qed "empty_fun"; |
|
63 |
|
64 (*The singleton function*) |
|
65 Goalw [Pi_def, function_def] "{<a,b>} : {a} -> {b}"; |
|
66 by (Blast_tac 1); |
|
67 qed "singleton_fun"; |
|
68 |
|
69 Addsimps [Pi_empty1, singleton_fun]; |
|
70 |
49 |
71 (*** Function Application ***) |
50 (*** Function Application ***) |
72 |
51 |
73 Goalw [Pi_def, function_def] "[| <a,b>: f; <a,c>: f; f: Pi(A,B) |] ==> b=c"; |
52 Goalw [Pi_def, function_def] "[| <a,b>: f; <a,c>: f; f: Pi(A,B) |] ==> b=c"; |
74 by (Blast_tac 1); |
53 by (Blast_tac 1); |
127 (*Such functions arise in non-standard datatypes, ZF/ex/Ntree for instance*) |
106 (*Such functions arise in non-standard datatypes, ZF/ex/Ntree for instance*) |
128 Goal "(f : Pi(A, %x. {y:B(x). P(x,y)})) \ |
107 Goal "(f : Pi(A, %x. {y:B(x). P(x,y)})) \ |
129 \ <-> f : Pi(A,B) & (ALL x: A. P(x, f`x))"; |
108 \ <-> f : Pi(A,B) & (ALL x: A. P(x, f`x))"; |
130 by (blast_tac (claset() addIs [Pi_type] addDs [apply_type]) 1); |
109 by (blast_tac (claset() addIs [Pi_type] addDs [apply_type]) 1); |
131 qed "Pi_Collect_iff"; |
110 qed "Pi_Collect_iff"; |
|
111 |
|
112 val [major,minor] = Goal |
|
113 "[| f : Pi(A,B); !!x. x:A ==> B(x)<=C(x) |] ==> f : Pi(A,C)"; |
|
114 by (fast_tac (claset() addSIs [major RS Pi_type, minor RS subsetD, |
|
115 major RS apply_type]) 1); |
|
116 qed "Pi_weaken_type"; |
132 |
117 |
133 |
118 |
134 (** Elimination of membership in a function **) |
119 (** Elimination of membership in a function **) |
135 |
120 |
136 Goal "[| <a,b> : f; f: Pi(A,B) |] ==> a : A"; |
121 Goal "[| <a,b> : f; f: Pi(A,B) |] ==> a : A"; |
201 by (rtac ballI 1); |
186 by (rtac ballI 1); |
202 by (stac beta 1); |
187 by (stac beta 1); |
203 by (assume_tac 1); |
188 by (assume_tac 1); |
204 by (etac (major RS theI) 1); |
189 by (etac (major RS theI) 1); |
205 qed "lam_theI"; |
190 qed "lam_theI"; |
|
191 |
|
192 Goal "[| (lam x:A. f(x)) = (lam x:A. g(x)); a:A |] ==> f(a)=g(a)"; |
|
193 by (fast_tac (claset() addSIs [lamI] addEs [equalityE, lamE]) 1); |
|
194 qed "lam_eqE"; |
|
195 |
|
196 |
|
197 (*Empty function spaces*) |
|
198 Goalw [Pi_def, function_def] "Pi(0,A) = {0}"; |
|
199 by (Blast_tac 1); |
|
200 qed "Pi_empty1"; |
|
201 Addsimps [Pi_empty1]; |
|
202 |
|
203 (*The singleton function*) |
|
204 Goalw [Pi_def, function_def] "{<a,b>} : {a} -> {b}"; |
|
205 by (Blast_tac 1); |
|
206 qed "singleton_fun"; |
|
207 Addsimps [singleton_fun]; |
|
208 |
|
209 Goalw [Pi_def, function_def] "(A->0) = (if A=0 then {0} else 0)"; |
|
210 by (Force_tac 1); |
|
211 qed "Pi_empty2"; |
|
212 Addsimps [Pi_empty2]; |
|
213 |
|
214 Goal "(A->X)=0 \\<longleftrightarrow> X=0 & (A \\<noteq> 0)"; |
|
215 by Auto_tac; |
|
216 by (fast_tac (claset() addSIs [equals0I] addIs [lam_type]) 1); |
|
217 qed "fun_space_empty_iff"; |
|
218 AddIffs [fun_space_empty_iff]; |
206 |
219 |
207 |
220 |
208 (** Extensionality **) |
221 (** Extensionality **) |
209 |
222 |
210 (*Semi-extensionality!*) |
223 (*Semi-extensionality!*) |