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