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