src/ZF/Perm.thy
author wenzelm
Thu Dec 14 11:24:26 2017 +0100 (20 months ago)
changeset 67198 694f29a5433b
parent 63901 4ce989e962e0
child 67399 eab6ce8368fa
permissions -rw-r--r--
merged
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
wenzelm@60770
    11
section\<open>Injections, Surjections, Bijections, Composition\<close>
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@46821
    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@46953
    29
    "inj(A,B) == { f \<in> 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@46953
    34
    "surj(A,B) == { f \<in> 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
wenzelm@60770
    42
subsection\<open>Surjective Function Space\<close>
paulson@13176
    43
paulson@46953
    44
lemma surj_is_fun: "f \<in> surj(A,B) ==> f \<in> A->B"
paulson@13176
    45
apply (unfold surj_def)
paulson@13176
    46
apply (erule CollectD1)
paulson@13176
    47
done
paulson@13176
    48
paulson@46953
    49
lemma fun_is_surj: "f \<in> Pi(A,B) ==> f \<in> 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@46953
    54
lemma surj_range: "f \<in> 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
wenzelm@60770
    59
text\<open>A function with a right inverse is a surjection\<close>
paulson@13176
    60
paulson@46821
    61
lemma f_imp_surjective:
paulson@46953
    62
    "[| f \<in> A->B;  !!y. y \<in> B ==> d(y): A;  !!y. y \<in> B ==> f`d(y) = y |]
paulson@46953
    63
     ==> f \<in> surj(A,B)"
paulson@41160
    64
  by (simp add: surj_def, blast)
paulson@13176
    65
paulson@46821
    66
lemma lam_surjective:
paulson@46953
    67
    "[| !!x. x \<in> A ==> c(x): B;
paulson@46953
    68
        !!y. y \<in> B ==> d(y): A;
paulson@46953
    69
        !!y. y \<in> B ==> c(d(y)) = y
paulson@46820
    70
     |] ==> (\<lambda>x\<in>A. c(x)) \<in> surj(A,B)"
paulson@46821
    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
wenzelm@60770
    75
text\<open>Cantor's theorem revisited\<close>
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@46821
    79
apply (best del: subsetI)
paulson@13176
    80
done
paulson@13176
    81
paulson@13176
    82
wenzelm@60770
    83
subsection\<open>Injective Function Space\<close>
paulson@13176
    84
paulson@46953
    85
lemma inj_is_fun: "f \<in> inj(A,B) ==> f \<in> A->B"
paulson@13176
    86
apply (unfold inj_def)
paulson@13176
    87
apply (erule CollectD1)
paulson@13176
    88
done
paulson@13176
    89
wenzelm@60770
    90
text\<open>Good for dealing with sets of pairs, but a bit ugly in use [used in AC]\<close>
paulson@46821
    91
lemma inj_equality:
paulson@46953
    92
    "[| <a,b>:f;  <c,b>:f;  f \<in> 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@46953
    97
lemma inj_apply_equality: "[| f \<in> inj(A,B);  f`a=f`b;  a \<in> A;  b \<in> A |] ==> a=b"
paulson@13180
    98
by (unfold inj_def, blast)
paulson@13176
    99
wenzelm@60770
   100
text\<open>A function with a left inverse is an injection\<close>
paulson@13176
   101
paulson@46953
   102
lemma f_imp_injective: "[| f \<in> A->B;  \<forall>x\<in>A. d(f`x)=x |] ==> f \<in> 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@46821
   107
lemma lam_injective:
paulson@46953
   108
    "[| !!x. x \<in> A ==> c(x): B;
paulson@46953
   109
        !!x. x \<in> 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
wenzelm@60770
   115
subsection\<open>Bijections\<close>
paulson@13176
   116
paulson@46953
   117
lemma bij_is_inj: "f \<in> bij(A,B) ==> f \<in> inj(A,B)"
paulson@13176
   118
apply (unfold bij_def)
paulson@13176
   119
apply (erule IntD1)
paulson@13176
   120
done
paulson@13176
   121
paulson@46953
   122
lemma bij_is_surj: "f \<in> bij(A,B) ==> f \<in> surj(A,B)"
paulson@13176
   123
