src/ZF/Perm.thy
author paulson
Tue Mar 06 15:15:49 2012 +0000 (2012-03-06)
changeset 46820 c656222c4dc1
parent 45602 2a858377c3d2
child 46821 ff6b0c1087f2
permissions -rw-r--r--
mathematical symbols instead of ASCII
wenzelm@32960
     1
(*  Title:      ZF/Perm.thy
clasohm@1478
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     3
    Copyright   1991  University of Cambridge
clasohm@0
     4
clasohm@0
     5
The theory underlying permutation groups
clasohm@0
     6
  -- Composition of relations, the identity relation
clasohm@0
     7
  -- Injections, surjections, bijections
clasohm@0
     8
  -- Lemmas for the Schroeder-Bernstein Theorem
clasohm@0
     9
*)
clasohm@0
    10
paulson@13356
    11
header{*Injections, Surjections, Bijections, Composition*}
paulson@13356
    12
haftmann@16417
    13
theory Perm imports func begin
clasohm@0
    14
wenzelm@24893
    15
definition
paulson@13176
    16
  (*composition of relations and functions; NOT Suppes's relative product*)
wenzelm@24893
    17
  comp     :: "[i,i]=>i"      (infixr "O" 60)  where
paulson@46820
    18
    "r O s == {xz \<in> domain(s)*range(r) . 
paulson@46820
    19
               \<exists>x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
paulson@13176
    20
wenzelm@24893
    21
definition
paulson@1806
    22
  (*the identity function for A*)
wenzelm@24893
    23
  id    :: "i=>i"  where
paulson@46820
    24
    "id(A) == (\<lambda>x\<in>A. x)"
clasohm@0
    25
wenzelm@24893
    26
definition
paulson@1806
    27
  (*one-to-one functions from A to B*)
wenzelm@24893
    28
  inj   :: "[i,i]=>i"  where
paulson@46820
    29
    "inj(A,B) == { f: A->B. \<forall>w\<in>A. \<forall>x\<in>A. f`w=f`x \<longrightarrow> w=x}"
clasohm@0
    30
wenzelm@24893
    31
definition
paulson@1806
    32
  (*onto functions from A to B*)
wenzelm@24893
    33
  surj  :: "[i,i]=>i"  where
paulson@46820
    34
    "surj(A,B) == { f: A->B . \<forall>y\<in>B. \<exists>x\<in>A. f`x=y}"
clasohm@0
    35
wenzelm@24893
    36
definition
paulson@1806
    37
  (*one-to-one and onto functions*)
wenzelm@24893
    38
  bij   :: "[i,i]=>i"  where
paulson@46820
    39
    "bij(A,B) == inj(A,B) \<inter> surj(A,B)"
paulson@13176
    40
paulson@13176
    41
paulson@41160
    42
subsection{*Surjective Function Space*}
paulson@13176
    43
paulson@13176
    44
lemma surj_is_fun: "f: surj(A,B) ==> f: A->B"
paulson@13176
    45
apply (unfold surj_def)
paulson@13176
    46
apply (erule CollectD1)
paulson@13176
    47
done
paulson@13176
    48
paulson@46820
    49
lemma fun_is_surj: "f \<in> Pi(A,B) ==> f: surj(A,range(f))"
paulson@13176
    50
apply (unfold surj_def)
paulson@13176
    51
apply (blast intro: apply_equality range_of_fun domain_type)
paulson@13176
    52
done
paulson@13176
    53
paulson@13176
    54
lemma surj_range: "f: surj(A,B) ==> range(f)=B"
paulson@13176
    55
apply (unfold surj_def)
paulson@13176
    56
apply (best intro: apply_Pair elim: range_type)
paulson@13176
    57
done
paulson@13176
    58
paulson@41160
    59
text{* A function with a right inverse is a surjection *}
paulson@13176
    60
paulson@13176
    61
lemma f_imp_surjective: 
paulson@13176
    62
    "[| f: A->B;  !!y. y:B ==> d(y): A;  !!y. y:B ==> f`d(y) = y |]
paulson@13176
    63
     ==> f: surj(A,B)"
paulson@41160
    64
  by (simp add: surj_def, blast)
paulson@13176
    65
paulson@13176
    66
lemma lam_surjective: 
paulson@13176
    67
    "[| !!x. x:A ==> c(x): B;            
paulson@13176
    68
        !!y. y:B ==> d(y): A;            
paulson@13176
    69
        !!y. y:B ==> c(d(y)) = y         
paulson@46820
    70
     |] ==> (\<lambda>x\<in>A. c(x)) \<in> surj(A,B)"
