src/ZF/func.thy
author paulson
Wed Jun 19 09:03:34 2002 +0200 (2002-06-19)
changeset 13221 e29378f347e4
parent 13219 7e44aa8a276e
child 13248 ae66c22ed52e
permissions -rw-r--r--
conversion of Cardinal, CardinalArith
     1 (*  Title:      ZF/func.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 
     6 Functions in Zermelo-Fraenkel Set Theory
     7 *)
     8 
     9 theory func = equalities:
    10 
    11 lemma relation_converse_converse [simp]:
    12      "relation(r) ==> converse(converse(r)) = r"
    13 by (simp add: relation_def, blast) 
    14 
    15 lemma relation_restrict [simp]:  "relation(restrict(r,A))"
    16 by (simp add: restrict_def relation_def, blast) 
    17 
    18 (*** The Pi operator -- dependent function space ***)
    19 
    20 lemma Pi_iff:
    21     "f: Pi(A,B) <-> function(f) & f<=Sigma(A,B) & A<=domain(f)"
    22 by (unfold Pi_def, blast)
    23 
    24 (*For upward compatibility with the former definition*)
    25 lemma Pi_iff_old:
    26     "f: Pi(A,B) <-> f<=Sigma(A,B) & (ALL x:A. EX! y. <x,y>: f)"
    27 by (unfold Pi_def function_def, blast)
    28 
    29 lemma fun_is_function: "f: Pi(A,B) ==> function(f)"
    30 by (simp only: Pi_iff)
    31 
    32 lemma function_imp_Pi:
    33      "[|function(f); relation(f)|] ==> f \<in> domain(f) -> range(f)"
    34 by (simp add: Pi_iff relation_def, blast) 
    35 
    36 lemma functionI: 
    37      "[| !!x y y'. [| <x,y>:r; <x,y'>:r |] ==> y=y' |] ==> function(r)"
    38 by (simp add: function_def, blast) 
    39 
    40 (*Functions are relations*)
    41 lemma fun_is_rel: "f: Pi(A,B) ==> f <= Sigma(A,B)"
    42 by (unfold Pi_def, blast)
    43 
    44 lemma Pi_cong:
    45     "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> Pi(A,B) = Pi(A',B')"
    46 by (simp add: Pi_def cong add: Sigma_cong)
    47 
    48 (*Sigma_cong, Pi_cong NOT given to Addcongs: they cause
    49   flex-flex pairs and the "Check your prover" error.  Most
    50   Sigmas and Pis are abbreviated as * or -> *)
    51 
    52 (*Weakening one function type to another; see also Pi_type*)
    53 lemma fun_weaken_type: "[| f: A->B;  B<=D |] ==> f: A->D"
    54 by (unfold Pi_def, best)
    55 
    56 (*** Function Application ***)
    57 
    58 lemma apply_equality2: "[| <a,b>: f;  <a,c>: f;  f: Pi(A,B) |] ==> b=c"
    59 by (unfold Pi_def function_def, blast)
    60 
    61 lemma function_apply_equality: "[| <a,b>: f;  function(f) |] ==> f`a = b"
    62 by (unfold apply_def function_def, blast)
    63 
    64 lemma apply_equality: "[| <a,b>: f;  f: Pi(A,B) |] ==> f`a = b"
    65 apply (unfold Pi_def)
    66 apply (blast intro: function_apply_equality)
    67 done
    68 
    69 (*Applying a function outside its domain yields 0*)
    70 lemma apply_0: "a ~: domain(f) ==> f`a = 0"
    71 by (unfold apply_def, blast)
    72 
    73 lemma Pi_memberD: "[| f: Pi(A,B);  c: f |] ==> EX x:A.  c = <x,f`x>"
    74 apply (frule fun_is_rel)
    75 apply (blast dest: apply_equality)
    76 done
    77 
    78 lemma function_apply_Pair: "[| function(f);  a : domain(f)|] ==> <a,f`a>: f"
    79 apply (simp add: function_def, clarify) 
    80 apply (subgoal_tac "f`a = y", blast) 
    81 apply (simp add: apply_def, blast) 
    82 done
    83 
    84 lemma apply_Pair: "[| f: Pi(A,B);  a:A |] ==> <a,f`a>: f"
    85 apply (simp add: Pi_iff)
    86 apply (blast intro: function_apply_Pair)
    87 done
    88 
    89 (*Conclusion is flexible -- use res_inst_tac or else apply_funtype below!*)
    90 lemma apply_type [TC]: "[| f: Pi(A,B);  a:A |] ==> f`a : B(a)"
    91 by (blast intro: apply_Pair dest: fun_is_rel)
    92 
    93 (*This version is acceptable to the simplifier*)
    94 lemma apply_funtype: "[| f: A->B;  a:A |] ==> f`a : B"
    95 by (blast dest: apply_type)
    96 
    97 lemma apply_iff: "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b"
    98 apply (frule fun_is_rel)
    99 apply (blast intro!: apply_Pair apply_equality)
   100 done
   101 
   102 (*Refining one Pi type to another*)
   103 lemma Pi_type: "[| f: Pi(A,C);  !!x. x:A ==> f`x : B(x) |] ==> f : Pi(A,B)"
   104 apply (simp only: Pi_iff)
   105 apply (blast dest: function_apply_equality)
   106 done
   107 
   108 (*Such functions arise in non-standard datatypes, ZF/ex/Ntree for instance*)
   109 lemma Pi_Collect_iff:
   110      "(f : Pi(A, %x. {y:B(x). P(x,y)}))
   111       <->  f : Pi(A,B) & (ALL x: A. P(x, f`x))"
   112 by (blast intro: Pi_type dest: apply_type)
   113 
   114 lemma Pi_weaken_type:
   115         "[| f : Pi(A,B);  !!x. x:A ==> B(x)<=C(x) |] ==> f : Pi(A,C)"
   116 by (blast intro: Pi_type dest: apply_type)
   117 
   118 
   119 (** Elimination of membership in a function **)
   120 
   121 lemma domain_type: "[| <a,b> : f;  f: Pi(A,B) |] ==> a : A"
   122 by (blast dest: fun_is_rel)
   123 
   124 lemma range_type: "[| <a,b> : f;  f: Pi(A,B) |] ==> b : B(a)"
   125 by (blast dest: fun_is_rel)
   126 
   127 lemma Pair_mem_PiD: "[| <a,b>: f;  f: Pi(A,B) |] ==> a:A & b:B(a) & f`a = b"
   128 by (blast intro: domain_type range_type apply_equality)
   129 
   130 (*** Lambda Abstraction ***)
   131 
   132 lemma lamI: "a:A ==> <a,b(a)> : (lam x:A. b(x))"
   133 apply (unfold lam_def)
   134 apply (erule RepFunI)
   135 done
   136 
   137 lemma lamE:
   138     "[| p: (lam x:A. b(x));  !!x.[| x:A; p=<x,b(x)> |] ==> P
   139      |] ==>  P"
   140 by (simp add: lam_def, blast)
   141 
   142 lemma lamD: "[| <a,c>: (lam x:A. b(x)) |] ==> c = b(a)"
   143 by (simp add: lam_def)
   144 
   145 lemma lam_type [TC]:
   146     "[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B)"
   147 by (simp add: lam_def Pi_def function_def, blast)
   148 
   149 lemma lam_funtype: "(lam x:A. b(x)) : A -> {b(x). x:A}"
   150 by (blast intro: lam_type)
   151 
   152 lemma function_lam: "function (lam x:A. b(x))"
   153 by (simp add: function_def lam_def) 
   154 
   155 lemma relation_lam: "relation (lam x:A. b(x))"  
   156 by (simp add: relation_def lam_def) 
   157 
   158 lemma beta_if [simp]: "(lam x:A. b(x)) ` a = (if a : A then b(a) else 0)"
   159 by (simp add: apply_def lam_def, blast)
   160 
   161 lemma beta: "a : A ==> (lam x:A. b(x)) ` a = b(a)"
   162 by (simp add: apply_def lam_def, blast)
   163 
   164 lemma lam_empty [simp]: "(lam x:0. b(x)) = 0"
   165 by (simp add: lam_def)
   166 
   167 lemma domain_lam [simp]: "domain(Lambda(A,b)) = A"
   168 by (simp add: lam_def, blast)
   169 
   170 (*congruence rule for lambda abstraction*)
   171 lemma lam_cong [cong]:
   172     "[| A=A';  !!x. x:A' ==> b(x)=b'(x) |] ==> Lambda(A,b) = Lambda(A',b')"
   173 by (simp only: lam_def cong add: RepFun_cong)
   174 
   175 lemma lam_theI:
   176     "(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)"
   177 apply (rule_tac x = "lam x: A. THE y. Q (x,y)" in exI)
   178 apply simp 
   179 apply (blast intro: theI)
   180 done
   181 
   182 lemma lam_eqE: "[| (lam x:A. f(x)) = (lam x:A. g(x));  a:A |] ==> f(a)=g(a)"
   183 by (fast intro!: lamI elim: equalityE lamE)
   184 
   185 
   186 (*Empty function spaces*)
   187 lemma Pi_empty1 [simp]: "Pi(0,A) = {0}"
   188 by (unfold Pi_def function_def, blast)
   189 
   190 (*The singleton function*)
   191 lemma singleton_fun [simp]: "{<a,b>} : {a} -> {b}"
   192 by (unfold Pi_def function_def, blast)
   193 
   194 lemma Pi_empty2 [simp]: "(A->0) = (if A=0 then {0} else 0)"
   195 by (unfold Pi_def function_def, force)
   196 
   197 lemma  fun_space_empty_iff [iff]: "(A->X)=0 \<longleftrightarrow> X=0 & (A \<noteq> 0)"
   198 apply auto
   199 apply (fast intro!: equals0I intro: lam_type)
   200 done
   201 
   202 
   203 (** Extensionality **)
   204 
   205 (*Semi-extensionality!*)
   206 
   207 lemma fun_subset:
   208     "[| f : Pi(A,B);  g: Pi(C,D);  A<=C;
   209         !!x. x:A ==> f`x = g`x       |] ==> f<=g"
   210 by (force dest: Pi_memberD intro: apply_Pair)
   211 
   212 lemma fun_extension:
   213     "[| f : Pi(A,B);  g: Pi(A,D);
   214         !!x. x:A ==> f`x = g`x       |] ==> f=g"
   215 by (blast del: subsetI intro: subset_refl sym fun_subset)
   216 
   217 lemma eta [simp]: "f : Pi(A,B) ==> (lam x:A. f`x) = f"
   218 apply (rule fun_extension)
   219 apply (auto simp add: lam_type apply_type beta)
   220 done
   221 
   222 lemma fun_extension_iff:
   223      "[| f:Pi(A,B); g:Pi(A,C) |] ==> (ALL a:A. f`a = g`a) <-> f=g"
   224 by (blast intro: fun_extension)
   225 
   226 (*thm by Mark Staples, proof by lcp*)
   227 lemma fun_subset_eq: "[| f:Pi(A,B); g:Pi(A,C) |] ==> f <= g <-> (f = g)"
   228 by (blast dest: apply_Pair
   229 	  intro: fun_extension apply_equality [symmetric])
   230 
   231 
   232 (*Every element of Pi(A,B) may be expressed as a lambda abstraction!*)
   233 lemma Pi_lamE:
   234   assumes major: "f: Pi(A,B)"
   235       and minor: "!!b. [| ALL x:A. b(x):B(x);  f = (lam x:A. b(x)) |] ==> P"
   236   shows "P"
   237 apply (rule minor)
   238 apply (rule_tac [2] eta [symmetric])
   239 apply (blast intro: major apply_type)+
   240 done
   241 
   242 
   243 (** Images of functions **)
   244 
   245 lemma image_lam: "C <= A ==> (lam x:A. b(x)) `` C = {b(x). x:C}"
   246 by (unfold lam_def, blast)
   247 
   248 lemma Repfun_function_if:
   249      "function(f) 
   250       ==> {f`x. x:C} = (if C <= domain(f) then f``C else cons(0,f``C))";
   251 apply simp
   252 apply (intro conjI impI)  
   253  apply (blast dest: function_apply_equality intro: function_apply_Pair) 
   254 apply (rule equalityI)
   255  apply (blast intro!: function_apply_Pair apply_0) 
   256 apply (blast dest: function_apply_equality intro: apply_0 [symmetric]) 
   257 done
   258 
   259 (*For this lemma and the next, the right-hand side could equivalently 
   260   be written UN x:C. {f`x} *)
   261 lemma image_function:
   262      "[| function(f);  C <= domain(f) |] ==> f``C = {f`x. x:C}";
   263 by (simp add: Repfun_function_if) 
   264 
   265 lemma image_fun: "[| f : Pi(A,B);  C <= A |] ==> f``C = {f`x. x:C}"
   266 apply (simp add: Pi_iff) 
   267 apply (blast intro: image_function) 
   268 done
   269 
   270 lemma Pi_image_cons:
   271      "[| f: Pi(A,B);  x: A |] ==> f `` cons(x,y) = cons(f`x, f``y)"
   272 by (blast dest: apply_equality apply_Pair)
   273 
   274 
   275 (*** properties of "restrict" ***)
   276 
   277 lemma restrict_subset: "restrict(f,A) <= f"
   278 by (unfold restrict_def, blast)
   279 
   280 lemma function_restrictI:
   281     "function(f) ==> function(restrict(f,A))"
   282 by (unfold restrict_def function_def, blast)
   283 
   284 lemma restrict_type2: "[| f: Pi(C,B);  A<=C |] ==> restrict(f,A) : Pi(A,B)"
   285 by (simp add: Pi_iff function_def restrict_def, blast)
   286 
   287 lemma restrict: "restrict(f,A) ` a = (if a : A then f`a else 0)"
   288 by (simp add: apply_def restrict_def, blast)
   289 
   290 lemma restrict_empty [simp]: "restrict(f,0) = 0"
   291 by (unfold restrict_def, simp)
   292 
   293 lemma restrict_iff: "z \<in> restrict(r,A) \<longleftrightarrow> z \<in> r & (\<exists>x\<in>A. \<exists>y. z = \<langle>x, y\<rangle>)"
   294 by (simp add: restrict_def) 
   295 
   296 lemma domain_restrict_lam [simp]: "domain(restrict(Lambda(A,f),C)) = A Int C"
   297 apply (unfold restrict_def lam_def)
   298 apply (rule equalityI)
   299 apply (auto simp add: domain_iff)
   300 done
   301 
   302 lemma restrict_restrict [simp]:
   303      "restrict(restrict(r,A),B) = restrict(r, A Int B)"
   304 by (unfold restrict_def, blast)
   305 
   306 lemma domain_restrict [simp]: "domain(restrict(f,C)) = domain(f) Int C"
   307 apply (unfold restrict_def)
   308 apply (auto simp add: domain_def)
   309 done
   310 
   311 lemma restrict_idem [simp]: "f <= Sigma(A,B) ==> restrict(f,A) = f"
   312 by (simp add: restrict_def, blast)
   313 
   314 lemma restrict_if [simp]: "restrict(f,A) ` a = (if a : A then f`a else 0)"
   315 by (simp add: restrict apply_0)
   316 
   317 lemma restrict_lam_eq:
   318     "A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))"
   319 by (unfold restrict_def lam_def, auto)
   320 
   321 lemma fun_cons_restrict_eq:
   322      "f : cons(a, b) -> B ==> f = cons(<a, f ` a>, restrict(f, b))"
   323 apply (rule equalityI)
   324 prefer 2 apply (blast intro: apply_Pair restrict_subset [THEN subsetD])
   325 apply (auto dest!: Pi_memberD simp add: restrict_def lam_def)
   326 done
   327 
   328 
   329 (*** Unions of functions ***)
   330 
   331 (** The Union of a set of COMPATIBLE functions is a function **)
   332 
   333 lemma function_Union:
   334     "[| ALL x:S. function(x);
   335         ALL x:S. ALL y:S. x<=y | y<=x  |]
   336      ==> function(Union(S))"
   337 by (unfold function_def, blast) 
   338 
   339 lemma fun_Union:
   340     "[| ALL f:S. EX C D. f:C->D;
   341              ALL f:S. ALL y:S. f<=y | y<=f  |] ==>
   342           Union(S) : domain(Union(S)) -> range(Union(S))"
   343 apply (unfold Pi_def)
   344 apply (blast intro!: rel_Union function_Union)
   345 done
   346 
   347 lemma gen_relation_Union [rule_format]:
   348      "\<forall>f\<in>F. relation(f) \<Longrightarrow> relation(Union(F))"
   349 by (simp add: relation_def) 
   350 
   351 
   352 (** The Union of 2 disjoint functions is a function **)
   353 
   354 lemmas Un_rls = Un_subset_iff SUM_Un_distrib1 prod_Un_distrib2
   355                 subset_trans [OF _ Un_upper1]
   356                 subset_trans [OF _ Un_upper2]
   357 
   358 lemma fun_disjoint_Un:
   359      "[| f: A->B;  g: C->D;  A Int C = 0  |]
   360       ==> (f Un g) : (A Un C) -> (B Un D)"
   361 (*Prove the product and domain subgoals using distributive laws*)
   362 apply (simp add: Pi_iff extension Un_rls)
   363 apply (unfold function_def, blast)
   364 done
   365 
   366 lemma fun_disjoint_apply1: "a \<notin> domain(g) ==> (f Un g)`a = f`a"
   367 by (simp add: apply_def, blast) 
   368 
   369 lemma fun_disjoint_apply2: "c \<notin> domain(f) ==> (f Un g)`c = g`c"
   370 by (simp add: apply_def, blast) 
   371 
   372 (** Domain and range of a function/relation **)
   373 
   374 lemma domain_of_fun: "f : Pi(A,B) ==> domain(f)=A"
   375 by (unfold Pi_def, blast)
   376 
   377 lemma apply_rangeI: "[| f : Pi(A,B);  a: A |] ==> f`a : range(f)"
   378 by (erule apply_Pair [THEN rangeI], assumption)
   379 
   380 lemma range_of_fun: "f : Pi(A,B) ==> f : A->range(f)"
   381 by (blast intro: Pi_type apply_rangeI)
   382 
   383 (*** Extensions of functions ***)
   384 
   385 lemma fun_extend:
   386      "[| f: A->B;  c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)"
   387 apply (frule singleton_fun [THEN fun_disjoint_Un], blast)
   388 apply (simp add: cons_eq) 
   389 done
   390 
   391 lemma fun_extend3:
   392      "[| f: A->B;  c~:A;  b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B"
   393 by (blast intro: fun_extend [THEN fun_weaken_type])
   394 
   395 lemma extend_apply:
   396      "c ~: domain(f) ==> cons(<c,b>,f)`a = (if a=c then b else f`a)"
   397 by (auto simp add: apply_def) 
   398 
   399 lemma fun_extend_apply [simp]:
   400      "[| f: A->B;  c~:A |] ==> cons(<c,b>,f)`a = (if a=c then b else f`a)" 
   401 apply (rule extend_apply) 
   402 apply (simp add: Pi_def, blast) 
   403 done
   404 
   405 lemmas singleton_apply = apply_equality [OF singletonI singleton_fun, simp]
   406 
   407 (*For Finite.ML.  Inclusion of right into left is easy*)
   408 lemma cons_fun_eq:
   409      "c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})"
   410 apply (rule equalityI)
   411 apply (safe elim!: fun_extend3)
   412 (*Inclusion of left into right*)
   413 apply (subgoal_tac "restrict (x, A) : A -> B")
   414  prefer 2 apply (blast intro: restrict_type2)
   415 apply (rule UN_I, assumption)
   416 apply (rule apply_funtype [THEN UN_I]) 
   417   apply assumption
   418  apply (rule consI1) 
   419 apply (simp (no_asm))
   420 apply (rule fun_extension) 
   421   apply assumption
   422  apply (blast intro: fun_extend) 
   423 apply (erule consE, simp_all)
   424 done
   425 
   426 ML
   427 {*
   428 val Pi_iff = thm "Pi_iff";
   429 val Pi_iff_old = thm "Pi_iff_old";
   430 val fun_is_function = thm "fun_is_function";
   431 val fun_is_rel = thm "fun_is_rel";
   432 val Pi_cong = thm "Pi_cong";
   433 val fun_weaken_type = thm "fun_weaken_type";
   434 val apply_equality2 = thm "apply_equality2";
   435 val function_apply_equality = thm "function_apply_equality";
   436 val apply_equality = thm "apply_equality";
   437 val apply_0 = thm "apply_0";
   438 val Pi_memberD = thm "Pi_memberD";
   439 val function_apply_Pair = thm "function_apply_Pair";
   440 val apply_Pair = thm "apply_Pair";
   441 val apply_type = thm "apply_type";
   442 val apply_funtype = thm "apply_funtype";
   443 val apply_iff = thm "apply_iff";
   444 val Pi_type = thm "Pi_type";
   445 val Pi_Collect_iff = thm "Pi_Collect_iff";
   446 val Pi_weaken_type = thm "Pi_weaken_type";
   447 val domain_type = thm "domain_type";
   448 val range_type = thm "range_type";
   449 val Pair_mem_PiD = thm "Pair_mem_PiD";
   450 val lamI = thm "lamI";
   451 val lamE = thm "lamE";
   452 val lamD = thm "lamD";
   453 val lam_type = thm "lam_type";
   454 val lam_funtype = thm "lam_funtype";
   455 val beta = thm "beta";
   456 val lam_empty = thm "lam_empty";
   457 val domain_lam = thm "domain_lam";
   458 val lam_cong = thm "lam_cong";
   459 val lam_theI = thm "lam_theI";
   460 val lam_eqE = thm "lam_eqE";
   461 val Pi_empty1 = thm "Pi_empty1";
   462 val singleton_fun = thm "singleton_fun";
   463 val Pi_empty2 = thm "Pi_empty2";
   464 val fun_space_empty_iff = thm "fun_space_empty_iff";
   465 val fun_subset = thm "fun_subset";
   466 val fun_extension = thm "fun_extension";
   467 val eta = thm "eta";
   468 val fun_extension_iff = thm "fun_extension_iff";
   469 val fun_subset_eq = thm "fun_subset_eq";
   470 val Pi_lamE = thm "Pi_lamE";
   471 val image_lam = thm "image_lam";
   472 val image_fun = thm "image_fun";
   473 val Pi_image_cons = thm "Pi_image_cons";
   474 val restrict_subset = thm "restrict_subset";
   475 val function_restrictI = thm "function_restrictI";
   476 val restrict_type2 = thm "restrict_type2";
   477 val restrict = thm "restrict";
   478 val restrict_empty = thm "restrict_empty";
   479 val domain_restrict_lam = thm "domain_restrict_lam";
   480 val restrict_restrict = thm "restrict_restrict";
   481 val domain_restrict = thm "domain_restrict";
   482 val restrict_idem = thm "restrict_idem";
   483 val restrict_if = thm "restrict_if";
   484 val restrict_lam_eq = thm "restrict_lam_eq";
   485 val fun_cons_restrict_eq = thm "fun_cons_restrict_eq";
   486 val function_Union = thm "function_Union";
   487 val fun_Union = thm "fun_Union";
   488 val fun_disjoint_Un = thm "fun_disjoint_Un";
   489 val fun_disjoint_apply1 = thm "fun_disjoint_apply1";
   490 val fun_disjoint_apply2 = thm "fun_disjoint_apply2";
   491 val domain_of_fun = thm "domain_of_fun";
   492 val apply_rangeI = thm "apply_rangeI";
   493 val range_of_fun = thm "range_of_fun";
   494 val fun_extend = thm "fun_extend";
   495 val fun_extend3 = thm "fun_extend3";
   496 val fun_extend_apply = thm "fun_extend_apply";
   497 val singleton_apply = thm "singleton_apply";
   498 val cons_fun_eq = thm "cons_fun_eq";
   499 *}
   500 
   501 end