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
```