paulson@13784
    71
apply (rule_tac d = d in f_imp_surjective) 
paulson@13176
    72
apply (simp_all add: lam_type)
paulson@13176
    73
done
paulson@13176
    74
paulson@41160
    75
text{*Cantor's theorem revisited*}
paulson@46820
    76
lemma cantor_surj: "f \<notin> surj(A,Pow(A))"
paulson@13180
    77
apply (unfold surj_def, safe)
paulson@13176
    78
apply (cut_tac cantor)
paulson@13176
    79
apply (best del: subsetI) 
paulson@13176
    80
done
paulson@13176
    81
paulson@13176
    82
paulson@41160
    83
subsection{*Injective Function Space*}
paulson@13176
    84
paulson@13176
    85
lemma inj_is_fun: "f: inj(A,B) ==> f: A->B"
paulson@13176
    86
apply (unfold inj_def)
paulson@13176
    87
apply (erule CollectD1)
paulson@13176
    88
done
paulson@13176
    89
paulson@41160
    90
text{*Good for dealing with sets of pairs, but a bit ugly in use [used in AC]*}
paulson@13176
    91
lemma inj_equality: 
paulson@13176
    92
    "[| <a,b>:f;  <c,b>:f;  f: inj(A,B) |] ==> a=c"
paulson@13176
    93
apply (unfold inj_def)
paulson@13176
    94
apply (blast dest: Pair_mem_PiD)
paulson@13176
    95
done
paulson@13176
    96
paulson@13513
    97
lemma inj_apply_equality: "[| f:inj(A,B);  f`a=f`b;  a:A;  b:A |] ==> a=b"
paulson@13180
    98
by (unfold inj_def, blast)
paulson@13176
    99
paulson@41160
   100
text{* A function with a left inverse is an injection *}
paulson@13176
   101
paulson@46820
   102
lemma f_imp_injective: "[| f: A->B;  \<forall>x\<in>A. d(f`x)=x |] ==> f: inj(A,B)"
paulson@13176
   103
apply (simp (no_asm_simp) add: inj_def)
paulson@13176
   104
apply (blast intro: subst_context [THEN box_equals])
paulson@13176
   105
done
paulson@13176
   106
paulson@13176
   107
lemma lam_injective: 
paulson@13176
   108
    "[| !!x. x:A ==> c(x): B;            
paulson@13176
   109
        !!x. x:A ==> d(c(x)) = x |]
paulson@46820
   110
     ==> (\<lambda>x\<in>A. c(x)) \<in> inj(A,B)"
paulson@13784
   111
apply (rule_tac d = d in f_imp_injective)
paulson@13176
   112
apply (simp_all add: lam_type)
paulson@13176
   113
done
paulson@13176
   114
paulson@13356
   115
subsection{*Bijections*}
paulson@13176
   116
paulson@13176
   117
lemma bij_is_inj: "f: bij(A,B) ==> f: inj(A,B)"
paulson@13176
   118
apply (unfold bij_def)
paulson@13176
   119
apply (erule IntD1)
paulson@13176
   120
done
paulson@13176
   121
paulson@13176
   122
lemma bij_is_surj: "f: bij(A,B) ==> f: surj(A,B)"
paulson@13176
   123
apply (unfold bij_def)
paulson@13176
   124
apply (erule IntD2)
paulson@13176
   125
done
paulson@13176
   126
paulson@41160
   127
text{* f: bij(A,B) ==> f: A->B *}
wenzelm@45602
   128
lemmas bij_is_fun = bij_is_inj [THEN inj_is_fun]
paulson@13176
   129
paulson@13176
   130
lemma lam_bijective: 
paulson@13176
   131
    "[| !!x. x:A ==> c(x): B;            
paulson@13176
   132
        !!y. y:B ==> d(y): A;            
paulson@13176
   133
        !!x. x:A ==> d(c(x)) = x;        
paulson@13176
   134
        !!y. y:B ==> c(d(y)) = y         
paulson@46820
   135
     |] ==> (\<lambda>x\<in>A. c(x)) \<in> bij(A,B)"
paulson@13176
   136
apply (unfold bij_def)
paulson@13180
   137
apply (blast intro!: lam_injective lam_surjective)
paulson@13176
   138
done
paulson@13176
   139
paulson@46820
   140
lemma RepFun_bijective: "(\<forall>y\<in>x. EX! y'. f(y') = f(y))   
paulson@46820
   141
      ==> (\<lambda>z\<in>{f(y). y:x}. THE y. f(y) = z) \<in> bij({f(y). y:x}, x)"
