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