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