paulson@13784
   142
apply (rule_tac d = f in lam_bijective)
paulson@13176
   143
apply (auto simp add: the_equality2)
paulson@13176
   144
done
paulson@13176
   145
paulson@13176
   146
paulson@13356
   147
subsection{*Identity Function*}
paulson@13176
   148
paulson@46820
   149
lemma idI [intro!]: "a:A ==> <a,a> \<in> id(A)"
paulson@13176
   150
apply (unfold id_def)
paulson@13176
   151
apply (erule lamI)
paulson@13176
   152
done
paulson@13176
   153
paulson@13176
   154
lemma idE [elim!]: "[| p: id(A);  !!x.[| x:A; p=<x,x> |] ==> P |] ==>  P"
paulson@13180
   155
by (simp add: id_def lam_def, blast)
paulson@13176
   156
paulson@46820
   157
lemma id_type: "id(A) \<in> A->A"
paulson@13176
   158
apply (unfold id_def)
paulson@13180
   159
apply (rule lam_type, assumption)
paulson@13176
   160
done
paulson@13176
   161
paulson@13176
   162
lemma id_conv [simp]: "x:A ==> id(A)`x = x"
paulson@13176
   163
apply (unfold id_def)
paulson@13176
   164
apply (simp (no_asm_simp))
paulson@13176
   165
done
paulson@13176
   166
paulson@46820
   167
lemma id_mono: "A<=B ==> id(A) \<subseteq> id(B)"
paulson@13176
   168
apply (unfold id_def)
paulson@13176
   169
apply (erule lam_mono)
paulson@13176
   170
done
paulson@13176
   171
paulson@13176
   172
lemma id_subset_inj: "A<=B ==> id(A): inj(A,B)"
paulson@13176
   173
apply (simp add: inj_def id_def)
paulson@13176
   174
apply (blast intro: lam_type) 
paulson@13176
   175
done
paulson@13176
   176
wenzelm@45602
   177
lemmas id_inj = subset_refl [THEN id_subset_inj]
paulson@13176
   178
paulson@13176
   179
lemma id_surj: "id(A): surj(A,A)"
paulson@13176
   180
apply (unfold id_def surj_def)
paulson@13176
   181
apply (simp (no_asm_simp))
paulson@13176
   182
done
paulson@13176
   183
paulson@13176
   184
lemma id_bij: "id(A): bij(A,A)"
paulson@13176
   185
apply (unfold bij_def)
paulson@13176
   186
apply (blast intro: id_inj id_surj)
paulson@13176
   187
done
paulson@13176
   188
paulson@46820
   189
lemma subset_iff_id: "A \<subseteq> B <-> id(A) \<in> A->B"
paulson@13176
   190
apply (unfold id_def)
paulson@13180
   191
apply (force intro!: lam_type dest: apply_type)
paulson@13176
   192
done
paulson@13176
   193
paulson@14060
   194
text{*@{term id} as the identity relation*}
paulson@14060
   195
lemma id_iff [simp]: "<x,y> \<in> id(A) <-> x=y & y \<in> A"
paulson@14060
   196
by auto
paulson@13176
   197
paulson@14060
   198
paulson@14060
   199
subsection{*Converse of a Function*}
paulson@13176
   200
paulson@46820
   201
lemma inj_converse_fun: "f: inj(A,B) ==> converse(f) \<in> range(f)->A"
paulson@13176
   202
apply (unfold inj_def)
paulson@13176
   203
apply (simp (no_asm_simp) add: Pi_iff function_def)
paulson@13176
   204
apply (erule CollectE)
paulson@13176
   205
apply (simp (no_asm_simp) add: apply_iff)
paulson@13176
   206
apply (blast dest: fun_is_rel)
paulson@13176
   207
done
paulson@13176
   208
paulson@41160
   209
text{* Equations for converse(f) *}
paulson@13176
   210
paulson@14060
   211
text{*The premises are equivalent to saying that f is injective...*}
paulson@13176
   212
lemma left_inverse_lemma:
paulson@13176
   213
     "[| f: A->B;  converse(f): C->A;  a: A |] ==> converse(f)`(f`a) = a"
paulson@13176
   214
by (blast intro: apply_Pair apply_equality converseI)
paulson@13176
   215
paulson@13176
   216
lemma left_inverse [simp]: "[| f: inj(A,B);  a: A |] ==> converse(f)`(f`a) = a"
paulson@13180
   217
