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