1139804Simp(* Title: ZF/func.thy 21541Srgrimes Author: Lawrence C Paulson, Cambridge University Computer Laboratory 31541Srgrimes Copyright 1991 University of Cambridge 41541Srgrimes*) 51541Srgrimes 61541Srgrimessection\<open>Functions, Function Spaces, Lambda-Abstraction\<close> 71541Srgrimes 81541Srgrimestheory func imports equalities Sum begin 91541Srgrimes 101541Srgrimessubsection\<open>The Pi Operator: Dependent Function Space\<close> 111541Srgrimes 121541Srgrimeslemma subset_Sigma_imp_relation: "r \<subseteq> Sigma(A,B) ==> relation(r)" 131541Srgrimesby (simp add: relation_def, blast) 141541Srgrimes 151541Srgrimeslemma relation_converse_converse [simp]: 161541Srgrimes "relation(r) ==> converse(converse(r)) = r" 171541Srgrimesby (simp add: relation_def, blast) 181541Srgrimes 191541Srgrimeslemma relation_restrict [simp]: "relation(restrict(r,A))" 201541Srgrimesby (simp add: restrict_def relation_def, blast) 211541Srgrimes 221541Srgrimeslemma Pi_iff: 231541Srgrimes "f \<in> Pi(A,B) \<longleftrightarrow> function(f) & f<=Sigma(A,B) & A<=domain(f)" 241541Srgrimesby (unfold Pi_def, blast) 251541Srgrimes 261541Srgrimes(*For upward compatibility with the former definition*) 271541Srgrimeslemma Pi_iff_old: 281541Srgrimes "f \<in> Pi(A,B) \<longleftrightarrow> f<=Sigma(A,B) & (\<forall>x\<in>A. \<exists>!y. <x,y>: f)" 2922521Sdysonby (unfold Pi_def function_def, blast) 3050477Speter 311541Srgrimeslemma fun_is_function: "f \<in> Pi(A,B) ==> function(f)" 3222521Sdysonby (simp only: Pi_iff) 3322521Sdyson 34159082Sddslemma function_imp_Pi: 35159082Sdds "[|function(f); relation(f)|] ==> f \<in> domain(f) -> range(f)" 36159082Sddsby (simp add: Pi_iff relation_def, blast) 37159082Sdds 38159082Sddslemma functionI: 39159082Sdds "[| !!x y y'. [| <x,y>:r; <x,y'>:r |] ==> y=y' |] ==> function(r)" 4022521Sdysonby (simp add: function_def, blast) 4122521Sdyson 4254444Seivind(*Functions are relations*) 4354444Seivindlemma fun_is_rel: "f \<in> Pi(A,B) ==> f \<subseteq> Sigma(A,B)" 4454444Seivindby (unfold Pi_def, blast) 4554444Seivind 4654444Seivindlemma Pi_cong: 4745058Seivind "[| A=A'; !!x. x \<in> A' ==> B(x)=B'(x) |] ==> Pi(A,B) = Pi(A',B')" 4822521Sdysonby (simp add: Pi_def cong add: Sigma_cong) 4922521Sdyson 5022521Sdyson(*Sigma_cong, Pi_cong NOT given to Addcongs: they cause 5122521Sdyson flex-flex pairs and the "Check your prover" error. Most 52116615Sse Sigmas and Pis are abbreviated as * or -> *) 53229728Sjhb 54116615Sse(*Weakening one function type to another; see also Pi_type*) 55159082Sddslemma fun_weaken_type: "[| f \<in> A->B; B<=D |] ==> f \<in> A->D" 56159082Sddsby (unfold Pi_def, best) 57159082Sdds 58116615Ssesubsection\<open>Function Application\<close> 59116615Sse 60116615Sselemma apply_equality2: "[| <a,b>: f; <a,c>: f; f \<in> Pi(A,B) |] ==> b=c" 6122521Sdysonby (unfold Pi_def function_def, blast) 6251679Seivind 6351679Seivindlemma function_apply_equality: "[| <a,b>: f; function(f) |] ==> f`a = b" 6451679Seivindby (unfold apply_def function_def, blast) 6551679Seivind 66159082Sddslemma apply_equality: "[| <a,b>: f; f \<in> Pi(A,B) |] ==> f`a = b" 67159082Sddsapply (unfold Pi_def) 68159082Sddsapply (blast intro: function_apply_equality) 69159082Sddsdone 70159082Sdds 7122521Sdyson(*Applying a function outside its domain yields 0*) 7222521Sdysonlemma apply_0: "a \<notin> domain(f) ==> f`a = 0" 7322521Sdysonby (unfold apply_def, blast) 74159082Sdds 751541Srgrimeslemma Pi_memberD: "[| f \<in> Pi(A,B); c \<in> f |] ==> \<exists>x\<in>A. c = <x,f`x>" 761541Srgrimesapply (frule fun_is_rel) 771541Srgrimesapply (blast dest: apply_equality) 781541Srgrimesdone 791541Srgrimes 801541Srgrimeslemma function_apply_Pair: "[| function(f); a \<in> domain(f)|] ==> <a,f`a>: f" 81159082Sddsapply (simp add: function_def, clarify) 82159082Sddsapply (subgoal_tac "f`a = y", blast) 83159082Sddsapply (simp add: apply_def, blast) 8428732Sphkdone 85159082Sdds 8628732Sphklemma apply_Pair: "[| f \<in> Pi(A,B); a \<in> A |] ==> <a,f`a>: f" 8728732Sphkapply (simp add: Pi_iff) 8828732Sphkapply (blast intro: function_apply_Pair) 8928732Sphkdone 9028732Sphk 9128732Sphk(*Conclusion is flexible -- use rule_tac or else apply_funtype below!*) 92159082Sddslemma apply_type [TC]: "[| f \<in> Pi(A,B); a \<in> A |] ==> f`a \<in> B(a)" 93159082Sddsby (blast intro: apply_Pair dest: fun_is_rel) 94159082Sdds 95159082Sdds(*This version is acceptable to the simplifier*) 961541Srgrimeslemma apply_funtype: "[| f \<in> A->B; a \<in> A |] ==> f`a \<in> B" 9735823Smsmithby (blast dest: apply_type) 981541Srgrimes 991541Srgrimeslemma apply_iff: "f \<in> Pi(A,B) ==> <a,b>: f \<longleftrightarrow> a \<in> A & f`a = b" 1001541Srgrimesapply (frule fun_is_rel) 1011541Srgrimesapply (blast intro!: apply_Pair apply_equality) 1021541Srgrimesdone 103159082Sdds 104159082Sdds(*Refining one Pi type to another*) 105159082Sddslemma Pi_type: "[| f \<in> Pi(A,C); !!x. x \<in> A ==> f`x \<in> B(x) |] ==> f \<in> Pi(A,B)" 10622521Sdysonapply (simp only: Pi_iff) 10735823Smsmithapply (blast dest: function_apply_equality) 10822521Sdysondone 10922521Sdyson 11022521Sdyson(*Such functions arise in non-standard datatypes, ZF/ex/Ntree for instance*) 11122521Sdysonlemma Pi_Collect_iff: 112159082Sdds "(f \<in> Pi(A, %x. {y \<in> B(x). P(x,y)})) 113159082Sdds \<longleftrightarrow> f \<in> Pi(A,B) & (\<forall>x\<in>A. P(x, f`x))" 114159082Sddsby (blast intro: Pi_type dest: apply_type) 115159082Sdds 116159082Sddslemma Pi_weaken_type: 1171541Srgrimes "[| f \<in> Pi(A,B); !!x. x \<in> A ==> B(x)<=C(x) |] ==> f \<in> Pi(A,C)" 11835823Smsmithby (blast intro: Pi_type dest: apply_type) 11953101Seivind 1201541Srgrimes 1211541Srgrimes(** Elimination of membership in a function **) 1221541Srgrimes 1231541Srgrimeslemma domain_type: "[| <a,b> \<in> f; f \<in> Pi(A,B) |] ==> a \<in> A" 124159082Sddsby (blast dest: fun_is_rel) 125159082Sdds 126159082Sddslemma range_type: "[| <a,b> \<in> f; f \<in> Pi(A,B) |] ==> b \<in> B(a)" 1271541Srgrimesby (blast dest: fun_is_rel) 1281541Srgrimes 1291541Srgrimeslemma Pair_mem_PiD: "[| <a,b>: f; f \<in> Pi(A,B) |] ==> a \<in> A & b \<in> B(a) & f`a = b" 1301541Srgrimesby (blast intro: domain_type range_type apply_equality) 13183366Sjulian 132170152Skibsubsection\<open>Lambda Abstraction\<close> 1331541Srgrimes 1341541Srgrimeslemma lamI: "a \<in> A ==> <a,b(a)> \<in> (\<lambda>x\<in>A. b(x))" 135159082Sddsapply (unfold lam_def) 136189696Sjhbapply (erule RepFunI) 137159082Sddsdone 1381541Srgrimes 1391541Srgrimeslemma lamE: 1401541Srgrimes "[| p: (\<lambda>x\<in>A. b(x)); !!x.[| x \<in> A; p=<x,b(x)> |] ==> P 1411541Srgrimes |] ==> P" 14283366Sjulianby (simp add: lam_def, blast) 1431541Srgrimes 1441541Srgrimeslemma lamD: "[| <a,c>: (\<lambda>x\<in>A. b(x)) |] ==> c = b(a)" 145159082Sddsby (simp add: lam_def) 146159082Sdds 147159082Sddslemma lam_type [TC]: 1481541Srgrimes "[| !!x. x \<in> A ==> b(x): B(x) |] ==> (\<lambda>x\<in>A. b(x)) \<in> Pi(A,B)" 1491541Srgrimesby (simp add: lam_def Pi_def function_def, blast) 150184413Strasz 1511541Srgrimeslemma lam_funtype: "(\<lambda>x\<in>A. b(x)) \<in> A -> {b(x). x \<in> A}" 15283366Sjulianby (blast intro: lam_type) 1531541Srgrimes 1541541Srgrimeslemma function_lam: "function (\<lambda>x\<in>A. b(x))" 155159082Sddsby (simp add: function_def lam_def) 156193092Strasz 157193092Straszlemma relation_lam: "relation (\<lambda>x\<in>A. b(x))" 158193092Straszby (simp add: relation_def lam_def) 159193092Strasz 160193092Straszlemma beta_if [simp]: "(\<lambda>x\<in>A. b(x)) ` a = (if a \<in> A then b(a) else 0)" 161193092Straszby (simp add: apply_def lam_def, blast) 162193092Strasz 163193092Straszlemma beta: "a \<in> A ==> (\<lambda>x\<in>A. b(x)) ` a = b(a)" 164193092Straszby (simp add: apply_def lam_def, blast) 165193092Strasz 166159082Sddslemma lam_empty [simp]: "(\<lambda>x\<in>0. b(x)) = 0" 167159082Sddsby (simp add: lam_def) 1681541Srgrimes 1691541Srgrimeslemma domain_lam [simp]: "domain(Lambda(A,b)) = A" 17054803Srwatsonby (simp add: lam_def, blast) 1711541Srgrimes 1721541Srgrimes(*congruence rule for lambda abstraction*) 1731541Srgrimeslemma lam_cong [cong]: 174159082Sdds "[| A=A'; !!x. x \<in> A' ==> b(x)=b'(x) |] ==> Lambda(A,b) = Lambda(A',b')" 175159082Sddsby (simp only: lam_def cong add: RepFun_cong) 176159082Sdds 177159082Sddslemma lam_theI: 1781541Srgrimes "(!!x. x \<in> A ==> \<exists>!y. Q(x,y)) ==> \<exists>f. \<forall>x\<in>A. Q(x, f`x)" 1791541Srgrimesapply (rule_tac x = "\<lambda>x\<in>A. THE y. Q (x,y)" in exI) 1801541Srgrimesapply simp 1811541Srgrimesapply (blast intro: theI) 1821541Srgrimesdone 1831541Srgrimes 184187526Sjhblemma lam_eqE: "[| (\<lambda>x\<in>A. f(x)) = (\<lambda>x\<in>A. g(x)); a \<in> A |] ==> f(a)=g(a)" 185159082Sddsby (fast intro!: lamI elim: equalityE lamE) 186187526Sjhb 187187526Sjhb 188187526Sjhb(*Empty function spaces*) 189187526Sjhblemma Pi_empty1 [simp]: "Pi(0,A) = {0}" 190159082Sddsby (unfold Pi_def function_def, blast) 191159082Sdds 1921541Srgrimes(*The singleton function*) 1931541Srgrimeslemma singleton_fun [simp]: "{<a,b>} \<in> {a} -> {b}" 1941541Srgrimesby (unfold Pi_def function_def, blast) 1951541Srgrimes 1961541Srgrimeslemma Pi_empty2 [simp]: "(A->0) = (if A=0 then {0} else 0)" 1971541Srgrimesby (unfold Pi_def function_def, force) 1981541Srgrimes 199159082Sddslemma fun_space_empty_iff [iff]: "(A->X)=0 \<longleftrightarrow> X=0 & (A \<noteq> 0)" 200193762Spsapply auto 201159082Sddsapply (fast intro!: equals0I intro: lam_type) 202159082Sddsdone 203159082Sdds 2041541Srgrimes 2051541Srgrimessubsection\<open>Extensionality\<close> 2061541Srgrimes 2071541Srgrimes(*Semi-extensionality!*) 2081541Srgrimes 2091541Srgrimeslemma fun_subset: 2101541Srgrimes "[| f \<in> Pi(A,B); g \<in> Pi(C,D); A<=C; 211159082Sdds !!x. x \<in> A ==> f`x = g`x |] ==> f<=g" 212159082Sddsby (force dest: Pi_memberD intro: apply_Pair) 213159082Sdds 2141541Srgrimeslemma fun_extension: 2151541Srgrimes "[| f \<in> Pi(A,B); g \<in> Pi(A,D); 21622521Sdyson !!x. x \<in> A ==> f`x = g`x |] ==> f=g" 217153400Sdesby (blast del: subsetI intro: subset_refl sym fun_subset) 2181541Srgrimes 2191541Srgrimeslemma eta [simp]: "f \<in> Pi(A,B) ==> (\<lambda>x\<in>A. f`x) = f" 22083366Sjulianapply (rule fun_extension) 2211541Srgrimesapply (auto simp add: lam_type apply_type beta) 2221541Srgrimesdone 223159082Sdds 224184377Sjhblemma fun_extension_iff: 225159082Sdds "[| f \<in> Pi(A,B); g \<in> Pi(A,C) |] ==> (\<forall>a\<in>A. f`a = g`a) \<longleftrightarrow> f=g" 22629353Speterby (blast intro: fun_extension) 2271541Srgrimes 22829353Speter(*thm by Mark Staples, proof by lcp*) 2291541Srgrimeslemma fun_subset_eq: "[| f \<in> Pi(A,B); g \<in> Pi(A,C) |] ==> f \<subseteq> g \<longleftrightarrow> (f = g)" 23083366Sjulianby (blast dest: apply_Pair 2311541Srgrimes intro: fun_extension apply_equality [symmetric]) 2321541Srgrimes 233159082Sdds 234159082Sdds(*Every element of Pi(A,B) may be expressed as a lambda abstraction!*) 235159082Sddslemma Pi_lamE: 23672521Sjlemon assumes major: "f \<in> Pi(A,B)" 23772521Sjlemon and minor: "!!b. [| \<forall>x\<in>A. b(x):B(x); f = (\<lambda>x\<in>A. b(x)) |] ==> P" 23872521Sjlemon shows "P" 23972521Sjlemonapply (rule minor) 24072521Sjlemonapply (rule_tac [2] eta [symmetric]) 241159082Sddsapply (blast intro: major apply_type)+ 242159082Sddsdone 243159082Sdds 24422521Sdyson 24522521Sdysonsubsection\<open>Images of Functions\<close> 24622521Sdyson 24722521Sdysonlemma image_lam: "C \<subseteq> A ==> (\<lambda>x\<in>A. b(x)) `` C = {b(x). x \<in> C}" 24822521Sdysonby (unfold lam_def, blast) 249159082Sdds 250194019Spslemma Repfun_function_if: 251159082Sdds "function(f) 2521541Srgrimes ==> {f`x. x \<in> C} = (if C \<subseteq> domain(f) then f``C else cons(0,f``C))" 2531541Srgrimesapply simp 2541541Srgrimesapply (intro conjI impI) 25583366Sjulian apply (blast dest: function_apply_equality intro: function_apply_Pair) 2561541Srgrimesapply (rule equalityI) 2571541Srgrimes apply (blast intro!: function_apply_Pair apply_0) 258159082Sddsapply (blast dest: function_apply_equality intro: apply_0 [symmetric]) 259159082Sddsdone 260159082Sdds 261159082Sdds(*For this lemma and the next, the right-hand side could equivalently 262159082Sdds be written \<Union>x\<in>C. {f`x} *) 2631541Srgrimeslemma image_function: 26435823Smsmith "[| function(f); C \<subseteq> domain(f) |] ==> f``C = {f`x. x \<in> C}" 26535823Smsmithby (simp add: Repfun_function_if) 2661541Srgrimes 2671541Srgrimeslemma image_fun: "[| f \<in> Pi(A,B); C \<subseteq> A |] ==> f``C = {f`x. x \<in> C}" 2681541Srgrimesapply (simp add: Pi_iff) 269159082Sddsapply (blast intro: image_function) 270159082Sddsdone 271159082Sdds 272159082Sddslemma image_eq_UN: 273159082Sdds assumes f: "f \<in> Pi(A,B)" "C \<subseteq> A" shows "f``C = (\<Union>x\<in>C. {f ` x})" 2749842Sdgby (auto simp add: image_fun [OF f]) 27535823Smsmith 2769842Sdglemma Pi_image_cons: 2779842Sdg "[| f \<in> Pi(A,B); x \<in> A |] ==> f `` cons(x,y) = cons(f`x, f``y)" 2789842Sdgby (blast dest: apply_equality apply_Pair) 2791541Srgrimes 280159082Sdds 281159082Sddssubsection\<open>Properties of \<^term>\<open>restrict(f,A)\<close>\<close> 282159082Sdds 283159082Sddslemma restrict_subset: "restrict(f,A) \<subseteq> f" 2841541Srgrimesby (unfold restrict_def, blast) 2851541Srgrimes 2861541Srgrimeslemma function_restrictI: 2871541Srgrimes "function(f) ==> function(restrict(f,A))" 2881541Srgrimesby (unfold restrict_def function_def, blast) 2891541Srgrimes 2901541Srgrimeslemma restrict_type2: "[| f \<in> Pi(C,B); A<=C |] ==> restrict(f,A) \<in> Pi(A,B)" 2911541Srgrimesby (simp add: Pi_iff function_def restrict_def, blast) 2921541Srgrimes 293159082Sddslemma restrict: "restrict(f,A) ` a = (if a \<in> A then f`a else 0)" 294159082Sddsby (simp add: apply_def restrict_def, blast) 295159082Sdds 296159082Sddslemma restrict_empty [simp]: "restrict(f,0) = 0" 297159082Sddsby (unfold restrict_def, simp) 2981541Srgrimes 29935823Smsmithlemma restrict_iff: "z \<in> restrict(r,A) \<longleftrightarrow> z \<in> r & (\<exists>x\<in>A. \<exists>y. z = \<langle>x, y\<rangle>)" 3001541Srgrimesby (simp add: restrict_def) 3011541Srgrimes 3021541Srgrimeslemma restrict_restrict [simp]: 3031541Srgrimes "restrict(restrict(r,A),B) = restrict(r, A \<inter> B)" 3041541Srgrimesby (unfold restrict_def, blast) 305159082Sdds 306159082Sddslemma domain_restrict [simp]: "domain(restrict(f,C)) = domain(f) \<inter> C" 307159082Sddsapply (unfold restrict_def) 308159082Sddsapply (auto simp add: domain_def) 309159082Sddsdone 3101541Srgrimes 31135823Smsmithlemma restrict_idem: "f \<subseteq> Sigma(A,B) ==> restrict(f,A) = f" 31235823Smsmithby (simp add: restrict_def, blast) 3131541Srgrimes 3141541Srgrimes 3151541Srgrimes(*converse probably holds too*) 316159082Sddslemma domain_restrict_idem: 317159082Sdds "[| domain(r) \<subseteq> A; relation(r) |] ==> restrict(r,A) = r" 318159082Sddsby (simp add: restrict_def relation_def, blast) 319159082Sdds 320159082Sddslemma domain_restrict_lam [simp]: "domain(restrict(Lambda(A,f),C)) = A \<inter> C" 3211541Srgrimesapply (unfold restrict_def lam_def) 32235823Smsmithapply (rule equalityI) 32353131Seivindapply (auto simp add: domain_iff) 3241541Srgrimesdone 3251541Srgrimes 3261541Srgrimeslemma restrict_if [simp]: "restrict(f,A) ` a = (if a \<in> A then f`a else 0)" 3271541Srgrimesby (simp add: restrict apply_0) 3281541Srgrimes 329159082Sddslemma restrict_lam_eq: 330159082Sdds "A<=C ==> restrict(\<lambda>x\<in>C. b(x), A) = (\<lambda>x\<in>A. b(x))" 331159082Sddsby (unfold restrict_def lam_def, auto) 3321541Srgrimes 3331541Srgrimeslemma fun_cons_restrict_eq: 3341541Srgrimes "f \<in> cons(a, b) -> B ==> f = cons(<a, f ` a>, restrict(f, b))" 3351541Srgrimesapply (rule equalityI) 3363167Sdfr prefer 2 apply (blast intro: apply_Pair restrict_subset [THEN subsetD]) 33722521Sdysonapply (auto dest!: Pi_memberD simp add: restrict_def lam_def) 33822521Sdysondone 3391541Srgrimes 3401541Srgrimes 341159082Sddssubsection\<open>Unions of Functions\<close> 342159082Sdds 343159082Sdds(** The Union of a set of COMPATIBLE functions is a function **) 3441541Srgrimes 3451541Srgrimeslemma function_Union: 3461541Srgrimes "[| \<forall>x\<in>S. function(x); 3471541Srgrimes \<forall>x\<in>S. \<forall>y\<in>S. x<=y | y<=x |] 3481541Srgrimes ==> function(\<Union>(S))" 3491541Srgrimesby (unfold function_def, blast) 350159082Sdds 351159082Sddslemma fun_Union: 352159082Sdds "[| \<forall>f\<in>S. \<exists>C D. f \<in> C->D; 3531541Srgrimes \<forall>f\<in>S. \<forall>y\<in>S. f<=y | y<=f |] ==> 3541541Srgrimes \<Union>(S) \<in> domain(\<Union>(S)) -> range(\<Union>(S))" 35583366Sjulianapply (unfold Pi_def) 3561541Srgrimesapply (blast intro!: rel_Union function_Union) 3571541Srgrimesdone 358159082Sdds 359159082Sddslemma gen_relation_Union: 360159082Sdds "(\<And>f. f\<in>F \<Longrightarrow> relation(f)) \<Longrightarrow> relation(\<Union>(F))" 3611541Srgrimesby (simp add: relation_def) 3621541Srgrimes 36383366Sjulian 3641541Srgrimes(** The Union of 2 disjoint functions is a function **) 3651541Srgrimes 366159082Sddslemmas Un_rls = Un_subset_iff SUM_Un_distrib1 prod_Un_distrib2 367169671Skib subset_trans [OF _ Un_upper1] 368169671Skib subset_trans [OF _ Un_upper2] 369159082Sdds 370169671Skiblemma fun_disjoint_Un: 3711541Srgrimes "[| f \<in> A->B; g \<in> C->D; A \<inter> C = 0 |] 37222521Sdyson ==> (f \<union> g) \<in> (A \<union> C) -> (B \<union> D)" 373164248Skmacy(*Prove the product and domain subgoals using distributive laws*) 374164248Skmacyapply (simp add: Pi_iff extension Un_rls) 3751541Srgrimesapply (unfold function_def, blast) 3761541Srgrimesdone 377159082Sdds 378159082Sddslemma fun_disjoint_apply1: "a \<notin> domain(g) ==> (f \<union> g)`a = f`a" 379159082Sddsby (simp add: apply_def, blast) 380159082Sdds 3811541Srgrimeslemma fun_disjoint_apply2: "c \<notin> domain(f) ==> (f \<union> g)`c = g`c" 3821541Srgrimesby (simp add: apply_def, blast) 38322521Sdyson 3841541Srgrimessubsection\<open>Domain and Range of a Function or Relation\<close> 3851541Srgrimes 386159082Sddslemma domain_of_fun: "f \<in> Pi(A,B) ==> domain(f)=A" 387159082Sddsby (unfold Pi_def, blast) 388159082Sdds 3891541Srgrimeslemma apply_rangeI: "[| f \<in> Pi(A,B); a \<in> A |] ==> f`a \<in> range(f)" 3901541Srgrimesby (erule apply_Pair [THEN rangeI], assumption) 39196572Sphk 392137726Sphklemma range_of_fun: "f \<in> Pi(A,B) ==> f \<in> A->range(f)" 39396572Sphkby (blast intro: Pi_type apply_rangeI) 3941541Srgrimes 39510551Sdysonsubsection\<open>Extensions of Functions\<close> 3961541Srgrimes 3971541Srgrimeslemma fun_extend: 398159082Sdds "[| f \<in> A->B; c\<notin>A |] ==> cons(<c,b>,f) \<in> cons(c,A) -> cons(b,B)" 399159082Sddsapply (frule singleton_fun [THEN fun_disjoint_Un], blast) 400159082Sddsapply (simp add: cons_eq) 401159082Sddsdone 40237384Sjulian 40337384Sjulianlemma fun_extend3: 40437384Sjulian "[| f \<in> A->B; c\<notin>A; b \<in> B |] ==> cons(<c,b>,f) \<in> cons(c,A) -> B" 40537384Sjulianby (blast intro: fun_extend [THEN fun_weaken_type]) 4061541Srgrimes 407159082Sddslemma extend_apply: 408159082Sdds "c \<notin> domain(f) ==> cons(<c,b>,f)`a = (if a=c then b else f`a)" 409159082Sddsby (auto simp add: apply_def) 41062976Smckusick 41162976Smckusicklemma fun_extend_apply [simp]: 41262976Smckusick "[| f \<in> A->B; c\<notin>A |] ==> cons(<c,b>,f)`a = (if a=c then b else f`a)" 41362976Smckusickapply (rule extend_apply) 41462976Smckusickapply (simp add: Pi_def, blast) 415159082Sddsdone 416176590Skib 417159082Sddslemmas singleton_apply = apply_equality [OF singletonI singleton_fun, simp] 4181541Srgrimes 4191541Srgrimes(*For Finite.ML. Inclusion of right into left is easy*) 4201541Srgrimeslemma cons_fun_eq: 4211541Srgrimes "c \<notin> A ==> cons(c,A) -> B = (\<Union>f \<in> A->B. \<Union>b\<in>B. {cons(<c,b>, f)})" 422159082Sddsapply (rule equalityI) 423159082Sddsapply (safe elim!: fun_extend3) 424159082Sdds(*Inclusion of left into right*) 4251541Srgrimesapply (subgoal_tac "restrict (x, A) \<in> A -> B") 4261541Srgrimes prefer 2 apply (blast intro: restrict_type2) 4271541Srgrimesapply (rule UN_I, assumption) 42822521Sdysonapply (rule apply_funtype [THEN UN_I]) 4291541Srgrimes apply assumption 4301541Srgrimes apply (rule consI1) 431159082Sddsapply (simp (no_asm)) 432159082Sddsapply (rule fun_extension) 433159082Sdds apply assumption 4341541Srgrimes apply (blast intro: fun_extend) 4351541Srgrimesapply (erule consE, simp_all) 436153400Sdesdone 4371541Srgrimes 4381541Srgrimeslemma succ_fun_eq: "succ(n) -> B = (\<Union>f \<in> n->B. \<Union>b\<in>B. {cons(<n,b>, f)})" 4391541Srgrimesby (simp add: succ_def mem_not_refl cons_fun_eq) 4401541Srgrimes 4411541Srgrimes 442159082Sddssubsection\<open>Function Updates\<close> 443177633Sdfr 444177633Sdfrdefinition 445177633Sdfr update :: "[i,i,i] => i" where 446177633Sdfr "update(f,a,b) == \<lambda>x\<in>cons(a, domain(f)). if(x=a, b, f`x)" 447177633Sdfr 448177633Sdfrnonterminal updbinds and updbind 449177633Sdfr 450177633Sdfrsyntax 451177633Sdfr 452177633Sdfr (* Let expressions *) 453177633Sdfr 454177633Sdfr "_updbind" :: "[i, i] => updbind" (\<open>(2_ :=/ _)\<close>) 455177633Sdfr "" :: "updbind => updbinds" (\<open>_\<close>) 456208003Szml "_updbinds" :: "[updbind, updbinds] => updbinds" (\<open>_,/ _\<close>) 457208003Szml "_Update" :: "[i, updbinds] => i" (\<open>_/'((_)')\<close> [900,0] 900) 458208003Szml 459208003Szmltranslations 460208003Szml "_Update (f, _updbinds(b,bs))" == "_Update (_Update(f,b), bs)" 461208003Szml "f(x:=y)" == "CONST update(f,x,y)" 462208003Szml 463159082Sdds 464159082Sddslemma update_apply [simp]: "f(x:=y) ` z = (if z=x then y else f`z)" 4651541Srgrimesapply (simp add: update_def) 4661541Srgrimesapply (case_tac "z \<in> domain(f)") 4671541Srgrimesapply (simp_all add: apply_0) 4681541Srgrimesdone 4691541Srgrimes 470159082Sddslemma update_idem: "[| f`x = y; f \<in> Pi(A,B); x \<in> A |] ==> f(x:=y) = f" 471159082Sddsapply (unfold update_def) 472159082Sddsapply (simp add: domain_of_fun cons_absorb) 47310551Sdysonapply (rule fun_extension) 47410551Sdysonapply (best intro: apply_type if_type lam_type, assumption, simp) 47510551Sdysondone 47610551Sdyson 47710551Sdyson 47812767Sdyson(* [| f \<in> Pi(A, B); x \<in> A |] ==> f(x := f`x) = f *) 47910551Sdysondeclare refl [THEN update_idem, simp] 48010551Sdyson 481159082Sddslemma domain_update [simp]: "domain(f(x:=y)) = cons(x, domain(f))" 482159082Sddsby (unfold update_def, simp) 483159082Sdds 48410551Sdysonlemma update_type: "[| f \<in> Pi(A,B); x \<in> A; y \<in> B(x) |] ==> f(x:=y) \<in> Pi(A, B)" 48510551Sdysonapply (unfold update_def) 48610551Sdysonapply (simp add: domain_of_fun cons_absorb apply_funtype lam_type) 48710551Sdysondone 48810551Sdyson 48910551Sdyson 49012767Sdysonsubsection\<open>Monotonicity Theorems\<close> 49110551Sdyson 49211704Sdysonsubsubsection\<open>Replacement in its Various Forms\<close> 493159082Sdds 494159082Sdds(*Not easy to express monotonicity in P, since any "bigger" predicate 495159082Sdds would have to be single-valued*) 49654803Srwatsonlemma Replace_mono: "A<=B ==> Replace(A,P) \<subseteq> Replace(B,P)" 49754803Srwatsonby (blast elim!: ReplaceE) 49854803Srwatson 49954803Srwatsonlemma RepFun_mono: "A<=B ==> {f(x). x \<in> A} \<subseteq> {f(x). x \<in> B}" 50054803Srwatsonby blast 50183366Sjulian 50254803Srwatsonlemma Pow_mono: "A<=B ==> Pow(A) \<subseteq> Pow(B)" 50354803Srwatsonby blast 504159082Sdds 505159082Sddslemma Union_mono: "A<=B ==> \<Union>(A) \<subseteq> \<Union>(B)" 506159082Sddsby blast 50754803Srwatson 50854803Srwatsonlemma UN_mono: 50954803Srwatson "[| A<=C; !!x. x \<in> A ==> B(x)<=D(x) |] ==> (\<Union>x\<in>A. B(x)) \<subseteq> (\<Union>x\<in>C. D(x))" 51054803Srwatsonby blast 51154803Srwatson 51283366Sjulian(*Intersection is ANTI-monotonic. There are TWO premises! *) 51354803Srwatsonlemma Inter_anti_mono: "[| A<=B; A\<noteq>0 |] ==> \<Inter>(B) \<subseteq> \<Inter>(A)" 51454803Srwatsonby blast 515159082Sdds 516159082Sddslemma cons_mono: "C<=D ==> cons(a,C) \<subseteq> cons(a,D)" 517159082Sddsby blast 51854803Srwatson 51954803Srwatsonlemma Un_mono: "[| A<=C; B<=D |] ==> A \<union> B \<subseteq> C \<union> D" 52054803Srwatsonby blast 52154803Srwatson 52254803Srwatsonlemma Int_mono: "[| A<=C; B<=D |] ==> A \<inter> B \<subseteq> C \<inter> D" 52383366Sjulianby blast 52454803Srwatson 52554803Srwatsonlemma Diff_mono: "[| A<=C; D<=B |] ==> A-B \<subseteq> C-D" 526159082Sddsby blast 527159082Sdds 528159082Sddssubsubsection\<open>Standard Products, Sums and Function Spaces\<close> 529102990Sphk 530102990Sphklemma Sigma_mono [rule_format]: 531102990Sphk "[| A<=C; !!x. x \<in> A \<longrightarrow> B(x) \<subseteq> D(x) |] ==> Sigma(A,B) \<subseteq> Sigma(C,D)" 532102990Sphkby blast 533102990Sphk 534102990Sphklemma sum_mono: "[| A<=C; B<=D |] ==> A+B \<subseteq> C+D" 535102990Sphkby (unfold sum_def, blast) 536159082Sdds 537159082Sdds(*Note that B->A and C->A are typically disjoint!*) 538159082Sddslemma Pi_mono: "B<=C ==> A->B \<subseteq> A->C" 53954803Srwatsonby (blast intro: lam_type elim: Pi_lamE) 54054803Srwatson 54174437Srwatsonlemma lam_mono: "A<=B ==> Lambda(A,c) \<subseteq> Lambda(B,c)" 54265119Srwatsonapply (unfold lam_def) 54354803Srwatsonapply (erule RepFun_mono) 54490448Srwatsondone 54554803Srwatson 54683366Sjuliansubsubsection\<open>Converse, Domain, Range, Field\<close> 54754803Srwatson 54854803Srwatsonlemma converse_mono: "r<=s ==> converse(r) \<subseteq> converse(s)" 549159082Sddsby blast 550159082Sdds 551159082Sddslemma domain_mono: "r<=s ==> domain(r)<=domain(s)" 552115867Srwatsonby blast 553115867Srwatson 554115867Srwatsonlemmas domain_rel_subset = subset_trans [OF domain_mono domain_subset] 555115867Srwatson 556115867Srwatsonlemma range_mono: "r<=s ==> range(r)<=range(s)" 557115867Srwatsonby blast 558115867Srwatson 559115867Srwatsonlemmas range_rel_subset = subset_trans [OF range_mono range_subset] 560115867Srwatson 561159082Sddslemma field_mono: "r<=s ==> field(r)<=field(s)" 562159082Sddsby blast 563159082Sdds 564102990Sphklemma field_rel_subset: "r \<subseteq> A*A ==> field(r) \<subseteq> A" 565102990Sphkby (erule field_mono [THEN subset_trans], blast) 566102990Sphk 567102990Sphk 568102990Sphksubsubsection\<open>Images\<close> 569102990Sphk 570159082Sddslemma image_pair_mono: 571159082Sdds "[| !! x y. <x,y>:r ==> <x,y>:s; A<=B |] ==> r``A \<subseteq> s``B" 572228849Sjhbby blast 573159082Sdds 574118131Srwatsonlemma vimage_pair_mono: 575116698Srwatson "[| !! x y. <x,y>:r ==> <x,y>:s; A<=B |] ==> r-``A \<subseteq> s-``B" 576116698Srwatsonby blast 577116698Srwatson 578116698Srwatsonlemma image_mono: "[| r<=s; A<=B |] ==> r``A \<subseteq> s``B" 579116698Srwatsonby blast 580116698Srwatson 581116698Srwatsonlemma vimage_mono: "[| r<=s; A<=B |] ==> r-``A \<subseteq> s-``B" 582159082Sddsby blast 583159082Sdds 584228849Sjhblemma Collect_mono: 585159082Sdds "[| A<=B; !!x. x \<in> A ==> P(x) \<longrightarrow> Q(x) |] ==> Collect(A,P) \<subseteq> Collect(B,Q)" 58654803Srwatsonby blast 58754803Srwatson 58874437Srwatson(*Used in intr_elim.ML and in individual datatype definitions*) 58965119Srwatsonlemmas basic_monos = subset_refl imp_refl disj_mono conj_mono ex_mono 59054803Srwatson Collect_mono Part_mono in_mono 59154803Srwatson 59283366Sjulian(* Useful with simp; contributed by Clemens Ballarin. *) 59354803Srwatson 59465770Sbplemma bex_image_simp: 595159082Sdds "[| f \<in> Pi(X, Y); A \<subseteq> X |] ==> (\<exists>x\<in>f``A. P(x)) \<longleftrightarrow> (\<exists>x\<in>A. P(f`x))" 596159082Sdds apply safe 597159082Sdds apply rule 598100984Srwatson prefer 2 apply assumption 599100984Srwatson apply (simp add: apply_equality) 600100984Srwatson apply (blast intro: apply_Pair) 601100984Srwatson done 602100984Srwatson 603100984Srwatsonlemma ball_image_simp: 604166774Spjd "[| f \<in> Pi(X, Y); A \<subseteq> X |] ==> (\<forall>x\<in>f``A. P(x)) \<longleftrightarrow> (\<forall>x\<in>A. P(f`x))" 605166774Spjd apply safe 606184377Sjhb apply (blast intro: apply_Pair) 607166774Spjd apply (drule bspec) apply assumption 608166774Spjd apply (simp add: apply_equality) 609166774Spjd done 610166774Spjd 611166774Spjdend 612185956Smarcus