by (blast intro: left_inverse_lemma inj_converse_fun inj_is_fun)
paulson@13176
   218
paulson@14883
   219
lemma left_inverse_eq:
paulson@14883
   220
     "[|f \<in> inj(A,B); f ` x = y; x \<in> A|] ==> converse(f) ` y = x"
paulson@14883
   221
by auto
paulson@14883
   222
wenzelm@45602
   223
lemmas left_inverse_bij = bij_is_inj [THEN left_inverse]
paulson@13176
   224
paulson@13176
   225
lemma right_inverse_lemma:
paulson@13176
   226
     "[| f: A->B;  converse(f): C->A;  b: C |] ==> f`(converse(f)`b) = b"
paulson@14883
   227
by (rule apply_Pair [THEN converseD [THEN apply_equality]], auto) 
paulson@13176
   228
paulson@13176
   229
(*Should the premises be f:surj(A,B), b:B for symmetry with left_inverse?
paulson@13176
   230
  No: they would not imply that converse(f) was a function! *)
paulson@13176
   231
lemma right_inverse [simp]:
paulson@13176
   232
     "[| f: inj(A,B);  b: range(f) |] ==> f`(converse(f)`b) = b"
paulson@13176
   233
by (blast intro: right_inverse_lemma inj_converse_fun inj_is_fun)
paulson@13176
   234
paulson@13176
   235
lemma right_inverse_bij: "[| f: bij(A,B);  b: B |] ==> f`(converse(f)`b) = b"
paulson@13180
   236
by (force simp add: bij_def surj_range)
paulson@13176
   237
paulson@13356
   238
subsection{*Converses of Injections, Surjections, Bijections*}
paulson@13176
   239
paulson@13176
   240
lemma inj_converse_inj: "f: inj(A,B) ==> converse(f): inj(range(f), A)"
paulson@13176
   241
apply (rule f_imp_injective)
paulson@13180
   242
apply (erule inj_converse_fun, clarify) 
paulson@13180
   243
apply (rule right_inverse)
paulson@13176
   244
 apply assumption
paulson@13180
   245
apply blast 
paulson@13176
   246
done
paulson@13176
   247
paulson@13176
   248
lemma inj_converse_surj: "f: inj(A,B) ==> converse(f): surj(range(f), A)"
paulson@13176
   249
by (blast intro: f_imp_surjective inj_converse_fun left_inverse inj_is_fun 
paulson@13176
   250
                 range_of_fun [THEN apply_type])
paulson@13176
   251
paulson@41160
   252
text{*Adding this as an intro! rule seems to cause looping*}
paulson@13176
   253
lemma bij_converse_bij [TC]: "f: bij(A,B) ==> converse(f): bij(B,A)"
paulson@13176
   254
apply (unfold bij_def)
paulson@13176
   255
apply (fast elim: surj_range [THEN subst] inj_converse_inj inj_converse_surj)
paulson@13176
   256
done
paulson@13176
   257
paulson@13176
   258
paulson@13176
   259
paulson@13356
   260
subsection{*Composition of Two Relations*}
paulson@13176
   261
paulson@46820
   262
text{*The inductive definition package could derive these theorems for @{term"r O s"}*}
paulson@13176
   263
paulson@46820
   264
lemma compI [intro]: "[| <a,b>:s; <b,c>:r |] ==> <a,c> \<in> r O s"
paulson@13180
   265
by (unfold comp_def, blast)
paulson@13176
   266
paulson@13176
   267
lemma compE [elim!]: 
paulson@46820
   268
    "[| xz \<in> r O s;   
paulson@13176
   269
        !!x y z. [| xz=<x,z>;  <x,y>:s;  <y,z>:r |] ==> P |]
paulson@13176
   270
     ==> P"
paulson@13180
   271
by (unfold comp_def, blast)
paulson@13176
   272
paulson@13176
   273
lemma compEpair: 
paulson@46820
   274
    "[| <a,c> \<in> r O s;   
paulson@13176
   275
        !!y. [| <a,y>:s;  <y,c>:r |] ==> P |]
paulson@13176
   276
     ==> P"
paulson@13180
   277
by (erule compE, simp)  
paulson@13176
   278
paulson@13176
   279
lemma converse_comp: "converse(R O S) = converse(S) O converse(R)"
paulson@13180
   280
by blast
paulson@13176
   281
paulson@13176
   282
paulson@13356
   283
subsection{*Domain and Range -- see Suppes, Section 3.1*}
paulson@13176
   284
paulson@41160
   285
text{*Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327*}
paulson@46820
   286
