author | obua |
Thu, 16 Feb 2006 04:17:19 +0100 | |
changeset 19067 | c0321d7d6b3d |
parent 16417 | 9bc16273c2d4 |
child 24893 | b8ef7afe3a6b |
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 |
*) |
|
7 |
||
13355 | 8 |
header{*Functions, Function Spaces, Lambda-Abstraction*} |
9 |
||
16417 | 10 |
theory func imports equalities Sum begin |
13163 | 11 |
|
13355 | 12 |
subsection{*The Pi Operator: Dependent Function Space*} |
13 |
||
13248 | 14 |
lemma subset_Sigma_imp_relation: "r <= Sigma(A,B) ==> relation(r)" |
15 |
by (simp add: relation_def, blast) |
|
16 |
||
13221 | 17 |
lemma relation_converse_converse [simp]: |
18 |
"relation(r) ==> converse(converse(r)) = r" |
|
19 |
by (simp add: relation_def, blast) |
|
20 |
||
21 |
lemma relation_restrict [simp]: "relation(restrict(r,A))" |
|
22 |
by (simp add: restrict_def relation_def, blast) |
|
23 |
||
13163 | 24 |
lemma Pi_iff: |
25 |
"f: Pi(A,B) <-> function(f) & f<=Sigma(A,B) & A<=domain(f)" |
|
26 |
by (unfold Pi_def, blast) |
|
27 |
||
28 |
(*For upward compatibility with the former definition*) |
|
29 |
lemma Pi_iff_old: |
|
30 |
"f: Pi(A,B) <-> f<=Sigma(A,B) & (ALL x:A. EX! y. <x,y>: f)" |
|
31 |
by (unfold Pi_def function_def, blast) |
|
32 |
||
33 |
lemma fun_is_function: "f: Pi(A,B) ==> function(f)" |
|
34 |
by (simp only: Pi_iff) |
|
35 |
||
13219 | 36 |
lemma function_imp_Pi: |
37 |
"[|function(f); relation(f)|] ==> f \<in> domain(f) -> range(f)" |
|
38 |
by (simp add: Pi_iff relation_def, blast) |
|
39 |
||
13172 | 40 |
lemma functionI: |
41 |
"[| !!x y y'. [| <x,y>:r; <x,y'>:r |] ==> y=y' |] ==> function(r)" |
|
42 |
by (simp add: function_def, blast) |
|
43 |
||
13163 | 44 |
(*Functions are relations*) |
45 |
lemma fun_is_rel: "f: Pi(A,B) ==> f <= Sigma(A,B)" |
|
46 |
by (unfold Pi_def, blast) |
|
47 |
||
48 |
lemma Pi_cong: |
|
49 |
"[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> Pi(A,B) = Pi(A',B')" |
|
50 |
by (simp add: Pi_def cong add: Sigma_cong) |
|
51 |
||
52 |
(*Sigma_cong, Pi_cong NOT given to Addcongs: they cause |
|
53 |
flex-flex pairs and the "Check your prover" error. Most |
|
54 |
Sigmas and Pis are abbreviated as * or -> *) |
|
55 |
||
56 |
(*Weakening one function type to another; see also Pi_type*) |
|
57 |
lemma fun_weaken_type: "[| f: A->B; B<=D |] ==> f: A->D" |
|
58 |
by (unfold Pi_def, best) |
|
59 |
||
13355 | 60 |
subsection{*Function Application*} |
13163 | 61 |
|
62 |
lemma apply_equality2: "[| <a,b>: f; <a,c>: f; f: Pi(A,B) |] ==> b=c" |
|
63 |
by (unfold Pi_def function_def, blast) |
|
64 |
||
65 |
lemma function_apply_equality: "[| <a,b>: f; function(f) |] ==> f`a = b" |
|
66 |
by (unfold apply_def function_def, blast) |
|
67 |
||
68 |
lemma apply_equality: "[| <a,b>: f; f: Pi(A,B) |] ==> f`a = b" |
|
69 |
apply (unfold Pi_def) |
|
70 |
apply (blast intro: function_apply_equality) |
|
71 |
done |
|
72 |
||
73 |
(*Applying a function outside its domain yields 0*) |
|
74 |
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
|
75 |
by (unfold apply_def, blast) |
13163 | 76 |
|
77 |
lemma Pi_memberD: "[| f: Pi(A,B); c: f |] ==> EX x:A. c = <x,f`x>" |
|
78 |
apply (frule fun_is_rel) |
|
79 |
apply (blast dest: apply_equality) |
|
80 |
done |
|
81 |
||
82 |
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
|
83 |
apply (simp add: function_def, clarify) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
84 |
apply (subgoal_tac "f`a = y", blast) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
85 |
apply (simp add: apply_def, blast) |
13163 | 86 |
done |
87 |
||
88 |
lemma apply_Pair: "[| f: Pi(A,B); a:A |] ==> <a,f`a>: f" |
|
89 |
apply (simp add: Pi_iff) |
|
90 |
apply (blast intro: function_apply_Pair) |
|
91 |
done |
|
92 |
||
93 |
(*Conclusion is flexible -- use res_inst_tac or else apply_funtype below!*) |
|
94 |
lemma apply_type [TC]: "[| f: Pi(A,B); a:A |] ==> f`a : B(a)" |
|
95 |
by (blast intro: apply_Pair dest: fun_is_rel) |
|
96 |
||
97 |
(*This version is acceptable to the simplifier*) |
|
98 |
lemma apply_funtype: "[| f: A->B; a:A |] ==> f`a : B" |
|
99 |
by (blast dest: apply_type) |
|
100 |
||
101 |
lemma apply_iff: "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b" |
|
102 |
apply (frule fun_is_rel) |
|
103 |
apply (blast intro!: apply_Pair apply_equality) |
|
104 |
done |
|
105 |
||
106 |
(*Refining one Pi type to another*) |
|
107 |
lemma Pi_type: "[| f: Pi(A,C); !!x. x:A ==> f`x : B(x) |] ==> f : Pi(A,B)" |
|
108 |
apply (simp only: Pi_iff) |
|
109 |
apply (blast dest: function_apply_equality) |
|
110 |
done |
|
111 |
||
112 |
(*Such functions arise in non-standard datatypes, ZF/ex/Ntree for instance*) |
|
113 |
lemma Pi_Collect_iff: |
|
114 |
"(f : Pi(A, %x. {y:B(x). P(x,y)})) |
|
115 |
<-> f : Pi(A,B) & (ALL x: A. P(x, f`x))" |
|
116 |
by (blast intro: Pi_type dest: apply_type) |
|
117 |
||
118 |
lemma Pi_weaken_type: |
|
119 |
"[| f : Pi(A,B); !!x. x:A ==> B(x)<=C(x) |] ==> f : Pi(A,C)" |
|
120 |
by (blast intro: Pi_type dest: apply_type) |
|
121 |
||
122 |
||
123 |
(** Elimination of membership in a function **) |
|
124 |
||
125 |
lemma domain_type: "[| <a,b> : f; f: Pi(A,B) |] ==> a : A" |
|
126 |
by (blast dest: fun_is_rel) |
|
127 |
||
128 |
lemma range_type: "[| <a,b> : f; f: Pi(A,B) |] ==> b : B(a)" |
|
129 |
by (blast dest: fun_is_rel) |
|
130 |
||
131 |
lemma Pair_mem_PiD: "[| <a,b>: f; f: Pi(A,B) |] ==> a:A & b:B(a) & f`a = b" |
|
132 |
by (blast intro: domain_type range_type apply_equality) |
|
133 |
||
13355 | 134 |
subsection{*Lambda Abstraction*} |
13163 | 135 |
|
136 |
lemma lamI: "a:A ==> <a,b(a)> : (lam x:A. b(x))" |
|
137 |
apply (unfold lam_def) |
|
138 |
apply (erule RepFunI) |
|
139 |
done |
|
140 |
||
141 |
lemma lamE: |
|
142 |
"[| p: (lam x:A. b(x)); !!x.[| x:A; p=<x,b(x)> |] ==> P |
|
143 |
|] ==> P" |
|
144 |
by (simp add: lam_def, blast) |
|
145 |
||
146 |
lemma lamD: "[| <a,c>: (lam x:A. b(x)) |] ==> c = b(a)" |
|
147 |
by (simp add: lam_def) |
|
148 |
||
149 |
lemma lam_type [TC]: |
|
150 |
"[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B)" |
|
151 |
by (simp add: lam_def Pi_def function_def, blast) |
|
152 |
||
153 |
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
|
154 |
by (blast intro: lam_type) |
13163 | 155 |
|
13172 | 156 |
lemma function_lam: "function (lam x:A. b(x))" |
157 |
by (simp add: function_def lam_def) |
|
158 |
||
159 |
lemma relation_lam: "relation (lam x:A. b(x))" |
|
160 |
by (simp add: relation_def lam_def) |
|
161 |
||
13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13174
diff
changeset
|
162 |
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
|
163 |
by (simp add: apply_def lam_def, blast) |
13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13174
diff
changeset
|
164 |
|
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13174
diff
changeset
|
165 |
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
|
166 |
by (simp add: apply_def lam_def, blast) |
13163 | 167 |
|
168 |
lemma lam_empty [simp]: "(lam x:0. b(x)) = 0" |
|
169 |
by (simp add: lam_def) |
|
170 |
||
171 |
lemma domain_lam [simp]: "domain(Lambda(A,b)) = A" |
|
172 |
by (simp add: lam_def, blast) |
|
173 |
||
174 |
(*congruence rule for lambda abstraction*) |
|
175 |
lemma lam_cong [cong]: |
|
176 |
"[| A=A'; !!x. x:A' ==> b(x)=b'(x) |] ==> Lambda(A,b) = Lambda(A',b')" |
|
177 |
by (simp only: lam_def cong add: RepFun_cong) |
|
178 |
||
179 |
lemma lam_theI: |
|
180 |
"(!!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
|
181 |
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
|
182 |
apply simp |
13163 | 183 |
apply (blast intro: theI) |
184 |
done |
|
185 |
||
186 |
lemma lam_eqE: "[| (lam x:A. f(x)) = (lam x:A. g(x)); a:A |] ==> f(a)=g(a)" |
|
187 |
by (fast intro!: lamI elim: equalityE lamE) |
|
188 |
||
189 |
||
190 |
(*Empty function spaces*) |
|
191 |
lemma Pi_empty1 [simp]: "Pi(0,A) = {0}" |
|
192 |
by (unfold Pi_def function_def, blast) |
|
193 |
||
194 |
(*The singleton function*) |
|
195 |
lemma singleton_fun [simp]: "{<a,b>} : {a} -> {b}" |
|
196 |
by (unfold Pi_def function_def, blast) |
|
197 |
||
198 |
lemma Pi_empty2 [simp]: "(A->0) = (if A=0 then {0} else 0)" |
|
199 |
by (unfold Pi_def function_def, force) |
|
200 |
||
201 |
lemma fun_space_empty_iff [iff]: "(A->X)=0 \<longleftrightarrow> X=0 & (A \<noteq> 0)" |
|
202 |
apply auto |
|
203 |
apply (fast intro!: equals0I intro: lam_type) |
|
204 |
done |
|
205 |
||
206 |
||
13355 | 207 |
subsection{*Extensionality*} |
13163 | 208 |
|
209 |
(*Semi-extensionality!*) |
|
210 |
||
211 |
lemma fun_subset: |
|
212 |
"[| f : Pi(A,B); g: Pi(C,D); A<=C; |
|
213 |
!!x. x:A ==> f`x = g`x |] ==> f<=g" |
|
214 |
by (force dest: Pi_memberD intro: apply_Pair) |
|
215 |
||
216 |
lemma fun_extension: |
|
217 |
"[| f : Pi(A,B); g: Pi(A,D); |
|
218 |
!!x. x:A ==> f`x = g`x |] ==> f=g" |
|
219 |
by (blast del: subsetI intro: subset_refl sym fun_subset) |
|
220 |
||
221 |
lemma eta [simp]: "f : Pi(A,B) ==> (lam x:A. f`x) = f" |
|
222 |
apply (rule fun_extension) |
|
223 |
apply (auto simp add: lam_type apply_type beta) |
|
224 |
done |
|
225 |
||
226 |
lemma fun_extension_iff: |
|
227 |
"[| f:Pi(A,B); g:Pi(A,C) |] ==> (ALL a:A. f`a = g`a) <-> f=g" |
|
228 |
by (blast intro: fun_extension) |
|
229 |
||
230 |
(*thm by Mark Staples, proof by lcp*) |
|
231 |
lemma fun_subset_eq: "[| f:Pi(A,B); g:Pi(A,C) |] ==> f <= g <-> (f = g)" |
|
232 |
by (blast dest: apply_Pair |
|
233 |
intro: fun_extension apply_equality [symmetric]) |
|
234 |
||
235 |
||
236 |
(*Every element of Pi(A,B) may be expressed as a lambda abstraction!*) |
|
237 |
lemma Pi_lamE: |
|
238 |
assumes major: "f: Pi(A,B)" |
|
239 |
and minor: "!!b. [| ALL x:A. b(x):B(x); f = (lam x:A. b(x)) |] ==> P" |
|
240 |
shows "P" |
|
241 |
apply (rule minor) |
|
242 |
apply (rule_tac [2] eta [symmetric]) |
|
243 |
apply (blast intro: major apply_type)+ |
|
244 |
done |
|
245 |
||
246 |
||
13355 | 247 |
subsection{*Images of Functions*} |
13163 | 248 |
|
249 |
lemma image_lam: "C <= A ==> (lam x:A. b(x)) `` C = {b(x). x:C}" |
|
250 |
by (unfold lam_def, blast) |
|
251 |
||
13179 | 252 |
lemma Repfun_function_if: |
253 |
"function(f) |
|
254 |
==> {f`x. x:C} = (if C <= domain(f) then f``C else cons(0,f``C))"; |
|
255 |
apply simp |
|
256 |
apply (intro conjI impI) |
|
257 |
apply (blast dest: function_apply_equality intro: function_apply_Pair) |
|
258 |
apply (rule equalityI) |
|
259 |
apply (blast intro!: function_apply_Pair apply_0) |
|
260 |
apply (blast dest: function_apply_equality intro: apply_0 [symmetric]) |
|
261 |
done |
|
262 |
||
263 |
(*For this lemma and the next, the right-hand side could equivalently |
|
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13357
diff
changeset
|
264 |
be written \<Union>x\<in>C. {f`x} *) |
13174 | 265 |
lemma image_function: |
266 |
"[| function(f); C <= domain(f) |] ==> f``C = {f`x. x:C}"; |
|
13179 | 267 |
by (simp add: Repfun_function_if) |
13174 | 268 |
|
13163 | 269 |
lemma image_fun: "[| f : Pi(A,B); C <= A |] ==> f``C = {f`x. x:C}" |
13174 | 270 |
apply (simp add: Pi_iff) |
271 |
apply (blast intro: image_function) |
|
13163 | 272 |
done |
273 |
||
14883 | 274 |
lemma image_eq_UN: |
275 |
assumes f: "f \<in> Pi(A,B)" "C \<subseteq> A" shows "f``C = (\<Union>x\<in>C. {f ` x})" |
|
276 |
by (auto simp add: image_fun [OF f]) |
|
277 |
||
13163 | 278 |
lemma Pi_image_cons: |
279 |
"[| f: Pi(A,B); x: A |] ==> f `` cons(x,y) = cons(f`x, f``y)" |
|
280 |
by (blast dest: apply_equality apply_Pair) |
|
281 |
||
124 | 282 |
|
13355 | 283 |
subsection{*Properties of @{term "restrict(f,A)"}*} |
13163 | 284 |
|
13179 | 285 |
lemma restrict_subset: "restrict(f,A) <= f" |
286 |
by (unfold restrict_def, blast) |
|
13163 | 287 |
|
288 |
lemma function_restrictI: |
|
289 |
"function(f) ==> function(restrict(f,A))" |
|
290 |
by (unfold restrict_def function_def, blast) |
|
291 |
||
292 |
lemma restrict_type2: "[| f: Pi(C,B); A<=C |] ==> restrict(f,A) : Pi(A,B)" |
|
293 |
by (simp add: Pi_iff function_def restrict_def, blast) |
|
294 |
||
13179 | 295 |
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
|
296 |
by (simp add: apply_def restrict_def, blast) |
13163 | 297 |
|
298 |
lemma restrict_empty [simp]: "restrict(f,0) = 0" |
|
13179 | 299 |
by (unfold restrict_def, simp) |
13163 | 300 |
|
13172 | 301 |
lemma restrict_iff: "z \<in> restrict(r,A) \<longleftrightarrow> z \<in> r & (\<exists>x\<in>A. \<exists>y. z = \<langle>x, y\<rangle>)" |
302 |
by (simp add: restrict_def) |
|
303 |
||
13163 | 304 |
lemma restrict_restrict [simp]: |
305 |
"restrict(restrict(r,A),B) = restrict(r, A Int B)" |
|
306 |
by (unfold restrict_def, blast) |
|
307 |
||
308 |
lemma domain_restrict [simp]: "domain(restrict(f,C)) = domain(f) Int C" |
|
309 |
apply (unfold restrict_def) |
|
310 |
apply (auto simp add: domain_def) |
|
311 |
done |
|
312 |
||
13248 | 313 |
lemma restrict_idem: "f <= Sigma(A,B) ==> restrict(f,A) = f" |
13163 | 314 |
by (simp add: restrict_def, blast) |
315 |
||
13248 | 316 |
|
317 |
(*converse probably holds too*) |
|
318 |
lemma domain_restrict_idem: |
|
319 |
"[| domain(r) <= A; relation(r) |] ==> restrict(r,A) = r" |
|
320 |
by (simp add: restrict_def relation_def, blast) |
|
321 |
||
322 |
lemma domain_restrict_lam [simp]: "domain(restrict(Lambda(A,f),C)) = A Int C" |
|
323 |
apply (unfold restrict_def lam_def) |
|
324 |
apply (rule equalityI) |
|
325 |
apply (auto simp add: domain_iff) |
|
326 |
done |
|
327 |
||
13163 | 328 |
lemma restrict_if [simp]: "restrict(f,A) ` a = (if a : A then f`a else 0)" |
329 |
by (simp add: restrict apply_0) |
|
330 |
||
331 |
lemma restrict_lam_eq: |
|
332 |
"A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))" |
|
333 |
by (unfold restrict_def lam_def, auto) |
|
334 |
||
335 |
lemma fun_cons_restrict_eq: |
|
336 |
"f : cons(a, b) -> B ==> f = cons(<a, f ` a>, restrict(f, b))" |
|
337 |
apply (rule equalityI) |
|
13248 | 338 |
prefer 2 apply (blast intro: apply_Pair restrict_subset [THEN subsetD]) |
13163 | 339 |
apply (auto dest!: Pi_memberD simp add: restrict_def lam_def) |
340 |
done |
|
341 |
||
342 |
||
13355 | 343 |
subsection{*Unions of Functions*} |
13163 | 344 |
|
345 |
(** The Union of a set of COMPATIBLE functions is a function **) |
|
346 |
||
347 |
lemma function_Union: |
|
348 |
"[| ALL x:S. function(x); |
|
349 |
ALL x:S. ALL y:S. x<=y | y<=x |] |
|
350 |
==> function(Union(S))" |
|
351 |
by (unfold function_def, blast) |
|
352 |
||
353 |
lemma fun_Union: |
|
354 |
"[| ALL f:S. EX C D. f:C->D; |
|
355 |
ALL f:S. ALL y:S. f<=y | y<=f |] ==> |
|
356 |
Union(S) : domain(Union(S)) -> range(Union(S))" |
|
357 |
apply (unfold Pi_def) |
|
358 |
apply (blast intro!: rel_Union function_Union) |
|
359 |
done |
|
360 |
||
13174 | 361 |
lemma gen_relation_Union [rule_format]: |
362 |
"\<forall>f\<in>F. relation(f) \<Longrightarrow> relation(Union(F))" |
|
363 |
by (simp add: relation_def) |
|
364 |
||
13163 | 365 |
|
366 |
(** The Union of 2 disjoint functions is a function **) |
|
367 |
||
368 |
lemmas Un_rls = Un_subset_iff SUM_Un_distrib1 prod_Un_distrib2 |
|
369 |
subset_trans [OF _ Un_upper1] |
|
370 |
subset_trans [OF _ Un_upper2] |
|
371 |
||
372 |
lemma fun_disjoint_Un: |
|
373 |
"[| f: A->B; g: C->D; A Int C = 0 |] |
|
374 |
==> (f Un g) : (A Un C) -> (B Un D)" |
|
375 |
(*Prove the product and domain subgoals using distributive laws*) |
|
376 |
apply (simp add: Pi_iff extension Un_rls) |
|
377 |
apply (unfold function_def, blast) |
|
378 |
done |
|
379 |
||
13179 | 380 |
lemma fun_disjoint_apply1: "a \<notin> domain(g) ==> (f Un g)`a = f`a" |
381 |
by (simp add: apply_def, blast) |
|
13163 | 382 |
|
13179 | 383 |
lemma fun_disjoint_apply2: "c \<notin> domain(f) ==> (f Un g)`c = g`c" |
384 |
by (simp add: apply_def, blast) |
|
13163 | 385 |
|
13355 | 386 |
subsection{*Domain and Range of a Function or Relation*} |
13163 | 387 |
|
388 |
lemma domain_of_fun: "f : Pi(A,B) ==> domain(f)=A" |
|
389 |
by (unfold Pi_def, blast) |
|
390 |
||
391 |
lemma apply_rangeI: "[| f : Pi(A,B); a: A |] ==> f`a : range(f)" |
|
392 |
by (erule apply_Pair [THEN rangeI], assumption) |
|
393 |
||
394 |
lemma range_of_fun: "f : Pi(A,B) ==> f : A->range(f)" |
|
395 |
by (blast intro: Pi_type apply_rangeI) |
|
396 |
||
13355 | 397 |
subsection{*Extensions of Functions*} |
13163 | 398 |
|
399 |
lemma fun_extend: |
|
400 |
"[| f: A->B; c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)" |
|
401 |
apply (frule singleton_fun [THEN fun_disjoint_Un], blast) |
|
402 |
apply (simp add: cons_eq) |
|
403 |
done |
|
404 |
||
405 |
lemma fun_extend3: |
|
406 |
"[| f: A->B; c~:A; b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B" |
|
407 |
by (blast intro: fun_extend [THEN fun_weaken_type]) |
|
408 |
||
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
409 |
lemma extend_apply: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
410 |
"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
|
411 |
by (auto simp add: apply_def) |
13163 | 412 |
|
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
413 |
lemma fun_extend_apply [simp]: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
414 |
"[| 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
|
415 |
apply (rule extend_apply) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
416 |
apply (simp add: Pi_def, blast) |
13163 | 417 |
done |
418 |
||
419 |
lemmas singleton_apply = apply_equality [OF singletonI singleton_fun, simp] |
|
420 |
||
421 |
(*For Finite.ML. Inclusion of right into left is easy*) |
|
422 |
lemma cons_fun_eq: |
|
13269 | 423 |
"c ~: A ==> cons(c,A) -> B = (\<Union>f \<in> A->B. \<Union>b\<in>B. {cons(<c,b>, f)})" |
13163 | 424 |
apply (rule equalityI) |
425 |
apply (safe elim!: fun_extend3) |
|
426 |
(*Inclusion of left into right*) |
|
427 |
apply (subgoal_tac "restrict (x, A) : A -> B") |
|
428 |
prefer 2 apply (blast intro: restrict_type2) |
|
429 |
apply (rule UN_I, assumption) |
|
430 |
apply (rule apply_funtype [THEN UN_I]) |
|
431 |
apply assumption |
|
432 |
apply (rule consI1) |
|
433 |
apply (simp (no_asm)) |
|
434 |
apply (rule fun_extension) |
|
435 |
apply assumption |
|
436 |
apply (blast intro: fun_extend) |
|
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
437 |
apply (erule consE, simp_all) |
13163 | 438 |
done |
439 |
||
13269 | 440 |
lemma succ_fun_eq: "succ(n) -> B = (\<Union>f \<in> n->B. \<Union>b\<in>B. {cons(<n,b>, f)})" |
441 |
by (simp add: succ_def mem_not_refl cons_fun_eq) |
|
442 |
||
13355 | 443 |
|
444 |
subsection{*Function Updates*} |
|
445 |
||
446 |
constdefs |
|
447 |
update :: "[i,i,i] => i" |
|
448 |
"update(f,a,b) == lam x: cons(a, domain(f)). if(x=a, b, f`x)" |
|
449 |
||
450 |
nonterminals |
|
451 |
updbinds updbind |
|
452 |
||
453 |
syntax |
|
454 |
||
455 |
(* Let expressions *) |
|
456 |
||
457 |
"_updbind" :: "[i, i] => updbind" ("(2_ :=/ _)") |
|
458 |
"" :: "updbind => updbinds" ("_") |
|
459 |
"_updbinds" :: "[updbind, updbinds] => updbinds" ("_,/ _") |
|
460 |
"_Update" :: "[i, updbinds] => i" ("_/'((_)')" [900,0] 900) |
|
461 |
||
462 |
translations |
|
463 |
"_Update (f, _updbinds(b,bs))" == "_Update (_Update(f,b), bs)" |
|
464 |
"f(x:=y)" == "update(f,x,y)" |
|
465 |
||
466 |
||
467 |
lemma update_apply [simp]: "f(x:=y) ` z = (if z=x then y else f`z)" |
|
468 |
apply (simp add: update_def) |
|
14153 | 469 |
apply (case_tac "z \<in> domain(f)") |
13355 | 470 |
apply (simp_all add: apply_0) |
471 |
done |
|
472 |
||
473 |
lemma update_idem: "[| f`x = y; f: Pi(A,B); x: A |] ==> f(x:=y) = f" |
|
474 |
apply (unfold update_def) |
|
475 |
apply (simp add: domain_of_fun cons_absorb) |
|
476 |
apply (rule fun_extension) |
|
477 |
apply (best intro: apply_type if_type lam_type, assumption, simp) |
|
478 |
done |
|
479 |
||
480 |
||
481 |
(* [| f: Pi(A, B); x:A |] ==> f(x := f`x) = f *) |
|
482 |
declare refl [THEN update_idem, simp] |
|
483 |
||
484 |
lemma domain_update [simp]: "domain(f(x:=y)) = cons(x, domain(f))" |
|
485 |
by (unfold update_def, simp) |
|
486 |
||
14046 | 487 |
lemma update_type: "[| f:Pi(A,B); x : A; y: B(x) |] ==> f(x:=y) : Pi(A, B)" |
13355 | 488 |
apply (unfold update_def) |
489 |
apply (simp add: domain_of_fun cons_absorb apply_funtype lam_type) |
|
490 |
done |
|
491 |
||
492 |
||
13357 | 493 |
subsection{*Monotonicity Theorems*} |
494 |
||
495 |
subsubsection{*Replacement in its Various Forms*} |
|
496 |
||
497 |
(*Not easy to express monotonicity in P, since any "bigger" predicate |
|
498 |
would have to be single-valued*) |
|
499 |
lemma Replace_mono: "A<=B ==> Replace(A,P) <= Replace(B,P)" |
|
500 |
by (blast elim!: ReplaceE) |
|
501 |
||
502 |
lemma RepFun_mono: "A<=B ==> {f(x). x:A} <= {f(x). x:B}" |
|
503 |
by blast |
|
504 |
||
505 |
lemma Pow_mono: "A<=B ==> Pow(A) <= Pow(B)" |
|
506 |
by blast |
|
507 |
||
508 |
lemma Union_mono: "A<=B ==> Union(A) <= Union(B)" |
|
509 |
by blast |
|
510 |
||
511 |
lemma UN_mono: |
|
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13357
diff
changeset
|
512 |
"[| A<=C; !!x. x:A ==> B(x)<=D(x) |] ==> (\<Union>x\<in>A. B(x)) <= (\<Union>x\<in>C. D(x))" |
13357 | 513 |
by blast |
514 |
||
515 |
(*Intersection is ANTI-monotonic. There are TWO premises! *) |
|
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14046
diff
changeset
|
516 |
lemma Inter_anti_mono: "[| A<=B; A\<noteq>0 |] ==> Inter(B) <= Inter(A)" |
13357 | 517 |
by blast |
518 |
||
519 |
lemma cons_mono: "C<=D ==> cons(a,C) <= cons(a,D)" |
|
520 |
by blast |
|
521 |
||
522 |
lemma Un_mono: "[| A<=C; B<=D |] ==> A Un B <= C Un D" |
|
523 |
by blast |
|
524 |
||
525 |
lemma Int_mono: "[| A<=C; B<=D |] ==> A Int B <= C Int D" |
|
526 |
by blast |
|
527 |
||
528 |
lemma Diff_mono: "[| A<=C; D<=B |] ==> A-B <= C-D" |
|
529 |
by blast |
|
530 |
||
531 |
subsubsection{*Standard Products, Sums and Function Spaces *} |
|
532 |
||
533 |
lemma Sigma_mono [rule_format]: |
|
534 |
"[| A<=C; !!x. x:A --> B(x) <= D(x) |] ==> Sigma(A,B) <= Sigma(C,D)" |
|
535 |
by blast |
|
536 |
||
537 |
lemma sum_mono: "[| A<=C; B<=D |] ==> A+B <= C+D" |
|
538 |
by (unfold sum_def, blast) |
|
539 |
||
540 |
(*Note that B->A and C->A are typically disjoint!*) |
|
541 |
lemma Pi_mono: "B<=C ==> A->B <= A->C" |
|
542 |
by (blast intro: lam_type elim: Pi_lamE) |
|
543 |
||
544 |
lemma lam_mono: "A<=B ==> Lambda(A,c) <= Lambda(B,c)" |
|
545 |
apply (unfold lam_def) |
|
546 |
apply (erule RepFun_mono) |
|
547 |
done |
|
548 |
||
549 |
subsubsection{*Converse, Domain, Range, Field*} |
|
550 |
||
551 |
lemma converse_mono: "r<=s ==> converse(r) <= converse(s)" |
|
552 |
by blast |
|
553 |
||
554 |
lemma domain_mono: "r<=s ==> domain(r)<=domain(s)" |
|
555 |
by blast |
|
556 |
||
557 |
lemmas domain_rel_subset = subset_trans [OF domain_mono domain_subset] |
|
558 |
||
559 |
lemma range_mono: "r<=s ==> range(r)<=range(s)" |
|
560 |
by blast |
|
561 |
||
562 |
lemmas range_rel_subset = subset_trans [OF range_mono range_subset] |
|
563 |
||
564 |
lemma field_mono: "r<=s ==> field(r)<=field(s)" |
|
565 |
by blast |
|
566 |
||
567 |
lemma field_rel_subset: "r <= A*A ==> field(r) <= A" |
|
568 |
by (erule field_mono [THEN subset_trans], blast) |
|
569 |
||
570 |
||
571 |
subsubsection{*Images*} |
|
572 |
||
573 |
lemma image_pair_mono: |
|
574 |
"[| !! x y. <x,y>:r ==> <x,y>:s; A<=B |] ==> r``A <= s``B" |
|
575 |
by blast |
|
576 |
||
577 |
lemma vimage_pair_mono: |
|
578 |
"[| !! x y. <x,y>:r ==> <x,y>:s; A<=B |] ==> r-``A <= s-``B" |
|
579 |
by blast |
|
580 |
||
581 |
lemma image_mono: "[| r<=s; A<=B |] ==> r``A <= s``B" |
|
582 |
by blast |
|
583 |
||
584 |
lemma vimage_mono: "[| r<=s; A<=B |] ==> r-``A <= s-``B" |
|
585 |
by blast |
|
586 |
||
587 |
lemma Collect_mono: |
|
588 |
"[| A<=B; !!x. x:A ==> P(x) --> Q(x) |] ==> Collect(A,P) <= Collect(B,Q)" |
|
589 |
by blast |
|
590 |
||
591 |
(*Used in intr_elim.ML and in individual datatype definitions*) |
|
592 |
lemmas basic_monos = subset_refl imp_refl disj_mono conj_mono ex_mono |
|
593 |
Collect_mono Part_mono in_mono |
|
594 |
||
13163 | 595 |
ML |
596 |
{* |
|
597 |
val Pi_iff = thm "Pi_iff"; |
|
598 |
val Pi_iff_old = thm "Pi_iff_old"; |
|
599 |
val fun_is_function = thm "fun_is_function"; |
|
600 |
val fun_is_rel = thm "fun_is_rel"; |
|
601 |
val Pi_cong = thm "Pi_cong"; |
|
602 |
val fun_weaken_type = thm "fun_weaken_type"; |
|
603 |
val apply_equality2 = thm "apply_equality2"; |
|
604 |
val function_apply_equality = thm "function_apply_equality"; |
|
605 |
val apply_equality = thm "apply_equality"; |
|
606 |
val apply_0 = thm "apply_0"; |
|
607 |
val Pi_memberD = thm "Pi_memberD"; |
|
608 |
val function_apply_Pair = thm "function_apply_Pair"; |
|
609 |
val apply_Pair = thm "apply_Pair"; |
|
610 |
val apply_type = thm "apply_type"; |
|
611 |
val apply_funtype = thm "apply_funtype"; |
|
612 |
val apply_iff = thm "apply_iff"; |
|
613 |
val Pi_type = thm "Pi_type"; |
|
614 |
val Pi_Collect_iff = thm "Pi_Collect_iff"; |
|
615 |
val Pi_weaken_type = thm "Pi_weaken_type"; |
|
616 |
val domain_type = thm "domain_type"; |
|
617 |
val range_type = thm "range_type"; |
|
618 |
val Pair_mem_PiD = thm "Pair_mem_PiD"; |
|
619 |
val lamI = thm "lamI"; |
|
620 |
val lamE = thm "lamE"; |
|
621 |
val lamD = thm "lamD"; |
|
622 |
val lam_type = thm "lam_type"; |
|
623 |
val lam_funtype = thm "lam_funtype"; |
|
624 |
val beta = thm "beta"; |
|
625 |
val lam_empty = thm "lam_empty"; |
|
626 |
val domain_lam = thm "domain_lam"; |
|
627 |
val lam_cong = thm "lam_cong"; |
|
628 |
val lam_theI = thm "lam_theI"; |
|
629 |
val lam_eqE = thm "lam_eqE"; |
|
630 |
val Pi_empty1 = thm "Pi_empty1"; |
|
631 |
val singleton_fun = thm "singleton_fun"; |
|
632 |
val Pi_empty2 = thm "Pi_empty2"; |
|
633 |
val fun_space_empty_iff = thm "fun_space_empty_iff"; |
|
634 |
val fun_subset = thm "fun_subset"; |
|
635 |
val fun_extension = thm "fun_extension"; |
|
636 |
val eta = thm "eta"; |
|
637 |
val fun_extension_iff = thm "fun_extension_iff"; |
|
638 |
val fun_subset_eq = thm "fun_subset_eq"; |
|
639 |
val Pi_lamE = thm "Pi_lamE"; |
|
640 |
val image_lam = thm "image_lam"; |
|
641 |
val image_fun = thm "image_fun"; |
|
642 |
val Pi_image_cons = thm "Pi_image_cons"; |
|
643 |
val restrict_subset = thm "restrict_subset"; |
|
644 |
val function_restrictI = thm "function_restrictI"; |
|
645 |
val restrict_type2 = thm "restrict_type2"; |
|
646 |
val restrict = thm "restrict"; |
|
647 |
val restrict_empty = thm "restrict_empty"; |
|
648 |
val domain_restrict_lam = thm "domain_restrict_lam"; |
|
649 |
val restrict_restrict = thm "restrict_restrict"; |
|
650 |
val domain_restrict = thm "domain_restrict"; |
|
651 |
val restrict_idem = thm "restrict_idem"; |
|
652 |
val restrict_if = thm "restrict_if"; |
|
653 |
val restrict_lam_eq = thm "restrict_lam_eq"; |
|
654 |
val fun_cons_restrict_eq = thm "fun_cons_restrict_eq"; |
|
655 |
val function_Union = thm "function_Union"; |
|
656 |
val fun_Union = thm "fun_Union"; |
|
657 |
val fun_disjoint_Un = thm "fun_disjoint_Un"; |
|
658 |
val fun_disjoint_apply1 = thm "fun_disjoint_apply1"; |
|
659 |
val fun_disjoint_apply2 = thm "fun_disjoint_apply2"; |
|
660 |
val domain_of_fun = thm "domain_of_fun"; |
|
661 |
val apply_rangeI = thm "apply_rangeI"; |
|
662 |
val range_of_fun = thm "range_of_fun"; |
|
663 |
val fun_extend = thm "fun_extend"; |
|
664 |
val fun_extend3 = thm "fun_extend3"; |
|
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13175
diff
changeset
|
665 |
val fun_extend_apply = thm "fun_extend_apply"; |
13163 | 666 |
val singleton_apply = thm "singleton_apply"; |
667 |
val cons_fun_eq = thm "cons_fun_eq"; |
|
13355 | 668 |
|
669 |
val update_def = thm "update_def"; |
|
670 |
val update_apply = thm "update_apply"; |
|
671 |
val update_idem = thm "update_idem"; |
|
672 |
val domain_update = thm "domain_update"; |
|
673 |
val update_type = thm "update_type"; |
|
13357 | 674 |
|
675 |
val Replace_mono = thm "Replace_mono"; |
|
676 |
val RepFun_mono = thm "RepFun_mono"; |
|
677 |
val Pow_mono = thm "Pow_mono"; |
|
678 |
val Union_mono = thm "Union_mono"; |
|
679 |
val UN_mono = thm "UN_mono"; |
|
680 |
val Inter_anti_mono = thm "Inter_anti_mono"; |
|
681 |
val cons_mono = thm "cons_mono"; |
|
682 |
val Un_mono = thm "Un_mono"; |
|
683 |
val Int_mono = thm "Int_mono"; |
|
684 |
val Diff_mono = thm "Diff_mono"; |
|
685 |
val Sigma_mono = thm "Sigma_mono"; |
|
686 |
val sum_mono = thm "sum_mono"; |
|
687 |
val Pi_mono = thm "Pi_mono"; |
|
688 |
val lam_mono = thm "lam_mono"; |
|
689 |
val converse_mono = thm "converse_mono"; |
|
690 |
val domain_mono = thm "domain_mono"; |
|
691 |
val domain_rel_subset = thm "domain_rel_subset"; |
|
692 |
val range_mono = thm "range_mono"; |
|
693 |
val range_rel_subset = thm "range_rel_subset"; |
|
694 |
val field_mono = thm "field_mono"; |
|
695 |
val field_rel_subset = thm "field_rel_subset"; |
|
696 |
val image_pair_mono = thm "image_pair_mono"; |
|
697 |
val vimage_pair_mono = thm "vimage_pair_mono"; |
|
698 |
val image_mono = thm "image_mono"; |
|
699 |
val vimage_mono = thm "vimage_mono"; |
|
700 |
val Collect_mono = thm "Collect_mono"; |
|
701 |
||
702 |
val basic_monos = thms "basic_monos"; |
|
13163 | 703 |
*} |
704 |
||
705 |
end |