author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46953  2b6e55924af3 
child 58860  fee7cfa69c50 
permissions  rwrr 
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, LambdaAbstraction*} 
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 
flexflex 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 nonstandard 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 
(*Semiextensionality!*) 

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 tabwidth;
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 righthand 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 singlevalued*) 

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 ANTImonotonic. 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 ] ==> AB \<subseteq> CD" 
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 