lemma range_comp: "range(r O s) \<subseteq> range(r)"
paulson@13180
   287
by blast
paulson@13176
   288
paulson@46820
   289
lemma range_comp_eq: "domain(r) \<subseteq> range(s) ==> range(r O s) = range(r)"
paulson@13180
   290
by (rule range_comp [THEN equalityI], blast)
paulson@13176
   291
paulson@46820
   292
lemma domain_comp: "domain(r O s) \<subseteq> domain(s)"
paulson@13180
   293
by blast
paulson@13176
   294
paulson@46820
   295
lemma domain_comp_eq: "range(s) \<subseteq> domain(r) ==> domain(r O s) = domain(s)"
paulson@13180
   296
by (rule domain_comp [THEN equalityI], blast)
paulson@13176
   297
paulson@13176
   298
lemma image_comp: "(r O s)``A = r``(s``A)"
paulson@13180
   299
by blast
paulson@13176
   300
paulson@46820
   301
lemma inj_inj_range: "f: inj(A,B) ==> f \<in> inj(A,range(f))"
paulson@41160
   302
  by (auto simp add: inj_def Pi_iff function_def)
paulson@41160
   303
paulson@46820
   304
lemma inj_bij_range: "f: inj(A,B) ==> f \<in> bij(A,range(f))"
paulson@41160
   305
  by (auto simp add: bij_def intro: inj_inj_range inj_is_fun fun_is_surj) 
paulson@41160
   306
paulson@13176
   307
paulson@13356
   308
subsection{*Other Results*}
paulson@13176
   309
paulson@46820
   310
lemma comp_mono: "[| r'<=r; s'<=s |] ==> (r' O s') \<subseteq> (r O s)"
paulson@13180
   311
by blast
paulson@13176
   312
paulson@41160
   313
text{*composition preserves relations*}
paulson@46820
   314
lemma comp_rel: "[| s<=A*B;  r<=B*C |] ==> (r O s) \<subseteq> A*C"
paulson@13180
   315
by blast
paulson@13176
   316
paulson@41160
   317
text{*associative law for composition*}
paulson@13176
   318
lemma comp_assoc: "(r O s) O t = r O (s O t)"
paulson@13180
   319
by blast
paulson@13176
   320
paulson@13176
   321
(*left identity of composition; provable inclusions are
paulson@46820
   322
        id(A) O r \<subseteq> r       
paulson@46820
   323
  and   [| r<=A*B; B<=C |] ==> r \<subseteq> id(C) O r *)
paulson@13176
   324
lemma left_comp_id: "r<=A*B ==> id(B) O r = r"
paulson@13180
   325
by blast
paulson@13176
   326
paulson@13176
   327
(*right identity of composition; provable inclusions are
paulson@46820
   328
        r O id(A) \<subseteq> r
paulson@46820
   329
  and   [| r<=A*B; A<=C |] ==> r \<subseteq> r O id(C) *)
paulson@13176
   330
lemma right_comp_id: "r<=A*B ==> r O id(A) = r"
paulson@13180
   331
by blast
paulson@13176
   332
paulson@13176
   333
paulson@13356
   334
subsection{*Composition Preserves Functions, Injections, and Surjections*}
paulson@13176
   335
paulson@13180
   336
lemma comp_function: "[| function(g);  function(f) |] ==> function(f O g)"
paulson@13180
   337
by (unfold function_def, blast)
paulson@13176
   338
paulson@41160
   339