apply (unfold bij_def)
paulson@13176
   124
apply (erule IntD2)
paulson@13176
   125
done
paulson@13176
   126
paulson@46953
   127
lemma bij_is_fun: "f \<in> bij(A,B) ==> f \<in> A->B"
paulson@46953
   128
  by (rule bij_is_inj [THEN inj_is_fun])
paulson@13176
   129
paulson@46821
   130
lemma lam_bijective:
paulson@46953
   131
    "[| !!x. x \<in> A ==> c(x): B;
paulson@46953
   132
        !!y. y \<in> B ==> d(y): A;
paulson@46953
   133
        !!x. x \<in> A ==> d(c(x)) = x;
paulson@46953
   134
        !!y. y \<in> 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
wenzelm@63901
   140
lemma RepFun_bijective: "(\<forall>y\<in>x. \<exists>!y'. f(y') = f(y))
paulson@46953
   141
      ==> (\<lambda>z\<in>{f(y). y \<in> x}. THE y. f(y) = z) \<in> bij({f(y). y \<in> 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
wenzelm@60770
   147
subsection\<open>Identity Function\<close>
paulson@13176
   148
paulson@46953
   149
lemma idI [intro!]: "a \<in> 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@46953
   154
lemma idE [elim!]: "[| p \<in> id(A);  !!x.[| x \<in> 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@46953
   162
lemma id_conv [simp]: "x \<in> 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@46821
   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@46821
   189
lemma subset_iff_id: "A \<subseteq> B \<longleftrightarrow> 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
wenzelm@60770
   194
text\<open>@{term id} as the identity relation\<close>
paulson@46821
   195
lemma id_iff [simp]: "<x,y> \<in> id(A) \<longleftrightarrow> x=y & y \<in> A"
paulson@14060
   196
by auto
paulson@13176
   197
paulson@14060
   198
wenzelm@60770
   199
subsection\<open>Converse of a Function\<close>
paulson@13176
   200
paulson@46953
   201
lemma inj_converse_fun: "f \<in> 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
wenzelm@60770
   209
text\<open>Equations for converse(f)\<close>
paulson@13176
   210
wenzelm@60770
   211
text\<open>The premises are equivalent to saying that f is injective...\<close>
paulson@13176
   212
lemma left_inverse_lemma:
paulson@46953
   213
     "[| f \<in> A->B;  converse(f): C->A;  a \<in> A |] ==> converse(f)`(f`a) = a"
paulson@13176
   214
by (blast intro: apply_Pair apply_equality converseI)
paulson@13176
   215
paulson@46953
   216
lemma left_inverse [simp]: "[| f \<in> inj(A,B);  a \<in> 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@46953
   226
     "[| f \<in> A->B;  converse(f): C->A;  b \<in> C |] ==> f`(converse(f)`b) = b"
paulson@46821
   227
by (rule apply_Pair [THEN converseD [THEN apply_equality]], auto)
paulson@13176
   228
paulson@46953
   229
(*Should the premises be f \<in> surj(A,B), b \<in> 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@46953
   232
     "[| f \<in> inj(A,B);  b \<in> 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@46953
   235
lemma right_inverse_bij: "[| f \<in> bij(A,B);  b \<in> B |] ==> f`(converse(f)`b) = b"
paulson@13180
   236
by (force simp add: bij_def surj_range)
paulson@13176
   237
wenzelm@60770
   238
subsection\<open>Converses of Injections, Surjections, Bijections\<close>
paulson@13176
   239
paulson@46953
   240
lemma inj_converse_inj: "f \<in> inj(A,B) ==> converse(f): inj(range(f), A)"
paulson@13176
   241
apply (rule f_imp_injective)
paulson@46821
   242
apply (erule inj_converse_fun, clarify)
paulson@13180
   243
apply (rule right_inverse)
paulson@13176
   244
 apply assumption
paulson@46821
   245
apply blast
paulson@13176
   246
done
paulson@13176
   247
paulson@46953
   248
lemma inj_converse_surj: "f \<in> inj(A,B) ==> converse(f): surj(range(f), A)"
paulson@46821
   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
wenzelm@60770
   252
text\<open>Adding this as an intro! rule seems to cause looping\<close>
paulson@46953
   253
lemma bij_converse_bij [TC]: "f \<in> 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
wenzelm@60770
   260
subsection\<open>Composition of Two Relations\<close>
paulson@13176
   261
wenzelm@60770
   262
text\<open>The inductive definition package could derive these theorems for @{term"r O s"}\<close>
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@46821
   267
lemma compE [elim!]:
paulson@46821
   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@46821
   273
lemma compEpair:
paulson@46821
   274
    "[| <a,c> \<in> r O s;
paulson@13176
   275
        !!y. [| <a,y>:s;  <y,c>:r |] ==> P |]
paulson@13176
   276
     ==> P"
paulson@46821
   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
wenzelm@60770
   283
subsection\<open>Domain and Range -- see Suppes, Section 3.1\<close>
paulson@13176
   284
wenzelm@60770
   285
text\<open>Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327\<close>
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@46953
   301
lemma inj_inj_range: "f \<in> 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@46953
   304
lemma inj_bij_range: "f \<in> inj(A,B) ==> f \<in> bij(A,range(f))"
paulson@46821
   305
  by (auto simp add: bij_def intro: inj_inj_range inj_is_fun fun_is_surj)
paulson@41160
   306
paulson@13176
   307
wenzelm@60770
   308
subsection\<open>Other Results\<close>
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
wenzelm@60770
   313
text\<open>composition preserves relations\<close>
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
wenzelm@60770
   317
text\<open>associative law for composition\<close>
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@46821
   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
wenzelm@60770
   334
subsection\<open>Composition Preserves Functions, Injections, and Surjections\<close>
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
wenzelm@60770
   339
text\<open>Don't think the premises can be weakened much\<close>
paulson@46953
   340
lemma comp_fun: "[| g \<in> A->B;  f \<in> B->C |] ==> (f O g) \<in> A->C"
paulson@13176
   341
apply (auto simp add: Pi_def comp_function Pow_iff comp_rel)
paulson@46821
   342
apply (subst range_rel_subset [THEN domain_comp_eq], auto)
paulson@13176
   343
done
paulson@13176
   344
paulson@46953
   345
(*Thanks to the new definition of "apply", the premise f \<in> B->C is gone!*)
paulson@13176
   346
lemma comp_fun_apply [simp]:
paulson@46953
   347
     "[| g \<in> A->B;  a \<in> A |] ==> (f O g)`a = f`(g`a)"
paulson@46821
   348
apply (frule apply_Pair, assumption)
paulson@13176
   349
apply (simp add: apply_def image_comp)
paulson@46821
   350
apply (blast dest: apply_equality)
paulson@13176
   351
done
paulson@13176
   352
wenzelm@60770
   353
text\<open>Simplifies compositions of lambda-abstractions\<close>
paulson@46821
   354
lemma comp_lam:
paulson@46953
   355
    "[| !!x. x \<in> 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@46821
   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@46821
   361
 apply simp
paulson@46821
   362
apply (simp add: lam_type)
paulson@13176
   363
done
paulson@13176
   364
paulson@13176
   365
lemma comp_inj:
paulson@46953
   366
     "[| g \<in> inj(A,B);  f \<in> inj(B,C) |] ==> (f O g) \<in> inj(A,C)"
paulson@46821
   367
apply (frule inj_is_fun [of g])
paulson@46821
   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@46821
   370
 apply (blast intro: comp_fun, simp)
paulson@13176
   371
done
paulson@13176
   372
paulson@46821
   373
lemma comp_surj:
paulson@46953
   374
    "[| g \<in> surj(A,B);  f \<in> 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@46821
   379
lemma comp_bij:
paulson@46953
   380
    "[| g \<in> bij(A,B);  f \<in> 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
wenzelm@60770
   386
subsection\<open>Dual Properties of @{term inj} and @{term surj}\<close>
paulson@13356
   387
wenzelm@60770
   388
text\<open>Useful for proofs from
paulson@46821
   389
    D Pastre.  Automatic theorem proving in set theory.
wenzelm@60770
   390
    Artificial Intelligence, 10:1--27, 1978.\<close>
paulson@13176
   391
paulson@46821
   392
lemma comp_mem_injD1:
paulson@46953
   393
    "[| (f O g): inj(A,C);  g \<in> A->B;  f \<in> B->C |] ==> g \<in> inj(A,B)"
paulson@46821
   394
by (unfold inj_def, force)
paulson@13176
   395
paulson@46821
   396
lemma comp_mem_injD2:
paulson@46953
   397
    "[| (f O g): inj(A,C);  g \<in> surj(A,B);  f \<in> B->C |] ==> f \<in> 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@46821
   406
lemma comp_mem_surjD1:
paulson@46953
   407
    "[| (f O g): surj(A,C);  g \<in> A->B;  f \<in> B->C |] ==> f \<in> 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@46821
   413
lemma comp_mem_surjD2:
paulson@46953
   414
    "[| (f O g): surj(A,C);  g \<in> A->B;  f \<in> inj(B,C) |] ==> g \<in> surj(A,B)"
paulson@13180
   415
apply (unfold inj_def surj_def, safe)
paulson@46821
   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
wenzelm@60770
   420
subsubsection\<open>Inverses of Composition\<close>
paulson@13176
   421
wenzelm@60770
   422
text\<open>left inverse of composition; one inclusion is
wenzelm@60770
   423
        @{term "f \<in> A->B ==> id(A) \<subseteq> converse(f) O f"}\<close>
paulson@46953
   424
lemma left_comp_inverse: "f \<in> inj(A,B) ==> converse(f) O f = id(A)"
paulson@46821
   425
apply (unfold inj_def, clarify)
paulson@46821
   426
apply (rule equalityI)
paulson@46821
   427
 apply (auto simp add: apply_iff, blast)
paulson@13176
   428
done
paulson@13176
   429
wenzelm@60770
   430
text\<open>right inverse of composition; one inclusion is
wenzelm@60770
   431
                @{term "f \<in> A->B ==> f O converse(f) \<subseteq> id(B)"}\<close>
paulson@46821
   432
lemma right_comp_inverse:
paulson@46953
   433
    "f \<in> surj(A,B) ==> f O converse(f) = id(B)"
paulson@46821
   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
wenzelm@60770
   441
subsubsection\<open>Proving that a Function is a Bijection\<close>
paulson@13176
   442
paulson@46821
   443
lemma comp_eq_id_iff:
paulson@46953
   444
    "[| f \<in> A->B;  g \<in> B->A |] ==> f O g = id(B) \<longleftrightarrow> (\<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@46821
   453
lemma fg_imp_bijective:
paulson@46953
   454
    "[| f \<in> A->B;  g \<in> 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@46953
   460
lemma nilpotent_imp_bijective: "[| f \<in> 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@46953
   464
     "[| converse(f): B->A;  f \<in> A->B |] ==> f \<in> bij(A,B)"
paulson@46821
   465
by (simp add: fg_imp_bijective comp_eq_id_iff
paulson@13180
   466
              left_inverse_lemma right_inverse_lemma)
paulson@13176
   467
wenzelm@60770
   468
subsubsection\<open>Unions of Functions\<close>
paulson@13356
   469
wenzelm@60770
   470
text\<open>See similar theorems in func.thy\<close>
paulson@13176
   471
wenzelm@60770
   472
text\<open>Theorem by KG, proof by LCP\<close>
paulson@13176
   473
lemma inj_disjoint_Un:
paulson@46953
   474
     "[| f \<in> inj(A,B);  g \<in> inj(C,D);  B \<inter> D = 0 |]
paulson@46953
   475
      ==> (\<lambda>a\<in>A \<union> C. if a \<in> A then f`a else g`a) \<in> inj(A \<union> C, B \<union> D)"
paulson@46953
   476
apply (rule_tac d = "%z. if z \<in> 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@46821
   481
lemma surj_disjoint_Un:
paulson@46953
   482
    "[| f \<in> surj(A,B);  g \<in> surj(C,D);  A \<inter> C = 0 |]
paulson@46820
   483
     ==> (f \<union> g) \<in> surj(A \<union> C, B \<union> D)"
paulson@46821
   484
apply (simp add: surj_def fun_disjoint_Un)
paulson@46821
   485
apply (blast dest!: domain_of_fun
wenzelm@32960
   486
             intro!: fun_disjoint_apply1 fun_disjoint_apply2)
paulson@13176
   487
done
paulson@13176
   488
wenzelm@60770
   489
text\<open>A simple, high-level proof; the version for injections follows from it,
wenzelm@60770
   490
  using  @{term "f \<in> inj(A,B) \<longleftrightarrow> f \<in> bij(A,range(f))"}\<close>
paulson@13176
   491
lemma bij_disjoint_Un:
paulson@46953
   492
     "[| f \<in> bij(A,B);  g \<in> 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
wenzelm@60770
   500
subsubsection\<open>Restrictions as Surjections and Bijections\<close>
paulson@13176
   501
paulson@13176
   502
lemma surj_image:
paulson@46953
   503
    "f \<in> Pi(A,B) ==> f \<in> surj(A, f``A)"
paulson@46821
   504
apply (simp add: surj_def)
paulson@46821
   505
apply (blast intro: apply_equality apply_Pair Pi_type)
paulson@13176
   506
done
paulson@13176
   507
paulson@47101
   508
lemma surj_image_eq: "f \<in> surj(A, B) ==> f``A = B"
paulson@47101
   509
  by (auto simp add: surj_def image_fun) (blast dest: apply_type) 
paulson@47101
   510
paulson@46820
   511
lemma restrict_image [simp]: "restrict(f,A) `` B = f `` (A \<inter> B)"
paulson@13180
   512
by (auto simp add: restrict_def)
paulson@13176
   513
paulson@46821
   514
lemma restrict_inj:
paulson@46953
   515
    "[| f \<in> inj(A,B);  C<=A |] ==> restrict(f,C): inj(C,B)"
paulson@13176
   516
apply (unfold inj_def)
paulson@46821
   517
apply (safe elim!: restrict_type2, auto)
paulson@13176
   518
done
paulson@13176
   519
paulson@46953
   520
lemma restrict_surj: "[| f \<in> Pi(A,B);  C<=A |] ==> restrict(f,C): surj(C, f``C)"
paulson@13176
   521
apply (insert restrict_type2 [THEN surj_image])
paulson@46821
   522
apply (simp add: restrict_image)
paulson@13176
   523
done
paulson@13176
   524
paulson@46821
   525
lemma restrict_bij:
paulson@46953
   526
    "[| f \<in> inj(A,B);  C<=A |] ==> restrict(f,C): bij(C, f``C)"
paulson@13180
   527
apply (simp add: inj_def bij_def)
paulson@13180
   528
apply (blast intro: restrict_surj surj_is_fun)
paulson@13176
   529
done
paulson@13176
   530
paulson@13176
   531
wenzelm@60770
   532
subsubsection\<open>Lemmas for Ramsey's Theorem\<close>
paulson@13176
   533
paulson@46953
   534
lemma inj_weaken_type: "[| f \<in> inj(A,B);  B<=D |] ==> f \<in> inj(A,D)"
paulson@13176
   535
apply (unfold inj_def)
paulson@13176
   536
apply (blast intro: fun_weaken_type)
paulson@13176
   537
done
paulson@13176
   538
paulson@13176
   539
lemma inj_succ_restrict:
paulson@46953
   540
     "[| f \<in> inj(succ(m), A) |] ==> restrict(f,m) \<in> inj(m, A-{f`m})"
paulson@13269
   541
apply (rule restrict_bij [THEN bij_is_inj, THEN inj_weaken_type], assumption, blast)
paulson@13176
   542
apply (unfold inj_def)
paulson@13176
   543
apply (fast elim: range_type mem_irrefl dest: apply_equality)
paulson@13176
   544
done
paulson@13176
   545
paulson@13176
   546
paulson@46821
   547
lemma inj_extend:
paulson@46953
   548
    "[| f \<in> inj(A,B);  a\<notin>A;  b\<notin>B |]
paulson@46820
   549
     ==> cons(<a,b>,f) \<in> inj(cons(a,A), cons(b,B))"
paulson@13176
   550
apply (unfold inj_def)
paulson@13176
   551
apply (force intro: apply_type  simp add: fun_extend)
paulson@13176
   552
done
paulson@13176
   553
clasohm@0
   554
end