author | paulson |
Wed, 19 Jun 2002 09:03:34 +0200 | |
changeset 13221 | e29378f347e4 |
parent 13219 | 7e44aa8a276e |
child 13248 | ae66c22ed52e |
permissions | -rw-r--r-- |
13163 | 1 |
(* Title: ZF/func.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1991 University of Cambridge |
|
5 |
||
6 |
Functions in Zermelo-Fraenkel Set Theory |
|
7 |
*) |
|
8 |
||
13168
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13163
diff
changeset
|
9 |
theory func = equalities: |
13163 | 10 |
|
13221 | 11 |
lemma relation_converse_converse [simp]: |
12 |
"relation(r) ==> converse(converse(r)) = r" |
|
13 |
by (simp add: relation_def, blast) |
|
14 |
||
15 |
lemma relation_restrict [simp]: "relation(restrict(r,A))" |
|
16 |
by (simp add: restrict_def relation_def, blast) |
|
17 |
||
13163 | 18 |
(*** The Pi operator -- dependent function space ***) |
19 |
||
20 |
lemma Pi_iff: |
|
21 |
"f: Pi(A,B) <-> function(f) & f<=Sigma(A,B) & A<=domain(f)" |
|
22 |
by (unfold Pi_def, blast) |
|
23 |
||
24 |
(*For upward compatibility with the former definition*) |
|
25 |
lemma Pi_iff_old: |
|
26 |
"f: Pi(A,B) <-> f<=Sigma(A,B) & (ALL x:A. EX! y. <x,y>: f)" |
|
27 |
by (unfold Pi_def function_def, blast) |
|
28 |
||
29 |
lemma fun_is_function: "f: Pi(A,B) ==> function(f)" |
|
30 |
by (simp only: Pi_iff) |
|
31 |
||
13219 | 32 |
lemma function_imp_Pi: |
33 |
"[|function(f); relation(f)|] ==> f \<in> domain(f) -> range(f)" |
|
34 |
by (simp add: Pi_iff relation_def, blast) |
|
35 |
||
13172 | 36 |
lemma functionI: |
37 |
"[| !!x y y'. [| <x,y>:r; <x,y'>:r |] ==> y=y' |] ==> function(r)" |
|
38 |
by (simp add: function_def, blast) |
|
39 |
||
13163 | 40 |
(*Functions are relations*) |
41 |
lemma fun_is_rel: "f: Pi(A,B) ==> f <= Sigma(A,B)" |
|
42 |
by (unfold Pi_def, blast) |
|
43 |
||
44 |
lemma Pi_cong: |
|
45 |
"[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> Pi(A,B) = Pi(A',B')" |
|
46 |
by (simp add: Pi_def cong add: Sigma_cong) |
|
47 |
||
48 |
(*Sigma_cong, Pi_cong NOT given to Addcongs: they cause |
|
49 |
flex-flex pairs and the "Check your prover" error. Most |
|
50 |
Sigmas and Pis are abbreviated as * or -> *) |
|
51 |
||
52 |
(*Weakening one function type to another; see also Pi_type*) |
|
53 |
lemma fun_weaken_type: "[| f: A->B; B<=D |] ==> f: A->D" |
|
54 |
by (unfold Pi_def, best) |
|
55 |
||
56 |
(*** Function Application ***) |
|
57 |
||
58 |
lemma apply_equality2: "[| <a,b>: f; <a,c>: f; f: Pi(A,B) |] ==> b=c" |
|
59 |
by (unfold Pi_def function_def, blast) |
|
60 |
||
61 |
lemma function_apply_equality: "[| <a,b>: f; function(f) |] ==> f`a = b" |
|
62 |
by (unfold apply_def function_def, blast) |
|
63 |
||
64 |
lemma apply_equality: "[| <a,b>: f; f: Pi(A,B) |] ==> f`a = b" |
|
65 |
apply (unfold Pi_def) |
|
66 |
apply (blast intro: function_apply_equality) |
|
67 |
done |
|
68 |
||
69 |
(*Applying a function outside its domain yields 0*) |
|
70 |
lemma apply_0: "a ~: domain(f) ==> f`a = 0" |
|
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
71 |
by (unfold apply_def, blast) |
13163 | 72 |
|
73 |
lemma Pi_memberD: "[| f: Pi(A,B); c: f |] ==> EX x:A. c = <x,f`x>" |
|
74 |
apply (frule fun_is_rel) |
|
75 |
apply (blast dest: apply_equality) |
|
76 |
done |
|
77 |
||
78 |
lemma function_apply_Pair: "[| function(f); a : domain(f)|] ==> <a,f`a>: f" |
|
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
79 |
apply (simp add: function_def, clarify) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
80 |
apply (subgoal_tac "f`a = y", blast) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
81 |
apply (simp add: apply_def, blast) |
13163 | 82 |
done |
83 |
||
84 |
lemma apply_Pair: "[| f: Pi(A,B); a:A |] ==> <a,f`a>: f" |
|
85 |
apply (simp add: Pi_iff) |
|
86 |
apply (blast intro: function_apply_Pair) |
|
87 |
done |
|
88 |
||
89 |
(*Conclusion is flexible -- use res_inst_tac or else apply_funtype below!*) |
|
90 |
lemma apply_type [TC]: "[| f: Pi(A,B); a:A |] ==> f`a : B(a)" |
|
91 |
by (blast intro: apply_Pair dest: fun_is_rel) |
|
92 |
||
93 |
(*This version is acceptable to the simplifier*) |
|
94 |
lemma apply_funtype: "[| f: A->B; a:A |] ==> f`a : B" |
|
95 |
by (blast dest: apply_type) |
|
96 |
||
97 |
lemma apply_iff: "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b" |
|
98 |
apply (frule fun_is_rel) |
|
99 |
apply (blast intro!: apply_Pair apply_equality) |
|
100 |
done |
|
101 |
||
102 |
(*Refining one Pi type to another*) |
|
103 |
lemma Pi_type: "[| f: Pi(A,C); !!x. x:A ==> f`x : B(x) |] ==> f : Pi(A,B)" |
|
104 |
apply (simp only: Pi_iff) |
|
105 |
apply (blast dest: function_apply_equality) |
|
106 |
done |
|
107 |
||
108 |
(*Such functions arise in non-standard datatypes, ZF/ex/Ntree for instance*) |
|
109 |
lemma Pi_Collect_iff: |
|
110 |
"(f : Pi(A, %x. {y:B(x). P(x,y)})) |
|
111 |
<-> f : Pi(A,B) & (ALL x: A. P(x, f`x))" |
|
112 |
by (blast intro: Pi_type dest: apply_type) |
|
113 |
||
114 |
lemma Pi_weaken_type: |
|
115 |
"[| f : Pi(A,B); !!x. x:A ==> B(x)<=C(x) |] ==> f : Pi(A,C)" |
|
116 |
by (blast intro: Pi_type dest: apply_type) |
|
117 |
||
118 |
||
119 |
(** Elimination of membership in a function **) |
|
120 |
||
121 |
lemma domain_type: "[| <a,b> : f; f: Pi(A,B) |] ==> a : A" |
|
122 |
by (blast dest: fun_is_rel) |
|
123 |
||
124 |
lemma range_type: "[| <a,b> : f; f: Pi(A,B) |] ==> b : B(a)" |
|
125 |
by (blast dest: fun_is_rel) |
|
126 |
||
127 |
lemma Pair_mem_PiD: "[| <a,b>: f; f: Pi(A,B) |] ==> a:A & b:B(a) & f`a = b" |
|
128 |
by (blast intro: domain_type range_type apply_equality) |
|
129 |
||
130 |
(*** Lambda Abstraction ***) |
|
131 |
||
132 |
lemma lamI: "a:A ==> <a,b(a)> : (lam x:A. b(x))" |
|
133 |
apply (unfold lam_def) |
|
134 |
apply (erule RepFunI) |
|
135 |
done |
|
136 |
||
137 |
lemma lamE: |
|
138 |
"[| p: (lam x:A. b(x)); !!x.[| x:A; p=<x,b(x)> |] ==> P |
|
139 |
|] ==> P" |
|
140 |
by (simp add: lam_def, blast) |
|
141 |
||
142 |
lemma lamD: "[| <a,c>: (lam x:A. b(x)) |] ==> c = b(a)" |
|
143 |
by (simp add: lam_def) |
|
144 |
||
145 |
lemma lam_type [TC]: |
|
146 |
"[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B)" |
|
147 |
by (simp add: lam_def Pi_def function_def, blast) |
|
148 |
||
149 |
lemma lam_funtype: "(lam x:A. b(x)) : A -> {b(x). x:A}" |
|
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
150 |
by (blast intro: lam_type) |
13163 | 151 |
|
13172 | 152 |
lemma function_lam: "function (lam x:A. b(x))" |
153 |
by (simp add: function_def lam_def) |
|
154 |
||
155 |
lemma relation_lam: "relation (lam x:A. b(x))" |
|
156 |
by (simp add: relation_def lam_def) |
|
157 |
||
13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13174
diff
changeset
|
158 |
lemma beta_if [simp]: "(lam x:A. b(x)) ` a = (if a : A then b(a) else 0)" |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
159 |
by (simp add: apply_def lam_def, blast) |
13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13174
diff
changeset
|
160 |
|
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13174
diff
changeset
|
161 |
lemma beta: "a : A ==> (lam x:A. b(x)) ` a = b(a)" |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
162 |
by (simp add: apply_def lam_def, blast) |
13163 | 163 |
|
164 |
lemma lam_empty [simp]: "(lam x:0. b(x)) = 0" |
|
165 |
by (simp add: lam_def) |
|
166 |
||
167 |
lemma domain_lam [simp]: "domain(Lambda(A,b)) = A" |
|
168 |
by (simp add: lam_def, blast) |
|
169 |
||
170 |
(*congruence rule for lambda abstraction*) |
|
171 |
lemma lam_cong [cong]: |
|
172 |
"[| A=A'; !!x. x:A' ==> b(x)=b'(x) |] ==> Lambda(A,b) = Lambda(A',b')" |
|
173 |
by (simp only: lam_def cong add: RepFun_cong) |
|
174 |
||
175 |
lemma lam_theI: |
|
176 |
"(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)" |
|
13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13174
diff
changeset
|
177 |
apply (rule_tac x = "lam x: A. THE y. Q (x,y)" in exI) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
178 |
apply simp |
13163 | 179 |
apply (blast intro: theI) |
180 |
done |
|
181 |
||
182 |
lemma lam_eqE: "[| (lam x:A. f(x)) = (lam x:A. g(x)); a:A |] ==> f(a)=g(a)" |
|
183 |
by (fast intro!: lamI elim: equalityE lamE) |
|
184 |
||
185 |
||
186 |
(*Empty function spaces*) |
|
187 |
lemma Pi_empty1 [simp]: "Pi(0,A) = {0}" |
|
188 |
by (unfold Pi_def function_def, blast) |
|
189 |
||
190 |
(*The singleton function*) |
|
191 |
lemma singleton_fun [simp]: "{<a,b>} : {a} -> {b}" |
|
192 |
by (unfold Pi_def function_def, blast) |
|
193 |
||
194 |
lemma Pi_empty2 [simp]: "(A->0) = (if A=0 then {0} else 0)" |
|
195 |
by (unfold Pi_def function_def, force) |
|
196 |
||
197 |
lemma fun_space_empty_iff [iff]: "(A->X)=0 \<longleftrightarrow> X=0 & (A \<noteq> 0)" |
|
198 |
apply auto |
|
199 |
apply (fast intro!: equals0I intro: lam_type) |
|
200 |
done |
|
201 |
||
202 |
||
203 |
(** Extensionality **) |
|
204 |
||
205 |
(*Semi-extensionality!*) |
|
206 |
||
207 |
lemma fun_subset: |
|
208 |
"[| f : Pi(A,B); g: Pi(C,D); A<=C; |
|
209 |
!!x. x:A ==> f`x = g`x |] ==> f<=g" |
|
210 |
by (force dest: Pi_memberD intro: apply_Pair) |
|
211 |
||
212 |
lemma fun_extension: |
|
213 |
"[| f : Pi(A,B); g: Pi(A,D); |
|
214 |
!!x. x:A ==> f`x = g`x |] ==> f=g" |
|
215 |
by (blast del: subsetI intro: subset_refl sym fun_subset) |
|
216 |
||
217 |
lemma eta [simp]: "f : Pi(A,B) ==> (lam x:A. f`x) = f" |
|
218 |
apply (rule fun_extension) |
|
219 |
apply (auto simp add: lam_type apply_type beta) |
|
220 |
done |
|
221 |
||
222 |
lemma fun_extension_iff: |
|
223 |
"[| f:Pi(A,B); g:Pi(A,C) |] ==> (ALL a:A. f`a = g`a) <-> f=g" |
|
224 |
by (blast intro: fun_extension) |
|
225 |
||
226 |
(*thm by Mark Staples, proof by lcp*) |
|
227 |
lemma fun_subset_eq: "[| f:Pi(A,B); g:Pi(A,C) |] ==> f <= g <-> (f = g)" |
|
228 |
by (blast dest: apply_Pair |
|
229 |
intro: fun_extension apply_equality [symmetric]) |
|
230 |
||
231 |
||
232 |
(*Every element of Pi(A,B) may be expressed as a lambda abstraction!*) |
|
233 |
lemma Pi_lamE: |
|
234 |
assumes major: "f: Pi(A,B)" |
|
235 |
and minor: "!!b. [| ALL x:A. b(x):B(x); f = (lam x:A. b(x)) |] ==> P" |
|
236 |
shows "P" |
|
237 |
apply (rule minor) |
|
238 |
apply (rule_tac [2] eta [symmetric]) |
|
239 |
apply (blast intro: major apply_type)+ |
|
240 |
done |
|
241 |
||
242 |
||
243 |
(** Images of functions **) |
|
244 |
||
245 |
lemma image_lam: "C <= A ==> (lam x:A. b(x)) `` C = {b(x). x:C}" |
|
246 |
by (unfold lam_def, blast) |
|
247 |
||
13179 | 248 |
lemma Repfun_function_if: |
249 |
"function(f) |
|
250 |
==> {f`x. x:C} = (if C <= domain(f) then f``C else cons(0,f``C))"; |
|
251 |
apply simp |
|
252 |
apply (intro conjI impI) |
|
253 |
apply (blast dest: function_apply_equality intro: function_apply_Pair) |
|
254 |
apply (rule equalityI) |
|
255 |
apply (blast intro!: function_apply_Pair apply_0) |
|
256 |
apply (blast dest: function_apply_equality intro: apply_0 [symmetric]) |
|
257 |
done |
|
258 |
||
259 |
(*For this lemma and the next, the right-hand side could equivalently |
|
260 |
be written UN x:C. {f`x} *) |
|
13174 | 261 |
lemma image_function: |
262 |
"[| function(f); C <= domain(f) |] ==> f``C = {f`x. x:C}"; |
|
13179 | 263 |
by (simp add: Repfun_function_if) |
13174 | 264 |
|
13163 | 265 |
lemma image_fun: "[| f : Pi(A,B); C <= A |] ==> f``C = {f`x. x:C}" |
13174 | 266 |
apply (simp add: Pi_iff) |
267 |
apply (blast intro: image_function) |
|
13163 | 268 |
done |
269 |
||
270 |
lemma Pi_image_cons: |
|
271 |
"[| f: Pi(A,B); x: A |] ==> f `` cons(x,y) = cons(f`x, f``y)" |
|
272 |
by (blast dest: apply_equality apply_Pair) |
|
273 |
||
124 | 274 |
|
13163 | 275 |
(*** properties of "restrict" ***) |
276 |
||
13179 | 277 |
lemma restrict_subset: "restrict(f,A) <= f" |
278 |
by (unfold restrict_def, blast) |
|
13163 | 279 |
|
280 |
lemma function_restrictI: |
|
281 |
"function(f) ==> function(restrict(f,A))" |
|
282 |
by (unfold restrict_def function_def, blast) |
|
283 |
||
284 |
lemma restrict_type2: "[| f: Pi(C,B); A<=C |] ==> restrict(f,A) : Pi(A,B)" |
|
285 |
by (simp add: Pi_iff function_def restrict_def, blast) |
|
286 |
||
13179 | 287 |
lemma restrict: "restrict(f,A) ` a = (if a : A then f`a else 0)" |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
288 |
by (simp add: apply_def restrict_def, blast) |
13163 | 289 |
|
290 |
lemma restrict_empty [simp]: "restrict(f,0) = 0" |
|
13179 | 291 |
by (unfold restrict_def, simp) |
13163 | 292 |
|
13172 | 293 |
lemma restrict_iff: "z \<in> restrict(r,A) \<longleftrightarrow> z \<in> r & (\<exists>x\<in>A. \<exists>y. z = \<langle>x, y\<rangle>)" |
294 |
by (simp add: restrict_def) |
|
295 |
||
13163 | 296 |
lemma domain_restrict_lam [simp]: "domain(restrict(Lambda(A,f),C)) = A Int C" |
297 |
apply (unfold restrict_def lam_def) |
|
298 |
apply (rule equalityI) |
|
299 |
apply (auto simp add: domain_iff) |
|
300 |
done |
|
301 |
||
302 |
lemma restrict_restrict [simp]: |
|
303 |
"restrict(restrict(r,A),B) = restrict(r, A Int B)" |
|
304 |
by (unfold restrict_def, blast) |
|
305 |
||
306 |
lemma domain_restrict [simp]: "domain(restrict(f,C)) = domain(f) Int C" |
|
307 |
apply (unfold restrict_def) |
|
308 |
apply (auto simp add: domain_def) |
|
309 |
done |
|
310 |
||
311 |
lemma restrict_idem [simp]: "f <= Sigma(A,B) ==> restrict(f,A) = f" |
|
312 |
by (simp add: restrict_def, blast) |
|
313 |
||
314 |
lemma restrict_if [simp]: "restrict(f,A) ` a = (if a : A then f`a else 0)" |
|
315 |
by (simp add: restrict apply_0) |
|
316 |
||
317 |
lemma restrict_lam_eq: |
|
318 |
"A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))" |
|
319 |
by (unfold restrict_def lam_def, auto) |
|
320 |
||
321 |
lemma fun_cons_restrict_eq: |
|
322 |
"f : cons(a, b) -> B ==> f = cons(<a, f ` a>, restrict(f, b))" |
|
323 |
apply (rule equalityI) |
|
324 |
prefer 2 apply (blast intro: apply_Pair restrict_subset [THEN subsetD]) |
|
325 |
apply (auto dest!: Pi_memberD simp add: restrict_def lam_def) |
|
326 |
done |
|
327 |
||
328 |
||
329 |
(*** Unions of functions ***) |
|
330 |
||
331 |
(** The Union of a set of COMPATIBLE functions is a function **) |
|
332 |
||
333 |
lemma function_Union: |
|
334 |
"[| ALL x:S. function(x); |
|
335 |
ALL x:S. ALL y:S. x<=y | y<=x |] |
|
336 |
==> function(Union(S))" |
|
337 |
by (unfold function_def, blast) |
|
338 |
||
339 |
lemma fun_Union: |
|
340 |
"[| ALL f:S. EX C D. f:C->D; |
|
341 |
ALL f:S. ALL y:S. f<=y | y<=f |] ==> |
|
342 |
Union(S) : domain(Union(S)) -> range(Union(S))" |
|
343 |
apply (unfold Pi_def) |
|
344 |
apply (blast intro!: rel_Union function_Union) |
|
345 |
done |
|
346 |
||
13174 | 347 |
lemma gen_relation_Union [rule_format]: |
348 |
"\<forall>f\<in>F. relation(f) \<Longrightarrow> relation(Union(F))" |
|
349 |
by (simp add: relation_def) |
|
350 |
||
13163 | 351 |
|
352 |
(** The Union of 2 disjoint functions is a function **) |
|
353 |
||
354 |
lemmas Un_rls = Un_subset_iff SUM_Un_distrib1 prod_Un_distrib2 |
|
355 |
subset_trans [OF _ Un_upper1] |
|
356 |
subset_trans [OF _ Un_upper2] |
|
357 |
||
358 |
lemma fun_disjoint_Un: |
|
359 |
"[| f: A->B; g: C->D; A Int C = 0 |] |
|
360 |
==> (f Un g) : (A Un C) -> (B Un D)" |
|
361 |
(*Prove the product and domain subgoals using distributive laws*) |
|
362 |
apply (simp add: Pi_iff extension Un_rls) |
|
363 |
apply (unfold function_def, blast) |
|
364 |
done |
|
365 |
||
13179 | 366 |
lemma fun_disjoint_apply1: "a \<notin> domain(g) ==> (f Un g)`a = f`a" |
367 |
by (simp add: apply_def, blast) |
|
13163 | 368 |
|
13179 | 369 |
lemma fun_disjoint_apply2: "c \<notin> domain(f) ==> (f Un g)`c = g`c" |
370 |
by (simp add: apply_def, blast) |
|
13163 | 371 |
|
372 |
(** Domain and range of a function/relation **) |
|
373 |
||
374 |
lemma domain_of_fun: "f : Pi(A,B) ==> domain(f)=A" |
|
375 |
by (unfold Pi_def, blast) |
|
376 |
||
377 |
lemma apply_rangeI: "[| f : Pi(A,B); a: A |] ==> f`a : range(f)" |
|
378 |
by (erule apply_Pair [THEN rangeI], assumption) |
|
379 |
||
380 |
lemma range_of_fun: "f : Pi(A,B) ==> f : A->range(f)" |
|
381 |
by (blast intro: Pi_type apply_rangeI) |
|
382 |
||
383 |
(*** Extensions of functions ***) |
|
384 |
||
385 |
lemma fun_extend: |
|
386 |
"[| f: A->B; c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)" |
|
387 |
apply (frule singleton_fun [THEN fun_disjoint_Un], blast) |
|
388 |
apply (simp add: cons_eq) |
|
389 |
done |
|
390 |
||
391 |
lemma fun_extend3: |
|
392 |
"[| f: A->B; c~:A; b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B" |
|
393 |
by (blast intro: fun_extend [THEN fun_weaken_type]) |
|
394 |
||
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
395 |
lemma extend_apply: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
396 |
"c ~: domain(f) ==> cons(<c,b>,f)`a = (if a=c then b else f`a)" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
397 |
by (auto simp add: apply_def) |
13163 | 398 |
|
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
399 |
lemma fun_extend_apply [simp]: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
400 |
"[| f: A->B; c~:A |] ==> cons(<c,b>,f)`a = (if a=c then b else f`a)" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
401 |
apply (rule extend_apply) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
402 |
apply (simp add: Pi_def, blast) |
13163 | 403 |
done |
404 |
||
405 |
lemmas singleton_apply = apply_equality [OF singletonI singleton_fun, simp] |
|
406 |
||
407 |
(*For Finite.ML. Inclusion of right into left is easy*) |
|
408 |
lemma cons_fun_eq: |
|
409 |
"c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})" |
|
410 |
apply (rule equalityI) |
|
411 |
apply (safe elim!: fun_extend3) |
|
412 |
(*Inclusion of left into right*) |
|
413 |
apply (subgoal_tac "restrict (x, A) : A -> B") |
|
414 |
prefer 2 apply (blast intro: restrict_type2) |
|
415 |
apply (rule UN_I, assumption) |
|
416 |
apply (rule apply_funtype [THEN UN_I]) |
|
417 |
apply assumption |
|
418 |
apply (rule consI1) |
|
419 |
apply (simp (no_asm)) |
|
420 |
apply (rule fun_extension) |
|
421 |
apply assumption |
|
422 |
apply (blast intro: fun_extend) |
|
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
423 |
apply (erule consE, simp_all) |
13163 | 424 |
done |
425 |
||
426 |
ML |
|
427 |
{* |
|
428 |
val Pi_iff = thm "Pi_iff"; |
|
429 |
val Pi_iff_old = thm "Pi_iff_old"; |
|
430 |
val fun_is_function = thm "fun_is_function"; |
|
431 |
val fun_is_rel = thm "fun_is_rel"; |
|
432 |
val Pi_cong = thm "Pi_cong"; |
|
433 |
val fun_weaken_type = thm "fun_weaken_type"; |
|
434 |
val apply_equality2 = thm "apply_equality2"; |
|
435 |
val function_apply_equality = thm "function_apply_equality"; |
|
436 |
val apply_equality = thm "apply_equality"; |
|
437 |
val apply_0 = thm "apply_0"; |
|
438 |
val Pi_memberD = thm "Pi_memberD"; |
|
439 |
val function_apply_Pair = thm "function_apply_Pair"; |
|
440 |
val apply_Pair = thm "apply_Pair"; |
|
441 |
val apply_type = thm "apply_type"; |
|
442 |
val apply_funtype = thm "apply_funtype"; |
|
443 |
val apply_iff = thm "apply_iff"; |
|
444 |
val Pi_type = thm "Pi_type"; |
|
445 |
val Pi_Collect_iff = thm "Pi_Collect_iff"; |
|
446 |
val Pi_weaken_type = thm "Pi_weaken_type"; |
|
447 |
val domain_type = thm "domain_type"; |
|
448 |
val range_type = thm "range_type"; |
|
449 |
val Pair_mem_PiD = thm "Pair_mem_PiD"; |
|
450 |
val lamI = thm "lamI"; |
|
451 |
val lamE = thm "lamE"; |
|
452 |
val lamD = thm "lamD"; |
|
453 |
val lam_type = thm "lam_type"; |
|
454 |
val lam_funtype = thm "lam_funtype"; |
|
455 |
val beta = thm "beta"; |
|
456 |
val lam_empty = thm "lam_empty"; |
|
457 |
val domain_lam = thm "domain_lam"; |
|
458 |
val lam_cong = thm "lam_cong"; |
|
459 |
val lam_theI = thm "lam_theI"; |
|
460 |
val lam_eqE = thm "lam_eqE"; |
|
461 |
val Pi_empty1 = thm "Pi_empty1"; |
|
462 |
val singleton_fun = thm "singleton_fun"; |
|
463 |
val Pi_empty2 = thm "Pi_empty2"; |
|
464 |
val fun_space_empty_iff = thm "fun_space_empty_iff"; |
|
465 |
val fun_subset = thm "fun_subset"; |
|
466 |
val fun_extension = thm "fun_extension"; |
|
467 |
val eta = thm "eta"; |
|
468 |
val fun_extension_iff = thm "fun_extension_iff"; |
|
469 |
val fun_subset_eq = thm "fun_subset_eq"; |
|
470 |
val Pi_lamE = thm "Pi_lamE"; |
|
471 |
val image_lam = thm "image_lam"; |
|
472 |
val image_fun = thm "image_fun"; |
|
473 |
val Pi_image_cons = thm "Pi_image_cons"; |
|
474 |
val restrict_subset = thm "restrict_subset"; |
|
475 |
val function_restrictI = thm "function_restrictI"; |
|
476 |
val restrict_type2 = thm "restrict_type2"; |
|
477 |
val restrict = thm "restrict"; |
|
478 |
val restrict_empty = thm "restrict_empty"; |
|
479 |
val domain_restrict_lam = thm "domain_restrict_lam"; |
|
480 |
val restrict_restrict = thm "restrict_restrict"; |
|
481 |
val domain_restrict = thm "domain_restrict"; |
|
482 |
val restrict_idem = thm "restrict_idem"; |
|
483 |
val restrict_if = thm "restrict_if"; |
|
484 |
val restrict_lam_eq = thm "restrict_lam_eq"; |
|
485 |
val fun_cons_restrict_eq = thm "fun_cons_restrict_eq"; |
|
486 |
val function_Union = thm "function_Union"; |
|
487 |
val fun_Union = thm "fun_Union"; |
|
488 |
val fun_disjoint_Un = thm "fun_disjoint_Un"; |
|
489 |
val fun_disjoint_apply1 = thm "fun_disjoint_apply1"; |
|
490 |
val fun_disjoint_apply2 = thm "fun_disjoint_apply2"; |
|
491 |
val domain_of_fun = thm "domain_of_fun"; |
|
492 |
val apply_rangeI = thm "apply_rangeI"; |
|
493 |
val range_of_fun = thm "range_of_fun"; |
|
494 |
val fun_extend = thm "fun_extend"; |
|
495 |
val fun_extend3 = thm "fun_extend3"; |
|
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
496 |
val fun_extend_apply = thm "fun_extend_apply"; |
13163 | 497 |
val singleton_apply = thm "singleton_apply"; |
498 |
val cons_fun_eq = thm "cons_fun_eq"; |
|
499 |
*} |
|
500 |
||
501 |
end |