text{*Don't think the premises can be weakened much*}
paulson@46820
   340
lemma comp_fun: "[| g: A->B;  f: B->C |] ==> (f O g) \<in> A->C"
paulson@13176
   341
apply (auto simp add: Pi_def comp_function Pow_iff comp_rel)
paulson@13180
   342
apply (subst range_rel_subset [THEN domain_comp_eq], auto) 
paulson@13176
   343
done
paulson@13176
   344
paulson@13176
   345
(*Thanks to the new definition of "apply", the premise f: B->C is gone!*)
paulson@13176
   346
lemma comp_fun_apply [simp]:
paulson@13176
   347
     "[| g: A->B;  a:A |] ==> (f O g)`a = f`(g`a)"
paulson@13176
   348
apply (frule apply_Pair, assumption) 
paulson@13176
   349
apply (simp add: apply_def image_comp)
paulson@13176
   350
apply (blast dest: apply_equality) 
paulson@13176
   351
done
paulson@13176
   352
paulson@41160
   353
text{*Simplifies compositions of lambda-abstractions*}
paulson@13176
   354
lemma comp_lam: 
paulson@13176
   355
    "[| !!x. x:A ==> b(x): B |]
paulson@46820
   356
     ==> (\<lambda>y\<in>B. c(y)) O (\<lambda>x\<in>A. b(x)) = (\<lambda>x\<in>A. c(b(x)))"
paulson@46820
   357
apply (subgoal_tac "(\<lambda>x\<in>A. b(x)) \<in> A -> B") 
paulson@13176
   358
 apply (rule fun_extension)
paulson@13176
   359
   apply (blast intro: comp_fun lam_funtype)
paulson@13176
   360
  apply (rule lam_funtype)
paulson@13180
   361
 apply simp 
paulson@13180
   362
apply (simp add: lam_type) 
paulson@13176
   363
done
paulson@13176
   364
paulson@13176
   365
lemma comp_inj:
paulson@46820
   366
     "[| g: inj(A,B);  f: inj(B,C) |] ==> (f O g) \<in> inj(A,C)"
paulson@13176
   367
apply (frule inj_is_fun [of g]) 
paulson@13176
   368
apply (frule inj_is_fun [of f]) 
paulson@13176
   369
apply (rule_tac d = "%y. converse (g) ` (converse (f) ` y)" in f_imp_injective)
paulson@13180
   370
 apply (blast intro: comp_fun, simp)  
paulson@13176
   371
done
paulson@13176
   372
paulson@13176
   373
lemma comp_surj: 
paulson@46820
   374
    "[| g: surj(A,B);  f: surj(B,C) |] ==> (f O g) \<in> surj(A,C)"
paulson@13176
   375
apply (unfold surj_def)
paulson@13176
   376
apply (blast intro!: comp_fun comp_fun_apply)
paulson@13176
   377
done
paulson@13176
   378
paulson@13176
   379
lemma comp_bij: 
paulson@46820
   380
    "[| g: bij(A,B);  f: bij(B,C) |] ==> (f O g) \<in> bij(A,C)"
paulson@13176
   381
apply (unfold bij_def)
paulson@13176
   382
apply (blast intro: comp_inj comp_surj)
paulson@13176
   383
done
paulson@13176
   384
paulson@13176
   385
paulson@13356
   386
subsection{*Dual Properties of @{term inj} and @{term surj}*}
paulson@13356
   387
paulson@13356
   388
text{*Useful for proofs from
paulson@13176
   389
    D Pastre.  Automatic theorem proving in set theory. 
paulson@13356
   390
    Artificial Intelligence, 10:1--27, 1978.*}
paulson@13176
   391
paulson@13176
   392
lemma comp_mem_injD1: 
paulson@13176
   393
    "[| (f O g): inj(A,C);  g: A->B;  f: B->C |] ==> g: inj(A,B)"
paulson@13356
   394
by (unfold inj_def, force) 
paulson@13176
   395
paulson@13176
   396
lemma comp_mem_injD2: 
paulson@13176
   397
    "[| (f O g): inj(A,C);  g: surj(A,B);  f: B->C |] ==> f: inj(B,C)"
paulson@13180
   398
apply (unfold inj_def surj_def, safe)
paulson@13784
   399
apply (rule_tac x1 = x in bspec [THEN bexE])
paulson@13784
   400
apply (erule_tac [3] x1 = w in bspec [THEN bexE], assumption+, safe)
paulson@13176
   401
apply (rule_tac t = "op ` (g) " in subst_context)
paulson@13176
   402
apply (erule asm_rl bspec [THEN bspec, THEN mp])+
paulson@13176
   403
apply (simp (no_asm_simp))
paulson@13176
   404
done
paulson@13176
   405
paulson@13176
   406
lemma comp_mem_surjD1: 
paulson@13176
   407
    "[| (f O g): surj(A,C);  g: A->B;  f: B->C |] ==> f: surj(B,C)"
paulson@13176
   408
apply (unfold surj_def)
paulson@13176
   409
apply (blast intro!: comp_fun_apply [symmetric] apply_funtype)
paulson@13176
   410
done
paulson@13176
   411
paulson@13176
   412
paulson@13176
   413
lemma comp_mem_surjD2: 
paulson@13176
   414
    "[| (f O g): surj(A,C);  g: A->B;  f: inj(B,C) |] ==> g: surj(A,B)"
paulson@13180
   415
apply (unfold inj_def surj_def, safe)
paulson@13180
   416
apply (drule_tac x = "f`y" in bspec, auto)  
paulson@13176
   417
apply (blast intro: apply_funtype)
paulson@13176
   418
done
paulson@13176
   419
paulson@13356
   420
subsubsection{*Inverses of Composition*}
paulson@13176
   421
paulson@41160
   422
text{*left inverse of composition; one inclusion is
paulson@46820
   423
        @{term "f: A->B ==> id(A) \<subseteq> converse(f) O f"} *}
paulson@13176
   424
lemma left_comp_inverse: "f: inj(A,B) ==> converse(f) O f = id(A)"
paulson@13180
   425
apply (unfold inj_def, clarify) 
paulson@13176
   426
apply (rule equalityI) 
paulson@13180
   427
 apply (auto simp add: apply_iff, blast)  
paulson@13176
   428
done
paulson@13176
   429
paulson@41160
   430
text{*right inverse of composition; one inclusion is
paulson@46820
   431
                @{term "f: A->B ==> f O converse(f) \<subseteq> id(B)"} *}
paulson@13176
   432
lemma right_comp_inverse: 
paulson@13176
   433
    "f: surj(A,B) ==> f O converse(f) = id(B)"
paulson@13180
   434
apply (simp add: surj_def, clarify) 
paulson@13176
   435
apply (rule equalityI)
paulson@13176
   436
apply (best elim: domain_type range_type dest: apply_equality2)
paulson@13176
   437
apply (blast intro: apply_Pair)
paulson@13176
   438
done
paulson@13176
   439
paulson@13176
   440
paulson@13356
   441
subsubsection{*Proving that a Function is a Bijection*}
paulson@13176
   442
paulson@13176
   443
lemma comp_eq_id_iff: 
paulson@46820
   444
    "[| f: A->B;  g: B->A |] ==> f O g = id(B) <-> (\<forall>y\<in>B. f`(g`y)=y)"
paulson@13180
   445
apply (unfold id_def, safe)
paulson@13176
   446
 apply (drule_tac t = "%h. h`y " in subst_context)
paulson@13176
   447
 apply simp
paulson@13176
   448
apply (rule fun_extension)
paulson@13176
   449
  apply (blast intro: comp_fun lam_type)
paulson@13176
   450
 apply auto
paulson@13176
   451
done
paulson@13176
   452
paulson@13176
   453
lemma fg_imp_bijective: 
paulson@46820
   454
    "[| f: A->B;  g: B->A;  f O g = id(B);  g O f = id(A) |] ==> f \<in> bij(A,B)"
paulson@13176
   455
apply (unfold bij_def)
paulson@13176
   456
apply (simp add: comp_eq_id_iff)
paulson@13180
   457
apply (blast intro: f_imp_injective f_imp_surjective apply_funtype)
paulson@13176
   458
done
paulson@13176
   459
paulson@46820
   460
lemma nilpotent_imp_bijective: "[| f: A->A;  f O f = id(A) |] ==> f \<in> bij(A,A)"
paulson@13180
   461
by (blast intro: fg_imp_bijective)
paulson@13176
   462
paulson@13180
   463
lemma invertible_imp_bijective:
paulson@46820
   464
     "[| converse(f): B->A;  f: A->B |] ==> f \<in> bij(A,B)"
paulson@13180
   465
by (simp add: fg_imp_bijective comp_eq_id_iff 
paulson@13180
   466
              left_inverse_lemma right_inverse_lemma)
paulson@13176
   467
paulson@13356
   468
subsubsection{*Unions of Functions*}
paulson@13356
   469
paulson@13356
   470
text{*See similar theorems in func.thy*}
paulson@13176
   471
paulson@41160
   472
text{*Theorem by KG, proof by LCP*}
paulson@13176
   473
lemma inj_disjoint_Un:
paulson@46820
   474
     "[| f: inj(A,B);  g: inj(C,D);  B \<inter> D = 0 |]  
paulson@46820
   475
      ==> (\<lambda>a\<in>A \<union> C. if a:A then f`a else g`a) \<in> inj(A \<union> C, B \<union> D)"
paulson@13180
   476
apply (rule_tac d = "%z. if z:B then converse (f) `z else converse (g) `z" 
paulson@13180
   477
       in lam_injective)
paulson@13176
   478
apply (auto simp add: inj_is_fun [THEN apply_type])
paulson@13176
   479
done
paulson@13176
   480
paulson@13176
   481
lemma surj_disjoint_Un: 
paulson@46820
   482
    "[| f: surj(A,B);  g: surj(C,D);  A \<inter> C = 0 |]   
paulson@46820
   483
     ==> (f \<union> g) \<in> surj(A \<union> C, B \<union> D)"
paulson@13180
   484
apply (simp add: surj_def fun_disjoint_Un) 
paulson@13180
   485
apply (blast dest!: domain_of_fun 
wenzelm@32960
   486
             intro!: fun_disjoint_apply1 fun_disjoint_apply2)
paulson@13176
   487
done
paulson@13176
   488
paulson@41160
   489
text{*A simple, high-level proof; the version for injections follows from it,
paulson@41160
   490
  using  @term{f:inj(A,B) <-> f:bij(A,range(f))}  *}
paulson@13176
   491
lemma bij_disjoint_Un:
paulson@46820
   492
     "[| f: bij(A,B);  g: bij(C,D);  A \<inter> C = 0;  B \<inter> D = 0 |]  
paulson@46820
   493
      ==> (f \<union> g) \<in> bij(A \<union> C, B \<union> D)"
paulson@13176
   494
apply (rule invertible_imp_bijective)
paulson@13176
   495
apply (subst converse_Un)
paulson@13176
   496
apply (auto intro: fun_disjoint_Un bij_is_fun bij_converse_bij)
paulson@13176
   497
done
paulson@13176
   498
paulson@13176
   499
paulson@13356
   500
subsubsection{*Restrictions as Surjections and Bijections*}
paulson@13176
   501
paulson@13176
   502
lemma surj_image:
paulson@13176
   503
    "f: Pi(A,B) ==> f: surj(A, f``A)"
paulson@13180
   504
apply (simp add: surj_def) 
paulson@13180
   505
apply (blast intro: apply_equality apply_Pair Pi_type) 
paulson@13176
   506
done
paulson@13176
   507
paulson@46820
   508
lemma restrict_image [simp]: "restrict(f,A) `` B = f `` (A \<inter> B)"
paulson@13180
   509
by (auto simp add: restrict_def)
paulson@13176
   510
paulson@13176
   511
lemma restrict_inj: 
paulson@13176
   512
    "[| f: inj(A,B);  C<=A |] ==> restrict(f,C): inj(C,B)"
paulson@13176
   513
apply (unfold inj_def)
paulson@13180
   514
apply (safe elim!: restrict_type2, auto) 
paulson@13176
   515
done
paulson@13176
   516
paulson@13176
   517
lemma restrict_surj: "[| f: Pi(A,B);  C<=A |] ==> restrict(f,C): surj(C, f``C)"
paulson@13176
   518
apply (insert restrict_type2 [THEN surj_image])
paulson@13180
   519
apply (simp add: restrict_image) 
paulson@13176
   520
done
paulson@13176
   521
paulson@13176
   522
lemma restrict_bij: 
paulson@13176
   523
    "[| f: inj(A,B);  C<=A |] ==> restrict(f,C): bij(C, f``C)"
paulson@13180
   524
apply (simp add: inj_def bij_def)
paulson@13180
   525
apply (blast intro: restrict_surj surj_is_fun)
paulson@13176
   526
done
paulson@13176
   527
paulson@13176
   528
paulson@13356
   529
subsubsection{*Lemmas for Ramsey's Theorem*}
paulson@13176
   530
paulson@13176
   531
lemma inj_weaken_type: "[| f: inj(A,B);  B<=D |] ==> f: inj(A,D)"
paulson@13176
   532
apply (unfold inj_def)
paulson@13176
   533
apply (blast intro: fun_weaken_type)
paulson@13176
   534
done
paulson@13176
   535
paulson@13176
   536
lemma inj_succ_restrict:
paulson@46820
   537
     "[| f: inj(succ(m), A) |] ==> restrict(f,m) \<in> inj(m, A-{f`m})"
paulson@13269
   538
apply (rule restrict_bij [THEN bij_is_inj, THEN inj_weaken_type], assumption, blast)
paulson@13176
   539
apply (unfold inj_def)
paulson@13176
   540
apply (fast elim: range_type mem_irrefl dest: apply_equality)
paulson@13176
   541
done
paulson@13176
   542
paulson@13176
   543
paulson@13176
   544
lemma inj_extend: 
paulson@46820
   545
    "[| f: inj(A,B);  a\<notin>A;  b\<notin>B |]  
paulson@46820
   546
     ==> cons(<a,b>,f) \<in> inj(cons(a,A), cons(b,B))"
paulson@13176
   547
apply (unfold inj_def)
paulson@13176
   548
apply (force intro: apply_type  simp add: fun_extend)
paulson@13176
   549
done
paulson@13176
   550
clasohm@0
   551
end